From aa3b64bb2a887e339bce6ca6a38e99299939269f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Thu, 3 Sep 2026 13:50:37 +0200 Subject: [PATCH 1/4] Add starting account balance intervals --- src/Ledger/Dijkstra/Foreign/Transaction.agda | 1 + .../Dijkstra/Specification/Entities.lagda.md | 17 ++++++++----- .../Properties/Computational.lagda.md | 21 +++++++++++----- .../Specification/Transaction.lagda.md | 24 +++++++++++++++---- 4 files changed, 46 insertions(+), 17 deletions(-) diff --git a/src/Ledger/Dijkstra/Foreign/Transaction.agda b/src/Ledger/Dijkstra/Foreign/Transaction.agda index c951548b90..d6cf075fc4 100644 --- a/src/Ledger/Dijkstra/Foreign/Transaction.agda +++ b/src/Ledger/Dijkstra/Foreign/Transaction.agda @@ -136,6 +136,7 @@ record TxBodyTop : Type where txGuards : ℙ Credential txDirectDeposits : DirectDeposits txBalanceIntervals : AccountBalanceIntervals + txStartingBalanceIntervals : AccountBalanceIntervals instance convTxBodyTop : Convertible (TxBody TxLevelTop) TxBodyTop diff --git a/src/Ledger/Dijkstra/Specification/Entities.lagda.md b/src/Ledger/Dijkstra/Specification/Entities.lagda.md index 11c234a2da..b1c2649d8c 100644 --- a/src/Ledger/Dijkstra/Specification/Entities.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Entities.lagda.md @@ -175,12 +175,13 @@ data _⊢_⇀⦇_,ENTITIES⦈_ : EntitiesEnv → CertState → TopLevelTx → Ce let refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txTop)) refreshedDReps = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh - withdrawalsSubTxs = foldl (λ acc txSub → acc ∪⁺ WithdrawalsOf txSub) ∅ (SubTransactionsOf txTop) - withdrawals = WithdrawalsOf txTop - withdrawalsCredentials = mapˢ stake (dom withdrawals) - accountBalanceIntervals = BalanceIntervalsOf txTop - directDeposits = DirectDepositsOf txTop - directDepositsCredentials = mapˢ stake (dom directDeposits) + withdrawalsSubTxs = foldl (λ acc txSub → acc ∪⁺ WithdrawalsOf txSub) ∅ (SubTransactionsOf txTop) + withdrawals = WithdrawalsOf txTop + withdrawalsCredentials = mapˢ stake (dom withdrawals) + accountBalanceIntervals = BalanceIntervalsOf txTop + startingAccountBalanceIntervals = StartingBalanceIntervalsOf txTop + directDeposits = DirectDepositsOf txTop + directDepositsCredentials = mapˢ stake (dom directDeposits) in ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId @@ -198,6 +199,10 @@ data _⊢_⇀⦇_,ENTITIES⦈_ : EntitiesEnv → CertState → TopLevelTx → Ce ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? rewards c)) interval) + ∙ dom startingAccountBalanceIntervals ⊆ dom rewards₀ + ∙ ∀[ (c , interval) ∈ startingAccountBalanceIntervals ˢ ] + (InBalanceInterval (maybe id 0 (lookupᵐ? rewards₀ c)) interval) + ∙ ⟦ e , pp , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , applyWithdrawals withdrawals rewards , depositsᵈ ⟧ , pState , ⟦ refreshedDReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ DCertsOf txTop ,CERTS⦈ ⟦ ⟦ voteDelegs' , stakeDelegs' , rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧ ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId diff --git a/src/Ledger/Dijkstra/Specification/Entities/Properties/Computational.lagda.md b/src/Ledger/Dijkstra/Specification/Entities/Properties/Computational.lagda.md index db81d681b9..655501aaed 100644 --- a/src/Ledger/Dijkstra/Specification/Entities/Properties/Computational.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Entities/Properties/Computational.lagda.md @@ -103,6 +103,7 @@ instance withdrawals = WithdrawalsOf txTop withdrawalsCredentials = mapˢ stake (dom withdrawals) accountBalanceIntervals = BalanceIntervalsOf txTop + startingAccountBalanceIntervals = StartingBalanceIntervalsOf txTop directDeposits = DirectDepositsOf txTop directDepositsCredentials = mapˢ stake (dom directDeposits) @@ -132,18 +133,22 @@ instance ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval) + ∙ dom startingAccountBalanceIntervals ⊆ dom Γ.rewards₀ + ∙ ∀[ (c , interval) ∈ startingAccountBalanceIntervals ˢ ] + (InBalanceInterval (maybe id 0 (lookupᵐ? Γ.rewards₀ c)) interval) + ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId ¿ | Computational-CERTS.computeProof ⟦ Γ.epoch , Γ.pp , Γ.coldCredentials ⟧ s₁ (DCertsOf txTop) ... | no ¬p | _ = failure "" ... | yes _ | failure e = failure e - ... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇) | success (s₂ , p) + ... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉) | success (s₂ , p) with ¿ ∙ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿ ... | no ¬p = failure "" - ... | yes p₈ = success (-, (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p , p₇ , p₈))) + ... | yes p₁₀ = success (-, (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p , p₉ , p₁₀))) completeness : ∀ (s' : CertState) → Γ ⊢ s₀ ⇀⦇ txTop ,ENTITIES⦈ s' → map proj₁ computeProof ≡ success s' - completeness s' (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p , p₇ , p₈)) + completeness s' (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p , p₉ , p₁₀)) with ¿ ∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId ∙ withdrawalsCredentials ⊆ dom (RewardsOf s₀) @@ -160,12 +165,16 @@ instance ∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ] (InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval) + ∙ dom startingAccountBalanceIntervals ⊆ dom Γ.rewards₀ + ∙ ∀[ (c , interval) ∈ startingAccountBalanceIntervals ˢ ] + (InBalanceInterval (maybe id 0 (lookupᵐ? Γ.rewards₀ c)) interval) + ∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId ¿ | Computational-CERTS.computeProof ⟦ Γ.epoch , Γ.pp , Γ.coldCredentials ⟧ s₁ (DCertsOf txTop) | Computational-CERTS.completeness _ _ _ _ p - ... | no ¬p | _ | p' = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇)) + ... | no ¬p | _ | p' = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉)) ... | yes _ | failure e | () - ... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆) | success (s₂ , p) | refl + ... | yes _ | success (s₂ , p) | refl with ¿ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿ - ... | no ¬p = ⊥-elim (¬p p₈) + ... | no ¬p = ⊥-elim (¬p p₁₀) ... | yes _ = refl ``` diff --git a/src/Ledger/Dijkstra/Specification/Transaction.lagda.md b/src/Ledger/Dijkstra/Specification/Transaction.lagda.md index 1404bd6c6b..cfef1a170f 100644 --- a/src/Ledger/Dijkstra/Specification/Transaction.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Transaction.lagda.md @@ -236,6 +236,10 @@ Of particular note in the Dijkstra era are interval as a Phase-1 validity condition, analogous to how slot validity intervals constrain the time at which a transaction may be processed. ++ `txStartingBalanceIntervals`{.AgdaField}: only present in top-level transactions, + this field records the account balance interval assertions that this transaction + makes about account balances before any sub-transaction is processed. + ```agda mutual record Tx (txLevel : TxLevel) : Type where @@ -269,11 +273,12 @@ Of particular note in the Dijkstra era are scriptIntegrityHash : Maybe ScriptHash -- New in Dijkstra -- - txSubTransactions : InTopLevel txLevel (List (Tx TxLevelSub)) - txGuards : ℙ Credential - txRequiredTopLevelGuards : ℙ (Credential × Maybe Datum) - txDirectDeposits : DirectDeposits - txBalanceIntervals : AccountBalanceIntervals + txSubTransactions : InTopLevel txLevel (List (Tx TxLevelSub)) + txGuards : ℙ Credential + txRequiredTopLevelGuards : ℙ (Credential × Maybe Datum) + txDirectDeposits : DirectDeposits + txBalanceIntervals : AccountBalanceIntervals + txStartingBalanceIntervals : InTopLevel txLevel AccountBalanceIntervals --------------------- requiredSignerHashes : ℙ KeyHash @@ -420,6 +425,10 @@ could be either of them. field BalanceIntervalsOf : A → AccountBalanceIntervals open HasBalanceIntervals ⦃...⦄ public + record HasStartingBalanceIntervals {a} (A : Type a) : Type a where + field StartingBalanceIntervalsOf : A → AccountBalanceIntervals + open HasStartingBalanceIntervals ⦃...⦄ public + record HasIsValidFlag {a} (A : Type a) : Type a where field IsValidFlagOf : A → Bool open HasIsValidFlag ⦃...⦄ public @@ -476,6 +485,11 @@ could be either of them. HasBalanceIntervals-Tx : HasBalanceIntervals (Tx txLevel) HasBalanceIntervals-Tx .BalanceIntervalsOf = BalanceIntervalsOf ∘ TxBodyOf + HasStartingBalanceIntervals-TxBody : HasStartingBalanceIntervals (TxBody TxLevelTop) + HasStartingBalanceIntervals-TxBody .StartingBalanceIntervalsOf = TxBody.txStartingBalanceIntervals + HasStartingBalanceIntervals-Tx : HasStartingBalanceIntervals TopLevelTx + HasStartingBalanceIntervals-Tx .StartingBalanceIntervalsOf = StartingBalanceIntervalsOf ∘ TxBodyOf + HasValidInterval-TxBody : HasValidInterval (TxBody txLevel) HasValidInterval-TxBody .ValidIntervalOf = TxBody.txVldt HasValidInterval-Tx : HasValidInterval (Tx txLevel) From e2d35cfbd07a205f9703c1633f23e9f60e94171e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Fri, 4 Sep 2026 12:27:14 +0200 Subject: [PATCH 2/4] Fix PoV ENTITIES --- .../Dijkstra/Specification/Entities/Properties/PoV.lagda.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Ledger/Dijkstra/Specification/Entities/Properties/PoV.lagda.md b/src/Ledger/Dijkstra/Specification/Entities/Properties/PoV.lagda.md index 1b5ca501c1..e920119537 100644 --- a/src/Ledger/Dijkstra/Specification/Entities/Properties/PoV.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Entities/Properties/PoV.lagda.md @@ -197,7 +197,7 @@ normal mode the rule bounds withdrawals only against the pre-batch ENTITIES-pov {txTop = txTop} {s = ⟦ ⟦ _ , _ , r₀ , _ ⟧ᵈ , _ , _ ⟧ᶜˢ} amts≤ - (ENTITIES {rewards' = r₁} (wd-netId , wdrls⊆ , _ , _ , _ , _ , certsStep , _ , ddCreds⊆)) = + (ENTITIES {rewards' = r₁} (wd-netId , wdrls⊆ , _ , _ , _ , _ , _ , _ , certsStep , _ , ddCreds⊆)) = begin getCoin r₀ + dd ≡⟨ cong (_+ dd) (applyWithdrawals-pov (WithdrawalsOf txTop) r₀ wdrls⊆ wd-netId amts≤) ⟩ @@ -249,7 +249,7 @@ preservation of `PoolDepositsRegistered`{.AgdaFunction}, and the + newCertDeposits (EntitiesEnv.pp Γ) (dom (PoolsOf s)) (DCertsOf txTop) ≡ coinFromDeposits s' + refundCertDeposits (EntitiesEnv.pp Γ) (DCertsOf txTop) - ENTITIES-deposits-pov registered (ENTITIES (_ , _ , _ , _ , _ , _ , certsStep , _ , _)) = + ENTITIES-deposits-pov registered (ENTITIES (_ , _ , _ , _ , _ , _ , _ , _ , certsStep , _ , _)) = CERTS-deposits-pov registered certsStep SUBENTITIES-deposits-registered : {Γ : SubEntitiesEnv} {s s' : CertState} @@ -263,7 +263,7 @@ preservation of `PoolDepositsRegistered`{.AgdaFunction}, and the → PoolDepositsRegistered s → Γ ⊢ s ⇀⦇ txTop ,ENTITIES⦈ s' → PoolDepositsRegistered s' - ENTITIES-deposits-registered registered (ENTITIES (_ , _ , _ , _ , _ , _ , certsStep , _ , _)) = + ENTITIES-deposits-registered registered (ENTITIES (_ , _ , _ , _ , _ , _ , _ , _ , certsStep , _ , _)) = CERTS-deposits-registered registered certsStep SUBENTITIES-new-thread : {Γ : SubEntitiesEnv} {s s' : CertState} From 93b8810c7f04a063a6585c63c9a80127ff5f538d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Wed, 9 Sep 2026 13:06:25 +0200 Subject: [PATCH 3/4] Update src/Ledger/Dijkstra/Specification/Entities.lagda.md Co-authored-by: William DeMeo --- src/Ledger/Dijkstra/Specification/Entities.lagda.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/Ledger/Dijkstra/Specification/Entities.lagda.md b/src/Ledger/Dijkstra/Specification/Entities.lagda.md index b1c2649d8c..828d55fc0f 100644 --- a/src/Ledger/Dijkstra/Specification/Entities.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Entities.lagda.md @@ -99,7 +99,13 @@ withdrawals, direct deposits, and account balance intervals. CIP-159 introduces two new fields to transactions: `directDeposits` and `balanceIntervals`. Direct deposits represent value that flows from the transaction into account addresses. Balance intervals enable -transactions to assert predicates about account balances. +CIP-159 introduces three new transaction fields: `txDirectDeposits`{.AgdaField}, +`txBalanceIntervals`{.AgdaField} and, at the top level only, +`txStartingBalanceIntervals`{.AgdaField}. Direct deposits represent value that +flows from the transaction into account addresses. The two interval fields let +a transaction assert bounds on account balances: `txBalanceIntervals`{.AgdaField} +against the balances this rule sees, and `txStartingBalanceIntervals`{.AgdaField} +against the balances at the start of the whole batch (`rewards₀`{.AgdaField}). ### Withdrawals From 2073267b92bcfe303f084801dc8bba302335c2f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Carlos=20Tom=C3=A9=20Corti=C3=B1as?= Date: Wed, 9 Sep 2026 16:06:13 +0200 Subject: [PATCH 4/4] Add StartingBalanceIntevals to UsesV4Features --- .../Dijkstra/Specification/Utxow.lagda.md | 23 +++++++++++-------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/src/Ledger/Dijkstra/Specification/Utxow.lagda.md b/src/Ledger/Dijkstra/Specification/Utxow.lagda.md index 434feb7114..b6da08e525 100644 --- a/src/Ledger/Dijkstra/Specification/Utxow.lagda.md +++ b/src/Ledger/Dijkstra/Specification/Utxow.lagda.md @@ -64,9 +64,10 @@ module _ (tx : TopLevelTx) where hasConwayCerts : L.Any IsConwayCert (DCertsOf tx) → UsesV3Features data UsesV4Features : Set where - hasScriptGuards : ¬ (∀[ g ∈ GuardsOf tx ] IsKeyHashObj g) → UsesV4Features - hasDirectDeposits : ¬ Is-∅ (dom (DirectDepositsOf tx)) → UsesV4Features - hasBalanceIntervals : ¬ Is-∅ (dom (BalanceIntervalsOf tx)) → UsesV4Features + hasScriptGuards : ¬ (∀[ g ∈ GuardsOf tx ] IsKeyHashObj g) → UsesV4Features + hasDirectDeposits : ¬ Is-∅ (dom (DirectDepositsOf tx)) → UsesV4Features + hasBalanceIntervals : ¬ Is-∅ (dom (BalanceIntervalsOf tx)) → UsesV4Features + hasStartingBalanceIntervals : ¬ Is-∅ (dom (StartingBalanceIntervalsOf tx)) → UsesV4Features ```