Skip to content

Ledger

This section is part of the Ledger.Conway.Specification.Ledger module of the formal ledger specification, where the entire state transformation of the ledger state caused by a valid transaction can now be given as a combination of the previously defined transition systems.

Conway specifics

As there is nothing new to the Conway era in this part of the ledger, we do not present any details of the Agda formalization.

{-# OPTIONS --safe #-}

import Data.List as L

open import Ledger.Prelude
open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction using (TransactionStructure)

module Ledger.Conway.Specification.Ledger
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Gov txs
open import Ledger.Conway.Specification.Utxo txs abs
open import Ledger.Conway.Specification.Utxow txs abs
open import Ledger.Conway.Specification.Certs govStructure

open Tx
open GState
open GovActionState
open EnactState using (cc)

Types and functions for the LEDGER transition system

record LEnv : Type where
  field
    slot        : Slot
    ppolicy     : Maybe ScriptHash
    pparams     : PParams
    enactState  : EnactState
    treasury    : Treasury

instance
  HasPParams-LEnv : HasPParams LEnv
  HasPParams-LEnv .PParamsOf = LEnv.pparams



record LState : Type where

  constructor ⟦_,_,_⟧ˡ

  field
    utxoSt     : UTxOState
    govSt      : GovState
    certState  : CertState

record HasLState {a} (A : Type a) : Type a where
  field LStateOf : A → LState
open HasLState ⦃...⦄ public

instance
  HasUTxOState-LState : HasUTxOState LState
  HasUTxOState-LState .UTxOStateOf = LState.utxoSt

  HasUTxO-LState : HasUTxO LState
  HasUTxO-LState .UTxOOf = UTxOOf ∘ UTxOStateOf

  HasGovState-LState : HasGovState LState
  HasGovState-LState .GovStateOf = LState.govSt

  HasCertState-LState : HasCertState LState
  HasCertState-LState .CertStateOf = LState.certState

  HasDeposits-LState : HasDeposits LState
  HasDeposits-LState .DepositsOf = DepositsOf ∘ UTxOStateOf

  HasPools-LState : HasPools LState
  HasPools-LState .PoolsOf = PoolsOf ∘ CertStateOf

  HasGState-LState : HasGState LState
  HasGState-LState .GStateOf = GStateOf ∘ CertStateOf

  HasDState-LState : HasDState LState
  HasDState-LState .DStateOf = DStateOf ∘ CertStateOf

  HasPState-LState : HasPState LState
  HasPState-LState .PStateOf = PStateOf ∘ CertStateOf

  HasVoteDelegs-LState : HasVoteDelegs LState
  HasVoteDelegs-LState .VoteDelegsOf = VoteDelegsOf ∘ DStateOf ∘ CertStateOf

  HasDonations-LState : HasDonations LState
  HasDonations-LState .DonationsOf = DonationsOf ∘ UTxOStateOf

open CertState
open DState

instance
  unquoteDecl HasCast-LEnv HasCast-LState = derive-HasCast
    ((quote LEnv , HasCast-LEnv) ∷ (quote LState , HasCast-LState) ∷ [])

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 : Voter → Type
   ifDRepRegistered (r , c) = r ≡ DRep → c ∈ dom (DRepsOf cs)

   go : GovActionState → GovActionState
   go gas = record gas { votes = filterKeys ifDRepRegistered (gas .votes) }

allColdCreds : GovState → EnactState → ℙ Credential
allColdCreds govSt es =
  ccCreds (es .cc) ∪ concatMapˢ (λ (_ , st) → proposedCC (GovActionOf st)) (fromList govSt)

private variable
  Γ : LEnv
  s s' s'' : LState
  utxoSt utxoSt' : UTxOState
  govSt govSt' : GovState
  certState certState' : CertState
  tx : Tx
  slot : Slot
  ppolicy : Maybe ScriptHash
  pp : PParams
  enactState : EnactState
  treasury : Treasury

LEDGER transition system

data _⊢_⇀⦇_,LEDGER⦈_ : LEnv → LState → Tx → LState → Type where

  LEDGER-V :
    let  txb         = tx .body

         open TxBody txb

    in
    ∙ isValid tx ≡ true
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4129}{\htmlId{4498}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4172}{\htmlId{4505}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4213}{\htmlId{4510}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$  ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
    ∙ $\begin{pmatrix} \,\href{Ledger.Core.Specification.Epoch.html#818}{\htmlId{4561}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#4129}{\htmlId{4567}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4172}{\htmlId{4574}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Transaction.html#5281}{\htmlId{4579}{\htmlClass{Function}{\text{txGovVotes}}}}\, \\ \,\href{Ledger.Conway.Specification.Transaction.html#5106}{\htmlId{4592}{\htmlClass{Function}{\text{txWithdrawals}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#3791}{\htmlId{4608}{\htmlClass{Function}{\text{allColdCreds}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#4058}{\htmlId{4621}{\htmlClass{Generalizable}{\text{govSt}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#4187}{\htmlId{4627}{\htmlClass{Generalizable}{\text{enactState}}}}\, \end{pmatrix}$ ⊢ certState ⇀⦇ txCerts ,CERTS⦈ certState'
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Transaction.html#4998}{\htmlId{4690}{\htmlClass{Function}{\text{txId}}}}\, \\ \,\href{Ledger.Core.Specification.Epoch.html#818}{\htmlId{4697}{\htmlClass{Function}{\text{epoch}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#4129}{\htmlId{4703}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4172}{\htmlId{4710}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4143}{\htmlId{4715}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4187}{\htmlId{4725}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4094}{\htmlId{4738}{\htmlClass{Generalizable}{\text{certState'}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{4751}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{4755}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2294}{\htmlId{4756}{\htmlClass{Field}{\text{RewardsOf}}}}\, \,\href{Ledger.Conway.Specification.Ledger.html#4084}{\htmlId{4766}{\htmlClass{Generalizable}{\text{certState}}}}\,\,\htmlId{4775}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ rmOrphanDRepVotes certState' govSt ⇀⦇ txgov txb ,GOVS⦈ govSt'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4129}{\htmlId{4890}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4143}{\htmlId{4897}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4172}{\htmlId{4907}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4187}{\htmlId{4912}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4213}{\htmlId{4925}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4029}{\htmlId{4940}{\htmlClass{Generalizable}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4058}{\htmlId{4949}{\htmlClass{Generalizable}{\text{govSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4084}{\htmlId{4957}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4036}{\htmlId{4986}{\htmlClass{Generalizable}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4064}{\htmlId{4996}{\htmlClass{Generalizable}{\text{govSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4094}{\htmlId{5005}{\htmlClass{Generalizable}{\text{certState'}}}}\, \end{pmatrix}$

  LEDGER-I :
    ∙ isValid tx ≡ false
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4129}{\htmlId{5065}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4172}{\htmlId{5072}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4213}{\htmlId{5077}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4129}{\htmlId{5166}{\htmlClass{Generalizable}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4143}{\htmlId{5173}{\htmlClass{Generalizable}{\text{ppolicy}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4172}{\htmlId{5183}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4187}{\htmlId{5188}{\htmlClass{Generalizable}{\text{enactState}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4213}{\htmlId{5201}{\htmlClass{Generalizable}{\text{treasury}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4029}{\htmlId{5216}{\htmlClass{Generalizable}{\text{utxoSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4058}{\htmlId{5225}{\htmlClass{Generalizable}{\text{govSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4084}{\htmlId{5233}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$ ⇀⦇ tx ,LEDGER⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ledger.html#4036}{\htmlId{5262}{\htmlClass{Generalizable}{\text{utxoSt'}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4058}{\htmlId{5272}{\htmlClass{Generalizable}{\text{govSt}}}}\, \\ \,\href{Ledger.Conway.Specification.Ledger.html#4084}{\htmlId{5280}{\htmlClass{Generalizable}{\text{certState}}}}\, \end{pmatrix}$

pattern LEDGER-V⋯ w x y z = LEDGER-V (w , x , y , z)
pattern LEDGER-I⋯ y z     = LEDGER-I (y , z)

LEDGERS transition system

_⊢_⇀⦇_,LEDGERS⦈_ : LEnv → LState → List Tx → LState → Type
_⊢_⇀⦇_,LEDGERS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,LEDGER⦈_}