Ledgers

This module defines the ledgers transition system where a list of valid transactions transform the ledger state.

{-# OPTIONS --safe #-}

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

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

open import Ledger.Dijkstra.Specification.Ledger txs abs
open import Ledger.Dijkstra.Specification.Utxo txs abs

Auxiliary Types

Dijkstra era introduces a new STS, LEDGERSWithLimits. This STS enforces limits on the size of reference scripts and execution units while applying LEDGER to individual transactions.

record LedgersEnv : Type where
  field
    ledgerEnv           : LedgerEnv
    refScriptsSizeLimit : ℕ
    exUnitsLimit        : ExUnits

record LedgersWithLimitsState : Type where
  field
    ledgerState       : LedgerState
    refScriptsSizeAcc : ℕ
    exUnitsAcc        : ExUnits

private
  variable
    Γ : LedgerEnv
    Γs : LedgersEnv
    s : LedgersWithLimitsState
    ls ls' ls'' : LedgerState
    topTx : TopLevelTx
    topTxs : List TopLevelTx
    accRefScriptSize accRefScriptSize' refScriptsSizeLimit : ℕ
    accExUnits accExUnits' exUnitsLimit : ExUnits

open PParams using (maxRefScriptSizePerBlock; maxBlockExUnits)

unquoteDecl HasCast-LedgersEnv HasCast-LedgersWithLimitsState = derive-HasCast
  ( (quote LedgersEnv , HasCast-LedgersEnv)
  ∷ (quote LedgersWithLimitsState , HasCast-LedgersWithLimitsState)
  ∷ [])

LEDGERSWithLimits Transition System

data _⊢_⇀⦇_,LEDGERSWithLimits⦈_ : LedgersEnv → LedgersWithLimitsState → List TopLevelTx → LedgersWithLimitsState → Type where
  LEDGERSWithLimits-[] : Γs ⊢ s ⇀⦇ [] ,LEDGERSWithLimits⦈ s
  LEDGERSWithLimits-∷  :
    let
      refScriptsSize = totalRefScriptsSize (UTxOOf ls) topTx
      exUnits        = totalExUnits topTx 
    in
    ∙ Γ ⊢ ls ⇀⦇ topTx  ,LEDGER⦈ ls'
    ∙ accRefScriptSize + refScriptsSize ≤ refScriptsSizeLimit
    ∙ accExUnits + exUnits ≤ᵉᵘ exUnitsLimit
    ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1284}{\htmlId{2379}{\htmlClass{Generalizable}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1470}{\htmlId{2383}{\htmlClass{Generalizable}{\text{refScriptsSizeLimit}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1521}{\htmlId{2405}{\htmlClass{Generalizable}{\text{exUnitsLimit}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1356}{\htmlId{2424}{\htmlClass{Generalizable}{\text{ls'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1435}{\htmlId{2430}{\htmlClass{Generalizable}{\text{accRefScriptSize}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{2447}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledgers.html#2124}{\htmlId{2449}{\htmlClass{Bound}{\text{refScriptsSize}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1498}{\htmlId{2466}{\htmlClass{Generalizable}{\text{accExUnits}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{2477}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Ledgers.html#2185}{\htmlId{2479}{\htmlClass{Bound}{\text{exUnits}}}}\, \end{pmatrix}$ ⇀⦇ topTxs ,LEDGERSWithLimits⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1360}{\htmlId{2521}{\htmlClass{Generalizable}{\text{ls''}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1452}{\htmlId{2528}{\htmlClass{Generalizable}{\text{accRefScriptSize'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1509}{\htmlId{2548}{\htmlClass{Generalizable}{\text{accExUnits'}}}}\, \end{pmatrix}$
    ────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1284}{\htmlId{2605}{\htmlClass{Generalizable}{\text{Γ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1470}{\htmlId{2609}{\htmlClass{Generalizable}{\text{refScriptsSizeLimit}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1521}{\htmlId{2631}{\htmlClass{Generalizable}{\text{exUnitsLimit}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1353}{\htmlId{2650}{\htmlClass{Generalizable}{\text{ls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1435}{\htmlId{2655}{\htmlClass{Generalizable}{\text{accRefScriptSize}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1498}{\htmlId{2674}{\htmlClass{Generalizable}{\text{accExUnits}}}}\, \end{pmatrix}$ ⇀⦇ topTx ∷ topTxs ,LEDGERSWithLimits⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1360}{\htmlId{2727}{\htmlClass{Generalizable}{\text{ls''}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1452}{\htmlId{2734}{\htmlClass{Generalizable}{\text{accRefScriptSize'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#1509}{\htmlId{2754}{\htmlClass{Generalizable}{\text{accExUnits'}}}}\, \end{pmatrix}$

LEDGERS Transition System

_⊢_⇀⦇_,LEDGERS⦈_ : LedgersEnv → LedgerState → List TopLevelTx → LedgerState → Type
Γ ⊢ ls ⇀⦇ topTxs ,LEDGERS⦈ ls' =
  ∃₂ λ (accRefScriptSize : ℕ) (accExUnits : ExUnits) → Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.html#2932}{\htmlId{3022}{\htmlClass{Bound}{\text{ls}}}}\, \\ \,\htmlId{3027}{\htmlClass{Number}{\text{0}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Script.Base.html#2360}{\htmlId{3031}{\htmlClass{Function}{\text{0ᵉᵘ}}}}\, \end{pmatrix}$ ⇀⦇ topTxs ,LEDGERSWithLimits⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ledgers.html#2955}{\htmlId{3069}{\htmlClass{Bound}{\text{ls'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#2969}{\htmlId{3075}{\htmlClass{Bound}{\text{accRefScriptSize}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ledgers.html#2992}{\htmlId{3094}{\htmlClass{Bound}{\text{accExUnits}}}}\, \end{pmatrix}$