From bdf4f8dc783bdf6a6fb16382dd52f8df76d6a9b8 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 23 Jun 2026 04:06:49 +0000 Subject: [PATCH 1/3] Conway PoV: discharge map/coin assumptions via new Ledger.Prelude lemmas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Split out of the LEDGER-pov work (#1203): this Conway-era properties cleanup is independent of the Dijkstra PoV proof and belongs in its own PR. - Add reusable coin/map lemmas to `Ledger.Prelude`: `getCoin-singleton`, `getCoin-cong`, `indexedSumᵛ'-∪`, `res-decomp`, `∪ˡsingleton∈dom`, `∪ˡsingleton∉dom`, `∪ˡsingleton0≡`, `sumConstZero`, `indexedSumL-proj₂-zero`, `setToList-∈`; relocate `≡ᵉ-getCoin` into the `⦃ DecEq A ⦄` module. - Drop the now-provable assumption parameters from the Conway PoV proofs, using the Prelude lemmas instead: - `Certs/Properties/PoV`: keep only `≡ᵉ-getCoinˢ'`. - `Certs/Properties/PoVLemmas`: remove the local `∪ˡsingleton*`/`getCoin-singleton` helpers and the `indexedSumᵛ'-∪` assumption module; qualify `IsEquivalence` as `Eq`. - `Ledger/Properties/PoV`: keep only `≡ᵉ-getCoinˢ`. - `Conformance/Properties`: drop the `indexedSum-∪⁺-hom` parameter. - `Utxo/Properties/GenMinSpend`: use the hoisted `getCoin-singleton`. No spec-semantic change (proof refactor only), so no CHANGELOG entry. `Ledger.Prelude` typechecks under Agda 2.8.0 via the project flake; the Conway files are their 1187 versions (which typecheck) and depend only on the hoisted lemmas. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r --- .../Conway/Conformance/Properties.lagda.md | 2 - .../Certs/Properties/PoV.lagda.md | 17 +-- .../Certs/Properties/PoVLemmas.lagda.md | 126 +++++++----------- .../Ledger/Properties/PoV.lagda.md | 16 +-- .../Utxo/Properties/GenMinSpend.lagda.md | 5 +- src/Ledger/Prelude.lagda.md | 95 ++++++++++++- 6 files changed, 149 insertions(+), 112 deletions(-) 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/Prelude.lagda.md b/src/Ledger/Prelude.lagda.md index f5bee341f0..a88353ecc6 100644 --- a/src/Ledger/Prelude.lagda.md +++ b/src/Ledger/Prelude.lagda.md @@ -48,6 +48,7 @@ open import abstract-set-theory.Axiom.Set.Map.Extra public import Data.Integer as ℤ open import Data.Integer using (0ℤ) public +open import Data.Nat.Properties using (+-identityʳ) import Data.Rational as ℚ open import Data.Rational using (ℚ) @@ -55,9 +56,6 @@ dec-de-morgan : ∀{P Q : Type} → ⦃ P ⁇ ⦄ → ¬ (P × Q) → ¬ P ⊎ 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 +96,95 @@ 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 + + -- A coin singleton has the coin you expect. + 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) + + open import Axiom.Set.Properties th + open import Relation.Binary using (IsEquivalence) + + 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}) + + -- If a is already in domain of m, left-biased union with singleton at a + -- leaves total unchanged (existing entry wins). + ∪ˡ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) + + -- If a is *not* in domain of m, left-biased union with singleton adds cleanly. + ∪ˡ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 = + 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 + ∎ + where open Equivalence ; open ≡-Reasoning + + -- The case-split corollary specialised to a zero-valued singleton. + ∪ˡ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)) + + + open import Data.List.Membership.Propositional.Properties using (∈-deduplicate⁻) + + sumConstZero : {X : ℙ A} → getCoin (constMap X 0) ≡ 0 + sumConstZero {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 ``` From fc88218dcc5434efa1647ff108b48757d9ae916e Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 22 Jun 2026 23:26:37 -0600 Subject: [PATCH 2/3] Apply suggestions from code review Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com> --- src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md | 2 +- .../Conway/Specification/Certs/Properties/PoVLemmas.lagda.md | 2 +- .../Conway/Specification/Ledger/Properties/PoV.lagda.md | 2 +- src/Ledger/Prelude.lagda.md | 4 +--- 4 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md index db2c5ba602..5f3da7669f 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md @@ -47,7 +47,7 @@ instance _ = +-0-monoid module Certs-PoV - -- TODO: prove the following assumption, used in roof of `CERTBASE-pov`. + -- TODO: prove the following assumption, used in proof 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 diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md index a481556fa9..a4b7277fcc 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md +++ b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md @@ -100,7 +100,7 @@ injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈))) module Certs-Pov-lemmas - -- TODO: prove the following assumption, used in roof of `CERTBASE-pov`. + -- TODO: prove the following assumption, used in proof 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 diff --git a/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md index cf21230924..eef496ec74 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md @@ -38,7 +38,7 @@ instance module _ (tx : Tx) (let open Tx tx; open TxBody body) - -- TODO: prove the following assumption, used in roof of `CERTBASE-pov`. + -- TODO: prove the following assumption, used in proof 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 diff --git a/src/Ledger/Prelude.lagda.md b/src/Ledger/Prelude.lagda.md index a88353ecc6..3cb44de9f2 100644 --- a/src/Ledger/Prelude.lagda.md +++ b/src/Ledger/Prelude.lagda.md @@ -133,10 +133,8 @@ module _ {A : Type} ⦃ _ : DecEq A ⦄ where -- If a is already in domain of m, left-biased union with singleton at a -- leaves total unchanged (existing entry wins). - ∪ˡ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) + ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) m (singleton-∈-∪ˡ {m = m} a∈dom) -- If a is *not* in domain of m, left-biased union with singleton adds cleanly. ∪ˡsingleton∉dom : (m : A ⇀ Coin) {(a , c) : A × Coin} From a6e229d78b393e701b2960e4a05e56d797a6afb1 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Tue, 23 Jun 2026 00:11:23 -0600 Subject: [PATCH 3/3] add forgotten signature --- src/Ledger/Prelude.lagda.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Ledger/Prelude.lagda.md b/src/Ledger/Prelude.lagda.md index 3cb44de9f2..e7d2be6a91 100644 --- a/src/Ledger/Prelude.lagda.md +++ b/src/Ledger/Prelude.lagda.md @@ -133,6 +133,8 @@ module _ {A : Type} ⦃ _ : DecEq A ⦄ where -- If a is already in domain of m, left-biased union with singleton at a -- leaves total unchanged (existing entry wins). + ∪ˡ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)