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 Conway era consists of the modules listed below.

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

Addresses

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

Epoch

import Ledger.Core.Specification.Epoch

Certificates

import Ledger.Dijkstra.Specification.Certs

Governance

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

Protocol Parameters

import Ledger.Dijkstra.Specification.PParams

Scripts

import Ledger.Dijkstra.Specification.Script
import Ledger.Dijkstra.Specification.Script.Validation

Token Algebras

import Ledger.Dijkstra.Specification.TokenAlgebra.Base

Transactions

import Ledger.Dijkstra.Specification.Transaction