From e5afed2c46026f094b2b8cadf77cf3eb3e4c3042 Mon Sep 17 00:00:00 2001 From: Emily Martins Date: Thu, 24 Feb 2022 00:20:57 +0100 Subject: [PATCH] stake validator basics --- bench/Main.hs | 1 + src/Agora/SafeMoney.hs | 36 +++------- src/Agora/Stake.hs | 149 +++++++++++++++++++++-------------------- src/Agora/Utils.hs | 108 ++++++++++++++++++++++++++++- 4 files changed, 192 insertions(+), 102 deletions(-) diff --git a/bench/Main.hs b/bench/Main.hs index 6fc2704..c03b5e4 100644 --- a/bench/Main.hs +++ b/bench/Main.hs @@ -25,4 +25,5 @@ benchmarks = "full_scripts" [ bench "authorityTokenPolicy" $ Agora.authorityTokenPolicy (Agora.AuthorityToken (Value.assetClass "" "")) , bench "stakePolicy" $ Agora.stakePolicy (Agora.Stake @Agora.LQ) + , bench "stakeValidator" $ Agora.stakeValidator (Agora.Stake @Agora.LQ) ] diff --git a/src/Agora/SafeMoney.hs b/src/Agora/SafeMoney.hs index f7abcaf..6124773 100644 --- a/src/Agora/SafeMoney.hs +++ b/src/Agora/SafeMoney.hs @@ -25,15 +25,10 @@ import Prelude -------------------------------------------------------------------------------- -import Plutus.V1.Ledger.Value (AssetClass (..)) -import Plutus.V1.Ledger.Value qualified as Ledger - --------------------------------------------------------------------------------- - import Plutarch.Api.V1 import Plutarch.Builtin import Plutarch.Internal -import Plutarch.Prelude +import Plutarch.Monadic qualified as P -------------------------------------------------------------------------------- @@ -55,26 +50,15 @@ newtype Discrete (mc :: MoneyClass) (s :: S) = Discrete (Term s PInteger) deriving (PlutusType, PIsData, PEq, POrd) via (DerivePNewtype (Discrete mc) PInteger) -instance Num (Term s (Discrete mc)) where - (+) x y = pcon $ - Discrete . unTermCont $ do - Discrete x' <- tcont $ pmatch x - Discrete y' <- tcont $ pmatch y - pure (x' + y') - abs x = pcon $ - Discrete . unTermCont $ do - Discrete x' <- tcont $ pmatch x - pure (abs x') - negate x = pcon $ - Discrete . unTermCont $ do - Discrete x' <- tcont $ pmatch x - pure (negate x') - (*) x y = pcon $ - Discrete . unTermCont $ do - Discrete x' <- tcont $ pmatch x - Discrete y' <- tcont $ pmatch y - pure (x' * y') - fromInteger = error "Tried to `fromInteger` for a Discrete type. use `discrete` quasiquoter instead." +-- In the future, this should use plutarch-numeric + +-- | Add two `Discrete` values of the same MoneyClass +paddDiscrete :: Term s (Discrete mc :--> Discrete mc :--> Discrete mc) +paddDiscrete = phoistAcyclic $ + plam $ \x y -> P.do + Discrete x' <- pmatch x + Discrete y' <- pmatch y + pcon (Discrete $ x' + y') (^*) :: Term s (Discrete mc) -> Term s PInteger -> Term s (Discrete mc) (^*) x y = pcon $ diff --git a/src/Agora/Stake.hs b/src/Agora/Stake.hs index 84f0b82..c9aac0a 100644 --- a/src/Agora/Stake.hs +++ b/src/Agora/Stake.hs @@ -1,10 +1,11 @@ +{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE UndecidableInstances #-} -- | Vote-lockable stake UTXOs holding GT module Agora.Stake ( - StakeDatum (..), - StakeAction (..), + PStakeDatum (..), + PStakeAction (..), Stake (..), stakePolicy, stakeValidator, @@ -22,6 +23,7 @@ import Prelude -------------------------------------------------------------------------------- +import Plutarch (popaque) import Plutarch.Api.V1 import Plutarch.DataRepr ( PDataFields, @@ -39,19 +41,19 @@ import Agora.Utils data Stake (gt :: MoneyClass) = Stake -data StakeAction (gt :: MoneyClass) (s :: S) +data PStakeAction (gt :: MoneyClass) (s :: S) = -- | Deposit or withdraw a discrete amount of the staked governance token - DepositWithdraw (Term s (PDataRecord '["delta" ':= Discrete gt])) + PDepositWithdraw (Term s (PDataRecord '["delta" ':= Discrete gt])) | -- | Destroy a stake, retrieving its LQ, the minimum ADA and any other assets - Destroy (Term s (PDataRecord '[])) + PDestroy (Term s (PDataRecord '[])) deriving stock (GHC.Generic) deriving anyclass (Generic) deriving anyclass (PIsDataRepr) deriving (PlutusType, PIsData) - via PIsDataReprInstances (StakeAction gt) + via PIsDataReprInstances (PStakeAction gt) -newtype StakeDatum (gt :: MoneyClass) (s :: S) = StakeDatum +newtype PStakeDatum (gt :: MoneyClass) (s :: S) = PStakeDatum { getStakeDatum :: ( Term s @@ -67,51 +69,7 @@ newtype StakeDatum (gt :: MoneyClass) (s :: S) = StakeDatum deriving anyclass (PIsDataRepr) deriving (PlutusType, PIsData, PDataFields) - via (PIsDataReprInstances (StakeDatum gt)) - --- | Check if any output matches the predicate -anyOutput :: - forall (datum :: PType) s. - ( PIsData datum - ) => - Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool) -anyOutput = phoistAcyclic $ - plam $ \txInfo' predicate -> P.do - txInfo <- pletFields @'["outputs"] txInfo' - pany - # ( plam $ \txOut'' -> P.do - PTxOut txOut' <- pmatch (pfromData txOut'') - txOut <- pletFields @'["value", "datumHash", "address"] txOut' - PDJust dh <- pmatch txOut.datumHash - pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \case - PJust datum -> P.do - predicate # txOut.value # txOut.address # pfromData datum - PNothing -> pcon PFalse - ) - # pfromData txInfo.outputs - --- | Check if any (resolved) input matches the predicate -anyInput :: - forall (datum :: PType) s. - ( PIsData datum - ) => - Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool) -anyInput = phoistAcyclic $ - plam $ \txInfo' predicate -> P.do - txInfo <- pletFields @'["inputs"] txInfo' - pany - # ( plam $ \txInInfo'' -> P.do - PTxInInfo txInInfo' <- pmatch (pfromData txInInfo'') - let txOut'' = pfield @"resolved" # txInInfo' - PTxOut txOut' <- pmatch (pfromData txOut'') - txOut <- pletFields @'["value", "datumHash", "address"] txOut' - PDJust dh <- pmatch txOut.datumHash - pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \case - PJust datum -> P.do - predicate # txOut.value # txOut.address # pfromData datum - PNothing -> pcon PFalse - ) - # pfromData txInfo.inputs + via (PIsDataReprInstances (PStakeDatum gt)) -------------------------------------------------------------------------------- -- @@ -135,7 +93,7 @@ stakePolicy :: , gt ~ '(ac, n, scale) ) => Stake gt -> - Term s (PData :--> PAsData PScriptContext :--> PUnit) + Term s PMintingPolicy stakePolicy _stake = plam $ \_redeemer ctx' -> P.do ctx <- pletFields @'["txInfo", "purpose"] ctx' @@ -144,36 +102,35 @@ stakePolicy _stake = PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose ownSymbol <- plet $ pfield @"_0" # ownSymbol' - valueSpent <- plet $ pvalueSpent # pfromData txInfo' + spentST <- plet $ psymbolValueOf # ownSymbol #$ pvalueSpent # pfromData txInfo' mintedST <- plet $ psymbolValueOf # ownSymbol # txInfo.mint - -- inputST <- plet $ stOf # (pvalueSpent # pfromData txInfo') let burning = P.do passert "ST at inputs must be 1" $ - psymbolValueOf # ownSymbol # valueSpent #== 1 + spentST #== 1 passert "ST burned" $ mintedST #== -1 passert "An unlocked input existed containing an ST" $ - anyInput @(StakeDatum gt) # pfromData txInfo' + anyInput @(PStakeDatum gt) # pfromData txInfo' #$ plam $ \value _ stakeDatum' -> P.do let hasST = psymbolValueOf # ownSymbol # value #== 1 let unlocked = pnot # (stakeLocked # stakeDatum') hasST #&& unlocked - pconstant () + popaque (pconstant ()) let minting = P.do passert "ST at inputs must be 0" $ - psymbolValueOf # ownSymbol # valueSpent #== 0 + spentST #== 0 passert "Minted ST must be exactly 1" $ mintedST #== 1 passert "A UTXO must exist with the correct output" $ - anyOutput @(StakeDatum gt) # pfromData txInfo' + anyOutput @(PStakeDatum gt) # pfromData txInfo' #$ plam $ \value address stakeDatum' -> P.do let cred = pfield @"credential" # address @@ -200,17 +157,10 @@ stakePolicy _stake = let valueCorrect = pdata value #== pdata expectedValue ownerSignsTransaction #&& valueCorrect - pconstant () + popaque (pconstant ()) pif (0 #< mintedST) minting burning --- | Check whether a Stake is locked. If it is locked, various actions are unavailable. -stakeLocked :: forall (gt :: MoneyClass) s. Term s (StakeDatum gt :--> PBool) -stakeLocked = phoistAcyclic $ - plam $ \_stakeDatum -> - -- TODO: when we extend this to support proposals, this will need to do something - pcon PFalse - -------------------------------------------------------------------------------- stakeValidator :: forall (gt :: MoneyClass) ac n scale s. @@ -219,11 +169,62 @@ stakeValidator :: , gt ~ '(ac, n, scale) ) => Stake gt -> - Term s (PData :--> PData :--> PAsData PScriptContext :--> PUnit) -stakeValidator _stake = + Term s PValidator +stakeValidator stake = plam $ \datum redeemer ctx' -> P.do - _ctx <- pletFields @'["txInfo", "purpose"] ctx' - let _stakeAction = punsafeCoerce redeemer :: Term s (StakeAction gt) - _stakeDatum <- pletFields @'["owner"] (punsafeCoerce datum :: Term s (StakeDatum gt)) + ctx <- pletFields @'["txInfo", "purpose"] ctx' + txInfo' <- plet ctx.txInfo + txInfo <- pletFields @'["mint", "inputs", "outputs"] txInfo' + let stakeAction = punsafeCoerce redeemer :: Term s (PStakeAction gt) + let stakeDatum' = punsafeCoerce datum :: Term s (PStakeDatum gt) + stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum' - pconstant () + PSpending txOutRef <- pmatch $ pfromData ctx.purpose + + PJust txInInfo <- pmatch $ pfindTxInByTxOutRef # (pfield @"_0" # txOutRef) # txInfo' + ownAddress <- plet $ pfield @"address" #$ pfield @"resolved" # txInInfo + let continuingValue = pfield @"value" #$ pfield @"resolved" # txInInfo + stCurrencySymbol <- plet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake) + mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfo.mint + spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfo' + + pmatch stakeAction $ \case + PDestroy _ -> P.do + passert "ST at inputs must be 1" $ + spentST #== 1 + passert "Should burn ST" $ + mintedST #== -1 + passert "Stake unlocked" $ + pnot #$ stakeLocked # stakeDatum' + popaque (pconstant ()) + PDepositWithdraw r -> P.do + passert "ST at inputs must be 1" $ + spentST #== 1 + passert "Stake unlocked" $ + pnot #$ stakeLocked # stakeDatum' + passert "A UTXO must exist with the correct output" $ + anyOutput @(PStakeDatum gt) # txInfo' + #$ plam + $ \value address newStakeDatum' -> P.do + newStakeDatum <- pletFields @'["owner", "stakedAmount"] newStakeDatum' + delta <- plet $ pfield @"delta" # r + let isScriptAddress = pdata address #== ownAddress + let correctOutputDatum = + stakeDatum.owner #== newStakeDatum.owner + #&& (paddDiscrete # stakeDatum.stakedAmount # delta) #== newStakeDatum.stakedAmount + let expectedValue = paddValue # continuingValue # (discreteValue # delta) + + -- TODO: As above, needs to be >=, rather than == + let correctValue = pdata value #== pdata expectedValue + isScriptAddress #&& correctOutputDatum #&& correctValue + + popaque (pconstant ()) + +-------------------------------------------------------------------------------- + +-- | Check whether a Stake is locked. If it is locked, various actions are unavailable. +stakeLocked :: forall (gt :: MoneyClass) s. Term s (PStakeDatum gt :--> PBool) +stakeLocked = phoistAcyclic $ + plam $ \_stakeDatum -> + -- TODO: when we extend this to support proposals, this will need to do something + pcon PFalse diff --git a/src/Agora/Utils.hs b/src/Agora/Utils.hs index dd6ff8c..47160a6 100644 --- a/src/Agora/Utils.hs +++ b/src/Agora/Utils.hs @@ -1,5 +1,25 @@ -- | Plutarch utility functions that should be upstreamed or don't belong anywhere else -module Agora.Utils (module Agora.Utils) where +module Agora.Utils ( + -- * Validator-level utility functions + passert, + pfind', + pfindDatum, + pfindDatum', + pvalueSpent, + ptxSignedBy, + paddValue, + plookup, + pfromMaybe, + psymbolValueOf, + passetClassValueOf, + passetClassValueOf', + pfindTxInByTxOutRef, + pfindMap, + + -- * Functions which should (probably) not be upstreamed + anyOutput, + anyInput, +) where -------------------------------------------------------------------------------- @@ -8,16 +28,19 @@ import Plutus.V1.Ledger.Value (AssetClass (..)) -------------------------------------------------------------------------------- import Plutarch.Api.V1 ( + PAddress, PCurrencySymbol, PDatum, PDatumHash, PMap (PMap), + PMaybeData (PDJust), PPubKeyHash, PTokenName, PTuple, PTxInInfo (PTxInInfo), PTxInfo (PTxInfo), PTxOut (PTxOut), + PTxOutRef, PValue (PValue), ) import Plutarch.Builtin (ppairDataBuiltin) @@ -25,6 +48,7 @@ import Plutarch.Internal (punsafeCoerce) import Plutarch.Monadic qualified as P -------------------------------------------------------------------------------- +-- Validator-level utility functions -- | Assert a particular bool, trace on falsehood. Use in monadic context passert :: Term s PString -> Term s PBool -> Term s k -> Term s k @@ -58,6 +82,22 @@ pfind' p = (\self x xs -> pif (p x) (pcon (PJust x)) (self # xs)) (const $ pcon PNothing) +-- | Get the first element that maps to a PJust in a list +pfindMap :: + PIsListLike list a => + Term s ((a :--> PMaybe b) :--> list a :--> PMaybe b) +pfindMap = + phoistAcyclic $ + plam $ \p -> + precList + ( \self x xs -> + -- In the future, this should use `pmatchSum`, I believe? + pmatch (p # x) $ \case + PNothing -> self # xs + PJust v -> pcon (PJust v) + ) + (const $ pcon PNothing) + -- | Find the value for a given key in an assoclist plookup :: (PEq a, PIsListLike list (PBuiltinPair a b)) => @@ -106,6 +146,7 @@ psymbolValueOf = PMap m <- pmatch (pfromData m') pfoldr # (plam $ \x v -> (pfromData $ psndBuiltin # x) + v) # 0 # m +-- | Extract amount from PValue belonging to a Plutarch-level asset class passetClassValueOf :: Term s (PCurrencySymbol :--> PTokenName :--> PValue :--> PInteger) passetClassValueOf = @@ -136,7 +177,7 @@ pmapUnionWith = phoistAcyclic $ pf <- plet $ pfstBuiltin # p ps <- plet $ psndBuiltin # p pmatch (plookup # pf # ys) $ \case - PJust v -> P.do + PJust v -> -- Data conversions here are silly, aren't they? ppairDataBuiltin # pf # (pdata (f # pfromData ps # pfromData v)) PNothing -> p @@ -177,3 +218,66 @@ pvalueSpent = phoistAcyclic $ ) # pconstant mempty # (pfield @"inputs" # txInfo) + +-- | Find the TxInInfo by a TxOutRef +pfindTxInByTxOutRef :: Term s (PTxOutRef :--> PTxInfo :--> PMaybe PTxInInfo) +pfindTxInByTxOutRef = phoistAcyclic $ + plam $ \txOutRef txInfo' -> + pmatch txInfo' $ \(PTxInfo txInfo) -> + pfindMap + # ( plam $ \txInInfo' -> + plet (pfromData txInInfo') $ \r -> + pmatch r $ \(PTxInInfo txInInfo) -> + pif + (pdata txOutRef #== pfield @"outRef" # txInInfo) + (pcon (PJust r)) + (pcon PNothing) + ) + #$ (pfield @"inputs" # txInfo) + +-------------------------------------------------------------------------------- +-- Functions which should (probably) not be upstreamed + +-- | Check if any output matches the predicate +anyOutput :: + forall (datum :: PType) s. + ( PIsData datum + ) => + Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool) +anyOutput = phoistAcyclic $ + plam $ \txInfo' predicate -> P.do + txInfo <- pletFields @'["outputs"] txInfo' + pany + # ( plam $ \txOut'' -> P.do + PTxOut txOut' <- pmatch (pfromData txOut'') + txOut <- pletFields @'["value", "datumHash", "address"] txOut' + PDJust dh <- pmatch txOut.datumHash + pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \case + PJust datum -> P.do + predicate # txOut.value # txOut.address # pfromData datum + PNothing -> pcon PFalse + ) + # pfromData txInfo.outputs + +-- | Check if any (resolved) input matches the predicate +anyInput :: + forall (datum :: PType) s. + ( PIsData datum + ) => + Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool) +anyInput = phoistAcyclic $ + plam $ \txInfo' predicate -> P.do + txInfo <- pletFields @'["inputs"] txInfo' + pany + # ( plam $ \txInInfo'' -> P.do + PTxInInfo txInInfo' <- pmatch (pfromData txInInfo'') + let txOut'' = pfield @"resolved" # txInInfo' + PTxOut txOut' <- pmatch (pfromData txOut'') + txOut <- pletFields @'["value", "datumHash", "address"] txOut' + PDJust dh <- pmatch txOut.datumHash + pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo') $ \case + PJust datum -> P.do + predicate # txOut.value # txOut.address # pfromData datum + PNothing -> pcon PFalse + ) + # pfromData txInfo.inputs