Skip to content

Ledger

This module defines the ledger transition system where valid transactions transform the ledger state.

{-# 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)

LEDGER Transition System Types

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

  HasFees-LState : HasFees LState
  HasFees-LState .FeesOf = FeesOf  UTxOStateOf

  HasCCHotKeys-LState : HasCCHotKeys LState
  HasCCHotKeys-LState .CCHotKeysOf = CCHotKeysOf  GStateOf

  HasDReps-LState : HasDReps LState
  HasDReps-LState .DRepsOf = DRepsOf  CertStateOf

open CertState
open DState
open GovVotes

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

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

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
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#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 DReps that are no longer registered (see function rmOrphanDRepVotes).

This mechanism serves to prevent attacks where malicious adversaries could submit transactions that:

  1. register a fraudulent DRep
  2. cast numerous votes utilizing that DRep
  3. deregisters the DRep, thereby recovering the deposit
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⦈_}