|
| 1 | +--- |
| 2 | +source_branch: master |
| 3 | +source_path: src/Ledger/Dijkstra/Specification/Utxow/Properties/PoV.lagda.md |
| 4 | +--- |
| 5 | + |
| 6 | +# UTXOW Properties: Preservation of Value {#sec:utxow-pov} |
| 7 | + |
| 8 | +This module provides the `UTXOW`{.AgdaDatatype}-level preservation-of-value |
| 9 | +facts consumed by `Ledger.Properties.PoV`{.AgdaModule}: it discharges the |
| 10 | +`utxow-pov-invalid`, `UTXOW-V-mechanical`, `UTXOW-batch-balance-coin` and |
| 11 | +`subutxow-step-coin` module parameters of the `LEDGER-PoV`{.AgdaModule} |
| 12 | +consumer (issue #1186), with statements matching those parameters verbatim. |
| 13 | + |
| 14 | +The `UTXOW`{.AgdaDatatype} rules perform witness checks (signatures, scripts, |
| 15 | +datums) and delegate the state change to the `UTXO`{.AgdaDatatype} rule: both |
| 16 | +`UTXOW-normal`{.AgdaInductiveConstructor} and |
| 17 | +`UTXOW-legacy`{.AgdaInductiveConstructor} embed a `UTXO`{.AgdaDatatype} |
| 18 | +derivation as their final premise, and likewise |
| 19 | +`SUBUTXOW`{.AgdaInductiveConstructor} embeds a `SUBUTXO`{.AgdaDatatype} |
| 20 | +derivation. Consequently every PoV statement about the witnessed rules |
| 21 | +reduces, via the extractors below, to its counterpart in |
| 22 | +`Utxo.Properties.PoV`{.AgdaModule}. |
| 23 | + |
| 24 | +<!-- |
| 25 | +```agda |
| 26 | +{-# OPTIONS --safe #-} |
| 27 | +
|
| 28 | +open import Ledger.Dijkstra.Specification.Abstract using (AbstractFunctions) |
| 29 | +open import Ledger.Dijkstra.Specification.Transaction |
| 30 | +
|
| 31 | +module Ledger.Dijkstra.Specification.Utxow.Properties.PoV |
| 32 | + (txs : _) (open TransactionStructure txs) |
| 33 | + (abs : AbstractFunctions txs) (open AbstractFunctions abs) |
| 34 | + where |
| 35 | +
|
| 36 | +open import Ledger.Prelude |
| 37 | +
|
| 38 | +open import Ledger.Dijkstra.Specification.Certs govStructure |
| 39 | +open import Ledger.Dijkstra.Specification.Utxo txs abs |
| 40 | +open import Ledger.Dijkstra.Specification.Utxow txs abs |
| 41 | +open import Ledger.Dijkstra.Specification.Utxo.Properties.PoV txs abs |
| 42 | +``` |
| 43 | +--> |
| 44 | + |
| 45 | +## Extracting the state-changing step |
| 46 | + |
| 47 | +```agda |
| 48 | +UTXOW⇒UTXO : ∀ {Γ : UTxOEnv} {s s' : UTxOState} {tx : TopLevelTx} |
| 49 | + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → Γ ⊢ s ⇀⦇ tx ,UTXO⦈ s' |
| 50 | +UTXOW⇒UTXO (UTXOW-normal-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ utxoStep) = utxoStep |
| 51 | +UTXOW⇒UTXO (UTXOW-legacy-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ utxoStep) = utxoStep |
| 52 | +
|
| 53 | +SUBUTXOW⇒SUBUTXO : ∀ {Γ : SubUTxOEnv} {s s' : UTxOState} {stx : SubLevelTx} |
| 54 | + → Γ ⊢ s ⇀⦇ stx ,SUBUTXOW⦈ s' → Γ ⊢ s ⇀⦇ stx ,SUBUTXO⦈ s' |
| 55 | +SUBUTXOW⇒SUBUTXO (SUBUTXOW-⋯ _ _ _ _ _ _ _ _ _ _ _ _ subUtxoStep) = subUtxoStep |
| 56 | +``` |
| 57 | + |
| 58 | +## The `UTXOW-PoV` module |
| 59 | + |
| 60 | +Stated for a fixed top-level transaction `tx` and the per-sub-transaction |
| 61 | +no-mint fact, mirroring the parameterisation of the |
| 62 | +`LEDGER-PoV`{.AgdaModule} consumer (which holds both and can instantiate this |
| 63 | +module directly). Each lemma delegates to `UTXO-PoV`{.AgdaModule} via |
| 64 | +`UTXOW⇒UTXO`{.AgdaFunction}. |
| 65 | + |
| 66 | +```agda |
| 67 | +module UTXOW-PoV |
| 68 | + (tx : TopLevelTx) |
| 69 | + (noMintSubTx : noMintingSubTxs tx) |
| 70 | + where |
| 71 | +
|
| 72 | + open UTXO-PoV tx noMintSubTx |
| 73 | +``` |
| 74 | + |
| 75 | +### `utxow-pov-invalid` |
| 76 | + |
| 77 | +An invalid top-level transaction moves its collateral balance into the fee pot, |
| 78 | +preserving `getCoin`{.AgdaField} of the `UTxOState`{.AgdaRecord} exactly: |
| 79 | + |
| 80 | +```agda |
| 81 | + utxow-pov-invalid : ∀ {Γ' : UTxOEnv} {s₀ s₁ : UTxOState} |
| 82 | + → Γ' ⊢ s₀ ⇀⦇ tx ,UTXOW⦈ s₁ |
| 83 | + → IsValidFlagOf tx ≡ false |
| 84 | + → getCoin s₀ ≡ getCoin s₁ |
| 85 | + utxow-pov-invalid utxowStep invalid = UTXO-pov-invalid (UTXOW⇒UTXO utxowStep) invalid |
| 86 | +``` |
| 87 | + |
| 88 | +### `UTXOW-V-mechanical` |
| 89 | + |
| 90 | +The valid-case coin equation for the top-level state change (spend inputs |
| 91 | +resolved against the running UTxO; freshness of `TxIdOf tx` lets `outs tx` |
| 92 | +split off cleanly): |
| 93 | + |
| 94 | +```agda |
| 95 | + UTXOW-V-mechanical : ∀ {Γ' : UTxOEnv} {s₀ s₁ : UTxOState} |
| 96 | + → Γ' ⊢ s₀ ⇀⦇ tx ,UTXOW⦈ s₁ |
| 97 | + → IsValidFlagOf tx ≡ true |
| 98 | + → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s₀)) |
| 99 | + → getCoin s₀ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx |
| 100 | + ≡ getCoin s₁ + cbalance (UTxOOf s₀ ∣ SpendInputsOf tx) |
| 101 | + UTXOW-V-mechanical utxowStep valid fresh = |
| 102 | + UTXO-V-mechanical (UTXOW⇒UTXO utxowStep) valid fresh |
| 103 | +``` |
| 104 | + |
| 105 | +### `UTXOW-batch-balance-coin` |
| 106 | + |
| 107 | +The coin projection of the spec's batch balance premise |
| 108 | +`consumedBatch ≡ producedBatch`, in closed form: cert deposits as |
| 109 | +`refundCertDeposits`{.AgdaFunction}/`newCertDeposits`{.AgdaFunction} over |
| 110 | +`allDCerts tx` against the environment's pre-batch registered-pool set, and the |
| 111 | +batch's governance-action deposits collected in a trailing group. The minted |
| 112 | +terms drop out (premise 7 of the `UTXO`{.AgdaDatatype} rule for the top level; |
| 113 | +the `noMintSubTx`{.AgdaBound} module parameter for the sub-transactions). |
| 114 | + |
| 115 | +```agda |
| 116 | + UTXOW-batch-balance-coin : ∀ {Γ' : UTxOEnv} {s₀ s₁ : UTxOState} |
| 117 | + → Γ' ⊢ s₀ ⇀⦇ tx ,UTXOW⦈ s₁ |
| 118 | + → cbalance (UTxOOf Γ' ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) |
| 119 | + + sum (map (λ stx → cbalance (UTxOOf Γ' ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) |
| 120 | + (SubTransactionsOf tx)) |
| 121 | + + refundCertDeposits (PParamsOf Γ') (allDCerts tx) |
| 122 | + ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) |
| 123 | + + sum (map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) |
| 124 | + (SubTransactionsOf tx)) |
| 125 | + + newCertDeposits (PParamsOf Γ') (dom (PoolsOf Γ')) (allDCerts tx) |
| 126 | + + ( govProposalsDeposits (PParamsOf Γ') (ListOfGovProposalsOf tx) |
| 127 | + + sum (map (λ stx → govProposalsDeposits (PParamsOf Γ') (ListOfGovProposalsOf stx)) |
| 128 | + (SubTransactionsOf tx)) ) |
| 129 | + UTXOW-batch-balance-coin utxowStep = UTXO-batch-balance-coin (UTXOW⇒UTXO utxowStep) |
| 130 | +``` |
| 131 | + |
| 132 | +## The `SUBUTXOW-PoV` module |
| 133 | + |
| 134 | +The per-step `SUBUTXOW`{.AgdaDatatype} coin equation resolves the spent balance |
| 135 | +against the *pre-batch snapshot* `UTxOOf Γ`, so — as explained in |
| 136 | +`Utxo.Properties.PoV`{.AgdaModule} — it holds only given two batch-threading |
| 137 | +facts that the per-step premises do not provide: freshness of the |
| 138 | +sub-transaction's TxId in the running UTxO, and agreement of the running UTxO |
| 139 | +with the snapshot on the sub-transaction's spend inputs. Both follow from |
| 140 | +batch-wide input disjointness and TxId freshness, which the outer |
| 141 | +`UTXO`{.AgdaDatatype} rule establishes at the batch level but does not expose |
| 142 | +per step. They are module parameters here, to be discharged by a |
| 143 | +batch-threading invariant (the same follow-up family as the |
| 144 | +`utxo₁-tx-spend-eq` and `fresh-top-tx-id` parameters of |
| 145 | +`Ledger.Properties.PoV`{.AgdaModule}). |
| 146 | + |
| 147 | +```agda |
| 148 | +module SUBUTXOW-PoV |
| 149 | + ( subtx-fresh-txid : ∀ {Γ : SubUTxOEnv} {s₀ s₁ : UTxOState} {stx : SubLevelTx} |
| 150 | + → IsTopLevelValidFlagOf Γ ≡ true |
| 151 | + → Γ ⊢ s₀ ⇀⦇ stx ,SUBUTXOW⦈ s₁ |
| 152 | + → TxIdOf stx ∉ mapˢ proj₁ (dom (UTxOOf s₀)) ) |
| 153 | + ( subtx-spend-agree : ∀ {Γ : SubUTxOEnv} {s₀ s₁ : UTxOState} {stx : SubLevelTx} |
| 154 | + → IsTopLevelValidFlagOf Γ ≡ true |
| 155 | + → Γ ⊢ s₀ ⇀⦇ stx ,SUBUTXOW⦈ s₁ |
| 156 | + → cbalance (UTxOOf s₀ ∣ SpendInputsOf stx) ≡ cbalance (UTxOOf Γ ∣ SpendInputsOf stx) ) |
| 157 | + where |
| 158 | +
|
| 159 | + subutxow-step-coin : ∀ {Γ : SubUTxOEnv} {s₀ s₁ : UTxOState} {stx : SubLevelTx} |
| 160 | + → IsTopLevelValidFlagOf Γ ≡ true |
| 161 | + → Γ ⊢ s₀ ⇀⦇ stx ,SUBUTXOW⦈ s₁ |
| 162 | + → getCoin s₀ + cbalance (outs stx) + DonationsOf stx |
| 163 | + ≡ getCoin s₁ + cbalance (UTxOOf Γ ∣ SpendInputsOf stx) |
| 164 | + subutxow-step-coin isV utxowStep = |
| 165 | + subutxo-step-coin isV (SUBUTXOW⇒SUBUTXO utxowStep) |
| 166 | + (subtx-fresh-txid isV utxowStep) |
| 167 | + (subtx-spend-agree isV utxowStep) |
| 168 | +``` |
0 commit comments