From 08be6b495d6bbafc5aaed9e4caa350666f7ddde6 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Sat, 11 Apr 2026 18:56:59 -0600 Subject: [PATCH 01/14] [Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`), apply batch-wide direct deposits to the final CertState via `applyDirectDeposits` and `allDirectDeposits`. `Ledger.lagda.md`: + Update `LEDGER-V` output: compute `certStateFinal` by applying `allDirectDeposits` to `certState₂`, use `certStateFinal` in the output `LedgerState` and in `rmOrphanDRepVotes`; + `LEDGER-I` unchanged (invalid batches don't apply deposits); + Document direct deposit application ordering and phantom asset prevention rationale. `Ledger/Properties/Computational.lagda.md`: + Update `computeProof` valid branch to compute `certStateFinal` and use it in the output `LedgerState`. + Clean up redundant code. --- CHANGELOG.md | 1 + .../Dijkstra/Specification/Ledger.lagda.md | 35 ++- .../Ledger/Properties/Computational.lagda.md | 246 +++++------------- 3 files changed, 106 insertions(+), 176 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index bce112fb2..5438072af 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,7 @@ ### WIP +- Apply batch-wide direct deposits to `CertState` in `LEDGER-V` output (CIP-159). - Forbid CIP-159 fields (`txDirectDeposits`, `txBalanceIntervals`) in legacy mode via explicit `UTXOW-legacy` premises. - Allow partial withdrawals in `PRE-CERT` rule; define `applyWithdrawals` and `_≤ᵐ_` (CIP-159). - Extend `TxInfo` with `txDirectDeposits` and `txBalanceIntervals` fields (CIP-159). diff --git a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md index bff049b17..2831bfea6 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md @@ -299,8 +299,37 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx _⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LedgerState → List SubLevelTx → LedgerState → Type _⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_} +``` + +**Direct Deposit Application (CIP-159)**. After all sub-rule transitions +(`SUBLEDGERS`{.AgdaDatatype}, `CERTS`{.AgdaDatatype}, `GOVS`{.AgdaDatatype}, +`UTXOW`{.AgdaDatatype}), batch-wide direct deposits are applied to the final +`CertState`{.AgdaRecord}. The function `applyDirectDeposits`{.AgdaFunction} (from +the `Certs`{.AgdaModule} module) adds deposit amounts to the `DState` + `rewards` map (stake credential reward account balances) via `∪⁺`, +and `allDirectDeposits`{.AgdaFunction} (from the `Transaction`{.AgdaModule} module) +aggregates direct deposits across the top-level transaction and all sub-transactions. + +Direct deposits are applied *after* withdrawal processing (in `CERTS`{.AgdaDatatype}) +to ensure that withdrawals are checked against pre-batch balances. This prevents +phantom asset attacks where a deposit from one sub-transaction inflates the balance +available for withdrawal by another sub-transaction in the same batch. + +```agda +certStateWithDDeps : TopLevelTx → CertState → CertState +certStateWithDDeps tx cs = record cs { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf cs) } +``` + +`depositsChange`{.AgdaFunction} is computed from `certStateᵢ` (`i ∈ {0,1,2}`) +(not `certStateFinal`) since it represents net deposit change across the batch +(not direct deposit value transfers) and reflects registration/deregistration. +`rmOrphanDRepVotes` uses `certStateFinal` (not `certState₂`) so it sees +the post-deposit `DRep` state. (In practice, `applyDirectDeposits`{.AgdaFunction} +only modifies rewards, so `rmOrphanDRepVotes` would produce the same result either +way, but using `certStateFinal` is semantically correct.) +```agda data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → LedgerState → Type where LEDGER-V : @@ -312,6 +341,9 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg depositsChange : DepositsChange depositsChange = calculateDepositsChange certState₀ certState₁ certState₂ + + certStateFinal : CertState + certStateFinal = certStateWithDDeps tx certState₂ in ∙ IsValidFlagOf tx ≡ true ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , RewardsOf certState₀ ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧ @@ -319,8 +351,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg ∙ ⟦ TxIdOf tx , epoch slot , pp , ppolicy , enactState , certState₂ , dom (RewardsOf certState₂) ⟧ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂ ∙ ⟦ slot , pp , treasury , utxo₀ , depositsChange , allScripts , RewardsOf certState₀ ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂ ──────────────────────────────── - ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₂ , rmOrphanDRepVotes certState₂ govState₂ , certState₂ ⟧ - + ⟦ slot , ppolicy , pp , enactState , treasury ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ tx ,LEDGER⦈ ⟦ utxoState₂ , rmOrphanDRepVotes certStateFinal govState₂ , certStateFinal ⟧ LEDGER-I : let utxo₀ : UTxO diff --git a/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md index c48ca8465..3ba7b8229 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md @@ -91,17 +91,16 @@ instance computeGov = comp {STS = _⊢_⇀⦇_,GOVS⦈_} -- Helper env constructors (avoid `let ... in with ...` parse issues) - subUtxoΓ : SubLedgerEnv → SubUTxOEnv - subUtxoΓ Γ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ - where open SubLedgerEnv Γ + module _ (Γ : SubLedgerEnv) where + open SubLedgerEnv Γ + subUtxoΓ : SubUTxOEnv + subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ - certΓ : SubLedgerEnv → LedgerState → SubLevelTx → CertEnv - certΓ Γ s stx = ⟦ epoch slot , pparams , ListOfGovVotesOf stx , WithdrawalsOf stx , allColdCreds (LedgerState.govSt s) enactState ⟧ - where open SubLedgerEnv Γ + certΓ : LedgerState → SubLevelTx → CertEnv + certΓ s stx = ⟦ epoch slot , pparams , ListOfGovVotesOf stx , WithdrawalsOf stx , allColdCreds (GovStateOf s) enactState ⟧ - govΓ : SubLedgerEnv → SubLevelTx → CertState → GovEnv - govΓ Γ stx certSt = ⟦ TxIdOf stx , epoch slot , pparams , ppolicy , enactState , certSt , dom (RewardsOf certSt) ⟧ - where open SubLedgerEnv Γ + govΓ : SubLevelTx → CertState → GovEnv + govΓ stx certSt = ⟦ TxIdOf stx , epoch slot , pparams , ppolicy , enactState , certSt , dom (RewardsOf certSt) ⟧ ``` --> @@ -114,38 +113,18 @@ instance ```agda computeProof Γ s stx with SubLedgerEnv.isTopLevelValid Γ ≟ true ... | yes isV = - let open SubLedgerEnv Γ - open LedgerState s - subUtxoΓ : SubUTxOEnv - subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ - certΓ : CertEnv - certΓ = ⟦ epoch slot , pparams , ListOfGovVotesOf stx , WithdrawalsOf stx - , allColdCreds govSt enactState ⟧ - in - computeSubutxow subUtxoΓ utxoSt stx >>= λ where + computeSubutxow (subUtxoΓ Γ) (UTxOStateOf s) stx >>= λ where (utxoSt' , utxoStep) → - computeCerts certΓ certState (DCertsOf stx) >>= λ where + computeCerts (certΓ Γ s stx) (CertStateOf s) (DCertsOf stx) >>= λ where (certSt' , certStep) → - let govΓ : GovEnv - govΓ = ⟦ TxIdOf stx , epoch slot , pparams , ppolicy , enactState - , certSt' , dom (RewardsOf certSt') ⟧ - in - computeGov govΓ govSt (GovProposals+Votes stx) >>= λ where + computeGov (govΓ Γ stx certSt') (GovStateOf s) (GovProposals+Votes stx) >>= λ where (govSt' , govStep) → - success ( ⟦ utxoSt' , govSt' , certSt' ⟧ˡ - , SUBLEDGER-V (isV , utxoStep , certStep , govStep)) - - ... | no ¬isV = - let open SubLedgerEnv Γ; open LedgerState s - isI : isTopLevelValid ≡ false - isI = ¬-not ¬isV - subUtxoΓ : SubUTxOEnv - subUtxoΓ = ⟦ slot , pparams , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ - in case computeSubutxow subUtxoΓ utxoSt stx of λ where - (failure e) → failure e - (success (utxoSt' , utxoStep)) → - success ( ⟦ utxoSt , govSt , certState ⟧ˡ - , SUBLEDGER-I ( isI , subst (subUtxoΓ ⊢ utxoSt ⇀⦇ stx ,SUBUTXOW⦈_) (SUBUTXOW-noop isI utxoStep) utxoStep )) + success ( ⟦ utxoSt' , govSt' , certSt' ⟧ˡ , SUBLEDGER-V (isV , utxoStep , certStep , govStep)) + + ... | no ¬isV = case computeSubutxow (subUtxoΓ Γ) (UTxOStateOf s) stx of λ where + (failure e) → failure e + (success (utxoSt' , utxoStep)) → + success ( s , SUBLEDGER-I ( ¬-not ¬isV , subst (subUtxoΓ Γ ⊢ (UTxOStateOf s) ⇀⦇ stx ,SUBUTXOW⦈_) (SUBUTXOW-noop (¬-not ¬isV) utxoStep) utxoStep )) ``` --> @@ -163,26 +142,22 @@ instance with SubLedgerEnv.isTopLevelValid Γ ≟ true ... | no ¬isV = contradiction isV ¬isV ... | yes refl - with computeSubutxow (subUtxoΓ Γ) (LedgerState.utxoSt s) stx - | complete {STS = _⊢_⇀⦇_,SUBUTXOW⦈_} - (subUtxoΓ Γ) (LedgerState.utxoSt s) stx utxoSt₁ utxoStep + with computeSubutxow (subUtxoΓ Γ) (UTxOStateOf s) stx + | complete {STS = _⊢_⇀⦇_,SUBUTXOW⦈_} (subUtxoΓ Γ) (UTxOStateOf s) stx utxoSt₁ utxoStep ... | success (utxoSt₁ , _) | refl - with computeCerts (certΓ Γ s stx) (LedgerState.certState s) (DCertsOf stx) - | complete {STS = _⊢_⇀⦇_,CERTS⦈_} - (certΓ Γ s stx) (LedgerState.certState s) (DCertsOf stx) certSt₁ certStep + with computeCerts (certΓ Γ s stx) (CertStateOf s) (DCertsOf stx) + | complete {STS = _⊢_⇀⦇_,CERTS⦈_} (certΓ Γ s stx) (CertStateOf s) (DCertsOf stx) certSt₁ certStep ... | success (certSt₁ , _) | refl - with computeGov (govΓ Γ stx certSt₁) (LedgerState.govSt s) (GovProposals+Votes stx) - | complete {STS = _⊢_⇀⦇_,GOVS⦈_} - (govΓ Γ stx certSt₁) (LedgerState.govSt s) (GovProposals+Votes stx) govSt₁ govStep + with computeGov (govΓ Γ stx certSt₁) (GovStateOf s) (GovProposals+Votes stx) + | complete {STS = _⊢_⇀⦇_,GOVS⦈_} (govΓ Γ stx certSt₁) (GovStateOf s) (GovProposals+Votes stx) govSt₁ govStep ... | success (govSt₁ , _) | refl = refl completeness Γ s stx s' (SUBLEDGER-I (isI , utxoStep)) with SubLedgerEnv.isTopLevelValid Γ ≟ true ... | yes isV = case trans (sym isV) isI of λ () ... | no ¬isV - with computeSubutxow (subUtxoΓ Γ) (LedgerState.utxoSt s) stx - | complete {STS = _⊢_⇀⦇_,SUBUTXOW⦈_} - (subUtxoΓ Γ) (LedgerState.utxoSt s) stx (LedgerState.utxoSt s) utxoStep + with computeSubutxow (subUtxoΓ Γ) (UTxOStateOf s) stx + | complete {STS = _⊢_⇀⦇_,SUBUTXOW⦈_} (subUtxoΓ Γ) (UTxOStateOf s) stx (UTxOStateOf s) utxoStep ... | success _ | refl = refl Computational-SUBLEDGERS : Computational _⊢_⇀⦇_,SUBLEDGERS⦈_ String @@ -209,67 +184,30 @@ instance computeUtxow = comp {STS = _⊢_⇀⦇_,UTXOW⦈_} -- Helper builders (avoid `let ... in with ...`) - utxo₀Of : LedgerState → UTxO - utxo₀Of s = UTxOOf (LedgerState.utxoSt s) - allScriptsOf : TopLevelTx → LedgerState → ℙ Script - allScriptsOf tx s = getAllScripts tx (utxo₀Of s) - - subΓOf : LedgerEnv → LedgerState → TopLevelTx → SubLedgerEnv - subΓOf Γ s tx = - ⟦ LedgerEnv.slot Γ - , LedgerEnv.ppolicy Γ - , LedgerEnv.pparams Γ - , LedgerEnv.enactState Γ - , LedgerEnv.treasury Γ - , utxo₀Of s - , IsValidFlagOf tx - , allScriptsOf tx s - , RewardsOf (CertStateOf s) - ⟧ - - certΓOf : LedgerEnv → TopLevelTx → GovState → CertEnv - certΓOf Γ tx govSt = - ⟦ epoch (LedgerEnv.slot Γ) - , LedgerEnv.pparams Γ - , ListOfGovVotesOf tx - , WithdrawalsOf tx - , allColdCreds govSt (LedgerEnv.enactState Γ) - ⟧ - - govΓOf : LedgerEnv → TopLevelTx → CertState → GovEnv - govΓOf Γ tx certSt = - ⟦ TxIdOf tx - , epoch (LedgerEnv.slot Γ) - , LedgerEnv.pparams Γ - , LedgerEnv.ppolicy Γ - , LedgerEnv.enactState Γ - , certSt - , dom (RewardsOf certSt) - ⟧ - - utxoΓ-valid : LedgerEnv → LedgerState → TopLevelTx → CertState → CertState → UTxOEnv - utxoΓ-valid Γ s tx certSt₁ certSt₂ = - let depositsChange = calculateDepositsChange (LedgerState.certState s) certSt₁ certSt₂ - in ⟦ LedgerEnv.slot Γ - , LedgerEnv.pparams Γ - , LedgerEnv.treasury Γ - , utxo₀Of s - , depositsChange - , allScriptsOf tx s - , RewardsOf (CertStateOf s) - ⟧ - - utxoΓ-invalid : LedgerEnv → LedgerState → TopLevelTx → UTxOEnv - utxoΓ-invalid Γ s tx = - ⟦ LedgerEnv.slot Γ - , LedgerEnv.pparams Γ - , LedgerEnv.treasury Γ - , utxo₀Of s - , ⟦ 0ℤ , 0ℤ ⟧ - , allScriptsOf tx s - , RewardsOf (CertStateOf s) - ⟧ + allScriptsOf tx s = getAllScripts tx (UTxOOf s) + + module _ (Γ : LedgerEnv) where + open LedgerEnv Γ + subΓOf : LedgerState → TopLevelTx → SubLedgerEnv + subΓOf s tx = + ⟦ slot , ppolicy , pparams , enactState , treasury , UTxOOf s , IsValidFlagOf tx , allScriptsOf tx s , RewardsOf (CertStateOf s) ⟧ + + certΓOf : TopLevelTx → GovState → CertEnv + certΓOf tx govSt = ⟦ epoch slot , pparams , ListOfGovVotesOf tx , WithdrawalsOf tx , allColdCreds govSt enactState ⟧ + + govΓOf : TopLevelTx → CertState → GovEnv + govΓOf tx certSt = ⟦ TxIdOf tx , epoch slot , pparams , ppolicy , enactState , certSt , dom (RewardsOf certSt) ⟧ + + utxoΓ-valid : LedgerState → TopLevelTx → CertState → CertState → UTxOEnv + utxoΓ-valid s tx certSt₁ certSt₂ = + ⟦ slot , pparams , treasury , UTxOOf s , calculateDepositsChange (CertStateOf s) certSt₁ certSt₂ + , allScriptsOf tx s , RewardsOf (CertStateOf s) ⟧ + + utxoΓ-invalid : LedgerState → TopLevelTx → UTxOEnv + utxoΓ-invalid s tx = + ⟦ slot , pparams , treasury , UTxOOf s , ⟦ 0ℤ , 0ℤ ⟧ , allScriptsOf tx s , RewardsOf (CertStateOf s) ⟧ + ``` --> @@ -280,68 +218,28 @@ instance @@ -384,9 +282,9 @@ instance | complete {STS = _⊢_⇀⦇_,SUBLEDGERS⦈_} (subΓOf Γ s txTop) s (SubTransactionsOf txTop) s subStep ... | success _ | refl - with computeUtxow (utxoΓ-invalid Γ s txTop) (LedgerState.utxoSt s) txTop + with computeUtxow (utxoΓ-invalid Γ s txTop) (UTxOStateOf s) txTop | complete {STS = _⊢_⇀⦇_,UTXOW⦈_} - (utxoΓ-invalid Γ s txTop) (LedgerState.utxoSt s) txTop utxoSt₁ utxoStep + (utxoΓ-invalid Γ s txTop) (UTxOStateOf s) txTop utxoSt₁ utxoStep ... | success _ | refl = refl Computational-LEDGERS : Computational _⊢_⇀⦇_,LEDGERS⦈_ String From aee38f2477f069be8fc9eebcec29a777721509b9 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 30 Apr 2026 14:58:25 -0600 Subject: [PATCH 02/14] add justification for batch processing of direct deposits --- .../Dijkstra/Specification/Ledger.lagda.md | 77 +++++++++++++++++++ 1 file changed, 77 insertions(+) diff --git a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md index 2831bfea6..893d2168b 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md @@ -329,6 +329,83 @@ the post-deposit `DRep` state. (In practice, `applyDirectDeposits`{.AgdaFunctio only modifies rewards, so `rmOrphanDRepVotes` would produce the same result either way, but using `certStateFinal` is semantically correct.) +### Design Rationale: Batch-wide Direct Deposit Application + +A natural alternative to applying direct deposits batch-wide (as above) is to +interleave them with the per-sub-transaction processing performed by +`SUBLEDGERS`{.AgdaDatatype}; that is, in each `SUBLEDGER-V`{.AgdaInductiveConstructor} +step, apply that sub-transaction's `DirectDepositsOf stx` to the threaded +`CertState`{.AgdaRecord} after running `CERTS`{.AgdaDatatype}/`GOVS`{.AgdaDatatype} +for the sub-transaction. + +**The CIP forbids this alternative, and the rule structure +adopted here makes the prohibition manifest rather than imposing it as an extra +premise.** + ++ **CIP-159 rules out per-sub-transaction application**. + + CIP-159 states that, "to prevent ... *phantom asset* attacks, transactions can + only withdraw funds that exist in the account *before* the overall transaction + is run. This means later sub-txs cannot withdraw assets that were deposited + by prior sub-txs in the same overall transaction." Per-sub-transaction + application would let sub-transaction `N`'s `PRE-CERT`{.AgdaDatatype} step + authorize withdrawals against a `rewards`{.AgdaField} map already inflated by + sub-transactions `1..N−1`'s deposits — exactly the situation the CIP forbids. + ++ **Phantom asset prevention follows structurally**. + + Because `applyDirectDeposits`{.AgdaFunction} never runs against the + `CertState`{.AgdaRecord} threaded through `SUBLEDGERS`{.AgdaDatatype}, every + `PRE-CERT`{.AgdaDatatype} step in the batch checks each withdrawal `amt` against + `rewards`{.AgdaField} as updated only by `applyWithdrawals`{.AgdaFunction} and + by registration/deregistration certificates. Summed across the batch this + yields, for every reward address, total withdrawals bounded by the pre-batch + balance (i.e., the `NoPhantomWithdrawals`{.AgdaFunction} property) *as a + consequence of the rule structure* rather than as a separate premise that would + need to be added and discharged. + ++ **Alignment with CIP-118 script context isolation**. + + CIP-118 requires that "Plutus scripts in one sub-transaction do not see other + sub-transactions or the top-level transaction in their context." Holding the + `accountBalances`{.AgdaField} field of `SubLedgerEnv`{.AgdaRecord} and + `SubUTxOEnv`{.AgdaRecord} fixed at the pre-batch snapshot `RewardsOf certState₀` + ensures that every sub-transaction's balance-interval check (and any future Plutus + context derived from this field) sees the same balances independently of the + surrounding sub-transactions. Per-sub-transaction application would make these + views order-dependent across sub-transactions. + ++ **Direct deposits are a diff, not a sequence of state updates**. + + CIP-159 specifies that the `direct_deposits` field carries only the diff to be + applied (e.g., `0.1 ADA`, not the resulting `100.1 ADA` balance). Aggregating + each sub-transaction's diff via `∪⁺` (union-with-addition) and applying the + sum once is the natural reading: the batch-level + `allDirectDeposits`{.AgdaFunction} is the diff from pre-batch to post-batch. + Per-sub-transaction application would impose an artificial sequential + interpretation on what is logically a commutative aggregation. + ++ **Determinism and reorderability**. + + CIP-159 motivates direct deposits in part by their freedom from contention: + deposits into the same account from different parties can be processed "in any + order and fully parallel." Batch-wide application makes this manifest at the + rule level: the order of sub-transactions in the batch does not affect the + `accountBalances`{.AgdaField} visible to any sub-transaction's + `SUBUTXO`{.AgdaDatatype} or `CERTS`{.AgdaDatatype} step, nor the final + `rewards`{.AgdaField} reached after the deposit step. + ++ **`depositsChange`{.AgdaFunction} remains orthogonal**. + + `calculateDepositsChange`{.AgdaFunction} measures *protocol* deposit movements + (registration/deregistration of credentials, DReps, pools), which live in the + `deposits`{.AgdaField} fields of `DState`{.AgdaRecord}/`PState`{.AgdaRecord}/ + `GState`{.AgdaRecord} — not in `rewards`{.AgdaField}. Because + `applyDirectDeposits`{.AgdaFunction} touches only `rewards`{.AgdaField} and + runs *after* `calculateDepositsChange`{.AgdaFunction}, the two notions of + "deposit" remain cleanly disjoint without case analysis. + + ```agda data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → LedgerState → Type where From d1691c9ee37a4f6d7c97723e25d0888de5adf68a Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 30 Apr 2026 21:11:04 -0600 Subject: [PATCH 03/14] LEDGER-V: forbid direct deposits to credentials deregistered in same batch MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `applyDirectDeposits` uses `∪⁺` (union-with-addition) on the `rewards` map, so a credential not present in `RewardsOf certState₂` is added as a new entry rather than rejected. The pre-existing SUBUTXO/UTXO premise `dom (DirectDepositsOf tx) ⊆ dom (AccountBalancesOf Γ)` only checks against the pre-batch balances `RewardsOf certState₀`, so it does not catch the case where a credential is registered pre-batch, deregistered during `CERTS`, and direct-deposited to in the same batch. Without the new premise, the resulting `certStateFinal` is internally inconsistent: the credential has a positive `rewards` entry but no corresponding `voteDelegs`, `stakeDelegs`, or `deposits` entry — effectively re- registering the credential without a key deposit. Add the phase-1 premise dom (allDirectDeposits tx) ⊆ dom (RewardsOf certState₂) to `LEDGER-V` to rule this out. Filtering `allDirectDeposits tx` by `dom (RewardsOf certState₂)` would be an alternative, but it would silently destroy user funds when a deposit and a deregistration race in the same batch. The premise is symmetric to (and complements) the existing pre-batch SUBUTXO/UTXO check. Update `Ledger/Properties/Computational.lagda.md` for the new premise, and pass `UTxOStateOf s₁` explicitly to `computeUtxow` in the LEDGER valid branch (the previous `_` resolved by chained unification through the LEDGER-V constructor, which was fragile and obscured intent). TODO: fix `Ledger/Properties/Computational.lagda.md`; it's choking on the new premise. --- .../Dijkstra/Specification/Ledger.lagda.md | 10 ++++++++++ .../Ledger/Properties/Computational.lagda.md | 18 ++++++++++++------ 2 files changed, 22 insertions(+), 6 deletions(-) diff --git a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md index 893d2168b..4c73a9f65 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md @@ -329,6 +329,15 @@ the post-deposit `DRep` state. (In practice, `applyDirectDeposits`{.AgdaFunctio only modifies rewards, so `rmOrphanDRepVotes` would produce the same result either way, but using `certStateFinal` is semantically correct.) +**Deposits target post-batch registered accounts**. `SUBUTXO`{.AgdaDatatype} +and `UTXO`{.AgdaDatatype} check that direct-deposit targets are registered in the +*pre-batch* balances, but they cannot account for deregistrations that occur during +the batch. Therefore, we add a new premise, `dom (allDirectDeposits tx) ⊆ dom (RewardsOf +certState₂)`, to check that `applyDirectDeposits` does not silently re-introduce a +deregistered credential into the `rewards` map without re-registering it via +`voteDelegs`, `stakeDelegs`, or `deposits`, as that would result in an inconsistent +`DState`. The premise rules this out at phase 1. + ### Design Rationale: Batch-wide Direct Deposit Application A natural alternative to applying direct deposits batch-wide (as above) is to @@ -425,6 +434,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg ∙ IsValidFlagOf tx ≡ true ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , RewardsOf certState₀ ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧ ∙ ⟦ epoch slot , pp , ListOfGovVotesOf tx , WithdrawalsOf tx , allColdCreds govState₁ enactState ⟧ ⊢ certState₁ ⇀⦇ DCertsOf tx ,CERTS⦈ certState₂ + ∙ dom (allDirectDeposits tx) ⊆ dom (RewardsOf certState₂) ∙ ⟦ TxIdOf tx , epoch slot , pp , ppolicy , enactState , certState₂ , dom (RewardsOf certState₂) ⟧ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂ ∙ ⟦ slot , pp , treasury , utxo₀ , depositsChange , allScripts , RewardsOf certState₀ ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂ ──────────────────────────────── diff --git a/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md index 3ba7b8229..6f211152f 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md @@ -224,10 +224,12 @@ instance (certSt₂ , certStep) → computeGov (govΓOf Γ txTop certSt₂) (GovStateOf s₁) (GovProposals+Votes txTop) >>= λ where (govSt₂ , govStep) → -- UTXOW must run from the post-SUBLEDGERS UTxOState ((UTxOState s₁)) - computeUtxow (utxoΓ-valid Γ s txTop (CertStateOf s₁) certSt₂) _ txTop >>= λ where - (utxoSt₂ , utxoStep) → - success ( ⟦ utxoSt₂ , rmOrphanDRepVotes (certStateWithDDeps txTop certSt₂) govSt₂ , certStateWithDDeps txTop certSt₂ ⟧ˡ - , LEDGER-V (isV , subStep , certStep , govStep , utxoStep)) + computeUtxow (utxoΓ-valid Γ s txTop (CertStateOf s₁) certSt₂) (UTxOStateOf s₁) txTop >>= λ where + (utxoSt₂ , utxoStep) → case ¿ dom (allDirectDeposits txTop) ⊆ dom (RewardsOf certSt₂) ¿ of λ where + (yes h) → + success ( ⟦ utxoSt₂ , rmOrphanDRepVotes (certStateWithDDeps txTop certSt₂) govSt₂ , certStateWithDDeps txTop certSt₂ ⟧ˡ + , LEDGER-V (isV , subStep , certStep , h , govStep , utxoStep) ) + (no _) → failure "direct deposit target was deregistered during this batch" (no ¬isV) → case computeSubledgers (subΓOf Γ s txTop) s (SubTransactionsOf txTop) of λ where (failure e) → failure e @@ -252,7 +254,7 @@ instance ```agda completeness Γ s txTop s' (LEDGER-V {certState₁ = certSt₁} {certSt₂} {utxoState₁ = utxoSt₁} {govSt₁} {govSt₂} {utxoSt₂} - (isV , subStep , certStep , govStep , utxoStep)) + (isV , subStep , certStep , h , govStep , utxoStep)) with IsValidFlagOf txTop ≟ true ... | no ¬isV = contradiction isV ¬isV ... | yes refl @@ -272,7 +274,11 @@ instance with computeUtxow (utxoΓ-valid Γ s txTop certSt₁ certSt₂) utxoSt₁ txTop | complete {STS = _⊢_⇀⦇_,UTXOW⦈_} (utxoΓ-valid Γ s txTop certSt₁ certSt₂) utxoSt₁ txTop utxoSt₂ utxoStep - ... | success (utxoSt₂ , _) | refl = refl + ... | success (utxoSt₂ , _) | refl + with ¿ dom (allDirectDeposits txTop) ⊆ dom (RewardsOf certSt₂) ¿ + ... | yes _ = refl + ... | no ¬h = ⊥-elim (¬h h) + completeness Γ s txTop s' (LEDGER-I {utxoState₁ = utxoSt₁} (isI , subStep , utxoStep)) with IsValidFlagOf txTop ≟ true From 93423f08c2ebc98a3bddb1ebc4f8ab82b6e71127 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Mon, 4 May 2026 23:19:08 -0600 Subject: [PATCH 04/14] Apply CIP-159 direct deposits per-transaction, not batch-wide MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Each transaction's `txDirectDeposits` are now applied to the threaded `CertState` immediately after that transaction's `CERTS` step, replacing the batch-wide application introduced earlier on this branch. * `SUBLEDGER-V` applies `DirectDepositsOf stx` to `certState₁` after `CERTS` and emits the result. * `LEDGER-V` still applies the top-level transaction's deposits to `certState₂` after the top-level `CERTS`, but the premise now bounds `dom (DirectDepositsOf tx)` rather than the batch aggregate `dom (allDirectDeposits tx)`. * `certStateWithDDeps` is generalised to `∀ {ℓ} → Tx ℓ → CertState → CertState` so both rules can invoke it with the local `DirectDepositsOf`. The original draft of this branch argued that batch-wide application made CIP-159's phantom-asset prohibition manifest in the rule structure. Per-transaction application is equally safe: the prohibition is enforced separately by `NoPhantomWithdrawals` in the `Utxo` module, which bounds batch-wide withdrawal totals against the `accountBalances` field of `UTxOEnv`/`SubUTxOEnv` — fixed at the pre-batch snapshot `RewardsOf certState₀` regardless of when (or how) deposits are applied to the threaded `CertState`. Per-transaction application also mirrors the Haskell ledger executor's sequential per-transaction processing, which simplifies the conformance proof and avoids a structural gap between the spec and the implementation. A direct-deposit registration premise is added to each rule to prevent `applyDirectDeposits` from silently re-introducing a credential into `rewards` after deregistration earlier in the same transaction: * `SUBLEDGER-V` requires `dom (DirectDepositsOf stx) ⊆ dom (RewardsOf certState₁)`. * `LEDGER-V` requires `dom (DirectDepositsOf tx) ⊆ dom (RewardsOf certState₂)`. The check is local to each transaction's post-`CERTS` state, so a sub-transaction whose deposit targets a credential deregistered by an earlier sub-transaction in the same batch will fail the premise. `Computational-SUBLEDGER` and `Computational-LEDGER` are updated to dispatch on these decidable premises in `computeProof` and `completeness`. `depositsChange` is unaffected: it reads only the protocol-deposit fields of `DState`/`PState`/`GState`, which `applyDirectDeposits` does not touch. Refs: #1122 --- CHANGELOG.md | 2 +- .../Dijkstra/Specification/Ledger.lagda.md | 234 ++++++++-------- .../Ledger/Properties/Computational.lagda.md | 263 +++++++++--------- 3 files changed, 241 insertions(+), 258 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 5438072af..b2c6c9ef8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,7 +4,7 @@ ### WIP -- Apply batch-wide direct deposits to `CertState` in `LEDGER-V` output (CIP-159). +- Apply per-transaction direct deposits to `CertState` after each `CERTS` step in `SUBLEDGER-V` and `LEDGER-V` (CIP-159). - Forbid CIP-159 fields (`txDirectDeposits`, `txBalanceIntervals`) in legacy mode via explicit `UTXOW-legacy` premises. - Allow partial withdrawals in `PRE-CERT` rule; define `applyWithdrawals` and `_≤ᵐ_` (CIP-159). - Extend `TxInfo` with `txDirectDeposits` and `txBalanceIntervals` fields (CIP-159). diff --git a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md index 4c73a9f65..90a6783eb 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md @@ -280,6 +280,119 @@ UTxOEnv{.AgdaDatatype}/SubUTxOEnv{.AgdaDatatype}. for both enacted CC credentials and any newly proposed CC actions that appear in the final (post-subtransaction processing) `GovState`{.AgdaRecord}. +### Direct Deposit Application (CIP-159) + +Each transaction's direct deposits (`txDirectDeposits`{.AgdaField}) are applied to +the `CertState`{.AgdaRecord} immediately after that transaction's +`CERTS`{.AgdaDatatype} step, before the rule emits its output state. + ++ In `SUBLEDGER-V`{.AgdaInductiveConstructor}, after `CERTS`{.AgdaDatatype} produces + `certState₁`, the deposits in `DirectDepositsOf stx` are credited to the + `rewards`{.AgdaField} map of `certState₁`'s `dState`{.AgdaField}, yielding the + `certStateFinal` that appears in the final `LedgerState`{.AgdaRecord} of the + `SUBLEDGER`{.AgdaDatatype} relation. ++ In `LEDGER-V`{.AgdaInductiveConstructor}, after the top-level + `CERTS`{.AgdaDatatype} produces `certState₂`, the deposits in + `DirectDepositsOf tx` are credited the same way, yielding the `certStateFinal` + that appears in the final `LedgerState`{.AgdaRecord} of the + `LEDGER`{.AgdaDatatype} relation. + +The helper `certStateWithDDeps`{.AgdaFunction} performs the per-transaction update. +It uses `applyDirectDeposits`{.AgdaFunction} (from the `Certs`{.AgdaModule} module), +which adds deposit amounts to the `DState`{.AgdaRecord} `rewards`{.AgdaField} map +via `∪⁺`{.AgdaFunction} (union with addition). + +```agda +certStateWithDDeps : ∀ {ℓ} → Tx ℓ → CertState → CertState +certStateWithDDeps tx cs = record cs { dState = applyDirectDeposits (DirectDepositsOf tx) (DStateOf cs) } +``` + +`certStateWithDDeps`{.AgdaFunction} is invoked once per transaction in the batch +(once per sub-transaction inside `SUBLEDGER-V`{.AgdaInductiveConstructor}, plus +once for the top-level transaction inside `LEDGER-V`{.AgdaInductiveConstructor}) +on the *post-`CERTS`{.AgdaDatatype}* `CertState`{.AgdaRecord} for that +transaction. (Since `applyDirectDeposits`{.AgdaFunction} only modifies +`rewards`{.AgdaField}, and leaves `voteDelegs`{.AgdaField}, +`stakeDelegs`{.AgdaField}, `deposits`{.AgdaField}, `pState`{.AgdaField}, and +`gState`{.AgdaField} unchanged, applying it per-transaction is +equivalent to aggregating all direct deposits in the batch via `∪⁺`{.AgdaFunction} +and applying the sum at the end.) + +`depositsChange`{.AgdaFunction} is computed from `certState₀`{.AgdaBound}, +`certState₁`{.AgdaBound}, and `certState₂`{.AgdaBound} (not from +`certStateFinal`{.AgdaBound}) because it measures *protocol* deposit movements +(registration/deregistration of credentials, DReps, pools), which live in the +`deposits`{.AgdaField} fields of `DState`{.AgdaRecord}/`PState`{.AgdaRecord}/ +`GState`{.AgdaRecord} — not in `rewards`{.AgdaField}. Since +`applyDirectDeposits`{.AgdaFunction} only updates `rewards`{.AgdaField}, the two +notions of "deposit" remain cleanly disjoint. + +`rmOrphanDRepVotes`{.AgdaFunction} in `LEDGER-V`{.AgdaInductiveConstructor} +receives `certStateFinal`{.AgdaBound} (rather than `certState₂`{.AgdaBound}) so +that it sees the post-deposit `DRep`{.AgdaInductiveConstructor} state. In +practice the result is the same either way, since `applyDirectDeposits`{.AgdaFunction} +does not modify `dreps`{.AgdaField}. + +#### Direct deposit registration premise + +Each rule additionally requires that the credentials targeted by that +transaction's direct deposits are registered in the *post-`CERTS`{.AgdaDatatype}* +`CertState`{.AgdaRecord}. + ++ `SUBLEDGER-V`{.AgdaInductiveConstructor} requires + `dom (DirectDepositsOf stx) ⊆ dom (RewardsOf certState₁)`. ++ `LEDGER-V`{.AgdaInductiveConstructor} requires + `dom (DirectDepositsOf tx) ⊆ dom (RewardsOf certState₂)`. + +Without this premise, `applyDirectDeposits`{.AgdaFunction} could silently +re-introduce a credential into `rewards`{.AgdaField} that had been deregistered +earlier in the same transaction's `CERTS`{.AgdaDatatype} step (and thus is no +longer present in `voteDelegs`{.AgdaField}, `stakeDelegs`{.AgdaField}, or +`deposits`{.AgdaField}), producing an inconsistent `DState`{.AgdaRecord}. The +domain check rules this out at phase 1. Note that the check is performed +against the post-`CERTS`{.AgdaDatatype} state of the *same* transaction, so +deregistrations performed by *prior* sub-transactions in the batch are +correctly accounted for; a sub-transaction whose deposit targets a credential +deregistered by an earlier sub-transaction will fail this premise. + +### Design Rationale: Per-transaction Direct Deposit Application + +Here we justify the choice to apply direct deposits per-transaction, instead of +aggregating and applying them batch-wide at the end of +`LEDGER-V`{.AgdaInductiveConstructor}. + ++ **Phantom asset prevention is enforced by `NoPhantomWithdrawals`{.AgdaFunction}**. + + CIP-159 forbids "phantom asset" attacks in which a sub-transaction's direct + deposit inflates the balance available to a later sub-transaction's withdrawal + within the same batch. This restriction is enforced in the `Utxo`{.AgdaModule} + module by the `NoPhantomWithdrawals`{.AgdaFunction} predicate, which bounds + *batch-wide* withdrawal totals (per reward address) by the + `accountBalances`{.AgdaField} field of `UTxOEnv`{.AgdaRecord} and + `SubUTxOEnv`{.AgdaRecord} — the *pre-batch* snapshot `RewardsOf + certState₀`{.AgdaBound}. Because `accountBalances`{.AgdaField} is fixed at the + pre-batch value and never updated by direct deposit application, the CIP-159 + phantom-asset prohibition holds regardless of whether deposits are applied + per-transaction or batch-wide. + ++ **CIP-118 script context isolation is preserved by `accountBalances`{.AgdaField}**. + + CIP-118 requires that Plutus scripts in one sub-transaction do not see other + sub-transactions or the top-level transaction in their context. In the current + spec, `accountBalances`{.AgdaField} (used for balance-interval checks and any + future Plutus context derived from this field) is held fixed at + `RewardsOf certState₀`{.AgdaBound} across the entire batch, so every + sub-transaction sees the same pre-batch balances regardless of when deposits of + other sub-transactions are applied. + ++ **`depositsChange`{.AgdaFunction} remains orthogonal**. + + `calculateDepositsChange`{.AgdaFunction} reads only the `deposits`{.AgdaField} + fields of `DState`{.AgdaRecord}/`PState`{.AgdaRecord}/`GState`{.AgdaRecord}, which + `applyDirectDeposits`{.AgdaFunction} does not touch. Whether direct deposits are + applied per-transaction or batch-wide, `depositsChange`{.AgdaFunction} is + unaffected. + ```agda data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx → LedgerState → Type where @@ -287,10 +400,10 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx ∙ isTopLevelValid ≡ true ∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁ ∙ ⟦ epoch slot , pp , ListOfGovVotesOf stx , WithdrawalsOf stx , allColdCreds govState₀ enactState ⟧ ⊢ certState₀ ⇀⦇ DCertsOf stx ,CERTS⦈ certState₁ + ∙ dom (DirectDepositsOf stx) ⊆ dom (RewardsOf certState₁) ∙ ⟦ TxIdOf stx , epoch slot , pp , ppolicy , enactState , certState₁ , dom (RewardsOf certState₁) ⟧ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁ ──────────────────────────────── - ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧ - + ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ stx ,SUBLEDGER⦈ ⟦ utxoState₁ , govState₁ , certStateWithDDeps stx certState₁ ⟧ SUBLEDGER-I : ∙ isTopLevelValid ≡ false ∙ ⟦ slot , pp , treasury , utxo₀ , isTopLevelValid , allScripts , accountBalances ⟧ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀ @@ -299,123 +412,8 @@ data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LedgerState → SubLevelTx _⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LedgerState → List SubLevelTx → LedgerState → Type _⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_} -``` -**Direct Deposit Application (CIP-159)**. After all sub-rule transitions -(`SUBLEDGERS`{.AgdaDatatype}, `CERTS`{.AgdaDatatype}, `GOVS`{.AgdaDatatype}, -`UTXOW`{.AgdaDatatype}), batch-wide direct deposits are applied to the final -`CertState`{.AgdaRecord}. The function `applyDirectDeposits`{.AgdaFunction} (from -the `Certs`{.AgdaModule} module) adds deposit amounts to the `DState` - `rewards` map (stake credential reward account balances) via `∪⁺`, -and `allDirectDeposits`{.AgdaFunction} (from the `Transaction`{.AgdaModule} module) -aggregates direct deposits across the top-level transaction and all sub-transactions. -Direct deposits are applied *after* withdrawal processing (in `CERTS`{.AgdaDatatype}) -to ensure that withdrawals are checked against pre-batch balances. This prevents -phantom asset attacks where a deposit from one sub-transaction inflates the balance -available for withdrawal by another sub-transaction in the same batch. - -```agda -certStateWithDDeps : TopLevelTx → CertState → CertState -certStateWithDDeps tx cs = record cs { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf cs) } -``` - -`depositsChange`{.AgdaFunction} is computed from `certStateᵢ` (`i ∈ {0,1,2}`) -(not `certStateFinal`) since it represents net deposit change across the batch -(not direct deposit value transfers) and reflects registration/deregistration. - -`rmOrphanDRepVotes` uses `certStateFinal` (not `certState₂`) so it sees -the post-deposit `DRep` state. (In practice, `applyDirectDeposits`{.AgdaFunction} -only modifies rewards, so `rmOrphanDRepVotes` would produce the same result either -way, but using `certStateFinal` is semantically correct.) - -**Deposits target post-batch registered accounts**. `SUBUTXO`{.AgdaDatatype} -and `UTXO`{.AgdaDatatype} check that direct-deposit targets are registered in the -*pre-batch* balances, but they cannot account for deregistrations that occur during -the batch. Therefore, we add a new premise, `dom (allDirectDeposits tx) ⊆ dom (RewardsOf -certState₂)`, to check that `applyDirectDeposits` does not silently re-introduce a -deregistered credential into the `rewards` map without re-registering it via -`voteDelegs`, `stakeDelegs`, or `deposits`, as that would result in an inconsistent -`DState`. The premise rules this out at phase 1. - -### Design Rationale: Batch-wide Direct Deposit Application - -A natural alternative to applying direct deposits batch-wide (as above) is to -interleave them with the per-sub-transaction processing performed by -`SUBLEDGERS`{.AgdaDatatype}; that is, in each `SUBLEDGER-V`{.AgdaInductiveConstructor} -step, apply that sub-transaction's `DirectDepositsOf stx` to the threaded -`CertState`{.AgdaRecord} after running `CERTS`{.AgdaDatatype}/`GOVS`{.AgdaDatatype} -for the sub-transaction. - -**The CIP forbids this alternative, and the rule structure -adopted here makes the prohibition manifest rather than imposing it as an extra -premise.** - -+ **CIP-159 rules out per-sub-transaction application**. - - CIP-159 states that, "to prevent ... *phantom asset* attacks, transactions can - only withdraw funds that exist in the account *before* the overall transaction - is run. This means later sub-txs cannot withdraw assets that were deposited - by prior sub-txs in the same overall transaction." Per-sub-transaction - application would let sub-transaction `N`'s `PRE-CERT`{.AgdaDatatype} step - authorize withdrawals against a `rewards`{.AgdaField} map already inflated by - sub-transactions `1..N−1`'s deposits — exactly the situation the CIP forbids. - -+ **Phantom asset prevention follows structurally**. - - Because `applyDirectDeposits`{.AgdaFunction} never runs against the - `CertState`{.AgdaRecord} threaded through `SUBLEDGERS`{.AgdaDatatype}, every - `PRE-CERT`{.AgdaDatatype} step in the batch checks each withdrawal `amt` against - `rewards`{.AgdaField} as updated only by `applyWithdrawals`{.AgdaFunction} and - by registration/deregistration certificates. Summed across the batch this - yields, for every reward address, total withdrawals bounded by the pre-batch - balance (i.e., the `NoPhantomWithdrawals`{.AgdaFunction} property) *as a - consequence of the rule structure* rather than as a separate premise that would - need to be added and discharged. - -+ **Alignment with CIP-118 script context isolation**. - - CIP-118 requires that "Plutus scripts in one sub-transaction do not see other - sub-transactions or the top-level transaction in their context." Holding the - `accountBalances`{.AgdaField} field of `SubLedgerEnv`{.AgdaRecord} and - `SubUTxOEnv`{.AgdaRecord} fixed at the pre-batch snapshot `RewardsOf certState₀` - ensures that every sub-transaction's balance-interval check (and any future Plutus - context derived from this field) sees the same balances independently of the - surrounding sub-transactions. Per-sub-transaction application would make these - views order-dependent across sub-transactions. - -+ **Direct deposits are a diff, not a sequence of state updates**. - - CIP-159 specifies that the `direct_deposits` field carries only the diff to be - applied (e.g., `0.1 ADA`, not the resulting `100.1 ADA` balance). Aggregating - each sub-transaction's diff via `∪⁺` (union-with-addition) and applying the - sum once is the natural reading: the batch-level - `allDirectDeposits`{.AgdaFunction} is the diff from pre-batch to post-batch. - Per-sub-transaction application would impose an artificial sequential - interpretation on what is logically a commutative aggregation. - -+ **Determinism and reorderability**. - - CIP-159 motivates direct deposits in part by their freedom from contention: - deposits into the same account from different parties can be processed "in any - order and fully parallel." Batch-wide application makes this manifest at the - rule level: the order of sub-transactions in the batch does not affect the - `accountBalances`{.AgdaField} visible to any sub-transaction's - `SUBUTXO`{.AgdaDatatype} or `CERTS`{.AgdaDatatype} step, nor the final - `rewards`{.AgdaField} reached after the deposit step. - -+ **`depositsChange`{.AgdaFunction} remains orthogonal**. - - `calculateDepositsChange`{.AgdaFunction} measures *protocol* deposit movements - (registration/deregistration of credentials, DReps, pools), which live in the - `deposits`{.AgdaField} fields of `DState`{.AgdaRecord}/`PState`{.AgdaRecord}/ - `GState`{.AgdaRecord} — not in `rewards`{.AgdaField}. Because - `applyDirectDeposits`{.AgdaFunction} touches only `rewards`{.AgdaField} and - runs *after* `calculateDepositsChange`{.AgdaFunction}, the two notions of - "deposit" remain cleanly disjoint without case analysis. - - -```agda data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → LedgerState → Type where LEDGER-V : @@ -434,7 +432,7 @@ data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LedgerState → TopLevelTx → Ledg ∙ IsValidFlagOf tx ≡ true ∙ ⟦ slot , ppolicy , pp , enactState , treasury , utxo₀ , IsValidFlagOf tx , allScripts , RewardsOf certState₀ ⟧ ⊢ ⟦ utxoState₀ , govState₀ , certState₀ ⟧ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ ⟦ utxoState₁ , govState₁ , certState₁ ⟧ ∙ ⟦ epoch slot , pp , ListOfGovVotesOf tx , WithdrawalsOf tx , allColdCreds govState₁ enactState ⟧ ⊢ certState₁ ⇀⦇ DCertsOf tx ,CERTS⦈ certState₂ - ∙ dom (allDirectDeposits tx) ⊆ dom (RewardsOf certState₂) + ∙ dom (DirectDepositsOf tx) ⊆ dom (RewardsOf certState₂) ∙ ⟦ TxIdOf tx , epoch slot , pp , ppolicy , enactState , certState₂ , dom (RewardsOf certState₂) ⟧ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂ ∙ ⟦ slot , pp , treasury , utxo₀ , depositsChange , allScripts , RewardsOf certState₀ ⟧ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂ ──────────────────────────────── diff --git a/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md index 6f211152f..8650ff3f9 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger/Properties/Computational.lagda.md @@ -82,83 +82,81 @@ instance ```agda - computeProof : (Γ : SubLedgerEnv) (s : LedgerState) (stx : SubLevelTx) - → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s') + computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s') ``` ```agda - completeness : (Γ : SubLedgerEnv) (s : LedgerState) (stx : SubLevelTx) (s' : LedgerState) - → Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s' → (proj₁ <$> computeProof Γ s stx) ≡ success s' + completeness : ∀ s' → Γ ⊢ s ⇀⦇ stx ,SUBLEDGER⦈ s' → (proj₁ <$> computeProof) ≡ success s' ``` ```agda - computeProof : (Γ : LedgerEnv) (s : LedgerState) (txTop : TopLevelTx) - → ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s') + computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s') ``` ```agda - completeness : (Γ : LedgerEnv) (s : LedgerState) (txTop : TopLevelTx) (s' : LedgerState) - → Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s' → (proj₁ <$> computeProof Γ s txTop) ≡ success s' + completeness : ∀ s' → Γ ⊢ s ⇀⦇ txTop ,LEDGER⦈ s' → (proj₁ <$> computeProof) ≡ success s' ``` + +## Module parameters + +We parameterize over the standard finite-map sum lemmas (same pattern as Conway). + + + +## Single-step lemma: `applyOne` decreases `getCoin` by `amt` + +When `stake addr ∈ dom acc` and `amt ≤ bal` (where `bal` is the current balance), +applying a single withdrawal decreases the total by exactly `amt`. + +```agda + applyOne-pov : + (acc : Rewards) (addr : RewardAddress) (amt bal : Coin) + → lookupᵐ? acc (stake addr) ≡ just bal + → amt ≤ bal + → getCoin acc ≡ getCoin (❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ)) + amt +``` + + + +## Fold invariant + +The fold invariant tracks three properties through the induction: + +1. All remaining withdrawal credentials are in the current accumulator's domain. +2. All remaining withdrawal amounts are bounded by the current balances. +3. Each credential appears at most once in the remaining list (NoDup on credentials). + + + +## Main lemma: fold over the full list + +```agda + applyOne : Rewards → RewardAddress × Coin → Rewards + applyOne ac (addr , amt) = + case lookupᵐ? ac (stake addr) of λ where + (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (ac ∣ ❴ stake addr ❵ ᶜ) + nothing → ac + + foldl-applyOne-pov : + (acc : Rewards) (entries : List (RewardAddress × Coin)) + → (∀ {addr amt} → (addr , amt) ∈ˡ entries + → stake addr ∈ dom acc + × amt ≤ maybe id 0 (lookupᵐ? acc (stake addr))) + -- → NoDup (map (stake ∘ proj₁) entries) -- needed for invariant preservation + → getCoin acc ≡ getCoin (foldl applyOne acc entries) + sum (map proj₂ entries) +``` + + + +## Top-level lemma + +This is the form needed by `PRE-CERT-pov`. + +```agda + applyWithdrawals-pov : + (wdrls : Withdrawals) (rwds : Rewards) + → mapˢ stake (dom wdrls) ⊆ dom rwds + → (∀[ (addr , amt) ∈ wdrls ˢ ] amt ≤ maybe id 0 (lookupᵐ? rwds (stake addr))) + → getCoin rwds ≡ getCoin (applyWithdrawals wdrls rwds) + getCoin wdrls +``` + + + +## Supporting lemmas (to be proved) + +The following auxiliary properties are needed but not yet proved. +They are standard finite-map facts independent of CIP-159. + +```agda + -- applyOne preserves domain membership for other credentials. + Claim-applyOne-dom-preserve : + ∀ (acc : Rewards) (addr : RewardAddress) (amt : Coin) (c : Credential) + → c ∈ dom acc → c ≢ stake addr + → c ∈ dom (case lookupᵐ? acc (stake addr) of λ where + (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ) + nothing → acc) + Claim-applyOne-dom-preserve = {!!} + + -- applyOne preserves balance for other credentials. + Claim-applyOne-balance-preserve : + ∀ (acc : Rewards) (addr : RewardAddress) (amt : Coin) (c : Credential) + → c ≢ stake addr + → lookupᵐ? (case lookupᵐ? acc (stake addr) of λ where + (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ) + nothing → acc) c + ≡ lookupᵐ? acc c + Claim-applyOne-balance-preserve = {!!} +``` diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md new file mode 100644 index 000000000..de1926b38 --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md @@ -0,0 +1,64 @@ +--- +source_branch: master +source_path: src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md +--- + +# CERTS: Preservation of Value {#sec:certs-pov} + + + +## Theorem: The `CERTS` rule preserves value {#thm:CERTS-PoV} + +```agda + CERTS-pov : {Γ : CertEnv} {s₁ sₙ : CertState} + → ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId + → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ + → getCoin s₁ ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ) +``` + +```agda + CERTS-pov {Γ = Γ} validNetId (run (pre-cert , certs)) = + trans (PRE-CERT-pov validNetId pre-cert) + (cong (_+ getCoin (WithdrawalsOf Γ)) {!!}) -- (sts-pov certs)) +``` diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md new file mode 100644 index 000000000..3f2ef5770 --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md @@ -0,0 +1,175 @@ +--- +source_branch: master +source_path: src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md +--- + + +# CERTS: Preservation of Value Lemmas {#sec:certs-pov-lemmas} + +## Key Differences from Conway + ++ **`PRE-CERT`**: Conway uses `constMap wdrlCreds 0 ∪ˡ rewards` (zeroing). + Dijkstra (CIP-159) uses `applyWithdrawals wdrls rewards` (subtraction). + The PoV equation still holds; the proof structure differs. ++ **`CERT` / `DELEG`**: Same value-relevant structure as Conway. ++ **No `CERT-vdel`**: Dijkstra has `CERT-deleg`, `CERT-pool`, `CERT-gov` only. + + + +## CERT-pov: Each certificate step preserves value + +```agda + CERT-pov : {Γ : CertEnv} {s s' : CertState} + → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' + → getCoin s ≡ getCoin s' +``` + + + +## POST-CERT-pov and sts-pov + +```agda + POST-CERT-pov : {Γ : CertEnv} {s s' : CertState} + → Γ ⊢ s ⇀⦇ _ ,POST-CERT⦈ s' → getCoin s ≡ getCoin s' + + POST-CERT-pov CERT-post = refl + + sts-pov : {Γ : CertEnv} {s₁ sₙ : CertState} {sigs : List DCert} + → RunTraceAndThen _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_ Γ s₁ sigs sₙ + → getCoin s₁ ≡ getCoin sₙ + sts-pov (run-[] x) = POST-CERT-pov x + sts-pov (run-∷ x xs) = trans (CERT-pov x) (sts-pov xs) +``` + +## PRE-CERT-pov (CIP-159: partial withdrawals) + +The key new assumption `applyWithdrawals-pov` states that applying withdrawals +decreases `rewardsBalance` by exactly the total withdrawn amount. This replaces +Conway's `constMap`/`res-decomp`/`sumConstZero` chain. + + + +```agda + PRE-CERT-pov : {Γ : CertEnv} {s s' : CertState} + → ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId + → Γ ⊢ s ⇀⦇ _ ,PRE-CERT⦈ s' + → getCoin s ≡ getCoin s' + getCoin (WithdrawalsOf Γ) +``` + + diff --git a/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md new file mode 100644 index 000000000..c6a50b8cd --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md @@ -0,0 +1,150 @@ +--- +source_branch: master +source_path: src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md +--- + +# LEDGER: Preservation of Value {#sec:ledger-pov} + +This module states the preservation-of-value property for the Dijkstra +`LEDGER`{.AgdaDatatype} rule, updated for CIP-159 (direct deposits and +partial withdrawals). + +## Key Differences from Conway + +1. **`UTxOState` has 3 fields** (no deposits) — simpler `HasCoin-UTxOState`. +2. **`LEDGER-V` applies `applyDirectDeposits`** after all sub-rules, creating + `certStateFinal` with increased rewards. Direct deposit value cancels + between `producedBatch` (UTxO side) and `certStateFinal` (CertState side). +3. **Batch structure**: `SUBLEDGERS` processes sub-transactions before top-level + `CERTS`/`GOVS`/`UTXOW`. Each `SUBLEDGER-V` step must preserve total value. +4. **Partial withdrawals**: `CERTS-pov` uses the new `applyWithdrawals` semantics. + + + +## HasCoin instances + +In Dijkstra, `UTxOState` has 3 fields (no deposits): + +```agda +instance + HasCoin-UTxOState : HasCoin UTxOState + HasCoin-UTxOState .getCoin s = getCoin (UTxOOf s) + FeesOf s + DonationsOf s + + HasCoin-LedgerState : HasCoin LedgerState + HasCoin-LedgerState .getCoin s = + getCoin (LedgerState.utxoSt s) + getCoin (LedgerState.certState s) +``` + +## Key Lemma: `applyDirectDeposits` increases `getCoin` by deposit total + +Since `applyDirectDeposits dd ds = record ds { rewards = RewardsOf ds ∪⁺ dd }`, +and `getCoin` for `CertState` is `rewardsBalance ∘ DStateOf = ∑[ x ← rewards ] x`, +we need: + + + +```agda + Claim-applyDirectDeposits-getCoin : + ∀ (dd : DirectDeposits) (ds : DState) + → getCoin (applyDirectDeposits dd ds) ≡ getCoin ds + getCoin dd + Claim-applyDirectDeposits-getCoin = ? +``` + +## LEDGER Preservation of Value + +```agda + LEDGER-pov : {Γ : LedgerEnv} {s s' : LedgerState} + → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' + → getCoin s ≡ getCoin s' +``` + +### Proof sketch + +**LEDGER-V case** (valid transaction): + +The `LEDGER-V` rule produces: + +`s' = ⟦ utxoSt₂ , rmOrphanDRepVotes certStateFinal govState₂ , certStateFinal ⟧` + +where `certStateFinal = record certState₂ { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf certState₂) }`. + +The proof decomposes as: + +1. `SUBLEDGERS` preserves total value: + `getCoin utxoSt₀ + getCoin certState₀ ≡ getCoin utxoSt₁ + getCoin certState₁` + (Each `SUBLEDGER-V` step preserves it via sub-CERTS-pov + sub-UTXO balance.) + +2. Top-level `CERTS-pov`: + `getCoin certState₁ ≡ getCoin certState₂ + getCoin (WithdrawalsOf tx)` + +3. `UTXO` premise `consumedBatch ≡ producedBatch` gives: + `getCoin utxoSt₁ + getCoin (WithdrawalsOf tx) + ... ≡ getCoin utxoSt₂ + getCoin (allDirectDeposits tx) + ...` + (The withdrawal terms on the consumed side cancel with CERTS-pov; + the direct deposit terms on the produced side cancel with step 4.) + +4. `applyDirectDeposits` adds exactly `getCoin (allDirectDeposits tx)` to certState₂: + `getCoin certStateFinal ≡ getCoin certState₂ + getCoin (allDirectDeposits tx)` + +5. **Cancellation**: direct deposits appear in `producedBatch` (UTxO side) and + in `certStateFinal` (CertState side), so they cancel in the total. + +**LEDGER-I case** (invalid transaction): + +`certState` is unchanged and `applyDirectDeposits` is not applied. +Follows the Conway pattern with `certState' ≡ certState₀`. + + From 840e8121191678a0298e6a0434c1b9835772a763 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Tue, 14 Apr 2026 21:33:58 -0600 Subject: [PATCH 08/14] =?UTF-8?q?`indexedSum=E1=B5=9B'-=E2=88=AA`=20and=20?= =?UTF-8?q?`sumConstZero`=20have=20proofs!?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit There were unresolved proof obligations from Conway. --- .../Conway/Conformance/Properties.lagda.md | 2 - .../Certs/Properties/PoV.lagda.md | 7 +- .../Certs/Properties/PoVLemmas.lagda.md | 126 +++++++----------- .../Ledger/Properties/PoV.lagda.md | 5 +- .../Utxo/Properties/GenMinSpend.lagda.md | 5 +- .../Properties/ApplyWithdrawalsPoV.lagda.md | 71 +++++++--- .../Certs/Properties/PoV.lagda.md | 2 +- .../Certs/Properties/PoVLemmas.lagda.md | 99 +++++--------- .../Ledger/Properties/PoV.lagda.md | 10 +- src/Ledger/Prelude.lagda.md | 67 ++++++++++ 10 files changed, 212 insertions(+), 182 deletions(-) diff --git a/src/Ledger/Conway/Conformance/Properties.lagda.md b/src/Ledger/Conway/Conformance/Properties.lagda.md index 02a6bda48..a0ef83016 100644 --- a/src/Ledger/Conway/Conformance/Properties.lagda.md +++ b/src/Ledger/Conway/Conformance/Properties.lagda.md @@ -124,8 +124,6 @@ module _ (s : ChainState) where -- Transaction properties module _ {slot} {tx} (let txb = body tx) (valid : validTxIn₂ s slot tx) - (indexedSum-∪⁺-hom : ∀ {A V : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq V ⦄ ⦃ mon : CommutativeMonoid 0ℓ 0ℓ V ⦄ - → (d₁ d₂ : A ⇀ V) → indexedSumᵛ' id (d₁ ∪⁺ d₂) ≡ indexedSumᵛ' id d₁ ◇ indexedSumᵛ' id d₂) (indexedSum-⊆ : ∀ {A : Type} ⦃ _ : DecEq A ⦄ (d d' : A ⇀ ℕ) → d ˢ ⊆ d' ˢ → indexedSumᵛ' id d ≤ indexedSumᵛ' id d') -- technically we could use an ordered monoid instead of ℕ where diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md index 80a46a5dd..08a732501 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md @@ -46,11 +46,8 @@ private variable instance _ = +-0-monoid -module Certs-PoV ( indexedSumᵛ'-∪' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → disjoint (dom m) (dom m') - → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) +module Certs-PoV -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`. - ( sumConstZero' : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 ) ( res-decomp' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ ) ( getCoin-cong' : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s' @@ -58,7 +55,7 @@ module Certs-PoV ( indexedSumᵛ'-∪' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' ( ≡ᵉ-getCoinˢ' : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) where - open Certs-Pov-lemmas indexedSumᵛ'-∪' sumConstZero' res-decomp' getCoin-cong' ≡ᵉ-getCoinˢ' + open Certs-Pov-lemmas res-decomp' getCoin-cong' ≡ᵉ-getCoinˢ' ``` --> diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md index 662a70526..9df670493 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md +++ b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md @@ -40,35 +40,7 @@ private variable instance _ = +-0-monoid -getCoin-singleton : ⦃ _ : DecEq A ⦄ {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c -getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _) - -∪ˡsingleton∈dom : ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin} - → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m -∪ˡsingleton∈dom m {(a , c)} a∈dom = ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom) - -module _ ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → disjoint (dom m) (dom m') - → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) - where - open ≡-Reasoning - open Equivalence - - ∪ˡsingleton∉dom : ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin} - → a ∉ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + c - ∪ˡsingleton∉dom m {(a , c)} a∉dom = begin - getCoin (m ∪ˡ ❴ a , c ❵ᵐ) - ≡⟨ indexedSumᵛ'-∪ m ❴ a , c ❵ᵐ - ( λ x y → a∉dom (subst (_∈ dom m) (from ∈-dom-singleton-pair y) x) ) ⟩ - getCoin m + getCoin ❴ a , c ❵ᵐ - ≡⟨ cong (getCoin m +_) getCoin-singleton ⟩ - getCoin m + c - ∎ - - ∪ˡsingleton0≡ : ⦃ _ : DecEq A ⦄ → (m : A ⇀ Coin) {a : A} → getCoin (m ∪ˡ ❴ (a , 0) ❵ᵐ) ≡ getCoin m - ∪ˡsingleton0≡ m {a} with a ∈? dom m - ... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom - ... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m)) +open ≡-Reasoning ``` --> @@ -83,61 +55,59 @@ some `dcert`{.AgdaBound} : `DCert`{.AgdaDatatype}. Then, *Formally*. ```agda - CERT-pov : {Γ : CertEnv} {s s' : CertState} - → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' - → getCoin s ≡ getCoin s' +CERT-pov : {Γ : CertEnv} {s s' : CertState} + → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' → getCoin s ≡ getCoin s' ``` *Proof*. (Click the "Show more Agda" button to reveal the proof.) diff --git a/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md index deef2d4f7..6aa0f8c53 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md @@ -38,9 +38,6 @@ instance module _ (tx : Tx) (let open Tx tx; open TxBody body) - ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → disjoint (dom m) (dom m') → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) - ( sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 ) ( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ ) ( getCoin-cong : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s' @@ -84,7 +81,7 @@ then the coin values of `s`{.AgdaBound} and `s'`{.AgdaBound} are equal, that is, open LState s' renaming (utxoSt to utxoSt'; govSt to govSt'; certState to certState') open CertState certState' open ≡-Reasoning - open Certs-PoV indexedSumᵛ'-∪ sumConstZero res-decomp getCoin-cong ≡ᵉ-getCoinˢ + open Certs-PoV res-decomp getCoin-cong ≡ᵉ-getCoinˢ zeroMap = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0 in begin diff --git a/src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md b/src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md index 9d0455be9..0e9671294 100644 --- a/src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md +++ b/src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md @@ -51,9 +51,6 @@ coin∅ = begin 0 ∎ where open Prelude.≡-Reasoning -getCoin-singleton : ((dp , c) : DepositPurpose × Coin) → indexedSumᵛ' id ❴ (dp , c) ❵ ≡ c -getCoin-singleton _ = indexedSum-singleton' {A = DepositPurpose × Coin} {f = proj₂} (finiteness _) - module _ -- ASSUMPTION -- (gc-hom : (d₁ d₂ : Deposits) → getCoin (d₁ ∪⁺ d₂) ≡ getCoin d₁ + getCoin d₂) where @@ -63,7 +60,7 @@ module _ -- ASSUMPTION -- getCoin (deps ∪⁺ ❴ (dp , c) ❵) ≡⟨ gc-hom deps ❴ (dp , c) ❵ ⟩ getCoin deps + getCoin{A = Deposits} ❴ (dp , c) ❵ - ≡⟨ cong (getCoin deps +_) (getCoin-singleton (dp , c)) ⟩ + ≡⟨ cong (getCoin deps +_) getCoin-singleton ⟩ getCoin deps + c ∎ where open Prelude.≡-Reasoning diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md index db5bf105d..e72871cad 100644 --- a/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md @@ -68,15 +68,13 @@ We parameterize over the standard finite-map sum lemmas (same pattern as Conway) @@ -95,21 +93,58 @@ applying a single withdrawal decreases the total by exactly `amt`. diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md index de1926b38..a1302dc48 100644 --- a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md @@ -60,5 +60,5 @@ module Certs-PoV ```agda CERTS-pov {Γ = Γ} validNetId (run (pre-cert , certs)) = trans (PRE-CERT-pov validNetId pre-cert) - (cong (_+ getCoin (WithdrawalsOf Γ)) {!!}) -- (sts-pov certs)) + (cong (_+ getCoin (WithdrawalsOf Γ)) (sts-pov indexedSumᵛ'-∪' certs)) ``` diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md index 3f2ef5770..1561e526c 100644 --- a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md @@ -40,52 +40,21 @@ private variable instance _ = +-0-monoid -getCoin-singleton : ⦃ _ : DecEq A ⦄ {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c -getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _) - -∪ˡsingleton∈dom : ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin} - → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m -∪ˡsingleton∈dom m {(a , c)} a∈dom = - ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom) - -module _ ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → disjoint (dom m) (dom m') - → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) - where - open ≡-Reasoning - open Equivalence - - ∪ˡsingleton∉dom : ⦃ _ : DecEq A ⦄ (m : A ⇀ Coin) {(a , c) : A × Coin} - → a ∉ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + c - ∪ˡsingleton∉dom m {(a , c)} a∉dom = begin - getCoin (m ∪ˡ ❴ a , c ❵ᵐ) - ≡⟨ indexedSumᵛ'-∪ m ❴ a , c ❵ᵐ - ( λ x y → a∉dom (subst (_∈ dom m) (from ∈-dom-singleton-pair y) x) ) ⟩ - getCoin m + getCoin ❴ a , c ❵ᵐ - ≡⟨ cong (getCoin m +_) getCoin-singleton ⟩ - getCoin m + c - ∎ - - ∪ˡsingleton0≡ : ⦃ _ : DecEq A ⦄ → (m : A ⇀ Coin) {a : A} - → getCoin (m ∪ˡ ❴ (a , 0) ❵ᵐ) ≡ getCoin m - ∪ˡsingleton0≡ m {a} with a ∈? dom m - ... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom - ... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m)) +open ≡-Reasoning ``` --> ## CERT-pov: Each certificate step preserves value ```agda - CERT-pov : {Γ : CertEnv} {s s' : CertState} - → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' - → getCoin s ≡ getCoin s' +CERT-pov : {Γ : CertEnv} {s s' : CertState} + → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' → getCoin s ≡ getCoin s' ``` ## POST-CERT-pov and sts-pov ```agda - POST-CERT-pov : {Γ : CertEnv} {s s' : CertState} - → Γ ⊢ s ⇀⦇ _ ,POST-CERT⦈ s' → getCoin s ≡ getCoin s' +POST-CERT-pov : {Γ : CertEnv} {s s' : CertState} + → Γ ⊢ s ⇀⦇ _ ,POST-CERT⦈ s' → getCoin s ≡ getCoin s' - POST-CERT-pov CERT-post = refl +POST-CERT-pov CERT-post = refl - sts-pov : {Γ : CertEnv} {s₁ sₙ : CertState} {sigs : List DCert} - → RunTraceAndThen _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_ Γ s₁ sigs sₙ - → getCoin s₁ ≡ getCoin sₙ - sts-pov (run-[] x) = POST-CERT-pov x - sts-pov (run-∷ x xs) = trans (CERT-pov x) (sts-pov xs) +sts-pov : {Γ : CertEnv} {s₁ sₙ : CertState} {sigs : List DCert} + → RunTraceAndThen _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_ Γ s₁ sigs sₙ + → getCoin s₁ ≡ getCoin sₙ +sts-pov (run-[] x) = POST-CERT-pov x +sts-pov (run-∷ x xs) = trans (CERT-pov x) (sts-pov xs) ``` ## PRE-CERT-pov (CIP-159: partial withdrawals) @@ -137,25 +106,25 @@ Conway's `constMap`/`res-decomp`/`sumConstZero` chain. diff --git a/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md index c6a50b8cd..9e5d7f8e4 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md @@ -85,9 +85,9 @@ module _ → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) -- CIP-159–specific assumption: ∪⁺ adds getCoin values - ( applyDirectDeposits-getCoin : + ( applyDirectDeposits-rewardsBalance : (dd : DirectDeposits) (ds : DState) - → getCoin (applyDirectDeposits dd ds) ≡ getCoin ds + getCoin dd ) + → rewardsBalance (applyDirectDeposits dd ds) ≡ rewardsBalance ds + getCoin dd ) where ``` @@ -96,8 +96,8 @@ module _ ```agda Claim-applyDirectDeposits-getCoin : ∀ (dd : DirectDeposits) (ds : DState) - → getCoin (applyDirectDeposits dd ds) ≡ getCoin ds + getCoin dd - Claim-applyDirectDeposits-getCoin = ? + → rewardsBalance (applyDirectDeposits dd ds) ≡ rewardsBalance ds + getCoin dd + Claim-applyDirectDeposits-getCoin = applyDirectDeposits-rewardsBalance ``` ## LEDGER Preservation of Value @@ -145,6 +145,6 @@ Follows the Conway pattern with `certState' ≡ certState₀`. diff --git a/src/Ledger/Prelude.lagda.md b/src/Ledger/Prelude.lagda.md index 17ddc3427..878a89eeb 100644 --- a/src/Ledger/Prelude.lagda.md +++ b/src/Ledger/Prelude.lagda.md @@ -41,6 +41,10 @@ open import Tactic.Derive.DecEq public open import Tactic.Inline public open import MyDebugOptions public open import Prelude.STS.GenPremises public +open import Data.List.Membership.Propositional.Properties using (∈-deduplicate⁻) +-- Data.List.Relation.Unary.Unique.DecPropositional.Properties + + open import abstract-set-theory.FiniteSetTheory public renaming (_⊆_ to _⊆ˢ_) @@ -51,6 +55,9 @@ open import Data.Integer using (0ℤ) public import Data.Rational as ℚ open import Data.Rational using (ℚ) +open import Data.Nat.Properties using (+-identityʳ) + + dec-de-morgan : ∀{P Q : Type} → ⦃ P ⁇ ⦄ → ¬ (P × Q) → ¬ P ⊎ ¬ Q dec-de-morgan ⦃ ⁇ no ¬p ⦄ ¬pq = inj₁ ¬p dec-de-morgan ⦃ ⁇ yes p ⦄ ¬pq = inj₂ λ q → ¬pq (p , q) @@ -98,4 +105,64 @@ Is-∅ X = Is-[] (setToList X) concatMapˡ : {A B : Type} → (A → ℙ B) → List A → ℙ B concatMapˡ f as = proj₁ $ unions (fromList (map f as)) + +indexedSumL-proj₂-zero : ∀ {A : Type} (l : List (A × Coin)) + → (∀ {x} → x ∈ˡ l → proj₂ x ≡ 0) + → indexedSumL {M = Coin} proj₂ l ≡ 0 +indexedSumL-proj₂-zero [] _ = refl +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)) + +module _ {A : Type} ⦃ _ : DecEq A ⦄ where + + getCoin-singleton : {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c + getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _) + + indexedSumᵛ'-∪ : (m m' : A ⇀ Coin) → disjoint (dom m) (dom m') + → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' + indexedSumᵛ'-∪ m m' disj = + trans (indexedSumᵐ-∪ˡ-∪ˡᶠ m m') + (indexedSumᵐ-∪ {X = m ᶠᵐ} {m' ᶠᵐ} {f = proj₂} disj) + + ∪ˡsingleton∈dom : (m : A ⇀ Coin) {(a , c) : A × Coin} + → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + ∪ˡsingleton∈dom m {(a , c)} a∈dom = ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom) + + ∪ˡsingleton∉dom : (m : A ⇀ Coin) {(a , c) : A × Coin} + → a ∉ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m + c + ∪ˡsingleton∉dom m {(a , c)} a∉dom = + trans (indexedSumᵛ'-∪ m ❴ a , c ❵ᵐ ( λ x y → a∉dom (subst (_∈ dom m) (from ∈-dom-singleton-pair y) x) )) + (cong (getCoin m +_) getCoin-singleton) + where open Equivalence + + ∪ˡsingleton0≡ : (m : A ⇀ Coin) {a : A} → getCoin (m ∪ˡ ❴ (a , 0) ❵ᵐ) ≡ getCoin m + ∪ˡsingleton0≡ m {a} with a ∈? dom m + ... | yes a∈dom = ∪ˡsingleton∈dom m a∈dom + ... | no a∉dom = trans (∪ˡsingleton∉dom m a∉dom) (+-identityʳ (getCoin m)) + + +opaque + unfolding List-Model finiteness + + sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 + sumConstZero {A} {X} = indexedSumL-proj₂-zero (deduplicate _≟_ l) all-zero-dedup + where + open Equivalence + + fin : finite (mapˢ (_, 0) X) + fin = finiteness (mapˢ (_, 0) X) + + l : List (A × Coin) + l = fin .proj₁ + + h : ∀ {a} → a ∈ (mapˢ (_, 0) X) ⇔ a ∈ˡ l + h = fin .proj₂ + + all-zero : ∀ {x} → x ∈ˡ l → proj₂ x ≡ 0 + all-zero x∈l with from ∈-map (from h x∈l) + ... | (a , refl , _) = refl + + all-zero-dedup : ∀ {x} → x ∈ˡ deduplicate _≟_ l → proj₂ x ≡ 0 + all-zero-dedup x∈dedup = all-zero (∈-deduplicate⁻ (DecEq._≟_ DecEq-×′) l x∈dedup) ``` From c207193c7f3f48141f8562125b7dd4daf5b4317f Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 15 Apr 2026 21:05:03 -0600 Subject: [PATCH 09/14] CIP-159-11: applyWithdrawals-pov and new library lemmas (#1123) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add the applyWithdrawals preservation-of-value proof machinery and prove several lemmas that were previously assumed as module parameters in Conway. New proofs in Ledger.Prelude (previously Conway module parameters): - indexedSumᵛ'-∪: getCoin distributes over disjoint ∪ˡ - sumConstZero: getCoin (constMap X 0) ≡ 0 - getCoin-cong: indexedSum' proj₂ respects set equality - res-decomp: (m ∪ˡ m') ≡ᵉ (m ∪ˡ (m' ∣ dom m ᶜ)) - getCoin-singleton, ≡ᵉ-getCoin, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom, ∪ˡsingleton0≡: singleton map getCoin lemmas - indexedSumL-proj₂-zero: sum of zero-valued entries is zero - setToList-∈: opaque bridge from list membership to set membership New module Certs.Properties.ApplyWithdrawalsPoV: - applyOne-pov: single withdrawal step decreases getCoin by amt - foldl-applyOne-pov: fold induction with Unique invariant - applyWithdrawals-pov: top-level lemma for PRE-CERT-pov - ∪ˡ-res-dom-preserve: ∪ˡ with complement restriction preserves domain membership for other credentials Remaining assumptions (deferred to agda-sets library): - ∪ˡ-res-lookup-preserve: lookupᵐ? stability under ∪ˡ for other keys - sum-map-proj₂≡getCoin: relates list-level sum to indexedSumᵛ' - setToList-Unique: credential uniqueness of withdrawal list - ≡ᵉ-getCoinˢ: getCoin invariance under injective key renaming --- .../Certs/Properties/PoV.lagda.md | 12 +- .../Certs/Properties/PoVLemmas.lagda.md | 16 +- .../Ledger/Properties/PoV.lagda.md | 13 +- .../Dijkstra/Specification/Certs.lagda.md | 27 +- .../Specification/Certs/Properties.lagda.md | 3 + .../Properties/ApplyWithdrawalsPoV.lagda.md | 381 +++++++++--------- .../Certs/Properties/PoV.lagda.md | 30 +- .../Certs/Properties/PoVLemmas.lagda.md | 25 +- .../Ledger/Properties/PoV.lagda.md | 45 +-- src/Ledger/Prelude.lagda.md | 28 +- 10 files changed, 295 insertions(+), 285 deletions(-) diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md index 08a732501..db2c5ba60 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md @@ -47,15 +47,11 @@ instance _ = +-0-monoid module Certs-PoV - -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`. - ( res-decomp' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ ) - ( getCoin-cong' : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s' - → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' ) - ( ≡ᵉ-getCoinˢ' : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} - → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) + -- TODO: prove the following assumption, used in roof of `CERTBASE-pov`. + ( ≡ᵉ-getCoinˢ' : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} + → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) where - open Certs-Pov-lemmas res-decomp' getCoin-cong' ≡ᵉ-getCoinˢ' + open Certs-Pov-lemmas ≡ᵉ-getCoinˢ' ``` --> diff --git a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md index 9df670493..a481556fa 100644 --- a/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md +++ b/src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md @@ -23,7 +23,7 @@ open import Axiom.Set.Properties th open import Algebra using (CommutativeMonoid) open import Data.Maybe.Properties open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid; +-identityʳ; +-identityˡ) -open import Relation.Binary using (IsEquivalence) +import Relation.Binary as Eq using (IsEquivalence) open import Relation.Nullary.Decidable open import Tactic.ReduceDec @@ -77,7 +77,7 @@ CERT-pov {s = ⟦ _ , stᵖ , stᵍ ⟧ᶜˢ}{⟦ _ , stᵖ' , stᵍ' ⟧ᶜˢ} getCoin ⟦ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ , stᵖ' , stᵍ' ⟧ ∎ where - module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin}) + module ≡ᵉ = Eq.IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin}) rwds-∪ˡ-decomp = (rwds ∣ ❴ c ❵ ᶜ) ∪ˡ (rwds ∣ ❴ c ❵ ) rwds-∪ˡ-∪ : rwds-∪ˡ-decomp ˢ ≡ᵉ (rwds ∣ ❴ c ❵ ᶜ)ˢ ∪ (rwds ∣ ❴ c ❵)ˢ @@ -100,13 +100,9 @@ injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈))) module Certs-Pov-lemmas - -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`. - ( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ ) - ( getCoin-cong : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s' - → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' ) - ( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} - → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) + -- TODO: prove the following assumption, used in roof of `CERTBASE-pov`. + ( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} + → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) where ``` --> @@ -145,7 +141,7 @@ value of the withdrawals in `Γ`{.AgdaBound}. In other terms, let open DState (dState cs ) open DState (dState cs') renaming (rewards to rewards') - module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin}) + module ≡ᵉ = Eq.IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin}) wdrlsCC = mapˢ (map₁ RewardAddress.stake) (wdrls ˢ) zeroMap = constMap (mapˢ RewardAddress.stake (dom wdrls)) 0 rwds-∪ˡ-decomp = (rewards ∣ dom wdrlsCC ᶜ) ∪ˡ (rewards ∣ dom wdrlsCC) diff --git a/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md b/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md index 6aa0f8c53..cf2123092 100644 --- a/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md +++ b/src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md @@ -38,12 +38,9 @@ instance module _ (tx : Tx) (let open Tx tx; open TxBody body) - ( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ ) - ( getCoin-cong : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s' - → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' ) - ( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} - → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) + -- TODO: prove the following assumption, used in roof of `CERTBASE-pov`. + ( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} + → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) where pattern UTXO-induction r = UTXO-inductive⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ r _ _ _ @@ -81,8 +78,8 @@ then the coin values of `s`{.AgdaBound} and `s'`{.AgdaBound} are equal, that is, open LState s' renaming (utxoSt to utxoSt'; govSt to govSt'; certState to certState') open CertState certState' open ≡-Reasoning - open Certs-PoV res-decomp getCoin-cong ≡ᵉ-getCoinˢ - zeroMap = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0 + open Certs-PoV ≡ᵉ-getCoinˢ + zeroMap = constMap (mapˢ RewardAddress.stake (dom txWithdrawals)) 0 in begin getCoin utxoSt + getCoin certState diff --git a/src/Ledger/Dijkstra/Specification/Certs.lagda.md b/src/Ledger/Dijkstra/Specification/Certs.lagda.md index 830f0ee31..52e930a6d 100644 --- a/src/Ledger/Dijkstra/Specification/Certs.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs.lagda.md @@ -294,22 +294,23 @@ The `LEDGER`{.AgdaDatatype} rule will call `applyDirectDeposits`{.AgdaFunction} credit direct deposits to account balances as part of processing a transaction batch. ```agda +-- For each withdrawal entry `(addr, amt)`, look up `stake addr` in the acc, +-- compute `bal ∸ amt`, create a singleton map with the new balance, and +-- merge it with the rest (complement-restricted, to remove the old entry). +applyOne : Rewards → RewardAddress × Coin → Rewards +applyOne acc (addr , amt) = + case lookupᵐ? acc (stake addr) of λ where + (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ) + nothing → acc + -- `nothing` case is defensive; the PRE-CERT precondition guarantees the + -- credential is registered, but handling it makes the function total. + applyWithdrawals : Withdrawals → Rewards → Rewards -applyWithdrawals wdrls rwds = - foldl applyOne rwds (setToList (wdrls ˢ)) - where - -- For each withdrawal entry `(addr, amt)`, look up `stake addr` in the acc, - -- compute `bal ∸ amt`, create a singleton map with the new balance, and - -- merge it with the rest (complement-restricted, to remove the old entry). - applyOne : Rewards → RewardAddress × Coin → Rewards - applyOne acc (addr , amt) = - case lookupᵐ? acc (stake addr) of λ where - (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ) - nothing → acc - -- `nothing` case is defensive; the PRE-CERT precondition guarantees the - -- credential is registered, but handling it makes the function total. +applyWithdrawals wdrls rwds = foldl applyOne rwds (setToList (wdrls ˢ)) ``` + + In the Dijkstra era, CIP-159 allows **partial withdrawals**: a transaction may withdraw any amount up to the current account balance. `applyWithdrawals`{.AgdaFunction} subtracts each withdrawal amount from the diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties.lagda.md index 4efa18eed..da5138584 100644 --- a/src/Ledger/Dijkstra/Specification/Certs/Properties.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties.lagda.md @@ -13,5 +13,8 @@ module Ledger.Dijkstra.Specification.Certs.Properties where --> ```agda +open import Ledger.Dijkstra.Specification.Certs.Properties.ApplyWithdrawalsPoV open import Ledger.Dijkstra.Specification.Certs.Properties.Computational +open import Ledger.Dijkstra.Specification.Certs.Properties.PoV +open import Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas ``` diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md index e72871cad..14d3587a2 100644 --- a/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md @@ -3,7 +3,6 @@ source_branch: master source_path: src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md --- - # `applyWithdrawals` Preservation of Value {#sec:apply-withdrawals-pov} This module proves that `applyWithdrawals` decreases the total rewards balance @@ -49,9 +48,15 @@ open import Axiom.Set.Properties th open import Data.Nat.Properties using ( +-0-monoid; +-identityʳ; +-identityˡ; +-comm; +-assoc ; m∸n+n≡m ) +open import Data.Maybe.Properties using (just-injective) +open import Data.List.Relation.Unary.Unique.Propositional using (Unique) renaming (_∷_ to _::_) +open import Data.List.Relation.Unary.Any using (Any) +open import Data.List.Membership.Propositional.Properties using (∈-map⁺) +import Data.List.Relation.Unary.All as All open import Relation.Binary using (IsEquivalence) - +open import Data.Nat.Properties using (n≤0⇒n≡0) open RewardAddress +open Any private variable A : Type @@ -61,232 +66,242 @@ instance ``` --> -## Module parameters +## Supporting lemmas + +The following auxiliary properties are needed. -We parameterize over the standard finite-map sum lemmas (same pattern as Conway). +### Single-step Lemma: `applyOne` decreases `getCoin` by `amt` + +When `stake addr ∈ dom acc` and `amt ≤ bal` (where `bal` is the current balance), +applying a single withdrawal decreases the total by exactly `amt`. + +```agda +applyOne-pov : + (acc : Rewards) (addr : RewardAddress) (amt bal : Coin) + → lookupᵐ? acc (stake addr) ≡ just bal + → amt ≤ bal + → getCoin acc ≡ getCoin (❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ)) + amt +``` -## Single-step lemma: `applyOne` decreases `getCoin` by `amt` -When `stake addr ∈ dom acc` and `amt ≤ bal` (where `bal` is the current balance), -applying a single withdrawal decreases the total by exactly `amt`. +### Domain Membership Preservation Lemma ```agda - applyOne-pov : - (acc : Rewards) (addr : RewardAddress) (amt bal : Coin) - → lookupᵐ? acc (stake addr) ≡ just bal - → amt ≤ bal - → getCoin acc ≡ getCoin (❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ)) + amt +∪ˡ-res-dom-preserve : + ∀ (m : Rewards) (c : Credential) (v : Coin) (c' : Credential) + → c' ∈ dom m → c' ≢ c + → c' ∈ dom (❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ)) ``` -## Fold invariant - -The fold invariant tracks three properties through the induction: - -1. All remaining withdrawal credentials are in the current accumulator's domain. -2. All remaining withdrawal amounts are bounded by the current balances. -3. Each credential appears at most once in the remaining list (NoDup on credentials). +-- applyOne preserves balance for other credentials. +module ApplyWithdrawals-PoV + -- ASSUMPTIONS -- -## Main lemma: fold over the full list + -- TODO: ask that these be proved in the `agda-sets` library. -```agda - applyOne : Rewards → RewardAddress × Coin → Rewards - applyOne ac (addr , amt) = - case lookupᵐ? ac (stake addr) of λ where - (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (ac ∣ ❴ stake addr ❵ ᶜ) - nothing → ac - - foldl-applyOne-pov : - (acc : Rewards) (entries : List (RewardAddress × Coin)) - → (∀ {addr amt} → (addr , amt) ∈ˡ entries - → stake addr ∈ dom acc - × amt ≤ maybe id 0 (lookupᵐ? acc (stake addr))) - -- → NoDup (map (stake ∘ proj₁) entries) -- needed for invariant preservation - → getCoin acc ≡ getCoin (foldl applyOne acc entries) + sum (map proj₂ entries) -``` + -- 1. For any credential `c'` other than `c`, lookupᵐ? (❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ)) c' ≡ lookupᵐ? m c' + ( ∪ˡ-res-lookup-preserve : ∀ (m : Rewards) (c : Credential) (v : Coin) (c' : Credential) + → c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ)) c' ≡ lookupᵐ? m c' ) + -- It's hard because the `agda-sets` API requires instance resolution for + -- `lookupᵐ?`, but the semantic content is clear (lookup in a left-biased union + -- for a key not in the left map equals lookup in the right map, and complement + -- restriction doesn't affect keys ≢ c); threading it through the `⁇` instance + -- resolution is painful library plumbing. - -## Top-level lemma + +## Main Theorem This is the form needed by `PRE-CERT-pov`. ```agda - applyWithdrawals-pov : - (wdrls : Withdrawals) (rwds : Rewards) + applyWithdrawals-pov : (wdrls : Withdrawals) (rwds : Rewards) → mapˢ stake (dom wdrls) ⊆ dom rwds - → (∀[ (addr , amt) ∈ wdrls ˢ ] amt ≤ maybe id 0 (lookupᵐ? rwds (stake addr))) + → ∀[ (addr , amt) ∈ wdrls ˢ ] amt ≤ maybe id 0 (lookupᵐ? rwds (stake addr)) → getCoin rwds ≡ getCoin (applyWithdrawals wdrls rwds) + getCoin wdrls ``` -## Supporting lemmas (to be proved) -The following auxiliary properties are needed but not yet proved. -They are standard finite-map facts independent of CIP-159. -```agda - -- applyOne preserves domain membership for other credentials. - Claim-applyOne-dom-preserve : - ∀ (acc : Rewards) (addr : RewardAddress) (amt : Coin) (c : Credential) - → c ∈ dom acc → c ≢ stake addr - → c ∈ dom (case lookupᵐ? acc (stake addr) of λ where - (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ) - nothing → acc) - Claim-applyOne-dom-preserve = {!!} - - -- applyOne preserves balance for other credentials. - Claim-applyOne-balance-preserve : - ∀ (acc : Rewards) (addr : RewardAddress) (amt : Coin) (c : Credential) - → c ≢ stake addr - → lookupᵐ? (case lookupᵐ? acc (stake addr) of λ where - (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ) - nothing → acc) c - ≡ lookupᵐ? acc c - Claim-applyOne-balance-preserve = {!!} -``` diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md index a1302dc48..a73783756 100644 --- a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md @@ -14,13 +14,17 @@ open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure) module Ledger.Dijkstra.Specification.Certs.Properties.PoV (gs : GovStructure) (open GovStructure gs) where +open import Ledger.Prelude + open import Ledger.Dijkstra.Specification.Certs gs open import Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas gs open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no) open import Ledger.Prelude +open import Data.List.Relation.Unary.Unique.Propositional using (Unique) open import Data.Nat.Properties using (+-0-monoid) open CertState +open RewardAddress private variable l : List DCert @@ -29,22 +33,14 @@ instance _ = +-0-monoid module Certs-PoV - ( indexedSumᵛ'-∪' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → disjoint (dom m) (dom m') - → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) - ( applyWithdrawals-pov' : - (wdrls : Withdrawals) (rwds : Rewards) - → mapˢ RewardAddress.stake (dom wdrls) ⊆ dom rwds - → (∀[ (addr , amt) ∈ wdrls ˢ ] - amt ≤ maybe id 0 (lookupᵐ? rwds (RewardAddress.stake addr))) - → getCoin rwds ≡ getCoin (applyWithdrawals wdrls rwds) + getCoin wdrls ) - ( ≡ᵉ-getCoinˢ' : - {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ - (s : ℙ (A × Coin)) {f : A → A'} - → InjectiveOn (dom s) f - → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) - where - open Certs-Pov-lemmas indexedSumᵛ'-∪' applyWithdrawals-pov' ≡ᵉ-getCoinˢ' + ( ∪ˡ-res-lookup-preserve : ∀ (m : Rewards) (c : Credential) (v : Coin) (c' : Credential) + → c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ)) c' ≡ lookupᵐ? m c' ) + + ( sum-map-proj₂≡getCoin : ∀ (m : Withdrawals) → sum (map proj₂ (setToList (m ˢ))) ≡ getCoin m ) + + ( setToList-Unique : ∀ (m : Withdrawals) → Unique (map (stake ∘ proj₁) (setToList (m ˢ))) ) + where + open Certs-Pov-lemmas ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique ``` --> @@ -60,5 +56,5 @@ module Certs-PoV ```agda CERTS-pov {Γ = Γ} validNetId (run (pre-cert , certs)) = trans (PRE-CERT-pov validNetId pre-cert) - (cong (_+ getCoin (WithdrawalsOf Γ)) (sts-pov indexedSumᵛ'-∪' certs)) + (cong (_+ getCoin (WithdrawalsOf Γ)) (sts-pov certs)) ``` diff --git a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md index 1561e526c..80c0f3d11 100644 --- a/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md @@ -24,12 +24,17 @@ module Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas (gs : GovStructure) (open GovStructure gs) where open import Ledger.Dijkstra.Specification.Certs gs +open import Ledger.Dijkstra.Specification.Certs.Properties.ApplyWithdrawalsPoV gs open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no) open import Ledger.Prelude + open import Axiom.Set.Properties th + +open import Data.List.Relation.Unary.Unique.Propositional using (Unique) open import Data.Nat.Properties using (+-0-monoid; +-identityʳ) open import Relation.Binary using (IsEquivalence) +open RewardAddress open Computational ⦃...⦄ open CertState @@ -113,18 +118,14 @@ injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈))) module Certs-Pov-lemmas - ( applyWithdrawals-pov : - (wdrls : Withdrawals) (rwds : Rewards) - → mapˢ RewardAddress.stake (dom wdrls) ⊆ dom rwds - → (∀[ (addr , amt) ∈ wdrls ˢ ] - amt ≤ maybe id 0 (lookupᵐ? rwds (RewardAddress.stake addr))) - → getCoin rwds ≡ getCoin (applyWithdrawals wdrls rwds) + getCoin wdrls ) - ( ≡ᵉ-getCoinˢ : - {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ - (s : ℙ (A × Coin)) {f : A → A'} - → InjectiveOn (dom s) f - → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) + ( ∪ˡ-res-lookup-preserve : ∀ (m : Rewards) (c : Credential) (v : Coin) (c' : Credential) + → c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ)) c' ≡ lookupᵐ? m c' ) + + ( sum-map-proj₂≡getCoin : ∀ (m : Withdrawals) → sum (map proj₂ (setToList (m ˢ))) ≡ getCoin m ) + + ( setToList-Unique : ∀ (m : Withdrawals) → Unique (map (stake ∘ proj₁) (setToList (m ˢ))) ) where + open ApplyWithdrawals-PoV ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique ``` --> @@ -139,6 +140,6 @@ module Certs-Pov-lemmas ```agda PRE-CERT-pov {Γ = Γ} {s = cs} validNetId (CERT-pre {wdrls = wdrls} (_ , wdrlCreds⊆rwds , wdrlBounded)) = - applyWithdrawals-pov wdrls (DState.rewards (dState cs)) wdrlCreds⊆rwds wdrlBounded + applyWithdrawals-pov wdrls (RewardsOf (dState cs)) wdrlCreds⊆rwds wdrlBounded ``` --> diff --git a/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md index 9e5d7f8e4..513a560d1 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md @@ -31,15 +31,21 @@ module Ledger.Dijkstra.Specification.Ledger.Properties.PoV (abs : AbstractFunctions txs) (open AbstractFunctions abs) where +open import Ledger.Prelude + +open import Axiom.Set.Properties th + open import Ledger.Dijkstra.Specification.Certs govStructure --- open import Ledger.Dijkstra.Specification.Certs.Properties.PoV govStructure +open import Ledger.Dijkstra.Specification.Certs.Properties.PoV govStructure open import Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas govStructure open import Ledger.Dijkstra.Specification.Ledger txs abs open import Ledger.Dijkstra.Specification.Utxo txs abs open import Ledger.Dijkstra.Specification.Utxow txs abs -open import Ledger.Prelude -open import Axiom.Set.Properties th + +open import Data.List.Relation.Unary.Unique.Propositional using (Unique) open import Data.Nat.Properties using (+-0-monoid; +-identityʳ; +-comm; +-assoc) + +open RewardAddress ``` --> @@ -69,20 +75,12 @@ module _ (tx : TopLevelTx) (let open Tx tx) -- Shared assumptions (same pattern as Conway) - ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) - → disjoint (dom m) (dom m') - → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' ) - ( applyWithdrawals-pov : - (wdrls : Withdrawals) (rwds : Rewards) - → mapˢ RewardAddress.stake (dom wdrls) ⊆ dom rwds - → (∀[ (addr , amt) ∈ wdrls ˢ ] - amt ≤ maybe id 0 (lookupᵐ? rwds (RewardAddress.stake addr))) - → getCoin rwds ≡ getCoin (applyWithdrawals wdrls rwds) + getCoin wdrls ) - ( ≡ᵉ-getCoinˢ : - {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ - (s : ℙ (A × Coin)) {f : A → A'} - → InjectiveOn (dom s) f - → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) + ( ∪ˡ-res-lookup-preserve : ∀ (m : Rewards) (c : Credential) (v : Coin) (c' : Credential) + → c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ)) c' ≡ lookupᵐ? m c' ) + + ( sum-map-proj₂≡getCoin : ∀ (m : Withdrawals) → sum (map proj₂ (setToList (m ˢ))) ≡ getCoin m ) + + ( setToList-Unique : ∀ (m : Withdrawals) → Unique (map (stake ∘ proj₁) (setToList (m ˢ))) ) -- CIP-159–specific assumption: ∪⁺ adds getCoin values ( applyDirectDeposits-rewardsBalance : @@ -90,22 +88,15 @@ module _ → rewardsBalance (applyDirectDeposits dd ds) ≡ rewardsBalance ds + getCoin dd ) where + open Certs-PoV ∪ˡ-res-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique ``` --> -```agda - Claim-applyDirectDeposits-getCoin : - ∀ (dd : DirectDeposits) (ds : DState) - → rewardsBalance (applyDirectDeposits dd ds) ≡ rewardsBalance ds + getCoin dd - Claim-applyDirectDeposits-getCoin = applyDirectDeposits-rewardsBalance -``` ## LEDGER Preservation of Value ```agda - LEDGER-pov : {Γ : LedgerEnv} {s s' : LedgerState} - → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' - → getCoin s ≡ getCoin s' + LEDGER-pov : {Γ : LedgerEnv} {s s' : LedgerState} → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s' ``` ### Proof sketch @@ -145,6 +136,6 @@ Follows the Conway pattern with `certState' ≡ certState₀`. diff --git a/src/Ledger/Prelude.lagda.md b/src/Ledger/Prelude.lagda.md index 878a89eeb..7c2d86d04 100644 --- a/src/Ledger/Prelude.lagda.md +++ b/src/Ledger/Prelude.lagda.md @@ -42,14 +42,14 @@ open import Tactic.Inline public open import MyDebugOptions public open import Prelude.STS.GenPremises public open import Data.List.Membership.Propositional.Properties using (∈-deduplicate⁻) --- Data.List.Relation.Unary.Unique.DecPropositional.Properties - - +open import Relation.Binary using (IsEquivalence) open import abstract-set-theory.FiniteSetTheory public renaming (_⊆_ to _⊆ˢ_) open import abstract-set-theory.Axiom.Set.Map.Extra th public +open import Axiom.Set.Properties th + import Data.Integer as ℤ open import Data.Integer using (0ℤ) public import Data.Rational as ℚ @@ -62,9 +62,6 @@ dec-de-morgan : ∀{P Q : Type} → ⦃ P ⁇ ⦄ → ¬ (P × Q) → ¬ P ⊎ dec-de-morgan ⦃ ⁇ no ¬p ⦄ ¬pq = inj₁ ¬p dec-de-morgan ⦃ ⁇ yes p ⦄ ¬pq = inj₂ λ q → ¬pq (p , q) -≡ᵉ-getCoin : ∀ {A} → ⦃ _ : DecEq A ⦄ → (s s' : A ⇀ Coin) → s ˢ ≡ᵉ s' ˢ → getCoin s ≡ getCoin s' -≡ᵉ-getCoin {A} ⦃ decEqA ⦄ s s' s≡s' = indexedSumᵛ'-cong {C = Coin} {x = s} {y = s'} s≡s' - setToMap : ∀ {A B : Type} → ⦃ DecEq A ⦄ → ℙ (A × B) → A ⇀ B setToMap = fromListᵐ ∘ setToList @@ -119,12 +116,24 @@ module _ {A : Type} ⦃ _ : DecEq A ⦄ where getCoin-singleton : {(a , c) : A × Coin} → indexedSumᵛ' id ❴ (a , c) ❵ ≡ c getCoin-singleton = indexedSum-singleton' {M = Coin} (finiteness _) + ≡ᵉ-getCoin : (s s' : A ⇀ Coin) → s ˢ ≡ᵉ s' ˢ → getCoin s ≡ getCoin s' + ≡ᵉ-getCoin s s' s≡s' = indexedSumᵛ'-cong {C = Coin} {x = s} {y = s'} s≡s' + + getCoin-cong : (s : A ⇀ Coin) (s' : ℙ (A × Coin)) + → s ˢ ≡ᵉ s' → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' + getCoin-cong s s' eq = indexedSum-cong {f = proj₂} {x = (s ˢ) ᶠˢ} {y = s' ᶠˢ} eq + indexedSumᵛ'-∪ : (m m' : A ⇀ Coin) → disjoint (dom m) (dom m') → getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' indexedSumᵛ'-∪ m m' disj = trans (indexedSumᵐ-∪ˡ-∪ˡᶠ m m') (indexedSumᵐ-∪ {X = m ᶠᵐ} {m' ᶠᵐ} {f = proj₂} disj) + + res-decomp : (m m' : A ⇀ Coin) → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ + res-decomp m m' = ∪-cong (≡ᵉ.refl {x = m ˢ}) (≡ᵉ.sym (filterᵐ-idem {m = m'})) + where module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {A × Coin}) + ∪ˡsingleton∈dom : (m : A ⇀ Coin) {(a , c) : A × Coin} → a ∈ dom m → getCoin (m ∪ˡ ❴ (a , c) ❵ᵐ) ≡ getCoin m ∪ˡsingleton∈dom m {(a , c)} a∈dom = ≡ᵉ-getCoin (m ∪ˡ ❴ (a , c) ❵) m (singleton-∈-∪ˡ {m = m} a∈dom) @@ -141,7 +150,6 @@ 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)) - opaque unfolding List-Model finiteness @@ -165,4 +173,10 @@ opaque all-zero-dedup : ∀ {x} → x ∈ˡ deduplicate _≟_ l → proj₂ x ≡ 0 all-zero-dedup x∈dedup = all-zero (∈-deduplicate⁻ (DecEq._≟_ DecEq-×′) l x∈dedup) + +opaque + unfolding setToList List-Model + + setToList-∈ : ∀ {A : Type} {a : A} {X : ℙ A} → a ∈ˡ setToList X → a ∈ X + setToList-∈ = id ``` From e6bc087a9a23858773e795a4ae445c3d5e24c871 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 16 Apr 2026 17:52:38 -0600 Subject: [PATCH 10/14] CIP-159-11: LEDGER-pov structure with LEDGER-I proved (#1123) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit State and partially prove the Dijkstra LEDGER preservation-of-value theorem with the corrected HasCoin-LedgerState that includes deposits. - LEDGER-I (invalid case): Fully proved via utxow-pov-invalid. - LEDGER-V (valid case): Equational chain with holes, to be filled. The HasCoin-LedgerState total is: getCoin utxoSt + rewardsBalance(certState) + coinFromDeposits(certState) Key insight: SUBLEDGERS-pov cannot be proved independently because individual SUBUTXO rules have no balance premise — only the batch-level consumedBatch ≡ producedBatch constrains the total. The LEDGER-V proof must reason about the entire step at once. --- .../Dijkstra/Specification/Certs.lagda.md | 4 +- .../Dijkstra/Specification/Ledger.lagda.md | 37 ++- .../Ledger/Properties/PoV.lagda.md | 246 ++++++++++++++---- .../Dijkstra/Specification/Utxo.lagda.md | 3 + 4 files changed, 233 insertions(+), 57 deletions(-) diff --git a/src/Ledger/Dijkstra/Specification/Certs.lagda.md b/src/Ledger/Dijkstra/Specification/Certs.lagda.md index 52e930a6d..210298760 100644 --- a/src/Ledger/Dijkstra/Specification/Certs.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Certs.lagda.md @@ -103,14 +103,14 @@ record PState : Type where field pools : Pools fPools : Pools - retiring : KeyHash ⇀ Epoch + retiring : Retiring deposits : KeyHash ⇀ Coin record GState : Type where constructor ⟦_,_,_⟧ᵛ field dreps : DReps - ccHotKeys : Credential ⇀ Maybe Credential + ccHotKeys : CCHotKeys deposits : Credential ⇀ Coin record CertState : Type where diff --git a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md index 90a6783eb..203f147b3 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger.lagda.md @@ -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 @@ -82,9 +85,9 @@ instance HasAccountBalances-SubLedgerEnv : HasAccountBalances SubLedgerEnv HasAccountBalances-SubLedgerEnv .AccountBalancesOf = SubLedgerEnv.accountBalances - ``` --> + ```agda record LedgerState : Type where ``` @@ -99,6 +102,7 @@ record LedgerState : Type where govSt : GovState certState : CertState ``` + + + + ## LEDGER Transition System -## HasCoin instances +## Key Lemma: `applyDirectDeposits` increases `getCoin` by deposit total -In Dijkstra, `UTxOState` has 3 fields (no deposits): +`applyDirectDeposits dd ds = record ds { rewards = RewardsOf ds ∪⁺ dd }`, +and `getCoin` for `CertState` is `rewardsBalance ∘ DStateOf = ∑[ x ← rewards ] x` -```agda -instance - HasCoin-UTxOState : HasCoin UTxOState - HasCoin-UTxOState .getCoin s = getCoin (UTxOOf s) + FeesOf s + DonationsOf s - HasCoin-LedgerState : HasCoin LedgerState - HasCoin-LedgerState .getCoin s = - getCoin (LedgerState.utxoSt s) + getCoin (LedgerState.certState s) -``` +## Proof Architecture -## Key Lemma: `applyDirectDeposits` increases `getCoin` by deposit total +The Dijkstra `LEDGER-pov`{.AgdaFunction} proof does NOT decompose into independent +`SUBLEDGERS-pov`{.AgdaFunction} and `UTXOW-pov`{.AgdaFunction} pieces, because: + +1. Individual `SUBUTXO` rules have no balance equation — only the + *batch-level* `consumedBatch ≡ producedBatch` (in `UTXO`) constrains + the total. + +2. Sub-transactions may individually transfer value between UTxO and CertState (via + sub-withdrawals, sub-deposits, sub-direct-deposits) without local balancing. + +Instead, the proof reasons about the **entire** `LEDGER-V`{.AgdaInductiveConstructor} +step at once. + +### LEDGER-V Proof Outline -Since `applyDirectDeposits dd ds = record ds { rewards = RewardsOf ds ∪⁺ dd }`, -and `getCoin` for `CertState` is `rewardsBalance ∘ DStateOf = ∑[ x ← rewards ] x`, +Given +`s = ⟦ utxoSt₀ , govSt₀ , certState₀ ⟧` +and +`s' = ⟦ utxoSt₂ , govSt₂' , certStateFinal ⟧`, +where +`certStateFinal` has `rewards = rewards₂ ∪⁺ allDirectDeposits tx`, we need: +`getCoin utxoSt₀ + rewardsBalance₀ + deposits₀` +`≡ getCoin utxoSt₂ + rewardsBalance_final + deposits₂` + +The key equations are: + +1. `consumedBatch ≡ producedBatch` (coin projection, from `UTXO`{.AgdaDatatype} premise). + + This gives (using `coin∘inject = id`, `coin mint = 0`): + + `Σ cbalance(utxo₀ ∣ SpendInputs_i) + Σ wdrls_i + depositRefunds` + `= Σ cbalance(outs_i) + txFee + Σ directDeps_i + Σ donations_i + newDeposits` + + where the sums range over all transactions in the batch (top + sub). + +2. `CERTS-pov` (combined sub + top level): + + `rewardsBalance₀ = rewardsBalance₂ + Σ wdrls_i` + + This requires composing sub-level `CERTS-pov` for each subtransaction + with top-level `CERTS-pov`. + +3. `depositsChange` property: + + `deposits₂ = deposits₀ + newDeposits - depositRefunds` + + This follows from the definition of `calculateDepositsChange` and + the posPart/negPart identity. + +4. `applyDirectDeposits`: + + `rewardsBalance_final = rewardsBalance₂ + Σ directDeps_i` + +5. Mechanical UTxO tracking: + + `getCoin utxoSt₂ = cbalance(utxo₂) + fees₂ + donations₂` + + where `utxo₂`, `fees₂`, `donations₂` are determined by the + `SUBLEDGERS` + `UTXO` mechanical state changes. + +Combining: + +From (1) and (3), adding the equations and using `+-cancelʳ-≡` to +eliminate `newDeposits + depositRefunds` from both sides: + ++ `getCoin utxoSt₀ + Σ wdrls_i + coinFromDeposits(cs₀)` + `= getCoin utxoSt₂ + Σ directDeps_i + coinFromDeposits(cs₂)` + +Then: + ++ `getCoin utxoSt₀ + rewardsBalance₀ + coinFromDeposits(cs₀)` + `= getCoin utxoSt₀ + (rewardsBalance₂ + Σ wdrls_i) + coinFromDeposits(cs₀)` (by 2) + `= getCoin utxoSt₂ + Σ directDeps_i + coinFromDeposits(cs₂) + rewardsBalance₂` (by combined 1+3) + `= getCoin utxoSt₂ + rewardsBalance_final + coinFromDeposits(cs₂)` (by 4) + `= getCoin utxoSt₂ + getCoin certStateFinal + coinFromDeposits(cs₂)` (since deposits unchanged by applyDirectDeposits) + + + +### `LEDGER-I` proof outline + +`certState` and `govSt` are unchanged. + +`SUBLEDGERS` is a no-op (`isValid ≡ false` ⟹ each `SUBLEDGER-I` preserves state). + +The UTXOW/UTXO step in the invalid case: + +`utxoSt₁ = ⟦ utxo₀ ∣ collateral ᶜ , fees + cbalance(utxo₀ ∣ collateral) , deposits₀ , donations₀ ⟧` + +(Actually in Dijkstra, deposits aren't in UTxOState, and the invalid case has +`depositsChange = ⟦ 0ℤ , 0ℤ ⟧`, so the UTxO changes are just collateral collection.) + +`getCoin utxoSt₁ = cbalance(utxo₀ ∣ coll ᶜ) + (fees + cbalance(utxo₀ ∣ coll)) + donations₀` + +`= cbalance utxo₀ + fees + donations₀` [by split-balance] + +`= getCoin utxoSt₀` + +So + +`getCoin s' = getCoin utxoSt₁ + getCoin certState₀ + coinFromDeposits certState₀` + +`= getCoin utxoSt₀ + getCoin certState₀ + coinFromDeposits certState₀` + +`= getCoin s` + + @@ -99,43 +230,68 @@ module _ LEDGER-pov : {Γ : LedgerEnv} {s s' : LedgerState} → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s' ``` -### Proof sketch - -**LEDGER-V case** (valid transaction): - -The `LEDGER-V` rule produces: - -`s' = ⟦ utxoSt₂ , rmOrphanDRepVotes certStateFinal govState₂ , certStateFinal ⟧` - -where `certStateFinal = record certState₂ { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf certState₂) }`. - -The proof decomposes as: +### LEDGER-I case (invalid transaction) -1. `SUBLEDGERS` preserves total value: - `getCoin utxoSt₀ + getCoin certState₀ ≡ getCoin utxoSt₁ + getCoin certState₁` - (Each `SUBLEDGER-V` step preserves it via sub-CERTS-pov + sub-UTXO balance.) +This follows the Conway pattern with `certState' ≡ certState₀`. +`certState` and `govSt` are unchanged and `applyDirectDeposits` is not applied. +Only the `UTXOW`{.AgdaDatatype} step matters and it preserves `getCoin utxoSt`. -2. Top-level `CERTS-pov`: - `getCoin certState₁ ≡ getCoin certState₂ + getCoin (WithdrawalsOf tx)` - -3. `UTXO` premise `consumedBatch ≡ producedBatch` gives: - `getCoin utxoSt₁ + getCoin (WithdrawalsOf tx) + ... ≡ getCoin utxoSt₂ + getCoin (allDirectDeposits tx) + ...` - (The withdrawal terms on the consumed side cancel with CERTS-pov; - the direct deposit terms on the produced side cancel with step 4.) +```agda + LEDGER-pov {Γ} {s} (LEDGER-I (invalid , subStep , utxoStep)) = + cong (λ u → u + getCoin (CertStateOf s) + coinFromDeposits (CertStateOf s)) + (utxow-pov-invalid utxoStep invalid) +``` -4. `applyDirectDeposits` adds exactly `getCoin (allDirectDeposits tx)` to certState₂: - `getCoin certStateFinal ≡ getCoin certState₂ + getCoin (allDirectDeposits tx)` +### LEDGER-V (valid transaction) -5. **Cancellation**: direct deposits appear in `producedBatch` (UTxO side) and - in `certStateFinal` (CertState side), so they cancel in the total. +The `LEDGER-V` rule produces -**LEDGER-I case** (invalid transaction): +`s' = ⟦ utxoSt₂ , rmOrphanDRepVotes certStateFinal govState₂ , certStateFinal ⟧` -`certState` is unchanged and `applyDirectDeposits` is not applied. -Follows the Conway pattern with `certState' ≡ certState₀`. +where `certStateFinal = record certState₂ { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf certState₂) }`. - diff --git a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md index e3814bc11..555f11043 100644 --- a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md @@ -256,6 +256,9 @@ minfee pp txTop utxo = pp .a * (SizeOf txTop) + pp .b instance HasCoin-UTxO : HasCoin UTxO HasCoin-UTxO .getCoin = cbalance + + HasCoin-UTxOState : HasCoin UTxOState + HasCoin-UTxOState .getCoin s = getCoin (UTxOOf s) + FeesOf s + DonationsOf s ``` --> From cf645b424442b2e581c78e496abc169ef6e32f67 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Thu, 16 Apr 2026 20:16:24 -0600 Subject: [PATCH 11/14] CIP-159-11: LEDGER-pov fully structured, all holes filled (#1123) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- .../Specification/Ledger/Properties.lagda.md | 1 + .../Ledger/Properties/PoV.lagda.md | 172 +++++++++++++++--- 2 files changed, 143 insertions(+), 30 deletions(-) diff --git a/src/Ledger/Dijkstra/Specification/Ledger/Properties.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger/Properties.lagda.md index 6caa69cfd..1d0b91bc9 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger/Properties.lagda.md +++ b/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 ``` diff --git a/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md index 2e5599b7f..ecb957c1f 100644 --- a/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md @@ -169,6 +169,32 @@ So @@ -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₂))) + ``` From c6163a32ad2f8a58fd48cd76e344389f8f71a50e Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Tue, 21 Apr 2026 21:21:37 -0600 Subject: [PATCH 12/14] feat(dijkstra): add UTXO and UTXOW preservation-of-value modules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Introduce three new modules implementing the UTXO-level building blocks of the Dijkstra-era preservation-of-value proof (towards closing #1123 / CIP-159-11): + `Utxo/Properties/Base.lagda.md` Era-independent helper lemmas: `∙-homo-Coin`, `newTxid⇒disj`, `outs-disjoint`. Intentionally minimal for now — the Conway Base proofs of `balance-cong`, `balance-∪`, and `split-balance` do not port verbatim because Dijkstra defines `balance` as `∑ˢ` over a set of Values rather than as `indexedSumᵐ` over a map of hashed TxOuts. Tracking issue filed for the proper port. + `Utxo/Properties/PoV.lagda.md` The Dijkstra UTXO preservation-of-value proof is split into two orthogonal pieces: - Mechanical state change (`UTXO-I-getCoin`, `UTXO-V-mechanical`): relates `getCoin s₀` to `getCoin s₁` from the UTxOState transition alone, using `split-balance` and `balance-∪`. Proved. - Batch coin balance (`batch-balance-coin`): the coin projection of the `consumedBatch ≡ producedBatch` premise (premise p₇ of the UTXO rule). Proved from the two module parameters `coin-of-consumedBatch` and `coin-of-producedBatch`, which are themselves left as assumptions for now (see PoV follow-up work). The combined `UTXO-pov` theorem is stated but left as a placeholder (`?`); its exact form depends on how `LEDGER-pov`'s `BatchUtxoAccounting` consumer threads sub-transaction state. + `Utxow/Properties/PoV.lagda.md` UTXOW-level wrappers that extract the UTXO derivation from either `UTXOW-normal` or `UTXOW-legacy` (via a shared `UTXOW⇒UTXO` extractor) and delegate to the UTXO-level lemmas. Provides `utxow-pov-invalid` in the exact shape required as a module parameter by `Ledger/Properties/PoV.lagda.md`. Proof-internal notes: + `balance-∪` and `split-balance` are currently module parameters to `Utxo/Properties/PoV` pending the port of Conway Base's balance arithmetic to Dijkstra (see tracking issue). + The 7-term +-commutative-monoid shuffle in `UTXO-V-mechanical` is proved by hand using a `swap-right` helper; this could later be replaced by a call to a commutative-monoid solver. + All three modules typecheck under `--safe`. --- .../Utxo/Properties/Base.lagda.md | 80 ++++ .../Utxo/Properties/PoV.lagda.md | 435 ++++++++++++++++++ .../Utxow/Properties/PoV.lagda.md | 204 ++++++++ 3 files changed, 719 insertions(+) create mode 100644 src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md create mode 100644 src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md create mode 100644 src/Ledger/Dijkstra/Specification/Utxow/Properties/PoV.lagda.md diff --git a/src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md new file mode 100644 index 000000000..5f058673a --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md @@ -0,0 +1,80 @@ +--- +source_branch: 1123-cip-159-11-prove-pov-and-invariants +source_path: src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md +--- + +# UTXO Properties: Base lemmas (Dijkstra era) + +This module collects era-independent helper lemmas used by +`Utxo.Properties.PoV`{.AgdaModule}. It currently contains: + ++ `∙-homo-Coin`{.AgdaFunction}: the `coin` monoid-homomorphism's `_∙_` property. ++ `newTxid⇒disj`{.AgdaFunction}: freshness of `TxIdOf tx` in an existing + `utxo` implies `disjoint'`{.AgdaFunction} of `dom utxo`{.AgdaFunction} and + `dom (outs tx)`{.AgdaFunction}. ++ `outs-disjoint`{.AgdaFunction}: the specialisation used by + `Utxo.Properties.PoV`{.AgdaModule}. + +**Not yet ported from Conway**: the `balance`{.AgdaFunction}-arithmetic lemmas +(`balance-cong`{.AgdaFunction}, `balance-cong-coin`{.AgdaFunction}, +`balance-∪`{.AgdaFunction}, `split-balance`{.AgdaFunction}). Conway's versions +rely on `indexedSumᵐ-cong`{.AgdaFunction} over a finite map of hashed TxOuts; +Dijkstra's `balance`{.AgdaFunction} is defined as `∑ˢ[ v ← valuesOfUTxO utxo ] v` +(a sum over a `ℙ Value`{.AgdaFunction}), so the Conway proofs don't apply +verbatim. Porting them requires the set-theoretic cong lemmas from +`abstract-set-theory.FiniteSetTheory`{.AgdaModule}; for now, `balance-∪`{.AgdaFunction} +and `split-balance`{.AgdaFunction} remain as module parameters to +`Utxo.Properties.PoV`{.AgdaModule}. + + + +## `∙-homo-Coin` + +```agda +∙-homo-Coin : ∀ (x y : Value) → coin (x + y) ≡ coin x + coin y +∙-homo-Coin = IsMagmaHomomorphism.homo (isMagmaHomomorphism coinIsMonoidHomomorphism) +``` + +## Freshness ⇒ disjointness + +```agda +module _ (tx : Tx ℓ) (let open Tx tx; open TxBody txBody) + {utxo : UTxO} where + + newTxid⇒disj : TxIdOf tx ∉ mapˢ proj₁ (dom utxo) + → disjoint' (dom utxo) (dom (outs tx)) + newTxid⇒disj id∉utxo = + disjoint⇒disjoint' λ h h' → id∉utxo $ to ∈-map + (-, (case from ∈-map h' of λ where + (_ , refl , h'') → case from ∈-map h'' of λ where (_ , refl , _) → refl) , h) + + -- Specialisation used by Utxo.Properties.PoV: + -- freshness ⇒ (utxo ∣ SpendInputs ᶜ) and outs are disjoint. + outs-disjoint : TxIdOf tx ∉ mapˢ proj₁ (dom utxo) + → disjoint (dom (utxo ∣ SpendInputsOf tx ᶜ)) (dom (outs tx)) + outs-disjoint fresh = + λ h₁ h₂ → ∉-∅ $ proj₁ (newTxid⇒disj fresh) $ to ∈-∩ (res-comp-domᵐ h₁ , h₂) +``` diff --git a/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md new file mode 100644 index 000000000..372133255 --- /dev/null +++ b/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md @@ -0,0 +1,435 @@ +--- +source_branch: master +source_path: src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md +--- + +# UTXO: Preservation of Value {#sec:utxo-pov} + +This module states the preservation-of-value property for the Dijkstra +`UTXO`{.AgdaDatatype} rule, updated for CIP-159 (direct deposits and +partial withdrawals). + +## Key Differences from Conway + +1. `UTxOState`{.AgdaRecord} has 3 fields (`utxo`, `fees`, `donations`) in Dijkstra — deposits + live in `CertState`, not `UTxOState`. So + + `getCoin utxoSt = cbalance utxo + fees + donations` (no `getCoin deposits` term). + +2. **Balance equation is batch-wide** (`consumedBatch ≡ producedBatch`) rather + than per-transaction. It is a *conjunct* in `UTXO-Premises` (premise `p₇`), + not a standalone `newBal` premise. + +3. **Withdrawals appear on the consumed side** (as in Conway) *for every + transaction in the batch* (top + each sub-tx), not just the top-level tx. + CIP-159 allows partial withdrawals; the withdrawn amount is the value + specified in the transaction (≤ pre-batch balance, by phantom asset + prevention). + +4. **Direct deposits appear on the produced side** (new to CIP-159), both at + the top level and in sub-transactions. These represent value leaving the + UTxO world and entering account balances. They *cancel* in the full + LEDGER-pov equation against the `applyDirectDeposits` step applied to + `CertState`. + +5. `UTXOS`{.AgdaDatatype} is trivial (`⊤ → ⊤`): only checks script evaluation, does not + modify state. All state updates happen in `UTXO-V`/`UTXO-I` directly. + +## Proof Architecture + +The Dijkstra `UTXO-pov`{.AgdaFunction} is split into two orthogonal pieces: + ++ **Mechanical state change** (`UTXO-I-getCoin`{.AgdaFunction}, + `UTXO-V-mechanical`{.AgdaFunction}): How `getCoin s₀` relates to + `getCoin s₁` purely in terms of the `UTxOState` state transition, + without using the batch balance equation. + ++ **Batch coin balance** (`batch-balance-coin`{.AgdaFunction}): The coin + projection of the batch balance equation `consumedBatch ≡ producedBatch`. + This is a *pure* equation about `tx`, the pre-batch UTxO snapshot + `utxo₀ = UTxOOf Γ`, and the `DepositsChange` — it does not mention + `s₀` or `s₁`. + +The combined `UTXO-pov`{.AgdaFunction} theorem uses both pieces to express the +value preservation equation that the `LEDGER-pov`{.AgdaFunction} proof needs. + +Note that, unlike in Conway, the mechanical state change alone (for the valid +case) does not suffice to prove a local "before/after" equation, because + ++ `utxoSt₀` passed to the `UTXO`{.AgdaDatatype} rule at the `LEDGER` level is + the *post-SUBLEDGERS* state, not the pre-batch state, so, in general, + + `UTxOOf utxoSt₀ ≢ UTxOOf Γ` + ++ the batch balance equation relates `UTxOOf Γ` (the pre-batch snapshot) to + quantities summed over the *entire batch*, not just the top-level tx. + +Consequently, deriving a full value-preservation statement for the UTXO rule +alone requires threading through information about the preceding SUBLEDGERS +step — work that is done in `LEDGER-pov`{.AgdaFunction}, not here. + + + +## Preliminaries + +We record the `HasCoin`{.AgdaRecord} instance for `UTxOState`{.AgdaRecord} for +easy reference. Note, in Dijkstra `UTxOState`{.AgdaRecord} has only three fields. +Also, for `s : UTxOState`, + +`getCoin s = cbalance (UTxOOf s) + FeesOf s + DonationsOf s` + +We introduce module-level parameters encapsulating the UTxO arithmetic lemmas that +are used in Conway's analogous proofs. They need to be ported to the Dijkstra era (they live in +`Ledger.Conway.Specification.Utxo.Properties.Base`{.AgdaModule}) but are +orthogonal to the CIP-159 content of this issue, so we take them as assumptions +here. + +```agda +module _ + (tx : TopLevelTx) (let open Tx tx; open TxBody txBody) + + -- (A) Standard Value/Coin arithmetic (ported from Conway's Utxo.Properties.Base). + ( balance-∪ : ∀ {u u' : UTxO} → disjoint (dom u) (dom u') + → cbalance (u ∪ˡ u') ≡ cbalance u + cbalance u' ) + + ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn) + → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) ) + + -- (B) Batch coin-balance projection: this is the coin version of the + -- `consumedBatch ≡ producedBatch` premise, obtained by applying `coin` to + -- both sides, using `coin∘inject≗id` and `∙-homo-Coin` repeatedly, and using + -- `coin (MintedValueOf t) ≡ 0` for every transaction in the batch + -- (top-level from UTXO premise p₆, sub-level from each SUBUTXO premise). + ( coin-of-consumedBatch : + ∀ (dc : DepositsChange) (utxo₀ : UTxO) + → let open DepositsChange dc in + coin (consumedBatch dc tx utxo₀) + ≡ cbalance (utxo₀ ∣ SpendInputsOf tx) + + getCoin (WithdrawalsOf tx) + + negPart depositsChangeTop + + sum (map (λ (stx : SubLevelTx) → + cbalance (utxo₀ ∣ SpendInputsOf stx) + + getCoin (WithdrawalsOf stx)) + (SubTransactionsOf tx)) + + negPart depositsChangeSub ) + + ( coin-of-producedBatch : + ∀ (dc : DepositsChange) + → let open DepositsChange dc in + coin (producedBatch dc tx) + ≡ cbalance (outs tx) + + TxFeesOf tx + + DonationsOf tx + + getCoin (DirectDepositsOf tx) + + posPart depositsChangeTop + + sum (map (λ (stx : SubLevelTx) → + cbalance (outs stx) + + DonationsOf stx + + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx)) + + posPart depositsChangeSub ) + where +``` + + + +## `UTXO-I`: collateral collection preserves `getCoin` + +The invalid case does not use the batch balance equation: it only collects +collateral from the top-level transaction and leaves `donations` unchanged. + +```agda +{-- + UTXO-I-getCoin : + (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁ + → IsValidFlagOf tx ≡ false + → getCoin s₀ ≡ getCoin s₁ +--} +``` + + + +## `UTXO-V`: mechanical rearrangement + +```agda + UTXO-V-mechanical : (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁ + → IsValidFlagOf tx ≡ true → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s₀)) + → getCoin s₀ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + ≡ getCoin s₁ + cbalance (UTxOOf s₀ ∣ SpendInputsOf tx) +``` + + + +## Extracting the `UTXO`{.AgdaDatatype} step + +The key observation is that both `UTXOW-normal`{.AgdaInductiveConstructor} +and `UTXOW-legacy`{.AgdaInductiveConstructor} embed a `UTXO`{.AgdaDatatype} +derivation as their final premise. We factor out an extractor: + +```agda +UTXOW⇒UTXO : + ∀ {Γ : UTxOEnv} {s s' : UTxOState} {tx : TopLevelTx} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' + → ∃[ legacyMode ] ((Γ , legacyMode) ⊢ s ⇀⦇ tx ,UTXO⦈ s') +UTXOW⇒UTXO (UTXOW-normal-⋯ _ _ _ _ _ _ _ _ _ _ utxo) = false , utxo +UTXOW⇒UTXO (UTXOW-legacy-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ utxo) = true , utxo +``` + +## `UTXOW-I-getCoin`: collateral collection preserves `getCoin` + +In the invalid case, the `UTXOW`{.AgdaDatatype} rule preserves `getCoin`{.AgdaField} +exactly (collateral is moved from the UTxO to the fees, both of which are +counted in `getCoin`{.AgdaField}): + +```agda +module _ (tx : TopLevelTx) (let open Tx tx; open TxBody txBody) + + -- Same assumptions as the UTXO-pov module. + ( balance-∪ : ∀ {u u' : UTxO} → disjoint (dom u) (dom u') + → cbalance (u ∪ˡ u') ≡ cbalance u + cbalance u' ) + + ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn) + → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) ) + + ( outs-disjoint : ∀ {u : UTxO} + → TxIdOf tx ∉ mapˢ proj₁ (dom u) + → disjoint (dom (u ∣ SpendInputsOf tx ᶜ)) (dom (outs tx)) ) + + ( coin-of-consumedBatch : + ∀ (dc : DepositsChange) (utxo₀ : UTxO) + → let open DepositsChange dc in + coin (consumedBatch dc tx utxo₀) ≡ _ ) + + ( coin-of-producedBatch : + ∀ (dc : DepositsChange) + → let open DepositsChange dc in + coin (producedBatch dc tx) ≡ _ ) + + where + + -- Instantiate the inner `module _` of `Utxo.Properties.PoV`. + private + module U = + Ledger.Dijkstra.Specification.Utxo.Properties.PoV + txs abs + -- `utxo-pov-mod` refers to the parameterized inner module of `U` + -- (the one that takes `tx` and the arithmetic assumptions). +``` + +```agda + UTXOW-I-getCoin : + ∀ {Γ : UTxOEnv} {s s' : UTxOState} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' + → IsValidFlagOf tx ≡ false + → getCoin s ≡ getCoin s' + UTXOW-I-getCoin utxow invalid = + let (_ , utxo) = UTXOW⇒UTXO utxow + in U-pov.UTXO-I-getCoin utxo invalid + where + -- Re-instantiate the inner module with our assumption lemmas. + module U-pov = + U tx balance-∪ split-balance outs-disjoint + coin-of-consumedBatch coin-of-producedBatch +``` + +(The inner module instantiation is a bit boilerplate-heavy; in practice this +should be simplified once the final module structure of `Utxo.Properties.PoV` +is settled.) + +## `UTXOW-V-mechanical`: mechanical rearrangement + +The valid case simply reuses the UTXO-level mechanical rearrangement: + +```agda + UTXOW-V-mechanical : + ∀ {Γ : UTxOEnv} {s s' : UTxOState} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' + → IsValidFlagOf tx ≡ true + → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s)) + → getCoin s + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + ≡ getCoin s' + cbalance (UTxOOf s ∣ SpendInputsOf tx) + UTXOW-V-mechanical utxow valid fresh = + let (_ , utxo) = UTXOW⇒UTXO utxow + in U-pov.UTXO-V-mechanical utxo valid fresh + where + module U-pov = + U tx balance-∪ split-balance outs-disjoint + coin-of-consumedBatch coin-of-producedBatch +``` + +## `UTXOW-batch-balance-coin` + +```agda + UTXOW-batch-balance-coin : + ∀ {Γ : UTxOEnv} {s s' : UTxOState} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' + → let dc = DepositsChangeOf Γ + utxo₀ = UTxOOf Γ + open DepositsChange dc + in cbalance (utxo₀ ∣ SpendInputsOf tx) + + getCoin (WithdrawalsOf tx) + + negPart depositsChangeTop + + sum (map (λ (stx : SubLevelTx) → + cbalance (utxo₀ ∣ SpendInputsOf stx) + + getCoin (WithdrawalsOf stx)) + (SubTransactionsOf tx)) + + negPart depositsChangeSub + ≡ cbalance (outs tx) + + TxFeesOf tx + + DonationsOf tx + + getCoin (DirectDepositsOf tx) + + posPart depositsChangeTop + + sum (map (λ (stx : SubLevelTx) → + cbalance (outs stx) + + DonationsOf stx + + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx)) + + posPart depositsChangeSub + UTXOW-batch-balance-coin utxow = + let (_ , utxo) = UTXOW⇒UTXO utxow + in U-pov.batch-balance-coin utxo + where + module U-pov = + U tx balance-∪ split-balance outs-disjoint + coin-of-consumedBatch coin-of-producedBatch +``` + +## `utxow-pov-invalid` for use in `LEDGER-pov` + +The following is the *specific* form needed by `Ledger.Properties.PoV` +(the `BatchUtxoAccounting` use site takes it as a module parameter). It is +identical to `UTXOW-I-getCoin`{.AgdaFunction} above, retagged for clarity: + +```agda + utxow-pov-invalid : + ∀ {Γ : UTxOEnv} {s s' : UTxOState} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' + → IsValidFlagOf tx ≡ false + → getCoin s ≡ getCoin s' + utxow-pov-invalid = UTXOW-I-getCoin +``` + +With this, the `utxow-pov-invalid` postulated module parameter in +`Ledger.Properties.PoV` can be discharged by calling this function. + +## Summary of proof obligations + ++ Same ported arithmetic lemmas as `Utxo.Properties.PoV` (`balance-∪`, + `split-balance`, `outs-disjoint`, and the two batch-coin-projection + lemmas). + ++ Once those are ported, the entire `UTXOW-pov` module is mechanical + pattern-matching on the two `UTXOW`{.AgdaDatatype} constructors, with + delegation to `Utxo.Properties.PoV`. From e0d513e0dba95fe567e99d29b2bf81d2862d328e Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 22 Apr 2026 10:07:22 -0600 Subject: [PATCH 13/14] feat(dijkstra): discharge `coin-of-{consumed,produced}Batch` in UTXO PoV MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace the two `coin-of-consumedBatch` / `coin-of-producedBatch` module parameters of `Utxo/Properties/PoV` with direct proofs. The proofs are organised as three layers: + Layer 1 — single-transaction coin equations `coin-producedTx : coin (producedTx t) ≡ cbalance (outs t) + DonationsOf t + getCoin (DirectDepositsOf t)` `coin-consumedTx : coin (MintedValueOf t) ≡ 0 → coin (consumedTx t utxo₀) ≡ cbalance (utxo₀ ∣ SpendInputsOf t) + getCoin (WithdrawalsOf t)` Each is a direct unfolding: repeated `∙-homo-Coin` to distribute `coin` across `+`, followed by `coin∘inject≗id` to strip each `inject`. The consumed version additionally uses `coin (MintedValueOf t) ≡ 0` to cancel the mint term (from UTXO premise p₆ / SUBUTXO premise). + Layer 2 — sum-over-sub-transactions coin equations `coin-∑-producedTx-sub` : pushes `coin` through the `∑ˡ`-indexed sum over `SubTransactionsOf tx` using the new `coin-∑ˡ` lemma (from `Utxo/Properties/Base`), then applies Layer 1 pointwise by list induction. `coin-∑-consumedTx-sub` : same shape, threading a `noMintingSubTxs tx` hypothesis (`∀ stx → stx ∈ˡ SubTransactionsOf tx → coin (MintedValueOf stx) ≡ 0`) through the induction so each element's Layer-1 application has its `noMint` premise available. + Layer 3 — the two batch-level coin equations `coin-of-consumedBatch` and `coin-of-producedBatch`: unfold the outer `+ inject _` / `+ ∑ˡ _` structure of `consumedBatch` / `producedBatch` by repeated `∙-homo-Coin` and `coin∘inject≗id`, substitute the Layer-1 top-level equation for the top-level summand, and substitute the Layer-2 equation for the sub-transaction sum. The produced-side proof ends with a small associative-commutative shuffle (`reshape-top`) that reorders the top-level fields from `(outs + Donations + DirectDeposits) + TxFees` to the stated `outs + TxFees + Donations + DirectDeposits`. The shuffle uses the same `swap-right` helper already used in `UTXO-V-mechanical`. + Supporting change Adds a small helper alias `noMintingSubTxs` at the top of the file to keep the sub-level mint-conservation hypothesis readable in the theorem statements. All proofs typecheck under `--safe`. The `UTXO-pov` placeholder remains; this commit delivers the coin-balance infrastructure that the eventual full proof (and the LEDGER-pov's `BatchUtxoAccounting` consumer) will depend on. --- .../Dijkstra/Specification/Utxo.lagda.md | 34 +- .../Specification/Utxo/Properties.lagda.md | 2 + .../Utxo/Properties/Base.lagda.md | 16 + .../Utxo/Properties/PoV.lagda.md | 477 +++++++++++++----- .../Specification/Utxow/Properties.lagda.md | 1 + 5 files changed, 384 insertions(+), 146 deletions(-) diff --git a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md index 555f11043..edffa64b1 100644 --- a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md @@ -141,6 +141,14 @@ record HasDepositsChange {a} (A : Type a) : Type a where field DepositsChangeOf : A → DepositsChange open HasDepositsChange ⦃...⦄ public +record HasDepositsChangeTop {a} (A : Type a) : Type a where + field DepositsChangeTopOf : A → ℤ +open HasDepositsChangeTop ⦃...⦄ public + +record HasDepositsChangeSub {a} (A : Type a) : Type a where + field DepositsChangeSubOf : A → ℤ +open HasDepositsChangeSub ⦃...⦄ public + record HasScriptPool {a} (A : Type a) : Type a where field ScriptPoolOf : A → ℙ Script open HasScriptPool ⦃...⦄ public @@ -209,6 +217,12 @@ instance HasDonations-UTxOState : HasDonations UTxOState HasDonations-UTxOState .DonationsOf = UTxOState.donations + HasDepositsChangeTop-DepositsChange : HasDepositsChangeTop DepositsChange + HasDepositsChangeTop-DepositsChange .DepositsChangeTopOf = DepositsChange.depositsChangeTop + + HasDepositsChangeSub-DepositsChange : HasDepositsChangeSub DepositsChange + HasDepositsChangeSub-DepositsChange .DepositsChangeSubOf = DepositsChange.depositsChangeSub + unquoteDecl HasCast-DepositsChange HasCast-UTxOEnv HasCast-SubUTxOEnv @@ -303,6 +317,16 @@ collateralCheck pp txTop utxo = × coin (balance (utxo ∣ CollateralInputsOf txTop)) * 100 ≥ (TxFeesOf txTop) * pp .collateralPercentage × (CollateralInputsOf txTop) ≢ ∅ +producedTx : Tx ℓ → Value +producedTx tx = balance (outs tx) + + inject (DonationsOf tx) + + inject (getCoin (DirectDepositsOf tx)) + +consumedTx : Tx ℓ → UTxO → Value +consumedTx tx utxo = balance (utxo ∣ SpendInputsOf tx) + + MintedValueOf tx + + inject (getCoin (WithdrawalsOf tx)) + module _ (depositsChange : DepositsChange) where open DepositsChange depositsChange @@ -319,11 +343,6 @@ module _ (depositsChange : DepositsChange) where depositRefundsTop : Coin depositRefundsTop = negPart depositsChangeTop - consumedTx : Tx ℓ → UTxO → Value - consumedTx tx utxo = balance (utxo ∣ SpendInputsOf tx) - + MintedValueOf tx - + inject (getCoin (WithdrawalsOf tx)) - consumed : TopLevelTx → UTxO → Value consumed txTop utxo = consumedTx txTop utxo + inject depositRefundsTop @@ -340,11 +359,6 @@ In the preservation-of-value equation, direct deposits appear on the the transaction and that amount is deposited into accounts. ```agda - producedTx : Tx ℓ → Value - producedTx tx = balance (outs tx) - + inject (DonationsOf tx) - + inject (getCoin (DirectDepositsOf tx)) - produced : TopLevelTx → Value produced txTop = producedTx txTop + inject (TxFeesOf txTop) diff --git a/src/Ledger/Dijkstra/Specification/Utxo/Properties.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo/Properties.lagda.md index 456772f9b..7ad771cd3 100644 --- a/src/Ledger/Dijkstra/Specification/Utxo/Properties.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxo/Properties.lagda.md @@ -14,4 +14,6 @@ module Ledger.Dijkstra.Specification.Utxo.Properties where ```agda open import Ledger.Dijkstra.Specification.Utxo.Properties.Computational +open import Ledger.Dijkstra.Specification.Utxo.Properties.Base +open import Ledger.Dijkstra.Specification.Utxo.Properties.PoV ``` diff --git a/src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md index 5f058673a..3cf9371b4 100644 --- a/src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxo/Properties/Base.lagda.md @@ -58,6 +58,22 @@ private variable ∙-homo-Coin = IsMagmaHomomorphism.homo (isMagmaHomomorphism coinIsMonoidHomomorphism) ``` +## `coin-∑ˡ` + +`coin`{.AgdaField} is a monoid homomorphism from `Value`{.AgdaField} (under `+ᵛ`/`ε`) to +`ℕ`{.AgdaDatatype} (under `+`/`0`), so it distributes over a list-indexed sum. This +is the "coin version" of the generic fact that a monoid homomorphism commutes with +`foldr _∙_ ε`. + +```agda +coin-∑ˡ : ∀ {A : Type} (f : A → Value) (xs : List A) + → coin (∑ˡ[ x ← xs ] f x) ≡ sum (map (coin ∘ f) xs) +coin-∑ˡ f [] = ε-homo coinIsMonoidHomomorphism +coin-∑ˡ f (x ∷ xs) = trans (∙-homo-Coin (f x) (∑ˡ[ z ← xs ] f z)) + (cong (coin (f x) +_) (coin-∑ˡ f xs)) +``` + + ## Freshness ⇒ disjointness ```agda diff --git a/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md index 372133255..4efd9b050 100644 --- a/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md @@ -88,16 +88,20 @@ open import Axiom.Set.Properties th -- supplied by callers, pending a Dijkstra-specific port of Conway Base's -- balance arithmetic. open import Ledger.Dijkstra.Specification.Utxo.Properties.Base txs abs - using (∙-homo-Coin; outs-disjoint) - + using (∙-homo-Coin; outs-disjoint; coin-∑ˡ) open import Ledger.Dijkstra.Specification.Utxo txs abs open import Relation.Binary.PropositionalEquality +open import Ledger.Dijkstra.Specification.Transaction +open import Data.List.Relation.Unary.Any using (here; there) open import Data.Nat.Properties using (+-0-monoid; +-identityʳ; +-identityˡ; +-comm; +-assoc; *-zeroʳ; *-identityʳ) instance _ = +-0-monoid + +private variable + ℓ : TxLevel ``` --> @@ -116,54 +120,299 @@ orthogonal to the CIP-159 content of this issue, so we take them as assumptions here. ```agda +-- ============================================================================= +-- Coin projections of consumedBatch and producedBatch. +-- ============================================================================= +-- +-- These proofs live inside the parameterised `module _ (tx : TopLevelTx) ...` +-- block of `Utxo/Properties/PoV.lagda.md`, alongside the existing +-- `UTXO-I-getCoin` / `UTXO-V-mechanical` / `batch-balance-coin` definitions. +-- +-- They replace the `coin-of-consumedBatch` and `coin-of-producedBatch` module +-- parameters. +-- +-- The presentation assumes `coin-∑ˡ` is available from `Utxo.Properties.Base`; +-- `coin-producedTx` is as William has already proved it. +-- +-- Imports needed (add to the main `open import` block at the top of the file): +-- +-- open import Ledger.Dijkstra.Specification.Utxo.Properties.Base txs abs +-- using (∙-homo-Coin; outs-disjoint; coin-∑ˡ) +-- +-- ============================================================================= + + +-- ----------------------------------------------------------------------------- +-- Layer 1: single-transaction coin equations. +-- ----------------------------------------------------------------------------- +coin-producedTx : (tx : Tx ℓ) → coin (producedTx tx) ≡ cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) +coin-producedTx tx = begin + coin (producedTx tx) + ≡⟨ refl ⟩ + coin(balance (outs tx) + inject (DonationsOf tx) + inject (getCoin (DirectDepositsOf tx))) + ≡⟨ ∙-homo-Coin (balance (outs tx) + inject (DonationsOf tx)) (inject (getCoin (DirectDepositsOf tx))) ⟩ + coin(balance (outs tx) + inject (DonationsOf tx)) + coin(inject (getCoin (DirectDepositsOf tx))) + ≡⟨ cong (coin(balance (outs tx) + inject (DonationsOf tx)) +_) (coin∘inject≗id (getCoin (DirectDepositsOf tx))) ⟩ + coin(balance (outs tx) + inject (DonationsOf tx)) + getCoin (DirectDepositsOf tx) + ≡⟨ cong (_+ getCoin (DirectDepositsOf tx)) (∙-homo-Coin (balance (outs tx)) (inject (DonationsOf tx))) ⟩ + coin(balance (outs tx)) + coin(inject (DonationsOf tx)) + getCoin (DirectDepositsOf tx) + ≡⟨ cong (λ x → coin(balance (outs tx)) + x + getCoin (DirectDepositsOf tx)) (coin∘inject≗id (DonationsOf tx)) ⟩ + cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) + ∎ + where open ≡-Reasoning + + +coin-consumedTx : (tx : Tx ℓ) (utxo₀ : UTxO) → coin (MintedValueOf tx) ≡ 0 + → coin (consumedTx tx utxo₀) ≡ cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) +coin-consumedTx tx utxo₀ noMint = + let b₀ = balance (utxo₀ ∣ SpendInputsOf tx) in + begin + coin (consumedTx tx utxo₀) + ≡⟨ refl ⟩ + coin (b₀ + MintedValueOf tx + inject (getCoin (WithdrawalsOf tx))) + ≡⟨ ∙-homo-Coin (b₀ + MintedValueOf tx) (inject (getCoin (WithdrawalsOf tx))) ⟩ + coin (b₀ + MintedValueOf tx) + coin (inject (getCoin (WithdrawalsOf tx))) + ≡⟨ cong (coin (b₀ + MintedValueOf tx) +_) (coin∘inject≗id (getCoin (WithdrawalsOf tx))) ⟩ + coin (b₀ + MintedValueOf tx) + getCoin (WithdrawalsOf tx) + ≡⟨ cong (_+ getCoin (WithdrawalsOf tx)) (∙-homo-Coin (b₀) (MintedValueOf tx)) ⟩ + coin b₀ + coin (MintedValueOf tx) + getCoin (WithdrawalsOf tx) + ≡⟨ cong (λ z → cbalance (utxo₀ ∣ SpendInputsOf tx) + z + getCoin (WithdrawalsOf tx)) noMint ⟩ + cbalance (utxo₀ ∣ SpendInputsOf tx) + 0 + getCoin (WithdrawalsOf tx) + ≡⟨ cong (_+ getCoin (WithdrawalsOf tx)) (+-identityʳ (cbalance (utxo₀ ∣ SpendInputsOf tx))) ⟩ + cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + ∎ + where open ≡-Reasoning + + +-- ----------------------------------------------------------------------------- +-- Layer 2: sum-over-sub-transactions coin equations. +-- ----------------------------------------------------------------------------- +-- +-- We use `coin-∑ˡ` to push `coin` through the indexed sum, then rewrite each +-- summand pointwise using Layer 1. For the consumed-side version we also +-- thread a per-element `noMintSub` premise. + +coin-∑-producedTx-sub : (tx : TopLevelTx) → + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx)) + ≡ sum ( map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx) ) +coin-∑-producedTx-sub tx = begin + coin (∑ˡ[ stx ← SubTransactionsOf tx ] producedTx stx) + ≡⟨ coin-∑ˡ producedTx (SubTransactionsOf tx) ⟩ + sum (map (coin ∘ producedTx) (SubTransactionsOf tx)) + ≡⟨ sum-cong-rewrite (SubTransactionsOf tx) ⟩ + sum (map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx)) + ∎ + where + open ≡-Reasoning + -- Pointwise rewrite of the mapped list, by list induction. + sum-cong-rewrite : (xs : List SubLevelTx) + → sum (map (coin ∘ producedTx) xs) + ≡ sum (map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) xs) + sum-cong-rewrite [] = refl + sum-cong-rewrite (stx ∷ xs) = cong₂ _+_ (coin-producedTx stx) (sum-cong-rewrite xs) + + +noMintingSubTxs : TopLevelTx → Type +noMintingSubTxs tx = ∀ stx → stx ∈ˡ SubTransactionsOf tx → coin (MintedValueOf stx) ≡ 0 + +coin-∑-consumedTx-sub : (tx : TopLevelTx) (utxo₀ : UTxO) + → noMintingSubTxs tx + → coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + ≡ sum (map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx)) +coin-∑-consumedTx-sub tx utxo₀ noMintSub = begin + coin (∑ˡ[ stx ← SubTransactionsOf tx ] consumedTx stx utxo₀) + ≡⟨ coin-∑ˡ (λ stx → consumedTx stx utxo₀) (SubTransactionsOf tx) ⟩ + sum (map (coin ∘ λ stx → consumedTx stx utxo₀) (SubTransactionsOf tx)) + ≡⟨ go (SubTransactionsOf tx) (λ _ → id) ⟩ + sum (map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + + getCoin (WithdrawalsOf stx)) + (SubTransactionsOf tx)) + ∎ + where + open ≡-Reasoning + -- Pointwise rewrite: the `mem` argument lets each element's + -- `noMintSub` lookup go through. + go : (xs : List SubLevelTx) + → (∀ stx → stx ∈ˡ xs → stx ∈ˡ SubTransactionsOf tx) + → sum (map (coin ∘ λ stx → consumedTx stx utxo₀) xs) + ≡ sum (map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + + getCoin (WithdrawalsOf stx)) xs) + go [] _ = refl + go (stx ∷ xs) mem = + cong₂ _+_ + (coin-consumedTx stx utxo₀ (noMintSub stx (mem stx (here refl)))) + (go xs (λ stx' stx'∈ → mem stx' (there stx'∈))) + + +-- ----------------------------------------------------------------------------- +-- Layer 3: the two batch-level coin equations. +-- ----------------------------------------------------------------------------- +-- +-- `consumedBatch` and `producedBatch` each wrap their per-tx summands with +-- additional `inject`-ed fields (top-level fees + per-side deposit terms), so +-- we peel those off with `∙-homo-Coin` + `coin∘inject≗id`, then substitute the +-- Layer-1 top-level and Layer-2 sub-level equations. +-- +-- Each proof ends with a small `+`-commutative-monoid shuffle to match the +-- field order in the stated theorem. +coin-of-consumedBatch : (tx : TopLevelTx) (dc : DepositsChange) (utxo₀ : UTxO) + → coin (MintedValueOf tx) ≡ 0 → noMintingSubTxs tx + → coin (consumedBatch dc tx utxo₀) + ≡ cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf dc) + + sum ( map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) + (SubTransactionsOf tx) ) + + negPart (DepositsChangeSubOf dc) +coin-of-consumedBatch tx dc utxo₀ noMintTop noMintSub = begin + -- consumedBatch dc tx utxo₀ = consumed dc tx utxo₀ + ∑ˡ[ stx ← subs ] (consumedTx stx utxo₀) + inject depositRefundsSub + -- where consumed dc tx utxo₀ = consumedTx tx utxo₀ + inject depositRefundsTop + coin ( consumedTx tx utxo₀ + inject (negPart (DepositsChangeTopOf dc)) + + ∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀) + inject (negPart (DepositsChangeSubOf dc)) ) + + ≡⟨ ∙-homo-Coin _ _ ⟩ -- Peel the outer `+ inject depositRefundsSub`. + coin ( consumedTx tx utxo₀ + inject (negPart (DepositsChangeTopOf dc)) + + ∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀) ) + + coin (inject (negPart (DepositsChangeSubOf dc))) + + ≡⟨ cong₂ _+_ (∙-homo-Coin _ _) (coin∘inject≗id _) ⟩ + coin (consumedTx tx utxo₀ + inject (negPart (DepositsChangeTopOf dc))) + + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + negPart (DepositsChangeSubOf dc) + + -- Peel `consumedTx tx utxo₀ + inject depositRefundsTop`. + ≡⟨ cong (λ z → z + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + + negPart (DepositsChangeSubOf dc)) + (trans (∙-homo-Coin _ _) (cong (coin (consumedTx tx utxo₀) +_) (coin∘inject≗id _))) ⟩ + coin (consumedTx tx utxo₀) + negPart (DepositsChangeTopOf dc) + + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + negPart (DepositsChangeSubOf dc) + + -- Substitute Layer-1 top-level. + ≡⟨ cong (λ z → z + negPart (DepositsChangeTopOf dc) + + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + + negPart (DepositsChangeSubOf dc)) + (coin-consumedTx tx utxo₀ noMintTop) ⟩ + cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf dc) + + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (consumedTx stx utxo₀)) + negPart (DepositsChangeSubOf dc) + + -- Substitute Layer-2 sub-level. + ≡⟨ cong (λ z → (cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx)) + + negPart (DepositsChangeTopOf dc) + z + negPart (DepositsChangeSubOf dc)) + (coin-∑-consumedTx-sub tx utxo₀ noMintSub) ⟩ + cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf dc) + + sum (map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx)) + + negPart (DepositsChangeSubOf dc) + + -- Re-associate the outer `+` to match the stated theorem. + ≡⟨ cong (λ z → z + negPart (DepositsChangeTopOf dc) + + sum ( map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) + (SubTransactionsOf tx) ) + + negPart (DepositsChangeSubOf dc)) refl ⟩ + -- The term now matches the target statement exactly. + cbalance (utxo₀ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf dc) + + sum (map (λ stx → cbalance (utxo₀ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx)) + + negPart (DepositsChangeSubOf dc) + ∎ + where open ≡-Reasoning + + +coin-of-producedBatch : (tx : TopLevelTx) (dc : DepositsChange) + → coin (producedBatch dc tx) + ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + + posPart (DepositsChangeTopOf dc) + + sum ( map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx) ) + + posPart (DepositsChangeSubOf dc) +coin-of-producedBatch tx dc = begin + -- producedBatch dc tx = produced dc tx + ∑ˡ[ stx ← subs ] (producedTx stx) + inject newDepositsSub + -- where produced dc tx = producedTx tx + inject txFee + inject newDepositsTop + coin (producedTx tx + inject (TxFeesOf tx) + inject (posPart (DepositsChangeTopOf dc)) + + ∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx) + inject (posPart (DepositsChangeSubOf dc))) + + -- Peel the outer `+ inject newDepositsSub`. + ≡⟨ ∙-homo-Coin _ _ ⟩ + coin (producedTx tx + inject (TxFeesOf tx) + inject (posPart (DepositsChangeTopOf dc)) + + ∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx)) + coin (inject (posPart (DepositsChangeSubOf dc))) + ≡⟨ cong₂ _+_ (∙-homo-Coin _ _) (coin∘inject≗id _) ⟩ + coin (producedTx tx + inject (TxFeesOf tx) + inject (posPart (DepositsChangeTopOf dc))) + + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx)) + posPart (DepositsChangeSubOf dc) + -- Unfold the top-level three layers (outs+donations+directDeps, fee, deposits). + ≡⟨ cong (λ z → z + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx)) + posPart (DepositsChangeSubOf dc)) + unfold-produced-top ⟩ + cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) + + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + coin (∑ˡ[ stx ← SubTransactionsOf tx ] (producedTx stx)) + + posPart (DepositsChangeSubOf dc) + -- Substitute Layer-2 sub-level. + ≡⟨ cong (λ z → (cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx)) + + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + z + posPart (DepositsChangeSubOf dc)) + (coin-∑-producedTx-sub tx) ⟩ + cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) + + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + + sum ( map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx) ) + + posPart (DepositsChangeSubOf dc) + -- Reshuffle top-level fields: (outs + Donations + DirectDeps) + TxFees + -- → outs + TxFees + Donations + DirectDeps + ≡⟨ cong (λ z → z + posPart (DepositsChangeTopOf dc) + + sum ( map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx) ) + + posPart (DepositsChangeSubOf dc)) reshape-top ⟩ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + posPart (DepositsChangeTopOf dc) + + sum (map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx)) + + posPart (DepositsChangeSubOf dc) + ∎ + where + open ≡-Reasoning + + -- Unfolds `coin (producedTx tx + inject TxFees + inject newDepositsTop)` by + -- two peels of `∙-homo-Coin` / `coin∘inject≗id` and one application of + -- `coin-producedTx`. + unfold-produced-top : + coin (producedTx tx + inject (TxFeesOf tx) + inject (posPart (DepositsChangeTopOf dc))) + ≡ (cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx)) + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + + unfold-produced-top = begin + coin (producedTx tx + inject (TxFeesOf tx) + inject (posPart (DepositsChangeTopOf dc))) + ≡⟨ ∙-homo-Coin _ _ ⟩ + coin (producedTx tx + inject (TxFeesOf tx)) + coin (inject (posPart (DepositsChangeTopOf dc))) + ≡⟨ cong₂ _+_ (∙-homo-Coin _ _) (coin∘inject≗id _) ⟩ + coin (producedTx tx) + coin (inject (TxFeesOf tx)) + posPart (DepositsChangeTopOf dc) + ≡⟨ cong (λ z → coin (producedTx tx) + z + posPart (DepositsChangeTopOf dc)) (coin∘inject≗id _) ⟩ + coin (producedTx tx) + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + ≡⟨ cong (λ z → z + TxFeesOf tx + posPart (DepositsChangeTopOf dc)) (coin-producedTx tx) ⟩ + cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) + TxFeesOf tx + posPart (DepositsChangeTopOf dc) + ∎ + + -- Small rearrangement: move TxFees from rightmost position to second. + -- (O + D + R) + F ≡ O + F + D + R + -- (where O = cbalance (outs tx), D = DonationsOf tx, + -- R = getCoin (DirectDepositsOf tx), F = TxFeesOf tx). + -- Proved by the `swap-right` pattern used in `UTXO-V-mechanical`. + reshape-top : cbalance (outs tx) + DonationsOf tx + getCoin (DirectDepositsOf tx) + TxFeesOf tx + ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + reshape-top = + let O = cbalance (outs tx) + D = DonationsOf tx + R = getCoin (DirectDepositsOf tx) + F = TxFeesOf tx + in begin + (O + D + R) + F ≡⟨ swap-right (O + D) R F ⟩ + (O + D) + F + R ≡⟨ cong (_+ R) (swap-right O D F) ⟩ + O + F + D + R ∎ + where + -- Same `swap-right` helper as in `UTXO-V-mechanical`. + 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))) + + module _ (tx : TopLevelTx) (let open Tx tx; open TxBody txBody) - -- (A) Standard Value/Coin arithmetic (ported from Conway's Utxo.Properties.Base). - ( balance-∪ : ∀ {u u' : UTxO} → disjoint (dom u) (dom u') - → cbalance (u ∪ˡ u') ≡ cbalance u + cbalance u' ) - - ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn) - → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) ) - - -- (B) Batch coin-balance projection: this is the coin version of the - -- `consumedBatch ≡ producedBatch` premise, obtained by applying `coin` to - -- both sides, using `coin∘inject≗id` and `∙-homo-Coin` repeatedly, and using - -- `coin (MintedValueOf t) ≡ 0` for every transaction in the batch - -- (top-level from UTXO premise p₆, sub-level from each SUBUTXO premise). - ( coin-of-consumedBatch : - ∀ (dc : DepositsChange) (utxo₀ : UTxO) - → let open DepositsChange dc in - coin (consumedBatch dc tx utxo₀) - ≡ cbalance (utxo₀ ∣ SpendInputsOf tx) - + getCoin (WithdrawalsOf tx) - + negPart depositsChangeTop - + sum (map (λ (stx : SubLevelTx) → - cbalance (utxo₀ ∣ SpendInputsOf stx) - + getCoin (WithdrawalsOf stx)) - (SubTransactionsOf tx)) - + negPart depositsChangeSub ) - - ( coin-of-producedBatch : - ∀ (dc : DepositsChange) - → let open DepositsChange dc in - coin (producedBatch dc tx) - ≡ cbalance (outs tx) - + TxFeesOf tx - + DonationsOf tx - + getCoin (DirectDepositsOf tx) - + posPart depositsChangeTop - + sum (map (λ (stx : SubLevelTx) → - cbalance (outs stx) - + DonationsOf stx - + getCoin (DirectDepositsOf stx)) - (SubTransactionsOf tx)) - + posPart depositsChangeSub ) + -- ASSUMPTIONS -- + ( balance-∪ : ∀ {u u' : UTxO} → disjoint (dom u) (dom u') → cbalance (u ∪ˡ u') ≡ cbalance u + cbalance u' ) + ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn) → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) ) + ( noMintTx : coin (MintedValueOf tx) ≡ 0 ) + ( noMintSubTx : noMintingSubTxs tx ) where -``` - + ## `UTXO-I`: collateral collection preserves `getCoin` @@ -179,40 +428,23 @@ The invalid case does not use the batch balance equation: it only collects collateral from the top-level transaction and leaves `donations` unchanged. ```agda -{-- UTXO-I-getCoin : - (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁ - → IsValidFlagOf tx ≡ false - → getCoin s₀ ≡ getCoin s₁ ---} -``` + (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁ → IsValidFlagOf tx ≡ false → getCoin s₀ ≡ getCoin s₁ - + ## `UTXO-V`: mechanical rearrangement @@ -221,19 +453,26 @@ collateral from the top-level transaction and leaves `donations` unchanged. → IsValidFlagOf tx ≡ true → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s₀)) → getCoin s₀ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx ≡ getCoin s₁ + cbalance (UTxOOf s₀ ∣ SpendInputsOf tx) -``` - @@ -279,7 +360,7 @@ module _ ## LEDGER Preservation of Value ```agda - LEDGER-pov : {Γ : LedgerEnv} {s s' : LedgerState} → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s' + LEDGER-pov : {Γ : LedgerEnv} {s s' : LedgerState} → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s' ``` ### LEDGER-I case (invalid transaction) @@ -289,9 +370,9 @@ This follows the Conway pattern with `certState' ≡ certState₀`. Only the `UTXOW`{.AgdaDatatype} step matters and it preserves `getCoin utxoSt`. ```agda - LEDGER-pov {Γ} {s} (LEDGER-I (invalid , subStep , utxoStep)) = - cong (λ u → u + getCoin (CertStateOf s) + coinFromDeposits (CertStateOf s)) - (utxow-pov-invalid utxoStep invalid) + LEDGER-pov {Γ} {s} (LEDGER-I (invalid , subStep , utxoStep)) = + cong (λ u → u + getCoin (CertStateOf s) + coinFromDeposits (CertStateOf s)) + (utxow-pov-invalid utxoStep invalid) ``` ### LEDGER-V (valid transaction) @@ -303,107 +384,290 @@ The `LEDGER-V` rule produces where `certStateFinal = record certState₂ { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf certState₂) }`. ```agda - -- LEDGER-V: equational reasoning - LEDGER-pov {Γ} {s} - (LEDGER-V {certState₁ = cs₁} {cs₂} {govSt₁} {govSt₂} - {utxoState₁ = us₁} {utxoState₂ = us₂} - (valid , subStep , certStep , govStep , utxoStep)) = - begin - getCoin (UTxOStateOf s) + rewardsBalance (DStateOf (CertStateOf s)) + coinFromDeposits (CertStateOf s) ≡⟨ step-i ⟩ - getCoin (UTxOStateOf s) + rewardsBalance (DStateOf cs₂) + allWdrls + coinFromDeposits (CertStateOf s) ≡⟨ arithmetic-1 ⟩ - getCoin (UTxOStateOf s) + allWdrls + coinFromDeposits (CertStateOf s) + rewardsBalance (DStateOf cs₂) ≡⟨ step-iii-iv ⟩ - getCoin us₂ + allDirectDeps + coinFromDeposits cs₂ + rewardsBalance (DStateOf cs₂) ≡⟨ arithmetic-2 ⟩ - getCoin us₂ + (rewardsBalance (DStateOf cs₂) + allDirectDeps) + coinFromDeposits cs₂ ≡⟨ step-ii ⟩ - getCoin us₂ + getCoin certStateFinal + coinFromDeposits cs₂ ∎ + LEDGER-pov {Γ} {s} + (LEDGER-V {certState₁ = cs₁} {cs₂} {govSt₁} {govSt₂} + {utxoState₁ = us₁} {utxoState₂ = us₂} + (valid , subStep , certStep , govStep , utxoStep)) = + begin + U₀ + R₀ + D₀ ≡⟨ step-i ⟩ + U₀ + R₂ + allWdrls + D₀ ≡⟨ arithmetic-1 U₀ R₂ allWdrls D₀ ⟩ + U₀ + allWdrls + D₀ + R₂ ≡⟨ step-iii-iv ⟩ + U₂ + allDirectDeps + D₂ + R₂ ≡⟨ arithmetic-2 U₂ allDirectDeps D₂ R₂ ⟩ + U₂ + (R₂ + allDirectDeps) + D₂ ≡⟨ step-ii ⟩ + U₂ + getCoin certStateFinal + D₂ ∎ where + + U₀ U₁ U₂ : Coin + U₀ = getCoin (UTxOStateOf s) + U₁ = getCoin us₁ + U₂ = getCoin us₂ + + D₀ D₂ : Coin + D₀ = coinFromDeposits (CertStateOf s) + D₂ = coinFromDeposits cs₂ + + R₀ R₂ : Coin + R₀ = rewardsBalance (DStateOf (CertStateOf s)) + R₂ = rewardsBalance (DStateOf cs₂) + certStateFinal : CertState certStateFinal = record cs₂ { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf cs₂) } + allDirectDeps : Coin + allDirectDeps = getCoin (allDirectDeposits tx) + subWdrlsCoin : Coin - subWdrlsCoin = sum (map (λ (stx : SubLevelTx) → getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx)) + subWdrlsCoin = sum (map wdrwl (SubTransactionsOf tx)) allWdrls : Coin allWdrls = getCoin (WithdrawalsOf tx) + subWdrlsCoin - allDirectDeps : Coin - 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 + 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) - ∎ + begin + getCoin (CertStateOf s) ≡⟨ SUBLEDGERS-certs-pov valid subStep ⟩ + getCoin cs₁ + subWdrlsCoin ≡⟨ cong (_+ subWdrlsCoin) (CERTS-pov (extract-utxo-netId utxoStep) certStep) ⟩ + 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 = - 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 ∎ - -- 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 = 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 = - let a = getCoin us₂ - b = allDirectDeps - c = coinFromDeposits cs₂ - d = rewardsBalance (DStateOf cs₂) - in + step-i : U₀ + R₀ + D₀ ≡ U₀ + R₂ + allWdrls + D₀ + step-i = 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 ∎ + U₀ + R₀ + D₀ ≡⟨ cong (λ x → U₀ + x + D₀ ) combined-certs ⟩ + U₀ + (R₂ + allWdrls) + D₀ ≡⟨ cong (_+ D₀) (sym (+-assoc U₀ R₂ allWdrls)) ⟩ + U₀ + R₂ + allWdrls + D₀ ∎ + -- applyDirectDeposits-rewardsBalance - step-ii : getCoin us₂ + (rewardsBalance (DStateOf cs₂) + allDirectDeps) + coinFromDeposits cs₂ - ≡ getCoin us₂ + getCoin certStateFinal + coinFromDeposits cs₂ - step-ii = cong (λ x → getCoin us₂ + x + coinFromDeposits cs₂) + step-ii : getCoin us₂ + (R₂ + allDirectDeps) + D₂ + ≡ getCoin us₂ + getCoin certStateFinal + D₂ + step-ii = cong (λ x → getCoin us₂ + x + D₂) (sym (applyDirectDeposits-rewardsBalance (allDirectDeposits tx) (DStateOf cs₂))) + + + -- Move the rightmost summand one position left (modulo re-assoc). + 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))) + + dc : DepositsChange + dc = calculateDepositsChange (CertStateOf s) cs₁ cs₂ + + dct dcs : ℤ + dct = DepositsChangeTopOf dc + dcs = DepositsChangeSubOf dc + + posneg : D₀ + posPart dct + posPart dcs ≡ D₂ + negPart dct + negPart dcs + posneg = posNeg-deposits (CertStateOf s) cs₁ cs₂ + + -- (MECH) UTXOW-V-mechanical, composed with the batch-wide invariants. + mech : U₁ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + ≡ U₂ + cbalance (UTxOOf (UTxOStateOf s) ∣ SpendInputsOf tx) + + mech = trans (UTXOW-V-mechanical utxoStep valid (fresh-top-tx-id valid subStep)) + (cong (U₂ +_) (utxo₁-tx-spend-eq valid refl subStep)) + + + arithmetic-1 : ∀ a b c d → a + b + c + d ≡ a + c + d + b + arithmetic-1 a b c d = 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 : ∀ a b c d → a + b + c + d ≡ a + (d + b) + c + arithmetic-2 a b c d = 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 ∎ + + + arithmetic-3 : ∀ a b c {d}{e}{f}{g} + → a + b + c + d + e + f + g ≡ a + e + b + (c + f + g) + d + arithmetic-3 a b c {d}{e}{f}{g} = begin + a + b + c + d + e + f + g ≡⟨ cong (λ x → x + f + g) (swap-right (a + b + c) d e) ⟩ + a + b + c + e + d + f + g ≡⟨ cong (_+ g) (swap-right (a + b + c + e) d f) ⟩ + a + b + c + e + f + d + g ≡⟨ swap-right (a + b + c + e + f) d g ⟩ + a + b + c + e + f + g + d ≡⟨ cong (λ x → x + f + g + d) (swap-right (a + b) c e) ⟩ + a + b + e + c + f + g + d ≡⟨ cong (λ x → x + c + f + g + d) (swap-right a b e) ⟩ + a + e + b + c + f + g + d ≡⟨ cong (_+ d) reassoc-middle ⟩ + (a + e) + b + (c + f + g) + d ∎ + where + reassoc-middle : a + e + b + c + f + g ≡ (a + e) + b + (c + f + g) + reassoc-middle = trans (+-assoc (a + e + b + c) f g) + (trans (+-assoc (a + e + b) c (f + g)) + (cong (a + e + b +_) (sym (+-assoc c f g)))) + + arithmetic-4 : ∀ a b c {d}{e}{f}{g} + → a + b + c + (d + e + f) + g ≡ a + (g + c + b + e + f) + d + arithmetic-4 a b c {d}{e}{f}{g} = begin + a + b + c + (d + e + f) + g ≡˘⟨ cong (_+ g) (+-assoc (a + b + c) (d + e) f) ⟩ + a + b + c + (d + e) + f + g ≡˘⟨ cong (λ x → x + f + g) (+-assoc (a + b + c) d e) ⟩ + a + b + c + d + e + f + g ≡⟨ swap-right (a + b + c + d + e) f g ⟩ + a + b + c + d + e + g + f ≡⟨ cong (_+ f) (swap-right (a + b + c + d) e g) ⟩ + a + b + c + d + g + e + f ≡⟨ cong (λ x → x + e + f) (swap-right (a + b + c) d g) ⟩ + a + b + c + g + d + e + f ≡⟨ cong (λ x → x + d + e + f) (swap-right (a + b) c g) ⟩ + a + b + g + c + d + e + f ≡⟨ cong (λ x → x + c + d + e + f) (swap-right a b g) ⟩ + a + g + b + c + d + e + f ≡⟨ cong (λ x → x + d + e + f) (swap-right (a + g) b c) ⟩ + a + g + c + b + d + e + f ≡⟨ cong (_+ f) (swap-right (a + g + c + b) d e) ⟩ + a + g + c + b + e + d + f ≡⟨ swap-right (a + g + c + b + e) d f ⟩ + a + g + c + b + e + f + d ≡⟨ cong (λ x → x + b + e + f + d) (+-assoc a g c) ⟩ + a + (g + c) + b + e + f + d ≡⟨ cong (λ x → x + e + f + d) (+-assoc a (g + c) b) ⟩ + a + (g + c + b) + e + f + d ≡⟨ cong (λ x → x + f + d) (+-assoc a (g + c + b) e) ⟩ + a + (g + c + b + e) + f + d ≡⟨ cong (_+ d) (+-assoc a (g + c + b + e) f) ⟩ + a + (g + c + b + e + f) + d ∎ + + arithmetic-5 : ∀ a b c {d}{e}{f}{g}{h}{i} + → a + (b + c + d + e + f + g + h) + i + ≡ a + b + c + d + e + f + g + h + i + arithmetic-5 a b c {d}{e}{f}{g}{h}{i} = cong (_+ i) $ + begin + a + (b + c + d + e + f + g + h) ≡˘⟨ +-assoc a _ h ⟩ + a + (b + c + d + e + f + g) + h ≡˘⟨ cong (_+ h) (+-assoc a _ g) ⟩ + a + (b + c + d + e + f) + g + h ≡˘⟨ cong (λ x → x + g + h) (+-assoc a _ f) ⟩ + a + (b + c + d + e) + f + g + h ≡˘⟨ cong (λ x → x + f + g + h) (+-assoc a _ e) ⟩ + a + (b + c + d) + e + f + g + h ≡˘⟨ cong (λ x → x + e + f + g + h) (+-assoc a _ d) ⟩ + a + (b + c) + d + e + f + g + h ≡˘⟨ cong (λ x → x + d + e + f + g + h) (+-assoc a b c) ⟩ + a + b + c + d + e + f + g + h ∎ + + arithmetic-6 : ∀ a b c {d}{e}{f}{g} + → a + b + c + d + e + f + g ≡ a + c + g + b + d + e + f + arithmetic-6 a b c {d}{e}{f}{g} = begin + a + b + c + d + e + f + g ≡⟨ cong (λ x → x + d + e + f + g) (swap-right a b c) ⟩ + a + c + b + d + e + f + g ≡⟨ swap-right (a + c + b + d + e) f g ⟩ + a + c + b + d + e + g + f ≡⟨ cong (_+ f) (swap-right (a + c + b + d) e g) ⟩ + a + c + b + d + g + e + f ≡⟨ cong (λ x → x + e + f) (swap-right (a + c + b) d g) ⟩ + a + c + b + g + d + e + f ≡⟨ cong (λ x → x + d + e + f) (swap-right (a + c) b g) ⟩ + a + c + g + b + d + e + f ∎ + + arithmetic-7 : ∀ a b c {d}{e}{f}{g} + → a + b + c + (d + e + f + g) ≡ a + b + c + d + e + f + g + arithmetic-7 a b c {d}{e}{f}{g} = begin + a + b + c + (d + e + f + g) ≡˘⟨ +-assoc (a + b + c) (d + e + f) g ⟩ + a + b + c + (d + e + f) + g ≡˘⟨ cong (_+ g) (+-assoc (a + b + c) (d + e) f) ⟩ + a + b + c + (d + e) + f + g ≡˘⟨ cong (λ x → x + f + g) (+-assoc (a + b + c) d e) ⟩ + a + b + c + d + e + f + g ∎ + + Ctop Csub : Coin + Ctop = cbalance (UTxOOf (UTxOStateOf s) ∣ SpendInputsOf tx) + Csub = sum (map (λ stx → cbalance (UTxOOf (UTxOStateOf s) ∣ SpendInputsOf stx)) (SubTransactionsOf tx)) + + Psub PsubDD : Coin + Psub = sum (map (λ stx → cbalance (outs stx) + DonationsOf stx) (SubTransactionsOf tx)) + PsubDD = sum (map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) + (SubTransactionsOf tx)) + + -- === The additive constant ================================================= + E : Coin + E = Ctop + Psub + posPart dct + posPart dcs + + bat' : Ctop + allWdrls + Csub + negPart dct + negPart dcs + ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + + allDirectDeps + Psub + posPart dct + posPart dcs + bat' = + begin + Ctop + W + Csub + negPart dct + negPart dcs + ≡⟨⟩ + Ctop + (Wtop + Wsub) + Csub + negPart dct + negPart dcs + ≡⟨ cong (λ x → x + Csub + negPart dct + negPart dcs) (sym (+-assoc Ctop Wtop Wsub)) ⟩ + Ctop + Wtop + Wsub + Csub + negPart dct + negPart dcs + ≡⟨ cong (λ x → x + negPart dct + negPart dcs) (swap-right (Ctop + Wtop) Wsub Csub) ⟩ + Ctop + Wtop + Csub + Wsub + negPart dct + negPart dcs + ≡⟨ cong (λ x → x + negPart dct + negPart dcs) (+-assoc (Ctop + Wtop) Csub Wsub) ⟩ + Ctop + Wtop + (Csub + Wsub) + negPart dct + negPart dcs + ≡˘⟨ cong (λ x → Ctop + Wtop + x + negPart dct + negPart dcs) + (sum-map-+ (λ stx → cbalance (UTxOOf s ∣ SpendInputsOf stx)) + wdrwl (SubTransactionsOf tx)) ⟩ + Ctop + Wtop + CsubW + negPart dct + negPart dcs + ≡⟨ cong (_+ negPart dcs) (swap-right (Ctop + Wtop) CsubW (negPart dct)) ⟩ + Ctop + Wtop + negPart dct + CsubW + negPart dcs + ≡⟨ UTXOW-batch-balance-coin utxoStep ⟩ + O + F + DN + DDtop + posPart dct + PsubDD + (posPart dcs) + ≡⟨ cong (λ x → O + F + DN + DDtop + posPart dct + x + posPart dcs) + (sum-map-+ (λ stx → cbalance (outs stx) + DonationsOf stx) + (λ stx → getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx)) ⟩ + O + F + DN + DDtop + posPart dct + (Psub + DDsub) + posPart dcs + ≡⟨ reshuffle-to-DD ⟩ + O + F + DN + (DDtop + DDsub) + Psub + posPart dct + posPart dcs + ≡⟨ cong (λ x → O + F + DN + x + Psub + posPart dct + posPart dcs) (sym DD-split) ⟩ + O + F + DN + DD + Psub + posPart dct + posPart dcs + ∎ + where + O = cbalance (outs tx) + F = TxFeesOf tx + DN = DonationsOf tx + DD = allDirectDeps + DDtop = getCoin (DirectDepositsOf tx) + DDsub = sum (map (λ stx → getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx)) + W = allWdrls + Wtop = getCoin (WithdrawalsOf tx) + Wsub = sum (map wdrwl (SubTransactionsOf tx)) + CsubW = sum (map (λ stx → cbalance (UTxOOf s ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx)) + reshuffle-to-DD : O + F + DN + DDtop + posPart dct + (Psub + DDsub) + posPart dcs + ≡ O + F + DN + (DDtop + DDsub) + Psub + posPart dct + posPart dcs + reshuffle-to-DD = begin + O + F + DN + DDtop + (posPart dct) + (Psub + DDsub) + (posPart dcs) + ≡⟨ cong (_+ (posPart dcs)) (sym (+-assoc (O + F + DN + DDtop + (posPart dct)) Psub DDsub)) ⟩ + O + F + DN + DDtop + (posPart dct) + Psub + DDsub + (posPart dcs) + ≡⟨ cong (_+ (posPart dcs)) (swap-right (O + F + DN + DDtop + (posPart dct)) Psub DDsub) ⟩ + O + F + DN + DDtop + (posPart dct) + DDsub + Psub + (posPart dcs) + ≡⟨ cong (λ x → x + Psub + (posPart dcs)) (swap-right (O + F + DN + DDtop) (posPart dct) DDsub) ⟩ + O + F + DN + DDtop + DDsub + (posPart dct) + Psub + (posPart dcs) + ≡⟨ cong (_+ (posPart dcs)) (swap-right (O + F + DN + DDtop + DDsub) (posPart dct) Psub) ⟩ + O + F + DN + DDtop + DDsub + Psub + (posPart dct) + (posPart dcs) + ≡⟨ cong (λ x → x + Psub + (posPart dct) + (posPart dcs)) (+-assoc (O + F + DN) DDtop DDsub) ⟩ + O + F + DN + (DDtop + DDsub) + Psub + (posPart dct) + (posPart dcs) + ∎ + + -- === Main chain ============================================================ + LHS+E≡RHS+E : (U₀ + allWdrls + D₀) + E ≡ (U₂ + allDirectDeps + D₂) + E + LHS+E≡RHS+E = begin + U₀ + allWdrls + D₀ + E + ≡⟨ refl ⟩ + U₀ + allWdrls + D₀ + (Ctop + Psub + posPart dct + posPart dcs) + ≡⟨ arithmetic-7 U₀ allWdrls D₀ ⟩ + U₀ + allWdrls + D₀ + Ctop + Psub + posPart dct + posPart dcs + ≡⟨ arithmetic-3 U₀ allWdrls D₀ ⟩ + U₀ + Psub + allWdrls + (D₀ + posPart dct + posPart dcs) + Ctop + ≡⟨ cong (λ x → x + allWdrls + (D₀ + posPart dct + posPart dcs) + Ctop) + (subst (λ u → U₀ + Psub ≡ U₁ + sum (map (λ stx → cbalance (u ∣ SpendInputsOf stx)) (SubTransactionsOf tx))) + (refl {x = UTxOOf s}) (SUBLEDGERS-utxo-coin valid subStep)) ⟩ + U₁ + Csub + allWdrls + (D₀ + posPart dct + posPart dcs) + Ctop + ≡⟨ cong (λ x → (U₁ + Csub) + allWdrls + x + Ctop) posneg ⟩ + U₁ + Csub + allWdrls + (D₂ + negPart dct + negPart dcs) + Ctop + ≡⟨ arithmetic-4 U₁ Csub allWdrls ⟩ + U₁ + (Ctop + allWdrls + Csub + negPart dct + negPart dcs) + D₂ + ≡⟨ cong (λ x → U₁ + x + D₂) bat' ⟩ + U₁ + (cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + allDirectDeps + Psub + posPart dct + posPart dcs) + D₂ + ≡⟨ arithmetic-5 U₁ (cbalance (outs tx)) (TxFeesOf tx) ⟩ + U₁ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + allDirectDeps + Psub + posPart dct + posPart dcs + D₂ + ≡⟨ cong (λ x → x + allDirectDeps + Psub + posPart dct + posPart dcs + D₂) mech ⟩ + U₂ + Ctop + allDirectDeps + Psub + posPart dct + posPart dcs + D₂ + ≡⟨ arithmetic-6 U₂ Ctop allDirectDeps ⟩ + U₂ + allDirectDeps + D₂ + Ctop + Psub + posPart dct + posPart dcs + ≡˘⟨ arithmetic-7 U₂ allDirectDeps D₂ ⟩ + U₂ + allDirectDeps + D₂ + E + ∎ + + -- deposit accounting + batch UTxO combined + step-iii-iv : U₀ + allWdrls + D₀ + R₂ ≡ U₂ + allDirectDeps + D₂ + R₂ + step-iii-iv = cong (_+ R₂) + (+-cancelʳ-≡ E (U₀ + allWdrls + D₀) (U₂ + allDirectDeps + D₂) LHS+E≡RHS+E) ``` diff --git a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md index edffa64b1..a56476ff8 100644 --- a/src/Ledger/Dijkstra/Specification/Utxo.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxo.lagda.md @@ -223,6 +223,12 @@ instance HasDepositsChangeSub-DepositsChange : HasDepositsChangeSub DepositsChange HasDepositsChangeSub-DepositsChange .DepositsChangeSubOf = DepositsChange.depositsChangeSub + HasDepositsChangeTop-UTxOEnv : HasDepositsChangeTop UTxOEnv + HasDepositsChangeTop-UTxOEnv .DepositsChangeTopOf = DepositsChangeTopOf ∘ DepositsChangeOf + + HasDepositsChangeSub-UTxOEnv : HasDepositsChangeSub UTxOEnv + HasDepositsChangeSub-UTxOEnv .DepositsChangeSubOf = DepositsChangeSubOf ∘ DepositsChangeOf + unquoteDecl HasCast-DepositsChange HasCast-UTxOEnv HasCast-SubUTxOEnv diff --git a/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md index 4efd9b050..35626c889 100644 --- a/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md @@ -403,7 +403,7 @@ coin-of-producedBatch tx dc = begin swap-right a b c = trans (+-assoc a b c) (trans (cong (a +_) (+-comm b c)) (sym (+-assoc a c b))) -module _ +module UTxO-PoV (tx : TopLevelTx) (let open Tx tx; open TxBody txBody) -- ASSUMPTIONS -- @@ -528,25 +528,25 @@ proof actually consumes. We expose it as a separate lemma here. ```agda batch-balance-coin : (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁ → cbalance (UTxOOf Γ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) - + negPart (DepositsChangeTopOf (DepositsChangeOf Γ)) + + negPart (DepositsChangeTopOf Γ) + sum ( map (λ stx → cbalance (UTxOOf Γ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx) ) - + negPart (DepositsChangeSubOf (DepositsChangeOf Γ)) + + negPart (DepositsChangeSubOf Γ) ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) - + posPart (DepositsChangeTopOf (DepositsChangeOf Γ)) + + posPart (DepositsChangeTopOf Γ) + sum ( map (λ stx → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx)) - + posPart (DepositsChangeSubOf (DepositsChangeOf Γ)) + + posPart (DepositsChangeSubOf Γ) batch-balance-coin {Γ = Γ} (UTXO-⋯ _ _ _ _ _ _ _ batchBal _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) = begin - cbalance (UTxOOf Γ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf (DepositsChangeOf Γ)) + _ + _ + cbalance (UTxOOf Γ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + negPart (DepositsChangeTopOf Γ) + _ + _ ≡˘⟨ coin-of-consumedBatch tx (DepositsChangeOf Γ) (UTxOOf Γ) noMintTx noMintSubTx ⟩ coin (consumedBatch (DepositsChangeOf Γ) tx (UTxOOf Γ)) ≡⟨ cong coin batchBal ⟩ coin (producedBatch (DepositsChangeOf Γ) tx) ≡⟨ coin-of-producedBatch tx (DepositsChangeOf Γ) ⟩ - cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + posPart (DepositsChangeTopOf (DepositsChangeOf Γ)) + _ + _ + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + posPart (DepositsChangeTopOf Γ) + _ + _ ∎ ``` @@ -574,8 +574,7 @@ when combined with the `SUBLEDGERS-pov`{.AgdaFunction} lemma. ```agda {-- - UTXO-pov : - ∀ {Γ : UTxOEnv} {legacyMode : Bool} {s₀ s₁ : UTxOState} + UTXO-pov : ∀ {Γ : UTxOEnv} {legacyMode : Bool} {s₀ s₁ : UTxOState} → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s₀)) → (Γ , legacyMode) ⊢ s₀ ⇀⦇ tx ,UTXO⦈ s₁ → getCoin s₀ diff --git a/src/Ledger/Dijkstra/Specification/Utxow/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Utxow/Properties/PoV.lagda.md index 58952f399..df2cc9c71 100644 --- a/src/Ledger/Dijkstra/Specification/Utxow/Properties/PoV.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxow/Properties/PoV.lagda.md @@ -48,10 +48,9 @@ and `UTXOW-legacy`{.AgdaInductiveConstructor} embed a `UTXO`{.AgdaDatatype} derivation as their final premise. We factor out an extractor: ```agda -UTXOW⇒UTXO : - ∀ {Γ : UTxOEnv} {s s' : UTxOState} {tx : TopLevelTx} - → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' - → ∃[ legacyMode ] ((Γ , legacyMode) ⊢ s ⇀⦇ tx ,UTXO⦈ s') +UTXOW⇒UTXO : ∀ {Γ : UTxOEnv} {s s' : UTxOState} {tx : TopLevelTx} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → ∃[ legacyMode ] ((Γ , legacyMode) ⊢ s ⇀⦇ tx ,UTXO⦈ s') + UTXOW⇒UTXO (UTXOW-normal-⋯ _ _ _ _ _ _ _ _ _ _ utxo) = false , utxo UTXOW⇒UTXO (UTXOW-legacy-⋯ _ _ _ _ _ _ _ _ _ _ _ _ _ utxo) = true , utxo ``` @@ -63,116 +62,58 @@ exactly (collateral is moved from the UTxO to the fees, both of which are counted in `getCoin`{.AgdaField}): ```agda -module _ (tx : TopLevelTx) (let open Tx tx; open TxBody txBody) +module UTXOW-PoV (tx : TopLevelTx) (let open Tx tx; open TxBody txBody) -- Same assumptions as the UTXO-pov module. - ( balance-∪ : ∀ {u u' : UTxO} → disjoint (dom u) (dom u') - → cbalance (u ∪ˡ u') ≡ cbalance u + cbalance u' ) - - ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn) - → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) ) + ( balance-∪ : ∀ {u u' : UTxO} → disjoint (dom u) (dom u') → cbalance (u ∪ˡ u') ≡ cbalance u + cbalance u' ) - ( outs-disjoint : ∀ {u : UTxO} - → TxIdOf tx ∉ mapˢ proj₁ (dom u) - → disjoint (dom (u ∣ SpendInputsOf tx ᶜ)) (dom (outs tx)) ) + ( split-balance : ∀ (u : UTxO) (keys : ℙ TxIn) → cbalance u ≡ cbalance (u ∣ keys ᶜ) + cbalance (u ∣ keys) ) - ( coin-of-consumedBatch : - ∀ (dc : DepositsChange) (utxo₀ : UTxO) - → let open DepositsChange dc in - coin (consumedBatch dc tx utxo₀) ≡ _ ) + ( noMintTx : coin (MintedValueOf tx) ≡ 0 ) - ( coin-of-producedBatch : - ∀ (dc : DepositsChange) - → let open DepositsChange dc in - coin (producedBatch dc tx) ≡ _ ) + ( noMintSubTx : noMintingSubTxs tx ) + ( outs-disjoint : ∀ {u : UTxO} → TxIdOf tx ∉ mapˢ proj₁ (dom u) → disjoint (dom (u ∣ SpendInputsOf tx ᶜ)) (dom (outs tx)) ) where - - -- Instantiate the inner `module _` of `Utxo.Properties.PoV`. - private - module U = - Ledger.Dijkstra.Specification.Utxo.Properties.PoV - txs abs - -- `utxo-pov-mod` refers to the parameterized inner module of `U` - -- (the one that takes `tx` and the arithmetic assumptions). + open UTxO-PoV tx (λ {u} {u'} → balance-∪ {u} {u'}) split-balance noMintTx noMintSubTx + -- The `λ {u}{u'} → balance-∪ {u}{u'}` η-expansion is needed because passing + -- `balance-∪` directly triggers Agda to eta-expand the `{u u' : UTxO}` implicits + -- through UTxO's `Σ _ left-unique` record structure, leaving the `left-unique` + -- field as an unresolved meta. Binding `{u}{u'}` as pattern variables in the outer + -- lambda makes them concrete bound values and sidesteps the eta-expansion. + + UTXOW-I-getCoin : ∀ {Γ : UTxOEnv} {s s' : UTxOState} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → IsValidFlagOf tx ≡ false → getCoin s ≡ getCoin s' + UTXOW-I-getCoin {Γ} utxow invalid = UTXO-I-getCoin (proj₂ (UTXOW⇒UTXO utxow)) invalid ``` -```agda - UTXOW-I-getCoin : - ∀ {Γ : UTxOEnv} {s s' : UTxOState} - → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' - → IsValidFlagOf tx ≡ false - → getCoin s ≡ getCoin s' - UTXOW-I-getCoin utxow invalid = - let (_ , utxo) = UTXOW⇒UTXO utxow - in U-pov.UTXO-I-getCoin utxo invalid - where - -- Re-instantiate the inner module with our assumption lemmas. - module U-pov = - U tx balance-∪ split-balance outs-disjoint - coin-of-consumedBatch coin-of-producedBatch -``` - -(The inner module instantiation is a bit boilerplate-heavy; in practice this -should be simplified once the final module structure of `Utxo.Properties.PoV` -is settled.) - ## `UTXOW-V-mechanical`: mechanical rearrangement The valid case simply reuses the UTXO-level mechanical rearrangement: ```agda - UTXOW-V-mechanical : - ∀ {Γ : UTxOEnv} {s s' : UTxOState} - → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' - → IsValidFlagOf tx ≡ true - → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s)) + UTXOW-V-mechanical : ∀ {Γ : UTxOEnv} {s s' : UTxOState} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → IsValidFlagOf tx ≡ true → TxIdOf tx ∉ mapˢ proj₁ (dom (UTxOOf s)) → getCoin s + cbalance (outs tx) + TxFeesOf tx + DonationsOf tx ≡ getCoin s' + cbalance (UTxOOf s ∣ SpendInputsOf tx) - UTXOW-V-mechanical utxow valid fresh = - let (_ , utxo) = UTXOW⇒UTXO utxow - in U-pov.UTXO-V-mechanical utxo valid fresh - where - module U-pov = - U tx balance-∪ split-balance outs-disjoint - coin-of-consumedBatch coin-of-producedBatch + + UTXOW-V-mechanical utxow valid fresh = UTXO-V-mechanical (proj₂ (UTXOW⇒UTXO utxow)) valid fresh ``` ## `UTXOW-batch-balance-coin` ```agda - UTXOW-batch-balance-coin : - ∀ {Γ : UTxOEnv} {s s' : UTxOState} + UTXOW-batch-balance-coin : ∀ {Γ : UTxOEnv} {s s' : UTxOState} → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' - → let dc = DepositsChangeOf Γ - utxo₀ = UTxOOf Γ - open DepositsChange dc - in cbalance (utxo₀ ∣ SpendInputsOf tx) - + getCoin (WithdrawalsOf tx) - + negPart depositsChangeTop - + sum (map (λ (stx : SubLevelTx) → - cbalance (utxo₀ ∣ SpendInputsOf stx) - + getCoin (WithdrawalsOf stx)) - (SubTransactionsOf tx)) - + negPart depositsChangeSub - ≡ cbalance (outs tx) - + TxFeesOf tx - + DonationsOf tx - + getCoin (DirectDepositsOf tx) - + posPart depositsChangeTop - + sum (map (λ (stx : SubLevelTx) → - cbalance (outs stx) - + DonationsOf stx - + getCoin (DirectDepositsOf stx)) - (SubTransactionsOf tx)) - + posPart depositsChangeSub - UTXOW-batch-balance-coin utxow = - let (_ , utxo) = UTXOW⇒UTXO utxow - in U-pov.batch-balance-coin utxo - where - module U-pov = - U tx balance-∪ split-balance outs-disjoint - coin-of-consumedBatch coin-of-producedBatch + → cbalance (UTxOOf Γ ∣ SpendInputsOf tx) + getCoin (WithdrawalsOf tx) + + negPart (DepositsChangeTopOf Γ) + + sum (map (λ stx → cbalance (UTxOOf Γ ∣ SpendInputsOf stx) + getCoin (WithdrawalsOf stx)) (SubTransactionsOf tx)) + + negPart (DepositsChangeSubOf Γ) + ≡ cbalance (outs tx) + TxFeesOf tx + DonationsOf tx + getCoin (DirectDepositsOf tx) + + posPart (DepositsChangeTopOf Γ) + + sum ( map (λ (stx : SubLevelTx) → cbalance (outs stx) + DonationsOf stx + getCoin (DirectDepositsOf stx)) (SubTransactionsOf tx) ) + + posPart (DepositsChangeSubOf Γ) + UTXOW-batch-balance-coin utxow = batch-balance-coin (proj₂ (UTXOW⇒UTXO utxow)) ``` ## `utxow-pov-invalid` for use in `LEDGER-pov` @@ -182,11 +123,8 @@ The following is the *specific* form needed by `Ledger.Properties.PoV` identical to `UTXOW-I-getCoin`{.AgdaFunction} above, retagged for clarity: ```agda - utxow-pov-invalid : - ∀ {Γ : UTxOEnv} {s s' : UTxOState} - → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' - → IsValidFlagOf tx ≡ false - → getCoin s ≡ getCoin s' + utxow-pov-invalid : ∀ {Γ : UTxOEnv} {s s' : UTxOState} + → Γ ⊢ s ⇀⦇ tx ,UTXOW⦈ s' → IsValidFlagOf tx ≡ false → getCoin s ≡ getCoin s' utxow-pov-invalid = UTXOW-I-getCoin ```