stake validator basics

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)
     ]

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
+-- In the future, this should use plutarch-numeric
-  (+) x y = pcon $
+
-    Discrete . unTermCont $ do
+-- | Add two `Discrete` values of the same MoneyClass
-      Discrete x' <- tcont $ pmatch x
+paddDiscrete :: Term s (Discrete mc :--> Discrete mc :--> Discrete mc)
-      Discrete y' <- tcont $ pmatch y
+paddDiscrete = phoistAcyclic $
-      pure (x' + y')
+  plam $ \x y -> P.do
-  abs x = pcon $
+    Discrete x' <- pmatch x
-    Discrete . unTermCont $ do
+    Discrete y' <- pmatch y
-      Discrete x' <- tcont $ pmatch x
+    pcon (Discrete $ x' + y')
-      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."
 
 (^*) :: Term s (Discrete mc) -> Term s PInteger -> Term s (Discrete mc)
 (^*) x y = pcon $

src/Agora/Stake.hs

@@ -1,10 +1,11 @@
+{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- | Vote-lockable stake UTXOs holding GT
 module Agora.Stake (
-  StakeDatum (..),
+  PStakeDatum (..),
-  StakeAction (..),
+  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))
+    via (PIsDataReprInstances (PStakeDatum 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
 
 --------------------------------------------------------------------------------
 --
@@ -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)
+  Term s PValidator
-stakeValidator _stake =
+stakeValidator stake =
   plam $ \datum redeemer ctx' -> P.do
-    _ctx <- pletFields @'["txInfo", "purpose"] ctx'
+    ctx <- pletFields @'["txInfo", "purpose"] ctx'
-    let _stakeAction = punsafeCoerce redeemer :: Term s (StakeAction gt)
+    txInfo' <- plet ctx.txInfo
-    _stakeDatum <- pletFields @'["owner"] (punsafeCoerce datum :: Term s (StakeDatum gt))
+    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

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