remove all instances of P.do in favour of TermCont.
This commit is contained in:
Emily Martins
parent
2a0c6eb4a6
commit
1bd6030855
14 changed files with 671 additions and 639 deletions
|
|
@ -24,7 +24,6 @@ import Plutarch.Api.V1 (
|
|||
import Plutarch.Api.V1.AssocMap (PMap (PMap))
|
||||
import Plutarch.Api.V1.Value (PValue (PValue))
|
||||
import Plutarch.Builtin (pforgetData)
|
||||
import Plutarch.Monadic qualified as P
|
||||
import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
|
||||
|
||||
import Prelude
|
||||
|
|
@ -33,10 +32,11 @@ import Prelude
|
|||
|
||||
import Agora.Utils (
|
||||
allOutputs,
|
||||
passert,
|
||||
plookup,
|
||||
psymbolValueOf,
|
||||
ptokenSpent,
|
||||
tcassert,
|
||||
tcmatch,
|
||||
)
|
||||
import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
|
||||
|
||||
|
|
@ -66,30 +66,32 @@ newtype AuthorityToken = AuthorityToken
|
|||
-}
|
||||
authorityTokensValidIn :: Term s (PCurrencySymbol :--> PTxOut :--> PBool)
|
||||
authorityTokensValidIn = phoistAcyclic $
|
||||
plam $ \authorityTokenSym txOut'' -> P.do
|
||||
PTxOut txOut' <- pmatch txOut''
|
||||
txOut <- pletFields @'["address", "value"] $ txOut'
|
||||
PAddress address <- pmatch txOut.address
|
||||
PValue value' <- pmatch txOut.value
|
||||
PMap value <- pmatch value'
|
||||
pmatch (plookup # pdata authorityTokenSym # value) $ \case
|
||||
PJust (pfromData -> tokenMap') ->
|
||||
pmatch (pfield @"credential" # address) $ \case
|
||||
PPubKeyCredential _ ->
|
||||
-- GATs should only be sent to Effect validators
|
||||
ptraceIfFalse "authorityTokensValidIn: GAT incorrectly lives at PubKey" $ pconstant False
|
||||
PScriptCredential ((pfromData . (pfield @"_0" #)) -> cred) -> P.do
|
||||
PMap tokenMap <- pmatch tokenMap'
|
||||
ptraceIfFalse "authorityTokensValidIn: GAT TokenName doesn't match ScriptHash" $
|
||||
pall
|
||||
# plam
|
||||
( \pair ->
|
||||
pforgetData (pfstBuiltin # pair) #== pforgetData (pdata cred)
|
||||
)
|
||||
# tokenMap
|
||||
PNothing ->
|
||||
-- No GATs exist at this output!
|
||||
pconstant True
|
||||
plam $ \authorityTokenSym txOut'' -> unTermCont $ do
|
||||
PTxOut txOut' <- tcmatch txOut''
|
||||
txOut <- tcont $ pletFields @'["address", "value"] $ txOut'
|
||||
PAddress address <- tcmatch txOut.address
|
||||
PValue value' <- tcmatch txOut.value
|
||||
PMap value <- tcmatch value'
|
||||
pure $
|
||||
pmatch (plookup # pdata authorityTokenSym # value) $ \case
|
||||
PJust (pfromData -> tokenMap') ->
|
||||
pmatch (pfield @"credential" # address) $ \case
|
||||
PPubKeyCredential _ ->
|
||||
-- GATs should only be sent to Effect validators
|
||||
ptraceIfFalse "authorityTokensValidIn: GAT incorrectly lives at PubKey" $ pconstant False
|
||||
PScriptCredential ((pfromData . (pfield @"_0" #)) -> cred) -> unTermCont $ do
|
||||
PMap tokenMap <- tcmatch tokenMap'
|
||||
pure $
|
||||
ptraceIfFalse "authorityTokensValidIn: GAT TokenName doesn't match ScriptHash" $
|
||||
pall
|
||||
# plam
|
||||
( \pair ->
|
||||
pforgetData (pfstBuiltin # pair) #== pforgetData (pdata cred)
|
||||
)
|
||||
# tokenMap
|
||||
PNothing ->
|
||||
-- No GATs exist at this output!
|
||||
pconstant True
|
||||
|
||||
-- | Assert that a single authority token has been burned.
|
||||
singleAuthorityTokenBurned ::
|
||||
|
|
@ -98,25 +100,26 @@ singleAuthorityTokenBurned ::
|
|||
Term s (PAsData PTxInfo) ->
|
||||
Term s PValue ->
|
||||
Term s PBool
|
||||
singleAuthorityTokenBurned gatCs txInfo mint = P.do
|
||||
singleAuthorityTokenBurned gatCs txInfo mint = unTermCont $ do
|
||||
let gatAmountMinted :: Term _ PInteger
|
||||
gatAmountMinted = psymbolValueOf # gatCs # mint
|
||||
|
||||
txInfoF <- pletFields @'["inputs"] $ txInfo
|
||||
txInfoF <- tcont $ pletFields @'["inputs"] $ txInfo
|
||||
|
||||
foldr1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "singleAuthorityTokenBurned: Must burn exactly 1 GAT" $ gatAmountMinted #== -1
|
||||
, ptraceIfFalse "singleAuthorityTokenBurned: All GAT tokens must be valid at the inputs" $
|
||||
pall
|
||||
# plam
|
||||
( \txInInfo' -> P.do
|
||||
PTxInInfo txInInfo <- pmatch (pfromData txInInfo')
|
||||
let txOut' = pfield @"resolved" # txInInfo
|
||||
authorityTokensValidIn # gatCs # pfromData txOut'
|
||||
)
|
||||
# txInfoF.inputs
|
||||
]
|
||||
pure $
|
||||
foldr1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "singleAuthorityTokenBurned: Must burn exactly 1 GAT" $ gatAmountMinted #== -1
|
||||
, ptraceIfFalse "singleAuthorityTokenBurned: All GAT tokens must be valid at the inputs" $
|
||||
pall
|
||||
# plam
|
||||
( \txInInfo' -> unTermCont $ do
|
||||
PTxInInfo txInInfo <- tcmatch (pfromData txInInfo')
|
||||
let txOut' = pfield @"resolved" # txInInfo
|
||||
pure $ authorityTokensValidIn # gatCs # pfromData txOut'
|
||||
)
|
||||
# txInfoF.inputs
|
||||
]
|
||||
|
||||
-- | Policy given 'AuthorityToken' params.
|
||||
authorityTokenPolicy ::
|
||||
|
|
@ -124,29 +127,31 @@ authorityTokenPolicy ::
|
|||
Term s (PData :--> PScriptContext :--> PUnit)
|
||||
authorityTokenPolicy params =
|
||||
plam $ \_redeemer ctx' ->
|
||||
pmatch ctx' $ \(PScriptContext ctx') -> P.do
|
||||
ctx <- pletFields @'["txInfo", "purpose"] ctx'
|
||||
PTxInfo txInfo' <- pmatch $ pfromData ctx.txInfo
|
||||
txInfo <- pletFields @'["inputs", "mint"] txInfo'
|
||||
pmatch ctx' $ \(PScriptContext ctx') -> unTermCont $ do
|
||||
ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
|
||||
PTxInfo txInfo' <- tcmatch $ pfromData ctx.txInfo
|
||||
txInfo <- tcont $ pletFields @'["inputs", "mint"] txInfo'
|
||||
let inputs = txInfo.inputs
|
||||
mintedValue = pfromData txInfo.mint
|
||||
AssetClass (govCs, govTn) = params.authority
|
||||
govAc = passetClass # pconstant govCs # pconstant govTn
|
||||
govTokenSpent = ptokenSpent # govAc # inputs
|
||||
|
||||
PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose
|
||||
PMinting ownSymbol' <- tcmatch $ pfromData ctx.purpose
|
||||
|
||||
let ownSymbol = pfromData $ pfield @"_0" # ownSymbol'
|
||||
mintedATs = passetClassValueOf # mintedValue # (passetClass # ownSymbol # pconstant "")
|
||||
pif
|
||||
(0 #< mintedATs)
|
||||
( P.do
|
||||
passert "Parent token did not move in minting GATs" govTokenSpent
|
||||
passert "All outputs only emit valid GATs" $
|
||||
allOutputs @PData # pfromData ctx.txInfo #$ plam $ \txOut _value _address _datum ->
|
||||
authorityTokensValidIn
|
||||
# ownSymbol
|
||||
# txOut
|
||||
pconstant ()
|
||||
)
|
||||
(pconstant ())
|
||||
pure $
|
||||
pif
|
||||
(0 #< mintedATs)
|
||||
( unTermCont $ do
|
||||
tcassert "Parent token did not move in minting GATs" govTokenSpent
|
||||
tcassert "All outputs only emit valid GATs" $
|
||||
allOutputs @PData # pfromData ctx.txInfo #$ plam $ \txOut _value _address _datum ->
|
||||
authorityTokensValidIn
|
||||
# ownSymbol
|
||||
# txOut
|
||||
|
||||
pure $ pconstant ()
|
||||
)
|
||||
(pconstant ())
|
||||
|
|
|
|||
|
|
@ -8,10 +8,9 @@ Helpers for constructing effects.
|
|||
module Agora.Effect (makeEffect) where
|
||||
|
||||
import Agora.AuthorityToken (singleAuthorityTokenBurned)
|
||||
import Agora.Utils (passert)
|
||||
import Agora.Utils (tcassert, tclet, tcmatch, tctryFrom)
|
||||
import Plutarch.Api.V1 (PCurrencySymbol, PScriptPurpose (PSpending), PTxInfo, PTxOutRef, PValidator, PValue)
|
||||
import Plutarch.Monadic qualified as P
|
||||
import Plutarch.TryFrom (PTryFrom, ptryFrom)
|
||||
import Plutarch.TryFrom (PTryFrom)
|
||||
import Plutus.V1.Ledger.Value (CurrencySymbol)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
|
@ -29,28 +28,28 @@ makeEffect ::
|
|||
(forall (s :: S). Term s PCurrencySymbol -> Term s datum -> Term s PTxOutRef -> Term s (PAsData PTxInfo) -> Term s POpaque) ->
|
||||
ClosedTerm PValidator
|
||||
makeEffect gatCs' f =
|
||||
plam $ \datum _redeemer ctx' -> P.do
|
||||
ctx <- pletFields @'["txInfo", "purpose"] ctx'
|
||||
txInfo' <- plet ctx.txInfo
|
||||
plam $ \datum _redeemer ctx' -> unTermCont $ do
|
||||
ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
|
||||
txInfo' <- tclet ctx.txInfo
|
||||
|
||||
-- convert input datum, PData, into desierable type
|
||||
-- the way this conversion is performed should be defined
|
||||
-- by PTryFrom for each datum in effect script.
|
||||
(datum', _) <- ptryFrom @datum datum
|
||||
(datum', _) <- tctryFrom @datum datum
|
||||
|
||||
-- ensure purpose is Spending.
|
||||
PSpending txOutRef <- pmatch $ pfromData ctx.purpose
|
||||
txOutRef' <- plet (pfield @"_0" # txOutRef)
|
||||
PSpending txOutRef <- tcmatch $ pfromData ctx.purpose
|
||||
txOutRef' <- tclet (pfield @"_0" # txOutRef)
|
||||
|
||||
-- fetch minted values to ensure single GAT is burned
|
||||
txInfo <- pletFields @'["mint"] txInfo'
|
||||
txInfo <- tcont $ pletFields @'["mint"] txInfo'
|
||||
let mint :: Term _ PValue
|
||||
mint = txInfo.mint
|
||||
|
||||
-- fetch script context
|
||||
gatCs <- plet $ pconstant gatCs'
|
||||
gatCs <- tclet $ pconstant gatCs'
|
||||
|
||||
passert "A single authority token has been burned" $ singleAuthorityTokenBurned gatCs txInfo' mint
|
||||
tcassert "A single authority token has been burned" $ singleAuthorityTokenBurned gatCs txInfo' mint
|
||||
|
||||
-- run effect function
|
||||
f gatCs datum' txOutRef' txInfo'
|
||||
pure $ f gatCs datum' txOutRef' txInfo'
|
||||
|
|
|
|||
|
|
@ -29,5 +29,4 @@ instance PTryFrom PData PNoOp where
|
|||
-- | Dummy effect which can only burn its GAT.
|
||||
noOpValidator :: CurrencySymbol -> ClosedTerm PValidator
|
||||
noOpValidator curr = makeEffect curr $
|
||||
\_ (_datum :: Term s PNoOp) _ _ -> P.do
|
||||
popaque (pconstant ())
|
||||
\_ (_datum :: Term s PNoOp) _ _ -> popaque (pconstant ())
|
||||
|
|
|
|||
|
|
@ -18,7 +18,7 @@ import GHC.Generics qualified as GHC
|
|||
import Generics.SOP (Generic, I (I))
|
||||
|
||||
import Agora.Effect (makeEffect)
|
||||
import Agora.Utils (findTxOutByTxOutRef, paddValue, passert)
|
||||
import Agora.Utils (findTxOutByTxOutRef, paddValue, tcassert, tclet, tcmatch)
|
||||
import Plutarch.Api.V1 (
|
||||
PCredential (..),
|
||||
PTuple,
|
||||
|
|
@ -34,7 +34,6 @@ import Plutarch.DataRepr (
|
|||
PIsDataReprInstances (..),
|
||||
)
|
||||
import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (..))
|
||||
import Plutarch.Monadic qualified as P
|
||||
import Plutarch.TryFrom (PTryFrom (..))
|
||||
import Plutus.V1.Ledger.Credential (Credential)
|
||||
import Plutus.V1.Ledger.Value (CurrencySymbol, Value)
|
||||
|
|
@ -106,29 +105,29 @@ instance PTryFrom PData PTreasuryWithdrawalDatum where
|
|||
-}
|
||||
treasuryWithdrawalValidator :: forall {s :: S}. CurrencySymbol -> Term s PValidator
|
||||
treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
|
||||
\_cs (datum' :: Term _ PTreasuryWithdrawalDatum) txOutRef' txInfo' -> P.do
|
||||
datum <- pletFields @'["receivers", "treasuries"] datum'
|
||||
txInfo <- pletFields @'["outputs", "inputs"] txInfo'
|
||||
PJust txOut <- pmatch $ findTxOutByTxOutRef # txOutRef' # pfromData txInfo.inputs
|
||||
effInput <- pletFields @'["address", "value"] $ txOut
|
||||
\_cs (datum' :: Term _ PTreasuryWithdrawalDatum) txOutRef' txInfo' -> unTermCont $ do
|
||||
datum <- tcont $ pletFields @'["receivers", "treasuries"] datum'
|
||||
txInfo <- tcont $ pletFields @'["outputs", "inputs"] txInfo'
|
||||
PJust txOut <- tcmatch $ findTxOutByTxOutRef # txOutRef' # pfromData txInfo.inputs
|
||||
effInput <- tcont $ pletFields @'["address", "value"] $ txOut
|
||||
outputValues <-
|
||||
plet $
|
||||
tclet $
|
||||
pmap
|
||||
# plam
|
||||
( \(pfromData -> txOut') -> P.do
|
||||
txOut <- pletFields @'["address", "value"] $ txOut'
|
||||
( \(pfromData -> txOut') -> unTermCont $ do
|
||||
txOut <- tcont $ pletFields @'["address", "value"] $ txOut'
|
||||
let cred = pfield @"credential" # pfromData txOut.address
|
||||
pdata $ ptuple # cred # txOut.value
|
||||
pure . pdata $ ptuple # cred # txOut.value
|
||||
)
|
||||
# txInfo.outputs
|
||||
inputValues <-
|
||||
plet $
|
||||
tclet $
|
||||
pmap
|
||||
# plam
|
||||
( \((pfield @"resolved" #) . pfromData -> txOut') -> P.do
|
||||
txOut <- pletFields @'["address", "value"] $ txOut'
|
||||
( \((pfield @"resolved" #) . pfromData -> txOut') -> unTermCont $ do
|
||||
txOut <- tcont $ pletFields @'["address", "value"] $ txOut'
|
||||
let cred = pfield @"credential" # pfromData txOut.address
|
||||
pdata $ ptuple # cred # txOut.value
|
||||
pure . pdata $ ptuple # cred # txOut.value
|
||||
)
|
||||
# txInfo.inputs
|
||||
let ofTreasury =
|
||||
|
|
@ -141,10 +140,11 @@ treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
|
|||
treasuryInputValuesSum = sumValues #$ ofTreasury # inputValues
|
||||
treasuryOutputValuesSum = sumValues #$ ofTreasury # outputValues
|
||||
receiverValuesSum = sumValues # datum.receivers
|
||||
isPubkey = plam $ \cred -> P.do
|
||||
pmatch cred $ \case
|
||||
PPubKeyCredential _ -> pcon PTrue
|
||||
PScriptCredential _ -> pcon PFalse
|
||||
isPubkey = plam $ \cred ->
|
||||
pmatch cred $
|
||||
\case
|
||||
PPubKeyCredential _ -> pcon PTrue
|
||||
PScriptCredential _ -> pcon PFalse
|
||||
|
||||
-- Constraints
|
||||
outputContentMatchesRecivers =
|
||||
|
|
@ -169,8 +169,8 @@ treasuryWithdrawalValidator currSymbol = makeEffect currSymbol $
|
|||
)
|
||||
# inputValues
|
||||
|
||||
passert "Transaction should not pay to effects" shouldNotPayToEffect
|
||||
passert "Transaction output does not match receivers" outputContentMatchesRecivers
|
||||
passert "Remainders should be returned to the treasury" excessShouldBePaidToInputs
|
||||
passert "Transaction should only have treasuries specified in the datum as input" inputsAreOnlyTreasuriesOrCollateral
|
||||
popaque $ pconstant ()
|
||||
tcassert "Transaction should not pay to effects" shouldNotPayToEffect
|
||||
tcassert "Transaction output does not match receivers" outputContentMatchesRecivers
|
||||
tcassert "Remainders should be returned to the treasury" excessShouldBePaidToInputs
|
||||
tcassert "Transaction should only have treasuries specified in the datum as input" inputsAreOnlyTreasuriesOrCollateral
|
||||
pure . popaque $ pconstant ()
|
||||
|
|
|
|||
|
|
@ -58,11 +58,9 @@ data Governor
|
|||
-- | Policy for Governors.
|
||||
governorPolicy :: Governor -> ClosedTerm PMintingPolicy
|
||||
governorPolicy _ =
|
||||
plam $ \_redeemer _ctx' -> P.do
|
||||
popaque (pconstant ())
|
||||
plam $ \_redeemer _ctx' -> popaque (pconstant ())
|
||||
|
||||
-- | Validator for Governors.
|
||||
governorValidator :: Governor -> ClosedTerm PValidator
|
||||
governorValidator _ =
|
||||
plam $ \_datum _redeemer _ctx' -> P.do
|
||||
popaque (pconstant ())
|
||||
plam $ \_datum _redeemer _ctx' -> popaque (pconstant ())
|
||||
|
|
|
|||
|
|
@ -28,7 +28,6 @@ import Plutarch.Lift (
|
|||
PLifted,
|
||||
PUnsafeLiftDecl,
|
||||
)
|
||||
import Plutarch.Monadic qualified as P
|
||||
|
||||
import Plutus.V1.Ledger.Crypto (PubKeyHash)
|
||||
import PlutusTx qualified
|
||||
|
|
@ -88,14 +87,15 @@ validatedByMultisig params =
|
|||
pvalidatedByMultisig :: Term s (PMultiSig :--> PTxInfo :--> PBool)
|
||||
pvalidatedByMultisig =
|
||||
phoistAcyclic $
|
||||
plam $ \multi' txInfo -> P.do
|
||||
multi <- pletFields @'["keys", "minSigs"] multi'
|
||||
plam $ \multi' txInfo -> unTermCont $ do
|
||||
multi <- tcont $ pletFields @'["keys", "minSigs"] multi'
|
||||
let signatories = pfield @"signatories" # txInfo
|
||||
pfromData multi.minSigs
|
||||
#<= ( plength #$ pfilter
|
||||
# plam
|
||||
( \a ->
|
||||
pelem # a # pfromData signatories
|
||||
)
|
||||
# multi.keys
|
||||
)
|
||||
pure $
|
||||
pfromData multi.minSigs
|
||||
#<= ( plength #$ pfilter
|
||||
# plam
|
||||
( \a ->
|
||||
pelem # a # pfromData signatories
|
||||
)
|
||||
# multi.keys
|
||||
)
|
||||
|
|
|
|||
|
|
@ -55,7 +55,6 @@ import Plutarch.Lift (
|
|||
PConstantDecl,
|
||||
PUnsafeLiftDecl (..),
|
||||
)
|
||||
import Plutarch.Monadic qualified as P
|
||||
import Plutarch.SafeMoney (PDiscrete, Tagged)
|
||||
import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
|
||||
import Plutarch.Unsafe (punsafeCoerce)
|
||||
|
|
@ -412,8 +411,8 @@ deriving via (DerivePConstantViaData ProposalRedeemer PProposalRedeemer) instanc
|
|||
proposalDatumValid :: Proposal -> Term s (Agora.Proposal.PProposalDatum :--> PBool)
|
||||
proposalDatumValid proposal =
|
||||
phoistAcyclic $
|
||||
plam $ \datum' -> P.do
|
||||
datum <- pletFields @'["effects", "cosigners", "votes"] $ datum'
|
||||
plam $ \datum' -> unTermCont $ do
|
||||
datum <- tcont $ pletFields @'["effects", "cosigners", "votes"] $ datum'
|
||||
|
||||
let effects :: Term _ (PBuiltinMap Agora.Proposal.PResultTag (PBuiltinMap Plutarch.Api.V1.PValidatorHash Plutarch.Api.V1.PDatumHash))
|
||||
effects =
|
||||
|
|
@ -427,10 +426,11 @@ proposalDatumValid proposal =
|
|||
atLeastOneNegativeResult =
|
||||
pany # plam (\pair -> pnull #$ pfromData $ psndBuiltin # pair) # effects
|
||||
|
||||
foldr1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "Proposal has at least one ResultTag has no effects" atLeastOneNegativeResult
|
||||
, ptraceIfFalse "Proposal has at least one cosigner" $ pnotNull # pfromData datum.cosigners
|
||||
, ptraceIfFalse "Proposal has fewer cosigners than the limit" $ plength # (pfromData datum.cosigners) #<= pconstant proposal.maximumCosigners
|
||||
, ptraceIfFalse "Proposal votes and effects are compatible with each other" $ pkeysEqual # datum.effects # pto (pfromData datum.votes)
|
||||
]
|
||||
pure $
|
||||
foldr1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "Proposal has at least one ResultTag has no effects" atLeastOneNegativeResult
|
||||
, ptraceIfFalse "Proposal has at least one cosigner" $ pnotNull # pfromData datum.cosigners
|
||||
, ptraceIfFalse "Proposal has fewer cosigners than the limit" $ plength # (pfromData datum.cosigners) #<= pconstant proposal.maximumCosigners
|
||||
, ptraceIfFalse "Proposal votes and effects are compatible with each other" $ pkeysEqual # datum.effects # pto (pfromData datum.votes)
|
||||
]
|
||||
|
|
|
|||
|
|
@ -21,12 +21,15 @@ import Agora.Utils (
|
|||
anyOutput,
|
||||
findTxOutByTxOutRef,
|
||||
getMintingPolicySymbol,
|
||||
passert,
|
||||
pisUniq,
|
||||
psymbolValueOf,
|
||||
ptokenSpent,
|
||||
ptxSignedBy,
|
||||
pvalueSpent,
|
||||
tcassert,
|
||||
tclet,
|
||||
tcmatch,
|
||||
tctryFrom,
|
||||
)
|
||||
import Plutarch.Api.V1 (
|
||||
PMintingPolicy,
|
||||
|
|
@ -36,8 +39,6 @@ import Plutarch.Api.V1 (
|
|||
PValidator,
|
||||
)
|
||||
import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
|
||||
import Plutarch.Monadic qualified as P
|
||||
import Plutarch.TryFrom (ptryFrom)
|
||||
import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
|
||||
|
||||
{- | Policy for Proposals.
|
||||
|
|
@ -60,32 +61,32 @@ import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
|
|||
-}
|
||||
proposalPolicy :: Proposal -> ClosedTerm PMintingPolicy
|
||||
proposalPolicy proposal =
|
||||
plam $ \_redeemer ctx' -> P.do
|
||||
PScriptContext ctx' <- pmatch ctx'
|
||||
ctx <- pletFields @'["txInfo", "purpose"] ctx'
|
||||
PTxInfo txInfo' <- pmatch $ pfromData ctx.txInfo
|
||||
txInfo <- pletFields @'["inputs", "mint"] txInfo'
|
||||
PMinting _ownSymbol <- pmatch $ pfromData ctx.purpose
|
||||
plam $ \_redeemer ctx' -> unTermCont $ do
|
||||
PScriptContext ctx' <- tcmatch ctx'
|
||||
ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
|
||||
PTxInfo txInfo' <- tcmatch $ pfromData ctx.txInfo
|
||||
txInfo <- tcont $ pletFields @'["inputs", "mint"] txInfo'
|
||||
PMinting _ownSymbol <- tcmatch $ pfromData ctx.purpose
|
||||
|
||||
let inputs = txInfo.inputs
|
||||
mintedValue = pfromData txInfo.mint
|
||||
AssetClass (govCs, govTn) = proposal.governorSTAssetClass
|
||||
|
||||
PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose
|
||||
PMinting ownSymbol' <- tcmatch $ pfromData ctx.purpose
|
||||
let mintedProposalST =
|
||||
passetClassValueOf
|
||||
# mintedValue
|
||||
# (passetClass # (pfield @"_0" # ownSymbol') # pconstant "")
|
||||
|
||||
passert "Governance state-thread token must move" $
|
||||
tcassert "Governance state-thread token must move" $
|
||||
ptokenSpent
|
||||
# (passetClass # pconstant govCs # pconstant govTn)
|
||||
# inputs
|
||||
|
||||
passert "Minted exactly one proposal ST" $
|
||||
tcassert "Minted exactly one proposal ST" $
|
||||
mintedProposalST #== 1
|
||||
|
||||
popaque (pconstant ())
|
||||
pure $ popaque (pconstant ())
|
||||
|
||||
{- | The validator for Proposals.
|
||||
|
||||
|
|
@ -115,114 +116,113 @@ A list of all time-sensitive redeemers and their requirements:
|
|||
-}
|
||||
proposalValidator :: Proposal -> ClosedTerm PValidator
|
||||
proposalValidator proposal =
|
||||
plam $ \datum redeemer ctx' -> P.do
|
||||
PScriptContext ctx' <- pmatch ctx'
|
||||
ctx <- pletFields @'["txInfo", "purpose"] ctx'
|
||||
txInfo <- plet $ pfromData ctx.txInfo
|
||||
PTxInfo txInfo' <- pmatch txInfo
|
||||
txInfoF <- pletFields @'["inputs", "mint", "datums", "signatories"] txInfo'
|
||||
PSpending ((pfield @"_0" #) -> txOutRef) <- pmatch $ pfromData ctx.purpose
|
||||
plam $ \datum redeemer ctx' -> unTermCont $ do
|
||||
PScriptContext ctx' <- tcmatch ctx'
|
||||
ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
|
||||
txInfo <- tclet $ pfromData ctx.txInfo
|
||||
PTxInfo txInfo' <- tcmatch txInfo
|
||||
txInfoF <- tcont $ pletFields @'["inputs", "mint", "datums", "signatories"] txInfo'
|
||||
PSpending ((pfield @"_0" #) -> txOutRef) <- tcmatch $ pfromData ctx.purpose
|
||||
|
||||
PJust txOut <- pmatch $ findTxOutByTxOutRef # txOutRef # txInfoF.inputs
|
||||
txOutF <- pletFields @'["address", "value"] $ txOut
|
||||
PJust txOut <- tcmatch $ findTxOutByTxOutRef # txOutRef # txInfoF.inputs
|
||||
txOutF <- tcont $ pletFields @'["address", "value"] $ txOut
|
||||
|
||||
(pfromData -> proposalDatum, _) <-
|
||||
ptryFrom @(PAsData PProposalDatum) datum
|
||||
tctryFrom @(PAsData PProposalDatum) datum
|
||||
(pfromData -> proposalRedeemer, _) <-
|
||||
ptryFrom @(PAsData PProposalRedeemer) redeemer
|
||||
tctryFrom @(PAsData PProposalRedeemer) redeemer
|
||||
|
||||
proposalF <-
|
||||
pletFields
|
||||
@'[ "proposalId"
|
||||
, "effects"
|
||||
, "status"
|
||||
, "cosigners"
|
||||
, "thresholds"
|
||||
, "votes"
|
||||
]
|
||||
proposalDatum
|
||||
tcont $
|
||||
pletFields
|
||||
@'[ "proposalId"
|
||||
, "effects"
|
||||
, "status"
|
||||
, "cosigners"
|
||||
, "thresholds"
|
||||
, "votes"
|
||||
]
|
||||
proposalDatum
|
||||
|
||||
ownAddress <- plet $ txOutF.address
|
||||
ownAddress <- tclet $ txOutF.address
|
||||
|
||||
let stCurrencySymbol =
|
||||
pconstant $ getMintingPolicySymbol (proposalPolicy proposal)
|
||||
valueSpent <- plet $ pvalueSpent # txInfoF.inputs
|
||||
spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ valueSpent
|
||||
valueSpent <- tclet $ pvalueSpent # txInfoF.inputs
|
||||
spentST <- tclet $ psymbolValueOf # stCurrencySymbol #$ valueSpent
|
||||
let AssetClass (stakeSym, stakeTn) = proposal.stakeSTAssetClass
|
||||
stakeSTAssetClass <-
|
||||
plet $ passetClass # pconstant stakeSym # pconstant stakeTn
|
||||
tclet $ passetClass # pconstant stakeSym # pconstant stakeTn
|
||||
spentStakeST <-
|
||||
plet $ passetClassValueOf # valueSpent # stakeSTAssetClass
|
||||
tclet $ passetClassValueOf # valueSpent # stakeSTAssetClass
|
||||
|
||||
signedBy <- plet $ ptxSignedBy # txInfoF.signatories
|
||||
signedBy <- tclet $ ptxSignedBy # txInfoF.signatories
|
||||
|
||||
passert "ST at inputs must be 1" $
|
||||
spentST #== 1
|
||||
tcassert "ST at inputs must be 1" (spentST #== 1)
|
||||
|
||||
pmatch proposalRedeemer $ \case
|
||||
PVote _r -> P.do
|
||||
popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PCosign r -> P.do
|
||||
newSigs <- plet $ pfield @"newCosigners" # r
|
||||
pure $
|
||||
pmatch proposalRedeemer $ \case
|
||||
PVote _r -> popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PCosign r -> unTermCont $ do
|
||||
newSigs <- tclet $ pfield @"newCosigners" # r
|
||||
|
||||
passert "Cosigners are unique" $
|
||||
pisUniq # newSigs
|
||||
tcassert "Cosigners are unique" $
|
||||
pisUniq # newSigs
|
||||
|
||||
passert "Signed by all new cosigners" $
|
||||
pall # signedBy # newSigs
|
||||
tcassert "Signed by all new cosigners" $
|
||||
pall # signedBy # newSigs
|
||||
|
||||
passert "As many new cosigners as Stake datums" $
|
||||
spentStakeST #== plength # newSigs
|
||||
tcassert "As many new cosigners as Stake datums" $
|
||||
spentStakeST #== plength # newSigs
|
||||
|
||||
passert "All new cosigners are witnessed by their Stake datums" $
|
||||
pall
|
||||
# plam
|
||||
( \sig ->
|
||||
pmatch
|
||||
( findStakeOwnedBy # stakeSTAssetClass
|
||||
# pfromData sig
|
||||
# txInfoF.datums
|
||||
# txInfoF.inputs
|
||||
)
|
||||
$ \case
|
||||
PNothing -> pcon PFalse
|
||||
PJust _ -> pcon PTrue
|
||||
)
|
||||
# newSigs
|
||||
tcassert "All new cosigners are witnessed by their Stake datums" $
|
||||
pall
|
||||
# plam
|
||||
( \sig ->
|
||||
pmatch
|
||||
( findStakeOwnedBy # stakeSTAssetClass
|
||||
# pfromData sig
|
||||
# txInfoF.datums
|
||||
# txInfoF.inputs
|
||||
)
|
||||
$ \case
|
||||
PNothing -> pcon PFalse
|
||||
PJust _ -> pcon PTrue
|
||||
)
|
||||
# newSigs
|
||||
|
||||
passert "Signatures are correctly added to cosignature list" $
|
||||
anyOutput @PProposalDatum # ctx.txInfo
|
||||
#$ plam
|
||||
$ \newValue address newProposalDatum -> P.do
|
||||
let updatedSigs = pconcat # newSigs # proposalF.cosigners
|
||||
correctDatum =
|
||||
pdata newProposalDatum
|
||||
#== pdata
|
||||
( mkRecordConstr
|
||||
PProposalDatum
|
||||
( #proposalId .= proposalF.proposalId
|
||||
.& #effects .= proposalF.effects
|
||||
.& #status .= proposalF.status
|
||||
.& #cosigners .= pdata updatedSigs
|
||||
.& #thresholds .= proposalF.thresholds
|
||||
.& #votes .= proposalF.votes
|
||||
)
|
||||
)
|
||||
tcassert "Signatures are correctly added to cosignature list" $
|
||||
anyOutput @PProposalDatum # ctx.txInfo
|
||||
#$ plam
|
||||
$ \newValue address newProposalDatum ->
|
||||
let updatedSigs = pconcat # newSigs # proposalF.cosigners
|
||||
correctDatum =
|
||||
pdata newProposalDatum
|
||||
#== pdata
|
||||
( mkRecordConstr
|
||||
PProposalDatum
|
||||
( #proposalId .= proposalF.proposalId
|
||||
.& #effects .= proposalF.effects
|
||||
.& #status .= proposalF.status
|
||||
.& #cosigners .= pdata updatedSigs
|
||||
.& #thresholds .= proposalF.thresholds
|
||||
.& #votes .= proposalF.votes
|
||||
)
|
||||
)
|
||||
in foldr1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "Datum must be correct" correctDatum
|
||||
, ptraceIfFalse "Value should be correct" $
|
||||
pdata txOutF.value #== pdata newValue
|
||||
, ptraceIfFalse "Must be sent to Proposal's address" $
|
||||
ownAddress #== pdata address
|
||||
]
|
||||
|
||||
foldr1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "Datum must be correct" correctDatum
|
||||
, ptraceIfFalse "Value should be correct" $
|
||||
pdata txOutF.value #== pdata newValue
|
||||
, ptraceIfFalse "Must be sent to Proposal's address" $
|
||||
ownAddress #== pdata address
|
||||
]
|
||||
|
||||
popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PUnlock _r -> P.do
|
||||
popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PAdvanceProposal _r -> P.do
|
||||
popaque (pconstant ())
|
||||
pure $ popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PUnlock _r ->
|
||||
popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PAdvanceProposal _r ->
|
||||
popaque (pconstant ())
|
||||
|
|
|
|||
|
|
@ -28,6 +28,7 @@ module Agora.Proposal.Time (
|
|||
) where
|
||||
|
||||
import Agora.Record (mkRecordConstr, (.&), (.=))
|
||||
import Agora.Utils (tcmatch)
|
||||
import GHC.Generics qualified as GHC
|
||||
import Generics.SOP (Generic, I (I))
|
||||
import Plutarch.Api.V1 (
|
||||
|
|
@ -39,7 +40,6 @@ import Plutarch.Api.V1 (
|
|||
PUpperBound (PUpperBound),
|
||||
)
|
||||
import Plutarch.DataRepr (PDataFields, PIsDataReprInstances (..))
|
||||
import Plutarch.Monadic qualified as P
|
||||
import Plutarch.Numeric (AdditiveSemigroup ((+)))
|
||||
import Plutarch.Unsafe (punsafeCoerce)
|
||||
import Plutus.V1.Ledger.Time (POSIXTime)
|
||||
|
|
@ -159,28 +159,29 @@ instance AdditiveSemigroup (Term s PPOSIXTime) where
|
|||
-}
|
||||
currentProposalTime :: forall (s :: S). Term s (PPOSIXTimeRange :--> PProposalTime)
|
||||
currentProposalTime = phoistAcyclic $
|
||||
plam $ \iv -> P.do
|
||||
PInterval iv' <- pmatch iv
|
||||
ivf <- pletFields @'["from", "to"] iv'
|
||||
PLowerBound lb <- pmatch ivf.from
|
||||
PUpperBound ub <- pmatch ivf.to
|
||||
lbf <- pletFields @'["_0", "_1"] lb
|
||||
ubf <- pletFields @'["_0", "_1"] ub
|
||||
mkRecordConstr PProposalTime $
|
||||
#lowerBound
|
||||
.= pmatch
|
||||
lbf._0
|
||||
( \case
|
||||
PFinite ((pfield @"_0" #) -> d) -> d
|
||||
_ -> ptraceError "currentProposalTime: Can't get fully-bounded proposal time."
|
||||
)
|
||||
.& #upperBound
|
||||
.= pmatch
|
||||
ubf._0
|
||||
( \case
|
||||
PFinite ((pfield @"_0" #) -> d) -> d
|
||||
_ -> ptraceError "currentProposalTime: Can't get fully-bounded proposal time."
|
||||
)
|
||||
plam $ \iv -> unTermCont $ do
|
||||
PInterval iv' <- tcmatch iv
|
||||
ivf <- tcont $ pletFields @'["from", "to"] iv'
|
||||
PLowerBound lb <- tcmatch ivf.from
|
||||
PUpperBound ub <- tcmatch ivf.to
|
||||
lbf <- tcont $ pletFields @'["_0", "_1"] lb
|
||||
ubf <- tcont $ pletFields @'["_0", "_1"] ub
|
||||
pure $
|
||||
mkRecordConstr PProposalTime $
|
||||
#lowerBound
|
||||
.= pmatch
|
||||
lbf._0
|
||||
( \case
|
||||
PFinite ((pfield @"_0" #) -> d) -> d
|
||||
_ -> ptraceError "currentProposalTime: Can't get fully-bounded proposal time."
|
||||
)
|
||||
.& #upperBound
|
||||
.= pmatch
|
||||
ubf._0
|
||||
( \case
|
||||
PFinite ((pfield @"_0" #) -> d) -> d
|
||||
_ -> ptraceError "currentProposalTime: Can't get fully-bounded proposal time."
|
||||
)
|
||||
|
||||
-- | Check if 'PProposalTime' is within two 'PPOSIXTime'. Inclusive.
|
||||
proposalTimeWithin ::
|
||||
|
|
@ -192,14 +193,15 @@ proposalTimeWithin ::
|
|||
:--> PBool
|
||||
)
|
||||
proposalTimeWithin = phoistAcyclic $
|
||||
plam $ \l h proposalTime' -> P.do
|
||||
PProposalTime proposalTime <- pmatch proposalTime'
|
||||
ptf <- pletFields @'["lowerBound", "upperBound"] proposalTime
|
||||
foldr1
|
||||
(#&&)
|
||||
[ l #<= pfromData ptf.lowerBound
|
||||
, pfromData ptf.upperBound #<= h
|
||||
]
|
||||
plam $ \l h proposalTime' -> unTermCont $ do
|
||||
PProposalTime proposalTime <- tcmatch proposalTime'
|
||||
ptf <- tcont $ pletFields @'["lowerBound", "upperBound"] proposalTime
|
||||
pure $
|
||||
foldr1
|
||||
(#&&)
|
||||
[ l #<= pfromData ptf.lowerBound
|
||||
, pfromData ptf.upperBound #<= h
|
||||
]
|
||||
|
||||
-- | True if the 'PProposalTime' is in the draft period.
|
||||
isDraftPeriod ::
|
||||
|
|
|
|||
|
|
@ -53,7 +53,6 @@ import Plutarch.DataRepr (
|
|||
)
|
||||
import Plutarch.Internal (punsafeCoerce)
|
||||
import Plutarch.Lift (PConstantDecl, PUnsafeLiftDecl (..))
|
||||
import Plutarch.Monadic qualified as P
|
||||
import Plutus.V1.Ledger.Value (AssetClass)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
|
@ -63,6 +62,8 @@ import Agora.SafeMoney (GTTag)
|
|||
import Agora.Utils (
|
||||
pnotNull,
|
||||
ptryFindDatum,
|
||||
tclet,
|
||||
tcmatch,
|
||||
)
|
||||
import Control.Applicative (Const)
|
||||
import Plutarch.Api.V1.Extra (PAssetClass, passetClassValueOf)
|
||||
|
|
@ -274,20 +275,21 @@ findStakeOwnedBy = phoistAcyclic $
|
|||
plam $ \ac pk datums inputs ->
|
||||
pmatch (pfind # (isInputStakeOwnedBy # ac # pk # datums) # inputs) $ \case
|
||||
PNothing -> pcon PNothing
|
||||
PJust (pfromData -> v) -> P.do
|
||||
PJust (pfromData -> v) -> unTermCont $ do
|
||||
let txOut = pfield @"resolved" # pto v
|
||||
txOutF <- pletFields @'["datumHash"] $ txOut
|
||||
pmatch txOutF.datumHash $ \case
|
||||
PDNothing _ -> pcon PNothing
|
||||
PDJust ((pfield @"_0" #) -> dh) -> P.do
|
||||
ptryFindDatum @(PAsData PStakeDatum) # dh # datums
|
||||
txOutF <- tcont $ pletFields @'["datumHash"] $ txOut
|
||||
pure $
|
||||
pmatch txOutF.datumHash $ \case
|
||||
PDNothing _ -> pcon PNothing
|
||||
PDJust ((pfield @"_0" #) -> dh) ->
|
||||
ptryFindDatum @(PAsData PStakeDatum) # dh # datums
|
||||
|
||||
stakeDatumOwnedBy :: Term _ (PPubKeyHash :--> PStakeDatum :--> PBool)
|
||||
stakeDatumOwnedBy =
|
||||
phoistAcyclic $
|
||||
plam $ \pk stakeDatum -> P.do
|
||||
stakeDatumF <- pletFields @'["owner"] $ pto stakeDatum
|
||||
stakeDatumF.owner #== pdata pk
|
||||
plam $ \pk stakeDatum ->
|
||||
pletFields @'["owner"] (pto stakeDatum) $ \stakeDatumF ->
|
||||
stakeDatumF.owner #== pdata pk
|
||||
|
||||
-- Does the input have a `Stake` owned by a particular PK?
|
||||
isInputStakeOwnedBy ::
|
||||
|
|
@ -299,18 +301,19 @@ isInputStakeOwnedBy ::
|
|||
:--> PBool
|
||||
)
|
||||
isInputStakeOwnedBy =
|
||||
plam $ \ac ss datums txInInfo' -> P.do
|
||||
PTxInInfo ((pfield @"resolved" #) -> txOut) <- pmatch $ pfromData txInInfo'
|
||||
PTxOut txOut' <- pmatch txOut
|
||||
txOutF <- pletFields @'["value", "datumHash"] txOut'
|
||||
outStakeST <- plet $ passetClassValueOf # txOutF.value # ac
|
||||
pmatch txOutF.datumHash $ \case
|
||||
PDNothing _ -> pcon PFalse
|
||||
PDJust ((pfield @"_0" #) -> datumHash) ->
|
||||
pif
|
||||
(outStakeST #== 1)
|
||||
( pmatch (ptryFindDatum @(PAsData PStakeDatum) # datumHash # datums) $ \case
|
||||
PNothing -> pcon PFalse
|
||||
PJust v -> stakeDatumOwnedBy # ss # pfromData (punsafeCoerce v)
|
||||
)
|
||||
(pcon PFalse)
|
||||
plam $ \ac ss datums txInInfo' -> unTermCont $ do
|
||||
PTxInInfo ((pfield @"resolved" #) -> txOut) <- tcmatch $ pfromData txInInfo'
|
||||
PTxOut txOut' <- tcmatch txOut
|
||||
txOutF <- tcont $ pletFields @'["value", "datumHash"] txOut'
|
||||
outStakeST <- tclet $ passetClassValueOf # txOutF.value # ac
|
||||
pure $
|
||||
pmatch txOutF.datumHash $ \case
|
||||
PDNothing _ -> pcon PFalse
|
||||
PDJust ((pfield @"_0" #) -> datumHash) ->
|
||||
pif
|
||||
(outStakeST #== 1)
|
||||
( pmatch (ptryFindDatum @(PAsData PStakeDatum) # datumHash # datums) $ \case
|
||||
PNothing -> pcon PFalse
|
||||
PJust v -> stakeDatumOwnedBy # ss # pfromData (punsafeCoerce v)
|
||||
)
|
||||
(pcon PFalse)
|
||||
|
|
|
|||
|
|
@ -13,7 +13,6 @@ import Agora.Utils (
|
|||
anyInput,
|
||||
anyOutput,
|
||||
paddValue,
|
||||
passert,
|
||||
pfindTxInByTxOutRef,
|
||||
pgeqByClass,
|
||||
pgeqByClass',
|
||||
|
|
@ -24,6 +23,10 @@ import Agora.Utils (
|
|||
ptxSignedBy,
|
||||
pvalidatorHashToTokenName,
|
||||
pvalueSpent,
|
||||
tcassert,
|
||||
tclet,
|
||||
tcmatch,
|
||||
tctryFrom,
|
||||
)
|
||||
import Plutarch.Api.V1 (
|
||||
PCredential (PPubKeyCredential, PScriptCredential),
|
||||
|
|
@ -37,14 +40,12 @@ import Plutarch.Api.V1 (
|
|||
)
|
||||
import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
|
||||
import Plutarch.Internal (punsafeCoerce)
|
||||
import Plutarch.Monadic qualified as P
|
||||
import Plutarch.Numeric
|
||||
import Plutarch.SafeMoney (
|
||||
Tagged (..),
|
||||
pdiscreteValue',
|
||||
untag,
|
||||
)
|
||||
import Plutarch.TryFrom (ptryFrom)
|
||||
import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
|
||||
import Prelude hiding (Num (..))
|
||||
|
||||
|
|
@ -70,93 +71,92 @@ stakePolicy ::
|
|||
Tagged GTTag AssetClass ->
|
||||
ClosedTerm PMintingPolicy
|
||||
stakePolicy gtClassRef =
|
||||
plam $ \_redeemer ctx' -> P.do
|
||||
ctx <- pletFields @'["txInfo", "purpose"] ctx'
|
||||
txInfo <- plet $ ctx.txInfo
|
||||
plam $ \_redeemer ctx' -> unTermCont $ do
|
||||
ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
|
||||
txInfo <- tclet $ ctx.txInfo
|
||||
let _a :: Term _ PTxInfo
|
||||
_a = txInfo
|
||||
txInfoF <- pletFields @'["mint", "inputs", "outputs", "signatories"] txInfo
|
||||
txInfoF <- tcont $ pletFields @'["mint", "inputs", "outputs", "signatories"] txInfo
|
||||
|
||||
PMinting ownSymbol' <- pmatch $ pfromData ctx.purpose
|
||||
ownSymbol <- plet $ pfield @"_0" # ownSymbol'
|
||||
spentST <- plet $ psymbolValueOf # ownSymbol #$ pvalueSpent # txInfoF.inputs
|
||||
mintedST <- plet $ psymbolValueOf # ownSymbol # txInfoF.mint
|
||||
PMinting ownSymbol' <- tcmatch $ pfromData ctx.purpose
|
||||
ownSymbol <- tclet $ pfield @"_0" # ownSymbol'
|
||||
spentST <- tclet $ psymbolValueOf # ownSymbol #$ pvalueSpent # txInfoF.inputs
|
||||
mintedST <- tclet $ psymbolValueOf # ownSymbol # txInfoF.mint
|
||||
|
||||
let burning = P.do
|
||||
passert "ST at inputs must be 1" $
|
||||
let burning = unTermCont $ do
|
||||
tcassert "ST at inputs must be 1" $
|
||||
spentST #== 1
|
||||
|
||||
passert "ST burned" $
|
||||
tcassert "ST burned" $
|
||||
mintedST #== -1
|
||||
|
||||
passert "An unlocked input existed containing an ST" $
|
||||
tcassert "An unlocked input existed containing an ST" $
|
||||
anyInput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value _ stakeDatum' -> P.do
|
||||
$ \value _ stakeDatum' ->
|
||||
let hasST = psymbolValueOf # ownSymbol # value #== 1
|
||||
let unlocked = pnot # (stakeLocked # stakeDatum')
|
||||
hasST #&& unlocked
|
||||
unlocked = pnot # (stakeLocked # stakeDatum')
|
||||
in hasST #&& unlocked
|
||||
|
||||
popaque (pconstant ())
|
||||
pure $ popaque (pconstant ())
|
||||
|
||||
let minting = P.do
|
||||
passert "ST at inputs must be 0" $
|
||||
let minting = unTermCont $ do
|
||||
tcassert "ST at inputs must be 0" $
|
||||
spentST #== 0
|
||||
|
||||
passert "Minted ST must be exactly 1" $
|
||||
tcassert "Minted ST must be exactly 1" $
|
||||
mintedST #== 1
|
||||
|
||||
passert "A UTXO must exist with the correct output" $
|
||||
tcassert "A UTXO must exist with the correct output" $
|
||||
anyOutput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value address stakeDatum' -> P.do
|
||||
$ \value address stakeDatum' ->
|
||||
let cred = pfield @"credential" # address
|
||||
pmatch cred $ \case
|
||||
-- Should pay to a script address
|
||||
PPubKeyCredential _ -> pcon PFalse
|
||||
PScriptCredential validatorHash -> P.do
|
||||
stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
|
||||
in pmatch cred $ \case
|
||||
-- Should pay to a script address
|
||||
PPubKeyCredential _ -> pcon PFalse
|
||||
PScriptCredential validatorHash -> unTermCont $ do
|
||||
stakeDatum <- tcont $ pletFields @'["owner", "stakedAmount"] stakeDatum'
|
||||
|
||||
tn :: Term _ PTokenName <- plet (pvalidatorHashToTokenName $ pfromData $ pfield @"_0" # validatorHash)
|
||||
tn :: Term _ PTokenName <- tclet (pvalidatorHashToTokenName $ pfromData $ pfield @"_0" # validatorHash)
|
||||
|
||||
let stValue =
|
||||
psingletonValue
|
||||
# ownSymbol
|
||||
-- This coerce is safe because the structure
|
||||
-- of PValidatorHash is the same as PTokenName.
|
||||
# tn
|
||||
# 1
|
||||
let expectedValue =
|
||||
paddValue
|
||||
# (pdiscreteValue' gtClassRef # stakeDatum.stakedAmount)
|
||||
# stValue
|
||||
let ownerSignsTransaction =
|
||||
ptxSignedBy
|
||||
# txInfoF.signatories
|
||||
# stakeDatum.owner
|
||||
|
||||
-- TODO: This is quite inefficient now, as it does two lookups
|
||||
-- instead of a more efficient single pass,
|
||||
-- but it doesn't really matter for this. At least it's correct.
|
||||
let valueCorrect =
|
||||
foldr1
|
||||
(#&&)
|
||||
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
|
||||
, pgeqByClass' (untag gtClassRef)
|
||||
# value
|
||||
# expectedValue
|
||||
, pgeqByClass
|
||||
let stValue =
|
||||
psingletonValue
|
||||
# ownSymbol
|
||||
-- This coerce is safe because the structure
|
||||
-- of PValidatorHash is the same as PTokenName.
|
||||
# tn
|
||||
# value
|
||||
# expectedValue
|
||||
]
|
||||
# 1
|
||||
let expectedValue =
|
||||
paddValue
|
||||
# (pdiscreteValue' gtClassRef # stakeDatum.stakedAmount)
|
||||
# stValue
|
||||
let ownerSignsTransaction =
|
||||
ptxSignedBy
|
||||
# txInfoF.signatories
|
||||
# stakeDatum.owner
|
||||
|
||||
ownerSignsTransaction
|
||||
#&& valueCorrect
|
||||
popaque (pconstant ())
|
||||
-- TODO: This is quite inefficient now, as it does two lookups
|
||||
-- instead of a more efficient single pass,
|
||||
-- but it doesn't really matter for this. At least it's correct.
|
||||
let valueCorrect =
|
||||
foldr1
|
||||
(#&&)
|
||||
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
|
||||
, pgeqByClass' (untag gtClassRef)
|
||||
# value
|
||||
# expectedValue
|
||||
, pgeqByClass
|
||||
# ownSymbol
|
||||
# tn
|
||||
# value
|
||||
# expectedValue
|
||||
]
|
||||
|
||||
pif (0 #< mintedST) minting burning
|
||||
pure $ ownerSignsTransaction #&& valueCorrect
|
||||
pure $ popaque (pconstant ())
|
||||
|
||||
pure $ pif (0 #< mintedST) minting burning
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
|
|
@ -212,194 +212,196 @@ this could use [CIP-31](https://cips.cardano.org/cips/cip31/) instead.
|
|||
-}
|
||||
stakeValidator :: Stake -> ClosedTerm PValidator
|
||||
stakeValidator stake =
|
||||
plam $ \datum redeemer ctx' -> P.do
|
||||
ctx <- pletFields @'["txInfo", "purpose"] ctx'
|
||||
txInfo <- plet $ pfromData ctx.txInfo
|
||||
txInfoF <- pletFields @'["mint", "inputs", "outputs", "signatories"] txInfo
|
||||
plam $ \datum redeemer ctx' -> unTermCont $ do
|
||||
ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
|
||||
txInfo <- tclet $ pfromData ctx.txInfo
|
||||
txInfoF <- tcont $ pletFields @'["mint", "inputs", "outputs", "signatories"] txInfo
|
||||
|
||||
(pfromData -> stakeRedeemer, _) <- ptryFrom redeemer
|
||||
(pfromData -> stakeRedeemer, _) <- tctryFrom redeemer
|
||||
|
||||
-- TODO: Use PTryFrom
|
||||
let stakeDatum' :: Term _ PStakeDatum
|
||||
stakeDatum' = pfromData $ punsafeCoerce datum
|
||||
stakeDatum <- pletFields @'["owner", "stakedAmount"] stakeDatum'
|
||||
stakeDatum <- tcont $ pletFields @'["owner", "stakedAmount"] stakeDatum'
|
||||
|
||||
PSpending txOutRef <- pmatch $ pfromData ctx.purpose
|
||||
PSpending txOutRef <- tcmatch $ pfromData ctx.purpose
|
||||
|
||||
PJust txInInfo <- pmatch $ pfindTxInByTxOutRef # (pfield @"_0" # txOutRef) # txInfoF.inputs
|
||||
ownAddress <- plet $ pfield @"address" #$ pfield @"resolved" # txInInfo
|
||||
PJust txInInfo <- tcmatch $ pfindTxInByTxOutRef # (pfield @"_0" # txOutRef) # txInfoF.inputs
|
||||
ownAddress <- tclet $ pfield @"address" #$ pfield @"resolved" # txInInfo
|
||||
let continuingValue = pfield @"value" #$ pfield @"resolved" # txInInfo
|
||||
|
||||
-- Whether the owner signs this transaction or not.
|
||||
ownerSignsTransaction <- plet $ ptxSignedBy # txInfoF.signatories # stakeDatum.owner
|
||||
ownerSignsTransaction <- tclet $ ptxSignedBy # txInfoF.signatories # stakeDatum.owner
|
||||
|
||||
stCurrencySymbol <- plet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake.gtClassRef)
|
||||
mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfoF.mint
|
||||
valueSpent <- plet $ pvalueSpent # txInfoF.inputs
|
||||
spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ valueSpent
|
||||
stCurrencySymbol <- tclet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake.gtClassRef)
|
||||
mintedST <- tclet $ psymbolValueOf # stCurrencySymbol # txInfoF.mint
|
||||
valueSpent <- tclet $ pvalueSpent # txInfoF.inputs
|
||||
spentST <- tclet $ psymbolValueOf # stCurrencySymbol #$ valueSpent
|
||||
|
||||
let AssetClass (propCs, propTn) = stake.proposalSTClass
|
||||
proposalSTClass = passetClass # pconstant propCs # pconstant propTn
|
||||
spentProposalST <- plet $ passetClassValueOf # valueSpent # proposalSTClass
|
||||
spentProposalST <- tclet $ passetClassValueOf # valueSpent # proposalSTClass
|
||||
|
||||
-- Is the stake currently locked?
|
||||
stakeIsLocked <- plet $ stakeLocked # stakeDatum'
|
||||
stakeIsLocked <- tclet $ stakeLocked # stakeDatum'
|
||||
|
||||
pmatch stakeRedeemer $ \case
|
||||
PDestroy _ -> P.do
|
||||
passert "ST at inputs must be 1" $
|
||||
spentST #== 1
|
||||
pure $
|
||||
pmatch stakeRedeemer $ \case
|
||||
PDestroy _ -> unTermCont $ do
|
||||
tcassert "ST at inputs must be 1" $
|
||||
spentST #== 1
|
||||
|
||||
passert "Should burn ST" $
|
||||
mintedST #== -1
|
||||
tcassert "Should burn ST" $
|
||||
mintedST #== -1
|
||||
|
||||
passert "Stake unlocked" $ pnot # stakeIsLocked
|
||||
tcassert "Stake unlocked" $ pnot # stakeIsLocked
|
||||
|
||||
passert "Owner signs this transaction" ownerSignsTransaction
|
||||
tcassert "Owner signs this transaction" ownerSignsTransaction
|
||||
|
||||
popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PRetractVotes _ -> P.do
|
||||
passert
|
||||
"Owner signs this transaction"
|
||||
ownerSignsTransaction
|
||||
pure $ popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PRetractVotes _ -> unTermCont $ do
|
||||
tcassert
|
||||
"Owner signs this transaction"
|
||||
ownerSignsTransaction
|
||||
|
||||
passert "ST at inputs must be 1" $
|
||||
spentST #== 1
|
||||
tcassert "ST at inputs must be 1" $
|
||||
spentST #== 1
|
||||
|
||||
-- This puts trust into the Proposal. The Proposal must necessarily check
|
||||
-- that this is not abused.
|
||||
passert "Proposal ST spent" $
|
||||
spentProposalST #== 1
|
||||
-- This puts trust into the Proposal. The Proposal must necessarily check
|
||||
-- that this is not abused.
|
||||
tcassert "Proposal ST spent" $
|
||||
spentProposalST #== 1
|
||||
|
||||
passert "A UTXO must exist with the correct output" $
|
||||
anyOutput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value address newStakeDatum' -> P.do
|
||||
let isScriptAddress = pdata address #== ownAddress
|
||||
let _correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum'
|
||||
let valueCorrect = pdata continuingValue #== pdata value
|
||||
pif
|
||||
isScriptAddress
|
||||
( foldl1
|
||||
tcassert "A UTXO must exist with the correct output" $
|
||||
anyOutput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value address newStakeDatum' ->
|
||||
let isScriptAddress = pdata address #== ownAddress
|
||||
_correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum'
|
||||
valueCorrect = pdata continuingValue #== pdata value
|
||||
in pif
|
||||
isScriptAddress
|
||||
( foldl1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||
]
|
||||
)
|
||||
(pcon PFalse)
|
||||
|
||||
pure $ popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PPermitVote _ -> unTermCont $ do
|
||||
tcassert
|
||||
"Owner signs this transaction"
|
||||
ownerSignsTransaction
|
||||
|
||||
-- This puts trust into the Proposal. The Proposal must necessarily check
|
||||
-- that this is not abused.
|
||||
tcassert "Proposal ST spent" $
|
||||
spentProposalST #== 1
|
||||
|
||||
tcassert "A UTXO must exist with the correct output" $
|
||||
anyOutput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value address newStakeDatum' ->
|
||||
let isScriptAddress = pdata address #== ownAddress
|
||||
_correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum'
|
||||
valueCorrect = pdata continuingValue #== pdata value
|
||||
in pif
|
||||
isScriptAddress
|
||||
( foldl1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||
]
|
||||
)
|
||||
(pcon PFalse)
|
||||
|
||||
pure $ popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PWitnessStake _ -> unTermCont $ do
|
||||
tcassert "ST at inputs must be 1" $
|
||||
spentST #== 1
|
||||
|
||||
let AssetClass (propCs, propTn) = stake.proposalSTClass
|
||||
propAssetClass = passetClass # pconstant propCs # pconstant propTn
|
||||
proposalTokenMoved =
|
||||
ptokenSpent
|
||||
# propAssetClass
|
||||
# txInfoF.inputs
|
||||
|
||||
-- In order for cosignature to be witnessed, it must be possible for a
|
||||
-- proposal to allow this transaction to happen. This puts trust into the Proposal.
|
||||
-- The Proposal must necessarily check that this is not abused.
|
||||
tcassert
|
||||
"Owner signs this transaction OR proposal token is spent"
|
||||
(ownerSignsTransaction #|| proposalTokenMoved)
|
||||
|
||||
tcassert "A UTXO must exist with the correct output" $
|
||||
anyOutput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value address newStakeDatum' ->
|
||||
let isScriptAddress = pdata address #== ownAddress
|
||||
correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum'
|
||||
valueCorrect = pdata continuingValue #== pdata value
|
||||
in pif
|
||||
isScriptAddress
|
||||
( foldl1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||
, ptraceIfFalse "correctOutputDatum" correctOutputDatum
|
||||
]
|
||||
)
|
||||
(pcon PFalse)
|
||||
pure $ popaque (pconstant ())
|
||||
PDepositWithdraw r -> unTermCont $ do
|
||||
tcassert "ST at inputs must be 1" $
|
||||
spentST #== 1
|
||||
tcassert "Stake unlocked" $
|
||||
pnot #$ stakeIsLocked
|
||||
tcassert
|
||||
"Owner signs this transaction"
|
||||
ownerSignsTransaction
|
||||
tcassert "A UTXO must exist with the correct output" $
|
||||
anyOutput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value address newStakeDatum' -> unTermCont $ do
|
||||
newStakeDatum <- tcont $ pletFields @'["owner", "stakedAmount"] newStakeDatum'
|
||||
delta <- tclet $ pfield @"delta" # r
|
||||
let isScriptAddress = pdata address #== ownAddress
|
||||
let correctOutputDatum =
|
||||
foldr1
|
||||
(#&&)
|
||||
[ stakeDatum.owner #== newStakeDatum.owner
|
||||
, (stakeDatum.stakedAmount + delta) #== newStakeDatum.stakedAmount
|
||||
, -- We can't magically conjure GT anyway (no input to spend!)
|
||||
-- do we need to check this, really?
|
||||
zero #<= pfromData newStakeDatum.stakedAmount
|
||||
]
|
||||
let expectedValue = paddValue # continuingValue # (pdiscreteValue' stake.gtClassRef # delta)
|
||||
|
||||
-- TODO: Same as above. This is quite inefficient now, as it does two lookups
|
||||
-- instead of a more efficient single pass,
|
||||
-- but it doesn't really matter for this. At least it's correct.
|
||||
let valueCorrect =
|
||||
foldr1
|
||||
(#&&)
|
||||
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
|
||||
, pgeqByClass' (untag stake.gtClassRef)
|
||||
# value
|
||||
# expectedValue
|
||||
, pgeqBySymbol
|
||||
# stCurrencySymbol
|
||||
# value
|
||||
# expectedValue
|
||||
]
|
||||
|
||||
pure $
|
||||
foldr1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||
]
|
||||
)
|
||||
(pcon PFalse)
|
||||
|
||||
popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PPermitVote _ -> P.do
|
||||
passert
|
||||
"Owner signs this transaction"
|
||||
ownerSignsTransaction
|
||||
|
||||
-- This puts trust into the Proposal. The Proposal must necessarily check
|
||||
-- that this is not abused.
|
||||
passert "Proposal ST spent" $
|
||||
spentProposalST #== 1
|
||||
|
||||
passert "A UTXO must exist with the correct output" $
|
||||
anyOutput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value address newStakeDatum' -> P.do
|
||||
let isScriptAddress = pdata address #== ownAddress
|
||||
let _correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum'
|
||||
let valueCorrect = pdata continuingValue #== pdata value
|
||||
pif
|
||||
isScriptAddress
|
||||
( foldl1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||
]
|
||||
)
|
||||
(pcon PFalse)
|
||||
|
||||
popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
PWitnessStake _ -> P.do
|
||||
passert "ST at inputs must be 1" $
|
||||
spentST #== 1
|
||||
|
||||
let AssetClass (propCs, propTn) = stake.proposalSTClass
|
||||
propAssetClass = passetClass # pconstant propCs # pconstant propTn
|
||||
proposalTokenMoved =
|
||||
ptokenSpent
|
||||
# propAssetClass
|
||||
# txInfoF.inputs
|
||||
|
||||
-- In order for cosignature to be witnessed, it must be possible for a
|
||||
-- proposal to allow this transaction to happen. This puts trust into the Proposal.
|
||||
-- The Proposal must necessarily check that this is not abused.
|
||||
passert
|
||||
"Owner signs this transaction OR proposal token is spent"
|
||||
(ownerSignsTransaction #|| proposalTokenMoved)
|
||||
|
||||
passert "A UTXO must exist with the correct output" $
|
||||
anyOutput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value address newStakeDatum' -> P.do
|
||||
let isScriptAddress = pdata address #== ownAddress
|
||||
let correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum'
|
||||
let valueCorrect = pdata continuingValue #== pdata value
|
||||
pif
|
||||
isScriptAddress
|
||||
( foldl1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||
[ ptraceIfFalse "isScriptAddress" isScriptAddress
|
||||
, ptraceIfFalse "correctOutputDatum" correctOutputDatum
|
||||
, ptraceIfFalse "valueCorrect" valueCorrect
|
||||
]
|
||||
)
|
||||
(pcon PFalse)
|
||||
popaque (pconstant ())
|
||||
PDepositWithdraw r -> P.do
|
||||
passert "ST at inputs must be 1" $
|
||||
spentST #== 1
|
||||
passert "Stake unlocked" $
|
||||
pnot #$ stakeIsLocked
|
||||
passert
|
||||
"Owner signs this transaction"
|
||||
ownerSignsTransaction
|
||||
passert "A UTXO must exist with the correct output" $
|
||||
anyOutput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value address newStakeDatum' -> P.do
|
||||
newStakeDatum <- pletFields @'["owner", "stakedAmount"] newStakeDatum'
|
||||
delta <- plet $ pfield @"delta" # r
|
||||
let isScriptAddress = pdata address #== ownAddress
|
||||
let correctOutputDatum =
|
||||
foldr1
|
||||
(#&&)
|
||||
[ stakeDatum.owner #== newStakeDatum.owner
|
||||
, (stakeDatum.stakedAmount + delta) #== newStakeDatum.stakedAmount
|
||||
, -- We can't magically conjure GT anyway (no input to spend!)
|
||||
-- do we need to check this, really?
|
||||
zero #<= pfromData newStakeDatum.stakedAmount
|
||||
]
|
||||
let expectedValue = paddValue # continuingValue # (pdiscreteValue' stake.gtClassRef # delta)
|
||||
|
||||
-- TODO: Same as above. This is quite inefficient now, as it does two lookups
|
||||
-- instead of a more efficient single pass,
|
||||
-- but it doesn't really matter for this. At least it's correct.
|
||||
let valueCorrect =
|
||||
foldr1
|
||||
(#&&)
|
||||
[ pgeqByClass' (AssetClass ("", "")) # value # expectedValue
|
||||
, pgeqByClass' (untag stake.gtClassRef)
|
||||
# value
|
||||
# expectedValue
|
||||
, pgeqBySymbol
|
||||
# stCurrencySymbol
|
||||
# value
|
||||
# expectedValue
|
||||
]
|
||||
|
||||
foldr1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "isScriptAddress" isScriptAddress
|
||||
, ptraceIfFalse "correctOutputDatum" correctOutputDatum
|
||||
, ptraceIfFalse "valueCorrect" valueCorrect
|
||||
]
|
||||
|
||||
popaque (pconstant ())
|
||||
pure $ popaque (pconstant ())
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ treasury.
|
|||
module Agora.Treasury (module Agora.Treasury) where
|
||||
|
||||
import Agora.AuthorityToken (singleAuthorityTokenBurned)
|
||||
import Agora.Utils (passert)
|
||||
import Agora.Utils (tcassert, tclet, tcmatch, tctryFrom)
|
||||
import GHC.Generics qualified as GHC
|
||||
import Generics.SOP
|
||||
import Plutarch.Api.V1 (PValidator)
|
||||
|
|
@ -22,8 +22,7 @@ import Plutarch.DataRepr (
|
|||
PIsDataReprInstances (PIsDataReprInstances),
|
||||
)
|
||||
import Plutarch.Lift (PConstantDecl (..), PLifted (..), PUnsafeLiftDecl)
|
||||
import Plutarch.Monadic qualified as P
|
||||
import Plutarch.TryFrom (PTryFrom, ptryFrom)
|
||||
import Plutarch.TryFrom (PTryFrom)
|
||||
import Plutus.V1.Ledger.Value (CurrencySymbol)
|
||||
import PlutusTx qualified
|
||||
|
||||
|
|
@ -75,27 +74,27 @@ deriving via
|
|||
treasuryValidator ::
|
||||
CurrencySymbol ->
|
||||
ClosedTerm PValidator
|
||||
treasuryValidator gatCs' = plam $ \_datum redeemer ctx' -> P.do
|
||||
(treasuryRedeemer, _) <- ptryFrom redeemer
|
||||
treasuryValidator gatCs' = plam $ \_datum redeemer ctx' -> unTermCont $ do
|
||||
(treasuryRedeemer, _) <- tctryFrom redeemer
|
||||
|
||||
-- plet required fields from script context.
|
||||
ctx <- pletFields @["txInfo", "purpose"] ctx'
|
||||
ctx <- tcont $ pletFields @["txInfo", "purpose"] ctx'
|
||||
|
||||
-- Ensure that script is for burning i.e. minting a negative amount.
|
||||
PMinting _ <- pmatch ctx.purpose
|
||||
PMinting _ <- tcmatch ctx.purpose
|
||||
|
||||
-- Ensure redeemer type is valid.
|
||||
PSpendTreasuryGAT _ <- pmatch $ pfromData treasuryRedeemer
|
||||
PSpendTreasuryGAT _ <- tcmatch $ pfromData treasuryRedeemer
|
||||
|
||||
-- Get the minted value from txInfo.
|
||||
txInfo' <- plet ctx.txInfo
|
||||
txInfo <- pletFields @'["mint"] txInfo'
|
||||
txInfo' <- tclet ctx.txInfo
|
||||
txInfo <- tcont $ pletFields @'["mint"] txInfo'
|
||||
let mint :: Term _ PValue
|
||||
mint = txInfo.mint
|
||||
|
||||
gatCs <- plet $ pconstant gatCs'
|
||||
gatCs <- tclet $ pconstant gatCs'
|
||||
|
||||
passert "A single authority token has been burned" $
|
||||
tcassert "A single authority token has been burned" $
|
||||
singleAuthorityTokenBurned gatCs txInfo' mint
|
||||
|
||||
popaque $ pconstant ()
|
||||
pure . popaque $ pconstant ()
|
||||
|
|
|
|||
|
|
@ -6,8 +6,13 @@ Description: Plutarch utility functions that should be upstreamed or don't belon
|
|||
Plutarch utility functions that should be upstreamed or don't belong anywhere else.
|
||||
-}
|
||||
module Agora.Utils (
|
||||
-- * TermCont-based combinators. Some of these will live in plutarch eventually.
|
||||
tcassert,
|
||||
tclet,
|
||||
tcmatch,
|
||||
tctryFrom,
|
||||
|
||||
-- * Validator-level utility functions
|
||||
passert,
|
||||
pfind',
|
||||
pfindDatum,
|
||||
ptryFindDatum,
|
||||
|
|
@ -80,16 +85,42 @@ import Plutarch.Api.V1.Extra (PAssetClass, passetClassValueOf, pvalueOf)
|
|||
import Plutarch.Api.V1.Value (PValue (PValue))
|
||||
import Plutarch.Builtin (ppairDataBuiltin)
|
||||
import Plutarch.Map.Extra (pkeys)
|
||||
import Plutarch.Monadic qualified as P
|
||||
import Plutarch.TryFrom (PTryFrom, ptryFrom)
|
||||
import Plutarch.Reducible (Reducible (Reduce))
|
||||
import Plutarch.TryFrom (PTryFrom (PTryFromExcess), ptryFrom)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- TermCont-based combinators. Some of these will live in plutarch eventually.
|
||||
|
||||
-- | Assert a particular 'PBool', trace if false.
|
||||
tcassert :: forall r (s :: S). Term s PString -> Term s PBool -> TermCont @r s ()
|
||||
tcassert errorMessage check = tcont $ \k -> pif check (k ()) (ptraceError errorMessage)
|
||||
|
||||
-- | 'plet' but for use in 'TermCont'.
|
||||
tclet :: forall r (s :: S) (a :: PType). Term s a -> TermCont @r s (Term s a)
|
||||
tclet = tcont . plet
|
||||
|
||||
-- | 'pmatch' but for use in 'TermCont'.
|
||||
tcmatch :: forall (a :: PType) (s :: S). PlutusType a => Term s a -> TermCont s (a s)
|
||||
tcmatch = tcont . pmatch
|
||||
|
||||
-- | 'ptryFrom' but for use in 'TermCont'.
|
||||
tctryFrom :: forall b a s r. PTryFrom a b => Term s a -> TermCont @r s (Term s b, Reduce (PTryFromExcess a b s))
|
||||
tctryFrom = tcont . ptryFrom
|
||||
|
||||
-- | Escape with a particular value on expecting 'Just'. For use in monadic context.
|
||||
tcexpectJust ::
|
||||
forall r (a :: PType) (s :: S).
|
||||
Term s r ->
|
||||
Term s (PMaybe a) ->
|
||||
TermCont @r s (Term s a)
|
||||
tcexpectJust escape ma = tcont $ \f ->
|
||||
pmatch ma $ \case
|
||||
PJust v -> f v
|
||||
PNothing -> escape
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Validator-level utility functions
|
||||
|
||||
-- | Assert a particular 'PBool', trace if false. Use in monadic context.
|
||||
passert :: Term s PString -> Term s PBool -> Term s k -> Term s k
|
||||
passert errorMessage check k = pif check k (ptraceError errorMessage)
|
||||
|
||||
-- | Find a datum with the given hash.
|
||||
pfindDatum :: Term s (PDatumHash :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PMaybe PDatum)
|
||||
pfindDatum = phoistAcyclic $
|
||||
|
|
@ -101,9 +132,9 @@ ptryFindDatum = phoistAcyclic $
|
|||
plam $ \datumHash inputs ->
|
||||
pmatch (pfindDatum # datumHash # inputs) $ \case
|
||||
PNothing -> pcon PNothing
|
||||
PJust datum -> P.do
|
||||
(datum', _) <- ptryFrom (pto datum)
|
||||
pcon (PJust datum')
|
||||
PJust datum -> unTermCont $ do
|
||||
(datum', _) <- tctryFrom (pto datum)
|
||||
pure $ pcon (PJust datum')
|
||||
|
||||
-- | Check if a PubKeyHash signs this transaction.
|
||||
ptxSignedBy :: Term s (PBuiltinList (PAsData PPubKeyHash) :--> PAsData PPubKeyHash :--> PBool)
|
||||
|
|
@ -169,34 +200,21 @@ pfromMaybe = phoistAcyclic $
|
|||
-- | Yield True if a given PMaybe is of form PJust _.
|
||||
pisJust :: forall a s. Term s (PMaybe a :--> PBool)
|
||||
pisJust = phoistAcyclic $
|
||||
plam $ \v' -> P.do
|
||||
v <- pmatch v'
|
||||
case v of
|
||||
plam $ \v' ->
|
||||
pmatch v' $ \case
|
||||
PJust _ -> pconstant True
|
||||
PNothing -> pconstant False
|
||||
|
||||
-- | Escape with a particular value on expecting 'Just'. For use in monadic context.
|
||||
pexpectJust ::
|
||||
forall r a s.
|
||||
Term s r ->
|
||||
Term s (PMaybe a) ->
|
||||
(Term s a -> Term s r) ->
|
||||
Term s r
|
||||
pexpectJust escape ma f =
|
||||
pmatch ma $ \case
|
||||
PJust v -> f v
|
||||
PNothing -> escape
|
||||
|
||||
-- | Get the sum of all values belonging to a particular CurrencySymbol.
|
||||
psymbolValueOf :: Term s (PCurrencySymbol :--> PValue :--> PInteger)
|
||||
psymbolValueOf =
|
||||
phoistAcyclic $
|
||||
plam $ \sym value'' -> P.do
|
||||
PValue value' <- pmatch value''
|
||||
PMap value <- pmatch value'
|
||||
m' <- pexpectJust 0 (plookup # pdata sym # value)
|
||||
PMap m <- pmatch (pfromData m')
|
||||
pfoldr # plam (\x v -> pfromData (psndBuiltin # x) + v) # 0 # m
|
||||
plam $ \sym value'' -> unTermCont $ do
|
||||
PValue value' <- tcmatch value''
|
||||
PMap value <- tcmatch value'
|
||||
m' <- tcexpectJust 0 (plookup # pdata sym # value)
|
||||
PMap m <- tcmatch (pfromData m')
|
||||
pure $ pfoldr # plam (\x v -> pfromData (psndBuiltin # x) + v) # 0 # m
|
||||
|
||||
-- | Extract amount from PValue belonging to a Haskell-level AssetClass.
|
||||
passetClassValueOf' :: AssetClass -> Term s (PValue :--> PInteger)
|
||||
|
|
@ -228,19 +246,20 @@ pgeqByClass' ac =
|
|||
pmapUnionWith :: forall k v s. PIsData v => Term s ((v :--> v :--> v) :--> PMap k v :--> PMap k v :--> PMap k v)
|
||||
pmapUnionWith = phoistAcyclic $
|
||||
-- TODO: this function is kinda suspect. I feel like a lot of optimizations could be done here
|
||||
plam $ \f xs' ys' -> P.do
|
||||
PMap xs <- pmatch xs'
|
||||
PMap ys <- pmatch ys'
|
||||
plam $ \f xs' ys' -> unTermCont $ do
|
||||
PMap xs <- tcmatch xs'
|
||||
PMap ys <- tcmatch ys'
|
||||
let ls =
|
||||
pmap
|
||||
# plam
|
||||
( \p -> P.do
|
||||
pf <- plet $ pfstBuiltin # p
|
||||
pmatch (plookup # pf # ys) $ \case
|
||||
PJust v ->
|
||||
-- Data conversions here are silly, aren't they?
|
||||
ppairDataBuiltin # pf # pdata (f # pfromData (psndBuiltin # p) # pfromData v)
|
||||
PNothing -> p
|
||||
( \p -> unTermCont $ do
|
||||
pf <- tclet $ pfstBuiltin # p
|
||||
pure $
|
||||
pmatch (plookup # pf # ys) $ \case
|
||||
PJust v ->
|
||||
-- Data conversions here are silly, aren't they?
|
||||
ppairDataBuiltin # pf # pdata (f # pfromData (psndBuiltin # p) # pfromData v)
|
||||
PNothing -> p
|
||||
)
|
||||
# xs
|
||||
rs =
|
||||
|
|
@ -250,18 +269,19 @@ pmapUnionWith = phoistAcyclic $
|
|||
pnot #$ pany # plam (\p' -> pfstBuiltin # p' #== pfstBuiltin # p) # xs
|
||||
)
|
||||
# ys
|
||||
pcon (PMap $ pconcat # ls # rs)
|
||||
pure $ pcon (PMap $ pconcat # ls # rs)
|
||||
|
||||
-- | Add two 'PValue's together.
|
||||
paddValue :: forall s. Term s (PValue :--> PValue :--> PValue)
|
||||
paddValue = phoistAcyclic $
|
||||
plam $ \a' b' -> P.do
|
||||
PValue a <- pmatch a'
|
||||
PValue b <- pmatch b'
|
||||
pcon
|
||||
( PValue $
|
||||
pmapUnionWith # plam (\a' b' -> pmapUnionWith # plam (+) # a' # b') # a # b
|
||||
)
|
||||
plam $ \a' b' -> unTermCont $ do
|
||||
PValue a <- tcmatch a'
|
||||
PValue b <- tcmatch b'
|
||||
pure $
|
||||
pcon
|
||||
( PValue $
|
||||
pmapUnionWith # plam (\a' b' -> pmapUnionWith # plam (+) # a' # b') # a # b
|
||||
)
|
||||
|
||||
-- | Sum of all value at input.
|
||||
pvalueSpent :: Term s (PBuiltinList (PAsData PTxInInfo) :--> PValue)
|
||||
|
|
@ -313,12 +333,12 @@ ptokenSpent =
|
|||
0
|
||||
#< pfoldr @PBuiltinList
|
||||
# plam
|
||||
( \txInInfo' acc -> P.do
|
||||
PTxInInfo txInInfo <- pmatch (pfromData txInInfo')
|
||||
PTxOut txOut' <- pmatch $ pfromData $ pfield @"resolved" # txInInfo
|
||||
txOut <- pletFields @'["value"] txOut'
|
||||
( \txInInfo' acc -> unTermCont $ do
|
||||
PTxInInfo txInInfo <- tcmatch (pfromData txInInfo')
|
||||
PTxOut txOut' <- tcmatch $ pfromData $ pfield @"resolved" # txInInfo
|
||||
txOut <- tcont $ pletFields @'["value"] txOut'
|
||||
let txOutValue = pfromData txOut.value
|
||||
acc + passetClassValueOf # txOutValue # tokenClass
|
||||
pure $ acc + passetClassValueOf # txOutValue # tokenClass
|
||||
)
|
||||
# 0
|
||||
# inputs
|
||||
|
|
@ -328,11 +348,12 @@ ptokenSpent =
|
|||
-}
|
||||
pkeysEqual :: forall (s :: S) k a b. Term s (PMap k a :--> PMap k b :--> PBool)
|
||||
pkeysEqual = phoistAcyclic $
|
||||
plam $ \p q -> P.do
|
||||
pks <- plet $ pkeys # p
|
||||
qks <- plet $ pkeys # q
|
||||
pall # plam (\pk -> pelem # pk # qks) # pks
|
||||
#&& pall # plam (\qk -> pelem # qk # pks) # qks
|
||||
plam $ \p q -> unTermCont $ do
|
||||
pks <- tclet $ pkeys # p
|
||||
qks <- tclet $ pkeys # q
|
||||
pure $
|
||||
pall # plam (\pk -> pelem # pk # qks) # pks
|
||||
#&& pall # plam (\qk -> pelem # qk # pks) # qks
|
||||
|
||||
-- | / O(n^2) /. Clear out duplicates in a list. The order is not preserved.
|
||||
pnub :: forall list a (s :: S). (PEq a, PIsListLike list a) => Term s (list a :--> list a)
|
||||
|
|
@ -371,20 +392,21 @@ anyOutput ::
|
|||
) =>
|
||||
Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
|
||||
anyOutput = phoistAcyclic $
|
||||
plam $ \txInfo' predicate -> P.do
|
||||
txInfo <- pletFields @'["outputs", "datums"] txInfo'
|
||||
pany
|
||||
# plam
|
||||
( \txOut'' -> P.do
|
||||
PTxOut txOut' <- pmatch (pfromData txOut'')
|
||||
txOut <- pletFields @'["value", "datumHash", "address"] txOut'
|
||||
PDJust dh <- pmatch txOut.datumHash
|
||||
pmatch (ptryFindDatum @(PAsData datum) # (pfield @"_0" # dh) # txInfo.datums) $ \case
|
||||
PJust datum -> P.do
|
||||
predicate # txOut.value # txOut.address # pfromData datum
|
||||
PNothing -> pcon PFalse
|
||||
)
|
||||
# pfromData txInfo.outputs
|
||||
plam $ \txInfo' predicate -> unTermCont $ do
|
||||
txInfo <- tcont $ pletFields @'["outputs", "datums"] txInfo'
|
||||
pure $
|
||||
pany
|
||||
# plam
|
||||
( \txOut'' -> unTermCont $ do
|
||||
PTxOut txOut' <- tcmatch (pfromData txOut'')
|
||||
txOut <- tcont $ pletFields @'["value", "datumHash", "address"] txOut'
|
||||
PDJust dh <- tcmatch txOut.datumHash
|
||||
pure $
|
||||
pmatch (ptryFindDatum @(PAsData datum) # (pfield @"_0" # dh) # txInfo.datums) $ \case
|
||||
PJust datum -> predicate # txOut.value # txOut.address # pfromData datum
|
||||
PNothing -> pcon PFalse
|
||||
)
|
||||
# pfromData txInfo.outputs
|
||||
|
||||
-- | Check if all outputs match the predicate.
|
||||
allOutputs ::
|
||||
|
|
@ -394,20 +416,21 @@ allOutputs ::
|
|||
) =>
|
||||
Term s (PTxInfo :--> (PTxOut :--> PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
|
||||
allOutputs = phoistAcyclic $
|
||||
plam $ \txInfo' predicate -> P.do
|
||||
txInfo <- pletFields @'["outputs", "datums"] txInfo'
|
||||
pall
|
||||
# plam
|
||||
( \txOut'' -> P.do
|
||||
PTxOut txOut' <- pmatch (pfromData txOut'')
|
||||
txOut <- pletFields @'["value", "datumHash", "address"] txOut'
|
||||
PDJust dh <- pmatch txOut.datumHash
|
||||
pmatch (ptryFindDatum @(PAsData datum) # (pfield @"_0" # dh) # txInfo.datums) $ \case
|
||||
PJust datum -> P.do
|
||||
predicate # pfromData txOut'' # txOut.value # txOut.address # pfromData datum
|
||||
PNothing -> pcon PFalse
|
||||
)
|
||||
# pfromData txInfo.outputs
|
||||
plam $ \txInfo' predicate -> unTermCont $ do
|
||||
txInfo <- tcont $ pletFields @'["outputs", "datums"] txInfo'
|
||||
pure $
|
||||
pall
|
||||
# plam
|
||||
( \txOut'' -> unTermCont $ do
|
||||
PTxOut txOut' <- tcmatch (pfromData txOut'')
|
||||
txOut <- tcont $ pletFields @'["value", "datumHash", "address"] txOut'
|
||||
PDJust dh <- tcmatch txOut.datumHash
|
||||
pure $
|
||||
pmatch (ptryFindDatum @(PAsData datum) # (pfield @"_0" # dh) # txInfo.datums) $ \case
|
||||
PJust datum -> predicate # pfromData txOut'' # txOut.value # txOut.address # pfromData datum
|
||||
PNothing -> pcon PFalse
|
||||
)
|
||||
# pfromData txInfo.outputs
|
||||
|
||||
-- | Check if any (resolved) input matches the predicate.
|
||||
anyInput ::
|
||||
|
|
@ -417,22 +440,23 @@ anyInput ::
|
|||
) =>
|
||||
Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
|
||||
anyInput = phoistAcyclic $
|
||||
plam $ \txInfo' predicate -> P.do
|
||||
txInfo <- pletFields @'["inputs", "datums"] 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 (ptryFindDatum @(PAsData datum) # (pfield @"_0" # dh) # txInfo.datums) $ \case
|
||||
PJust datum -> P.do
|
||||
predicate # txOut.value # txOut.address # pfromData datum
|
||||
PNothing -> pcon PFalse
|
||||
)
|
||||
# pfromData txInfo.inputs
|
||||
plam $ \txInfo' predicate -> unTermCont $ do
|
||||
txInfo <- tcont $ pletFields @'["inputs", "datums"] txInfo'
|
||||
pure $
|
||||
pany
|
||||
# plam
|
||||
( \txInInfo'' -> unTermCont $ do
|
||||
PTxInInfo txInInfo' <- tcmatch (pfromData txInInfo'')
|
||||
let txOut'' = pfield @"resolved" # txInInfo'
|
||||
PTxOut txOut' <- tcmatch (pfromData txOut'')
|
||||
txOut <- tcont $ pletFields @'["value", "datumHash", "address"] txOut'
|
||||
PDJust dh <- tcmatch txOut.datumHash
|
||||
pure $
|
||||
pmatch (ptryFindDatum @(PAsData datum) # (pfield @"_0" # dh) # txInfo.datums) $ \case
|
||||
PJust datum -> predicate # txOut.value # txOut.address # pfromData datum
|
||||
PNothing -> pcon PFalse
|
||||
)
|
||||
# pfromData txInfo.inputs
|
||||
|
||||
-- | Create a value with a single asset class.
|
||||
psingletonValue :: forall s. Term s (PCurrencySymbol :--> PTokenName :--> PInteger :--> PValue)
|
||||
|
|
@ -462,17 +486,18 @@ scriptHashFromAddress = phoistAcyclic $
|
|||
-- | Find all TxOuts sent to an Address
|
||||
findOutputsToAddress :: Term s (PBuiltinList (PAsData PTxOut) :--> PAddress :--> PBuiltinList (PAsData PTxOut))
|
||||
findOutputsToAddress = phoistAcyclic $
|
||||
plam $ \outputs address' -> P.do
|
||||
address <- plet $ pdata address'
|
||||
pfilter # plam (\(pfromData -> txOut) -> pfield @"address" # txOut #== address)
|
||||
# outputs
|
||||
plam $ \outputs address' -> unTermCont $ do
|
||||
address <- tclet $ pdata address'
|
||||
pure $
|
||||
pfilter # plam (\(pfromData -> txOut) -> pfield @"address" # txOut #== address)
|
||||
# outputs
|
||||
|
||||
-- | Find the data corresponding to a TxOut, if there is one
|
||||
findTxOutDatum :: Term s (PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PTxOut :--> PMaybe PDatum)
|
||||
findTxOutDatum = phoistAcyclic $
|
||||
plam $ \datums out -> P.do
|
||||
datumHash' <- pmatch $ pfromData $ pfield @"datumHash" # out
|
||||
case datumHash' of
|
||||
plam $ \datums out -> unTermCont $ do
|
||||
datumHash' <- tcmatch $ pfromData $ pfield @"datumHash" # out
|
||||
pure $ case datumHash' of
|
||||
PDJust ((pfield @"_0" #) -> datumHash) -> pfindDatum # datumHash # datums
|
||||
_ -> pcon PNothing
|
||||
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@
|
|||
|
||||
module Agora.Utils.Value (pgeq, pleq, pgt, plt) where
|
||||
|
||||
import Agora.Utils (tcmatch)
|
||||
import Plutarch.Api.V1.AssocMap (PMap (PMap))
|
||||
import Plutarch.Api.V1.These (PTheseData (..))
|
||||
import Plutarch.Api.V1.Tuple (ptupleFromBuiltin)
|
||||
|
|
@ -26,15 +27,15 @@ punionVal = undefined
|
|||
pmapAll ::
|
||||
(PUnsafeLiftDecl v, PIsData v) =>
|
||||
Term s ((v :--> PBool) :--> PMap k v :--> PBool)
|
||||
pmapAll = plam $ \f m -> P.do
|
||||
PMap builtinMap <- pmatch m
|
||||
pmapAll = plam $ \f m -> unTermCont $ do
|
||||
PMap builtinMap <- tcmatch m
|
||||
|
||||
let getV = plam $ \bip -> P.do
|
||||
let getV = plam $ \bip ->
|
||||
let tuple = pfromData $ ptupleFromBuiltin (pdata bip)
|
||||
pfromData $ pfield @"_1" # tuple
|
||||
in pfromData $ pfield @"_1" # tuple
|
||||
|
||||
let vs = pmap # getV # builtinMap
|
||||
pall # f # vs
|
||||
pure $ pall # f # vs
|
||||
|
||||
pcheckPred ::
|
||||
forall {s :: S}.
|
||||
|
|
@ -45,8 +46,7 @@ pcheckPred ::
|
|||
:--> PValue
|
||||
:--> PBool
|
||||
)
|
||||
pcheckPred = plam $ \_f _l _r -> P.do
|
||||
undefined
|
||||
pcheckPred = plam $ \_f _l _r -> undefined
|
||||
|
||||
-- let inner :: Term s (PMap PTokenName (PTheseData PInteger PInteger) :--> PBool)
|
||||
-- inner = pmapAll # f
|
||||
|
|
@ -61,14 +61,14 @@ pcheckBinRel ::
|
|||
:--> PValue
|
||||
:--> PBool
|
||||
)
|
||||
pcheckBinRel = plam $ \f l r -> P.do
|
||||
pcheckBinRel = plam $ \f l r ->
|
||||
let unThese :: Term s (PTheseData PInteger PInteger :--> PBool)
|
||||
unThese = plam $ \k' ->
|
||||
pmatch k' $ \case
|
||||
PDThis r -> f # (pfield @"_0" # r) # 0
|
||||
PDThat r -> f # 0 # (pfield @"_0" # r)
|
||||
PDThese r -> f # (pfield @"_0" # r) # (pfield @"_1" # r)
|
||||
pcheckPred # unThese # l # r
|
||||
in pcheckPred # unThese # l # r
|
||||
|
||||
-- | Establishes if a value is less than or equal to another.
|
||||
pleq :: Term s (PValue :--> PValue :--> PBool)
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue