CIP-159-11: LEDGER-pov fully structured, all holes filled (#1123)

Complete the LEDGER preservation-of-value proof structure for Dijkstra.

- LEDGER-I: Fully proved via utxow-pov-invalid.
- LEDGER-V: Complete equational chain with no holes or unresolved metas.
  Decomposes into:
  - step-i: combined CERTS accounting (sub + top level)
  - arithmetic-1, arithmetic-2: ℕ rearrangements
  - step-iii-iv: batch UTxO + deposit accounting (assumption)
  - step-ii: applyDirectDeposits cancellation (assumption)

New sub-lemma proved:
- SUBLEDGERS-certs-pov: induction on ReflexiveTransitiveClosure showing
  rewardsBalance decreases by exactly the sum of sub-withdrawal amounts.
  Dispatches SUBLEDGER-I (impossible when isTopLevelValid ≡ true) and
  SUBLEDGER-V (uses sub-level CERTS-pov with NetworkId extracted from
  SUBUTXOW → SUBUTXO premises).

Remaining assumptions (module parameters):
- batch-utxo-accounting: consumedBatch ≡ producedBatch coin projection
  combined with mechanical UTxO tracking and deposit accounting
- applyDirectDeposits-rewardsBalance: gc-hom (∪⁺ distributes getCoin)
- utxow-pov-invalid: collateral collection preserves getCoin utxoSt
- ∪ˡ-res-lookup-preserve, sum-map-proj₂≡getCoin, setToList-Unique

Author: williamdemeo

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

@@ -14,4 +14,5 @@ module Ledger.Dijkstra.Specification.Ledger.Properties where
 
 ```agda
 open import Ledger.Dijkstra.Specification.Ledger.Properties.Computational
+open import Ledger.Dijkstra.Specification.Ledger.Properties.PoV
 ```

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

@@ -169,6 +169,32 @@ So
 
 <!--
 ```agda
+-- Batch accounting: the coin projection of consumedBatch ≡ producedBatch,
+-- combined with mechanical UTxO tracking and deposit accounting,
+-- gives us the full value preservation for the valid case.
+--
+BatchUtxoAccounting : Type
+BatchUtxoAccounting =
+  {tx : TopLevelTx} {Γ : LedgerEnv} {s : LedgerState} {utxoSt₁ : UTxOState} {certState₁ certState₂ : CertState}
+  {govSt₁ : GovState} {utxoSt₂ : UTxOState}
+  → let
+      utxo₀ = UTxOOf (UTxOStateOf s)
+      dc = calculateDepositsChange (CertStateOf s) certState₁ certState₂
+      subWdrlsCoin : Coin
+      subWdrlsCoin = sum (map (λ (stx : SubLevelTx) → getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx))
+      allWdrls = getCoin (WithdrawalsOf tx) + subWdrlsCoin
+      allDirectDeps = getCoin (allDirectDeposits tx)
+    in
+      ⟦ LedgerEnv.slot Γ , PParamsOf Γ , TreasuryOf Γ , utxo₀ , dc
+      , getAllScripts tx utxo₀
+      , setToMap (mapˢ < hash , id > (getAllData tx))
+      , RewardsOf (CertStateOf s) ⟧ ⊢ utxoSt₁ ⇀⦇ tx ,UTXOW⦈ utxoSt₂
+      -- SUBLEDGERS step (needed to relate utxoSt₀ to utxoSt₁):
+      → ∀ {subΓ : SubLedgerEnv}
+      → subΓ ⊢ s ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoSt₁ , govSt₁ , certState₁ ⟧ˡ
+      → getCoin (UTxOStateOf s) + allWdrls + coinFromDeposits (CertStateOf s)
+        ≡ getCoin utxoSt₂ + allDirectDeps + coinFromDeposits certState₂
+
 module _
   (tx : TopLevelTx) (let open Tx tx)
 
@@ -187,27 +213,9 @@ module _
       (dd : DirectDeposits) (ds : DState)
       → rewardsBalance (applyDirectDeposits dd ds) ≡ rewardsBalance ds + getCoin dd )
 
-  -- Batch accounting: the coin projection of consumedBatch ≡ producedBatch,
-  -- combined with mechanical UTxO tracking and deposit accounting,
-  -- gives us the full value preservation for the valid case.
-  --
-  -- This lemma encapsulates steps 1, 3, and 4 from the outline:
-  -- it relates the UTxO-side change to withdrawals, direct deposits,
-  -- and deposit changes.
-  ( batch-utxo-accounting :
-      ∀ {Γ : LedgerEnv} {s : LedgerState}
-        {utxoSt₁ : UTxOState} {certState₁ certState₂ : CertState}
-        {govSt₁ : GovState} {utxoSt₂ : UTxOState}
-      → let depositsChange = calculateDepositsChange (CertStateOf s) certState₁ certState₂
-        in
-        -- From UTXOW (which wraps UTXO with consumedBatch ≡ producedBatch):
-        ⟦ LedgerEnv.slot Γ , PParamsOf Γ , TreasuryOf Γ , UTxOOf (UTxOStateOf s)
-        , depositsChange , getAllScripts tx (UTxOOf (UTxOStateOf s))
-        , setToMap (mapˢ < hash , id > (getAllData tx))
-        , RewardsOf (CertStateOf s) ⟧ ⊢ utxoSt₁ ⇀⦇ tx ,UTXOW⦈ utxoSt₂
-      → getCoin utxoSt₁ + getCoin (WithdrawalsOf tx)
-        ≡ getCoin utxoSt₂ + getCoin (allDirectDeposits tx)
-          + (coinFromDeposits certState₂ ∸ coinFromDeposits (CertStateOf s)) )
+  -- Assumption (for now) encapsulating steps 1, 3, and 4 from the outline:
+  -- relates UTxO-side change to withdrawals, direct deposits, and deposit changes.
+  ( batch-utxo-accounting : BatchUtxoAccounting )
 
   -- LEDGER-I: collateral collection preserves getCoin utxoSt
   ( utxow-pov-invalid :
@@ -220,6 +228,50 @@ module _
     open Certs-PoV ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique
     open ≡-Reasoning
 
+
+    SUBLEDGERS-certs-pov :
+      ∀ {Γ : SubLedgerEnv} {s₀ s₁ : LedgerState} {stxs : List SubLevelTx}
+      → SubLedgerEnv.isTopLevelValid Γ ≡ true
+      → Γ ⊢ s₀ ⇀⦇ stxs ,SUBLEDGERS⦈ s₁
+      → getCoin (CertStateOf s₀)
+        ≡ getCoin (CertStateOf s₁) + sum (map (λ (stx : SubLevelTx) → getCoin (WithdrawalsOf stx)) stxs)
+
+    -- Base case: empty list, getCoin cs₀ ≡ getCoin cs₀ + 0
+    SUBLEDGERS-certs-pov isV (BS-base Id-nop) = sym (+-identityʳ _)
+
+    -- Inductive step: one SUBLEDGER step + rest
+    SUBLEDGERS-certs-pov {Γ} isV (BS-ind {s = s₀} {s' = s₁} {sigs} {s'' = sₙ} step rest) with step
+    ... | SUBLEDGER-I (isI , _) = ⊥-elim (case trans (sym isV) isI of λ ())
+    ... | SUBLEDGER-V {stx = stx} (isV' , subutxowStep , certsStep , govsStep) =
+      let f = λ (stx : SubLevelTx) → getCoin (WithdrawalsOf stx)
+      in
+      begin
+        getCoin (CertStateOf s₀)
+          ≡⟨ sub-certs ⟩
+        getCoin (CertStateOf s₁) + getCoin (WithdrawalsOf stx)
+          ≡⟨ cong (_+ getCoin (WithdrawalsOf stx)) ih ⟩
+        (getCoin (CertStateOf sₙ) + sum (map f sigs)) + getCoin (WithdrawalsOf stx)
+          ≡⟨ +-assoc (getCoin (CertStateOf sₙ)) _ _ ⟩
+        getCoin (CertStateOf sₙ) + (sum (map f sigs) + getCoin (WithdrawalsOf stx))
+          ≡⟨ cong (getCoin (CertStateOf sₙ) +_) (+-comm _ (getCoin (WithdrawalsOf stx))) ⟩
+        getCoin (CertStateOf sₙ) + (getCoin (WithdrawalsOf stx) + sum (map f sigs))
+          ∎
+      where
+      extract-subutxo-netId : ∀ {Γ' s₀' s₁'} → Γ' ⊢ s₀' ⇀⦇ stx ,SUBUTXOW⦈ s₁'
+            → ∀[ a ∈ dom (WithdrawalsOf stx) ] NetworkIdOf a ≡ NetworkId
+      extract-subutxo-netId (SUBUTXOW (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , SUBUTXO (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , netId , _))) = netId
+
+      wdrl-netId : ∀[ a ∈ dom (WithdrawalsOf stx) ] NetworkIdOf a ≡ NetworkId
+      wdrl-netId = extract-subutxo-netId subutxowStep -- extract from subutxowStep → SUBUTXOW → SUBUTXO premise 11
+
+      -- Sub-level CERTS-pov
+      sub-certs : getCoin (CertStateOf s₀) ≡ getCoin (CertStateOf s₁) + getCoin (WithdrawalsOf stx)
+      sub-certs = CERTS-pov wdrl-netId certsStep
+
+      -- IH
+      ih : getCoin (CertStateOf s₁) ≡  getCoin (CertStateOf sₙ)
+                                       + sum (map (λ (stx : SubLevelTx) → getCoin (WithdrawalsOf stx)) sigs)
+      ih = SUBLEDGERS-certs-pov isV rest
 ```
 -->
 
@@ -267,31 +319,91 @@ where `certStateFinal = record certState₂ { dState = applyDirectDeposits (allD
       certStateFinal : CertState
       certStateFinal = record cs₂ { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf cs₂) }
 
+      subWdrlsCoin : Coin
+      subWdrlsCoin = sum (map (λ (stx : SubLevelTx) → getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx))
+
       allWdrls : Coin
-      allWdrls = getCoin(WithdrawalsOf tx) + {!!} -- Σ getCoin(subWdrls_i)
+      allWdrls = getCoin (WithdrawalsOf tx) + subWdrlsCoin
 
       allDirectDeps : Coin
-      allDirectDeps = getCoin(allDirectDeposits tx)
+      allDirectDeps = getCoin (allDirectDeposits tx)
 
+      extract-utxo-netId : ∀ {Γ' s₀' s₁'} → Γ' ⊢ s₀' ⇀⦇ tx ,UTXOW⦈ s₁'
+        → ∀[ a ∈ dom (WithdrawalsOf tx) ] NetworkIdOf a ≡ NetworkId
+      extract-utxo-netId (UTXOW-normal-⋯ _ _ _ _ _ _ _ _ _ _ (UTXO (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , netId , _))) = netId
+      extract-utxo-netId (UTXOW-legacy-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ (UTXO (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , netId , _))) = netId
 
       -- combined CERTS: rewardsBalance₀ = rewardsBalance₂ + allWdrls
+      combined-certs : getCoin (CertStateOf s) ≡ getCoin cs₂ + allWdrls
+      combined-certs =
+        let
+          sub = SUBLEDGERS-certs-pov valid subStep
+          top-wdrl-netId : ∀[ a ∈ dom (WithdrawalsOf tx) ] NetworkIdOf a ≡ NetworkId
+          top-wdrl-netId = extract-utxo-netId utxoStep
+          top = CERTS-pov top-wdrl-netId certStep
+        in begin
+          getCoin (CertStateOf s)              ≡⟨ sub ⟩
+          getCoin cs₁ + subWdrlsCoin           ≡⟨ cong (_+ subWdrlsCoin) top ⟩
+          (getCoin cs₂ + getCoin (WithdrawalsOf tx)) + subWdrlsCoin
+            ≡⟨ +-assoc (getCoin cs₂) _ subWdrlsCoin ⟩
+          getCoin cs₂ + (getCoin (WithdrawalsOf tx) + subWdrlsCoin)
+            ∎
+
       step-i : getCoin (UTxOStateOf s) + rewardsBalance (DStateOf (CertStateOf s)) + coinFromDeposits (CertStateOf s)
                ≡ getCoin (UTxOStateOf s) + rewardsBalance (DStateOf cs₂) + allWdrls + coinFromDeposits (CertStateOf s)
-      step-i = {!!}
+      step-i =
+        let a  = getCoin (UTxOStateOf s)
+            b  = rewardsBalance (DStateOf (CertStateOf s))
+            b₂ = rewardsBalance (DStateOf cs₂)
+            c  = coinFromDeposits (CertStateOf s)
+        in
+          begin
+          a + b + c                 ≡⟨ cong (λ x → a + x + c) combined-certs ⟩
+          a + (b₂ + allWdrls) + c   ≡⟨ cong (_+ c) (sym (+-assoc a b₂ allWdrls)) ⟩
+          a + b₂ + allWdrls + c     ∎
 
-      arithmetic-1 :  getCoin (UTxOStateOf s) + rewardsBalance (DStateOf cs₂) + allWdrls + coinFromDeposits (CertStateOf s)
-                      ≡ getCoin (UTxOStateOf s) + allWdrls + coinFromDeposits (CertStateOf s) + rewardsBalance (DStateOf cs₂)
-      arithmetic-1 = {!!}
       -- deposit accounting + batch UTxO combined
       step-iii-iv :  getCoin (UTxOStateOf s) + allWdrls + coinFromDeposits (CertStateOf s) + rewardsBalance (DStateOf cs₂)
                      ≡ getCoin us₂ + allDirectDeps + coinFromDeposits cs₂ + rewardsBalance (DStateOf cs₂)
-      step-iii-iv = {!!}
+      step-iii-iv = cong (_+ rewardsBalance (DStateOf cs₂)) (batch-utxo-accounting {Γ = Γ} {certState₂ = cs₂} utxoStep  subStep)
+
+      arithmetic-1 :
+        getCoin (UTxOStateOf s) + rewardsBalance (DStateOf cs₂) + allWdrls + coinFromDeposits (CertStateOf s)
+        ≡ getCoin (UTxOStateOf s) + allWdrls + coinFromDeposits (CertStateOf s) + rewardsBalance (DStateOf cs₂)
+      arithmetic-1 =
+        let a = getCoin (UTxOStateOf s)
+            b = rewardsBalance (DStateOf cs₂)
+            c = allWdrls
+            d = coinFromDeposits (CertStateOf s)
+        in begin
+          a + b + c + d         ≡⟨ cong (_+ d) (+-assoc a b c) ⟩
+          a + (b + c) + d       ≡⟨ cong (λ x → a + x + d) (+-comm b c) ⟩
+          a + (c + b) + d       ≡⟨ cong (_+ d) (sym (+-assoc a c b)) ⟩
+          (a + c) + b + d       ≡⟨ +-assoc (a + c) b d ⟩
+          (a + c) + (b + d)     ≡⟨ cong ((a + c) +_) (+-comm b d) ⟩
+          (a + c) + (d + b)     ≡⟨ sym (+-assoc (a + c) d b) ⟩
+          a + c + d + b         ∎
 
       arithmetic-2 : getCoin us₂ + allDirectDeps + coinFromDeposits cs₂ + rewardsBalance (DStateOf cs₂)
                      ≡ getCoin us₂ + (rewardsBalance (DStateOf cs₂) + allDirectDeps) + coinFromDeposits cs₂
-      arithmetic-2 = {!!}
+      arithmetic-2 =
+        let a = getCoin us₂
+            b = allDirectDeps
+            c = coinFromDeposits cs₂
+            d = rewardsBalance (DStateOf cs₂)
+        in
+        begin
+          a + b + c + d       ≡⟨ +-assoc (a + b) c d ⟩
+          a + b + (c + d)     ≡⟨ cong ((a + b) +_) (+-comm c d) ⟩
+          a + b + (d + c)     ≡⟨ sym (+-assoc (a + b) d c) ⟩
+          a + b + d + c       ≡⟨ cong (_+ c) (+-assoc a b d) ⟩
+          a + (b + d) + c     ≡⟨ cong (λ x → a + x + c) (+-comm b d) ⟩
+          a + (d + b) + c     ∎
+
       -- applyDirectDeposits-rewardsBalance
       step-ii : getCoin us₂ + (rewardsBalance (DStateOf cs₂) + allDirectDeps) + coinFromDeposits cs₂
                 ≡ getCoin us₂ + getCoin certStateFinal + coinFromDeposits cs₂
-      step-ii = {!!}
+      step-ii = cong (λ x → getCoin us₂ + x + coinFromDeposits cs₂)
+                     (sym (applyDirectDeposits-rewardsBalance (allDirectDeposits tx) (DStateOf cs₂)))
+
 ```