use nested pmatches instead of laziness
This commit is contained in:
fanghr
parent
6145d9ef68
commit
cafe91f7a1
2 changed files with 179 additions and 184 deletions
|
|
@ -187,25 +187,23 @@ proposalValidator proposal =
|
||||||
|
|
||||||
-- Filter out own output with own address and PST.
|
-- Filter out own output with own address and PST.
|
||||||
-- Delay the evaluation cause in some cases there won't be any continuing output.
|
-- Delay the evaluation cause in some cases there won't be any continuing output.
|
||||||
ownOutputD <-
|
ownOutput <-
|
||||||
tclet $
|
tclet $
|
||||||
pdelay $
|
mustBePJust # "Own output should be present" #$ pfind
|
||||||
mustBePJust # "Own output should be present" #$ pfind
|
# plam
|
||||||
# plam
|
( \input -> unTermCont $ do
|
||||||
( \input -> unTermCont $ do
|
inputF <- tcont $ pletFields @'["address", "value"] input
|
||||||
inputF <- tcont $ pletFields @'["address", "value"] input
|
pure $
|
||||||
pure $
|
inputF.address #== ownAddress
|
||||||
inputF.address #== ownAddress
|
#&& psymbolValueOf # stCurrencySymbol # inputF.value #== 1
|
||||||
#&& psymbolValueOf # stCurrencySymbol # inputF.value #== 1
|
)
|
||||||
)
|
# pfromData txInfoF.outputs
|
||||||
# pfromData txInfoF.outputs
|
|
||||||
|
|
||||||
proposalOutD <-
|
proposalOut <-
|
||||||
tclet $
|
tclet $
|
||||||
pdelay $
|
mustFindDatum' @PProposalDatum
|
||||||
mustFindDatum' @PProposalDatum
|
# (pfield @"datumHash" # ownOutput)
|
||||||
# (pfield @"datumHash" # pforce ownOutputD)
|
# txInfoF.datums
|
||||||
# txInfoF.datums
|
|
||||||
|
|
||||||
pure $
|
pure $
|
||||||
pmatch proposalRedeemer $ \case
|
pmatch proposalRedeemer $ \case
|
||||||
|
|
@ -273,7 +271,7 @@ proposalValidator proposal =
|
||||||
.& #startingTime .= proposalF.startingTime
|
.& #startingTime .= proposalF.startingTime
|
||||||
)
|
)
|
||||||
|
|
||||||
tcassert "Output proposal should be valid" $ pforce proposalOutD #== expectedProposalOut
|
tcassert "Output proposal should be valid" $ proposalOut #== expectedProposalOut
|
||||||
|
|
||||||
-- We validate the output stake datum here as well: We need the vote option
|
-- We validate the output stake datum here as well: We need the vote option
|
||||||
-- to create a valid 'ProposalLock', however the vote option is encoded
|
-- to create a valid 'ProposalLock', however the vote option is encoded
|
||||||
|
|
@ -360,7 +358,7 @@ proposalValidator proposal =
|
||||||
)
|
)
|
||||||
|
|
||||||
tcassert "Signatures are correctly added to cosignature list" $
|
tcassert "Signatures are correctly added to cosignature list" $
|
||||||
pforce proposalOutD #== expectedDatum
|
proposalOut #== expectedDatum
|
||||||
|
|
||||||
pure $ popaque (pconstant ())
|
pure $ popaque (pconstant ())
|
||||||
--------------------------------------------------------------------------
|
--------------------------------------------------------------------------
|
||||||
|
|
|
||||||
|
|
@ -244,43 +244,6 @@ 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
|
||||||
|
|
@ -296,151 +259,185 @@ stakeValidator stake =
|
||||||
|
|
||||||
pure $ popaque (pconstant ())
|
pure $ popaque (pconstant ())
|
||||||
--------------------------------------------------------------------------
|
--------------------------------------------------------------------------
|
||||||
PRetractVotes _ -> unTermCont $ do
|
-- Handle redeemers that require own stake output.
|
||||||
tcassert
|
_ -> unTermCont $ do
|
||||||
"Owner signs this transaction"
|
-- Filter out own output with own address and PST.
|
||||||
ownerSignsTransaction
|
ownOutput <-
|
||||||
|
|
||||||
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.
|
|
||||||
tcassert "Proposal ST spent" $
|
|
||||||
spentProposalST #== 1
|
|
||||||
|
|
||||||
tcassert "A UTXO must exist with the correct output" $
|
|
||||||
unTermCont $ do
|
|
||||||
let valueCorrect = pforce ownOutputValueUnchangedD
|
|
||||||
|
|
||||||
-- TODO: check output datum is expected.
|
|
||||||
|
|
||||||
pure $
|
|
||||||
foldl1
|
|
||||||
(#&&)
|
|
||||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
|
||||||
]
|
|
||||||
|
|
||||||
pure $ popaque (pconstant ())
|
|
||||||
--------------------------------------------------------------------------
|
|
||||||
PPermitVote l -> 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
|
|
||||||
|
|
||||||
-- Update the stake datum, but only the 'lockedBy' field.
|
|
||||||
|
|
||||||
let -- We actually don't know whether the given lock is valid or not.
|
|
||||||
-- This is checked in the proposal validator.
|
|
||||||
newLock = pfield @"lock" # l
|
|
||||||
-- Prepend the new lock to the existing locks.
|
|
||||||
expectedLocks = pcons # newLock # stakeDatum.lockedBy
|
|
||||||
|
|
||||||
expectedDatum <-
|
|
||||||
tclet $
|
tclet $
|
||||||
mkRecordConstr
|
mustBePJust # "Own output should be present" #$ pfind
|
||||||
PStakeDatum
|
# plam
|
||||||
( #stakedAmount .= stakeDatum.stakedAmount
|
( \input -> unTermCont $ do
|
||||||
.& #owner .= stakeDatum.owner
|
inputF <- tcont $ pletFields @'["address", "value"] input
|
||||||
.& #lockedBy .= pdata expectedLocks
|
pure $
|
||||||
)
|
inputF.address #== ownAddress
|
||||||
|
#&& psymbolValueOf # stCurrencySymbol # inputF.value #== 1
|
||||||
|
)
|
||||||
|
# pfromData txInfoF.outputs
|
||||||
|
|
||||||
tcassert "A UTXO must exist with the correct output" $
|
stakeOut <-
|
||||||
let correctOutputDatum = pdata (pforce stakeOutD) #== pdata expectedDatum
|
tclet $
|
||||||
valueCorrect = pforce ownOutputValueUnchangedD
|
mustFindDatum' @PStakeDatum
|
||||||
in foldl1
|
# (pfield @"datumHash" # ownOutput)
|
||||||
(#&&)
|
# txInfoF.datums
|
||||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
|
||||||
, ptraceIfFalse "datumCorrect" correctOutputDatum
|
|
||||||
]
|
|
||||||
|
|
||||||
pure $ popaque (pconstant ())
|
ownOutputValue <-
|
||||||
--------------------------------------------------------------------------
|
tclet $
|
||||||
PWitnessStake _ -> unTermCont $ do
|
pfield @"value" # ownOutput
|
||||||
tcassert "ST at inputs must be 1" $
|
|
||||||
spentST #== 1
|
|
||||||
|
|
||||||
let AssetClass (propCs, propTn) = stake.proposalSTClass
|
ownOutputValueUnchanged <-
|
||||||
propAssetClass = passetClass # pconstant propCs # pconstant propTn
|
tclet $
|
||||||
proposalTokenMoved =
|
pdata continuingValue #== pdata ownOutputValue
|
||||||
ptokenSpent
|
|
||||||
# propAssetClass
|
|
||||||
# txInfoF.inputs
|
|
||||||
|
|
||||||
-- In order for cosignature to be witnessed, it must be possible for a
|
stakeOutUnchanged <-
|
||||||
-- proposal to allow this transaction to happen. This puts trust into the Proposal.
|
tclet $
|
||||||
-- The Proposal must necessarily check that this is not abused.
|
pdata stakeOut #== pdata stakeDatum'
|
||||||
tcassert
|
|
||||||
"Owner signs this transaction OR proposal token is spent"
|
|
||||||
(ownerSignsTransaction #|| proposalTokenMoved)
|
|
||||||
|
|
||||||
tcassert "A UTXO must exist with the correct output" $
|
pure $
|
||||||
let correctOutputDatum = pforce stakeOutUnchangedD
|
pmatch stakeRedeemer $ \case
|
||||||
valueCorrect = pforce ownOutputValueUnchangedD
|
PRetractVotes _ -> unTermCont $ do
|
||||||
in foldl1
|
tcassert
|
||||||
(#&&)
|
"Owner signs this transaction"
|
||||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
ownerSignsTransaction
|
||||||
, ptraceIfFalse "correctOutputDatum" correctOutputDatum
|
|
||||||
]
|
|
||||||
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" $
|
|
||||||
unTermCont $ do
|
|
||||||
let stakeOut = pforce stakeOutD
|
|
||||||
|
|
||||||
let oldStakedAmount = pfromData $ stakeDatum.stakedAmount
|
tcassert "ST at inputs must be 1" $
|
||||||
delta = pfromData $ pfield @"delta" # r
|
spentST #== 1
|
||||||
|
|
||||||
newStakedAmount <- tclet $ oldStakedAmount + delta
|
-- This puts trust into the Proposal. The Proposal must necessarily check
|
||||||
|
-- that this is not abused.
|
||||||
|
tcassert "Proposal ST spent" $
|
||||||
|
spentProposalST #== 1
|
||||||
|
|
||||||
tcassert "New staked amount shoudl be greater than or equal to 0" $
|
tcassert "A UTXO must exist with the correct output" $
|
||||||
zero #<= newStakedAmount
|
unTermCont $ do
|
||||||
|
let valueCorrect = ownOutputValueUnchanged
|
||||||
|
|
||||||
let expectedDatum =
|
-- TODO: check output datum is expected.
|
||||||
|
|
||||||
|
pure $
|
||||||
|
foldl1
|
||||||
|
(#&&)
|
||||||
|
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||||
|
]
|
||||||
|
|
||||||
|
pure $ popaque (pconstant ())
|
||||||
|
--------------------------------------------------------------------------
|
||||||
|
PPermitVote l -> 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
|
||||||
|
|
||||||
|
-- Update the stake datum, but only the 'lockedBy' field.
|
||||||
|
|
||||||
|
let -- We actually don't know whether the given lock is valid or not.
|
||||||
|
-- This is checked in the proposal validator.
|
||||||
|
newLock = pfield @"lock" # l
|
||||||
|
-- Prepend the new lock to the existing locks.
|
||||||
|
expectedLocks = pcons # newLock # stakeDatum.lockedBy
|
||||||
|
|
||||||
|
expectedDatum <-
|
||||||
|
tclet $
|
||||||
mkRecordConstr
|
mkRecordConstr
|
||||||
PStakeDatum
|
PStakeDatum
|
||||||
( #stakedAmount .= pdata newStakedAmount
|
( #stakedAmount .= stakeDatum.stakedAmount
|
||||||
.& #owner .= stakeDatum.owner
|
.& #owner .= stakeDatum.owner
|
||||||
.& #lockedBy .= stakeDatum.lockedBy
|
.& #lockedBy .= pdata expectedLocks
|
||||||
)
|
)
|
||||||
datumCorrect = stakeOut #== expectedDatum
|
|
||||||
|
|
||||||
ownOutputValue <- tclet $ pforce ownOutputValueD
|
tcassert "A UTXO must exist with the correct output" $
|
||||||
|
let correctOutputDatum = stakeOut #== expectedDatum
|
||||||
|
valueCorrect = ownOutputValueUnchanged
|
||||||
|
in foldl1
|
||||||
|
(#&&)
|
||||||
|
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||||
|
, ptraceIfFalse "datumCorrect" correctOutputDatum
|
||||||
|
]
|
||||||
|
|
||||||
let expectedValue = paddValue # continuingValue # (pdiscreteValue' stake.gtClassRef # delta)
|
pure $ popaque (pconstant ())
|
||||||
|
--------------------------------------------------------------------------
|
||||||
|
PWitnessStake _ -> unTermCont $ do
|
||||||
|
tcassert "ST at inputs must be 1" $
|
||||||
|
spentST #== 1
|
||||||
|
|
||||||
valueCorrect =
|
let AssetClass (propCs, propTn) = stake.proposalSTClass
|
||||||
foldr1
|
propAssetClass = passetClass # pconstant propCs # pconstant propTn
|
||||||
(#&&)
|
proposalTokenMoved =
|
||||||
[ pgeqByClass' (AssetClass ("", ""))
|
ptokenSpent
|
||||||
# ownOutputValue
|
# propAssetClass
|
||||||
# expectedValue
|
# txInfoF.inputs
|
||||||
, pgeqByClass' (untag stake.gtClassRef)
|
|
||||||
# ownOutputValue
|
|
||||||
# expectedValue
|
|
||||||
, pgeqBySymbol
|
|
||||||
# stCurrencySymbol
|
|
||||||
# ownOutputValue
|
|
||||||
# expectedValue
|
|
||||||
]
|
|
||||||
|
|
||||||
pure $
|
-- In order for cosignature to be witnessed, it must be possible for a
|
||||||
foldl1
|
-- proposal to allow this transaction to happen. This puts trust into the Proposal.
|
||||||
(#&&)
|
-- The Proposal must necessarily check that this is not abused.
|
||||||
[ ptraceIfFalse "valueCorrect" valueCorrect
|
tcassert
|
||||||
, ptraceIfFalse "datumCorrect" datumCorrect
|
"Owner signs this transaction OR proposal token is spent"
|
||||||
]
|
(ownerSignsTransaction #|| proposalTokenMoved)
|
||||||
|
|
||||||
pure $ popaque (pconstant ())
|
tcassert "A UTXO must exist with the correct output" $
|
||||||
|
let correctOutputDatum = stakeOutUnchanged
|
||||||
|
valueCorrect = ownOutputValueUnchanged
|
||||||
|
in foldl1
|
||||||
|
(#&&)
|
||||||
|
[ ptraceIfFalse "valueCorrect" valueCorrect
|
||||||
|
, ptraceIfFalse "correctOutputDatum" correctOutputDatum
|
||||||
|
]
|
||||||
|
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" $
|
||||||
|
unTermCont $ do
|
||||||
|
let oldStakedAmount = pfromData $ stakeDatum.stakedAmount
|
||||||
|
delta = pfromData $ pfield @"delta" # r
|
||||||
|
|
||||||
|
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
|
||||||
|
|
||||||
|
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 ())
|
||||||
|
_ -> popaque (pconstant ())
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue