UTxOW¶
Witnessing Functions¶
UsesBootstrapAddress : UTxO → Tx ℓ → Type UsesBootstrapAddress utxo tx = ∃[ o ∈ (range txOuts) ∪ range (utxo ∣ (txIns ∪ referenceInputs)) ] IsBootstrapAddr (proj₁ o) where open Tx tx; open TxBody txBody HasInlineDatum : TxOut → Type HasInlineDatum txout = Is-just (txOutToDatum txout) HasDataHash : TxOut → Type HasDataHash txout = Is-just (txOutToDataHash txout) module _ (tx : TopLevelTx) where module _ (utxo : UTxO) where UsesV2Features : Type UsesV2Features = ∃[ o ∈ (range (TxOutsOf tx)) ∪ range (utxo ∣ (SpendInputsOf tx ∪ ReferenceInputsOf tx)) ] HasInlineDatum o data UsesV3Features : Set where hasVotes : ¬ (Is-[] (ListOfGovVotesOf tx)) → UsesV3Features hasProposals : ¬ (Is-[] (ListOfGovProposalsOf tx)) → UsesV3Features hasDonation : NonZero (DonationsOf tx) → UsesV3Features hasTreasure : Is-just (CurrentTreasuryOf tx) → UsesV3Features hasConwayCerts : L.Any IsConwayCert (DCertsOf tx) → UsesV3Features data UsesV4Features : Set where hasScriptGuards : ¬ (∀[ g ∈ GuardsOf tx ] IsKeyHashObj g) → UsesV4Features hasDirectDeposits : ¬ Is-∅ (dom (DirectDepositsOf tx)) → UsesV4Features hasBalanceIntervals : ¬ Is-∅ (dom (BalanceIntervalsOf tx)) → UsesV4Features
The set of languages allowed in phase-2 scripts within a transaction depends on (1) the operation mode (see below), and (2) the features of a transaction and their compatibility with Plutus versions.
languages : ℙ P2Script → ℙ Language languages p2Scripts = mapˢ language p2Scripts allowedLanguagesLegacy : TopLevelTx → UTxO → ℙ Language allowedLanguagesLegacy tx utxo = ( if ¬ usesBootstrapAddr × SpendInputsOf tx ∩ ReferenceInputsOf tx ≡ ∅ then ❴ PlutusV4 ❵ else ∅ ) ∪ ( if ¬ usesBootstrapAddr × ¬ usesV4Features × SpendInputsOf tx ∩ ReferenceInputsOf tx ≡ ∅ then ❴ PlutusV3 ❵ else ∅ ) ∪ ( if ¬ usesBootstrapAddr × ¬ usesV4Features × ¬ usesV3Features then ❴ PlutusV2 ❵ else ∅ ) ∪ ( if ¬ usesBootstrapAddr × ¬ usesV4Features × ¬ usesV3Features × ¬ usesV2Features then ❴ PlutusV1 ❵ else ∅ ) where os = range (TxOutsOf tx) ∪ range (utxo ∣ (SpendInputsOf tx ∪ ReferenceInputsOf tx)) usesBootstrapAddr = ∃[ (a , _) ∈ os ] IsBootstrapAddr a usesV4Features = UsesV4Features tx usesV3Features = UsesV3Features tx usesV2Features = UsesV2Features tx utxo allowedLanguages : Tx ℓ → UTxO → ℙ Language allowedLanguages tx utxo = if ¬ UsesBootstrapAddress utxo tx × SpendInputsOf tx ∩ ReferenceInputsOf tx ≡ ∅ then ❴ PlutusV4 ❵ else ∅
TxOutSpendable-PlutusV1-V2 : ℙ Script → TxOut → Type TxOutSpendable-PlutusV1-V2 scripts txOut = Maybe.All (λ s → language s ≡ PlutusV1 → HasDataHash txOut) (txOutToP2Script scripts txOut) × Maybe.All (λ s → language s ≡ PlutusV2 → HasDataHash txOut ⊎ HasInlineDatum txOut) (txOutToP2Script scripts txOut)
Deciding the Operation Mode¶
The phase-2 scripts a transaction needs are the scripts in the (batch-wide) script pool whose hashes appear among the credentials the transaction needs.
neededP2Scripts : UTxO → ℙ Script → Tx ℓ → ℙ P2Script neededP2Scripts utxo scriptPool tx = mapPartial toP2Script scriptsNeeded where scriptHashesNeeded : ℙ ScriptHash scriptHashesNeeded = mapPartial isScriptObj (mapˢ proj₂ (credsNeeded utxo tx)) scriptsNeeded : ℙ Script scriptsNeeded = filterˢ (λ s → hash s ∈ scriptHashesNeeded) scriptPool
A top-level transaction is processed in legacy mode exactly when some
phase-2 script it needs uses a Plutus language older than V4. This decision
is made once, in the LEDGER rule, and the result is threaded
through the rules via the legacyMode field of
UTxOEnv and of EntitiesEnv.
isLegacyMode : UTxO → ℙ Script → TopLevelTx → Bool isLegacyMode utxo scriptPool txTop = ¿ ∃[ s ∈ neededP2Scripts utxo scriptPool txTop ] language s ∈ fromList (PlutusV1 ∷ PlutusV2 ∷ PlutusV3 ∷ []) ¿ᵇ
Checking the script integrity hash¶
The script integrity hash helps determining that the cost model for execution of a script hasn't changed since the transaction was submitted. Otherwise, evaluation of the script could yield a different value than expected. It also helps checking that the same datums and redeemers are provided every time a transaction is validated. See Section 2.2, Propery C.8 and the proof of Lemma C.10 in VK21, for the details.
hashScriptIntegrity : PParams → ℙ Language → RedeemerPtr ⇀ (Redeemer × ExUnits) → ℙ Datum → Maybe ScriptHash hashScriptIntegrity pp langs rdrms dats with rdrms ˢ ≟ ∅ˢ | langs ≟ ∅ˢ | dats ≟ ∅ˢ ... | yes _ | yes _ | yes _ = nothing ... | _ | _ | _ = just $ hash (dats , rdrms , mapˢ (getLanguageView pp) langs)
Required Top-level Guards¶
A required top-level guard is well-formed when either a datum is specified and
the credential resolves to a phase-2 script, or no datum is specified and the
credential is a KeyHash or resolves to a phase-1 script.
TopLevelGuardWellFormed : ℙ Script → Credential × Maybe Datum → Type TopLevelGuardWellFormed scripts (c , just d) = Is-just (credentialToP2Script c scripts) TopLevelGuardWellFormed scripts (c , nothing) = Is-just (isKeyHashObj c) ⊎ Is-just (credentialToP1Script c scripts)
The SUBUTXOW Transition System¶
-
All needed phase-2 scripts use Plutus language V4.
-
Required top-level guards are well-formed.
data _⊢_⇀⦇_,SUBUTXOW⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where SUBUTXOW : let open Tx txSub open TxBody txBody open TxWitnesses txWitnesses utxo₀ = UTxOOf Γ vKeyHashesProvided : ℙ KeyHash vKeyHashesProvided = mapˢ hash (dom vKeySigs) scriptsProvided : ℙ Script scriptsProvided = ScriptPoolOf Γ dataHashesProvided : ℙ DataHash dataHashesProvided = mapˢ hash (DataOf txSub) credentialsNeeded : ℙ Credential credentialsNeeded = mapˢ proj₂ (credsNeeded utxo₀ txSub) vKeyHashesNeeded : ℙ KeyHash vKeyHashesNeeded = mapPartial isKeyHashObj credentialsNeeded scriptHashesNeeded : ℙ ScriptHash scriptHashesNeeded = mapPartial isScriptObj credentialsNeeded scriptsNeeded : ℙ Script scriptsNeeded = filterˢ (λ s → hash s ∈ scriptHashesNeeded) scriptsProvided p1ScriptsNeeded : ℙ P1Script p1ScriptsNeeded = mapPartial toP1Script scriptsNeeded p2ScriptsNeeded : ℙ P2Script p2ScriptsNeeded = mapPartial toP2Script scriptsNeeded dataHashesNeededSpendInputs : ℙ DataHash dataHashesNeededSpendInputs = mapPartial (λ txOut@(a , _ , d , _) → do sh ← isScriptObj (payCred a) _ ← lookupHash sh p2ScriptsNeeded d >>= isInj₂) (range (utxo₀ ∣ txIns)) dataHashesOutputs : ℙ DataHash dataHashesOutputs = mapPartial txOutToDataHash (range txOuts) dataHashesReferenceInputs : ℙ DataHash dataHashesReferenceInputs = mapPartial txOutToDataHash (range (UTxOOf Γ ∣ referenceInputs)) scriptRedeemerPtrs : ℙ RedeemerPtr scriptRedeemerPtrs = mapPartial (λ (sp , c) → if credentialToP2Script c scriptsNeeded then rdptr txSub sp else nothing) (credsNeeded utxo₀ txSub) in ∙ ∀[ s ∈ p2ScriptsNeeded ] language s ∈ fromList (PlutusV4 ∷ []) -- (1) ∙ ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes txId) σ ∙ ∀[ s ∈ p1ScriptsNeeded ] validP1Script vKeyHashesProvided (GuardsOf txSub) txVldt s ∙ ∀[ tlg ∈ TopLevelGuardsOf txSub ] TopLevelGuardWellFormed scriptsProvided tlg -- (2) ∙ vKeyHashesNeeded ⊆ vKeyHashesProvided ∙ scriptHashesNeeded ⊆ mapˢ hash scriptsProvided ∙ dataHashesNeededSpendInputs ⊆ dataHashesProvided ∙ dataHashesProvided ⊆ dataHashesNeededSpendInputs ∪ dataHashesOutputs ∪ dataHashesReferenceInputs ∙ dom txRedeemers ≡ᵉ scriptRedeemerPtrs ∙ languages p2ScriptsNeeded ⊆ dom (PParams.costmdls (PParamsOf Γ)) ∩ allowedLanguages txSub utxo₀ ∙ txADhash ≡ map hash txAuxData ∙ scriptIntegrityHash ≡ hashScriptIntegrity (PParamsOf Γ) (languages p2ScriptsNeeded) txRedeemers txData ∙ Γ ⊢ s₀ ⇀⦇ txSub ,SUBUTXO⦈ s₁ ──────────────────────────────── Γ ⊢ s₀ ⇀⦇ txSub ,SUBUTXOW⦈ s₁
The UTXOW Transition System¶
data _⊢_⇀⦇_,UTXOW⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where
In Dijkstra, the UTXOW transition system for the top-level transaction has two
different operating modes, normal mode and legacy mode. These correspond to
the rules UTXOW-normal and
UTXOW-legacy.
The mode itself is not decided here: it is decided once, in the
LEDGER rule, by isLegacyMode (see
above), and communicated through the
legacyMode field of the environment. Each rule selects on that
field, so a computation can pick the applicable mode up front rather than
attempting both.
Normal Mode¶
-
All needed phase-2 scripts use Plutus language V4.
-
The required top-level guards of the top-level transaction and of its subtransactions must appear in the top-level guard set.
-
Required top-level guards are well-formed.
UTXOW-normal : let open Tx txTop open TxBody txBody open TxWitnesses txWitnesses utxo₀ = UTxOOf Γ scriptsProvided : ℙ Script scriptsProvided = ScriptPoolOf Γ dataHashesProvided : ℙ DataHash dataHashesProvided = mapˢ hash (DataOf txTop) credentialsNeeded : ℙ Credential credentialsNeeded = mapˢ proj₂ (credsNeeded utxo₀ txTop) vKeyHashesProvided : ℙ KeyHash vKeyHashesProvided = mapˢ hash (dom vKeySigs) vKeyHashesNeeded : ℙ KeyHash vKeyHashesNeeded = mapPartial isKeyHashObj credentialsNeeded scriptHashesNeeded : ℙ ScriptHash scriptHashesNeeded = mapPartial isScriptObj credentialsNeeded scriptsNeeded : ℙ Script scriptsNeeded = filterˢ (λ s → hash s ∈ scriptHashesNeeded) scriptsProvided p1ScriptsNeeded : ℙ P1Script p1ScriptsNeeded = mapPartial toP1Script scriptsNeeded p2ScriptsNeeded : ℙ P2Script p2ScriptsNeeded = mapPartial toP2Script scriptsNeeded dataHashesNeededSpendInputs : ℙ DataHash dataHashesNeededSpendInputs = mapPartial (λ txOut@(a , _ , d , _) → do sh ← isScriptObj (payCred a) _ ← lookupHash sh p2ScriptsNeeded x ← d isInj₂ x) (range (utxo₀ ∣ txIns)) dataHashesOutputs : ℙ DataHash dataHashesOutputs = mapPartial txOutToDataHash (range txOuts) dataHashesReferenceInputs : ℙ DataHash dataHashesReferenceInputs = mapPartial txOutToDataHash (range (utxo₀ ∣ referenceInputs)) allReferenceScriptHashes : ℙ ScriptHash allReferenceScriptHashes = mapˢ hash (allReferenceScripts txTop utxo₀) allScriptHashesNeeded : ℙ ScriptHash allScriptHashesNeeded = mapPartial (isScriptObj ∘ proj₂) (allCredsNeeded utxo₀ txTop) allWitnessScriptHashes : ℙ ScriptHash allWitnessScriptHashes = mapˢ hash (allWitnessScripts txTop) scriptRedeemerPtrs : ℙ RedeemerPtr scriptRedeemerPtrs = mapPartial (λ (sp , c) → if credentialToP2Script c scriptsNeeded then rdptr txTop sp else nothing) (credsNeeded utxo₀ txTop) in ∙ LegacyModeOf Γ ≡ false ∙ isLegacyMode utxo₀ scriptsProvided txTop ≡ false -- (1) ∙ concatMapˡ (λ txSub → mapˢ proj₁ (TopLevelGuardsOf txSub)) (SubTransactionsOf txTop) ∪ mapˢ proj₁ (TopLevelGuardsOf txTop) ⊆ GuardsOf txTop -- (2) ∙ ∀[ tlg ∈ TopLevelGuardsOf txTop ] TopLevelGuardWellFormed scriptsProvided tlg -- (3) ∙ ∀[ (vk , σ) ∈ TxWitnesses.vKeySigs (Tx.txWitnesses txTop) ] isSigned vk (txidBytes (TxIdOf txTop)) σ ∙ ∀[ s ∈ p1ScriptsNeeded ] validP1Script vKeyHashesProvided (GuardsOf txTop) txVldt s ∙ vKeyHashesNeeded ⊆ vKeyHashesProvided ∙ allScriptHashesNeeded - allReferenceScriptHashes ≡ᵉ allWitnessScriptHashes ∙ scriptHashesNeeded ⊆ mapˢ hash scriptsProvided ∙ dataHashesNeededSpendInputs ⊆ dataHashesProvided ∙ dataHashesProvided ⊆ dataHashesNeededSpendInputs ∪ dataHashesOutputs ∪ dataHashesReferenceInputs ∙ dom txRedeemers ≡ᵉ scriptRedeemerPtrs ∙ languages p2ScriptsNeeded ⊆ dom (PParams.costmdls (PParamsOf Γ)) ∩ allowedLanguages txTop utxo₀ ∙ txADhash ≡ map hash txAuxData ∙ scriptIntegrityHash ≡ hashScriptIntegrity (PParamsOf Γ) (languages p2ScriptsNeeded) txRedeemers txData ∙ Γ ⊢ s ⇀⦇ txTop ,UTXO⦈ s' ──────────────────────────────── Γ ⊢ s ⇀⦇ txTop ,UTXOW⦈ s'
Legacy mode¶
-
There is at least a needed phase-2 script with Plutus language version V1, V2 or V3. Note that Plutus V4 scripts are allowed in legacy mode.
-
The set of required top-level guards of the top-level transaction and the subtransactions appear in the set of guards at the top-level.
-
Required top-level guards are well-formed.
UTXOW-legacy : let open Tx txTop open TxBody txBody open TxWitnesses txWitnesses utxo₀ = UTxOOf Γ scriptsProvided : ℙ Script scriptsProvided = ScriptPoolOf Γ dataHashesProvided : ℙ DataHash dataHashesProvided = mapˢ hash (DataOf txTop) credentialsNeeded : ℙ Credential credentialsNeeded = mapˢ proj₂ (credsNeeded utxo₀ txTop) vKeyHashesProvided : ℙ KeyHash vKeyHashesProvided = mapˢ hash (dom vKeySigs) vKeyHashesNeeded : ℙ KeyHash vKeyHashesNeeded = mapPartial isKeyHashObj credentialsNeeded scriptHashesNeeded : ℙ ScriptHash scriptHashesNeeded = mapPartial isScriptObj credentialsNeeded scriptsNeeded : ℙ Script scriptsNeeded = filterˢ (λ s → hash s ∈ scriptHashesNeeded) scriptsProvided p1ScriptsNeeded : ℙ P1Script p1ScriptsNeeded = mapPartial toP1Script scriptsNeeded p2ScriptsNeeded : ℙ P2Script p2ScriptsNeeded = mapPartial toP2Script scriptsNeeded dataHashesNeededSpendInputs : ℙ DataHash dataHashesNeededSpendInputs = mapPartial (λ txOut@(a , _ , d , _) → do sh ← isScriptObj (payCred a) _ ← lookupHash sh p2ScriptsNeeded x ← d isInj₂ x) (range (utxo₀ ∣ txIns)) dataHashesOutputs : ℙ DataHash dataHashesOutputs = mapPartial txOutToDataHash (range txOuts) dataHashesReferenceInputs : ℙ DataHash dataHashesReferenceInputs = mapPartial txOutToDataHash (range (utxo₀ ∣ referenceInputs)) allReferenceScriptHashes : ℙ ScriptHash allReferenceScriptHashes = mapˢ hash (allReferenceScripts txTop utxo₀) allScriptHashesNeeded : ℙ ScriptHash allScriptHashesNeeded = mapPartial (isScriptObj ∘ proj₂) (allCredsNeeded utxo₀ txTop) allWitnessScriptHashes : ℙ ScriptHash allWitnessScriptHashes = mapˢ hash (allWitnessScripts txTop) scriptRedeemerPtrs : ℙ RedeemerPtr scriptRedeemerPtrs = mapPartial (λ (sp , c) → if credentialToP2Script c scriptsNeeded then rdptr txTop sp else nothing) (credsNeeded utxo₀ txTop) in ∙ LegacyModeOf Γ ≡ true ∙ isLegacyMode utxo₀ scriptsProvided txTop ≡ true -- (1) ∙ concatMapˡ (λ txSub → mapˢ proj₁ (TopLevelGuardsOf txSub)) (SubTransactionsOf txTop) ∪ mapˢ proj₁ (TopLevelGuardsOf txTop) ⊆ GuardsOf txTop -- (2) ∙ ∀[ tlg ∈ TopLevelGuardsOf txTop ] TopLevelGuardWellFormed scriptsProvided tlg -- (3) ∙ ∀[ (vk , σ) ∈ vKeySigs ] isSigned vk (txidBytes (TxIdOf txTop)) σ ∙ ∀[ s ∈ p1ScriptsNeeded ] validP1Script vKeyHashesProvided (GuardsOf txTop) txVldt s ∙ vKeyHashesNeeded ⊆ vKeyHashesProvided ∙ allScriptHashesNeeded - allReferenceScriptHashes ≡ᵉ allWitnessScriptHashes ∙ scriptHashesNeeded ⊆ mapˢ hash scriptsProvided ∙ dataHashesNeededSpendInputs ⊆ dataHashesProvided ∙ dataHashesProvided ⊆ dataHashesNeededSpendInputs ∪ dataHashesOutputs ∪ dataHashesReferenceInputs ∙ dom txRedeemers ≡ᵉ scriptRedeemerPtrs ∙ languages p2ScriptsNeeded ⊆ dom (PParams.costmdls (PParamsOf Γ)) ∩ allowedLanguagesLegacy txTop utxo₀ ∙ ∀[ txOut ∈ range (utxo₀ ∣ SpendInputsOf txTop) ] TxOutSpendable-PlutusV1-V2 scriptsProvided txOut ∙ txADhash ≡ map hash txAuxData ∙ scriptIntegrityHash ≡ hashScriptIntegrity (PParamsOf Γ) (languages p2ScriptsNeeded) txRedeemers txData ∙ Γ ⊢ s ⇀⦇ txTop ,UTXO⦈ s' ──────────────────────────────── Γ ⊢ s ⇀⦇ txTop ,UTXOW⦈ s'