Skip to content

Commit 8f514a6

Browse files
carlostomecarlostome
committed
Add starting account balance intervals
1 parent 8e87437 commit 8f514a6

4 files changed

Lines changed: 46 additions & 17 deletions

File tree

‎src/Ledger/Dijkstra/Foreign/Transaction.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,7 @@ record TxBodyTop : Type where
136136
txGuards : ℙ Credential
137137
txDirectDeposits : DirectDeposits
138138
txBalanceIntervals : AccountBalanceIntervals
139+
txStartingBalanceIntervals : AccountBalanceIntervals
139140

140141
instance
141142
convTxBodyTop : Convertible (TxBody TxLevelTop) TxBodyTop

‎src/Ledger/Dijkstra/Specification/Entities.lagda.md‎

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -177,12 +177,13 @@ data _⊢_⇀⦇_,ENTITIES⦈_ : EntitiesEnv → CertState → TopLevelTx → Ce
177177
let refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList (ListOfGovVotesOf txTop))
178178
refreshedDReps = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
179179
180-
withdrawalsSubTxs = foldl (λ acc txSub → acc ∪⁺ WithdrawalsOf txSub) ∅ (SubTransactionsOf txTop)
181-
withdrawals = WithdrawalsOf txTop
182-
withdrawalsCredentials = mapˢ stake (dom withdrawals)
183-
accountBalanceIntervals = BalanceIntervalsOf txTop
184-
directDeposits = DirectDepositsOf txTop
185-
directDepositsCredentials = mapˢ stake (dom directDeposits)
180+
withdrawalsSubTxs = foldl (λ acc txSub → acc ∪⁺ WithdrawalsOf txSub) ∅ (SubTransactionsOf txTop)
181+
withdrawals = WithdrawalsOf txTop
182+
withdrawalsCredentials = mapˢ stake (dom withdrawals)
183+
accountBalanceIntervals = BalanceIntervalsOf txTop
184+
startingAccountBalanceIntervals = StartingBalanceIntervalsOf txTop
185+
directDeposits = DirectDepositsOf txTop
186+
directDepositsCredentials = mapˢ stake (dom directDeposits)
186187
in
187188
188189
∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId
@@ -200,6 +201,10 @@ data _⊢_⇀⦇_,ENTITIES⦈_ : EntitiesEnv → CertState → TopLevelTx → Ce
200201
∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ]
201202
(InBalanceInterval (maybe id 0 (lookupᵐ? rewards c)) interval)
202203
204+
∙ dom startingAccountBalanceIntervals ⊆ dom rewards₀
205+
∙ ∀[ (c , interval) ∈ startingAccountBalanceIntervals ˢ ]
206+
(InBalanceInterval (maybe id 0 (lookupᵐ? rewards₀ c)) interval)
207+
203208
∙ ⟦ e , pp , cc ⟧ ⊢ ⟦ ⟦ voteDelegs , stakeDelegs , applyWithdrawals withdrawals rewards , depositsᵈ ⟧ , pState , ⟦ refreshedDReps , ccHotKeys , depositsᵍ ⟧ ⟧ ⇀⦇ DCertsOf txTop ,CERTS⦈ ⟦ ⟦ voteDelegs' , stakeDelegs' , rewards' , depositsᵈ' ⟧ , pState' , gState' ⟧
204209
205210
∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId

‎src/Ledger/Dijkstra/Specification/Entities/Properties/Computational.lagda.md‎

Lines changed: 15 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,7 @@ instance
103103
withdrawals = WithdrawalsOf txTop
104104
withdrawalsCredentials = mapˢ stake (dom withdrawals)
105105
accountBalanceIntervals = BalanceIntervalsOf txTop
106+
startingAccountBalanceIntervals = StartingBalanceIntervalsOf txTop
106107
directDeposits = DirectDepositsOf txTop
107108
directDepositsCredentials = mapˢ stake (dom directDeposits)
108109
@@ -132,18 +133,22 @@ instance
132133
∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ]
133134
(InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval)
134135
136+
∙ dom startingAccountBalanceIntervals ⊆ dom Γ.rewards₀
137+
∙ ∀[ (c , interval) ∈ startingAccountBalanceIntervals ˢ ]
138+
(InBalanceInterval (maybe id 0 (lookupᵐ? Γ.rewards₀ c)) interval)
139+
135140
∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
136141
¿ | Computational-CERTS.computeProof ⟦ Γ.epoch , Γ.pp , Γ.coldCredentials ⟧ s₁ (DCertsOf txTop)
137142
... | no ¬p | _ = failure ""
138143
... | yes _ | failure e = failure e
139-
... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇) | success (s₂ , p)
144+
... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉) | success (s₂ , p)
140145
with ¿
141146
∙ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿
142147
... | no ¬p = failure ""
143-
... | yes p₈ = success (-, (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p , p₇ , p₈)))
148+
... | yes p₁₀ = success (-, (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p , p₉ , p₁₀)))
144149
145150
completeness : ∀ (s' : CertState) → Γ ⊢ s₀ ⇀⦇ txTop ,ENTITIES⦈ s' → map proj₁ computeProof ≡ success s'
146-
completeness s' (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p , p₇ , p₈))
151+
completeness s' (ENTITIES (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p , p₉ , p₁₀))
147152
with ¿
148153
∙ ∀[ a ∈ dom withdrawals ] NetworkIdOf a ≡ NetworkId
149154
∙ withdrawalsCredentials ⊆ dom (RewardsOf s₀)
@@ -160,12 +165,16 @@ instance
160165
∙ ∀[ (c , interval) ∈ accountBalanceIntervals ˢ ]
161166
(InBalanceInterval (maybe id 0 (lookupᵐ? (RewardsOf s₀) c)) interval)
162167
168+
∙ dom startingAccountBalanceIntervals ⊆ dom Γ.rewards₀
169+
∙ ∀[ (c , interval) ∈ startingAccountBalanceIntervals ˢ ]
170+
(InBalanceInterval (maybe id 0 (lookupᵐ? Γ.rewards₀ c)) interval)
171+
163172
∙ ∀[ a ∈ dom directDeposits ] NetworkIdOf a ≡ NetworkId
164173
¿ | Computational-CERTS.computeProof ⟦ Γ.epoch , Γ.pp , Γ.coldCredentials ⟧ s₁ (DCertsOf txTop) | Computational-CERTS.completeness _ _ _ _ p
165-
... | no ¬p | _ | p' = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇))
174+
... | no ¬p | _ | p' = ⊥-elim (¬p (p₁ , p₂ , p₃ , p₄ , p₅ , p₆ , p₇ , p₈ , p₉))
166175
... | yes _ | failure e | ()
167-
... | yes (p₁ , p₂ , p₃ , p₄ , p₅ , p₆) | success (s₂ , p) | refl
176+
... | yes _ | success (s₂ , p) | refl
168177
with ¿ directDepositsCredentials ⊆ dom (RewardsOf s₂) ¿
169-
... | no ¬p = ⊥-elim (¬p p₈)
178+
... | no ¬p = ⊥-elim (¬p p₁₀)
170179
... | yes _ = refl
171180
```

‎src/Ledger/Dijkstra/Specification/Transaction.lagda.md‎

Lines changed: 19 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -236,6 +236,10 @@ Of particular note in the Dijkstra era are
236236
interval as a Phase-1 validity condition, analogous to how slot validity
237237
intervals constrain the time at which a transaction may be processed.
238238

239+
+ `txStartingBalanceIntervals`{.AgdaField}: only present in top-level transactions,
240+
this field records the account balance interval assertions that this transaction
241+
makes about account balances before any sub-transaction is processed.
242+
239243
```agda
240244
mutual
241245
record Tx (txLevel : TxLevel) : Type where
@@ -269,11 +273,12 @@ Of particular note in the Dijkstra era are
269273
scriptIntegrityHash : Maybe ScriptHash
270274
271275
-- New in Dijkstra --
272-
txSubTransactions : InTopLevel txLevel (List (Tx TxLevelSub))
273-
txGuards : ℙ Credential
274-
txRequiredTopLevelGuards : ℙ (Credential × Maybe Datum)
275-
txDirectDeposits : DirectDeposits
276-
txBalanceIntervals : AccountBalanceIntervals
276+
txSubTransactions : InTopLevel txLevel (List (Tx TxLevelSub))
277+
txGuards : ℙ Credential
278+
txRequiredTopLevelGuards : ℙ (Credential × Maybe Datum)
279+
txDirectDeposits : DirectDeposits
280+
txBalanceIntervals : AccountBalanceIntervals
281+
txStartingBalanceIntervals : InTopLevel txLevel AccountBalanceIntervals
277282
---------------------
278283
279284
requiredSignerHashes : ℙ KeyHash
@@ -420,6 +425,10 @@ could be either of them.
420425
field BalanceIntervalsOf : A → AccountBalanceIntervals
421426
open HasBalanceIntervals ⦃...⦄ public
422427
428+
record HasStartingBalanceIntervals {a} (A : Type a) : Type a where
429+
field StartingBalanceIntervalsOf : A → AccountBalanceIntervals
430+
open HasStartingBalanceIntervals ⦃...⦄ public
431+
423432
record HasIsValidFlag {a} (A : Type a) : Type a where
424433
field IsValidFlagOf : A → Bool
425434
open HasIsValidFlag ⦃...⦄ public
@@ -476,6 +485,11 @@ could be either of them.
476485
HasBalanceIntervals-Tx : HasBalanceIntervals (Tx txLevel)
477486
HasBalanceIntervals-Tx .BalanceIntervalsOf = BalanceIntervalsOf ∘ TxBodyOf
478487
488+
HasStartingBalanceIntervals-TxBody : HasStartingBalanceIntervals (TxBody TxLevelTop)
489+
HasStartingBalanceIntervals-TxBody .StartingBalanceIntervalsOf = TxBody.txStartingBalanceIntervals
490+
HasStartingBalanceIntervals-Tx : HasStartingBalanceIntervals TopLevelTx
491+
HasStartingBalanceIntervals-Tx .StartingBalanceIntervalsOf = StartingBalanceIntervalsOf ∘ TxBodyOf
492+
479493
HasValidInterval-TxBody : HasValidInterval (TxBody txLevel)
480494
HasValidInterval-TxBody .ValidIntervalOf = TxBody.txVldt
481495
HasValidInterval-Tx : HasValidInterval (Tx txLevel)

0 commit comments

Comments
 (0)