reduce use of unjustified punsafeCoerce

This commit is contained in:
Emily Martins 2022-04-27 12:42:19 +02:00
parent 34827aeca6
commit 9dd5bed05e
7 changed files with 143 additions and 56 deletions

View file

@ -145,7 +145,7 @@ authorityTokenPolicy params =
( P.do
passert "Parent token did not move in minting GATs" govTokenSpent
passert "All outputs only emit valid GATs" $
allOutputs @PUnit # pfromData ctx.txInfo #$ plam $ \txOut _value _address _datum ->
allOutputs @PData # pfromData ctx.txInfo #$ plam $ \txOut _value _address _datum ->
authorityTokensValidIn
# ownSymbol
# txOut

View file

@ -26,6 +26,9 @@ module Agora.Proposal (
PProposalVotes (..),
PProposalId (..),
PResultTag (..),
-- * Plutarch helpers
proposalDatumValid,
) where
import GHC.Generics qualified as GHC
@ -41,13 +44,17 @@ import PlutusTx.AssocMap qualified as AssocMap
--------------------------------------------------------------------------------
import Agora.SafeMoney (GTTag)
import Agora.Utils (pnotNull)
import Control.Applicative (Const)
import Control.Arrow (first)
import Plutarch.Builtin (PBuiltinMap)
import Plutarch.DataRepr (DerivePConstantViaData (..), PDataFields, PIsDataReprInstances (..))
import Plutarch.Lift (
DerivePConstantViaNewtype (..),
PConstantDecl,
PUnsafeLiftDecl (..),
)
import Plutarch.Monadic qualified as P
import Plutarch.SafeMoney (PDiscrete, Tagged)
import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
import Plutarch.Unsafe (punsafeCoerce)
@ -348,6 +355,12 @@ newtype PProposalDatum (s :: S) = PProposalDatum
(PlutusType, PIsData, PDataFields)
via (PIsDataReprInstances PProposalDatum)
-- TODO: Derive this.
instance PTryFrom PData (PAsData PProposalDatum) where
type PTryFromExcess PData (PAsData PProposalDatum) = Const ()
ptryFrom' d k =
k (punsafeCoerce d, ())
instance PUnsafeLiftDecl PProposalDatum where type PLifted PProposalDatum = ProposalDatum
deriving via (DerivePConstantViaData ProposalDatum PProposalDatum) instance (PConstantDecl ProposalDatum)
@ -364,6 +377,12 @@ data PProposalRedeemer (s :: S)
(PlutusType, PIsData)
via PIsDataReprInstances PProposalRedeemer
-- See below.
instance PTryFrom PData (PAsData PProposalRedeemer) where
type PTryFromExcess PData (PAsData PProposalRedeemer) = Const ()
ptryFrom' d k =
k (punsafeCoerce d, ())
-- TODO: Waiting on PTryFrom for 'PPubKeyHash'
-- deriving via
-- PAsData (PIsDataReprInstances PProposalRedeemer)
@ -372,3 +391,34 @@ data PProposalRedeemer (s :: S)
instance PUnsafeLiftDecl PProposalRedeemer where type PLifted PProposalRedeemer = ProposalRedeemer
deriving via (DerivePConstantViaData ProposalRedeemer PProposalRedeemer) instance (PConstantDecl ProposalRedeemer)
--------------------------------------------------------------------------------
{- | Check for various invariants a proposal must uphold.
This can be used to check both upopn creation and
upon any following state transitions in the proposal.
-}
proposalDatumValid :: Term s (Agora.Proposal.PProposalDatum :--> PBool)
proposalDatumValid =
phoistAcyclic $
plam $ \datum' -> P.do
datum <- pletFields @'["effects", "cosigners"] $ datum'
let effects :: Term _ (PBuiltinMap Agora.Proposal.PResultTag (PBuiltinMap Plutarch.Api.V1.PValidatorHash Plutarch.Api.V1.PDatumHash))
effects =
-- JUSTIFICATION:
-- @datum.effects : PMap PResultTag (PMap PValidatorHash PDatumHash)@
-- @PMap PResultTag (PMap PValidatorHash PDatumHash)@ is equivalent to
-- @PBuiltinMap PResultTag (PBuiltinMap Plutarch.Api.V1.PValidatorHash Plutarch.Api.V1.PDatumHash)@
punsafeCoerce datum.effects
atLeastOneNegativeResult :: Term _ PBool
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 at most five cosigners" $ plength # (pfromData datum.cosigners) #< 6
]

View file

@ -8,13 +8,11 @@ Plutus Scripts for Proposals.
module Agora.Proposal.Scripts (
proposalValidator,
proposalPolicy,
proposalDatumValid,
) where
import Agora.Proposal (
PProposalDatum (PProposalDatum),
PProposalRedeemer (..),
PResultTag,
Proposal (governorSTAssetClass, stakeSTAssetClass),
)
import Agora.Record (mkRecordConstr, (.&), (.=))
@ -23,27 +21,23 @@ import Agora.Utils (
anyOutput,
findTxOutByTxOutRef,
passert,
pnotNull,
psymbolValueOf,
ptokenSpent,
ptxSignedBy,
pvalueSpent,
)
import Plutarch.Api.V1 (
PDatumHash,
PMintingPolicy,
PScriptContext (PScriptContext),
PScriptPurpose (PMinting, PSpending),
PTxInfo (PTxInfo),
PValidator,
PValidatorHash,
mintingPolicySymbol,
mkMintingPolicy,
)
import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
import Plutarch.Builtin (PBuiltinMap)
import Plutarch.Monadic qualified as P
import Plutarch.Unsafe (punsafeCoerce)
import Plutarch.TryFrom (ptryFrom)
import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
{- | Policy for Proposals.
@ -94,10 +88,8 @@ proposalValidator proposal =
PJust txOut <- pmatch $ findTxOutByTxOutRef # txOutRef # txInfoF.inputs
txOutF <- pletFields @'["address", "value"] $ txOut
let proposalDatum :: Term _ Agora.Proposal.PProposalDatum
proposalDatum = pfromData $ punsafeCoerce datum
proposalRedeemer :: Term _ Agora.Proposal.PProposalRedeemer
proposalRedeemer = pfromData $ punsafeCoerce redeemer
(pfromData -> proposalDatum, _) <- ptryFrom @(PAsData PProposalDatum) datum
(pfromData -> proposalRedeemer, _) <- ptryFrom @(PAsData PProposalRedeemer) redeemer
proposalF <-
pletFields
@ -189,27 +181,3 @@ proposalValidator proposal =
spentST #== 1
popaque (pconstant ())
{- | Check for various invariants a proposal must uphold.
This can be used to check both upopn creation and
upon any following state transitions in the proposal.
-}
proposalDatumValid :: Term s (Agora.Proposal.PProposalDatum :--> PBool)
proposalDatumValid =
phoistAcyclic $
plam $ \datum' -> P.do
datum <- pletFields @'["effects", "cosigners"] $ datum'
let effects :: Term _ (PBuiltinMap Agora.Proposal.PResultTag (PBuiltinMap Plutarch.Api.V1.PValidatorHash Plutarch.Api.V1.PDatumHash))
effects = punsafeCoerce datum.effects
atLeastOneNegativeResult :: Term _ PBool
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 at most five cosigners" $ plength # (pfromData datum.cosigners) #< 6
]

View file

@ -61,16 +61,17 @@ import Plutus.V1.Ledger.Value (AssetClass)
import Agora.Proposal (PProposalId, PResultTag, ProposalId (..), ResultTag (..))
import Agora.SafeMoney (GTTag)
import Agora.Utils (
pfindDatum,
pnotNull,
ptryFindDatum,
)
import Control.Applicative (Const)
import Plutarch.Api.V1.Extra (PAssetClass, passetClassValueOf)
import Plutarch.Numeric ()
import Plutarch.SafeMoney (
PDiscrete,
Tagged (..),
)
import Plutarch.TryFrom (PTryFrom)
import Plutarch.TryFrom (PTryFrom (PTryFromExcess, ptryFrom'))
--------------------------------------------------------------------------------
@ -191,6 +192,11 @@ newtype PStakeDatum (s :: S) = PStakeDatum
(PlutusType, PIsData, PDataFields)
via (PIsDataReprInstances PStakeDatum)
instance PTryFrom PData (PAsData PStakeDatum) where
type PTryFromExcess PData (PAsData PStakeDatum) = Const ()
ptryFrom' d k =
k (punsafeCoerce d, ())
instance PUnsafeLiftDecl PStakeDatum where type PLifted PStakeDatum = StakeDatum
deriving via (DerivePConstantViaData StakeDatum PStakeDatum) instance (PConstantDecl StakeDatum)
@ -262,7 +268,7 @@ findStakeOwnedBy ::
:--> PPubKeyHash
:--> PBuiltinList (PAsData (PTuple PDatumHash PDatum))
:--> PBuiltinList (PAsData PTxInInfo)
:--> PMaybe PTxOut
:--> PMaybe (PAsData PStakeDatum)
)
findStakeOwnedBy = phoistAcyclic $
plam $ \ac pk datums inputs ->
@ -273,9 +279,8 @@ findStakeOwnedBy = phoistAcyclic $
txOutF <- pletFields @'["datumHash"] $ txOut
pmatch txOutF.datumHash $ \case
PDNothing _ -> pcon PNothing
PDJust ((pfield @"_0" #) -> dh) ->
-- TODO: PTryFrom here
punsafeCoerce $ pfindDatum # dh # datums
PDJust ((pfield @"_0" #) -> dh) -> P.do
ptryFindDatum @(PAsData PStakeDatum) # dh # datums
stakeDatumOwnedBy :: Term _ (PPubKeyHash :--> PStakeDatum :--> PBool)
stakeDatumOwnedBy =
@ -304,8 +309,7 @@ isInputStakeOwnedBy =
PDJust ((pfield @"_0" #) -> datumHash) ->
pif
(outStakeST #== 1)
-- TODO: use 'ptryFindDatum' instead in the future
( pmatch (pfindDatum # datumHash # datums) $ \case
( pmatch (ptryFindDatum @(PAsData PStakeDatum) # datumHash # datums) $ \case
PNothing -> pcon PFalse
PJust v -> stakeDatumOwnedBy # ss # pfromData (punsafeCoerce v)
)

View file

@ -35,7 +35,7 @@ import Plutarch.Api.V1 (
mintingPolicySymbol,
mkMintingPolicy,
)
import Plutarch.Api.V1.Extra (passetClass)
import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
import Plutarch.Internal (punsafeCoerce)
import Plutarch.Monadic qualified as P
import Plutarch.Numeric
@ -183,7 +183,12 @@ stakeValidator stake =
stCurrencySymbol <- plet $ pconstant $ mintingPolicySymbol $ mkMintingPolicy (stakePolicy stake.gtClassRef)
mintedST <- plet $ psymbolValueOf # stCurrencySymbol # txInfoF.mint
spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ pvalueSpent # txInfoF.inputs
valueSpent <- plet $ pvalueSpent # txInfoF.inputs
spentST <- plet $ psymbolValueOf # stCurrencySymbol #$ valueSpent
let AssetClass (propCs, propTn) = stake.proposalSTClass
proposalSTClass = passetClass # pconstant propCs # pconstant propTn
spentProposalST <- plet $ passetClassValueOf # valueSpent # proposalSTClass
-- Is the stake currently locked?
stakeIsLocked <- plet $ stakeLocked # stakeDatum'
@ -192,26 +197,76 @@ stakeValidator stake =
PDestroy _ -> P.do
passert "ST at inputs must be 1" $
spentST #== 1
passert "Should burn ST" $
mintedST #== -1
passert "Stake unlocked" $ pnot # stakeIsLocked
passert
"Owner signs this transaction"
ownerSignsTransaction
passert "Owner signs this transaction" ownerSignsTransaction
popaque (pconstant ())
--------------------------------------------------------------------------
PRetractVotes _ -> P.do
passert
"Owner signs this transaction"
ownerSignsTransaction
-- TODO: check proposal constraints
passert "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
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 ())
--------------------------------------------------------------------------
PPermitVote _ -> P.do
passert
"Owner signs this transaction"
ownerSignsTransaction
-- TODO: check proposal constraints
passert "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
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
@ -225,6 +280,9 @@ stakeValidator stake =
# 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)

View file

@ -84,7 +84,7 @@ pfindDatum = phoistAcyclic $
plam $ \datumHash datums -> plookupTuple # datumHash # datums
-- | Find a datum with the given hash, and `ptryFrom` it.
ptryFindDatum :: PTryFrom PData a => Term s (PDatumHash :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PMaybe a)
ptryFindDatum :: forall (a :: PType) (s :: S). PTryFrom PData a => Term s (PDatumHash :--> PBuiltinList (PAsData (PTuple PDatumHash PDatum)) :--> PMaybe a)
ptryFindDatum = phoistAcyclic $
plam $ \datumHash inputs -> P.do
pmatch (pfindDatum # datumHash # inputs) $ \case
@ -326,6 +326,7 @@ ptokenSpent =
anyOutput ::
forall (datum :: PType) s.
( PIsData datum
, PTryFrom PData (PAsData datum)
) =>
Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
anyOutput = phoistAcyclic $
@ -337,7 +338,7 @@ anyOutput = phoistAcyclic $
PTxOut txOut' <- pmatch (pfromData txOut'')
txOut <- pletFields @'["value", "datumHash", "address"] txOut'
PDJust dh <- pmatch txOut.datumHash
pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo.datums) $ \case
pmatch (ptryFindDatum @(PAsData datum) # (pfield @"_0" # dh) # txInfo.datums) $ \case
PJust datum -> P.do
predicate # txOut.value # txOut.address # pfromData datum
PNothing -> pcon PFalse
@ -348,6 +349,7 @@ anyOutput = phoistAcyclic $
allOutputs ::
forall (datum :: PType) s.
( PIsData datum
, PTryFrom PData (PAsData datum)
) =>
Term s (PTxInfo :--> (PTxOut :--> PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
allOutputs = phoistAcyclic $
@ -359,7 +361,7 @@ allOutputs = phoistAcyclic $
PTxOut txOut' <- pmatch (pfromData txOut'')
txOut <- pletFields @'["value", "datumHash", "address"] txOut'
PDJust dh <- pmatch txOut.datumHash
pmatch (pfindDatum' @datum # (pfield @"_0" # dh) # txInfo.datums) $ \case
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

View file

@ -4,7 +4,7 @@ This document gives an overview of the technical design of the proposals system
| Specification | Implementation | Last revision |
|:-----------:|:-----------:|:-------------:|
| WIP | WIP | v0.1 2022-04-11 |
| WIP | WIP | v0.1 2022-04-27 |
---
@ -35,7 +35,12 @@ Initiating a proposal requires the proposer to have more than a certain amount o
### Voting stages
The life-cycle of a proposal is neatly represented by a state machine, with the 'draft' phase being the initial state, and 'executed' and 'failed' being the terminating states. Please note that this state-machine representation is purely conceptual and should not be expected to reflect technical implementation.
The life-cycle of a proposal is neatly represented by a state machine, with the 'draft' phase being the initial state, and 'executed' and 'failed' being the terminating states.
**Please note that this state-machine representation is purely conceptual and should not be expected to reflect technical implementation.** This is because some state transitions in the state machine representation don't need to happen in the actual implementation as a transaction. A key example is going from the "lock" phase to the "execution" phase. The only thing that needs to happen is that time goes by. So under the hood, they are represented the same in the Proposal's datum.
> Emily 2022-04-27: This is quite confusing still, I feel. @Jack, could you try to reword this and make it more clear?
![](../diagrams/ProposalStateMachine.svg)