Don't count pool deposits when reregistering pools #973
Conversation
| open import Relation.Binary.Reasoning.PartialOrder ⊆-Poset | ||
| open import Relation.Binary.Structures using (IsEquivalence) | ||
| module ≡ᵉA = IsEquivalence (≡ᵉ-isEquivalence {A = A}) | ||
| open import Relation.Binary.Reasoning.Syntax | ||
| open ⊆-syntax _IsRelatedTo_ _IsRelatedTo_ ≤-go public |
There was a problem hiding this comment.
The setup is longer than the proof. Maybe we should create a module
Axiom.Set.Reasoning to reexport these?
There was a problem hiding this comment.
Another option is just to use the same style as in the proofs below:
dom∪ˡˡ a∈ = begin→ a∈ $
a ∈ dom (m ˢ) →⟨ ∪-⊆ˡ ⟩
a ∈ dom (m ˢ) ∪ dom (rhs-∪ˡ ˢ) →⟨ proj₂ dom∪ ⟩
a ∈ dom ((m ˢ) ∪ (rhs-∪ˡ ˢ)) →⟨ id ⟩
a ∈ dom ((m ∪ˡ m') ˢ)
∎→There was a problem hiding this comment.
In the latest version I rewrote this with Function.Reasoning._|>_:. Thanks to @javierdiaz72 for pointing it.
@WhatisRT suggested using EquivalenceReasoning from Function.Related.Propositional, but I couldn't figure out how to use it with implication yet.
dom∪ˡˡ {a} a∈ = a∈ |> id ∶
a ∈ dom (m ˢ) |> ∪-⊆ˡ ∶
a ∈ dom (m ˢ) ∪ dom (rhs-∪ˡ ˢ) |> proj₂ dom∪ ∶
a ∈ dom ((m ˢ) ∪ (rhs-∪ˡ ˢ)) |> id ∶
a ∈ dom ((m ∪ˡ m') ˢ)
| _∎→ : ∀ (A : Type) → A → A | ||
| A ∎→ = id | ||
| infix 3 _∎→ | ||
|
|
||
| _→⟨_⟩_ : ∀ (x : Type) {y z : Type} → (x → y) → (y → z) → x → z | ||
| _ →⟨ f ⟩ g = g ∘ f | ||
| infixr 2 _→⟨_⟩_ | ||
|
|
||
| begin→ : ∀ {A B : Type} → A → (A → B) → B | ||
| begin→ a f = f a |
There was a problem hiding this comment.
These are used in the proofs below. Do they belong here or in some more general place?
facundominguez
force-pushed
the
fd/reregistration-deposits
branch
3 times, most recently
from
8f29a25 to
7a868c3
Compare
facundominguez
force-pushed
the
fd/reregistration-deposits
branch
4 times, most recently
from
90c7453 to
5f87d42
Compare
carlostome
left a comment
carlostome
left a comment
There was a problem hiding this comment.
LGTM
I'd suggest to move the auxiliary lemmata that belongs to agda-sets to src-lib-exts/agda-sets to (1) not clutter main files, and (2) contain those definitions that do not really belong to ledger in a specific place.
williamdemeo
left a comment
williamdemeo
left a comment
There was a problem hiding this comment.
This all looks good. I just pushed one small fix to mkdocs site (correct nav toc to reflect new location of Test module).
|
I should have just created a separate issue and small PR to fix the nav toc issue instead of pushing the fix to your PR. (Sorry!) I'm creating the "mkdocs nav fix" PR now and hoping that if we merge that into master first, then rebase your PR on master, there won't be any serious conflicts and the nav issue will be resolved. |
Reducing the scope of the equation in which POOLREAP is pattern matched reduces type checking time an order of magnitude.
facundominguez
force-pushed
the
fd/reregistration-deposits
branch
from
5688a2b to
40e4a82
Compare
|
I rebased master and updated agda-sets. Maybe this is ready to merge now. |
…n the Nix configuration
carlostome
left a comment
carlostome
left a comment
There was a problem hiding this comment.
Looks good to go modulo removing those lemmas that correspond to the PR input-output-hk/agda-sets#19
|
I think it is better to merge this now and continue the work on moving proofs to agda-sets in other PRs. Or at least, I don't see the benefit of putting everything together in a single PR. It is looking like more contributions need to be done in |
3 participants
This PR modifies updates
updateCertDepositsso pool deposits are not counted again when reregistering a pool. This is the function used by the UTXO rule to update deposits.The change to the function is fairly simple, but then there are a few broken proofs that are fixed in later commits.