Formal Ledger Specification

Ledger.Core

Formal Ledger Specification

Home
Preliminaries
Preliminaries
Core
Core
- Introduction
- Modules/
  Modules/
  - Address
  - Crypto
  - Epoch
Conway
Conway
- Introduction
- Modules/
  Modules/
  - Abstract
  - BlockBody
  - BlockBody/
    BlockBody/
    
    Properties
    
    Properties/
    Properties/
    
    Computational
  - Certs
  - Certs/
    Certs/
    
    Properties
    
    Properties/
    Properties/
    
    Computational
    
    PoV
    
    PoVLemmas
    
    VoteDelegsVDeleg
  - Chain
  - Chain/
    Chain/
    
    Properties
    
    Properties/
    Properties/
    
    Computational
    
    CredDepsEqualDomRwds
    
    EpochStep
    
    GovDepsMatch
    
    PParamsWellFormed
  - Enact
  - Enact/
    Enact/
    
    Properties
    
    Properties/
    Properties/
    
    Computational
  - Epoch
  - Epoch/
    Epoch/
    
    Properties
    
    Properties/
    Properties/
    
    Computational
    
    ConstRwds
    
    ExpiredDReps
    
    GovDepsMatch
    
    NoPropSameDReps
  - Fees
  - Gov
  - Gov/
    Gov/
    
    Base
    
    Actions
    
    Properties
    
    Properties/
    Properties/
    
    Computational
    
    ChangePPGroup
  - Ledger
  - Ledger/
    Ledger/
    
    Properties
    
    Properties/
    Properties/
    
    Base
    
    Computational
    
    GovDepsMatch
    
    PoV
  - PoolReap
  - PoolReap/
    PoolReap/
    
    Properties/
    Properties/
    
    Computational
  - PParams
  - Properties
  - Ratify
  - Ratify/
    Ratify/
    
    Properties
    
    Properties/
    Properties/
    
    Computational
  - Rewards
  - Rewards/
    Rewards/
    
    Properties/
    Properties/
    
    Computational
  - RewardUpdate
  - RewardUpdate/
    RewardUpdate/
    
    Properties
    
    Properties/
    Properties/
    
    Computational
  - Script
  - Script/
    Script/
    
    Base
    
    ScriptPurpose
    
    Timelock
    
    Validation
  - TokenAlgebra/
    TokenAlgebra/
    
    Base
    
    Coin
    
    ValueSet
    
    ValueVector
  - Transaction
  - Utxo
  - Utxo/
    Utxo/
    
    Properties
    
    Properties/
    Properties/
    
    Base
    
    Computational
    
    GenMinspend
    
    MinSpend
    
    PoV
  - Utxow
  - Utxow/
    Utxow/
    
    Properties
    
    Properties/
    Properties/
    
    Computational
  - Types/
    Types/
    
    GovStructure
Dijkstra
Dijkstra
- Introduction
- Abstract
- Certs
- Gov/
  Gov/
  - Actions
  - Base
- PParams
- Script
- Script/
  Script/
  - Validation
- TokenAlgebra
- Transaction
Appendix
Appendix
- Background
  Background
  - Definitions
  - Essential Agda
  - Bootstrapping
    Bootstrapping
    
    Bootstrapping Governance
    
    Bootstrapping EnactState
- Era-independent Modules
  Era-independent Modules
  - Prelude
  - Ledger
  - Ledger.Core
  - Ledger.Prelude
  - Ledger.Prelude/
    Ledger.Prelude/
    
    Base
    
    Foreign/
    Foreign/
    
    HSTypes
    
    Util
    
    HasCoin
    
    Instances
    
    Numeric
    
    Numeric/
    Numeric/
    
    PositiveNat
    
    UnitInterval
  - Interface
    Interface
    
    STS
    
    ComputationalRelation
    
    TypeClasses
    
    TypeClasses/
    TypeClasses/
    
    TypeClasses
    
    HasSubset
    
    HasSubtract
    
    HasSubtract/
    HasSubtract/
    
    Instance
  - Foreign
    Foreign
    
    Convertible
    
    Convertible/
    Convertible/
    
    Deriving
    
    DerivingTest
    
    HaskellTypes
    
    HaskellTypes/
    HaskellTypes/
    
    Deriving
  - MyDebugOptions
  - Test/
    Test/
    
    Examples
    
    Examples/
    Examples/
    
    HelloWorld
    
    SucceedIfNumber
    
    AccountSim/
    AccountSim/
    
    Datum
    
    OffChain/
    OffChain/
    
    Cleanup
    
    Close
    
    Deposit
    
    Lib
    
    OffChain
    
    Open
    
    Start
    
    Transfer
    
    Withdraw
    
    Test/
    Test/
    
    Trace
    
    Validator
    
    DEx/
    DEx/
    
    Datum
    
    OffChain/
    OffChain/
    
    Close
    
    Exchange
    
    Lib
    
    OffChain
    
    Start
    
    Update
    
    Test/
    Test/
    
    Trace
    
    Validator
    
    MultiSig/
    MultiSig/
    
    Datum
    
    OffChain/
    OffChain/
    
    AddSig
    
    Lib
    
    OffChain
    
    Open
    
    Pay
    
    Propose
    
    Test/
    Test/
    
    Trace
    
    Validator
    
    MultiSigV2/
    MultiSigV2/
    
    Datum
    
    OffChain/
    OffChain/
    
    AddSig
    
    Cancel
    
    Cleanup
    
    Lib
    
    OffChain
    
    Open
    
    Pay
    
    Propose
    
    Test/
    Test/
    
    Trace
    
    Validator
    
    AbstractImplementation
    
    LedgerImplementation
    
    Lib
    
    Prelude
    
    SymbolicData
- Era-dependent Modules
  Era-dependent Modules
  - Dijkstra
    Dijkstra
    
    Ledger.Dijkstra
  - PreConway
    PreConway
    
    Ledger.PreConway
    
    Ledger.PreConway/
    Ledger.PreConway/
    
    Conformance
    Conformance
    
    NewPP
    
    NewPP/
    NewPP/
    
    Properties
    
    PPUp
    
    PPUp/
    PPUp/
    
    Properties
    
    NewPP
    
    NewPP/
    NewPP/
    
    Properties
    
    PPUp
    
    PPUp/
    PPUp/
    
    Properties
  - Conway
    Conway
    
    Ledger.Conway
    
    Foreign
    Foreign
    
    ExternalFunctions
    
    HSLedger
    
    HSLedger/
    HSLedger/
    
    Address
    
    BaseTypes
    
    Cert
    
    Certs
    
    Chain
    
    Core
    
    Enact
    
    Epoch
    
    ExternalStructures
    
    Gov
    
    Gov/
    Gov/
    
    Core
    
    Actions
    
    Ledger
    
    NewEpoch
    
    PParams
    
    Ratify
    
    Rewards
    
    Transaction
    
    Utxo
    
    Conformance
    
    Conformance/
    Conformance/
    
    Certs
    
    Certs/
    Certs/
    
    Properties
    
    Chain
    
    Chain/
    Chain/
    
    Properties
    
    Epoch
    
    Epoch/
    Epoch/
    
    Properties
    
    Equivalence
    
    Equivalence/
    Equivalence/
    
    Bisimilarity
    
    Certs
    
    Convert
    
    Deposits
    
    Map
    
    Utxo
    
    Gov
    
    Ledger
    
    Ledger/
    Ledger/
    
    Properties
    
    Properties
    
    Rewards
    
    Script
    
    Utxo
    
    Utxo/
    Utxo/
    
    Properties
    
    Utxow
    
    Utxow/
    Utxow/
    
    Properties

Ledger.Core

module Ledger.Core where

import Ledger.Core.Specification