Validation
rdptr : Tx ℓ → ScriptPurpose → Maybe (RedeemerPtr ℓ) rdptr tx = λ where (Cert h) → map (Cert ,_) $ indexOfDCert h (DCertsOf tx) (Rwrd h) → map (Reward ,_) $ indexOfRewardAddress h (WithdrawalsOf tx) (Mint h) → map (Mint ,_) $ indexOfPolicyId h (policies (MintedValueOf tx)) (Spend h) → map (Spend ,_) $ indexOfTxIn h (SpendInputsOf tx) (Vote h) → map (Vote ,_) $ indexOfVote h (map GovVote.voter (ListOfGovVotesOf tx)) (Propose h) → map (Propose ,_) $ indexOfProposal h (ListOfGovProposalsOf tx) (Guard c) → map (Guard ,_) $ indexOfGuard c (map proj₁ (setToList (GuardsOf tx))) indexedRdmrs : Tx ℓ → ScriptPurpose → Maybe (Redeemer × ExUnits) indexedRdmrs tx sp = maybe (λ x → lookupᵐ? (RedeemersOf tx) x) nothing (rdptr tx sp)
The function getDatumSpend (formerly getDatum)
retrieves the datum required by a phase-2 script associated to a spending input.
Note that, even though this function formally returns an element of type Maybe
Datum, the preconditions of the UTXOW rule
ensure that the datum is always present (otherwise, it is a phase-1 validation
failure).
getDatumSpend : Tx ℓ → UTxO → (DataHash ⇀ Datum) → TxIn → Maybe Datum getDatumSpend tx utxo₀ allData txin with lookupᵐ? utxo₀ txin ... | just (_ , _ , just d , _) = case d of λ where (inj₁ d) → just d (inj₂ h) → lookupᵐ? allData h ... | _ = nothing
In Dijkstra, we introduce the function getDataGuard, which
retrieves the set of data required by a guard script. In addition, the function
returns a boolean that signals whether the guard script is also required without
datum.
getDataGuard : Tx ℓ → UTxO → Credential → ℙ Datum × Bool getDataGuard tx utxo₀ c = mapPartial (λ (c' , d) → if c ≡ c' then d else nothing) (GuardsOf tx) , ¿ (c , nothing) ∈ GuardsOf tx ¿ᵇ
txInfo : (ℓ : TxLevel) → UTxO → Tx ℓ → TxInfo txInfo TxLevelTop utxo tx = record { realizedInputs = utxo ∣ (SpendInputsOf tx) ; txOuts = TxOutsOf tx ; txFee = FeesOf? tx ; mint = MintedValueOf tx ; txCerts = DCertsOf tx ; txWithdrawals = WithdrawalsOf tx ; txVldt = ValidIntervalOf tx ; vkKey = RequiredSignerHashesOf tx ; txGuards = GuardsOf tx ; txData = DataOf tx ; txId = TxIdOf tx ; txInfoSubTxs = nothing } txInfo TxLevelSub utxo tx = record { realizedInputs = utxo ∣ (TxBody.txIns txBody) ; txOuts = TxBody.txOuts txBody ; txFee = nothing ; mint = TxBody.mint txBody ; txCerts = TxBody.txCerts txBody ; txWithdrawals = TxBody.txWithdrawals txBody ; txVldt = TxBody.txVldt txBody ; vkKey = TxBody.requiredSignerHashes txBody ; txGuards = TxBody.txGuards txBody ; txData = DataOf tx ; txId = TxBody.txId txBody ; txInfoSubTxs = nothing } where open Tx tx txInfoForPurpose : {ℓ : TxLevel} → UTxO → Tx ℓ → ScriptPurpose → TxInfo -- subtransactions: never get subTx infos (even if the ScriptPurpose is Guard). txInfoForPurpose {TxLevelSub} utxo tx _ = txInfo TxLevelSub utxo tx -- top-level transactions: txInfoForPurpose {TxLevelTop} utxo tx sp with sp -- · guard scripts see subTx infos ... | Guard _ = record base { txInfoSubTxs = just subInfos } where base : TxInfo base = txInfo TxLevelTop utxo tx subInfos : List SubTxInfo subInfos = map (txInfo TxLevelSub utxo) (SubTransactionsOf tx) -- · other top-level scripts see no subTx infos ... | _ = txInfo TxLevelTop utxo tx txOutToDataHash : TxOut → Maybe DataHash txOutToDataHash (_ , _ , d , _) = d >>= isInj₂
credsNeeded : UTxO → Tx ℓ → ℙ (ScriptPurpose × Credential) credsNeeded utxo tx = mapˢ (λ (i , o) → (Spend i , payCred (proj₁ o))) ((utxo ∣ (SpendInputsOf tx ∪ collateralInputs tx)) ˢ) ∪ mapˢ (λ a → (Rwrd a , CredentialOf a)) (dom ∣ WithdrawalsOf tx ∣) ∪ mapPartial (λ c → (Cert c ,_) <$> cwitness c) (fromList (DCertsOf tx)) ∪ mapˢ (λ x → (Mint x , ScriptObj x)) (policies (MintedValueOf tx)) ∪ mapˢ (λ v → (Vote v , govVoterCredential v)) (fromList (map GovVoterOf (ListOfGovVotesOf tx))) ∪ mapPartial (λ p → if PolicyOf p then (λ {sh} → just (Propose p , ScriptObj sh)) else nothing) (fromList (ListOfGovProposalsOf tx)) ∪ mapˢ (λ (c , d) → (Guard c , c)) (GuardsOf tx) where collateralInputs : Tx ℓ → ℙ TxIn collateralInputs {TxLevelTop} tx = CollateralInputsOf tx collateralInputs {TxLevelSub} tx = ∅
The function collectP2ScriptsWithContext.{AgdaFunction} builds a list of
phase-2 scripts paired with their contexts for phase-2 validation. The scripts
that are needed for validation are retrieved from the transaction using the
function credsNeeded.
In Dijkstra, the execution of a guard script can require several (including
none) data. The function assembleData accounts for this situation by returning
a list of lists of data (a list of data is part of the context of a script).
collectP2ScriptsWithContext : PParams → Tx ℓ → UTxO → (DataHash ⇀ Datum) → ℙ Script → List (P2Script × List Data × ExUnits × CostModel) collectP2ScriptsWithContext pp tx utxo allData allScripts = concat (setToList (mapˢ toScript (credsNeeded utxo tx))) where context : ScriptPurpose → Data context sp = valContext (txInfoForPurpose utxo tx sp) sp getScript : Credential → ScriptPurpose → Maybe (P2Script × Redeemer × ExUnits × CostModel) getScript c sp = do script ← isScriptObj c >>= λ sh → lookupHash sh allScripts >>= toP2Script (reedemer , exUnits) ← indexedRdmrs tx sp costModel ← lookupᵐ? (PParams.costmdls pp) (language script) return (script , reedemer , exUnits , costModel) assembleData : Redeemer → ScriptPurpose → List (List Data) assembleData redeemer sp@(Spend txin) = [ fromMaybe (getDatumSpend tx utxo allData txin) ++ (redeemer ∷ [ context sp ]) ] assembleData redeemer sp@(Guard c) = let data′ , withoutDatum = getDataGuard tx utxo c in map (λ d → [ d ] ++ (redeemer ∷ [ context sp ])) (setToList data′) ++ (if withoutDatum then [(redeemer ∷ [ context sp ])] else []) assembleData redeemer sp = [ redeemer ∷ [ context sp ] ] toScript : ScriptPurpose × Credential → List (P2Script × List Data × ExUnits × CostModel) toScript (sp , c) = do (script , reedemer , exUnits , costModel) ← fromMaybe (getScript c sp) data′ ← assembleData reedemer sp [ (script , data′ , exUnits , costModel) ] evalP2Scripts : List (P2Script × List Data × ExUnits × CostModel) → Bool evalP2Scripts = all (λ (s , d , eu , cm) → runPLCScript cm s eu d)
→