Description
Parent issue: #1187 (LEDGER PoV)
Depends on: #1117, #1120
This issue discharges the three Utxo/Utxow-level lemmas that LEDGER-pov (issue #1187) calls out by name: UTXOW-batch-balance-coin, UTXOW-V-mechanical, and utxow-pov-invalid. Nothing here is in scope beyond what LEDGER-pov actually needs.
What this PR delivers
| Lemma |
Used in LEDGER-pov to … |
utxow-pov-invalid |
establish the LEDGER-I case (invalid transaction preserves getCoin utxoSt) |
UTXOW-V-mechanical |
track getCoin utxoSt₀ + Σ outs + Σ donations + txFee ≡ getCoin utxoSt₂ + Σ cbalance (UTxOOf Γ ∣ SpendInputs) |
UTXOW-batch-balance-coin |
provide the coin projection of the batch-balance premise consumedBatch ≡ producedBatch, in the precise field-order required by the step-ii chain |
Supporting lemmas (proved in this PR because the three above call them):
UTXO-I-getCoin, UTXO-V-mechanical (UTXOW wrappers delegate to these via UTXOW⇒UTXO).batch-balance-coin (the UTXO-level analogue of UTXOW-batch-balance-coin).- Three-layer batch-coin decomposition:
coin-producedTx/coin-consumedTx (per-transaction), coin-∑-producedTx-sub/coin-∑-consumedTx-sub (sub-transaction sums), coin-of-producedBatch/coin-of-consumedBatch (batch level).
- Era-independent helpers in
Utxo.Properties.Base: ∙-homo-Coin, newTxid⇒disj, outs-disjoint, coin-∑ˡ.
Out of scope
A standalone UTXO-pov theorem is not proved. LEDGER-pov doesn't consume one — it composes UTXOW-V-mechanical with UTXOW-batch-balance-coin directly. The earlier draft of this issue carried a UTXO-pov claim as a placeholder; it is dropped.
Module parameters
balance-∪, split-balance, outs-disjoint, noMintTx, noMintSubTx remain as module parameters of the relevant sub-modules. Each is era-independent and orthogonal to CIP-159; they will be ported from Conway in follow-ups (see the parent issue #1187 for the list).
Modules introduced
| Module |
Purpose |
Utxo.Properties.Base |
Era-independent helpers |
Utxo.Properties.PoV |
UTXO-level building blocks called by the Utxow wrappers |
Utxow.Properties.PoV |
The three lemmas LEDGER-pov invokes |
Acceptance criteria
Description
Parent issue: #1187 (LEDGER PoV)
Depends on: #1117, #1120
This issue discharges the three Utxo/Utxow-level lemmas that
LEDGER-pov(issue #1187) calls out by name:UTXOW-batch-balance-coin,UTXOW-V-mechanical, andutxow-pov-invalid. Nothing here is in scope beyond whatLEDGER-povactually needs.What this PR delivers
LEDGER-povto …utxow-pov-invalidLEDGER-Icase (invalid transaction preservesgetCoin utxoSt)UTXOW-V-mechanicalgetCoin utxoSt₀ + Σ outs + Σ donations + txFee ≡ getCoin utxoSt₂ + Σ cbalance (UTxOOf Γ ∣ SpendInputs)UTXOW-batch-balance-coinconsumedBatch ≡ producedBatch, in the precise field-order required by thestep-iichainSupporting lemmas (proved in this PR because the three above call them):
UTXO-I-getCoin,UTXO-V-mechanical(UTXOW wrappers delegate to these viaUTXOW⇒UTXO).batch-balance-coin(the UTXO-level analogue ofUTXOW-batch-balance-coin).coin-producedTx/coin-consumedTx(per-transaction),coin-∑-producedTx-sub/coin-∑-consumedTx-sub(sub-transaction sums),coin-of-producedBatch/coin-of-consumedBatch(batch level).Utxo.Properties.Base:∙-homo-Coin,newTxid⇒disj,outs-disjoint,coin-∑ˡ.Out of scope
A standalone
UTXO-povtheorem is not proved.LEDGER-povdoesn't consume one — it composesUTXOW-V-mechanicalwithUTXOW-batch-balance-coindirectly. The earlier draft of this issue carried aUTXO-povclaim as a placeholder; it is dropped.Module parameters
balance-∪,split-balance,outs-disjoint,noMintTx,noMintSubTxremain as module parameters of the relevant sub-modules. Each is era-independent and orthogonal to CIP-159; they will be ported from Conway in follow-ups (see the parent issue #1187 for the list).Modules introduced
Utxo.Properties.BaseUtxo.Properties.PoVUtxow.Properties.PoVLEDGER-povinvokesAcceptance criteria
UTXOW-batch-balance-coin,UTXOW-V-mechanical,utxow-pov-invalidtypecheck and are exposed toLEDGER-povmodulo the listed module parameters.UTXO-povclaim.--safe.