Skip to content

[Dijkstra] (DEPRECATED) CIP-159-11c: Prove LEDGER PoV #1190

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
williamdemeo wants to merge 6 commits into from
Closed

[Dijkstra] (DEPRECATED) CIP-159-11c: Prove LEDGER PoV #1190

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
5ff53e9
[Dijkstra] CIP-159-11a: Prove Certs preservation of value (#1185)
williamdemeo May 7, 2026
22cabe9
[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187)
williamdemeo May 7, 2026
b3f5876
fix import of CERTS-PoV module
williamdemeo May 8, 2026
a691c0e
Refactor Ledger PoV proof for new symmetric CERTS-pov (CIP-159)
williamdemeo May 9, 2026
495acf3
temporarily committing old stuff before rebase
williamdemeo May 19, 2026
87f68f0
fix proofs to accommodate dd netid premises
williamdemeo May 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,7 +173,6 @@ split-by-lookup acc c bal lookup-eq =
-->



### Single-step Lemma: `applyOne` decreases `getCoin` by `amt`

When `stake addr ∈ dom acc` and `amt ≤ bal` (where `bal` is the current balance),
Expand Down
6 changes: 3 additions & 3 deletions src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,8 +62,8 @@ Equivalently, the *increase* in rewards balance from `s₁`{.AgdaBound} to

```agda
CERTS-pov : {Γ : CertEnv} {s₁ sₙ : CertState}
→ ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId
→ ∀[ a ∈ dom (DirectDepositsOf Γ) ] NetworkIdOf a ≡ NetworkId
→ (∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId)
× (∀[ a ∈ dom (DirectDepositsOf Γ) ] NetworkIdOf a ≡ NetworkId)
→ Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ
→ getCoin s₁ + getCoin (DirectDepositsOf Γ) ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)
```
Expand All @@ -75,7 +75,7 @@ plus an arithmetic shuffle to interleave the two accounting terms.

<!--
```agda
CERTS-pov {Γ = Γ} {s₁} {sₙ} validNetIdW validNetIdDD (run {s' = s'} (pre-cert , certs)) =
CERTS-pov {Γ = Γ} {s₁} {sₙ} (validNetIdW , validNetIdDD) (run {s' = s'} (pre-cert , certs)) =
begin
getCoin s₁ + cdd ≡⟨ cong (_+ cdd) (PRE-CERT-pov validNetIdW pre-cert) ⟩
getCoin s' + cwd + cdd ≡⟨ swap-right _ (cwd) (cdd) ⟩
Expand Down
37 changes: 27 additions & 10 deletions src/Ledger/Dijkstra/Specification/Ledger.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,9 @@ instance
HasEnactState-LedgerEnv : HasEnactState LedgerEnv
HasEnactState-LedgerEnv .EnactStateOf = LedgerEnv.enactState

HasTreasury-LedgerEnv : HasTreasury LedgerEnv
HasTreasury-LedgerEnv .TreasuryOf = LedgerEnv.treasury

HasPParams-SubLedgerEnv : HasPParams SubLedgerEnv
HasPParams-SubLedgerEnv .PParamsOf = SubLedgerEnv.pparams

Expand All @@ -82,9 +85,9 @@ instance

HasAccountBalances-SubLedgerEnv : HasAccountBalances SubLedgerEnv
HasAccountBalances-SubLedgerEnv .AccountBalancesOf = SubLedgerEnv.accountBalances

```
-->

```agda
record LedgerState : Type where
```
Expand All @@ -99,6 +102,7 @@ record LedgerState : Type where
govSt : GovState
certState : CertState
```

<!--
```agda
record HasLedgerState {a} (A : Type a) : Type a where
Expand Down Expand Up @@ -174,24 +178,24 @@ allColdCreds : GovState → EnactState → ℙ Credential
allColdCreds govSt es =
ccCreds (es .cc) ∪ concatMapˢ (λ (_ , st) → proposedCC (GovActionOf st)) (fromList govSt)

coinFromDeposits : CertState → Coin
coinFromDeposits certState =
getCoin (DepositsOf (DStateOf certState))
+ getCoin (DepositsOf (PStateOf certState))
+ getCoin (DepositsOf (GStateOf certState))

calculateDepositsChange : CertState → CertState → CertState → DepositsChange
calculateDepositsChange certState₀ certState₁ certState₂
= ⟦ coinChangeTop , coinChangeSub ⟧
where
coinFromDeposit : CertState → Coin
coinFromDeposit certState =
getCoin (DepositsOf (DStateOf certState))
+ getCoin (DepositsOf (PStateOf certState))
+ getCoin (DepositsOf (GStateOf certState))

coin₀ : Coin
coin₀ = coinFromDeposit certState₀
coin₀ = coinFromDeposits certState₀

coin₁ : Coin
coin₁ = coinFromDeposit certState₁
coin₁ = coinFromDeposits certState₁

coin₂ : Coin
coin₂ = coinFromDeposit certState₂
coin₂ = coinFromDeposits certState₂

coinChangeSub : ℤ
coinChangeSub = coin₁ - coin₀
Expand All @@ -200,6 +204,19 @@ calculateDepositsChange certState₀ certState₁ certState₂
coinChangeTop = coin₂ - coin₁
```

<!--
```agda
instance
HasCoin-LedgerState : HasCoin LedgerState
HasCoin-LedgerState .getCoin s =
getCoin (UTxOStateOf s) -- cbalance + fees + donations
+ getCoin (CertStateOf s) -- rewards
+ coinFromDeposits (CertStateOf s) -- deposits
```
-->



## <span class="AgdaDatatype">LEDGER</span> Transition System

<!--
Expand Down
1 change: 1 addition & 0 deletions src/Ledger/Dijkstra/Specification/Ledger/Properties.lagda.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
```
Loading
Loading