Ledger¶
This module defines the ledger transition system where valid transactions transform the ledger state.
LEDGER Transition System Types¶
record SubLedgerEnv : Type where field slot : Slot ppolicy : Maybe ScriptHash pparams : PParams enactState : EnactState treasury : Treasury utxo₀ : UTxO isTopLevelValid : Bool allScripts : ℙ Script allData : DataHash ⇀ Datum record LedgerEnv : Type where field slot : Slot ppolicy : Maybe ScriptHash pparams : PParams enactState : EnactState treasury : Treasury
record LState : Type where
field utxoSt : UTxOState govSt : GovState certState : CertState
Helper Functions¶
txgov : ∀ {ℓ} → TxBody ℓ → List (GovVote ⊎ GovProposal) txgov txb = map inj₂ txGovProposals ++ map inj₁ txGovVotes where open TxBody txb GovProposals+Votes : ∀ {ℓ} → Tx ℓ → List (GovVote ⊎ GovProposal) GovProposals+Votes tx = map inj₂ (ListOfGovProposalsOf tx) ++ map inj₁ (ListOfGovVotesOf tx) rmOrphanDRepVotes : CertState → GovState → GovState rmOrphanDRepVotes cs govSt = L.map (map₂ go) govSt where ifDRepRegistered : Credential → Type ifDRepRegistered c = c ∈ dom (DRepsOf cs) go : GovActionState → GovActionState go gas = record gas { votes = record (GovVotesOf gas) { gvDRep = filterKeys ifDRepRegistered (GovVotes.gvDRep (GovVotesOf gas)) } } allColdCreds : GovState → EnactState → ℙ Credential allColdCreds govSt es = ccCreds (es .cc) ∪ concatMapˢ (λ (_ , st) → proposedCC (GovActionOf st)) (fromList govSt) calculateDepositsChange : CertState → CertState → CertState → DepositsChange calculateDepositsChange certState₀ certState₁ certState₂ = $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5336}{\htmlId{4844}{\htmlClass{Function}{\text{coinChangeTop}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5279}{\htmlId{4860}{\htmlClass{Function}{\text{coinChangeSub}}}}\, \end{pmatrix}$ where coinFromDeposit : CertState → Coin coinFromDeposit certState = getCoin (DepositsOf (DStateOf certState)) + getCoin (DepositsOf (PStateOf certState)) + getCoin (DepositsOf (GStateOf certState)) coin₀ : Coin coin₀ = coinFromDeposit certState₀ coin₁ : Coin coin₁ = coinFromDeposit certState₁ coin₂ : Coin coin₂ = coinFromDeposit certState₂ coinChangeSub : ℤ coinChangeSub = coin₁ - coin₀ coinChangeTop : ℤ coinChangeTop = coin₂ - coin₁
LEDGER Transition System¶
New in Dijkstra¶
In Dijkstra we compute the set of "global" scripts and data once at the
top-level in the LEDGER{.AgdaDatatype} rule. This is threaded through
SUBLEDGER via
UTxOEnv{.AgdaDatatype}/SubUTxOEnv{.AgdaDatatype}.} to UTXOW{.AgdaDatatype}/SUBUTXOW{.AgdaDatatype
-
allScripts : ℙ Script is the union of all scripts relevant to the entire batch: scripts referenced/witnessed by the top-level transaction plus scripts referenced/witnessed by every subtransaction (computed by
getAllScripts). -
allData : DataHash ⇀ Datumis the collection of all data relevant to the entire batch: all datums appearing in witnesses and in any (sub)transaction context (computer by getAllData).
Design Rationale for Ledger Rule Premises¶
- Batch-scoped phase-2 context.
We compute allScripts and allData once, from the pre-batch UTxO snapshot
and the full batch (top-level transaction and all subtransactions). This ensures a
shared, batch-scoped pool of scripts and datums for phase-2 validation.
-
Subtransactions are conditional on top-level validity.
-
If
IsValidFlagOf txTop ≡ true, then each subtransaction parametrizes its ownUTXOW/CERTS/GOVSrelation and the resulting (codomain) states are carried forward (viaSUBLEDGERS). -
If
IsValidFlagOf txTop ≡ false, thenSUBLEDGERSis the identity relation (no subtransaction effects are applied). -
Connecting top-level CERTS and GOVS relations relative to UTXOW.
We check top-level CERTS and GOVS relations before
top-level UTXOW because:
CERTStracks deposit updates (now included inCertState),-
UTXOaccounting needs the net deposit change of the whole batch in theUTxOEnv(used innewDepositsBatch/depositRefundsBatchin theUtxo.Accountingmodule). -
CertState and GovState Dependencies.
-
Top-level
CERTSrelates the post-SUBLEDGERSCertState(which reflects subtransaction certificates) to the finalCertState. - Top-level
GOVSrelates the post-SUBLEDGERSGovState(which relfects proposals/votes of subtransactions) to the finalGovState, and is parameterized by the finalCertState(so it sees the final registered DRep set after certificates). -
Orphan DRep votes are removed using the final (post-
CERTS)CertState. -
allColdCredsuses the finalGovState
The CertEnv assumed in the CERTS relation includes
allColdCreds govState₁ enactState to so that CC hot key registration can account
for both enacted CC credentials and any newly proposed CC actions that appear in
the final (post-subtransaction processing) GovState.
data _⊢_⇀⦇_,SUBLEDGER⦈_ : SubLedgerEnv → LState → SubLevelTx → LState → Type where SUBLEDGER-V : ∙ isTopLevelValid ≡ true ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{9494}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{9501}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5965}{\htmlId{9506}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5488}{\htmlId{9517}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6012}{\htmlId{9525}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6055}{\htmlId{9543}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6102}{\htmlId{9556}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁ ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{9618}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{9624}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{9631}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#11630}{\htmlId{9636}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5723}{\htmlId{9653}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2976}{\htmlId{9659}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5723}{\htmlId{9673}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4535}{\htmlId{9679}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5627}{\htmlId{9692}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5916}{\htmlId{9702}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState₀ ⇀⦇ DCertsOf stx ,CERTS⦈ certState₁ ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#10359}{\htmlId{9773}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5723}{\htmlId{9780}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{9786}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{9792}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{9799}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5815}{\htmlId{9804}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5916}{\htmlId{9814}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5590}{\htmlId{9827}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{9840}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{9844}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3320}{\htmlId{9845}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5590}{\htmlId{9855}{\htmlClass{Generalizable}{\text{certState₁}}}}\,\,\htmlId{9865}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁ ──────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{9975}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5815}{\htmlId{9982}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{9992}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5916}{\htmlId{9997}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5965}{\htmlId{10010}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5488}{\htmlId{10021}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6012}{\htmlId{10029}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6055}{\htmlId{10047}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6102}{\htmlId{10060}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5531}{\htmlId{10074}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5627}{\htmlId{10087}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5579}{\htmlId{10099}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5542}{\htmlId{10133}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5638}{\htmlId{10146}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5590}{\htmlId{10158}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \end{pmatrix}$ SUBLEDGER-I : ∙ isTopLevelValid ≡ false ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{10230}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{10237}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5965}{\htmlId{10242}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5488}{\htmlId{10253}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6012}{\htmlId{10261}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6055}{\htmlId{10279}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6102}{\htmlId{10292}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀ ──────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{10395}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5815}{\htmlId{10402}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{10412}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5916}{\htmlId{10417}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5965}{\htmlId{10430}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5488}{\htmlId{10441}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6012}{\htmlId{10449}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6055}{\htmlId{10467}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#6102}{\htmlId{10480}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5531}{\htmlId{10494}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5627}{\htmlId{10507}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5579}{\htmlId{10519}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5531}{\htmlId{10553}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5627}{\htmlId{10566}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5579}{\htmlId{10578}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ _⊢_⇀⦇_,SUBLEDGERS⦈_ : SubLedgerEnv → LState → List SubLevelTx → LState → Type _⊢_⇀⦇_,SUBLEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,SUBLEDGER⦈_} data _⊢_⇀⦇_,LEDGER⦈_ : LedgerEnv → LState → TopLevelTx → LState → Type where LEDGER-V : let utxo₀ : UTxO utxo₀ = UTxOOf utxoState₀ allScripts : ℙ Script allScripts = getAllScripts tx utxo₀ allData : DataHash ⇀ Datum allData = setToMap (mapˢ < hash , id > (getAllData tx utxo₀)) depositsChange : DepositsChange depositsChange = calculateDepositsChange certState₀ certState₁ certState₂ in ∙ IsValidFlagOf tx ≡ true ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{11255}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5815}{\htmlId{11262}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{11272}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5916}{\htmlId{11277}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5965}{\htmlId{11290}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10848}{\htmlId{11301}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12448}{\htmlId{11309}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5674}{\htmlId{11323}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10906}{\htmlId{11328}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10983}{\htmlId{11341}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5531}{\htmlId{11355}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5627}{\htmlId{11368}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5579}{\htmlId{11380}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5542}{\htmlId{11432}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5638}{\htmlId{11445}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5590}{\htmlId{11457}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \end{pmatrix}$ ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{11480}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{11486}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{11493}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#11630}{\htmlId{11498}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5674}{\htmlId{11515}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2976}{\htmlId{11520}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5674}{\htmlId{11534}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4535}{\htmlId{11539}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5638}{\htmlId{11552}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5916}{\htmlId{11562}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState₁ ⇀⦇ DCertsOf tx ,CERTS⦈ certState₂ ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#10359}{\htmlId{11632}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5674}{\htmlId{11639}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{11644}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{11650}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{11657}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5815}{\htmlId{11662}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5916}{\htmlId{11672}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5601}{\htmlId{11685}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{11698}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{11702}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3320}{\htmlId{11703}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5601}{\htmlId{11713}{\htmlClass{Generalizable}{\text{certState₂}}}}\,\,\htmlId{11723}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂ ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{11791}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{11798}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5965}{\htmlId{11803}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10848}{\htmlId{11814}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#11091}{\htmlId{11822}{\htmlClass{Bound}{\text{depositsChange}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10906}{\htmlId{11839}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10983}{\htmlId{11852}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂ ──────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{11951}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5815}{\htmlId{11958}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{11968}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5916}{\htmlId{11973}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5965}{\htmlId{11986}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5531}{\htmlId{12001}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5627}{\htmlId{12014}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5579}{\htmlId{12026}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5553}{\htmlId{12056}{\htmlClass{Generalizable}{\text{utxoState₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4162}{\htmlId{12069}{\htmlClass{Function}{\text{rmOrphanDRepVotes}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5601}{\htmlId{12087}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5649}{\htmlId{12098}{\htmlClass{Generalizable}{\text{govState₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5601}{\htmlId{12110}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \end{pmatrix}$ LEDGER-I : let utxo₀ : UTxO utxo₀ = UTxOOf utxoState₀ allScripts : ℙ Script allScripts = getAllScripts tx utxo₀ allData : DataHash ⇀ Datum allData = setToMap (mapˢ < hash , id > (getAllData tx utxo₀)) in ∙ IsValidFlagOf tx ≡ false ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{12430}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5815}{\htmlId{12437}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{12447}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5916}{\htmlId{12452}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5965}{\htmlId{12465}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12147}{\htmlId{12476}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12448}{\htmlId{12484}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5674}{\htmlId{12498}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12205}{\htmlId{12503}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12282}{\htmlId{12516}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5531}{\htmlId{12530}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5627}{\htmlId{12543}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5579}{\htmlId{12555}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5531}{\htmlId{12607}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5627}{\htmlId{12620}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5579}{\htmlId{12632}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{12655}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{12662}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5965}{\htmlId{12667}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12147}{\htmlId{12678}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \begin{pmatrix} \,\href{Data.Integer.Base.html#1545}{\htmlId{12688}{\htmlClass{Function}{\text{0ℤ}}}}\, \\ \,\href{Data.Integer.Base.html#1545}{\htmlId{12693}{\htmlClass{Function}{\text{0ℤ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12205}{\htmlId{12700}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12282}{\htmlId{12713}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁ ──────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5772}{\htmlId{12812}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5815}{\htmlId{12819}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5870}{\htmlId{12829}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5916}{\htmlId{12834}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5965}{\htmlId{12847}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5531}{\htmlId{12862}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5627}{\htmlId{12875}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5579}{\htmlId{12887}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5542}{\htmlId{12917}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5627}{\htmlId{12930}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5579}{\htmlId{12942}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ _⊢_⇀⦇_,LEDGERS⦈_ : LedgerEnv → LState → List TopLevelTx → LState → Type _⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}