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 → ℤ calculateDepositsChange certState certState' = finalCoin - initialCoin where initialCoin : ℕ initialCoin = getCoin (DepositsOf (DStateOf certState)) + getCoin (DepositsOf (PStateOf certState)) + getCoin (DepositsOf (GStateOf certState)) finalCoin : ℕ finalCoin = getCoin (DepositsOf (DStateOf certState')) + getCoin (DepositsOf (PStateOf certState')) + getCoin (DepositsOf (GStateOf certState'))
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#5624}{\htmlId{9346}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{9353}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5817}{\htmlId{9358}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5340}{\htmlId{9369}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5864}{\htmlId{9377}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5907}{\htmlId{9395}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5954}{\htmlId{9408}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₁ ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{9470}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{9476}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{9483}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#11540}{\htmlId{9488}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5575}{\htmlId{9505}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2976}{\htmlId{9511}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5575}{\htmlId{9525}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4535}{\htmlId{9531}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5479}{\htmlId{9544}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5768}{\htmlId{9554}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState₀ ⇀⦇ DCertsOf stx ,CERTS⦈ certState₁ ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#10269}{\htmlId{9625}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5575}{\htmlId{9632}{\htmlClass{Generalizable}{\text{stx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{9638}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{9644}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{9651}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5667}{\htmlId{9656}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5768}{\htmlId{9666}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5442}{\htmlId{9679}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{9692}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{9696}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3320}{\htmlId{9697}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5442}{\htmlId{9707}{\htmlClass{Generalizable}{\text{certState₁}}}}\,\,\htmlId{9717}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ govState₀ ⇀⦇ GovProposals+Votes stx ,GOVS⦈ govState₁ ──────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{9827}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5667}{\htmlId{9834}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{9844}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5768}{\htmlId{9849}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5817}{\htmlId{9862}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5340}{\htmlId{9873}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5864}{\htmlId{9881}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5907}{\htmlId{9899}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5954}{\htmlId{9912}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5383}{\htmlId{9926}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5479}{\htmlId{9939}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5431}{\htmlId{9951}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5394}{\htmlId{9985}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5490}{\htmlId{9998}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5442}{\htmlId{10010}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \end{pmatrix}$ SUBLEDGER-I : ∙ isTopLevelValid ≡ false ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{10082}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{10089}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5817}{\htmlId{10094}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5340}{\htmlId{10105}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5864}{\htmlId{10113}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5907}{\htmlId{10131}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5954}{\htmlId{10144}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ stx ,SUBUTXOW⦈ utxoState₀ ──────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{10247}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5667}{\htmlId{10254}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{10264}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5768}{\htmlId{10269}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5817}{\htmlId{10282}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5340}{\htmlId{10293}{\htmlClass{Generalizable}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5864}{\htmlId{10301}{\htmlClass{Generalizable}{\text{isTopLevelValid}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5907}{\htmlId{10319}{\htmlClass{Generalizable}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5954}{\htmlId{10332}{\htmlClass{Generalizable}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5383}{\htmlId{10346}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5479}{\htmlId{10359}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5431}{\htmlId{10371}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ stx ,SUBLEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5383}{\htmlId{10405}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5479}{\htmlId{10418}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5431}{\htmlId{10430}{\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 = calculateDepositsChange certState₀ certState₂ in ∙ IsValidFlagOf tx ≡ true ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{11083}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5667}{\htmlId{11090}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{11100}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5768}{\htmlId{11105}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5817}{\htmlId{11118}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10700}{\htmlId{11129}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12342}{\htmlId{11137}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5526}{\htmlId{11151}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10758}{\htmlId{11156}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10835}{\htmlId{11169}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5383}{\htmlId{11183}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5479}{\htmlId{11196}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5431}{\htmlId{11208}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5394}{\htmlId{11260}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5490}{\htmlId{11273}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5442}{\htmlId{11285}{\htmlClass{Generalizable}{\text{certState₁}}}}\, \end{pmatrix}$ ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{11308}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{11314}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{11321}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#11540}{\htmlId{11326}{\htmlClass{Field}{\text{ListOfGovVotesOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5526}{\htmlId{11343}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Address.html#2976}{\htmlId{11348}{\htmlClass{Field}{\text{WithdrawalsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5526}{\htmlId{11362}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4535}{\htmlId{11367}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5490}{\htmlId{11380}{\htmlClass{Generalizable}{\text{govState₁}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5768}{\htmlId{11390}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState₁ ⇀⦇ DCertsOf tx ,CERTS⦈ certState₂ ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Transaction.html#10269}{\htmlId{11460}{\htmlClass{Field}{\text{TxIdOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5526}{\htmlId{11467}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#954}{\htmlId{11472}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{11478}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{11485}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5667}{\htmlId{11490}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5768}{\htmlId{11500}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5453}{\htmlId{11513}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{11526}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{11530}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#3320}{\htmlId{11531}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5453}{\htmlId{11541}{\htmlClass{Generalizable}{\text{certState₂}}}}\,\,\htmlId{11551}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ govState₁ ⇀⦇ GovProposals+Votes tx ,GOVS⦈ govState₂ ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{11619}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{11626}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5817}{\htmlId{11631}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10700}{\htmlId{11642}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10943}{\htmlId{11650}{\htmlClass{Bound}{\text{depositsChange}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10758}{\htmlId{11667}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#10835}{\htmlId{11680}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₁ ⇀⦇ tx ,UTXOW⦈ utxoState₂ ──────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{11779}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5667}{\htmlId{11786}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{11796}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5768}{\htmlId{11801}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5817}{\htmlId{11814}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5383}{\htmlId{11829}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5479}{\htmlId{11842}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5431}{\htmlId{11854}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5405}{\htmlId{11884}{\htmlClass{Generalizable}{\text{utxoState₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#4162}{\htmlId{11897}{\htmlClass{Function}{\text{rmOrphanDRepVotes}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5453}{\htmlId{11915}{\htmlClass{Generalizable}{\text{certState₂}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5501}{\htmlId{11926}{\htmlClass{Generalizable}{\text{govState₂}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5453}{\htmlId{11938}{\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#5624}{\htmlId{12258}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5667}{\htmlId{12265}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{12275}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5768}{\htmlId{12280}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5817}{\htmlId{12293}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#11975}{\htmlId{12304}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Transaction.html#12342}{\htmlId{12312}{\htmlClass{Field}{\text{IsValidFlagOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledger.html#5526}{\htmlId{12326}{\htmlClass{Generalizable}{\text{tx}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12033}{\htmlId{12331}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12110}{\htmlId{12344}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5383}{\htmlId{12358}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5479}{\htmlId{12371}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5431}{\htmlId{12383}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ SubTransactionsOf tx ,SUBLEDGERS⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5383}{\htmlId{12435}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5479}{\htmlId{12448}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5431}{\htmlId{12460}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{12483}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{12490}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5817}{\htmlId{12495}{\htmlClass{Generalizable}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#11975}{\htmlId{12506}{\htmlClass{Bound}{\text{utxo₀}}}}\, \\ \,\href{Data.Integer.Base.html#1545}{\htmlId{12514}{\htmlClass{Function}{\text{0ℤ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12033}{\htmlId{12519}{\htmlClass{Bound}{\text{allScripts}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#12110}{\htmlId{12532}{\htmlClass{Bound}{\text{allData}}}}\, \end{pmatrix}$ ⊢ utxoState₀ ⇀⦇ tx ,UTXOW⦈ utxoState₁ ──────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5624}{\htmlId{12631}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5667}{\htmlId{12638}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5722}{\htmlId{12648}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5768}{\htmlId{12653}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5817}{\htmlId{12666}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5383}{\htmlId{12681}{\htmlClass{Generalizable}{\text{utxoState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5479}{\htmlId{12694}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5431}{\htmlId{12706}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledger.html#5394}{\htmlId{12736}{\htmlClass{Generalizable}{\text{utxoState₁}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5479}{\htmlId{12749}{\htmlClass{Generalizable}{\text{govState₀}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledger.html#5431}{\htmlId{12761}{\htmlClass{Generalizable}{\text{certState₀}}}}\, \end{pmatrix}$ _⊢_⇀⦇_,LEDGERS⦈_ : LedgerEnv → LState → List TopLevelTx → LState → Type _⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}