Ledger¶
This module defines the ledger transition system where valid transactions transform the ledger state.
LEDGER Transition System Types¶
record LEnv : 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 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 (gas .votes) { gvDRep = filterKeys ifDRepRegistered (gas .votes .gvDRep) } } allColdCreds : GovState → EnactState → ℙ Credential allColdCreds govSt es = ccCreds (es .cc) ∪ concatMapˢ (λ (_ , st) → proposedCC (GovActionOf st)) (fromList govSt)
LEDGER Transition System¶
data _⊢_⇀⦇_,LEDGER⦈_ : LEnv → LState → Tx → LState → Type where LEDGER-V : let txb = tx .body
in ∙ isValid tx ≡ true ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4071}{\htmlId{4402}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4114}{\htmlId{4409}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4155}{\htmlId{4414}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt' ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#903}{\htmlId{4467}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#4071}{\htmlId{4473}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4114}{\htmlId{4480}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Transaction.html#5375}{\htmlId{4485}{\htmlClass{Function}{\text{txGovVotes}}}}\, \\ \,\href{Ledger.Conway.Specification.Transaction.html#5200}{\htmlId{4498}{\htmlClass{Function}{\text{txWithdrawals}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#3671}{\htmlId{4514}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#4000}{\htmlId{4527}{\htmlClass{Generalizable}{\text{govSt}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#4129}{\htmlId{4533}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState ⇀⦇ txCerts ,CERTS⦈ certState' ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Transaction.html#5092}{\htmlId{4598}{\htmlClass{Function}{\text{txId}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#903}{\htmlId{4605}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#4071}{\htmlId{4611}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4114}{\htmlId{4618}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4085}{\htmlId{4623}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4129}{\htmlId{4633}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4036}{\htmlId{4646}{\htmlClass{Generalizable}{\text{certState'}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{4659}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{4663}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2421}{\htmlId{4664}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#4026}{\htmlId{4674}{\htmlClass{Generalizable}{\text{certState}}}}\,\,\htmlId{4683}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ rmOrphanDRepVotes certState' govSt ⇀⦇ txgov txb ,GOVS⦈ govSt' ──────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4071}{\htmlId{4798}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4085}{\htmlId{4805}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4114}{\htmlId{4815}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4129}{\htmlId{4820}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4155}{\htmlId{4833}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#3971}{\htmlId{4848}{\htmlClass{Generalizable}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4000}{\htmlId{4857}{\htmlClass{Generalizable}{\text{govSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4026}{\htmlId{4865}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#3978}{\htmlId{4894}{\htmlClass{Generalizable}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4006}{\htmlId{4904}{\htmlClass{Generalizable}{\text{govSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4036}{\htmlId{4913}{\htmlClass{Generalizable}{\text{certState'}}}}\, \end{pmatrix}$ LEDGER-I : ∙ isValid tx ≡ false ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4071}{\htmlId{4977}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4114}{\htmlId{4984}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4155}{\htmlId{4989}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt' ──────────────────────────────── $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4071}{\htmlId{5078}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4085}{\htmlId{5085}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4114}{\htmlId{5095}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4129}{\htmlId{5100}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4155}{\htmlId{5113}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#3971}{\htmlId{5128}{\htmlClass{Generalizable}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4000}{\htmlId{5137}{\htmlClass{Generalizable}{\text{govSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4026}{\htmlId{5145}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#3978}{\htmlId{5174}{\htmlClass{Generalizable}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4000}{\htmlId{5184}{\htmlClass{Generalizable}{\text{govSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4026}{\htmlId{5192}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$
The rule LEDGER
invokes the GOVS
rule to
process governance action proposals and votes.
Note
The governance state used as input to GOVS
is filtered to
remove votes from DRep
s that are no longer
registered (see function rmOrphanDRepVotes
).
This mechanism serves to prevent attacks where malicious adversaries could submit transactions that:
- register a fraudulent
DRep
- cast numerous votes utilizing that
DRep
- deregisters the
DRep
, thereby recovering the deposit
LEDGERS Transition System¶
_⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type _⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}