[Dijkstra] Add starting account balance intervals

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

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
 
@@ -175,12 +181,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 +205,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

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
 ```

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}

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)

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
 ```
 
 <!--
@@ -97,14 +98,18 @@ module _ {tx : TopLevelTx} where
     Dec-UsesV4Features : UsesV4Features tx ⁇
     Dec-UsesV4Features .dec
       with ¿ ¬ (∀[ g ∈ GuardsOf tx ] IsKeyHashObj g) ¿
-         | ¿ ¬ Is-∅ (dom (DirectDepositsOf tx)) ¿ | ¿ ¬ Is-∅ (dom (BalanceIntervalsOf tx)) ¿
-    ... | yes p | _ | _ = yes (hasScriptGuards p)
-    ... | _ | yes p | _ = yes (hasDirectDeposits p)
-    ... | _ | _ | yes p = yes (hasBalanceIntervals p)
-    ... | no p₂ | no p₃ | no p₄
+         | ¿ ¬ Is-∅ (dom (DirectDepositsOf tx)) ¿
+         | ¿ ¬ Is-∅ (dom (BalanceIntervalsOf tx)) ¿
+         | ¿ ¬ Is-∅ (dom (StartingBalanceIntervalsOf tx)) ¿
+    ... | yes p | _ | _ | _ = yes (hasScriptGuards p)
+    ... | _ | yes p | _ | _ = yes (hasDirectDeposits p)
+    ... | _ | _ | yes p | _ = yes (hasBalanceIntervals p)
+    ... | _ | _ | _ | yes p = yes (hasStartingBalanceIntervals p)
+    ... | no p₂ | no p₃ | no p₄ | no p₅
       = no λ { (hasScriptGuards x) → p₂ x
              ; (hasDirectDeposits x) → p₃ x
-             ; (hasBalanceIntervals x) → p₄ x }
+             ; (hasBalanceIntervals x) → p₄ x
+             ; (hasStartingBalanceIntervals x) → p₅ x }
 ```
 -->