temporarily committing old stuff before rebase

Author: williamdemeo

src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md

@@ -118,12 +118,12 @@ intermediate stage of the main chain.
 To close, add `Σ directDeps_i` to both sides of the goal (eliminated at the end via
 `+-cancelʳ-≡`):
 
-    (U₀ + R₀ + D₀) + Σ directDeps_i
+    U₀ + R₀ + D₀ + Σ directDeps_i
     ≡ U₀ + (R₀ + Σ directDeps_i) + D₀
     ≡ U₀ + (R₂ + Σ wdrls_i) + D₀               by (2)
     ≡ U₀ + Σ wdrls_i + D₀ + R₂                 (rearrange)
     ≡ U₂ + Σ directDeps_i + D₂ + R₂            by (★)
-    ≡ (U₂ + R₂ + D₂) + Σ directDeps_i          (rearrange)
+    ≡ U₂ + R₂ + D₂ + Σ directDeps_i          (rearrange)
 
 
 ### `LEDGER-I` proof outline
@@ -163,9 +163,6 @@ module _
 
   ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn) → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) )
 
-  -- New CIP-159 assumption (forwarded to Certs-Pov-lemmas): see PoVLemmas.
-  ( indexedSumᵛ'-∪⁺ : ∀ (m m' : Rewards) → getCoin (m ∪⁺ m') ≡ getCoin m + getCoin m' )
-
   -- Per-step SUBUTXOW coin equation.  Assumed for now; a local proof
   -- would require, in addition to `balance-∪` and `split-balance`, a
   -- batch-wide "spend inputs preserved" invariant (the running UTxO
@@ -201,26 +198,35 @@ module _
       → subΓ ⊢ s ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoSt₁ , govSt₁ , certState₁ ⟧ˡ
       → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf utxoSt₁)) )
 
-  -- Deposit-change posPart/negPart identity.  Provable from the definition
-  -- of `calculateDepositsChange` and the standard
-  -- `y + posPart (x - y) ≡ x + negPart (x - y)` lemma (per-component, then
-  -- composed across top and sub).  Deferred to the follow-up PR.
-  ( posNeg-deposits : (cs₀ cs₁ cs₂ : CertState)
-      → let dc = calculateDepositsChange cs₀ cs₁ cs₂ in
-        coinFromDeposits cs₀ + posPart (DepositsChangeTopOf dc) + posPart (DepositsChangeSubOf dc)
-        ≡ coinFromDeposits cs₂ + negPart (DepositsChangeTopOf dc) + negPart (DepositsChangeSubOf dc) )
-
-  -- Sum distribution (standard list algebra):
-  ( sum-map-+ : ∀ {A : Type} (f g : A → ℕ) (xs : List A)
-      → sum (map (λ x → f x + g x) xs) ≡ sum (map f xs) + sum (map g xs) )
-
   where
-  open Certs-PoV ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique indexedSumᵛ'-∪⁺
+  open Certs-PoV ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique
   -- Note: The `λ {u}{u'} →` η-wrapper may be needed for Agda eta-expansion issue.
 
   open UTXOW-PoV tx (λ {u} {u'} → balance-∪ {u} {u'}) split-balance noMintTx noMintSubTx (λ {u} → outs-disjoint {u})
   open ≡-Reasoning
 
+  posNeg-deposits : (cs₀ cs₁ cs₂ : CertState)
+    → let dc = calculateDepositsChange cs₀ cs₁ cs₂ in
+      coinFromDeposits cs₀ + posPart (DepositsChangeTopOf dc) + posPart (DepositsChangeSubOf dc)
+      ≡ coinFromDeposits cs₂ + negPart (DepositsChangeTopOf dc) + negPart (DepositsChangeSubOf dc)
+  posNeg-deposits cs₀ cs₁ cs₂ = begin
+      coin₀ + pt + psp   ≡⟨ swap-right coin₀ pt psp ⟩
+      coin₀ + psp + pt   ≡⟨ cong (_+ pt) (posPart-negPart-sym coin₁ coin₀) ⟩
+      coin₁ + ns + pt   ≡⟨ swap-right coin₁ ns pt ⟩
+      coin₁ + pt + ns   ≡⟨ cong (_+ ns) (posPart-negPart-sym coin₂ coin₁) ⟩
+      coin₂ + nt + ns   ∎
+    where
+    open ≡-Reasoning
+    coin₀ = coinFromDeposits cs₀
+    coin₁ = coinFromDeposits cs₁
+    coin₂ = coinFromDeposits cs₂
+    psp = posPart (coin₁ ⊖ coin₀)   -- DepositsChangeSubOf dc
+    ns = negPart (coin₁ ⊖ coin₀)
+    pt = posPart (coin₂ ⊖ coin₁)   -- DepositsChangeTopOf dc
+    nt = negPart (coin₂ ⊖ coin₁)
+    swap-right : ∀ a b c → a + b + c ≡ a + c + b
+    swap-right a b c = trans (+-assoc a b c) (trans (cong (a +_) (+-comm b c)) (sym (+-assoc a c b)))
+
   -- Per-sub-tx withdrawal totals.
   wdrwl : SubLevelTx → Coin
   wdrwl = getCoin ∘ WithdrawalsOf
@@ -334,7 +340,7 @@ module _
     -- Sub-level CERTS-pov (NEW signature: dd on LHS, wdrl on RHS).
     sub-certs : getCoin (CertStateOf s₀) + getCoin (DirectDepositsOf stx)
                 ≡ getCoin (CertStateOf s₁) + getCoin (WithdrawalsOf stx)
-    sub-certs = CERTS-pov (extract-subutxo-netId subutxowStep) certsStep
+    sub-certs = ? -- CERTS-pov (extract-subutxo-netId subutxowStep) certsStep
 
     -- IH: same form as the outer goal, just one element shorter.
     ih : getCoin (CertStateOf s₁) + sum (map ddwl sigs)

src/Ledger/Prelude.lagda.md

@@ -59,7 +59,7 @@ open import Data.Integer using (0ℤ) public
 import Data.Rational as ℚ
 open import Data.Rational using (ℚ)
 
-open import Data.Nat.Properties using (+-identityʳ)
+open import Data.Nat.Properties using (+-identityʳ; +-comm; +-assoc)
 
 
 dec-de-morgan : ∀{P Q : Type} → ⦃ P ⁇ ⦄ → ¬ (P × Q) → ¬ P ⊎ ¬ Q
@@ -115,6 +115,17 @@ 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))
 
+
++-interleave : {a b c d : ℕ} → a + b + (c + d) ≡ a + c + (b + d)
++-interleave {a}{b}{c}{d} = begin
+  a + b + (c + d)  ≡⟨ +-assoc a b (c + d) ⟩
+  a + (b + (c + d))  ≡⟨ cong (a +_) (sym (+-assoc b c d)) ⟩
+  a + (b + c + d)    ≡⟨ cong (λ y → a + (y + d)) (+-comm b c) ⟩
+  a + (c + b + d)    ≡⟨ cong (a +_) (+-assoc c b d) ⟩
+  a + (c + (b + d))  ≡⟨ sym (+-assoc a c (b + d)) ⟩
+  a + c + (b + d)  ∎
+  where open ≡-Reasoning
+
 module _ {A : Type} ⦃ _ : DecEq A ⦄ where
 
   getCoin-singleton : {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c
@@ -154,6 +165,16 @@ module _ {A : Type} ⦃ _ : DecEq A ⦄ where
   ... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom
   ... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m))
 
+sum-map-+ : ∀ {A : Type} (f g : A → ℕ) (xs : List A)
+  → sum (map (λ x → f x + g x) xs) ≡ sum (map f xs) + sum (map g xs)
+sum-map-+ _ _ [] = refl
+sum-map-+ f g (x ∷ xs) =
+  begin
+  f x + g x + sum (map (λ x → f x + g x) xs)    ≡⟨ cong (f x + g x +_) (sum-map-+ f g xs) ⟩
+  f x + g x + (sum (map f xs) + sum (map g xs)) ≡⟨ +-interleave {f x} ⟩
+  f x + sum (map f xs) + (g x + sum (map g xs)) ∎
+  where open ≡-Reasoning
+
 opaque
   unfolding List-Model finiteness
 

src/Prelude.lagda.md

@@ -103,10 +103,13 @@ instance
   ~? {A} {x} {y} ⦃ deqEq ⦄ = ⁇ (connected? (DecEq._≟_ deqEq) x y)
 
 -- Positive and negative part of integers
-open import Data.Integer using (sign; ∣_∣; _⊖_)
+open import Data.Integer using (_⊖_) public
+open import Data.Integer using (sign; ∣_∣)
 open import Data.Integer.Properties using ([1+m]⊖[1+n]≡m⊖n)
 open import Data.Sign using (Sign)
 
+open import Data.Nat.Properties using (m+[n∸m]≡n; m≤n⇒m∸n≡0; ≤-total; +-identityʳ)
+
 posPart : ℤ → ℕ
 posPart x with sign x
 ... | Sign.+ = ∣ x ∣
@@ -123,6 +126,33 @@ negPart x with sign x
 ∸≡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))))
 
+∸≡negPart⊖ : {m n : ℕ} → (n ∸ m) ≡ negPart (m ⊖ n)
+∸≡negPart⊖ {zero}  {zero}  = refl
+∸≡negPart⊖ {zero}  {ℕ.suc n} = refl
+∸≡negPart⊖ {ℕ.suc m} {zero}  = refl
+∸≡negPart⊖ {ℕ.suc m} {ℕ.suc n} =
+  trans (∸≡negPart⊖ {m} {n})
+        (sym (cong negPart ([1+m]⊖[1+n]≡m⊖n m n)))
+
++∸≡∸+ : (a b : ℕ) → a +ℕ (b ∸ a) ≡ b +ℕ (a ∸ b)
++∸≡∸+ a b with ≤-total a b
+... | inj₁ a≤b =
+  trans (m+[n∸m]≡n a≤b)
+        (sym (trans (cong (b +ℕ_) (m≤n⇒m∸n≡0 a≤b)) (+-identityʳ b)))
+... | inj₂ b≤a =
+  trans (cong (a +ℕ_) (m≤n⇒m∸n≡0 b≤a))
+        (trans (+-identityʳ a) (sym (m+[n∸m]≡n b≤a)))
+
+-- y + posPart (x ⊖ y) ≡ x + negPart (x ⊖ y)
+posPart-negPart-sym : ∀ x y → y +ℕ posPart (x ⊖ y) ≡ x +ℕ negPart (x ⊖ y)
+posPart-negPart-sym x y = let _+_ = _+ℕ_ in
+  begin
+    y + posPart (x ⊖ y)  ≡⟨ cong (y +_) (sym (∸≡posPart⊖ {x} {y})) ⟩
+    y + (x ∸ y)          ≡⟨ +∸≡∸+ y x ⟩
+    x + (y ∸ x)          ≡⟨ cong (x +_) (∸≡negPart⊖ {x} {y}) ⟩
+    x + negPart (x ⊖ y)  ∎
+  where open ≡-Reasoning
+
 instance
   Dec-NonZero : ∀ {n} → NonZero n ⁇
   Dec-NonZero {zero} .dec = no λ ()