diff --git a/CHANGELOG.md b/CHANGELOG.md index bce112fb2d..964a0416fa 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,8 +4,9 @@ ### WIP +- Apply per-transaction direct deposits to `CertState` after each `CERTS` step in `SUBLEDGER-V` and `LEDGER-V` (CIP-159). - Forbid CIP-159 fields (`txDirectDeposits`, `txBalanceIntervals`) in legacy mode via explicit `UTXOW-legacy` premises. -- Allow partial withdrawals in `PRE-CERT` rule; define `applyWithdrawals` and `_≤ᵐ_` (CIP-159). +- Allow partial withdrawals in `PRE-CERT` rule; define `applyWithdrawals` (CIP-159). - Extend `TxInfo` with `txDirectDeposits` and `txBalanceIntervals` fields (CIP-159). - Remove `allBalanceIntervals` batch-level aggregation helper; balance interval assertions will be checked per-(sub)transaction in `UTXO`/`SUBUTXO` rules (see #1117). diff --git a/src/Ledger/Conway/Conformance/Properties.lagda.md b/src/Ledger/Conway/Conformance/Properties.lagda.md index 02a6bda488..a0ef830169 100644 --- a/src/Ledger/Conway/Conformance/Properties.lagda.md +++ b/src/Ledger/Conway/Conformance/Properties.lagda.md @@ -124,8 +124,6 @@ module _ (s : ChainState) where -- Transaction properties module _ {slot} {tx} (let txb = body tx) (valid : validTxIn₂ s slot tx) - (indexedSum-∪⁺-hom : ∀ {A V : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq V ⦄ ⦃ mon : CommutativeMonoid 0ℓ 0ℓ V ⦄ - → (d₁ d₂ : A ⇀ V) → indexedSumᵛ' id (d₁ ∪⁺ d₂) ≡ indexedSumᵛ' id d₁ ◇ indexedSumᵛ' id d₂) (indexedSum-⊆ : ∀ {A : Type} ⦃ _ : DecEq A ⦄ (d d' : A ⇀ ℕ) → d ˢ ⊆ d' ˢ → indexedSumᵛ' id d ≤ indexedSumᵛ' id d') -- technically we could use an ordered monoid instead of ℕ where diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md index 80a46a5dd9..db2c5ba602 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md @@ -46,19 +46,12 @@ private variable instance _ = +-0-monoid -module Certs-PoV ( indexedSumᵛ'-∪' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → disjoint (dom m) (dom m') - → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) - -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`. - ( sumConstZero' : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 ) - ( res-decomp' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ ) - ( getCoin-cong' : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s' - → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' ) - ( ≡ᵉ-getCoinˢ' : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} - → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) +module Certs-PoV + -- TODO: prove the following assumption, used in roof of `CERTBASE-pov`. + ( ≡ᵉ-getCoinˢ' : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} + → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) where - open Certs-Pov-lemmas indexedSumᵛ'-∪' sumConstZero' res-decomp' getCoin-cong' ≡ᵉ-getCoinˢ' + open Certs-Pov-lemmas ≡ᵉ-getCoinˢ' ``` --> diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md index 662a705262..a481556fa9 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md +++ b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md @@ -23,7 +23,7 @@ open import Axiom.Set.Properties th open import Algebra using (CommutativeMonoid) open import Data.Maybe.Properties open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid; +-identityʳ; +-identityˡ) -open import Relation.Binary using (IsEquivalence) +import Relation.Binary as Eq using (IsEquivalence) open import Relation.Nullary.Decidable open import Tactic.ReduceDec @@ -40,35 +40,7 @@ private variable instance _ = +-0-monoid -getCoin-singleton : ⦃ _ : DecEq A ⦄ {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c -getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _) - -∪ˡsingleton∈dom : ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin} - → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m -∪ˡsingleton∈dom m {(a , c)} a∈dom = ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom) - -module _ ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → disjoint (dom m) (dom m') - → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) - where - open ≡-Reasoning - open Equivalence - - ∪ˡsingleton∉dom : ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin} - → a ∉ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + c - ∪ˡsingleton∉dom m {(a , c)} a∉dom = begin - getCoin (m ∪ˡ ❴ a , c ❵ᵐ) - ≡⟨ indexedSumᵛ'-∪ m ❴ a , c ❵ᵐ - ( λ x y → a∉dom (subst (_∈ dom m) (from ∈-dom-singleton-pair y) x) ) ⟩ - getCoin m + getCoin ❴ a , c ❵ᵐ - ≡⟨ cong (getCoin m +_) getCoin-singleton ⟩ - getCoin m + c - ∎ - - ∪ˡsingleton0≡ : ⦃ _ : DecEq A ⦄ → (m : A ⇀ Coin) {a : A} → getCoin (m ∪ˡ ❴ (a , 0) ❵ᵐ) ≡ getCoin m - ∪ˡsingleton0≡ m {a} with a ∈? dom m - ... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom - ... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m)) +open ≡-Reasoning ``` --> @@ -83,61 +55,55 @@ some `dcert`{.AgdaBound} : `DCert`{.AgdaDatatype}. Then, *Formally*. ```agda - CERT-pov : {Γ : CertEnv} {s s' : CertState} - → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' - → getCoin s ≡ getCoin s' +CERT-pov : {Γ : CertEnv} {s s' : CertState} + → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' → getCoin s ≡ getCoin s' ``` *Proof*. (Click the "Show more Agda" button to reveal the proof.) @@ -175,7 +141,7 @@ value of the withdrawals in `Γ`{.AgdaBound}. In other terms, let open DState (dState cs ) open DState (dState cs') renaming (rewards to rewards') - module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin}) + module ≡ᵉ = Eq.IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin}) wdrlsCC = mapˢ (map₁ RewardAddress.stake) (wdrls ˢ) zeroMap = constMap (mapˢ RewardAddress.stake (dom wdrls)) 0 rwds-∪ˡ-decomp = (rewards ∣ dom wdrlsCC ᶜ) ∪ˡ (rewards ∣ dom wdrlsCC) diff --git a/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md index deef2d4f72..cf21230924 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md @@ -38,15 +38,9 @@ instance module _ (tx : Tx) (let open Tx tx; open TxBody body) - ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → disjoint (dom m) (dom m') → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) - ( sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 ) - ( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ ) - ( getCoin-cong : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s' - → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' ) - ( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} - → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) + -- TODO: prove the following assumption, used in roof of `CERTBASE-pov`. + ( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} + → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) where pattern UTXO-induction r = UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ r _ _ _ @@ -84,8 +78,8 @@ then the coin values of `s`{.AgdaBound} and `s'`{.AgdaBound} are equal, that is, open LState s' renaming (utxoSt to utxoSt'; govSt to govSt'; certState to certState') open CertState certState' open ≡-Reasoning - open Certs-PoV indexedSumᵛ'-∪ sumConstZero res-decomp getCoin-cong ≡ᵉ-getCoinˢ - zeroMap = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0 + open Certs-PoV ≡ᵉ-getCoinˢ + zeroMap = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0 in begin getCoin utxoSt + getCoin certState diff --git a/src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md b/src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md index 9d0455be9f..0e96712946 100644 --- a/src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md +++ b/src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md @@ -51,9 +51,6 @@ coin∅ = begin 0 ∎ where open Prelude.≡-Reasoning -getCoin-singleton : ((dp , c) : DepositPurpose × Coin) → indexedSumᵛ' id ❴ (dp , c) ❵ ≡ c -getCoin-singleton _ = indexedSum-singleton' {A = DepositPurpose × Coin} {f = proj₂} (finiteness _) - module _ -- ASSUMPTION -- (gc-hom : (d₁ d₂ : Deposits) → getCoin (d₁ ∪⁺ d₂) ≡ getCoin d₁ + getCoin d₂) where @@ -63,7 +60,7 @@ module _ -- ASSUMPTION -- getCoin (deps ∪⁺ ❴ (dp , c) ❵) ≡⟨ gc-hom deps ❴ (dp , c) ❵ ⟩ getCoin deps + getCoin{A = Deposits} ❴ (dp , c) ❵ - ≡⟨ cong (getCoin deps +_) (getCoin-singleton (dp , c)) ⟩ + ≡⟨ cong (getCoin deps +_) getCoin-singleton ⟩ getCoin deps + c ∎ where open Prelude.≡-Reasoning diff --git a/src/Ledger/Dijkstra/Specification/Certs.lagda.md b/src/Ledger/Dijkstra/Specification/Certs.lagda.md index 830f0ee316..2102987601 100644 --- a/src/Ledger/Dijkstra/Specification/Certs.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs.lagda.md @@ -103,14 +103,14 @@ record PState : Type where field pools : Pools fPools : Pools - retiring : KeyHash ⇀ Epoch + retiring : Retiring deposits : KeyHash ⇀ Coin record GState : Type where constructor ⟦_,_,_⟧ᵛ field dreps : DReps - ccHotKeys : Credential ⇀ Maybe Credential + ccHotKeys : CCHotKeys deposits : Credential ⇀ Coin record CertState : Type where @@ -294,22 +294,23 @@ The `LEDGER`{.AgdaDatatype} rule will call `applyDirectDeposits`{.AgdaFunction} credit direct deposits to account balances as part of processing a transaction batch. ```agda +-- For each withdrawal entry `(addr, amt)`, look up `stake addr` in the acc, +-- compute `bal ∸ amt`, create a singleton map with the new balance, and +-- merge it with the rest (complement-restricted, to remove the old entry). +applyOne : Rewards → RewardAddress × Coin → Rewards +applyOne acc (addr , amt) = + case lookupᵐ? acc (stake addr) of λ where + (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ) + nothing → acc + -- `nothing` case is defensive; the PRE-CERT precondition guarantees the + -- credential is registered, but handling it makes the function total. + applyWithdrawals : Withdrawals → Rewards → Rewards -applyWithdrawals wdrls rwds = - foldl applyOne rwds (setToList (wdrls ˢ)) - where - -- For each withdrawal entry `(addr, amt)`, look up `stake addr` in the acc, - -- compute `bal ∸ amt`, create a singleton map with the new balance, and - -- merge it with the rest (complement-restricted, to remove the old entry). - applyOne : Rewards → RewardAddress × Coin → Rewards - applyOne acc (addr , amt) = - case lookupᵐ? acc (stake addr) of λ where - (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ) - nothing → acc - -- `nothing` case is defensive; the PRE-CERT precondition guarantees the - -- credential is registered, but handling it makes the function total. +applyWithdrawals wdrls rwds = foldl applyOne rwds (setToList (wdrls ˢ)) ``` + + In the Dijkstra era, CIP-159 allows **partial withdrawals**: a transaction may withdraw any amount up to the current account balance. `applyWithdrawals`{.AgdaFunction} subtracts each withdrawal amount from the diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties.lagda.md index 4efa18eed5..da51385844 100644 --- a/src/Ledger/Dijkstra/Specification/Certs/Properties.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties.lagda.md @@ -13,5 +13,8 @@ module Ledger.Dijkstra.Specification.Certs.Properties where --> ```agda +open import Ledger.Dijkstra.Specification.Certs.Properties.ApplyWithdrawalsPoV open import Ledger.Dijkstra.Specification.Certs.Properties.Computational +open import Ledger.Dijkstra.Specification.Certs.Properties.PoV +open import Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas ``` diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md new file mode 100644 index 0000000000..14d3587a26 --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md @@ -0,0 +1,307 @@ +--- +source_branch: master +source_path: src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md +--- + +# `applyWithdrawals` Preservation of Value {#sec:apply-withdrawals-pov} + +This module proves that `applyWithdrawals` decreases the total rewards balance +by exactly the sum of the withdrawal amounts. This is the key new lemma +for the Dijkstra (CIP-159) CERTS preservation-of-value proof. + +## Proof Strategy + +`applyWithdrawals` is defined as a `foldl` over the list representation of the +withdrawal map. The proof proceeds by induction on this list, with a single-step +lemma showing that each `applyOne` step decreases `getCoin` by exactly the +withdrawal amount. + +The single-step argument decomposes the accumulator map `acc` into: +`acc ≡ᵉ (acc ∣ ❴ c ❵ ᶜ) ∪ˡ (acc ∣ ❴ c ❵)` +where `c = stake addr`. When `lookupᵐ? acc c ≡ just bal` and `amt ≤ bal`: +`getCoin acc = getCoin (acc ∣ ❴ c ❵ ᶜ) + bal`, by decomposition; +`getCoin (applyOne acc (addr , amt))` = `getCoin (❴ c , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ c ❵ ᶜ))` += `(bal ∸ amt) + getCoin (acc ∣ ❴ c ❵ ᶜ)`, by disjoint union. + +So the decrease is `bal - (bal ∸ amt) = amt` (since `amt ≤ bal`). + +For the fold induction, the invariant is maintained because: +- Each credential is targeted at most once (by injectivity of `stake` on `dom wdrls`, + which follows from the `NetworkId` constraint). +- `applyOne` preserves domain membership (it replaces entries, never removes them). +- Therefore, remaining entries still have their credentials registered and their + amounts bounded by the (unchanged) balances. + + + +## Supporting lemmas + +The following auxiliary properties are needed. + +### Single-step Lemma: `applyOne` decreases `getCoin` by `amt` + +When `stake addr ∈ dom acc` and `amt ≤ bal` (where `bal` is the current balance), +applying a single withdrawal decreases the total by exactly `amt`. + +```agda +applyOne-pov : + (acc : Rewards) (addr : RewardAddress) (amt bal : Coin) + → lookupᵐ? acc (stake addr) ≡ just bal + → amt ≤ bal + → getCoin acc ≡ getCoin (❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ)) + amt +``` + + + + +### Domain Membership Preservation Lemma + +```agda +∪ˡ-res-dom-preserve : + ∀ (m : Rewards) (c : Credential) (v : Coin) (c' : Credential) + → c' ∈ dom m → c' ≢ c + → c' ∈ dom (❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ)) +``` + + + + + + + +## Main Theorem + +This is the form needed by `PRE-CERT-pov`. + +```agda + applyWithdrawals-pov : (wdrls : Withdrawals) (rwds : Rewards) + → mapˢ stake (dom wdrls) ⊆ dom rwds + → ∀[ (addr , amt) ∈ wdrls ˢ ] amt ≤ maybe id 0 (lookupᵐ? rwds (stake addr)) + → getCoin rwds ≡ getCoin (applyWithdrawals wdrls rwds) + getCoin wdrls +``` + + + + + diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md new file mode 100644 index 0000000000..a73783756d --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md @@ -0,0 +1,60 @@ +--- +source_branch: master +source_path: src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md +--- + +# CERTS: Preservation of Value {#sec:certs-pov} + + + +## Theorem: The `CERTS` rule preserves value {#thm:CERTS-PoV} + +```agda + CERTS-pov : {Γ : CertEnv} {s₁ sₙ : CertState} + → ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId + → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ + → getCoin s₁ ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ) +``` + +```agda + CERTS-pov {Γ = Γ} validNetId (run (pre-cert , certs)) = + trans (PRE-CERT-pov validNetId pre-cert) + (cong (_+ getCoin (WithdrawalsOf Γ)) (sts-pov certs)) +``` diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md new file mode 100644 index 0000000000..80c0f3d113 --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md @@ -0,0 +1,145 @@ +--- +source_branch: master +source_path: src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md +--- + + +# CERTS: Preservation of Value Lemmas {#sec:certs-pov-lemmas} + +## Key Differences from Conway + ++ **`PRE-CERT`**: Conway uses `constMap wdrlCreds 0 ∪ˡ rewards` (zeroing). + Dijkstra (CIP-159) uses `applyWithdrawals wdrls rewards` (subtraction). + The PoV equation still holds; the proof structure differs. ++ **`CERT` / `DELEG`**: Same value-relevant structure as Conway. ++ **No `CERT-vdel`**: Dijkstra has `CERT-deleg`, `CERT-pool`, `CERT-gov` only. + + + +## CERT-pov: Each certificate step preserves value + +```agda +CERT-pov : {Γ : CertEnv} {s s' : CertState} + → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' → getCoin s ≡ getCoin s' +``` + + + +## POST-CERT-pov and sts-pov + +```agda +POST-CERT-pov : {Γ : CertEnv} {s s' : CertState} + → Γ ⊢ s ⇀⦇ _ ,POST-CERT⦈ s' → getCoin s ≡ getCoin s' + +POST-CERT-pov CERT-post = refl + +sts-pov : {Γ : CertEnv} {s₁ sₙ : CertState} {sigs : List DCert} + → RunTraceAndThen _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_ Γ s₁ sigs sₙ + → getCoin s₁ ≡ getCoin sₙ +sts-pov (run-[] x) = POST-CERT-pov x +sts-pov (run-∷ x xs) = trans (CERT-pov x) (sts-pov xs) +``` + +## PRE-CERT-pov (CIP-159: partial withdrawals) + +The key new assumption `applyWithdrawals-pov` states that applying withdrawals +decreases `rewardsBalance` by exactly the total withdrawn amount. This replaces +Conway's `constMap`/`res-decomp`/`sumConstZero` chain. + + + +```agda + PRE-CERT-pov : {Γ : CertEnv} {s s' : CertState} + → ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId + → Γ ⊢ s ⇀⦇ _ ,PRE-CERT⦈ s' + → getCoin s ≡ getCoin s' + getCoin (WithdrawalsOf Γ) +``` + + diff --git a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md index bff049b17e..203f147b30 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md @@ -68,6 +68,9 @@ instance HasEnactState-LedgerEnv : HasEnactState LedgerEnv HasEnactState-LedgerEnv .EnactStateOf = LedgerEnv.enactState + HasTreasury-LedgerEnv : HasTreasury LedgerEnv + HasTreasury-LedgerEnv .TreasuryOf = LedgerEnv.treasury + HasPParams-SubLedgerEnv : HasPParams SubLedgerEnv HasPParams-SubLedgerEnv .PParamsOf = SubLedgerEnv.pparams @@ -82,9 +85,9 @@ instance HasAccountBalances-SubLedgerEnv : HasAccountBalances SubLedgerEnv HasAccountBalances-SubLedgerEnv .AccountBalancesOf = SubLedgerEnv.accountBalances - ``` --> + ```agda record LedgerState : Type where ``` @@ -99,6 +102,7 @@ record LedgerState : Type where govSt : GovState certState : CertState ``` + + + + ## LEDGER Transition System ```agda - computeProof : (Γ : SubLedgerEnv) (s : LedgerState) (stx : SubLevelTx) - → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s') + computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s') ``` ```agda - completeness : (Γ : SubLedgerEnv) (s : LedgerState) (stx : SubLevelTx) (s' : LedgerState) - → Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s' → (proj₁ <$> computeProof Γ s stx) ≡ success s' + completeness : ∀ s' → Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s' → (proj₁ <$> computeProof) ≡ success s' ``` ```agda - computeProof : (Γ : LedgerEnv) (s : LedgerState) (txTop : TopLevelTx) - → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s') + computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s') ``` ```agda - completeness : (Γ : LedgerEnv) (s : LedgerState) (txTop : TopLevelTx) (s' : LedgerState) - → Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s' → (proj₁ <$> computeProof Γ s txTop) ≡ success s' + completeness : ∀ s' → Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s' → (proj₁ <$> computeProof) ≡ success s' ``` + +## Key Lemma: `applyDirectDeposits` increases `getCoin` by deposit total + +`applyDirectDeposits dd ds = record ds { rewards = RewardsOf ds ∪⁺ dd }`, +and `getCoin` for `CertState` is `rewardsBalance ∘ DStateOf = ∑[ x ← rewards ] x` + + +## Proof Architecture + +The Dijkstra `LEDGER-pov`{.AgdaFunction} proof does NOT decompose into independent +`SUBLEDGERS-pov`{.AgdaFunction} and `UTXOW-pov`{.AgdaFunction} pieces, because: + +1. Individual `SUBUTXO` rules have no balance equation — only the + *batch-level* `consumedBatch ≡ producedBatch` (in `UTXO`) constrains + the total. + +2. Sub-transactions may individually transfer value between UTxO and CertState (via + sub-withdrawals, sub-deposits, sub-direct-deposits) without local balancing. + +Instead, the proof reasons about the **entire** `LEDGER-V`{.AgdaInductiveConstructor} +step at once. + +### LEDGER-V Proof Outline + +Given +`s = ⟦ utxoSt₀ , govSt₀ , certState₀ ⟧` +and +`s' = ⟦ utxoSt₂ , govSt₂' , certStateFinal ⟧`, +where +`certStateFinal` has `rewards = rewards₂ ∪⁺ allDirectDeposits tx`, +we need: + +`getCoin utxoSt₀ + rewardsBalance₀ + deposits₀` +`≡ getCoin utxoSt₂ + rewardsBalance_final + deposits₂` + +The key equations are: + +1. `consumedBatch ≡ producedBatch` (coin projection, from `UTXO`{.AgdaDatatype} premise). + + This gives (using `coin∘inject = id`, `coin mint = 0`): + + `Σ cbalance(utxo₀ ∣ SpendInputs_i) + Σ wdrls_i + depositRefunds` + `= Σ cbalance(outs_i) + txFee + Σ directDeps_i + Σ donations_i + newDeposits` + + where the sums range over all transactions in the batch (top + sub). + +2. `CERTS-pov` (combined sub + top level): + + `rewardsBalance₀ = rewardsBalance₂ + Σ wdrls_i` + + This requires composing sub-level `CERTS-pov` for each subtransaction + with top-level `CERTS-pov`. + +3. `depositsChange` property: + + `deposits₂ = deposits₀ + newDeposits - depositRefunds` + + This follows from the definition of `calculateDepositsChange` and + the posPart/negPart identity. + +4. `applyDirectDeposits`: + + `rewardsBalance_final = rewardsBalance₂ + Σ directDeps_i` + +5. Mechanical UTxO tracking: + + `getCoin utxoSt₂ = cbalance(utxo₂) + fees₂ + donations₂` + + where `utxo₂`, `fees₂`, `donations₂` are determined by the + `SUBLEDGERS` + `UTXO` mechanical state changes. + +Combining: + +From (1) and (3), adding the equations and using `+-cancelʳ-≡` to +eliminate `newDeposits + depositRefunds` from both sides: + ++ `getCoin utxoSt₀ + Σ wdrls_i + coinFromDeposits(cs₀)` + `= getCoin utxoSt₂ + Σ directDeps_i + coinFromDeposits(cs₂)` + +Then: + ++ `getCoin utxoSt₀ + rewardsBalance₀ + coinFromDeposits(cs₀)` + `= getCoin utxoSt₀ + (rewardsBalance₂ + Σ wdrls_i) + coinFromDeposits(cs₀)` (by 2) + `= getCoin utxoSt₂ + Σ directDeps_i + coinFromDeposits(cs₂) + rewardsBalance₂` (by combined 1+3) + `= getCoin utxoSt₂ + rewardsBalance_final + coinFromDeposits(cs₂)` (by 4) + `= getCoin utxoSt₂ + getCoin certStateFinal + coinFromDeposits(cs₂)` (since deposits unchanged by applyDirectDeposits) + + + +### `LEDGER-I` proof outline + +`certState` and `govSt` are unchanged. + +`SUBLEDGERS` is a no-op (`isValid ≡ false` ⟹ each `SUBLEDGER-I` preserves state). + +The UTXOW/UTXO step in the invalid case: + +`utxoSt₁ = ⟦ utxo₀ ∣ collateral ᶜ , fees + cbalance(utxo₀ ∣ collateral) , deposits₀ , donations₀ ⟧` + +(Actually in Dijkstra, deposits aren't in UTxOState, and the invalid case has +`depositsChange = ⟦ 0ℤ , 0ℤ ⟧`, so the UTxO changes are just collateral collection.) + +`getCoin utxoSt₁ = cbalance(utxo₀ ∣ coll ᶜ) + (fees + cbalance(utxo₀ ∣ coll)) + donations₀` + +`= cbalance utxo₀ + fees + donations₀` [by split-balance] + +`= getCoin utxoSt₀` + +So + +`getCoin s' = getCoin utxoSt₁ + getCoin certState₀ + coinFromDeposits certState₀` + +`= getCoin utxoSt₀ + getCoin certState₀ + coinFromDeposits certState₀` + +`= getCoin s` + + + + + +## LEDGER Preservation of Value + +```agda + LEDGER-pov : {Γ : LedgerEnv} {s s' : LedgerState} → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s' +``` + +### LEDGER-I case (invalid transaction) + +This follows the Conway pattern with `certState' ≡ certState₀`. +`certState` and `govSt` are unchanged and `applyDirectDeposits` is not applied. +Only the `UTXOW`{.AgdaDatatype} step matters and it preserves `getCoin utxoSt`. + +```agda + LEDGER-pov {Γ} {s} (LEDGER-I (invalid , subStep , utxoStep)) = + cong (λ u → u + getCoin (CertStateOf s) + coinFromDeposits (CertStateOf s)) + (utxow-pov-invalid utxoStep invalid) +``` + +### LEDGER-V (valid transaction) + +The `LEDGER-V` rule produces + +`s' = ⟦ utxoSt₂ , rmOrphanDRepVotes certStateFinal govState₂ , certStateFinal ⟧` + +where `certStateFinal = record certState₂ { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf certState₂) }`. + +```agda + LEDGER-pov {Γ} {s} + (LEDGER-V {certState₁ = cs₁} {cs₂} {govSt₁} {govSt₂} + {utxoState₁ = us₁} {utxoState₂ = us₂} + (valid , subStep , certStep , govStep , utxoStep)) = + begin + U₀ + R₀ + D₀ ≡⟨ step-i ⟩ + U₀ + R₂ + allWdrls + D₀ ≡⟨ arithmetic-1 U₀ R₂ allWdrls D₀ ⟩ + U₀ + allWdrls + D₀ + R₂ ≡⟨ step-iii-iv ⟩ + U₂ + allDirectDeps + D₂ + R₂ ≡⟨ arithmetic-2 U₂ allDirectDeps D₂ R₂ ⟩ + U₂ + (R₂ + allDirectDeps) + D₂ ≡⟨ step-ii ⟩ + U₂ + getCoin certStateFinal + D₂ ∎ + where + + U₀ U₁ U₂ : Coin + U₀ = getCoin (UTxOStateOf s) + U₁ = getCoin us₁ + U₂ = getCoin us₂ + + D₀ D₂ : Coin + D₀ = coinFromDeposits (CertStateOf s) + D₂ = coinFromDeposits cs₂ + + R₀ R₂ : Coin + R₀ = rewardsBalance (DStateOf (CertStateOf s)) + R₂ = rewardsBalance (DStateOf cs₂) + + certStateFinal : CertState + certStateFinal = record cs₂ { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf cs₂) } + + allDirectDeps : Coin + allDirectDeps = getCoin (allDirectDeposits tx) + + subWdrlsCoin : Coin + subWdrlsCoin = sum (map wdrwl (SubTransactionsOf tx)) + + allWdrls : Coin + allWdrls = getCoin (WithdrawalsOf tx) + subWdrlsCoin + + extract-utxo-netId : ∀ {Γ' s₀' s₁'} → Γ' ⊢ s₀' ⇀⦇ tx ,UTXOW⦈ s₁' + → ∀[ a ∈ dom (WithdrawalsOf tx) ] NetworkIdOf a ≡ NetworkId + extract-utxo-netId + (UTXOW-normal-⋯ _ _ _ _ _ _ _ _ _ _ + (UTXO (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , netId , _))) = netId + extract-utxo-netId + (UTXOW-legacy-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ + (UTXO (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , netId , _))) = netId + + -- combined CERTS: rewardsBalance₀ = rewardsBalance₂ + allWdrls + combined-certs : getCoin (CertStateOf s) ≡ getCoin cs₂ + allWdrls + combined-certs = + begin + getCoin (CertStateOf s) ≡⟨ SUBLEDGERS-certs-pov valid subStep ⟩ + getCoin cs₁ + subWdrlsCoin ≡⟨ cong (_+ subWdrlsCoin) (CERTS-pov (extract-utxo-netId utxoStep) certStep) ⟩ + getCoin cs₂ + getCoin (WithdrawalsOf tx) + subWdrlsCoin ≡⟨ +-assoc (getCoin cs₂) _ subWdrlsCoin ⟩ + getCoin cs₂ + (getCoin (WithdrawalsOf tx) + subWdrlsCoin) ∎ + + + step-i : U₀ + R₀ + D₀ ≡ U₀ + R₂ + allWdrls + D₀ + step-i = + begin + U₀ + R₀ + D₀ ≡⟨ cong (λ x → U₀ + x + D₀ ) combined-certs ⟩ + U₀ + (R₂ + allWdrls) + D₀ ≡⟨ cong (_+ D₀) (sym (+-assoc U₀ R₂ allWdrls)) ⟩ + U₀ + R₂ + allWdrls + D₀ ∎ + + + -- applyDirectDeposits-rewardsBalance + step-ii : getCoin us₂ + (R₂ + allDirectDeps) + D₂ + ≡ getCoin us₂ + getCoin certStateFinal + D₂ + step-ii = cong (λ x → getCoin us₂ + x + D₂) + (sym (applyDirectDeposits-rewardsBalance (allDirectDeposits tx) (DStateOf cs₂))) + + + + -- Move the rightmost summand one position left (modulo re-assoc). + swap-right : ∀ a b c → a + b + c ≡ a + c + b + swap-right a b c = trans (+-assoc a b c) (trans (cong (a +_) (+-comm b c)) (sym (+-assoc a c b))) + + dc : DepositsChange + dc = calculateDepositsChange (CertStateOf s) cs₁ cs₂ + + dct dcs : ℤ + dct = DepositsChangeTopOf dc + dcs = DepositsChangeSubOf dc + + posneg : D₀ + posPart dct + posPart dcs ≡ D₂ + negPart dct + negPart dcs + posneg = posNeg-deposits (CertStateOf s) cs₁ cs₂ + + -- (MECH) UTXOW-V-mechanical, composed with the batch-wide invariants. + mech : U₁ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + ≡ U₂ + cbalance (UTxOOf (UTxOStateOf s) ∣ SpendInputsOf tx) + + mech = trans (UTXOW-V-mechanical utxoStep valid (fresh-top-tx-id valid subStep)) + (cong (U₂ +_) (utxo₁-tx-spend-eq valid refl subStep)) + + + arithmetic-1 : ∀ a b c d → a + b + c + d ≡ a + c + d + b + arithmetic-1 a b c d = begin + a + b + c + d ≡⟨ cong (_+ d) (+-assoc a b c) ⟩ + a + (b + c) + d ≡⟨ cong (λ x → a + x + d) (+-comm b c) ⟩ + a + (c + b) + d ≡⟨ cong (_+ d) (sym (+-assoc a c b)) ⟩ + a + c + b + d ≡⟨ +-assoc (a + c) b d ⟩ + a + c + (b + d) ≡⟨ cong ((a + c) +_) (+-comm b d) ⟩ + a + c + (d + b) ≡⟨ sym (+-assoc (a + c) d b) ⟩ + a + c + d + b ∎ + + arithmetic-2 : ∀ a b c d → a + b + c + d ≡ a + (d + b) + c + arithmetic-2 a b c d = begin + a + b + c + d ≡⟨ +-assoc (a + b) c d ⟩ + a + b + (c + d) ≡⟨ cong (a + b +_) (+-comm c d) ⟩ + a + b + (d + c) ≡⟨ sym (+-assoc (a + b) d c) ⟩ + a + b + d + c ≡⟨ cong (_+ c) (+-assoc a b d) ⟩ + a + (b + d) + c ≡⟨ cong (λ x → a + x + c) (+-comm b d) ⟩ + a + (d + b) + c ∎ + + + arithmetic-3 : ∀ a b c {d}{e}{f}{g} + → a + b + c + d + e + f + g ≡ a + e + b + (c + f + g) + d + arithmetic-3 a b c {d}{e}{f}{g} = begin + a + b + c + d + e + f + g ≡⟨ cong (λ x → x + f + g) (swap-right (a + b + c) d e) ⟩ + a + b + c + e + d + f + g ≡⟨ cong (_+ g) (swap-right (a + b + c + e) d f) ⟩ + a + b + c + e + f + d + g ≡⟨ swap-right (a + b + c + e + f) d g ⟩ + a + b + c + e + f + g + d ≡⟨ cong (λ x → x + f + g + d) (swap-right (a + b) c e) ⟩ + a + b + e + c + f + g + d ≡⟨ cong (λ x → x + c + f + g + d) (swap-right a b e) ⟩ + a + e + b + c + f + g + d ≡⟨ cong (_+ d) reassoc-middle ⟩ + (a + e) + b + (c + f + g) + d ∎ + where + reassoc-middle : a + e + b + c + f + g ≡ (a + e) + b + (c + f + g) + reassoc-middle = trans (+-assoc (a + e + b + c) f g) + (trans (+-assoc (a + e + b) c (f + g)) + (cong (a + e + b +_) (sym (+-assoc c f g)))) + + arithmetic-4 : ∀ a b c {d}{e}{f}{g} + → a + b + c + (d + e + f) + g ≡ a + (g + c + b + e + f) + d + arithmetic-4 a b c {d}{e}{f}{g} = begin + a + b + c + (d + e + f) + g ≡˘⟨ cong (_+ g) (+-assoc (a + b + c) (d + e) f) ⟩ + a + b + c + (d + e) + f + g ≡˘⟨ cong (λ x → x + f + g) (+-assoc (a + b + c) d e) ⟩ + a + b + c + d + e + f + g ≡⟨ swap-right (a + b + c + d + e) f g ⟩ + a + b + c + d + e + g + f ≡⟨ cong (_+ f) (swap-right (a + b + c + d) e g) ⟩ + a + b + c + d + g + e + f ≡⟨ cong (λ x → x + e + f) (swap-right (a + b + c) d g) ⟩ + a + b + c + g + d + e + f ≡⟨ cong (λ x → x + d + e + f) (swap-right (a + b) c g) ⟩ + a + b + g + c + d + e + f ≡⟨ cong (λ x → x + c + d + e + f) (swap-right a b g) ⟩ + a + g + b + c + d + e + f ≡⟨ cong (λ x → x + d + e + f) (swap-right (a + g) b c) ⟩ + a + g + c + b + d + e + f ≡⟨ cong (_+ f) (swap-right (a + g + c + b) d e) ⟩ + a + g + c + b + e + d + f ≡⟨ swap-right (a + g + c + b + e) d f ⟩ + a + g + c + b + e + f + d ≡⟨ cong (λ x → x + b + e + f + d) (+-assoc a g c) ⟩ + a + (g + c) + b + e + f + d ≡⟨ cong (λ x → x + e + f + d) (+-assoc a (g + c) b) ⟩ + a + (g + c + b) + e + f + d ≡⟨ cong (λ x → x + f + d) (+-assoc a (g + c + b) e) ⟩ + a + (g + c + b + e) + f + d ≡⟨ cong (_+ d) (+-assoc a (g + c + b + e) f) ⟩ + a + (g + c + b + e + f) + d ∎ + + arithmetic-5 : ∀ a b c {d}{e}{f}{g}{h}{i} + → a + (b + c + d + e + f + g + h) + i + ≡ a + b + c + d + e + f + g + h + i + arithmetic-5 a b c {d}{e}{f}{g}{h}{i} = cong (_+ i) $ + begin + a + (b + c + d + e + f + g + h) ≡˘⟨ +-assoc a _ h ⟩ + a + (b + c + d + e + f + g) + h ≡˘⟨ cong (_+ h) (+-assoc a _ g) ⟩ + a + (b + c + d + e + f) + g + h ≡˘⟨ cong (λ x → x + g + h) (+-assoc a _ f) ⟩ + a + (b + c + d + e) + f + g + h ≡˘⟨ cong (λ x → x + f + g + h) (+-assoc a _ e) ⟩ + a + (b + c + d) + e + f + g + h ≡˘⟨ cong (λ x → x + e + f + g + h) (+-assoc a _ d) ⟩ + a + (b + c) + d + e + f + g + h ≡˘⟨ cong (λ x → x + d + e + f + g + h) (+-assoc a b c) ⟩ + a + b + c + d + e + f + g + h ∎ + + arithmetic-6 : ∀ a b c {d}{e}{f}{g} + → a + b + c + d + e + f + g ≡ a + c + g + b + d + e + f + arithmetic-6 a b c {d}{e}{f}{g} = begin + a + b + c + d + e + f + g ≡⟨ cong (λ x → x + d + e + f + g) (swap-right a b c) ⟩ + a + c + b + d + e + f + g ≡⟨ swap-right (a + c + b + d + e) f g ⟩ + a + c + b + d + e + g + f ≡⟨ cong (_+ f) (swap-right (a + c + b + d) e g) ⟩ + a + c + b + d + g + e + f ≡⟨ cong (λ x → x + e + f) (swap-right (a + c + b) d g) ⟩ + a + c + b + g + d + e + f ≡⟨ cong (λ x → x + d + e + f) (swap-right (a + c) b g) ⟩ + a + c + g + b + d + e + f ∎ + + arithmetic-7 : ∀ a b c {d}{e}{f}{g} + → a + b + c + (d + e + f + g) ≡ a + b + c + d + e + f + g + arithmetic-7 a b c {d}{e}{f}{g} = begin + a + b + c + (d + e + f + g) ≡˘⟨ +-assoc (a + b + c) (d + e + f) g ⟩ + a + b + c + (d + e + f) + g ≡˘⟨ cong (_+ g) (+-assoc (a + b + c) (d + e) f) ⟩ + a + b + c + (d + e) + f + g ≡˘⟨ cong (λ x → x + f + g) (+-assoc (a + b + c) d e) ⟩ + a + b + c + d + e + f + g ∎ + + Ctop Csub : Coin + Ctop = cbalance (UTxOOf (UTxOStateOf s) ∣ SpendInputsOf tx) + Csub = sum (map (λ stx → cbalance (UTxOOf (UTxOStateOf s) ∣ SpendInputsOf stx)) (SubTransactionsOf tx)) + + Psub PsubDD : Coin + Psub = sum (map (λ stx → cbalance (outs stx) + DonationsOf stx) (SubTransactionsOf tx)) + PsubDD = sum (map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx)) + + -- === The additive constant ================================================= + E : Coin + E = Ctop + Psub + posPart dct + posPart dcs + + bat' : Ctop + allWdrls + Csub + negPart dct + negPart dcs + ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + + allDirectDeps + Psub + posPart dct + posPart dcs + bat' = + begin + Ctop + W + Csub + negPart dct + negPart dcs + ≡⟨⟩ + Ctop + (Wtop + Wsub) + Csub + negPart dct + negPart dcs + ≡⟨ cong (λ x → x + Csub + negPart dct + negPart dcs) (sym (+-assoc Ctop Wtop Wsub)) ⟩ + Ctop + Wtop + Wsub + Csub + negPart dct + negPart dcs + ≡⟨ cong (λ x → x + negPart dct + negPart dcs) (swap-right (Ctop + Wtop) Wsub Csub) ⟩ + Ctop + Wtop + Csub + Wsub + negPart dct + negPart dcs + ≡⟨ cong (λ x → x + negPart dct + negPart dcs) (+-assoc (Ctop + Wtop) Csub Wsub) ⟩ + Ctop + Wtop + (Csub + Wsub) + negPart dct + negPart dcs + ≡˘⟨ cong (λ x → Ctop + Wtop + x + negPart dct + negPart dcs) + (sum-map-+ (λ stx → cbalance (UTxOOf s ∣ SpendInputsOf stx)) + wdrwl (SubTransactionsOf tx)) ⟩ + Ctop + Wtop + CsubW + negPart dct + negPart dcs + ≡⟨ cong (_+ negPart dcs) (swap-right (Ctop + Wtop) CsubW (negPart dct)) ⟩ + Ctop + Wtop + negPart dct + CsubW + negPart dcs + ≡⟨ UTXOW-batch-balance-coin utxoStep ⟩ + O + F + DN + DDtop + posPart dct + PsubDD + (posPart dcs) + ≡⟨ cong (λ x → O + F + DN + DDtop + posPart dct + x + posPart dcs) + (sum-map-+ (λ stx → cbalance (outs stx) + DonationsOf stx) + (λ stx → getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx)) ⟩ + O + F + DN + DDtop + posPart dct + (Psub + DDsub) + posPart dcs + ≡⟨ reshuffle-to-DD ⟩ + O + F + DN + (DDtop + DDsub) + Psub + posPart dct + posPart dcs + ≡⟨ cong (λ x → O + F + DN + x + Psub + posPart dct + posPart dcs) (sym DD-split) ⟩ + O + F + DN + DD + Psub + posPart dct + posPart dcs + ∎ + where + O = cbalance (outs tx) + F = TxFeesOf tx + DN = DonationsOf tx + DD = allDirectDeps + DDtop = getCoin (DirectDepositsOf tx) + DDsub = sum (map (λ stx → getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx)) + W = allWdrls + Wtop = getCoin (WithdrawalsOf tx) + Wsub = sum (map wdrwl (SubTransactionsOf tx)) + CsubW = sum (map (λ stx → cbalance (UTxOOf s ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx)) + reshuffle-to-DD : O + F + DN + DDtop + posPart dct + (Psub + DDsub) + posPart dcs + ≡ O + F + DN + (DDtop + DDsub) + Psub + posPart dct + posPart dcs + reshuffle-to-DD = begin + O + F + DN + DDtop + (posPart dct) + (Psub + DDsub) + (posPart dcs) + ≡⟨ cong (_+ (posPart dcs)) (sym (+-assoc (O + F + DN + DDtop + (posPart dct)) Psub DDsub)) ⟩ + O + F + DN + DDtop + (posPart dct) + Psub + DDsub + (posPart dcs) + ≡⟨ cong (_+ (posPart dcs)) (swap-right (O + F + DN + DDtop + (posPart dct)) Psub DDsub) ⟩ + O + F + DN + DDtop + (posPart dct) + DDsub + Psub + (posPart dcs) + ≡⟨ cong (λ x → x + Psub + (posPart dcs)) (swap-right (O + F + DN + DDtop) (posPart dct) DDsub) ⟩ + O + F + DN + DDtop + DDsub + (posPart dct) + Psub + (posPart dcs) + ≡⟨ cong (_+ (posPart dcs)) (swap-right (O + F + DN + DDtop + DDsub) (posPart dct) Psub) ⟩ + O + F + DN + DDtop + DDsub + Psub + (posPart dct) + (posPart dcs) + ≡⟨ cong (λ x → x + Psub + (posPart dct) + (posPart dcs)) (+-assoc (O + F + DN) DDtop DDsub) ⟩ + O + F + DN + (DDtop + DDsub) + Psub + (posPart dct) + (posPart dcs) + ∎ + + -- === Main chain ============================================================ + LHS+E≡RHS+E : (U₀ + allWdrls + D₀) + E ≡ (U₂ + allDirectDeps + D₂) + E + LHS+E≡RHS+E = begin + U₀ + allWdrls + D₀ + E + ≡⟨ refl ⟩ + U₀ + allWdrls + D₀ + (Ctop + Psub + posPart dct + posPart dcs) + ≡⟨ arithmetic-7 U₀ allWdrls D₀ ⟩ + U₀ + allWdrls + D₀ + Ctop + Psub + posPart dct + posPart dcs + ≡⟨ arithmetic-3 U₀ allWdrls D₀ ⟩ + U₀ + Psub + allWdrls + (D₀ + posPart dct + posPart dcs) + Ctop + ≡⟨ cong (λ x → x + allWdrls + (D₀ + posPart dct + posPart dcs) + Ctop) + (subst (λ u → U₀ + Psub ≡ U₁ + sum (map (λ stx → cbalance (u ∣ SpendInputsOf stx)) (SubTransactionsOf tx))) + (refl {x = UTxOOf s}) (SUBLEDGERS-utxo-coin valid subStep)) ⟩ + U₁ + Csub + allWdrls + (D₀ + posPart dct + posPart dcs) + Ctop + ≡⟨ cong (λ x → (U₁ + Csub) + allWdrls + x + Ctop) posneg ⟩ + U₁ + Csub + allWdrls + (D₂ + negPart dct + negPart dcs) + Ctop + ≡⟨ arithmetic-4 U₁ Csub allWdrls ⟩ + U₁ + (Ctop + allWdrls + Csub + negPart dct + negPart dcs) + D₂ + ≡⟨ cong (λ x → U₁ + x + D₂) bat' ⟩ + U₁ + (cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + allDirectDeps + Psub + posPart dct + posPart dcs) + D₂ + ≡⟨ arithmetic-5 U₁ (cbalance (outs tx)) (TxFeesOf tx) ⟩ + U₁ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + allDirectDeps + Psub + posPart dct + posPart dcs + D₂ + ≡⟨ cong (λ x → x + allDirectDeps + Psub + posPart dct + posPart dcs + D₂) mech ⟩ + U₂ + Ctop + allDirectDeps + Psub + posPart dct + posPart dcs + D₂ + ≡⟨ arithmetic-6 U₂ Ctop allDirectDeps ⟩ + U₂ + allDirectDeps + D₂ + Ctop + Psub + posPart dct + posPart dcs + ≡˘⟨ arithmetic-7 U₂ allDirectDeps D₂ ⟩ + U₂ + allDirectDeps + D₂ + E + ∎ + + -- deposit accounting + batch UTxO combined + step-iii-iv : U₀ + allWdrls + D₀ + R₂ ≡ U₂ + allDirectDeps + D₂ + R₂ + step-iii-iv = cong (_+ R₂) + (+-cancelʳ-≡ E (U₀ + allWdrls + D₀) (U₂ + allDirectDeps + D₂) LHS+E≡RHS+E) +``` diff --git a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md index 13e5b665ec..a56476ff80 100644 --- a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md @@ -141,6 +141,14 @@ record HasDepositsChange {a} (A : Type a) : Type a where field DepositsChangeOf : A → DepositsChange open HasDepositsChange ⦃...⦄ public +record HasDepositsChangeTop {a} (A : Type a) : Type a where + field DepositsChangeTopOf : A → ℤ +open HasDepositsChangeTop ⦃...⦄ public + +record HasDepositsChangeSub {a} (A : Type a) : Type a where + field DepositsChangeSubOf : A → ℤ +open HasDepositsChangeSub ⦃...⦄ public + record HasScriptPool {a} (A : Type a) : Type a where field ScriptPoolOf : A → ℙ Script open HasScriptPool ⦃...⦄ public @@ -209,6 +217,18 @@ instance HasDonations-UTxOState : HasDonations UTxOState HasDonations-UTxOState .DonationsOf = UTxOState.donations + HasDepositsChangeTop-DepositsChange : HasDepositsChangeTop DepositsChange + HasDepositsChangeTop-DepositsChange .DepositsChangeTopOf = DepositsChange.depositsChangeTop + + HasDepositsChangeSub-DepositsChange : HasDepositsChangeSub DepositsChange + HasDepositsChangeSub-DepositsChange .DepositsChangeSubOf = DepositsChange.depositsChangeSub + + HasDepositsChangeTop-UTxOEnv : HasDepositsChangeTop UTxOEnv + HasDepositsChangeTop-UTxOEnv .DepositsChangeTopOf = DepositsChangeTopOf ∘ DepositsChangeOf + + HasDepositsChangeSub-UTxOEnv : HasDepositsChangeSub UTxOEnv + HasDepositsChangeSub-UTxOEnv .DepositsChangeSubOf = DepositsChangeSubOf ∘ DepositsChangeOf + unquoteDecl HasCast-DepositsChange HasCast-UTxOEnv HasCast-SubUTxOEnv @@ -256,6 +276,9 @@ minfee pp txTop utxo = pp .a * (SizeOf txTop) + pp .b instance HasCoin-UTxO : HasCoin UTxO HasCoin-UTxO .getCoin = cbalance + + HasCoin-UTxOState : HasCoin UTxOState + HasCoin-UTxOState .getCoin s = getCoin (UTxOOf s) + FeesOf s + DonationsOf s ``` --> @@ -300,6 +323,16 @@ collateralCheck pp txTop utxo = × coin (balance (utxo ∣ CollateralInputsOf txTop)) * 100 ≥ (TxFeesOf txTop) * pp .collateralPercentage × (CollateralInputsOf txTop) ≢ ∅ +producedTx : Tx ℓ → Value +producedTx tx = balance (outs tx) + + inject (DonationsOf tx) + + inject (getCoin (DirectDepositsOf tx)) + +consumedTx : Tx ℓ → UTxO → Value +consumedTx tx utxo = balance (utxo ∣ SpendInputsOf tx) + + MintedValueOf tx + + inject (getCoin (WithdrawalsOf tx)) + module _ (depositsChange : DepositsChange) where open DepositsChange depositsChange @@ -316,11 +349,6 @@ module _ (depositsChange : DepositsChange) where depositRefundsTop : Coin depositRefundsTop = negPart depositsChangeTop - consumedTx : Tx ℓ → UTxO → Value - consumedTx tx utxo = balance (utxo ∣ SpendInputsOf tx) - + MintedValueOf tx - + inject (getCoin (WithdrawalsOf tx)) - consumed : TopLevelTx → UTxO → Value consumed txTop utxo = consumedTx txTop utxo + inject depositRefundsTop @@ -337,11 +365,6 @@ In the preservation-of-value equation, direct deposits appear on the the transaction and that amount is deposited into accounts. ```agda - 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) @@ -506,7 +529,6 @@ data _⊢_⇀⦇_,SUBUTXO⦈_ : SubUTxOEnv → UTxOState → SubLevelTx → UTxO ∙ MaybeNetworkIdOf txSub ~ just NetworkId ∙ CurrentTreasuryOf txSub ~ just (TreasuryOf Γ) ∙ dom (DirectDepositsOf txSub) ⊆ dom (AccountBalancesOf Γ) - ∙ dom (BalanceIntervalsOf txSub) ⊆ dom (AccountBalancesOf Γ) ∙ ∀[ (c , interval) ∈ BalanceIntervalsOf txSub ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? (AccountBalancesOf Γ) c)) interval) ──────────────────────────────── diff --git a/src/Ledger/Dijkstra/Specification/Utxo/Properties.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo/Properties.lagda.md index 456772f9b4..7ad771cd3b 100644 --- a/src/Ledger/Dijkstra/Specification/Utxo/Properties.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxo/Properties.lagda.md @@ -14,4 +14,6 @@ module Ledger.Dijkstra.Specification.Utxo.Properties where ```agda open import Ledger.Dijkstra.Specification.Utxo.Properties.Computational +open import Ledger.Dijkstra.Specification.Utxo.Properties.Base +open import Ledger.Dijkstra.Specification.Utxo.Properties.PoV ``` diff --git a/src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md new file mode 100644 index 0000000000..3cf9371b48 --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md @@ -0,0 +1,96 @@ +--- +source_branch: 1123-cip-159-11-prove-pov-and-invariants +source_path: src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md +--- + +# UTXO Properties: Base lemmas (Dijkstra era) + +This module collects era-independent helper lemmas used by +`Utxo.Properties.PoV`{.AgdaModule}. It currently contains: + ++ `∙-homo-Coin`{.AgdaFunction}: the `coin` monoid-homomorphism's `_∙_` property. ++ `newTxid⇒disj`{.AgdaFunction}: freshness of `TxIdOf tx` in an existing + `utxo` implies `disjoint'`{.AgdaFunction} of `dom utxo`{.AgdaFunction} and + `dom (outs tx)`{.AgdaFunction}. ++ `outs-disjoint`{.AgdaFunction}: the specialisation used by + `Utxo.Properties.PoV`{.AgdaModule}. + +**Not yet ported from Conway**: the `balance`{.AgdaFunction}-arithmetic lemmas +(`balance-cong`{.AgdaFunction}, `balance-cong-coin`{.AgdaFunction}, +`balance-∪`{.AgdaFunction}, `split-balance`{.AgdaFunction}). Conway's versions +rely on `indexedSumᵐ-cong`{.AgdaFunction} over a finite map of hashed TxOuts; +Dijkstra's `balance`{.AgdaFunction} is defined as `∑ˢ[ v ← valuesOfUTxO utxo ] v` +(a sum over a `ℙ Value`{.AgdaFunction}), so the Conway proofs don't apply +verbatim. Porting them requires the set-theoretic cong lemmas from +`abstract-set-theory.FiniteSetTheory`{.AgdaModule}; for now, `balance-∪`{.AgdaFunction} +and `split-balance`{.AgdaFunction} remain as module parameters to +`Utxo.Properties.PoV`{.AgdaModule}. + + + +## `∙-homo-Coin` + +```agda +∙-homo-Coin : ∀ (x y : Value) → coin (x + y) ≡ coin x + coin y +∙-homo-Coin = IsMagmaHomomorphism.homo (isMagmaHomomorphism coinIsMonoidHomomorphism) +``` + +## `coin-∑ˡ` + +`coin`{.AgdaField} is a monoid homomorphism from `Value`{.AgdaField} (under `+ᵛ`/`ε`) to +`ℕ`{.AgdaDatatype} (under `+`/`0`), so it distributes over a list-indexed sum. This +is the "coin version" of the generic fact that a monoid homomorphism commutes with +`foldr _∙_ ε`. + +```agda +coin-∑ˡ : ∀ {A : Type} (f : A → Value) (xs : List A) + → coin (∑ˡ[ x ← xs ] f x) ≡ sum (map (coin ∘ f) xs) +coin-∑ˡ f [] = ε-homo coinIsMonoidHomomorphism +coin-∑ˡ f (x ∷ xs) = trans (∙-homo-Coin (f x) (∑ˡ[ z ← xs ] f z)) + (cong (coin (f x) +_) (coin-∑ˡ f xs)) +``` + + +## Freshness ⇒ disjointness + +```agda +module _ (tx : Tx ℓ) (let open Tx tx; open TxBody txBody) + {utxo : UTxO} where + + newTxid⇒disj : TxIdOf tx ∉ mapˢ proj₁ (dom utxo) + → disjoint' (dom utxo) (dom (outs tx)) + newTxid⇒disj id∉utxo = + disjoint⇒disjoint' λ h h' → id∉utxo $ to ∈-map + (-, (case from ∈-map h' of λ where + (_ , refl , h'') → case from ∈-map h'' of λ where (_ , refl , _) → refl) , h) + + -- Specialisation used by Utxo.Properties.PoV: + -- freshness ⇒ (utxo ∣ SpendInputs ᶜ) and outs are disjoint. + outs-disjoint : TxIdOf tx ∉ mapˢ proj₁ (dom utxo) + → disjoint (dom (utxo ∣ SpendInputsOf tx ᶜ)) (dom (outs tx)) + outs-disjoint fresh = + λ h₁ h₂ → ∉-∅ $ proj₁ (newTxid⇒disj fresh) $ to ∈-∩ (res-comp-domᵐ h₁ , h₂) +``` diff --git a/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md new file mode 100644 index 0000000000..35626c889f --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md @@ -0,0 +1,639 @@ +--- +source_branch: master +source_path: src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md +--- + +# UTXO: Preservation of Value {#sec:utxo-pov} + +This module states the preservation-of-value property for the Dijkstra +`UTXO`{.AgdaDatatype} rule, updated for CIP-159 (direct deposits and +partial withdrawals). + +## Key Differences from Conway + +1. `UTxOState`{.AgdaRecord} has 3 fields (`utxo`, `fees`, `donations`) in Dijkstra — deposits + live in `CertState`, not `UTxOState`. So + + `getCoin utxoSt = cbalance utxo + fees + donations` (no `getCoin deposits` term). + +2. **Balance equation is batch-wide** (`consumedBatch ≡ producedBatch`) rather + than per-transaction. It is a *conjunct* in `UTXO-Premises` (premise `p₇`), + not a standalone `newBal` premise. + +3. **Withdrawals appear on the consumed side** (as in Conway) *for every + transaction in the batch* (top + each sub-tx), not just the top-level tx. + CIP-159 allows partial withdrawals; the withdrawn amount is the value + specified in the transaction (≤ pre-batch balance, by phantom asset + prevention). + +4. **Direct deposits appear on the produced side** (new to CIP-159), both at + the top level and in sub-transactions. These represent value leaving the + UTxO world and entering account balances. They *cancel* in the full + LEDGER-pov equation against the `applyDirectDeposits` step applied to + `CertState`. + +5. `UTXOS`{.AgdaDatatype} is trivial (`⊤ → ⊤`): only checks script evaluation, does not + modify state. All state updates happen in `UTXO-V`/`UTXO-I` directly. + +## Proof Architecture + +The Dijkstra `UTXO-pov`{.AgdaFunction} is split into two orthogonal pieces: + ++ **Mechanical state change** (`UTXO-I-getCoin`{.AgdaFunction}, + `UTXO-V-mechanical`{.AgdaFunction}): How `getCoin s₀` relates to + `getCoin s₁` purely in terms of the `UTxOState` state transition, + without using the batch balance equation. + ++ **Batch coin balance** (`batch-balance-coin`{.AgdaFunction}): The coin + projection of the batch balance equation `consumedBatch ≡ producedBatch`. + This is a *pure* equation about `tx`, the pre-batch UTxO snapshot + `utxo₀ = UTxOOf Γ`, and the `DepositsChange` — it does not mention + `s₀` or `s₁`. + +The combined `UTXO-pov`{.AgdaFunction} theorem uses both pieces to express the +value preservation equation that the `LEDGER-pov`{.AgdaFunction} proof needs. + +Note that, unlike in Conway, the mechanical state change alone (for the valid +case) does not suffice to prove a local "before/after" equation, because + ++ `utxoSt₀` passed to the `UTXO`{.AgdaDatatype} rule at the `LEDGER` level is + the *post-SUBLEDGERS* state, not the pre-batch state, so, in general, + + `UTxOOf utxoSt₀ ≢ UTxOOf Γ` + ++ the batch balance equation relates `UTxOOf Γ` (the pre-batch snapshot) to + quantities summed over the *entire batch*, not just the top-level tx. + +Consequently, deriving a full value-preservation statement for the UTXO rule +alone requires threading through information about the preceding SUBLEDGERS +step — work that is done in `LEDGER-pov`{.AgdaFunction}, not here. + + + +## Preliminaries + +We record the `HasCoin`{.AgdaRecord} instance for `UTxOState`{.AgdaRecord} for +easy reference. Note, in Dijkstra `UTxOState`{.AgdaRecord} has only three fields. +Also, for `s : UTxOState`, + +`getCoin s = cbalance (UTxOOf s) + FeesOf s + DonationsOf s` + +We introduce module-level parameters encapsulating the UTxO arithmetic lemmas that +are used in Conway's analogous proofs. They need to be ported to the Dijkstra era (they live in +`Ledger.Conway.Specification.Utxo.Properties.Base`{.AgdaModule}) but are +orthogonal to the CIP-159 content of this issue, so we take them as assumptions +here. + +```agda +-- ============================================================================= +-- Coin projections of consumedBatch and producedBatch. +-- ============================================================================= +-- +-- These proofs live inside the parameterised `module _ (tx : TopLevelTx) ...` +-- block of `Utxo/Properties/PoV.lagda.md`, alongside the existing +-- `UTXO-I-getCoin` / `UTXO-V-mechanical` / `batch-balance-coin` definitions. +-- +-- They replace the `coin-of-consumedBatch` and `coin-of-producedBatch` module +-- parameters. +-- +-- The presentation assumes `coin-∑ˡ` is available from `Utxo.Properties.Base`; +-- `coin-producedTx` is as William has already proved it. +-- +-- Imports needed (add to the main `open import` block at the top of the file): +-- +-- open import Ledger.Dijkstra.Specification.Utxo.Properties.Base txs abs +-- using (∙-homo-Coin; outs-disjoint; coin-∑ˡ) +-- +-- ============================================================================= + + +-- ----------------------------------------------------------------------------- +-- Layer 1: single-transaction coin equations. +-- ----------------------------------------------------------------------------- +coin-producedTx : (tx : Tx ℓ) → coin (producedTx tx) ≡ cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) +coin-producedTx tx = begin + coin (producedTx tx) + ≡⟨ refl ⟩ + coin(balance (outs tx) + inject (DonationsOf tx) + inject (getCoin (DirectDepositsOf tx))) + ≡⟨ ∙-homo-Coin (balance (outs tx) + inject (DonationsOf tx)) (inject (getCoin (DirectDepositsOf tx))) ⟩ + coin(balance (outs tx) + inject (DonationsOf tx)) + coin(inject (getCoin (DirectDepositsOf tx))) + ≡⟨ cong (coin(balance (outs tx) + inject (DonationsOf tx)) +_) (coin∘inject≗id (getCoin (DirectDepositsOf tx))) ⟩ + coin(balance (outs tx) + inject (DonationsOf tx)) + getCoin (DirectDepositsOf tx) + ≡⟨ cong (_+ getCoin (DirectDepositsOf tx)) (∙-homo-Coin (balance (outs tx)) (inject (DonationsOf tx))) ⟩ + coin(balance (outs tx)) + coin(inject (DonationsOf tx)) + getCoin (DirectDepositsOf tx) + ≡⟨ cong (λ x → coin(balance (outs tx)) + x + getCoin (DirectDepositsOf tx)) (coin∘inject≗id (DonationsOf tx)) ⟩ + cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) + ∎ + where open ≡-Reasoning + + +coin-consumedTx : (tx : Tx ℓ) (utxo₀ : UTxO) → coin (MintedValueOf tx) ≡ 0 + → coin (consumedTx tx utxo₀) ≡ cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) +coin-consumedTx tx utxo₀ noMint = + let b₀ = balance (utxo₀ ∣ SpendInputsOf tx) in + begin + coin (consumedTx tx utxo₀) + ≡⟨ refl ⟩ + coin (b₀ + MintedValueOf tx + inject (getCoin (WithdrawalsOf tx))) + ≡⟨ ∙-homo-Coin (b₀ + MintedValueOf tx) (inject (getCoin (WithdrawalsOf tx))) ⟩ + coin (b₀ + MintedValueOf tx) + coin (inject (getCoin (WithdrawalsOf tx))) + ≡⟨ cong (coin (b₀ + MintedValueOf tx) +_) (coin∘inject≗id (getCoin (WithdrawalsOf tx))) ⟩ + coin (b₀ + MintedValueOf tx) + getCoin (WithdrawalsOf tx) + ≡⟨ cong (_+ getCoin (WithdrawalsOf tx)) (∙-homo-Coin (b₀) (MintedValueOf tx)) ⟩ + coin b₀ + coin (MintedValueOf tx) + getCoin (WithdrawalsOf tx) + ≡⟨ cong (λ z → cbalance (utxo₀ ∣ SpendInputsOf tx) + z + getCoin (WithdrawalsOf tx)) noMint ⟩ + cbalance (utxo₀ ∣ SpendInputsOf tx) + 0 + getCoin (WithdrawalsOf tx) + ≡⟨ cong (_+ getCoin (WithdrawalsOf tx)) (+-identityʳ (cbalance (utxo₀ ∣ SpendInputsOf tx))) ⟩ + cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + ∎ + where open ≡-Reasoning + + +-- ----------------------------------------------------------------------------- +-- Layer 2: sum-over-sub-transactions coin equations. +-- ----------------------------------------------------------------------------- +-- +-- We use `coin-∑ˡ` to push `coin` through the indexed sum, then rewrite each +-- summand pointwise using Layer 1. For the consumed-side version we also +-- thread a per-element `noMintSub` premise. + +coin-∑-producedTx-sub : (tx : TopLevelTx) → + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx)) + ≡ sum ( map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx) ) +coin-∑-producedTx-sub tx = begin + coin (∑ˡ[ stx ← SubTransactionsOf tx ] producedTx stx) + ≡⟨ coin-∑ˡ producedTx (SubTransactionsOf tx) ⟩ + sum (map (coin ∘ producedTx) (SubTransactionsOf tx)) + ≡⟨ sum-cong-rewrite (SubTransactionsOf tx) ⟩ + sum (map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx)) + ∎ + where + open ≡-Reasoning + -- Pointwise rewrite of the mapped list, by list induction. + sum-cong-rewrite : (xs : List SubLevelTx) + → sum (map (coin ∘ producedTx) xs) + ≡ sum (map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) xs) + sum-cong-rewrite [] = refl + sum-cong-rewrite (stx ∷ xs) = cong₂ _+_ (coin-producedTx stx) (sum-cong-rewrite xs) + + +noMintingSubTxs : TopLevelTx → Type +noMintingSubTxs tx = ∀ stx → stx ∈ˡ SubTransactionsOf tx → coin (MintedValueOf stx) ≡ 0 + +coin-∑-consumedTx-sub : (tx : TopLevelTx) (utxo₀ : UTxO) + → noMintingSubTxs tx + → coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + ≡ sum (map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx)) +coin-∑-consumedTx-sub tx utxo₀ noMintSub = begin + coin (∑ˡ[ stx ← SubTransactionsOf tx ] consumedTx stx utxo₀) + ≡⟨ coin-∑ˡ (λ stx → consumedTx stx utxo₀) (SubTransactionsOf tx) ⟩ + sum (map (coin ∘ λ stx → consumedTx stx utxo₀) (SubTransactionsOf tx)) + ≡⟨ go (SubTransactionsOf tx) (λ _ → id) ⟩ + sum (map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + + getCoin (WithdrawalsOf stx)) + (SubTransactionsOf tx)) + ∎ + where + open ≡-Reasoning + -- Pointwise rewrite: the `mem` argument lets each element's + -- `noMintSub` lookup go through. + go : (xs : List SubLevelTx) + → (∀ stx → stx ∈ˡ xs → stx ∈ˡ SubTransactionsOf tx) + → sum (map (coin ∘ λ stx → consumedTx stx utxo₀) xs) + ≡ sum (map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + + getCoin (WithdrawalsOf stx)) xs) + go [] _ = refl + go (stx ∷ xs) mem = + cong₂ _+_ + (coin-consumedTx stx utxo₀ (noMintSub stx (mem stx (here refl)))) + (go xs (λ stx' stx'∈ → mem stx' (there stx'∈))) + + +-- ----------------------------------------------------------------------------- +-- Layer 3: the two batch-level coin equations. +-- ----------------------------------------------------------------------------- +-- +-- `consumedBatch` and `producedBatch` each wrap their per-tx summands with +-- additional `inject`-ed fields (top-level fees + per-side deposit terms), so +-- we peel those off with `∙-homo-Coin` + `coin∘inject≗id`, then substitute the +-- Layer-1 top-level and Layer-2 sub-level equations. +-- +-- Each proof ends with a small `+`-commutative-monoid shuffle to match the +-- field order in the stated theorem. +coin-of-consumedBatch : (tx : TopLevelTx) (dc : DepositsChange) (utxo₀ : UTxO) + → coin (MintedValueOf tx) ≡ 0 → noMintingSubTxs tx + → coin (consumedBatch dc tx utxo₀) + ≡ cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf dc) + + sum ( map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) + (SubTransactionsOf tx) ) + + negPart (DepositsChangeSubOf dc) +coin-of-consumedBatch tx dc utxo₀ noMintTop noMintSub = begin + -- consumedBatch dc tx utxo₀ = consumed dc tx utxo₀ + ∑ˡ[ stx ← subs ] (consumedTx stx utxo₀) + inject depositRefundsSub + -- where consumed dc tx utxo₀ = consumedTx tx utxo₀ + inject depositRefundsTop + coin ( consumedTx tx utxo₀ + inject (negPart (DepositsChangeTopOf dc)) + + ∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀) + inject (negPart (DepositsChangeSubOf dc)) ) + + ≡⟨ ∙-homo-Coin _ _ ⟩ -- Peel the outer `+ inject depositRefundsSub`. + coin ( consumedTx tx utxo₀ + inject (negPart (DepositsChangeTopOf dc)) + + ∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀) ) + + coin (inject (negPart (DepositsChangeSubOf dc))) + + ≡⟨ cong₂ _+_ (∙-homo-Coin _ _) (coin∘inject≗id _) ⟩ + coin (consumedTx tx utxo₀ + inject (negPart (DepositsChangeTopOf dc))) + + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + negPart (DepositsChangeSubOf dc) + + -- Peel `consumedTx tx utxo₀ + inject depositRefundsTop`. + ≡⟨ cong (λ z → z + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + + negPart (DepositsChangeSubOf dc)) + (trans (∙-homo-Coin _ _) (cong (coin (consumedTx tx utxo₀) +_) (coin∘inject≗id _))) ⟩ + coin (consumedTx tx utxo₀) + negPart (DepositsChangeTopOf dc) + + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + negPart (DepositsChangeSubOf dc) + + -- Substitute Layer-1 top-level. + ≡⟨ cong (λ z → z + negPart (DepositsChangeTopOf dc) + + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + + negPart (DepositsChangeSubOf dc)) + (coin-consumedTx tx utxo₀ noMintTop) ⟩ + cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf dc) + + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + negPart (DepositsChangeSubOf dc) + + -- Substitute Layer-2 sub-level. + ≡⟨ cong (λ z → (cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx)) + + negPart (DepositsChangeTopOf dc) + z + negPart (DepositsChangeSubOf dc)) + (coin-∑-consumedTx-sub tx utxo₀ noMintSub) ⟩ + cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf dc) + + sum (map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx)) + + negPart (DepositsChangeSubOf dc) + + -- Re-associate the outer `+` to match the stated theorem. + ≡⟨ cong (λ z → z + negPart (DepositsChangeTopOf dc) + + sum ( map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) + (SubTransactionsOf tx) ) + + negPart (DepositsChangeSubOf dc)) refl ⟩ + -- The term now matches the target statement exactly. + cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf dc) + + sum (map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx)) + + negPart (DepositsChangeSubOf dc) + ∎ + where open ≡-Reasoning + + +coin-of-producedBatch : (tx : TopLevelTx) (dc : DepositsChange) + → coin (producedBatch dc tx) + ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + + posPart (DepositsChangeTopOf dc) + + sum ( map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx) ) + + posPart (DepositsChangeSubOf dc) +coin-of-producedBatch tx dc = begin + -- producedBatch dc tx = produced dc tx + ∑ˡ[ stx ← subs ] (producedTx stx) + inject newDepositsSub + -- where produced dc tx = producedTx tx + inject txFee + inject newDepositsTop + coin (producedTx tx + inject (TxFeesOf tx) + inject (posPart (DepositsChangeTopOf dc)) + + ∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx) + inject (posPart (DepositsChangeSubOf dc))) + + -- Peel the outer `+ inject newDepositsSub`. + ≡⟨ ∙-homo-Coin _ _ ⟩ + coin (producedTx tx + inject (TxFeesOf tx) + inject (posPart (DepositsChangeTopOf dc)) + + ∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx)) + coin (inject (posPart (DepositsChangeSubOf dc))) + ≡⟨ cong₂ _+_ (∙-homo-Coin _ _) (coin∘inject≗id _) ⟩ + coin (producedTx tx + inject (TxFeesOf tx) + inject (posPart (DepositsChangeTopOf dc))) + + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx)) + posPart (DepositsChangeSubOf dc) + -- Unfold the top-level three layers (outs+donations+directDeps, fee, deposits). + ≡⟨ cong (λ z → z + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx)) + posPart (DepositsChangeSubOf dc)) + unfold-produced-top ⟩ + cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) + + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx)) + + posPart (DepositsChangeSubOf dc) + -- Substitute Layer-2 sub-level. + ≡⟨ cong (λ z → (cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx)) + + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + z + posPart (DepositsChangeSubOf dc)) + (coin-∑-producedTx-sub tx) ⟩ + cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) + + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + + sum ( map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx) ) + + posPart (DepositsChangeSubOf dc) + -- Reshuffle top-level fields: (outs + Donations + DirectDeps) + TxFees + -- → outs + TxFees + Donations + DirectDeps + ≡⟨ cong (λ z → z + posPart (DepositsChangeTopOf dc) + + sum ( map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx) ) + + posPart (DepositsChangeSubOf dc)) reshape-top ⟩ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + posPart (DepositsChangeTopOf dc) + + sum (map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx)) + + posPart (DepositsChangeSubOf dc) + ∎ + where + open ≡-Reasoning + + -- Unfolds `coin (producedTx tx + inject TxFees + inject newDepositsTop)` by + -- two peels of `∙-homo-Coin` / `coin∘inject≗id` and one application of + -- `coin-producedTx`. + unfold-produced-top : + coin (producedTx tx + inject (TxFeesOf tx) + inject (posPart (DepositsChangeTopOf dc))) + ≡ (cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx)) + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + + unfold-produced-top = begin + coin (producedTx tx + inject (TxFeesOf tx) + inject (posPart (DepositsChangeTopOf dc))) + ≡⟨ ∙-homo-Coin _ _ ⟩ + coin (producedTx tx + inject (TxFeesOf tx)) + coin (inject (posPart (DepositsChangeTopOf dc))) + ≡⟨ cong₂ _+_ (∙-homo-Coin _ _) (coin∘inject≗id _) ⟩ + coin (producedTx tx) + coin (inject (TxFeesOf tx)) + posPart (DepositsChangeTopOf dc) + ≡⟨ cong (λ z → coin (producedTx tx) + z + posPart (DepositsChangeTopOf dc)) (coin∘inject≗id _) ⟩ + coin (producedTx tx) + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + ≡⟨ cong (λ z → z + TxFeesOf tx + posPart (DepositsChangeTopOf dc)) (coin-producedTx tx) ⟩ + cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + ∎ + + -- Small rearrangement: move TxFees from rightmost position to second. + -- (O + D + R) + F ≡ O + F + D + R + -- (where O = cbalance (outs tx), D = DonationsOf tx, + -- R = getCoin (DirectDepositsOf tx), F = TxFeesOf tx). + -- Proved by the `swap-right` pattern used in `UTXO-V-mechanical`. + reshape-top : cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) + TxFeesOf tx + ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + reshape-top = + let O = cbalance (outs tx) + D = DonationsOf tx + R = getCoin (DirectDepositsOf tx) + F = TxFeesOf tx + in begin + (O + D + R) + F ≡⟨ swap-right (O + D) R F ⟩ + (O + D) + F + R ≡⟨ cong (_+ R) (swap-right O D F) ⟩ + O + F + D + R ∎ + where + -- Same `swap-right` helper as in `UTXO-V-mechanical`. + swap-right : ∀ a b c → a + b + c ≡ a + c + b + swap-right a b c = trans (+-assoc a b c) (trans (cong (a +_) (+-comm b c)) (sym (+-assoc a c b))) + + +module UTxO-PoV + (tx : TopLevelTx) (let open Tx tx; open TxBody txBody) + + -- ASSUMPTIONS -- + ( balance-∪ : ∀ {u u' : UTxO} → disjoint (dom u) (dom u') → cbalance (u ∪ˡ u') ≡ cbalance u + cbalance u' ) + ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn) → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) ) + ( noMintTx : coin (MintedValueOf tx) ≡ 0 ) + ( noMintSubTx : noMintingSubTxs tx ) + where + + private variable + Γ : UTxOEnv + legacyMode : Bool + s s' s₀ s₁ : UTxOState + + open ≡-Reasoning +``` + + +## `UTXO-I`: collateral collection preserves `getCoin` + +The invalid case does not use the batch balance equation: it only collects +collateral from the top-level transaction and leaves `donations` unchanged. + +```agda + UTXO-I-getCoin : + (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁ → IsValidFlagOf tx ≡ false → getCoin s₀ ≡ getCoin s₁ + + UTXO-I-getCoin {s₀ = ⟦ u , f , d ⟧ᵘ} (UTXO-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) refl = + begin + cbalance u + f + d + ≡⟨ cong (λ x → x + f + d) (split-balance u (CollateralInputsOf tx)) ⟩ + cbalance (u ∣ CollateralInputsOf tx ᶜ) + cbalance (u ∣ CollateralInputsOf tx) + f + d + ≡⟨ cong (_+ d) (+-assoc (cbalance (u ∣ CollateralInputsOf tx ᶜ)) + (cbalance (u ∣ CollateralInputsOf tx)) f) ⟩ + cbalance (u ∣ CollateralInputsOf tx ᶜ) + (cbalance (u ∣ CollateralInputsOf tx) + f) + d + ≡⟨ cong (λ x → (cbalance (u ∣ CollateralInputsOf tx ᶜ)) + x + d) + (+-comm (cbalance (u ∣ CollateralInputsOf tx)) f) ⟩ + cbalance (u ∣ CollateralInputsOf tx ᶜ) + (f + cbalance (u ∣ CollateralInputsOf tx)) + d + ∎ +``` + + +## `UTXO-V`: mechanical rearrangement + +```agda + UTXO-V-mechanical : (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁ + → IsValidFlagOf tx ≡ true → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s₀)) + → getCoin s₀ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + ≡ getCoin s₁ + cbalance (UTxOOf s₀ ∣ SpendInputsOf tx) + + UTXO-V-mechanical {s₀ = ⟦ u , f , d ⟧ᵘ} {s₁ = ⟦ u' , f' , d' ⟧ᵘ} + (UTXO-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h) refl freshId = + begin + cbalance u + f + d + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + + ≡⟨ i ⟩ cbalance (u ∣ SpendInputsOf tx ᶜ) + cbalance (u ∣ SpendInputsOf tx) + f + d + + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + + ≡⟨ ii ⟩ cbalance (u ∣ SpendInputsOf tx ᶜ) + cbalance (outs tx) + + (f + TxFeesOf tx) + (d + DonationsOf tx) + cbalance (u ∣ SpendInputsOf tx) + + ≡˘⟨ iii ⟩ cbalance ((u ∣ SpendInputsOf tx ᶜ) ∪ˡ outs tx) + (f + TxFeesOf tx) + + (d + DonationsOf tx) + cbalance (u ∣ SpendInputsOf tx) + ∎ + where + -- Helper: a + b + c ≡ a + c + b + -- (i.e., swap the rightmost pair, modulo re-associating). + swap-right : ∀ a b c → a + b + c ≡ a + c + b + swap-right a b c = trans (+-assoc a b c) (trans (cong (a +_) (+-comm b c)) (sym (+-assoc a c b))) + + rearrange : + ∀ {A B F Tf D Td Ot : Coin} → A + B + F + D + Ot + Tf + Td ≡ A + Ot + (F + Tf) + (D + Td) + B + rearrange {A}{B}{F}{Tf}{D}{Td}{Ot} = begin + A + B + F + D + Ot + Tf + Td + ≡⟨ cong (λ x → x + Tf + Td) (+-comm (A + B + F + D) Ot ) ⟩ + Ot + (A + B + F + D) + Tf + Td + ≡⟨ cong (λ x → x + Tf + Td) (sym (+-assoc Ot ((A + B + F)) D)) ⟩ + Ot + (A + B + F) + D + Tf + Td + ≡⟨ cong (λ x → x + D + Tf + Td) (sym (+-assoc Ot (A + B) F)) ⟩ + Ot + (A + B) + F + D + Tf + Td + ≡⟨ cong (λ x → x + F + D + Tf + Td) (sym (+-assoc Ot A B)) ⟩ + Ot + A + B + F + D + Tf + Td + ≡⟨ cong (λ x → x + B + F + D + Tf + Td) (+-comm Ot A) ⟩ + A + Ot + B + F + D + Tf + Td + -- Hoist B rightward, one neighbour at a time + ≡⟨ cong (λ x → x + D + Tf + Td) (swap-right (A + Ot) B F) ⟩ + A + Ot + F + B + D + Tf + Td + ≡⟨ cong (λ x → x + Tf + Td) (swap-right (A + Ot + F) B D) ⟩ + A + Ot + F + D + B + Tf + Td + ≡⟨ cong (_+ Td) (swap-right (A + Ot + F + D) B Tf) ⟩ + A + Ot + F + D + Tf + B + Td + ≡⟨ swap-right (A + Ot + F + D + Tf) B Td ⟩ + A + Ot + F + D + Tf + Td + B + -- Bring Tf next to F, then group (F + Tf) and (D + Td) + ≡⟨ cong (λ x → x + Td + B) (swap-right (A + Ot + F) D Tf) ⟩ + A + Ot + F + Tf + D + Td + B + ≡⟨ cong (λ x → x + D + Td + B) (+-assoc (A + Ot) F Tf) ⟩ + A + Ot + (F + Tf) + D + Td + B + ≡⟨ cong (_+ B) (+-assoc (A + Ot + (F + Tf)) D Td) ⟩ + A + Ot + (F + Tf) + (D + Td) + B + ∎ + + -- equational reasoning steps -- + i = cong (λ x → x + f + d + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx) (split-balance u (SpendInputsOf tx)) + ii = rearrange {cbalance (u ∣ SpendInputsOf tx ᶜ)} + iii = cong (λ x → x + (f + TxFeesOf tx) + (d + DonationsOf tx) + cbalance (u ∣ SpendInputsOf tx)) + (balance-∪ {u = (u ∣ SpendInputsOf tx ᶜ)}{u' = (outs tx)} (outs-disjoint tx {utxo = u} freshId)) + +``` + +(The arithmetic `rearrange`{.AgdaFunction} is left as a `postulate`{.AgdaKeyword} +pending a future clean-up — it is purely a `+`/`∸`-free associative-commutative +rearrangement over `ℕ`{.AgdaDatatype}, provable by `solve-macro`{.AgdaFunction} +for the `+-0`-monoid.) + +## Batch coin balance + +The coin projection of the batch balance equation +`consumedBatch ≡ producedBatch`{.AgdaFunction} is what the `LEDGER-pov`{.AgdaFunction} +proof actually consumes. We expose it as a separate lemma here. + +```agda + batch-balance-coin : (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁ + → cbalance (UTxOOf Γ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + + negPart (DepositsChangeTopOf Γ) + + sum ( map (λ stx → cbalance (UTxOOf Γ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) + (SubTransactionsOf tx) ) + + negPart (DepositsChangeSubOf Γ) + ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + + posPart (DepositsChangeTopOf Γ) + + sum ( map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx)) + + posPart (DepositsChangeSubOf Γ) + + batch-balance-coin {Γ = Γ} (UTXO-⋯ _ _ _ _ _ _ _ batchBal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) = + begin + cbalance (UTxOOf Γ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf Γ) + _ + _ + ≡˘⟨ coin-of-consumedBatch tx (DepositsChangeOf Γ) (UTxOOf Γ) noMintTx noMintSubTx ⟩ + coin (consumedBatch (DepositsChangeOf Γ) tx (UTxOOf Γ)) + ≡⟨ cong coin batchBal ⟩ + coin (producedBatch (DepositsChangeOf Γ) tx) + ≡⟨ coin-of-producedBatch tx (DepositsChangeOf Γ) ⟩ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + posPart (DepositsChangeTopOf Γ) + _ + _ + ∎ +``` + +## `UTXO-pov`: combined statement + +The full statement uses `χ`{.AgdaFunction}, the characteristic function of +`Bool`{.AgdaDatatype}, which returns `0`{.AgdaInductiveConstructor} for +`false`{.AgdaInductiveConstructor} and `1`{.AgdaInductiveConstructor} for +`true`{.AgdaInductiveConstructor}: + +```agda + χ : Bool → ℕ + χ true = 1 + χ false = 0 +``` + +The combined `UTXO-pov`{.AgdaFunction} statement packages together the +mechanical change and the value-"withdrawals-in, direct-deposits-out" flow of +the top-level transaction alone. It is *not* a standalone preservation-of-value +theorem (the full batch equation requires also the sub-transaction data), +but it is the right statement for use in the `LEDGER-pov`{.AgdaFunction} proof +when combined with the `SUBLEDGERS-pov`{.AgdaFunction} lemma. + +**Claim.** + +```agda +{-- + UTXO-pov : ∀ {Γ : UTxOEnv} {legacyMode : Bool} {s₀ s₁ : UTxOState} + → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s₀)) + → (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁ + → getCoin s₀ + + getCoin (WithdrawalsOf tx) * χ (IsValidFlagOf tx) + + sum (map (λ (stx : SubLevelTx) → + getCoin (WithdrawalsOf stx) * χ (IsValidFlagOf tx)) + (SubTransactionsOf tx)) + ≡ getCoin s₁ + + getCoin (DirectDepositsOf tx) * χ (IsValidFlagOf tx) + -- + ... -- (see sketch below) +--} +``` + +*Proof sketch.* + ++ **Invalid case** (`IsValidFlagOf tx ≡ false`): Both sides simplify via + `*-zeroʳ`. The top-level `getCoin s₀ ≡ getCoin s₁` is + `UTXO-I-getCoin`{.AgdaFunction}. Sub-transaction sums all disappear + because each `χ ∘ IsValidFlagOf tx ≡ 0`. + ++ **Valid case** (`IsValidFlagOf tx ≡ true`): Combine + `UTXO-V-mechanical`{.AgdaFunction} (the mechanical rearrangement) with + `batch-balance-coin`{.AgdaFunction} (the batch balance) to derive the + full equation. The batch equation transfers value between the consumed + side (inputs + withdrawals) and produced side (outs + fees + donations + + direct deposits) at the *batch* level, threaded through the tx's local + state change. + +This theorem is stated as a `Claim`{.AgdaFunction} because the exact form +used by `LEDGER-pov`{.AgdaFunction} depends on how the +`SUBLEDGERS-pov`{.AgdaFunction} lemma threads through sub-transaction state +changes. The two building blocks it relies on — +`UTXO-I-getCoin`{.AgdaFunction}, `UTXO-V-mechanical`{.AgdaFunction}, and +`batch-balance-coin`{.AgdaFunction} — are already proved above (modulo the +parameterized assumptions). + +```agda +-- UTXO-pov = {!!} -- placeholder; the final form is to be fixed in follow-up work. +``` + +## Summary of proof obligations + ++ Port `balance-∪`{.AgdaFunction}, `split-balance`{.AgdaFunction}, and + `newTxid⇒disj`{.AgdaFunction} from + `Ledger.Conway.Specification.Utxo.Properties.Base`{.AgdaModule} to the + Dijkstra equivalent. These are era-independent; the port should be + mechanical. + ++ Prove `coin-of-consumedBatch`{.AgdaFunction} and + `coin-of-producedBatch`{.AgdaFunction} from their definitions, by + repeated application of `∙-homo-Coin`{.AgdaFunction} and + `coin∘inject≗id`{.AgdaField}, plus the per-transaction `coin (MintedValueOf t) ≡ 0` + facts (from UTXO's `p₆` premise for top-level, and from each SUBUTXO's + premise for sub-transactions — the latter requires threading the SUBLEDGERS + step through). + ++ Finalize the exact statement of `UTXO-pov`{.AgdaFunction}, in coordination + with the `LEDGER-pov`{.AgdaFunction} proof's `BatchUtxoAccounting`{.AgdaFunction} + requirement. + ++ Prove the small arithmetic `rearrange`{.AgdaFunction} `postulate`{.AgdaKeyword} + in `UTXO-V-mechanical`{.AgdaFunction}, e.g. via `solve-macro`{.AgdaFunction}. diff --git a/src/Ledger/Dijkstra/Specification/Utxow/Properties.lagda.md b/src/Ledger/Dijkstra/Specification/Utxow/Properties.lagda.md index 01e669ca92..b1b879e4a6 100644 --- a/src/Ledger/Dijkstra/Specification/Utxow/Properties.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxow/Properties.lagda.md @@ -14,4 +14,5 @@ module Ledger.Dijkstra.Specification.Utxow.Properties where ```agda open import Ledger.Dijkstra.Specification.Utxow.Properties.Computational +open import Ledger.Dijkstra.Specification.Utxow.Properties.PoV ``` diff --git a/src/Ledger/Dijkstra/Specification/Utxow/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Utxow/Properties/PoV.lagda.md new file mode 100644 index 0000000000..df2cc9c710 --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Utxow/Properties/PoV.lagda.md @@ -0,0 +1,142 @@ +--- +source_branch: master +source_path: src/Ledger/Dijkstra/Specification/Utxow/Properties/PoV.lagda.md +--- + +# UTXOW: Preservation of Value {#sec:utxow-pov} + +This module states the preservation-of-value (PoV) property for the Dijkstra +`UTXOW`{.AgdaDatatype} rule. The `UTXOW`{.AgdaDatatype} rule performs all +witness checks (signatures, scripts, datums) and then delegates the actual +state change to the `UTXO`{.AgdaDatatype} rule. In Dijkstra there are two +flavours of `UTXOW`{.AgdaDatatype}. + +1. `UTXOW-normal`{.AgdaInductiveConstructor}: only Plutus V4 scripts are used. +2. `UTXOW-legacy`{.AgdaInductiveConstructor}: at least one Plutus V1/V2/V3 + script is used; guards must be empty; direct deposits and balance intervals + must be empty. + +Both constructors have the *same* final premise, `(Γ , ?) ⊢ s ⇀⦇ tx ,UTXO⦈ s'`, +so the state change is identical. Consequently, every PoV statement about +`UTXOW`{.AgdaDatatype} reduces directly to the corresponding statement about +`UTXO`{.AgdaDatatype}. + + + +## Extracting the `UTXO`{.AgdaDatatype} step + +The key observation is that both `UTXOW-normal`{.AgdaInductiveConstructor} +and `UTXOW-legacy`{.AgdaInductiveConstructor} embed a `UTXO`{.AgdaDatatype} +derivation as their final premise. We factor out an extractor: + +```agda +UTXOW⇒UTXO : ∀ {Γ : UTxOEnv} {s s' : UTxOState} {tx : TopLevelTx} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → ∃[ legacyMode ] ((Γ , legacyMode) ⊢ s ⇀⦇ tx ,UTXO⦈ s') + +UTXOW⇒UTXO (UTXOW-normal-⋯ _ _ _ _ _ _ _ _ _ _ utxo) = false , utxo +UTXOW⇒UTXO (UTXOW-legacy-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ utxo) = true , utxo +``` + +## `UTXOW-I-getCoin`: collateral collection preserves `getCoin` + +In the invalid case, the `UTXOW`{.AgdaDatatype} rule preserves `getCoin`{.AgdaField} +exactly (collateral is moved from the UTxO to the fees, both of which are +counted in `getCoin`{.AgdaField}): + +```agda +module UTXOW-PoV (tx : TopLevelTx) (let open Tx tx; open TxBody txBody) + + -- Same assumptions as the UTXO-pov module. + ( balance-∪ : ∀ {u u' : UTxO} → disjoint (dom u) (dom u') → cbalance (u ∪ˡ u') ≡ cbalance u + cbalance u' ) + + ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn) → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) ) + + ( noMintTx : coin (MintedValueOf tx) ≡ 0 ) + + ( noMintSubTx : noMintingSubTxs tx ) + + ( outs-disjoint : ∀ {u : UTxO} → TxIdOf tx ∉ mapˢ proj₁ (dom u) → disjoint (dom (u ∣ SpendInputsOf tx ᶜ)) (dom (outs tx)) ) + where + open UTxO-PoV tx (λ {u} {u'} → balance-∪ {u} {u'}) split-balance noMintTx noMintSubTx + -- The `λ {u}{u'} → balance-∪ {u}{u'}` η-expansion is needed because passing + -- `balance-∪` directly triggers Agda to eta-expand the `{u u' : UTxO}` implicits + -- through UTxO's `Σ _ left-unique` record structure, leaving the `left-unique` + -- field as an unresolved meta. Binding `{u}{u'}` as pattern variables in the outer + -- lambda makes them concrete bound values and sidesteps the eta-expansion. + + UTXOW-I-getCoin : ∀ {Γ : UTxOEnv} {s s' : UTxOState} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → IsValidFlagOf tx ≡ false → getCoin s ≡ getCoin s' + UTXOW-I-getCoin {Γ} utxow invalid = UTXO-I-getCoin (proj₂ (UTXOW⇒UTXO utxow)) invalid +``` + +## `UTXOW-V-mechanical`: mechanical rearrangement + +The valid case simply reuses the UTXO-level mechanical rearrangement: + +```agda + UTXOW-V-mechanical : ∀ {Γ : UTxOEnv} {s s' : UTxOState} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → IsValidFlagOf tx ≡ true → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s)) + → getCoin s + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + ≡ getCoin s' + cbalance (UTxOOf s ∣ SpendInputsOf tx) + + UTXOW-V-mechanical utxow valid fresh = UTXO-V-mechanical (proj₂ (UTXOW⇒UTXO utxow)) valid fresh +``` + +## `UTXOW-batch-balance-coin` + +```agda + UTXOW-batch-balance-coin : ∀ {Γ : UTxOEnv} {s s' : UTxOState} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' + → cbalance (UTxOOf Γ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + + negPart (DepositsChangeTopOf Γ) + + sum (map (λ stx → cbalance (UTxOOf Γ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx)) + + negPart (DepositsChangeSubOf Γ) + ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + + posPart (DepositsChangeTopOf Γ) + + sum ( map (λ (stx : SubLevelTx) → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx) ) + + posPart (DepositsChangeSubOf Γ) + UTXOW-batch-balance-coin utxow = batch-balance-coin (proj₂ (UTXOW⇒UTXO utxow)) +``` + +## `utxow-pov-invalid` for use in `LEDGER-pov` + +The following is the *specific* form needed by `Ledger.Properties.PoV` +(the `BatchUtxoAccounting` use site takes it as a module parameter). It is +identical to `UTXOW-I-getCoin`{.AgdaFunction} above, retagged for clarity: + +```agda + utxow-pov-invalid : ∀ {Γ : UTxOEnv} {s s' : UTxOState} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → IsValidFlagOf tx ≡ false → getCoin s ≡ getCoin s' + utxow-pov-invalid = UTXOW-I-getCoin +``` + +With this, the `utxow-pov-invalid` postulated module parameter in +`Ledger.Properties.PoV` can be discharged by calling this function. + +## Summary of proof obligations + ++ Same ported arithmetic lemmas as `Utxo.Properties.PoV` (`balance-∪`, + `split-balance`, `outs-disjoint`, and the two batch-coin-projection + lemmas). + ++ Once those are ported, the entire `UTXOW-pov` module is mechanical + pattern-matching on the two `UTXOW`{.AgdaDatatype} constructors, with + delegation to `Utxo.Properties.PoV`. diff --git a/src/Ledger/Prelude.lagda.md b/src/Ledger/Prelude.lagda.md index 17ddc34276..7c2d86d04a 100644 --- a/src/Ledger/Prelude.lagda.md +++ b/src/Ledger/Prelude.lagda.md @@ -41,23 +41,27 @@ open import Tactic.Derive.DecEq public open import Tactic.Inline public open import MyDebugOptions public open import Prelude.STS.GenPremises public +open import Data.List.Membership.Propositional.Properties using (∈-deduplicate⁻) +open import Relation.Binary using (IsEquivalence) open import abstract-set-theory.FiniteSetTheory public renaming (_⊆_ to _⊆ˢ_) open import abstract-set-theory.Axiom.Set.Map.Extra th public +open import Axiom.Set.Properties th + import Data.Integer as ℤ open import Data.Integer using (0ℤ) public import Data.Rational as ℚ open import Data.Rational using (ℚ) +open import Data.Nat.Properties using (+-identityʳ) + + dec-de-morgan : ∀{P Q : Type} → ⦃ P ⁇ ⦄ → ¬ (P × Q) → ¬ P ⊎ ¬ Q dec-de-morgan ⦃ ⁇ no ¬p ⦄ ¬pq = inj₁ ¬p dec-de-morgan ⦃ ⁇ yes p ⦄ ¬pq = inj₂ λ q → ¬pq (p , q) -≡ᵉ-getCoin : ∀ {A} → ⦃ _ : DecEq A ⦄ → (s s' : A ⇀ Coin) → s ˢ ≡ᵉ s' ˢ → getCoin s ≡ getCoin s' -≡ᵉ-getCoin {A} ⦃ decEqA ⦄ s s' s≡s' = indexedSumᵛ'-cong {C = Coin} {x = s} {y = s'} s≡s' - setToMap : ∀ {A B : Type} → ⦃ DecEq A ⦄ → ℙ (A × B) → A ⇀ B setToMap = fromListᵐ ∘ setToList @@ -98,4 +102,81 @@ Is-∅ X = Is-[] (setToList X) concatMapˡ : {A B : Type} → (A → ℙ B) → List A → ℙ B concatMapˡ f as = proj₁ $ unions (fromList (map f as)) + +indexedSumL-proj₂-zero : ∀ {A : Type} (l : List (A × Coin)) + → (∀ {x} → x ∈ˡ l → proj₂ x ≡ 0) + → indexedSumL {M = Coin} proj₂ l ≡ 0 +indexedSumL-proj₂-zero [] _ = refl +indexedSumL-proj₂-zero ((a , v) ∷ xs) all-zero = + trans (cong (_+ indexedSumL proj₂ xs) (all-zero (Prelude.Init.here refl))) + (indexedSumL-proj₂-zero xs (all-zero ∘ Prelude.Init.there)) + +module _ {A : Type} ⦃ _ : DecEq A ⦄ where + + getCoin-singleton : {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c + getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _) + + ≡ᵉ-getCoin : (s s' : A ⇀ Coin) → s ˢ ≡ᵉ s' ˢ → getCoin s ≡ getCoin s' + ≡ᵉ-getCoin s s' s≡s' = indexedSumᵛ'-cong {C = Coin} {x = s} {y = s'} s≡s' + + getCoin-cong : (s : A ⇀ Coin) (s' : ℙ (A × Coin)) + → s ˢ ≡ᵉ s' → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' + getCoin-cong s s' eq = indexedSum-cong {f = proj₂} {x = (s ˢ) ᶠˢ} {y = s' ᶠˢ} eq + + indexedSumᵛ'-∪ : (m m' : A ⇀ Coin) → disjoint (dom m) (dom m') + → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' + indexedSumᵛ'-∪ m m' disj = + trans (indexedSumᵐ-∪ˡ-∪ˡᶠ m m') + (indexedSumᵐ-∪ {X = m ᶠᵐ} {m' ᶠᵐ} {f = proj₂} disj) + + + res-decomp : (m m' : A ⇀ Coin) → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ + res-decomp m m' = ∪-cong (≡ᵉ.refl {x = m ˢ}) (≡ᵉ.sym (filterᵐ-idem {m = m'})) + where module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {A × Coin}) + + ∪ˡsingleton∈dom : (m : A ⇀ Coin) {(a , c) : A × Coin} + → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + ∪ˡsingleton∈dom m {(a , c)} a∈dom = ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom) + + ∪ˡsingleton∉dom : (m : A ⇀ Coin) {(a , c) : A × Coin} + → a ∉ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + c + ∪ˡsingleton∉dom m {(a , c)} a∉dom = + trans (indexedSumᵛ'-∪ m ❴ a , c ❵ᵐ ( λ x y → a∉dom (subst (_∈ dom m) (from ∈-dom-singleton-pair y) x) )) + (cong (getCoin m +_) getCoin-singleton) + where open Equivalence + + ∪ˡsingleton0≡ : (m : A ⇀ Coin) {a : A} → getCoin (m ∪ˡ ❴ (a , 0) ❵ᵐ) ≡ getCoin m + ∪ˡsingleton0≡ m {a} with a ∈? dom m + ... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom + ... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m)) + +opaque + unfolding List-Model finiteness + + sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 + sumConstZero {A} {X} = indexedSumL-proj₂-zero (deduplicate _≟_ l) all-zero-dedup + where + open Equivalence + + fin : finite (mapˢ (_, 0) X) + fin = finiteness (mapˢ (_, 0) X) + + l : List (A × Coin) + l = fin .proj₁ + + h : ∀ {a} → a ∈ (mapˢ (_, 0) X) ⇔ a ∈ˡ l + h = fin .proj₂ + + all-zero : ∀ {x} → x ∈ˡ l → proj₂ x ≡ 0 + all-zero x∈l with from ∈-map (from h x∈l) + ... | (a , refl , _) = refl + + all-zero-dedup : ∀ {x} → x ∈ˡ deduplicate _≟_ l → proj₂ x ≡ 0 + all-zero-dedup x∈dedup = all-zero (∈-deduplicate⁻ (DecEq._≟_ DecEq-×′) l x∈dedup) + +opaque + unfolding setToList List-Model + + setToList-∈ : ∀ {A : Type} {a : A} {X : ℙ A} → a ∈ˡ setToList X → a ∈ X + setToList-∈ = id ```