Introduction

This is the formal specification of the Cardano ledger for the Conway era.

The Agda source code which formalizes the ledger specification in the Conway era consists of the modules listed below. How these modules fit together to form a collection of interdependent state transition systems is illustrated by the STS Diagram in the Introduction section.

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

BlockBody¶

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

import Ledger.Conway.Specification.BlockBody
import Ledger.Conway.Specification.BlockBody.Properties

Certificates¶

import Ledger.Conway.Specification.Certs
import Ledger.Conway.Specification.Certs.Properties

Chain¶

import Ledger.Conway.Specification.Chain
import Ledger.Conway.Specification.Chain.Properties

Enactment¶

These modules concern the enactment of governance proposals and actions.

import Ledger.Conway.Specification.Enact
import Ledger.Conway.Specification.Enact.Properties

Epoch¶

import Ledger.Conway.Specification.Epoch
import Ledger.Conway.Specification.Epoch.Properties

Fees¶

This module defines a function that calculates the fee for reference scripts in a transaction.

import Ledger.Conway.Specification.Fees

Governance¶

import Ledger.Conway.Specification.Gov
import Ledger.Conway.Specification.Gov.Actions
import Ledger.Conway.Specification.Gov.Properties
import Ledger.Conway.Specification.Gov.Properties.ChangePPGroup
import Ledger.Conway.Specification.Types.GovStructure

Ledger¶

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

import Ledger.Conway.Specification.Ledger
import Ledger.Conway.Specification.Ledger.Properties

Protocol Parameters¶

The defines the adjustable protocol parameters of the Cardano ledger.

import Ledger.Conway.Specification.PParams

Properties of the Ledger Specification¶

import Ledger.Conway.Specification.Properties

Ratification¶

import Ledger.Conway.Specification.Ratify
import Ledger.Conway.Specification.Ratify.Properties

Rewards¶

import Ledger.Conway.Specification.Rewards
import Ledger.Conway.Specification.RewardUpdate
import Ledger.Conway.Specification.RewardUpdate.Properties

Scripts¶

import Ledger.Conway.Specification.Script
import Ledger.Conway.Specification.Script.Validation

Token Algebras¶

import Ledger.Conway.Specification.TokenAlgebra.Base
import Ledger.Conway.Specification.TokenAlgebra.Coin
import Ledger.Conway.Specification.TokenAlgebra.ValueSet
import Ledger.Conway.Specification.TokenAlgebra.ValueVector

Transactions¶

import Ledger.Conway.Specification.Transaction

Utxo¶

import Ledger.Conway.Specification.Utxo
import Ledger.Conway.Specification.Utxo.Properties

Utxow¶

import Ledger.Conway.Specification.Utxow
import Ledger.Conway.Specification.Utxow.Properties