Introduction

This is the formal specification of the Cardano ledger for the Dijkstra era. The Agda source code which formalizes the ledger specification in the Dijkstra era consists of the modules listed below.

{-# OPTIONS --safe #-}
module Ledger.Dijkstra.Specification where

Abstract Functions¶

import Ledger.Dijkstra.Specification.Abstract

Accounts¶

import Ledger.Dijkstra.Specification.Account

Addresses¶

import Ledger.Core.Specification.Address renaming (RewardAddress to RewardAddress)

Block Body¶

The Block Body Transition updates the block body state which comprises the ledger state and the map describing the produced blocks.

import Ledger.Dijkstra.Specification.BlockBody
import Ledger.Dijkstra.Specification.BlockBody.Properties

Certificates¶

import Ledger.Dijkstra.Specification.Certs
import Ledger.Dijkstra.Specification.Certs.Properties

Chain¶

import Ledger.Dijkstra.Specification.Chain
import Ledger.Dijkstra.Specification.Chain.Properties

Enactment¶

import Ledger.Dijkstra.Specification.Enact
import Ledger.Dijkstra.Specification.Enact.Properties

Epoch¶

import Ledger.Core.Specification.Epoch
import Ledger.Dijkstra.Specification.Epoch
import Ledger.Dijkstra.Specification.Epoch.Properties

Fees¶

import Ledger.Dijkstra.Specification.Fees

Governance¶

import Ledger.Dijkstra.Specification.Gov
import Ledger.Dijkstra.Specification.Gov.Base
import Ledger.Dijkstra.Specification.Gov.Actions
import Ledger.Dijkstra.Specification.Gov.Properties

Ledger¶

import Ledger.Dijkstra.Specification.Ledger
import Ledger.Dijkstra.Specification.Ledger.Properties

Pool Reaping Transition¶

import Ledger.Dijkstra.Specification.PoolReap
import Ledger.Dijkstra.Specification.PoolReap.Properties

Protocol Parameters¶

import Ledger.Dijkstra.Specification.PParams

Ratification¶

import Ledger.Dijkstra.Specification.Ratify
import Ledger.Dijkstra.Specification.Ratify.Properties

Rewards¶

import Ledger.Dijkstra.Specification.Rewards
import Ledger.Dijkstra.Specification.Rewards.Properties
import Ledger.Dijkstra.Specification.RewardUpdate
import Ledger.Dijkstra.Specification.RewardUpdate.Properties

Scripts¶

import Ledger.Dijkstra.Specification.Script
import Ledger.Dijkstra.Specification.Script.Base
import Ledger.Dijkstra.Specification.Script.ScriptPurpose
import Ledger.Dijkstra.Specification.Script.Validation

Token Algebras¶

import Ledger.Dijkstra.Specification.TokenAlgebra.Base

Transactions¶

import Ledger.Dijkstra.Specification.Transaction

Utxo¶

import Ledger.Dijkstra.Specification.Utxo
import Ledger.Dijkstra.Specification.Utxo.Properties

Utxow¶

import Ledger.Dijkstra.Specification.Utxow
import Ledger.Dijkstra.Specification.Utxow.Properties