remove anyOutput

This commit is contained in:
fanghr 2022-05-23 23:18:18 +08:00
parent e89b245b20
commit 6145d9ef68
3 changed files with 163 additions and 191 deletions

View file

@ -21,7 +21,6 @@ import Agora.Proposal.Time (currentProposalTime, isVotingPeriod)
import Agora.Record (mkRecordConstr, (.&), (.=)) import Agora.Record (mkRecordConstr, (.&), (.=))
import Agora.Stake (PProposalLock (..), PStakeDatum (..), findStakeOwnedBy) import Agora.Stake (PProposalLock (..), PStakeDatum (..), findStakeOwnedBy)
import Agora.Utils ( import Agora.Utils (
anyOutput,
findTxOutByTxOutRef, findTxOutByTxOutRef,
getMintingPolicySymbol, getMintingPolicySymbol,
mustBePJust, mustBePJust,
@ -346,34 +345,22 @@ proposalValidator proposal =
) )
# newSigs # newSigs
let updatedSigs = pconcat # newSigs # proposalF.cosigners
expectedDatum =
mkRecordConstr
PProposalDatum
( #proposalId .= proposalF.proposalId
.& #effects .= proposalF.effects
.& #status .= proposalF.status
.& #cosigners .= pdata updatedSigs
.& #thresholds .= proposalF.thresholds
.& #votes .= proposalF.votes
.& #timingConfig .= proposalF.timingConfig
.& #startingTime .= proposalF.startingTime
)
tcassert "Signatures are correctly added to cosignature list" $ tcassert "Signatures are correctly added to cosignature list" $
anyOutput @PProposalDatum # ctx.txInfo pforce proposalOutD #== expectedDatum
#$ 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
.& #timingConfig .= proposalF.timingConfig
.& #startingTime .= proposalF.startingTime
)
)
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
]
pure $ popaque (pconstant ()) pure $ popaque (pconstant ())
-------------------------------------------------------------------------- --------------------------------------------------------------------------

View file

@ -11,14 +11,12 @@ import Agora.Record (mkRecordConstr, (.&), (.=))
import Agora.SafeMoney (GTTag) import Agora.SafeMoney (GTTag)
import Agora.Stake import Agora.Stake
import Agora.Utils ( import Agora.Utils (
anyOutput, mustBePJust,
mustFindDatum', mustFindDatum',
paddValue, paddValue,
pfindTxInByTxOutRef, pfindTxInByTxOutRef,
pgeqByClass,
pgeqByClass', pgeqByClass',
pgeqBySymbol, pgeqBySymbol,
psingletonValue,
psymbolValueOf, psymbolValueOf,
ptokenSpent, ptokenSpent,
ptxSignedBy, ptxSignedBy,
@ -39,12 +37,13 @@ import Plutarch.Api.V1 (
mintingPolicySymbol, mintingPolicySymbol,
mkMintingPolicy, mkMintingPolicy,
) )
import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf) import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf, pvalueOf)
import Plutarch.Internal (punsafeCoerce) import Plutarch.Internal (punsafeCoerce)
import Plutarch.Numeric import Plutarch.Numeric
import Plutarch.SafeMoney ( import Plutarch.SafeMoney (
Tagged (..), Tagged (..),
pdiscreteValue', pdiscreteValue',
pvalueDiscrete',
untag, untag,
) )
import Plutus.V1.Ledger.Value (AssetClass (AssetClass)) import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
@ -116,52 +115,44 @@ stakePolicy gtClassRef =
mintedST #== 1 mintedST #== 1
tcassert "A UTXO must exist with the correct output" $ tcassert "A UTXO must exist with the correct output" $
anyOutput @PStakeDatum # txInfo unTermCont $ do
#$ plam let scriptOutputWithStakeST =
$ \value address stakeDatum' -> mustBePJust
let cred = pfield @"credential" # address # "Output to script not found"
in pmatch cred $ \case #$ pfind
-- Should pay to a script address # plam
PPubKeyCredential _ -> pcon PFalse ( \output -> unTermCont $ do
PScriptCredential validatorHash -> unTermCont $ do outputF <- tcont $ pletFields @'["value", "address"] output
stakeDatum <- tcont $ pletFields @'["owner", "stakedAmount"] stakeDatum' pure $
pmatch (pfromData $ pfield @"credential" # outputF.address) $ \case
-- Should pay to a script address
PPubKeyCredential _ -> pcon PFalse
PScriptCredential ((pfield @"_0" #) -> validatorHash) ->
let tn :: Term _ PTokenName
tn = pvalidatorHashToTokenName validatorHash
in pvalueOf # outputF.value # ownSymbol # tn #== 1
)
# pfromData txInfoF.outputs
tn :: Term _ PTokenName <- tclet (pvalidatorHashToTokenName $ pfromData $ pfield @"_0" # validatorHash) outputF <-
tcont $
pletFields @'["value", "address", "datumHash"] scriptOutputWithStakeST
datumF <-
tcont $
pletFields @'["owner", "stakedAmount"] $
mustFindDatum' @PStakeDatum # outputF.datumHash # txInfoF.datums
let stValue = let hasExpectedStake =
psingletonValue ptraceIfFalse "Stake ouput has expected amount of stake token" $
# ownSymbol pvalueDiscrete' gtClassRef # outputF.value #== datumF.stakedAmount
-- This coerce is safe because the structure let ownerSignsTransaction =
-- of PValidatorHash is the same as PTokenName. ptraceIfFalse "Stake Owner should sign the transaction" $
# tn ptxSignedBy
# 1 # txInfoF.signatories
let expectedValue = # datumF.owner
paddValue
# (pdiscreteValue' gtClassRef # stakeDatum.stakedAmount)
# stValue
let ownerSignsTransaction =
ptxSignedBy
# txInfoF.signatories
# stakeDatum.owner
-- TODO: This is quite inefficient now, as it does two lookups pure $ hasExpectedStake #&& ownerSignsTransaction
-- 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
]
pure $ ownerSignsTransaction #&& valueCorrect
pure $ popaque (pconstant ()) pure $ popaque (pconstant ())
pure $ pif (0 #< mintedST) minting burning pure $ pif (0 #< mintedST) minting burning
@ -223,7 +214,7 @@ stakeValidator stake =
plam $ \datum redeemer ctx' -> unTermCont $ do plam $ \datum redeemer ctx' -> unTermCont $ do
ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx' ctx <- tcont $ pletFields @'["txInfo", "purpose"] ctx'
txInfo <- tclet $ pfromData ctx.txInfo txInfo <- tclet $ pfromData ctx.txInfo
txInfoF <- tcont $ pletFields @'["mint", "inputs", "outputs", "signatories"] txInfo txInfoF <- tcont $ pletFields @'["mint", "inputs", "outputs", "signatories", "datums"] txInfo
(pfromData -> stakeRedeemer, _) <- tctryFrom redeemer (pfromData -> stakeRedeemer, _) <- tctryFrom redeemer
@ -253,6 +244,43 @@ stakeValidator stake =
-- Is the stake currently locked? -- Is the stake currently locked?
stakeIsLocked <- tclet $ stakeLocked # stakeDatum' stakeIsLocked <- tclet $ stakeLocked # stakeDatum'
-- Filter out own output with own address and PST.
-- Delay the evaluation cause in some cases there won't be any continuing output.
ownOutputD <-
tclet $
pdelay $
mustBePJust # "Own output should be present" #$ pfind
# plam
( \input -> unTermCont $ do
inputF <- tcont $ pletFields @'["address", "value"] input
pure $
inputF.address #== ownAddress
#&& psymbolValueOf # stCurrencySymbol # inputF.value #== 1
)
# pfromData txInfoF.outputs
stakeOutD <-
tclet $
pdelay $
mustFindDatum' @PStakeDatum
# (pfield @"datumHash" # pforce ownOutputD)
# txInfoF.datums
ownOutputValueD <-
tclet $
pdelay $
pfield @"value" # pforce ownOutputD
ownOutputValueUnchangedD <-
tclet $
pdelay $
pdata continuingValue #== pdata (pforce ownOutputValueD)
stakeOutUnchangedD <-
tclet $
pdelay $
pdata (pforce stakeOutD) #== pdata stakeDatum'
pure $ pure $
pmatch stakeRedeemer $ \case pmatch stakeRedeemer $ \case
PDestroy _ -> unTermCont $ do PDestroy _ -> unTermCont $ do
@ -282,20 +310,16 @@ stakeValidator stake =
spentProposalST #== 1 spentProposalST #== 1
tcassert "A UTXO must exist with the correct output" $ tcassert "A UTXO must exist with the correct output" $
anyOutput @PStakeDatum # txInfo unTermCont $ do
#$ plam let valueCorrect = pforce ownOutputValueUnchangedD
$ \value address newStakeDatum' ->
let isScriptAddress = pdata address #== ownAddress -- TODO: check output datum is expected.
_correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum'
valueCorrect = pdata continuingValue #== pdata value pure $
in pif foldl1
isScriptAddress (#&&)
( foldl1 [ ptraceIfFalse "valueCorrect" valueCorrect
(#&&) ]
[ ptraceIfFalse "valueCorrect" valueCorrect
]
)
(pcon PFalse)
pure $ popaque (pconstant ()) pure $ popaque (pconstant ())
-------------------------------------------------------------------------- --------------------------------------------------------------------------
@ -319,31 +343,21 @@ stakeValidator stake =
expectedDatum <- expectedDatum <-
tclet $ tclet $
pdata $ mkRecordConstr
mkRecordConstr PStakeDatum
PStakeDatum ( #stakedAmount .= stakeDatum.stakedAmount
( #stakedAmount .= stakeDatum.stakedAmount .& #owner .= stakeDatum.owner
.& #owner .= stakeDatum.owner .& #lockedBy .= pdata expectedLocks
.& #lockedBy .= pdata expectedLocks )
)
tcassert "A UTXO must exist with the correct output" $ tcassert "A UTXO must exist with the correct output" $
-- FIXME: no need to pass the whole txInfo to 'anyOutput'. let correctOutputDatum = pdata (pforce stakeOutD) #== pdata expectedDatum
anyOutput @PStakeDatum # txInfo valueCorrect = pforce ownOutputValueUnchangedD
#$ plam in foldl1
$ \value address newStakeDatum' -> (#&&)
let isScriptAddress = pdata address #== ownAddress [ ptraceIfFalse "valueCorrect" valueCorrect
correctOutputDatum = pdata newStakeDatum' #== expectedDatum , ptraceIfFalse "datumCorrect" correctOutputDatum
valueCorrect = pdata continuingValue #== pdata value ]
in pif
isScriptAddress
( foldl1
(#&&)
[ ptraceIfFalse "valueCorrect" valueCorrect
, ptraceIfFalse "datumCorrect" correctOutputDatum
]
)
(pcon PFalse)
pure $ popaque (pconstant ()) pure $ popaque (pconstant ())
-------------------------------------------------------------------------- --------------------------------------------------------------------------
@ -366,21 +380,13 @@ stakeValidator stake =
(ownerSignsTransaction #|| proposalTokenMoved) (ownerSignsTransaction #|| proposalTokenMoved)
tcassert "A UTXO must exist with the correct output" $ tcassert "A UTXO must exist with the correct output" $
anyOutput @PStakeDatum # txInfo let correctOutputDatum = pforce stakeOutUnchangedD
#$ plam valueCorrect = pforce ownOutputValueUnchangedD
$ \value address newStakeDatum' -> in foldl1
let isScriptAddress = pdata address #== ownAddress (#&&)
correctOutputDatum = pdata newStakeDatum' #== pdata stakeDatum' [ ptraceIfFalse "valueCorrect" valueCorrect
valueCorrect = pdata continuingValue #== pdata value , ptraceIfFalse "correctOutputDatum" correctOutputDatum
in pif ]
isScriptAddress
( foldl1
(#&&)
[ ptraceIfFalse "valueCorrect" valueCorrect
, ptraceIfFalse "correctOutputDatum" correctOutputDatum
]
)
(pcon PFalse)
pure $ popaque (pconstant ()) pure $ popaque (pconstant ())
PDepositWithdraw r -> unTermCont $ do PDepositWithdraw r -> unTermCont $ do
tcassert "ST at inputs must be 1" $ tcassert "ST at inputs must be 1" $
@ -391,45 +397,50 @@ stakeValidator stake =
"Owner signs this transaction" "Owner signs this transaction"
ownerSignsTransaction ownerSignsTransaction
tcassert "A UTXO must exist with the correct output" $ tcassert "A UTXO must exist with the correct output" $
anyOutput @PStakeDatum # txInfo unTermCont $ do
#$ plam let stakeOut = pforce stakeOutD
$ \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 let oldStakedAmount = pfromData $ stakeDatum.stakedAmount
-- instead of a more efficient single pass, delta = pfromData $ pfield @"delta" # r
-- 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 $ newStakedAmount <- tclet $ oldStakedAmount + delta
foldr1
(#&&) tcassert "New staked amount shoudl be greater than or equal to 0" $
[ ptraceIfFalse "isScriptAddress" isScriptAddress zero #<= newStakedAmount
, ptraceIfFalse "correctOutputDatum" correctOutputDatum
, ptraceIfFalse "valueCorrect" valueCorrect let expectedDatum =
] mkRecordConstr
PStakeDatum
( #stakedAmount .= pdata newStakedAmount
.& #owner .= stakeDatum.owner
.& #lockedBy .= stakeDatum.lockedBy
)
datumCorrect = stakeOut #== expectedDatum
ownOutputValue <- tclet $ pforce ownOutputValueD
let expectedValue = paddValue # continuingValue # (pdiscreteValue' stake.gtClassRef # delta)
valueCorrect =
foldr1
(#&&)
[ pgeqByClass' (AssetClass ("", ""))
# ownOutputValue
# expectedValue
, pgeqByClass' (untag stake.gtClassRef)
# ownOutputValue
# expectedValue
, pgeqBySymbol
# stCurrencySymbol
# ownOutputValue
# expectedValue
]
pure $
foldl1
(#&&)
[ ptraceIfFalse "valueCorrect" valueCorrect
, ptraceIfFalse "datumCorrect" datumCorrect
]
pure $ popaque (pconstant ()) pure $ popaque (pconstant ())

View file

@ -44,7 +44,6 @@ module Agora.Utils (
pmapMaybe, pmapMaybe,
-- * Functions which should (probably) not be upstreamed -- * Functions which should (probably) not be upstreamed
anyOutput,
findTxOutByTxOutRef, findTxOutByTxOutRef,
scriptHashFromAddress, scriptHashFromAddress,
findOutputsToAddress, findOutputsToAddress,
@ -87,7 +86,6 @@ import Plutarch.Api.V1 (
PTokenName (PTokenName), PTokenName (PTokenName),
PTuple, PTuple,
PTxInInfo (PTxInInfo), PTxInInfo (PTxInInfo),
PTxInfo,
PTxOut (PTxOut), PTxOut (PTxOut),
PTxOutRef, PTxOutRef,
PValidatorHash, PValidatorHash,
@ -556,30 +554,6 @@ phalve = phoistAcyclic $ plam $ \l -> go # l # l
All of these functions are quite inefficient. All of these functions are quite inefficient.
-} -}
-- | Check if any output matches the predicate.
anyOutput ::
forall (datum :: PType) s.
( PIsData datum
, PTryFrom PData (PAsData datum)
) =>
Term s (PTxInfo :--> (PValue :--> PAddress :--> datum :--> PBool) :--> PBool)
anyOutput = phoistAcyclic $
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
-- | Create a value with a single asset class. -- | Create a value with a single asset class.
psingletonValue :: forall s. Term s (PCurrencySymbol :--> PTokenName :--> PInteger :--> PValue) psingletonValue :: forall s. Term s (PCurrencySymbol :--> PTokenName :--> PInteger :--> PValue)
psingletonValue = phoistAcyclic $ psingletonValue = phoistAcyclic $