Prove a minimum spending condition for proposals (#375)

* first pass/sketch of minimal spending condition

* proposed representation of `removes-no-deposits`

* expose deposit-update subroutines

* add representation of "no deposits removed" as `depositsPreserved`

* define set-difference and prove its main decomposition property

* prove constant deposit sum lemma and provide access to `consumed ≡ produced` property inside proof

* improve parameter intros for the general msc inequality

* restructured proof with new outline of how proof might go

  proved all claims except one: that "new deposits" is equal to the sum of
  deposits of all proposals in txprop, where "new deposits" is the positive part
  of the change in deposits.

  ..remaining steps:
  + prove `getCoin` of union with singleton just adds the singleton
  + account for Cert deposits

* cleanup and remove unused additions to Axiom library

* remove code that duplicates stuff in the std lib

* move lemmas to Utxo.Properties

* move proofs of properties to Utxo.Properties

* remove extraneous functions/proofs

* remove unused imports and other misc. cleanup

* revise assumptions and rewrite proofs

* finish PR change requests

* remove unused utilities
   will add when needed, probably in ga-deposits PR

* remove set difference operation (not used in this PR)
   will add when needed in ga-deposits PR or babbage-refs PR

src/Axiom/Set/Map.agda

@@ -285,6 +285,9 @@ module Restrictionᵐ (sp-∈ : spec-∈ A) where
   _∣_ᶜ : Map A B → Set A → Map A B
   m ∣ X ᶜ = ⊆-map (R._∣ X ᶜ) R.ex-⊆ m
 
+  resᵐ-∅ᶜ : {M : Map A B} → (M ∣ ∅ ᶜ) ˢ ≡ᵉ M ˢ
+  resᵐ-∅ᶜ = R.res-∅ᶜ
+
   -- map only values in X
   mapValueRestricted : (B → B) → Map A B → Set A → Map A B
   mapValueRestricted f m X = mapValues f (m ∣ X) ∪ˡ m

src/Axiom/Set/Properties.agda

@@ -23,6 +23,8 @@ open import Data.List.Relation.Unary.Unique.Propositional.Properties.WithK using
 open import Data.Product using (map₂)
 open import Relation.Binary hiding (_⇔_)
 open import Relation.Binary.Lattice
+import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice as Bounded∨Semilattice
+import Relation.Binary.Lattice.Properties.JoinSemilattice as ∨Semilattice
 open import Relation.Binary.Morphism using (IsOrderHomomorphism)
 open import Data.Relation.Nullary.Decidable.Ext using (map′⇔)
 
@@ -218,6 +220,11 @@ filter-finite {X = X} {P} sp P? (l , hl) = Data.List.filter P? l , λ {a} →
 ∪-⊆ : X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z
 ∪-⊆ X⊆Z Y⊆Z = λ a∈X∪Y → [ X⊆Z , Y⊆Z ]′ (∈⇔P a∈X∪Y)
 
+⊆→∪ : X ⊆ Y → X ∪ Y ≡ᵉ Y
+⊆→∪ X⊆Y = (λ {a} x → case from ∈-∪ x of λ where
+            (inj₁ v) → X⊆Y v
+            (inj₂ v) → v) , ∪-⊆ʳ
+
 ∪-Supremum : Supremum (_⊆_ {A}) _∪_
 ∪-Supremum _ _ = ∪-⊆ˡ , ∪-⊆ʳ , λ _ → ∪-⊆
 
@@ -246,6 +253,25 @@ Set-BoundedJoinSemilattice : IsBoundedJoinSemilattice (_≡ᵉ_ {A}) _⊆_ _∪_
 Set-BoundedJoinSemilattice = record
   { isJoinSemilattice = Set-JoinSemilattice ; minimum = ∅-minimum }
 
+Set-BddSemilattice : {A : Type ℓ} → BoundedJoinSemilattice _ _ _
+Set-BddSemilattice {A} = record
+                      { Carrier = Set A
+                      ; _≈_ = _≡ᵉ_ {A}
+                      ; _≤_ = _⊆_
+                      ; _∨_ = _∪_
+                      ; ⊥ = ∅
+                      ; isBoundedJoinSemilattice = Set-BoundedJoinSemilattice
+                      }
+
+module _ {A : Type ℓ} where
+  open import Relation.Binary.Lattice.Properties.BoundedJoinSemilattice (Set-BddSemilattice {A})
+
+  ∪-identityˡ : (X : Set A) → ∅ ∪ X ≡ᵉ X
+  ∪-identityˡ = identityˡ
+
+  ∪-identityʳ : (X : Set A) → X ∪ ∅ ≡ᵉ X
+  ∪-identityʳ = identityʳ
+
 disjoint-sym : disjoint X Y → disjoint Y X
 disjoint-sym disj = flip disj
 

src/Axiom/Set/Rel.agda

@@ -171,6 +171,9 @@ module Restriction (sp-∈ : spec-∈ A) where
   res-∅ : R ∣ ∅ ≡ᵉ ∅
   res-∅ = dom-∅ res-dom
 
+  res-∅ᶜ : R ∣ ∅ ᶜ ≡ᵉ R
+  res-∅ᶜ = ex-⊆ , λ a∈R → ∈⇔P (∉-∅ , a∈R)
+
   res-ex-∪ : Decidable (_∈ X) → (R ∣ X) ∪ (R ∣ X ᶜ) ≡ᵉ R
   res-ex-∪ ∈X? = ∪-⊆ res-⊆ ex-⊆ , λ {a} h → case ∈X? (proj₁ a) of λ where
     (yes p) → ∈⇔P (inj₁ (∈⇔P (p , h)))

src/Data/Integer/Ext.agda

@@ -3,9 +3,11 @@
 module Data.Integer.Ext where
 
 open import Data.Integer
+open import Data.Integer.Properties using ([1+m]⊖[1+n]≡m⊖n)
 open import Data.Nat
 open import Data.Product
 open import Data.Sign
+open import Relation.Binary.PropositionalEquality using (_≡_; sym; cong; trans)
 
 ℤtoSignedℕ : ℤ → Sign × ℕ
 ℤtoSignedℕ x = (sign x , ∣ x ∣)
@@ -19,3 +21,9 @@ negPart : ℤ → ℕ
 negPart x with ℤtoSignedℕ x
 ... | (Sign.- , x) = x
 ... | _            = 0
+
+∸≡posPart⊖ : {m n : ℕ} → (m ∸ n) ≡ posPart (m ⊖ n)
+∸≡posPart⊖ {zero} {zero} = _≡_.refl
+∸≡posPart⊖ {zero} {ℕ.suc n} = _≡_.refl
+∸≡posPart⊖ {ℕ.suc m} {zero} = _≡_.refl
+∸≡posPart⊖ {ℕ.suc m} {ℕ.suc n} = trans (∸≡posPart⊖{m}{n}) (sym (cong posPart (([1+m]⊖[1+n]≡m⊖n m n))))

src/Ledger/Set/Theory.agda

@@ -7,7 +7,7 @@ open import Prelude
 open import Axiom.Set
 import Axiom.Set.List as L
 
-abstract
+opaque
   List-Model : Theory {0ℓ}
   List-Model = L.List-Model
   List-Modelᶠ : Theoryᶠ
@@ -24,7 +24,8 @@ open Theoryᵈ List-Modelᵈ public
 
 open import Interface.IsSet th public
 
-abstract
+opaque
+  unfolding List-Model
   open import Axiom.Set.Properties th using (card-≡ᵉ)
 
   to-sp : {A : Set} (P : A → Set) → ⦃ P ⁇¹ ⦄ → specProperty P

src/Ledger/TokenAlgebra.lagda

@@ -60,6 +60,15 @@ record TokenAlgebra : Set₁ where
   instance
     addValue : HasAdd Value
     addValue = record { _+_ = _+ᵛ_ }
+
+  coin-inject-lemma : ∀ {val} {c} → coin (val + inject c) ≡ coin val + c
+  coin-inject-lemma {val} {c} = begin
+    coin (val + inject c)         ≡⟨ homo coinIsMonoidHomomorphism val (inject c) ⟩
+    coin val + (coin ∘ inject) c  ≡⟨ cong (coin val +_) (property c) ⟩
+    coin val + c                  ∎
+    where
+    open ≡-Reasoning
+    open MonoidMorphisms.IsMonoidHomomorphism
 \end{code}
 \emph{Helper functions}
 \AgdaTarget{sumᵛ}

src/Ledger/Utxo.lagda

@@ -130,42 +130,37 @@ instance
   HasCoin-UTxO : HasCoin UTxO
   HasCoin-UTxO .getCoin = cbalance
 
-module _ (let open TxBody) where
 \end{code}
 \begin{code}
-
-  updateDeposits : PParams → TxBody → DepositPurpose ⇀ Coin → DepositPurpose ⇀ Coin
-  updateDeposits pp txb
-    = updateCertDeposits (txb .txcerts) ∘ updateProposalDeposits (txb .txprop)
-    where
-      certDeposit : DCert → DepositPurpose ⇀ Coin
-      certDeposit  (delegate c _ _ v)  = ❴ CredentialDeposit c , v                ❵
-      certDeposit  (regpool c _)       = ❴ PoolDeposit       c , pp .poolDeposit  ❵
-      certDeposit  (regdrep c v _)     = ❴ DRepDeposit       c , v                ❵
-      certDeposit  _                   = ∅
-
-      propDeposit : GovActionID → DepositPurpose ⇀ Coin
-      propDeposit gaid = ❴ GovActionDeposit gaid , pp .govActionDeposit ❵
-
-      certRefund : DCert → ℙ DepositPurpose
-      certRefund (dereg c)      = ❴ CredentialDeposit c ❵
-      certRefund (deregdrep c)  = ❴ DRepDeposit c ❵
-      certRefund _              = ∅
-
-      updateCertDeposits : List DCert → DepositPurpose ⇀ Coin → DepositPurpose ⇀ Coin
-      updateCertDeposits []              deposits = deposits
-      updateCertDeposits (cert ∷ certs)  deposits
-        = updateCertDeposits certs deposits ∪⁺ certDeposit cert ∣ certRefund cert ᶜ
-
-      updateProposalDeposits : List GovProposal → DepositPurpose ⇀ Coin
-        → DepositPurpose ⇀ Coin
-      updateProposalDeposits [] deposits = deposits
-      updateProposalDeposits (_ ∷ props) deposits
-        = updateProposalDeposits props deposits ∪⁺ propDeposit (txb .txid , length props)
-
-  depositsChange : PParams → TxBody → DepositPurpose ⇀ Coin → ℤ
-  depositsChange pp txb deposits
-    = getCoin (updateDeposits pp txb deposits) - getCoin deposits
+updateCertDeposits : PParams → List DCert → DepositPurpose ⇀ Coin → DepositPurpose ⇀ Coin
+updateCertDeposits _   []              deposits = deposits
+updateCertDeposits pp  (cert ∷ certs)  deposits
+  = (updateCertDeposits pp certs deposits ∪⁺ certDeposit cert {pp}) ∣ certRefund cert ᶜ
+  where
+  certDeposit : DCert → {pp : PParams} → DepositPurpose ⇀ Coin
+  certDeposit (delegate c _ _ v)  = ❴ CredentialDeposit c , v                ❵
+  certDeposit (regpool c _) {pp}  = ❴ PoolDeposit       c , pp .poolDeposit  ❵
+  certDeposit (regdrep c v _)     = ❴ DRepDeposit       c , v                ❵
+  certDeposit _                   = ∅
+
+  certRefund :  DCert → ℙ DepositPurpose
+  certRefund (dereg c)      = ❴ CredentialDeposit c ❵
+  certRefund (deregdrep c)  = ❴ DRepDeposit c ❵
+  certRefund _              = ∅
+
+updateProposalDeposits : List GovProposal → TxId → Coin → DepositPurpose ⇀ Coin → DepositPurpose ⇀ Coin
+updateProposalDeposits [] _ _ deposits = deposits
+updateProposalDeposits (_ ∷ ps) txid gaDep deposits =
+  updateProposalDeposits ps txid gaDep deposits ∪⁺ ❴ GovActionDeposit (txid , length ps) , gaDep ❵
+
+updateDeposits : PParams → TxBody → DepositPurpose ⇀ Coin → DepositPurpose ⇀ Coin
+updateDeposits pp txb =
+  updateCertDeposits pp txcerts ∘ updateProposalDeposits txprop txid (pp .govActionDeposit)
+  where open TxBody txb
+
+depositsChange : PParams → TxBody → DepositPurpose ⇀ Coin → ℤ
+depositsChange pp txb deposits
+  = getCoin (updateDeposits pp txb deposits) - getCoin deposits
 \end{code}
 \end{AgdaMultiCode}
 \caption{Functions used in UTxO rules}