The UTxO Transition System¶
This is a work-in-progress of the Dijkstra-era UTxO transition system. Historically, this module captured the phase-1 structural checks specific to Dijkstra (nested transactions + guards). It now also contains a first pass at the batch semantics and the phase-2 (Plutus) execution model for validating a top-level transaction together with all of its subtransactions.
The primary guiding design principles are
- Spend-side safety. All spending inputs across the whole batch must come from a pre-batch UTxO snapshot (see point 6 of the Changes to Transaction Validity section of CIP-0118);
- Batch-scoped witnesses. Scripts and datums are collected once per batch and then shared for phase-2 evaluation; CIP-0118 explicitly states that reference scripts, and by implication reference-input-resolved UTxO entries, could be outputs of preceding transactions in the batch (see point 5 of the Changes to Transaction Validity section of CIP-0118);
- Batch-consistency. No two transactions in the batch may spend the
same input. This is enforced explicitly at the top level by a predicate
(called
NoOverlappingSpendInputsbelow) that is checked in theUTXOrule.
Functions and Types of the UTxO Transition System¶
The UTxO rules are parameterised by an environment UTxOEnv and an
evolving state UTxOState.
record UTxOEnv : Type where field slot : Slot pparams : PParams treasury : Treasury utxo₀ : UTxO certState : CertState allScripts : ℙ Script accountBalances : Rewards record SubUTxOEnv : Type where field slot : Slot pparams : PParams treasury : Treasury utxo₀ : UTxO isTopLevelValid : Bool allScripts : ℙ Script accountBalances : Rewards
The UTxOEnv carries
utxo₀: pre-batch snapshot of the UTxO;allScripts: batch-wide script pool containing all scripts available to the batch (witness scripts plus reference scripts resolved from allowed reference inputs and batch outputs);
The pre-batch UTxO snapshot utxo₀ is used to resolve all
spend-side lookups (inputs, collateral, and datum lookup for spent outputs).
The allScripts field of UTxOEnv capture
the batch-wide script pool. This pool is used to resolve all
script lookups during validation.
Scripts are treated as batch-wide witnesses; attaching a script to a transaction in the batch makes it available for phase-2 validation of any transaction in the batch, independent of which subtransaction originally supplied it.
If Γ denotes a particular UTxOEnv, then
we often access the allScripts field of Γ
via ScriptPoolOf Γ.
record UTxOState : Type where constructor ⟦_,_,_⟧ᵘ field utxo : UTxO fees : Fees donations : Donations
outs : Tx ℓ → UTxO outs tx = mapKeys (TxIdOf tx ,_) (TxOutsOf tx) balance : UTxO → Value balance utxo = ∑ˢ[ v ← valuesOfUTxO utxo ] v cbalance : UTxO → Coin cbalance utxo = coin (balance utxo) refScriptsSize : Tx ℓ → UTxO → ℕ refScriptsSize tx utxo = ∑ˡ[ x ← setToList (referenceScripts tx utxo) ] scriptSize x minfee : PParams → TopLevelTx → UTxO → Coin minfee pp txTop utxo = pp .a * (SizeOf txTop) + pp .b + txScriptFee (pp .prices) (totExUnits txTop) + scriptsCost pp (refScriptsSize txTop utxo)
data inInterval (slot : Slot) : (Maybe Slot × Maybe Slot) → Type where both : ∀ {l r} → l ≤ slot × slot ≤ r → inInterval slot (just l , just r) lower : ∀ {l} → l ≤ slot → inInterval slot (just l , nothing) upper : ∀ {r} → slot ≤ r → inInterval slot (nothing , just r) none : inInterval slot (nothing , nothing)
Collateral Check¶
collateralCheck : PParams → TopLevelTx → UTxO → Type collateralCheck pp txTop utxo = All (λ (addr , _) → isVKeyAddr addr) (range (utxo ∣ CollateralInputsOf txTop)) × isAdaOnly (balance (utxo ∣ CollateralInputsOf txTop)) × coin (balance (utxo ∣ CollateralInputsOf txTop)) * 100 ≥ (TxFeesOf txTop) * pp .collateralPercentage × (CollateralInputsOf txTop) ≢ ∅
Change in Deposits¶
module _ (pp : PParams) (certState : CertState) where updateCertDeposit : DCert → (Credential ⇀ Coin) × (KeyHash ⇀ Coin) × (Credential ⇀ Coin) → (Credential ⇀ Coin) × (KeyHash ⇀ Coin) × (Credential ⇀ Coin) updateCertDeposit cert (depositsᵈ , depositsᵖ , depositsᵍ) = case cert of λ where (delegate c _ _ d) → (depositsᵈ ∪⁺ ❴ c , d ❵ , depositsᵖ , depositsᵍ) (dereg c _ ) → (depositsᵈ ∣ ❴ c ❵ ᶜ , depositsᵖ , depositsᵍ) (regpool kh _ ) → (depositsᵈ , depositsᵖ ∪ˡ ❴ kh , pp .poolDeposit ❵ , depositsᵍ) (regdrep c d _ ) → (depositsᵈ , depositsᵖ , depositsᵍ ∪⁺ ❴ c , d ❵) (deregdrep c _ ) → (depositsᵈ , depositsᵖ , depositsᵍ ∣ ❴ c ❵ ᶜ) _ → (depositsᵈ , depositsᵖ , depositsᵍ) updateCertDeposits : List DCert → CertState updateCertDeposits = foldr (λ c certState → let open CertState certState (depositsᵈ , depositsᵖ , depositsᵍ) = updateCertDeposit c ( DepositsOf dState , DepositsOf pState , DepositsOf gState) in $\begin{pmatrix} \,\htmlId{11014}{\htmlClass{Keyword}{\text{record}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#3007}{\htmlId{11021}{\htmlClass{Field}{\text{dState}}}}\, \,\htmlId{11028}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#2600}{\htmlId{11030}{\htmlClass{Field}{\text{deposits}}}}\, \,\htmlId{11039}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#10710}{\htmlId{11041}{\htmlClass{Bound}{\text{depositsᵍ}}}}\, \,\htmlId{11051}{\htmlClass{Symbol}{\text{}}}}\, \\ \,\htmlId{11085}{\htmlClass{Keyword}{\text{record}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#3027}{\htmlId{11092}{\htmlClass{Field}{\text{pState}}}}\, \,\htmlId{11099}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#2749}{\htmlId{11101}{\htmlClass{Field}{\text{deposits}}}}\, \,\htmlId{11110}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#10698}{\htmlId{11112}{\htmlClass{Bound}{\text{depositsᵖ}}}}\, \,\htmlId{11122}{\htmlClass{Symbol}{\text{}}}}\, \\ \,\htmlId{11156}{\htmlClass{Keyword}{\text{record}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#3047}{\htmlId{11163}{\htmlClass{Field}{\text{gState}}}}\, \,\htmlId{11170}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#2909}{\htmlId{11172}{\htmlClass{Field}{\text{deposits}}}}\, \,\htmlId{11181}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#10710}{\htmlId{11183}{\htmlClass{Bound}{\text{depositsᵍ}}}}\, \,\htmlId{11193}{\htmlClass{Symbol}{\text{}}}}\, \end{pmatrix}$) certState coinFromDeposits : CertState → Coin coinFromDeposits certState = getCoin (DepositsOf (DStateOf certState)) + getCoin (DepositsOf (PStateOf certState)) + getCoin (DepositsOf (GStateOf certState)) depositsChange : List DCert → ℤ depositsChange certs = coinFromDeposits (updateCertDeposits certs) - coinFromDeposits certState newCertDeposits : List DCert → Coin newCertDeposits certs = posPart (depositsChange certs) refundCertDeposits : List DCert → Coin refundCertDeposits certs = negPart (depositsChange certs) module _ (pp : PParams) where govProposalsDeposits : List GovProposal → Coin govProposalsDeposits = foldl (λ acc _ → acc + pp .govActionDeposit) 0
Design Note: Cert-State Threading and Deposit Accounting¶
This subsection accompanies the new updateCertDeposit family of
functions above and explains the design choice that led to them. Anyone
modifying updateCertDeposit (or the CERT
sub-rules DELEG, POOL, or
GOVCERT) should read this section first.
What changed¶
Previously, the LEDGER rule computed a DepositsChange
record at the top level — holding precomputed posPart/negPart summands for the
top-level and sub-level deposit deltas — and folded that record into
UTxOEnv for use by consumedBatch and
producedBatch. Now, UTxOEnv instead carries the
pre-batch CertState directly, and the UTXO rule
recomputes deposit deltas on the fly from the certificates in the transaction batch.
The motivation is structural: by passing the actual CertState rather
than a precomputed delta, downstream proofs (notably the preservation-of-value proof
in Ledger.Properties.PoV) can relate the UTxO-side deposit accounting
to the genuine CertState evolution produced by the
ENTITIES/CERT rules without intermediating through
posPart/negPart algebra. Gov-proposal deposits also enter this picture
naturally, which is why govProposalsDeposits was added at the same
time.
Promoting the UTxO rule¶
A consequence of this change is that the UTXO rule has been promoted
from a consumer of CertState data (it used to receive a precomputed
DepositsChange) to a secondary executor of certificate accounting.
The updateCertDeposit function in this module recomputes, from a
list of DCerts and a starting CertState, what the
deposits of the resulting CertState should be.
As such, the certificate-deposit logic now exists in two places:
- inside the
CERTsub-rulesDELEG,POOL, andGOVCERTinCerts.lagda.md, where each constructor's result state determines how the deposits evolve as part of the operational semantics; - inside
updateCertDepositin this module, where the same evolution is recomputed in closed form against the pre-batchCertState, for use in theUTXObatch balance equation.
The function updateCertDeposit is a deliberate parallel to the
existing logic inside the CERT sub-rules. Cases must correspond
constructor-for-constructor; the exact Coin update at each cert must
agree.
(Any drift between the two implementations is a soundness problem. If
updateCertDeposit computes a different deposit update for, say,
regdrep c d _ than the GOVCERT-regdrep constructor in
the Certs module does, then the UTXO batch balance equation will
admit transactions whose actual CertState evolution doesn't balance;
i.e., transactions that create or destroy value out of thin air.
The consistency obligation can be stated precisely as a lemma to be
proved alongside LEDGER-pov:
updateCertDeposits-consistent :
∀ {Γ : CertEnv} {s s' : CertState} {dCerts : List DCert}
→ Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s'
→ updateCertDeposits (PParamsOf Γ) s dCerts ≡ s'
Consumed and Produced¶
module _ (pp : PParams) (certState : CertState) where consumedTx : Tx ℓ → UTxO → Value consumedTx tx utxo = balance (utxo ∣ SpendInputsOf tx) + MintedValueOf tx + inject (getCoin (WithdrawalsOf tx)) + inject (govProposalsDeposits pp (ListOfGovProposalsOf tx)) consumed : TopLevelTx → UTxO → Value consumed txTop utxo = consumedTx txTop utxo + inject (newCertDeposits pp certState (allDCerts txTop)) consumedBatch : TopLevelTx → UTxO → Value consumedBatch txTop utxo = consumed txTop utxo + ∑ˡ[ stx ← SubTransactionsOf txTop ] (consumedTx stx utxo)
Direct deposits can be made into account addresses.
In the preservation-of-value equation, direct deposits appear on the
produced side: getCoin (DirectDepositsOf tx) sums the ADA of all direct deposits in
the transaction and that amount is deposited into accounts.
producedTx : Tx ℓ → Value producedTx tx = balance (outs tx) + inject (DonationsOf tx) + inject (getCoin (DirectDepositsOf tx)) produced : TopLevelTx → Value produced txTop = producedTx txTop + inject (TxFeesOf txTop) + inject (refundCertDeposits pp certState (allDCerts txTop)) producedBatch : TopLevelTx → Value producedBatch txTop = produced txTop + ∑ˡ[ stx ← SubTransactionsOf txTop ] (producedTx stx)
CIP-159 Notes¶
Preservation of Value¶
CIP-159 introduces two new fields to transactions: directDeposits and
balanceIntervals. Direct deposits represent value that flows from the transaction
into account addresses.
In the preservation-of-value equation, direct deposits appear on the
produced side: value leaves the UTxO and enters account balances. The
getCoin (DirectDepositsOf tx) term, appearing in the definition of
producedTx, sums the ADA of all direct deposits in
the transaction.
Phantom Asset Prevention¶
NoPhantomWithdrawals : Rewards → TopLevelTx → Type NoPhantomWithdrawals preBalances txTop = ∀[ (addr , amt) ∈ allWithdrawals txTop ˢ ] amt ≤ maybe id 0 (lookupᵐ? preBalances (RewardAddress.stake addr))
The Problem. CIP-159 identifies a "phantom asset" attack when nested transactions combine direct deposits and withdrawals to the same account within a single batch. If a sub-transaction deposits ADA into an account and a later sub-transaction withdraws it, Plutus scripts may be tricked into believing native assets were minted.
The Solution. Withdrawals across the entire batch are bounded by the
pre-batch account balances. The NoPhantomWithdrawals predicate
checks that the total withdrawal for each reward address (aggregated via
allWithdrawals) does not exceed the pre-batch balance of the
corresponding credential. This mirrors the spend-side safety principle where
spending inputs must come from the pre-batch UTxO snapshot (utxo₀).
The UTXOS Transition System¶
Phase-2 Validation¶
Phase-2 validation is the evaluation of all Plutus scripts needed by the top-level transaction and all its subtransactions in the shared, batch-scoped context.
The Script.Validation module is not UTxOEnv-context
aware, so in order to assemble the correct set of scripts and data
for each transaction, we must provide Script.Validation with
the following components:
- the pre-batch spend-side snapshot
UTxOOfΓ, - the script pool
ScriptPoolOfΓ,
Phase-2 scripts together with their context are collected by the function
allP2ScriptsWithContext:
allP2ScriptsWithContext : UTxOEnv → TopLevelTx → List (P2Script × List Data × ExUnits × CostModel) allP2ScriptsWithContext Γ txTop = p2ScriptsWithContext txTop ++ concatMap p2ScriptsWithContext (SubTransactionsOf txTop) where p2ScriptsWithContext : Tx ℓ → List (P2Script × List Data × ExUnits × CostModel) p2ScriptsWithContext t = collectP2ScriptsWithContext (PParamsOf Γ) txTop (UTxOOf Γ) -- (1) (ScriptPoolOf Γ) -- (2)
New in Dijkstra¶
In Dijkstra, the state-modifying logic, which before was part to
UTXOS (cf,. Conway specification), now belongs to the
UTXO rule.
The UTXOS rule validates the correspondence between evaluating
phase-2 scripts and the isValid flag in the top-level transaction.
Phase-2 validation occurs after (successful) phase-1 validation. In Dijkstra,
the evaluation of scripts, from the sub- and top-level transactions, is defered
to the UTXOS rule. This enforces that sub-transactions and
other aspects of the top-level transaction are phase-1 valid.
data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → ⊤ → TopLevelTx → ⊤ → Type where UTXOS : ∙ evalP2Scripts (allP2ScriptsWithContext Γ txTop) ≡ IsValidFlagOf txTop ──────────────────────────────── Γ ⊢ tt ⇀⦇ txTop ,UTXOS⦈ tt
The UTXO Transition System¶
The UTXO Transition System¶
The CIP states:
All inputs of all transactions in a single batch must be contained in the UTxO set before any of the batch transactions are applied. This ensures that operation of scripts is not disrupted, for example, by temporarily duplicating thread tokens, or falsifying access to assets via flash loans.
The SUBUTXO Rule¶
-
The set of spending inputs must be nonempty. This prevents replay attacks.
-
The set of spending and reference inputs must exist in the UTxO before applying the transaction (or partially applying any part of it).
-
The set of spending inputs must exist in the UTXO state, which has been updated by other sub-transactions in the batch. This prevents sub/top-level transactions from spending inputs twice. In other words, spending inputs across all top- and sub-level transactions are disjoint.
-
Direct deposit targets must be registered accounts (their credentials must appear in
dom accountBalances). -
Each balance interval assertion must hold against the pre-batch account balances; this is a Phase-1 validity condition.
data _⊢_⇀⦇_,SUBUTXO⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxOState → Type where SUBUTXO : let UTxOOverhead = 160 maxBootstrapAddrSize = 64 in ∙ SpendInputsOf txSub ≢ ∅ -- (1) ∙ SpendInputsOf txSub ⊆ dom (UTxOOf Γ) -- (2) ∙ ReferenceInputsOf txSub ⊆ dom (UTxOOf Γ) -- (2) ∙ SpendInputsOf txSub ⊆ dom (UTxOOf s₀) -- (3) ∙ inInterval (SlotOf Γ) (ValidIntervalOf txSub) ∙ coin (MintedValueOf txSub) ≡ 0 ∙ ∀[ (_ , o) ∈ ∣ TxOutsOf txSub ∣ ] (inject ((UTxOOverhead + utxoEntrySize o) * coinsPerUTxOByte (PParamsOf Γ)) ≤ᵗ txOutToValue o) ∙ ∀[ (_ , o) ∈ ∣ TxOutsOf txSub ∣ ] (serializedSize (txOutToValue o) ≤ maxValSize (PParamsOf Γ)) ∙ ∀[ (a , _) ∈ range (TxOutsOf txSub) ] (Sum.All (const ⊤) (λ a → AttrSizeOf a ≤ maxBootstrapAddrSize) a) ∙ ∀[ (a , _) ∈ range (TxOutsOf txSub) ] (netId a ≡ NetworkId) ∙ ∀[ a ∈ dom (WithdrawalsOf txSub)] (NetworkIdOf a ≡ NetworkId) ∙ ∀[ a ∈ dom (DirectDepositsOf txSub)] (NetworkIdOf a ≡ NetworkId) ∙ MaybeNetworkIdOf txSub ~ just NetworkId ∙ CurrentTreasuryOf txSub ~ just (TreasuryOf Γ) ∙ mapˢ stake (dom (DirectDepositsOf txSub)) ⊆ dom (AccountBalancesOf Γ) ∙ dom (BalanceIntervalsOf txSub) ⊆ dom (AccountBalancesOf Γ) ∙ ∀[ (c , interval) ∈ BalanceIntervalsOf txSub ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? (AccountBalancesOf Γ) c)) interval) ──────────────────────────────── let s₁ = if IsTopLevelValidFlagOf Γ then $\begin{pmatrix} \,\htmlId{23843}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5756}{\htmlId{23844}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{23851}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{23854}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#11706}{\htmlId{23856}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7374}{\htmlId{23870}{\htmlClass{Generalizable}{\text{txSub}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{23876}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{23877}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{23879}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7415}{\htmlId{23882}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7374}{\htmlId{23887}{\htmlClass{Generalizable}{\text{txSub}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{23895}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{23902}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{23907}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{23919}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{23922}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#650}{\htmlId{23924}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7374}{\htmlId{23936}{\htmlClass{Generalizable}{\text{txSub}}}}\, \end{pmatrix}$ else $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#5756}{\htmlId{23951}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{23958}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{23963}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{23970}{\htmlClass{Generalizable}{\text{s₀}}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{23975}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{23987}{\htmlClass{Generalizable}{\text{s₀}}}}\, \end{pmatrix}$ in Γ ⊢ s₀ ⇀⦇ txSub ,SUBUTXO⦈ s₁
The UTXO Rule¶
-
The set of spending inputs must be nonempty. This prevents replay attacks.
-
The set of spending and reference inputs must exist in the UTxO before applying the transaction (or partially applying any part of it).
-
The set of spending inputs must exist in the UTXO state, which has been updated by other sub-transactions in the batch. This prevents sub/top-level transactions from spending inputs twice. In other words, spending inputs across all top- and sub-level transactions are disjoint.
-
In Legacy Mode: The top-level transaction must be self-balancing.
data _⊢_⇀⦇_,UTXO⦈_ : UTxOEnv × Bool → UTxOState → TopLevelTx → UTxOState → Type where UTXO : let UTxOOverhead = 160 maxBootstrapAddrSize = 64 in ∙ SpendInputsOf txTop ≢ ∅ ∙ SpendInputsOf txTop ⊆ dom (UTxOOf Γ) -- (2) ∙ ReferenceInputsOf txTop ⊆ dom (UTxOOf Γ) -- (2) ∙ SpendInputsOf txTop ⊆ dom (UTxOOf s₀) -- (3) ∙ inInterval (SlotOf Γ) (ValidIntervalOf txTop) ∙ minfee (PParamsOf Γ) txTop (UTxOOf Γ) ≤ TxFeesOf txTop ∙ coin (MintedValueOf txTop) ≡ 0 ∙ consumedBatch (PParamsOf Γ) (CertStateOf Γ) txTop (UTxOOf Γ) ≡ producedBatch (PParamsOf Γ) (CertStateOf Γ) txTop ∙ (legacyMode ≡ true → consumed (PParamsOf Γ) (CertStateOf Γ) txTop (UTxOOf Γ) ≡ produced (PParamsOf Γ) (CertStateOf Γ) txTop) -- (4) ∙ SizeOf txTop ≤ maxTxSize (PParamsOf Γ) ∙ ∑ˡ[ x ← setToList (allReferenceScripts txTop (UTxOOf Γ)) ] scriptSize x ≤ (PParamsOf Γ) .maxRefScriptSizePerTx ∙ ((RedeemersOf txTop ˢ ≢ ∅) ⊎ (List.Any (λ txSub → RedeemersOf txSub ˢ ≢ ∅) (SubTransactionsOf txTop)) → collateralCheck (PParamsOf Γ) txTop (UTxOOf Γ)) ∙ ∀[ (_ , o) ∈ ∣ TxOutsOf txTop ∣ ] (inject ((UTxOOverhead + utxoEntrySize o) * coinsPerUTxOByte (PParamsOf Γ)) ≤ᵗ txOutToValue o) ∙ ∀[ (_ , o) ∈ ∣ TxOutsOf txTop ∣ ] (serializedSize (txOutToValue o) ≤ maxValSize (PParamsOf Γ)) ∙ ∀[ (a , _) ∈ range (TxOutsOf txTop) ] (Sum.All (const ⊤) (λ a → AttrSizeOf a ≤ maxBootstrapAddrSize)) a ∙ ∀[ (a , _) ∈ range (TxOutsOf txTop) ] (netId a ≡ NetworkId) ∙ ∀[ a ∈ dom (WithdrawalsOf txTop)] NetworkIdOf a ≡ NetworkId ∙ ∀[ a ∈ dom (DirectDepositsOf txTop)] (NetworkIdOf a ≡ NetworkId) ∙ MaybeNetworkIdOf txTop ~ just NetworkId ∙ CurrentTreasuryOf txTop ~ just (TreasuryOf Γ) ∙ mapˢ stake (dom (DirectDepositsOf txTop)) ⊆ dom (AccountBalancesOf Γ) ∙ dom (BalanceIntervalsOf txTop) ⊆ dom (AccountBalancesOf Γ) ∙ ∀[ (c , interval) ∈ BalanceIntervalsOf txTop ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? (AccountBalancesOf Γ) c)) interval) ∙ Γ ⊢ _ ⇀⦇ txTop ,UTXOS⦈ _ ──────────────────────────────── let s₁ = if IsValidFlagOf txTop then $\begin{pmatrix} \,\htmlId{26948}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5756}{\htmlId{26949}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{26956}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{26959}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#11706}{\htmlId{26961}{\htmlClass{Field}{\text{SpendInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7346}{\htmlId{26975}{\htmlClass{Generalizable}{\text{txTop}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{26981}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,\,\htmlId{26982}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{26984}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7415}{\htmlId{26987}{\htmlClass{Function}{\text{outs}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7346}{\htmlId{26992}{\htmlClass{Generalizable}{\text{txTop}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{27000}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{27007}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{27010}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#10767}{\htmlId{27012}{\htmlClass{Field}{\text{TxFeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7346}{\htmlId{27021}{\htmlClass{Generalizable}{\text{txTop}}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{27029}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{27041}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{27044}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Prelude.Base.html#650}{\htmlId{27046}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7346}{\htmlId{27058}{\htmlClass{Generalizable}{\text{txTop}}}}\, \end{pmatrix}$ else $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#5756}{\htmlId{27073}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{27080}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{27083}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\htmlId{27085}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#10602}{\htmlId{27086}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7346}{\htmlId{27105}{\htmlClass{Generalizable}{\text{txTop}}}}\,\,\htmlId{27110}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{27112}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Prelude.Base.html#765}{\htmlId{27116}{\htmlClass{Field}{\text{FeesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{27123}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{27126}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7552}{\htmlId{27128}{\htmlClass{Function}{\text{cbalance}}}}\, \,\htmlId{27137}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Transaction.html#5756}{\htmlId{27138}{\htmlClass{Field}{\text{UTxOOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{27145}{\htmlClass{Generalizable}{\text{s₀}}}}\, \,\href{Axiom.Set.Map.html#13536}{\htmlId{27148}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Ledger.Dijkstra.Specification.Transaction.html#10602}{\htmlId{27150}{\htmlClass{Field}{\text{CollateralInputsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7346}{\htmlId{27169}{\htmlClass{Generalizable}{\text{txTop}}}}\,\,\htmlId{27174}{\htmlClass{Symbol}{\text{)}}}\, \\ \,\href{Ledger.Prelude.Base.html#650}{\htmlId{27178}{\htmlClass{Field}{\text{DonationsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Utxo.html#7319}{\htmlId{27190}{\htmlClass{Generalizable}{\text{s₀}}}}\, \end{pmatrix}$ in (Γ , legacyMode) ⊢ s₀ ⇀⦇ txTop ,UTXO⦈ s₁