Merge pull request #973 from IntersectMBO/fd/reregistration-deposits

Don't count pool deposits when reregistering pools

Author: facundominguez

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.
@@ -701,6 +701,27 @@ See [the `conformance-example` directory][conformance-example].
 ## 🗃️ Miscellanea
 
 
+### Updating Agda dependencies in the Nix configuration
+
+The following example ilustrates the procedure
+
+```
+nix flake update agda-nix/abstract-set-theory \
+  --override-input agda-nix/abstract-set-theory \
+  github:input-output-hk/agda-sets/bbaa00abc4aef061896ae5d3cdec148bfbf5029f
+nix build ./#fls-agdaWithPackages -o ~/ledger-agda
+```
+
+The first line updates the commit hash to use for a dependency. In the example,
+it updates the dependency `agda-nix/abstract-set-theory` to point at the commit
+`bbaa00abc4aef061896ae5d3cdec148bfbf5029f` or the repository
+`github:input-output-hk/agda-sets`.
+
+The second line rebuilds the Agda mode to use with emacs. This step is necessary
+for emacs to use the new version of the dependency when loading Agda code. This
+assumes that `~/ledger-agda/bin` is in your `PATH`.
+
+
 ### Plotting typechecking times
 
 The script `scripts/plot_typecheck_time.py` can be used to generate an `html`

flake.lock

@@ -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/Deposits.agda

@@ -2,9 +2,8 @@
 
 module Ledger.Conway.Conformance.Equivalence.Map where
 
-open import Ledger.Prelude
+open import Ledger.Prelude hiding (filterᵐ-singleton-false)
 open import Axiom.Set.Properties th
-open import Axiom.Set.Map.Dec
 
 import Algebra as Alg
 import Algebra.Definitions as AlgDefs
@@ -614,6 +613,8 @@ module _  {A B : Type}
       filterᵐ-singleton-true p .proj₁ = proj₂ ∘ (from ∈-filter)
       filterᵐ-singleton-true {k}{v} p .proj₂ {a} x = to ∈-filter (subst P′ (sym (from ∈-singleton x)) p , x)
 
+      -- TODO: move to agda-sets
+      -- https://github.com/input-output-hk/agda-sets/pull/19
       filterᵐ-singleton-false : ¬ P k → filterᵐ P′ ❴ k , v ❵ ≡ᵐ ∅
       filterᵐ-singleton-false ¬p .proj₁ x =
         ⊥-elim $ ¬p $ subst P′ (from ∈-singleton $ proj₂ (from ∈-filter x)) (proj₁ $ from ∈-filter x)
@@ -656,5 +657,33 @@ module _  {A B : Type}
       lem-add-excluded p =
         filterᵐ-∪⁺-distr _ _ ⟨≈⟩ ∪⁺-cong-l (filterᵐ-singleton-false p) ⟨≈⟩ ∪⁺-id-r _
 
+      -- TODO: move to agda-sets
+      -- https://github.com/input-output-hk/agda-sets/pull/19
+      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/Conformance/Equivalence/Map.agda

@@ -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/Epoch/Properties/GovDepsMatch.lagda.md

@@ -113,6 +113,7 @@ 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₁
 
+
 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 +192,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/Ledger/Properties/Base.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.lagda.md

@@ -104,6 +104,41 @@ 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ᵐ-∪ˡ-∪ˡᶠ {B = ⊤} d ❴ dp , c ❵ ⟩
+      getCoin (d ∪ˡ ❴ dp , c ❵)
+      ∎
+    where
+      open ≤-Reasoning
+
+      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
+
   ≤updateCertDeps : (cs : List DCert) {pp : PParams} {deposits : Deposits}
     → noRefundCert cs
     → getCoin deposits ≤ getCoin (updateCertDeposits pp cs deposits)
@@ -112,7 +147,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 +224,3 @@ module _ -- ASSUMPTION --
     balIn = balance (st ∣ txIns)
     balOut = balance (outs txb)
 ```
-
-