diff --git a/src/Ledger/Dijkstra/Specification/Abstract.lagda.md b/src/Ledger/Dijkstra/Specification/Abstract.lagda.md index 905e31791e..877f84b34c 100644 --- a/src/Ledger/Dijkstra/Specification/Abstract.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Abstract.lagda.md @@ -8,6 +8,7 @@ module Ledger.Dijkstra.Specification.Abstract (txs : TransactionStructure) where open import Ledger.Prelude open TransactionStructure txs open import Ledger.Dijkstra.Specification.Certs govStructure +open import Ledger.Dijkstra.Specification.Script.ScriptPurpose txs record indexOf : Type where @@ -26,4 +27,5 @@ record AbstractFunctions : Type where indexOfImp : indexOf runPLCScript : CostModel → P2Script → ExUnits → List Data → Bool scriptSize : Script → ℕ + valContext : TxInfo → ScriptPurpose → Data ``` diff --git a/src/Ledger/Dijkstra/Specification/Script/ScriptPurpose.lagda.md b/src/Ledger/Dijkstra/Specification/Script/ScriptPurpose.lagda.md new file mode 100644 index 0000000000..931d491b43 --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Script/ScriptPurpose.lagda.md @@ -0,0 +1,59 @@ +--- +source_branch: master +source_path: src/Ledger/Dijkstra/Specification/Script/ScriptPurpose.lagda.md +--- + +# Script Purpose {#sec:script-purpose} + + + +```agda +data ScriptPurpose : Type where + Cert : DCert → ScriptPurpose + Rwrd : RewardAddress → ScriptPurpose + Mint : ScriptHash → ScriptPurpose + Spend : TxIn → ScriptPurpose + Vote : GovVoter → ScriptPurpose + Propose : GovProposal → ScriptPurpose + Guard : Credential → ScriptPurpose +``` + +Note that `Guard c` always indexes into *the current `tx`'s* `txGuards`: + ++ if `tx : TopLevelTx`, it indexes into the top-level guard set's list-view; ++ if `tx : SubLevelTx`, it indexes into the subTx's guard set's list-view. + +```agda +mutual + record TxInfo : Type where + inductive + field + realizedInputs : UTxO + txOuts : Ix ⇀ TxOut + txFee : Maybe Fees + mint : Value + txCerts : List DCert + txWithdrawals : Withdrawals + txVldt : Maybe Slot × Maybe Slot + vkKey : ℙ KeyHash -- native/phase-1/timelock signers + txGuards : ℙ Credential -- CIP-0112/0118 guards (required by tx body) + txData : ℙ Datum + txId : TxId + txInfoSubTxs : Maybe (List SubTxInfo) + + SubTxInfo : Type + SubTxInfo = TxInfo + +``` diff --git a/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md b/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md index 71538ecac4..fd0fa614fc 100644 --- a/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Script/Validation.lagda.md @@ -17,24 +17,11 @@ module Ledger.Dijkstra.Specification.Script.Validation open import Ledger.Prelude open import Ledger.Dijkstra.Specification.Certs govStructure -``` ---> -```agda -data ScriptPurpose : Type where - Cert : DCert → ScriptPurpose - Rwrd : RewardAddress → ScriptPurpose - Mint : ScriptHash → ScriptPurpose - Spend : TxIn → ScriptPurpose - Vote : GovVoter → ScriptPurpose - Propose : GovProposal → ScriptPurpose - Guard : Credential → ScriptPurpose +open import Ledger.Dijkstra.Specification.Abstract txs +open import Ledger.Dijkstra.Specification.Script.ScriptPurpose txs ``` - -Note that `Guard c` always indexes into *the current `tx`'s* `txGuards`: - -+ if `tx : TopLevelTx`, it indexes into the top-level guard set's list-view; -+ if `tx : SubLevelTx`, it indexes into the subTx's guard set's list-view. +--> ```agda -mutual - record TxInfo : Type where - inductive - field - realizedInputs : UTxO - txOuts : Ix ⇀ TxOut - txFee : Maybe Fees - mint : Value - txCerts : List DCert - txWithdrawals : Withdrawals - txVldt : Maybe Slot × Maybe Slot - vkKey : ℙ KeyHash -- native/phase-1/timelock signers - txGuards : ℙ Credential -- CIP-0112/0118 guards (required by tx body) - txData : ℙ Datum - txId : TxId - txInfoSubTxs : Maybe (List SubTxInfo) - - SubTxInfo : Type - SubTxInfo = TxInfo - - txInfo : (ℓ : TxLevel) → UTxO → Tx ℓ → TxInfo txInfo TxLevelTop utxo tx = @@ -145,15 +111,13 @@ txInfoForPurpose TxLevelTop utxo tx sp with sp @@ -426,47 +511,46 @@ This section collects some unimportant but useful helper and accessor functions. ``` In the Dijkstra era, *spending* inputs must exist in the initial UTxO snapshot, while -*reference* inputs may see earlier outputs, so we need two UTxO views: +*reference* inputs may come from earlier outputs, so we will need two to keep track +of two UTxOs; we'll denote these as follows: -+ `utxoSpend₀`{.AgdaBound}, the initial snapshot, used for `txIns`{.AgdaField}, -+ `utxoRefView`{.AgdaBound}, the evolving view, used for `refInputs`{.AgdaField}. ++ `utxo₀`{.AgdaBound}, the initial UTxO snapshot, used for `txIns`{.AgdaField}; ++ `utxoRef`{.AgdaBound}, the evolving UTxO, used for reference input lookups. -Thus functions like `refScripts`{.AgdaFunction}, `txscripts`{.AgdaFunction}, -and `lookupScriptHash`{.AgdaFunction} (defined below) will take *two* UTxO arguments. +We now define some functions for scripts. Some of these will take two UTxO +arguments, denoting the initial UTxO snapshot and an evolving UTxO, which evolves as +a batch of subtransactions is processed. (Later, when the functions below are used, +the two UTxO arguments may come from the UTxO environment and an evolving UTxO state; +types for these are defined in the `Utxo`{.AgdaModule} module, which depends +on the present module; thus, we cannot bind the UTxO arguments to a particular +UTxO environment and state at this point.) ```agda refScripts : Tx txLevel → UTxO → UTxO → List Script - refScripts tx utxoSpend₀ utxoRefView = - mapMaybe (proj₂ ∘ proj₂ ∘ proj₂) ( setToList (range (utxoSpend₀ ∣ txIns)) - ++ setToList (range (utxoRefView ∣ refInputs)) - ) - where open Tx tx; open TxBody (TxBodyOf tx) + refScripts tx utxo₀ utxoRef = + mapMaybe (proj₂ ∘ proj₂ ∘ proj₂) + ( setToList (range (utxo₀ ∣ SpendInputsOf tx)) + ++ setToList (range (utxoRef ∣ ReferenceInputsOf tx)) ) txscripts : Tx txLevel → UTxO → UTxO → ℙ Script - txscripts tx utxoSpend₀ utxoRefView = - scripts (tx .txWitnesses) ∪ fromList (refScripts tx utxoSpend₀ utxoRefView) - where open Tx; open TxWitnesses + txscripts tx utxo₀ utxoRef = ScriptsOf tx ∪ fromList (refScripts tx utxo₀ utxoRef) lookupScriptHash : ScriptHash → Tx txLevel → UTxO → UTxO → Maybe Script - lookupScriptHash sh tx utxoSpend₀ utxoRefView = + lookupScriptHash sh tx utxo₀ utxoRef = if sh ∈ mapˢ proj₁ (m ˢ) then just (lookupᵐ m sh) else nothing - where m = setToMap (mapˢ < hash , id > (txscripts tx utxoSpend₀ utxoRefView)) - - -- TODO: implement the actual evolving `utxoRefView` (issue #1006) + where m = setToMap (mapˢ < hash , id > (txscripts tx utxo₀ utxoRef)) getSubTxScripts : SubLevelTx → ℙ (TxId × ScriptHash) getSubTxScripts subtx = mapˢ (λ hash → (TxIdOf subtx , hash)) (ScriptHashes subtx) where ScriptHashes : Tx TxLevelSub → ℙ ScriptHash - ScriptHashes tx = -- `txRequiredTopLevelGuards` - mapPartial (isScriptObj ∘ proj₁) -- has key creds too, but only - (TxBody.txRequiredTopLevelGuards (TxBodyOf tx)) -- `ScriptObj hash` contributes - -- a phase-2 script hash. + ScriptHashes tx = mapPartial (isScriptObj ∘ proj₁) (TopLevelGuardsOf tx) + -- `txRequiredTopLevelGuards` has key creds too, but only + -- `ScriptObj hash` contributes a phase-2 script hash. getTxScripts : {ℓ : TxLevel} → Tx ℓ → ℙ (TxId × ScriptHash) getTxScripts {TxLevelSub} = getSubTxScripts - getTxScripts {TxLevelTop} = - concatMapˢ getSubTxScripts ∘ fromList ∘ TxBody.txSubTransactions ∘ TxBodyOf + getTxScripts {TxLevelTop} = concatMapˢ getSubTxScripts ∘ fromList ∘ SubTransactionsOf ``` CIP-0118 models "required top-level guards" as a list of requirements coming @@ -524,17 +608,16 @@ remaining helper functions of this section. subTxTaggedGuards : SubLevelTx → ℙ TaggedTopLevelGuard subTxTaggedGuards subtx = - mapˢ (λ (cred , md) → (TxIdOf subtx , cred , md)) - (TxBody.txRequiredTopLevelGuards (TxBodyOf subtx)) + mapˢ (λ (cred , md) → (TxIdOf subtx , cred , md)) (TopLevelGuardsOf subtx) -- Turn a subTx body's `txRequiredTopLevelGuards` into a set of guard credentials. subTxGuardCredentials : SubLevelTx → ℙ Credential - subTxGuardCredentials = (mapˢ proj₁) ∘ (TxBody.txRequiredTopLevelGuards ∘ TxBodyOf) + subTxGuardCredentials = (mapˢ proj₁) ∘ TopLevelGuardsOf -- Phase-1 condition (CIP-0118): -- every credential required by a subTx body must appear in the top-level txGuards set. requiredTopLevelGuardsSatisfied : TopLevelTx → List SubLevelTx → Type - requiredTopLevelGuardsSatisfied topTx subTxs = requiredCreds ⊆ TxBody.txGuards (TxBodyOf topTx) + requiredTopLevelGuardsSatisfied topTx subTxs = requiredCreds ⊆ GuardsOf topTx where concatMapˡ : {A B : Type} → (A → ℙ B) → List A → ℙ B concatMapˡ f as = proj₁ $ unions (fromList (map f as)) diff --git a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md index d9a9345793..e575e299fb 100644 --- a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md @@ -33,7 +33,6 @@ open import Ledger.Dijkstra.Specification.Script.Validation txs abs ## Environments and states -(copied shape from Conway; semantics TBD) ```agda record UTxOEnv : Type where @@ -42,7 +41,12 @@ record UTxOEnv : Type where pparams : PParams treasury : Treasury utxo₀ : UTxO +``` + +The `utxo₀`{.AgdaField} field of `UTxOEnv`{.AgdaRecord} is introduced in the Dijkstra +era; it denotes a *snapshot* of the UTxO before any subtransactions of a batch are applied. +```agda record UTxOState : Type where field utxo : UTxO