remove anyOutput
This commit is contained in:
fanghr
parent
75c236db01
commit
ab12406f3d
3 changed files with 163 additions and 191 deletions
|
|
@ -21,7 +21,6 @@ import Agora.Proposal.Time (currentProposalTime, isVotingPeriod)
|
|||
import Agora.Record (mkRecordConstr, (.&), (.=))
|
||||
import Agora.Stake (PProposalLock (..), PStakeDatum (..), findStakeOwnedBy)
|
||||
import Agora.Utils (
|
||||
anyOutput,
|
||||
findTxOutByTxOutRef,
|
||||
getMintingPolicySymbol,
|
||||
mustBePJust,
|
||||
|
|
@ -346,34 +345,22 @@ proposalValidator proposal =
|
|||
)
|
||||
# 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" $
|
||||
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
|
||||
.& #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
|
||||
]
|
||||
pforce proposalOutD #== expectedDatum
|
||||
|
||||
pure $ popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
|
|
|
|||
|
|
@ -11,14 +11,12 @@ import Agora.Record (mkRecordConstr, (.&), (.=))
|
|||
import Agora.SafeMoney (GTTag)
|
||||
import Agora.Stake
|
||||
import Agora.Utils (
|
||||
anyOutput,
|
||||
mustBePJust,
|
||||
mustFindDatum',
|
||||
paddValue,
|
||||
pfindTxInByTxOutRef,
|
||||
pgeqByClass,
|
||||
pgeqByClass',
|
||||
pgeqBySymbol,
|
||||
psingletonValue,
|
||||
psymbolValueOf,
|
||||
ptokenSpent,
|
||||
ptxSignedBy,
|
||||
|
|
@ -39,12 +37,13 @@ import Plutarch.Api.V1 (
|
|||
mintingPolicySymbol,
|
||||
mkMintingPolicy,
|
||||
)
|
||||
import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf)
|
||||
import Plutarch.Api.V1.Extra (passetClass, passetClassValueOf, pvalueOf)
|
||||
import Plutarch.Internal (punsafeCoerce)
|
||||
import Plutarch.Numeric
|
||||
import Plutarch.SafeMoney (
|
||||
Tagged (..),
|
||||
pdiscreteValue',
|
||||
pvalueDiscrete',
|
||||
untag,
|
||||
)
|
||||
import Plutus.V1.Ledger.Value (AssetClass (AssetClass))
|
||||
|
|
@ -116,52 +115,44 @@ stakePolicy gtClassRef =
|
|||
mintedST #== 1
|
||||
|
||||
tcassert "A UTXO must exist with the correct output" $
|
||||
anyOutput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value address stakeDatum' ->
|
||||
let cred = pfield @"credential" # address
|
||||
in pmatch cred $ \case
|
||||
-- Should pay to a script address
|
||||
PPubKeyCredential _ -> pcon PFalse
|
||||
PScriptCredential validatorHash -> unTermCont $ do
|
||||
stakeDatum <- tcont $ pletFields @'["owner", "stakedAmount"] stakeDatum'
|
||||
unTermCont $ do
|
||||
let scriptOutputWithStakeST =
|
||||
mustBePJust
|
||||
# "Output to script not found"
|
||||
#$ pfind
|
||||
# plam
|
||||
( \output -> unTermCont $ do
|
||||
outputF <- tcont $ pletFields @'["value", "address"] output
|
||||
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 =
|
||||
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
|
||||
let hasExpectedStake =
|
||||
ptraceIfFalse "Stake ouput has expected amount of stake token" $
|
||||
pvalueDiscrete' gtClassRef # outputF.value #== datumF.stakedAmount
|
||||
let ownerSignsTransaction =
|
||||
ptraceIfFalse "Stake Owner should sign the transaction" $
|
||||
ptxSignedBy
|
||||
# txInfoF.signatories
|
||||
# datumF.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
|
||||
# ownSymbol
|
||||
# tn
|
||||
# value
|
||||
# expectedValue
|
||||
]
|
||||
pure $ hasExpectedStake #&& ownerSignsTransaction
|
||||
|
||||
pure $ ownerSignsTransaction #&& valueCorrect
|
||||
pure $ popaque (pconstant ())
|
||||
|
||||
pure $ pif (0 #< mintedST) minting burning
|
||||
|
|
@ -223,7 +214,7 @@ stakeValidator stake =
|
|||
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
|
||||
txInfoF <- tcont $ pletFields @'["mint", "inputs", "outputs", "signatories", "datums"] txInfo
|
||||
|
||||
(pfromData -> stakeRedeemer, _) <- tctryFrom redeemer
|
||||
|
||||
|
|
@ -253,6 +244,43 @@ stakeValidator stake =
|
|||
-- Is the stake currently locked?
|
||||
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 $
|
||||
pmatch stakeRedeemer $ \case
|
||||
PDestroy _ -> unTermCont $ do
|
||||
|
|
@ -282,20 +310,16 @@ stakeValidator stake =
|
|||
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)
|
||||
unTermCont $ do
|
||||
let valueCorrect = pforce ownOutputValueUnchangedD
|
||||
|
||||
-- TODO: check output datum is expected.
|
||||
|
||||
pure $
|
||||
foldl1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||
]
|
||||
|
||||
pure $ popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
|
|
@ -319,31 +343,21 @@ stakeValidator stake =
|
|||
|
||||
expectedDatum <-
|
||||
tclet $
|
||||
pdata $
|
||||
mkRecordConstr
|
||||
PStakeDatum
|
||||
( #stakedAmount .= stakeDatum.stakedAmount
|
||||
.& #owner .= stakeDatum.owner
|
||||
.& #lockedBy .= pdata expectedLocks
|
||||
)
|
||||
mkRecordConstr
|
||||
PStakeDatum
|
||||
( #stakedAmount .= stakeDatum.stakedAmount
|
||||
.& #owner .= stakeDatum.owner
|
||||
.& #lockedBy .= pdata expectedLocks
|
||||
)
|
||||
|
||||
tcassert "A UTXO must exist with the correct output" $
|
||||
-- FIXME: no need to pass the whole txInfo to 'anyOutput'.
|
||||
anyOutput @PStakeDatum # txInfo
|
||||
#$ plam
|
||||
$ \value address newStakeDatum' ->
|
||||
let isScriptAddress = pdata address #== ownAddress
|
||||
correctOutputDatum = pdata newStakeDatum' #== expectedDatum
|
||||
valueCorrect = pdata continuingValue #== pdata value
|
||||
in pif
|
||||
isScriptAddress
|
||||
( foldl1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||
, ptraceIfFalse "datumCorrect" correctOutputDatum
|
||||
]
|
||||
)
|
||||
(pcon PFalse)
|
||||
let correctOutputDatum = pdata (pforce stakeOutD) #== pdata expectedDatum
|
||||
valueCorrect = pforce ownOutputValueUnchangedD
|
||||
in foldl1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||
, ptraceIfFalse "datumCorrect" correctOutputDatum
|
||||
]
|
||||
|
||||
pure $ popaque (pconstant ())
|
||||
--------------------------------------------------------------------------
|
||||
|
|
@ -366,21 +380,13 @@ stakeValidator stake =
|
|||
(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)
|
||||
let correctOutputDatum = pforce stakeOutUnchangedD
|
||||
valueCorrect = pforce ownOutputValueUnchangedD
|
||||
in foldl1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||
, ptraceIfFalse "correctOutputDatum" correctOutputDatum
|
||||
]
|
||||
pure $ popaque (pconstant ())
|
||||
PDepositWithdraw r -> unTermCont $ do
|
||||
tcassert "ST at inputs must be 1" $
|
||||
|
|
@ -391,45 +397,50 @@ stakeValidator stake =
|
|||
"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)
|
||||
unTermCont $ do
|
||||
let stakeOut = pforce stakeOutD
|
||||
|
||||
-- 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
|
||||
]
|
||||
let oldStakedAmount = pfromData $ stakeDatum.stakedAmount
|
||||
delta = pfromData $ pfield @"delta" # r
|
||||
|
||||
pure $
|
||||
foldr1
|
||||
(#&&)
|
||||
[ ptraceIfFalse "isScriptAddress" isScriptAddress
|
||||
, ptraceIfFalse "correctOutputDatum" correctOutputDatum
|
||||
, ptraceIfFalse "valueCorrect" valueCorrect
|
||||
]
|
||||
newStakedAmount <- tclet $ oldStakedAmount + delta
|
||||
|
||||
tcassert "New staked amount shoudl be greater than or equal to 0" $
|
||||
zero #<= newStakedAmount
|
||||
|
||||
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 ())
|
||||
|
|
|
|||
|
|
@ -44,7 +44,6 @@ module Agora.Utils (
|
|||
pmapMaybe,
|
||||
|
||||
-- * Functions which should (probably) not be upstreamed
|
||||
anyOutput,
|
||||
findTxOutByTxOutRef,
|
||||
scriptHashFromAddress,
|
||||
findOutputsToAddress,
|
||||
|
|
@ -87,7 +86,6 @@ import Plutarch.Api.V1 (
|
|||
PTokenName (PTokenName),
|
||||
PTuple,
|
||||
PTxInInfo (PTxInInfo),
|
||||
PTxInfo,
|
||||
PTxOut (PTxOut),
|
||||
PTxOutRef,
|
||||
PValidatorHash,
|
||||
|
|
@ -556,30 +554,6 @@ phalve = phoistAcyclic $ plam $ \l -> go # l # l
|
|||
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.
|
||||
psingletonValue :: forall s. Term s (PCurrencySymbol :--> PTokenName :--> PInteger :--> PValue)
|
||||
psingletonValue = phoistAcyclic $
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue