stake validator basics

This commit is contained in:
Emily Martins 2022-02-24 00:20:57 +01:00
parent 6f741b6dbe
commit e5afed2c46
4 changed files with 192 additions and 102 deletions

View file

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

View file

@ -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 $

View file

@ -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

View file

@ -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