Don't count pool deposits when reregistering pools

CHANGELOG.md

@@ -4,6 +4,7 @@
 
 ### WIP
 
+- Do not count pool deposits a second time when reregistering pools
 - Allow reregistration of pools in the POOL transition relation
 - Implement the fPoolParams field of PState as in the Shelley specification
 - Add the BBODY transition relation from Shelley

CONTRIBUTING.md

@@ -225,7 +225,7 @@ nix develop
 
 # Build specific artifacts using fls-shake
 fls-shake html                # Build HTML docs
-fls-shake hs                  # Build Haskell source
+rm -rf _build dist/hs; fls-shake hs   # Build Haskell source
 
 # See all available targets
 fls-shake --help
@@ -341,10 +341,10 @@ Then point your browser to <http://127.0.0.1:8000>.
 
 For the best development experience, you should configure your IDE to use the Agda executable provided by this project's Nix environment.
 
-First, build `agdaWithPackages` and create a stable symlink to it in your home directory. This prevents you from having to update your IDE settings every time the project's dependencies change.
+First, build `fls-agdaWithPackages` and create a stable symlink to it in your home directory. This prevents you from having to update your IDE settings every time the project's dependencies change.
 
 ```bash
-nix build ./#agdaWithPackages -o ~/ledger-agda
+nix build ./#fls-agdaWithPackages -o ~/ledger-agda
 ```
 
 Then make sure that the `~/ledger-agda/bin` directory is in your `PATH` when starting your editor.

src/Ledger/Conway/Conformance/Equivalence/Deposits.agda

@@ -16,13 +16,13 @@ module Ledger.Conway.Conformance.Equivalence.Deposits
   (txs : _) (open TransactionStructure txs)
   (abs : AbstractFunctions txs) (open AbstractFunctions abs)
   where
- 
+
 private
   module L where
     open import Ledger.Conway.Specification.Ledger txs abs public
     open import Ledger.Conway.Specification.Utxo txs abs public
     open import Ledger.Conway.Specification.Certs govStructure public
-  
+
   module C where
     open import Ledger.Conway.Conformance.Ledger txs abs public
     open import Ledger.Conway.Conformance.Utxo txs abs public
@@ -118,8 +118,8 @@ cong-certGDeps = cong-filterᵐ
 castValidDepsᵈ : ∀ {pp deps₁ deps₂ certs} → deps₁ ≡ᵐ deps₂ → ValidDepsᵈ pp deps₁ certs → ValidDepsᵈ pp deps₂ certs
 castValidDepsᵈ                         eq [] = []
 castValidDepsᵈ {pp} {certs = cert ∷ _} eq (delegate   deps) = delegate           (castValidDepsᵈ (cong-updateCertDeposit pp cert eq) deps)
-castValidDepsᵈ {pp} {deps₁} {deps₂} {certs = cert ∷ _} eq (dereg h h' deps) = 
-  dereg (proj₁ eq h) h' 
+castValidDepsᵈ {pp} {deps₁} {deps₂} {certs = cert ∷ _} eq (dereg h h' deps) =
+  dereg (proj₁ eq h) h'
         (castValidDepsᵈ (cong-updateCertDeposit pp cert {deps₁} {deps₂} eq) deps)
 --castValidDepsᵈ {pp} {deps₁} {deps₂}
 --                    {certs = cert ∷ _} eq (dereg h    deps) = dereg (map₂ (proj₁ eq) h) (castValidDepsᵈ (cong-updateCertDeposit
@@ -292,8 +292,8 @@ lem-upd-cert-ddeps {pp} deps (L.reg c v ∷ certs) =
   lem-upd-cert-ddeps (deps ∪⁺ dep) certs
   where dep = ❴ L.CredentialDeposit c , pp .PParams.keyDeposit ❵
 lem-upd-cert-ddeps {pp} deps (L.regpool kh p ∷ certs) =
-  ≈-sym (cong-updateDDeps certs (lem-add-excluded λ ())) ⟨≈⟩
-  lem-upd-cert-ddeps (deps ∪⁺ dep) certs
+  ≈-sym (cong-updateDDeps certs (lem-add-excluded-∪ˡ deps λ ())) ⟨≈⟩
+  lem-upd-cert-ddeps (deps ∪ˡ dep) certs
   where dep = ❴ L.PoolDeposit kh , pp .PParams.poolDeposit ❵
 lem-upd-cert-ddeps {pp} deps (L.regdrep c v a ∷ certs) =
   ≈-sym (cong-updateDDeps certs (lem-add-excluded λ ())) ⟨≈⟩
@@ -322,8 +322,8 @@ lem-upd-cert-gdeps {pp} deps (L.reg c v ∷ certs) =
   lem-upd-cert-gdeps (deps ∪⁺ dep) certs
   where dep = ❴ L.CredentialDeposit c , pp .PParams.keyDeposit ❵
 lem-upd-cert-gdeps {pp} deps (L.regpool kh p ∷ certs) =
-  ≈-sym (cong-updateGDeps certs (lem-add-excluded λ ())) ⟨≈⟩
-  lem-upd-cert-gdeps (deps ∪⁺ dep) certs
+  ≈-sym (cong-updateGDeps certs (lem-add-excluded-∪ˡ deps λ ())) ⟨≈⟩
+  lem-upd-cert-gdeps (deps ∪ˡ dep) certs
   where dep = ❴ L.PoolDeposit kh , pp .PParams.poolDeposit ❵
 lem-upd-cert-gdeps {pp} deps (L.regdrep c v a ∷ certs) =
   ≈-sym (cong-updateGDeps certs (lem-add-included DRepDeposit)) ⟨≈⟩

src/Ledger/Conway/Conformance/Equivalence/Map.agda

@@ -656,5 +656,31 @@ module _  {A B : Type}
       lem-add-excluded p =
         filterᵐ-∪⁺-distr _ _ ⟨≈⟩ ∪⁺-cong-l (filterᵐ-singleton-false p) ⟨≈⟩ ∪⁺-id-r _
 
+      lem-add-excluded-∪ˡ
+        : (m : A ⇀ B)
+        → ¬ P k
+        → filterᵐ P′ (m ∪ˡ ❴ k , v ❵) ≡ᵐ filterᵐ P′ m
+      lem-add-excluded-∪ˡ {k = k} {v = v} m ¬p with k ∈? dom m
+      ... | yes k∈m =
+          filterᵐ-cong
+            {m = m ∪ˡ ❴ k , v ❵}
+            {m' = m}
+            (singleton-∈-∪ˡ {m = m} k∈m)
+      ... | no k∉m = begin
+          filterᵐ P′ (m ∪ˡ ❴ k , v ❵) ˢ
+            ≈⟨ filter-cong $ disjoint-∪ˡ-∪ (disjoint-sing k∉m) ⟩
+          filterˢ P′ (m ˢ ∪ ❴ k , v ❵)
+            ≈⟨ filter-hom-∪ ⟩
+          filterˢ P′ (m ˢ) ∪ filterˢ P′ ❴ k , v ❵
+            ≈⟨ ∪-cong ≡ᵉ.refl (filterᵐ-singleton-false ¬p) ⟩
+          filterˢ P′ (m ˢ) ∪ ∅
+            ≈⟨ ∪-identityʳ (filterˢ P′ (m ˢ)) ⟩
+          filterˢ P′ (m ˢ)
+          ∎
+        where
+          disjoint-sing : k ∉ dom m → disjoint (dom m) (dom (singleton (k , v)))
+          disjoint-sing k∉m a∈d a∈sing
+            rewrite from ∈-dom-singleton-pair a∈sing = k∉m a∈d
+
       lem-del-excluded : ∀ m → ¬ P k → filterᵐ P′ (m ∣ ❴ k ❵ ᶜ) ≡ᵐ filterᵐ P′ m
       lem-del-excluded m ¬p = filterᵐ-restrict m ⟨≈⟩ restrict-singleton-filterᵐ-false m ¬p

src/Ledger/Conway/Specification/Epoch/Properties/GovDepsMatch.lagda.md

@@ -96,8 +96,7 @@ For the formal statement of the lemma,
 *Proof*.
 
 ```agda
-  EPOCH-govDepsMatch {eps'} {e} ratify-removed (EPOCH (x , POOLREAP , _)) =
-      poolReapMatch ∘ ratifiesSnapMatch
+  EPOCH-govDepsMatch {eps'} {e} ratify-removed = mainProof
     where
 
     -- the combinator used in the EPOCH rule
@@ -200,11 +199,6 @@ For the formal statement of the lemma,
          res-dom d∈res  -- d ∈ retiredDeposits
       where import Data.Product.Base as Product using (map₂)
 
-    ratifiesSnapMatch : govDepsMatch (LStateOf eps) → govDepsMatch ls₁
-    ratifiesSnapMatch =
-       ≡ᵉ.trans (filter-cong $ dom-cong (res-comp-cong $ ≡ᵉ.sym ΔΠ'≡ΔΠ))
-       ∘ from ≡ᵉ⇔≡ᵉ' ∘ main-invariance-lemma ∘ to ≡ᵉ⇔≡ᵉ'
-
     noGADepositIsRetired
       : (d : DepositPurpose)
       → d ∈ dom (DepositsOf ls₁ ∣ retiredDeposits)
@@ -271,7 +265,18 @@ For the formal statement of the lemma,
         open import Relation.Binary using (IsEquivalence)
         import Axiom.Set.Rel th as Rel
 
-    poolReapMatch : govDepsMatch ls₁ → govDepsMatch (LStateOf eps')
-    poolReapMatch = ≡ᵉ.trans dropRetiredDeposits
+    mainProof
+     : _ ⊢ eps ⇀⦇ e ,EPOCH⦈ eps'
+     → govDepsMatch (LStateOf eps) → govDepsMatch (LStateOf eps')
+    -- Pattern matching POOLREAP used to be done in EPOCH-govDepsMatch directly.
+    -- However, that made typechecking much slower.
+    mainProof (EPOCH (x , POOLREAP , _)) = poolReapMatch ∘ ratifiesSnapMatch
+      where
+        ratifiesSnapMatch : govDepsMatch (LStateOf eps) → govDepsMatch ls₁
+        ratifiesSnapMatch =
+          ≡ᵉ.trans (filter-cong $ dom-cong (res-comp-cong $ ≡ᵉ.sym ΔΠ'≡ΔΠ))
+          ∘ from ≡ᵉ⇔≡ᵉ' ∘ main-invariance-lemma ∘ to ≡ᵉ⇔≡ᵉ'
 
+        poolReapMatch : govDepsMatch ls₁ → govDepsMatch (LStateOf eps')
+        poolReapMatch = ≡ᵉ.trans dropRetiredDeposits
 ```

src/Ledger/Conway/Specification/Ledger/Properties/Base.lagda.md

@@ -113,6 +113,59 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where
     dpMap-rmOrphanDRepVotes : ∀ certState govSt → dpMap (rmOrphanDRepVotes certState govSt) ≡ dpMap govSt
     dpMap-rmOrphanDRepVotes certState govSt = sym (fmap-∘ govSt) -- map proj₁ ∘ map (map₂ _) ≡ map (proj₁ ∘ map₂ _) ≡ map proj₁
 
+-- TODO: Move these proofs to agda-sets
+module _ {A V : Set} ⦃ mon : CommutativeMonoid 0ℓ 0ℓ V ⦄ ⦃ dA : DecEq A ⦄ {m m' : A ⇀ V} where
+  open import Function.Reasoning
+
+  rhs-∪ˡ : A ⇀ V
+  rhs-∪ˡ = filterᵐ? (sp-∘ (sp-¬ (∈-sp {X = dom (m ˢ)})) proj₁) m'
+
+  dom∪ˡˡ : dom (m ˢ) ⊆ dom ((m ∪ˡ m') ˢ)
+  dom∪ˡˡ {a} a∈ = a∈ |> id ∶
+      a ∈ dom (m ˢ)                   |> ∪-⊆ˡ ∶
+      a ∈ dom (m ˢ) ∪ dom (rhs-∪ˡ ˢ)  |> proj₂ dom∪ ∶
+      a ∈ dom ((m ˢ) ∪ (rhs-∪ˡ ˢ))    |> id ∶
+      a ∈ dom ((m ∪ˡ m') ˢ)
+
+  dom∪ˡʳ : dom (m' ˢ) ⊆ dom ((m ∪ˡ m') ˢ)
+  dom∪ˡʳ {a} a∈ with a ∈? dom m
+  ... | yes p = dom∪ˡˡ p
+  ... | no ¬p =
+      a ∈ dom m'                       ∋ a∈ |> from ∈-map ∶
+      (∃[ ab ] a ≡ proj₁ ab × ab ∈ (m' ˢ))  |>
+         (λ { (ab , refl , ab∈m') → (¬p , ab∈m') |> id ∶
+             (a ∉ dom m × ab ∈ m')  |> to ∈-filter ∶
+             ab ∈ rhs-∪ˡ            |> (λ ab∈f → to ∈-map (ab , refl , ab∈f)) ∶
+             a ∈ dom rhs-∪ˡ
+         }) ∶
+      a ∈ dom rhs-∪ˡ                |> ∈-∪⁺ ∘ inj₂ ∶
+      a ∈ dom m ∪ dom rhs-∪ˡ        |> proj₂ dom∪ ∶
+      a ∈ dom ((m ˢ) ∪ (rhs-∪ˡ ˢ))  |> id ∶
+      a ∈ dom ((m ∪ˡ m') ˢ)
+
+  dom∪ˡ⊆∪dom : dom ((m ∪ˡ m') ˢ) ⊆ dom (m ˢ) ∪ dom (m' ˢ)
+  dom∪ˡ⊆∪dom {a} a∈dom∪ with ∈-∪⁻ (proj₁ dom∪ a∈dom∪)
+  ... | inj₁ a∈domm = ∈-∪⁺ (inj₁ a∈domm)
+  ... | inj₂ a∈domf = a∈domf |> id ∶
+      a ∈ dom rhs-∪ˡ                        |> from ∈-map ∶
+      (∃[ ab ] a ≡ proj₁ ab × ab ∈ rhs-∪ˡ)  |>
+         (λ { (ab , refl , ab∈fm') →
+             ab ∈ rhs-∪ˡ ∋ ab∈fm'           |> proj₂ ∘ from ∈-filter ∶
+             ab ∈ m'                        |> (λ ab∈m' → to ∈-map (ab , refl , ab∈m')) ∶
+             a ∈ dom m'
+         }) ∶
+      a ∈ dom m'          |> ∈-∪⁺ ∘ inj₂ ∶
+      a ∈ dom m ∪ dom m'
+
+  ∪dom⊆dom∪ˡ : dom (m ˢ) ∪ dom (m' ˢ) ⊆ dom ((m ∪ˡ m') ˢ)
+  ∪dom⊆dom∪ˡ {a} a∈
+    with from ∈-∪ a∈
+  ... | inj₁ a∈ˡ = dom∪ˡˡ a∈ˡ
+  ... | inj₂ a∈ʳ = dom∪ˡʳ a∈ʳ
+
+  dom∪ˡ≡∪dom : dom ((m ∪ˡ m')ˢ) ≡ᵉ dom (m ˢ) ∪ dom (m' ˢ)
+  dom∪ˡ≡∪dom = dom∪ˡ⊆∪dom , ∪dom⊆dom∪ˡ
+
 module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
   open Tx tx renaming (body to txb); open TxBody txb
   open LEnv Γ renaming (pparams to pp)
@@ -191,8 +244,8 @@ module SetoidProperties (tx : Tx) (Γ : LEnv) (s : LState) where
       cd = certDeposit dcert pp
       filter0 = filterCD dcert deps
   noGACerts (dcert@(regpool _ _) ∷ cs) deps = begin
-    filterˢ isGADeposit (dom (updateCertDeposits pp cs (deps ∪⁺ cd))) ≈⟨ noGACerts cs _ ⟩
-    filterˢ isGADeposit (dom (deps ∪⁺ cd)) ≈⟨ filter-cong dom∪⁺≡∪dom ⟩
+    filterˢ isGADeposit (dom (updateCertDeposits pp cs (deps ∪ˡ cd))) ≈⟨ noGACerts cs _ ⟩
+    filterˢ isGADeposit (dom (deps ∪ˡ cd)) ≈⟨ filter-cong (dom∪ˡ≡∪dom {m = deps} {m' = cd}) ⟩
     filterˢ isGADeposit (dom deps ∪ dom (cd ˢ )) ≈⟨ filter-hom-∪ ⟩
     filterˢ isGADeposit (dom deps) ∪ filterˢ isGADeposit (dom (cd ˢ)) ≈⟨ ∪-cong ≡ᵉ.refl filter0 ⟩
     filterˢ isGADeposit (dom deps) ∪ ∅ ≈⟨ ∪-identityʳ $ filterˢ isGADeposit (dom deps) ⟩

src/Ledger/Conway/Specification/Utxo.lagda.md

@@ -319,7 +319,9 @@ updateCertDeposits pp (reg c v ∷ certs) deposits
 updateCertDeposits pp (delegate c vd khs v ∷ certs) deposits
   = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (delegate c vd khs v) pp)
 updateCertDeposits pp (regpool kh p ∷ certs) deposits
-  = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (regpool kh p) pp)
+  -- pool deposits are not added a second time if they are already present
+  -- (reregistrations or duplicate certificates).
+  = updateCertDeposits pp certs (deposits ∪ˡ certDeposit (regpool kh p) pp)
 updateCertDeposits pp (regdrep c v a ∷ certs) deposits
   = updateCertDeposits pp certs (deposits ∪⁺ certDeposit (regdrep c v a) pp)
 updateCertDeposits pp (dereg c v ∷ certs) deposits

src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md

@@ -104,6 +104,53 @@ module _ -- ASSUMPTION --
     where open ≤-Reasoning
 
 
+  ≤certDeps∪ˡ : {d : Deposits} {(dp , c) : DepositPurpose × Coin}
+              → getCoin d ≤ getCoin (d ∪ˡ ❴ (dp , c) ❵)
+
+  ≤certDeps∪ˡ {d} {dp , c} with dp ∈? dom d
+  ... | yes dp∈ =
+      from ≤⇔<∨≈ $ inj₂ $
+        indexedSumᵛ'-cong {C = Coin} {x = d} {y = d ∪ˡ ❴ dp , c ❵} $
+        begin
+          d ˢ ≈⟨ ≡ᵉ.sym $ singleton-∈-∪ˡ {m = d} dp∈ ⟩
+          (d ∪ˡ ❴ (dp , c) ❵) ˢ
+        ∎
+    where
+      open import Relation.Binary.Structures using (IsEquivalence; IsPreorder)
+      open import Relation.Binary.Reasoning.Setoid (≡ᵉ-Setoid {A = DepositPurpose × Coin})
+      module ≡ᵉ = IsEquivalence ≡ᵉ-isEquivalence
+
+  ... | no ¬p = begin
+      getCoin d             ≤⟨ m≤m+n (getCoin d) _ ⟩
+      getCoin d + _         ≡⟨ sym $ indexedSumᵐ-∪
+                                 {X = d ᶠᵐ}
+                                 {Y = ❴ dp , c ❵ ᶠᵐ}
+                                 {f = proj₂}
+                                 (disjoint-sing ¬p)
+                             ⟩
+      indexedSumᵐ proj₂ ((d ᶠᵐ) ∪ˡᶠ (❴ dp , c ❵ ᶠᵐ))
+                            ≡⟨ sym $ indexedSumᵐ-∪ˡ-∪ˡᶠ d ❴ dp , c ❵ ⟩
+      getCoin (d ∪ˡ ❴ dp , c ❵)
+      ∎
+    where
+      open ≤-Reasoning
+      open import Relation.Binary.Structures using (IsEquivalence)
+      module ≡ᵉ = IsEquivalence ≡ᵉ-isEquivalence
+
+      disjoint-sing : dp ∉ dom d → disjoint (dom d) (dom ❴ dp , c ❵ˢ)
+      disjoint-sing dp∉d a∈d a∈sing
+        rewrite from ∈-dom-singleton-pair a∈sing = dp∉d a∈d
+
+      indexedSumᵐ-∪ˡ-∪ˡᶠ
+        : ∀ m m'
+        → indexedSumᵐ proj₂ ((m ∪ˡ m') ᶠᵐ) ≡ indexedSumᵐ proj₂ ((m ᶠᵐ) ∪ˡᶠ (m' ᶠᵐ))
+      indexedSumᵐ-∪ˡ-∪ˡᶠ m m' =
+        indexedSumᵐ-cong
+          {f = proj₂}
+          {x = (m ∪ˡ m') ᶠᵐ}
+          {y = (m ᶠᵐ) ∪ˡᶠ (m' ᶠᵐ)}
+          ≡ᵉ.refl
+
   ≤updateCertDeps : (cs : List DCert) {pp : PParams} {deposits : Deposits}
     → noRefundCert cs
     → getCoin deposits ≤ getCoin (updateCertDeposits pp cs deposits)
@@ -112,7 +159,8 @@ module _ -- ASSUMPTION --
     ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵} nrf)
   ≤updateCertDeps (delegate c _ _ v ∷ cs) {pp} {deposits} (_ All.∷ nrf) =
     ≤-trans ≤certDeps (≤updateCertDeps cs {pp} {deposits ∪⁺ ❴ CredentialDeposit c , v ❵} nrf)
-  ≤updateCertDeps (regpool _ _ ∷ cs)       (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf)
+  ≤updateCertDeps (regpool _ _ ∷ cs) {_} {deposits} (_ All.∷ nrf) =
+    ≤-trans (≤certDeps∪ˡ {d = deposits}) (≤updateCertDeps cs nrf)
   ≤updateCertDeps (retirepool _ _ ∷ cs)    (_ All.∷ nrf) = ≤updateCertDeps cs nrf
   ≤updateCertDeps (regdrep _ _ _ ∷ cs)     (_ All.∷ nrf) = ≤-trans ≤certDeps (≤updateCertDeps cs nrf)
   ≤updateCertDeps (ccreghot _ _ ∷ cs)      (_ All.∷ nrf) = ≤updateCertDeps cs nrf
@@ -188,5 +236,3 @@ module _ -- ASSUMPTION --
     balIn = balance (st ∣ txIns)
     balOut = balance (outs txb)
 ```
-
-