Skip to content

Properties

Properties

This section presents the properties of the ledger that we have formally proved in Agda or plan to do so in the near future. We indicate in which Agda module each property is formally stated and (possibly) proved. A "Claim" is a property that is not yet proved, while a "Theorem" is one for which we have a formal proof.

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction

module Ledger.Conway.Specification.Properties
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where
open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Chain txs abs
open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Epoch txs abs
open import Ledger.Conway.Specification.Ledger txs abs
open import Ledger.Prelude

Preservation of Value

A key property of the ledger is that the total amount of coin in the system remains constant as transactions are processed. This is known as "preservation of value" (PoV).

There are several "preservation of value" proofs throughout this formal specificaition. These can be found in the following modules:

  • Theorem LEDGER-PoV. The LEDGER rule preserves value.

  • Lemma UTXO-PoV. The UTXO rule preserves value.

  • Lemma CERTS-PoV. The CERTS rule preserves value.

  • Lemma CERT-PoV. The CERT rule preserves value.

Invariance Properties

To say that a predicate P is an invariant of a transition rule R means the following: if the rule R relates states s and s' and if P holds at state s, then P holds at state s'.

Here are two examples of invariance properties.

  • Claim [CredDepsEqualDomRwds][]. Equality of credential deposits is a CHAIN invariant.

  • Claim CHAIN-PParamsWellFormed-inv. Well-formedness of PParams is a CHAIN invariant.

Matching Governance Action Deposits

Given a ledger state s, we focus on deposits in the UTxOState of s that are GovActionDeposits and we compare that set of deposits with the GovActionDeposits of the GovState of s. When these two sets are the same, we write govDepsMatch s and say the govDepsMatch relation holds for s. The formal definition of govDepsMatch is given in Ledger.Properties.

The properties [ChainGovDepsMatch][], [LedgerGovDepsMatch][] and [EpochGovDepsMatch][] assert that govDepsMatch is an invariant of the CHAIN, LEDGER, and EPOCH rules, respectively.

That is, if govDepsMatch s and if s ⇀⦇ tx ,CHAIN⦈ s', then govDepsMatch s'.

To be clear, the assertion that "the govDepsMatch relation is an invariant of the LEDGER rule" means the following: if govDepsMatch s and s ⇀⦇ tx ,LEDGER⦈ s', then govDepsMatch s'.

Minimum Spending Condition

Theorem UTXO-minspend. Let s and s' be UTxO states. If s ⇀⦇ tx ,UTXO⦈ s' and if there are no refunds from deregistrations, then the coin consumed by tx is at least the sum of the governance action deposits of the proposals in tx.

Other Miscellaneous Properties

Let p : GovProposal be a governance proposal and suppose the GovActionType of p .action is ChangePParams. Moreover, suppose pu is the data field of p. Then the set updateGroups pu is nonempty.

Let cs and cs' be ChainStates and b a Block. If cs ⇀⦇ b ,CHAIN⦈ cs' and if the enact states of cs and cs' differ, then the epoch of the slot of b is the successor of the last epoch of cs.

That is, if es and es' are two NewEpochStates such that es ⇀⦇ e ,NEWEPOCH⦈ es', then the rewards of es and es' are equal.

  • Claim Epoch-NoPropSameDReps. The set of active DReps remains unchanged if there are no governance proposals.

That is, if es is a NewEpochState, and if the GovState of es contains no governance proposals, then the set of activeDReps of es in Epoch e is equal to the set of activeDReps of es in the next epoch.

Suppose we have a collection C of credentials—for instance, given d : DState, take C to be the domain of the voteDelegs field of d. Then the set of VDelegs that results from applying vDelegCredential to the domain of the voteDelegs of d contains the range of the voteDelegs of d.

Transaction Validity

This section defines some of the types and functions we use to check the validity of transactions and blocks of the Cardano blockchain.

Transaction validity is complicated. In the truest sense, a transaction is valid if it is part of a valid block; i.e., validTxIn₁ s tx, where s is a chain state and tx is the transaction in question. However, a transaction can also be seen as valid if it could be applied at a certain slot (with no knowledge of an actual block). This is closer to how the mempool sees transaction validity and is expressed by validTxIn₂.

Note that these two are not equivalent and in fact there is no implication between the two in either direction. Indeed, validTxIn₂ => validTxIn₁ would require one to come up with a block, which we can't, while validTxIn₁ => validTxIn₂ may fail since the transaction might depend on a previous transaction in the same block.1

isCredDeposit : DepositPurpose → Type
isCredDeposit (CredentialDeposit x) = ⊤
isCredDeposit _ = ⊥

instance
  isCredDeposit? : isCredDeposit ⁇¹
  isCredDeposit? {CredentialDeposit x} = ⁇ (yes tt)
  isCredDeposit? {PoolDeposit x} = ⁇ (no λ ())
  isCredDeposit? {DRepDeposit x} = ⁇ (no λ ())
  isCredDeposit? {GovActionDeposit x} = ⁇ (no λ ())

isGADeposit : DepositPurpose → Type
isGADeposit (GovActionDeposit x) = ⊤
isGADeposit _ = ⊥

instance
  isGADeposit? : isGADeposit ⁇¹
  isGADeposit? {CredentialDeposit x} = ⁇ (no λ ())
  isGADeposit? {PoolDeposit x} = ⁇ (no λ ())
  isGADeposit? {DRepDeposit x} = ⁇ (no λ ())
  isGADeposit? {GovActionDeposit x} = ⁇ (yes tt)

instance
  _ : IsSet Block Tx
  _ = record { toSet = fromList ∘ Block.ts }

  _ : IsSet TxBody GovProposal
  _ = record { toSet = fromList ∘ TxBody.txGovProposals }

validBlockIn : ChainState → Block → Type
validBlockIn s b = ∃[ s' ] _ ⊢ s ⇀⦇ b ,CHAIN⦈ s'

validBlock : Block → Type
validBlock b = ∃[ s ] validBlockIn s b

validTxIn₁ : ChainState → Tx → Type
validTxIn₁ s tx = ∃[ b ] tx ∈ b × validBlockIn s b

module _ (s : ChainState) (slot : Slot) where
  open ChainState s; open NewEpochState newEpochState
  open EpochState epochState; open EnactState es

  private
    ledgerEnv = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Properties.html#9130}{\htmlId{9297}{\htmlClass{Bound}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#1739}{\htmlId{9304}{\htmlClass{Function}{\text{constitution}}}}\, \,\htmlId{9317}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{9318}{\htmlClass{Field}{\text{proj₁}}}}\, \,\htmlId{9324}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#650}{\htmlId{9325}{\htmlClass{Field}{\text{proj₂}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#1844}{\htmlId{9333}{\htmlClass{Function}{\text{pparams}}}}\, \,\htmlId{9341}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{9342}{\htmlClass{Field}{\text{proj₁}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#2378}{\htmlId{9350}{\htmlClass{Function}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.PParams.html#3084}{\htmlId{9355}{\htmlClass{Field}{\text{Acnt.treasury}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#2305}{\htmlId{9369}{\htmlClass{Function}{\text{acnt}}}}\, \end{pmatrix}$

  validTxIn₂ : Tx → Type
  validTxIn₂ tx = ∃[ ls' ] ledgerEnv ⊢ ls ⇀⦇ tx ,LEDGER⦈ ls'

validTx₁ : Tx → Type
validTx₁ tx = ∃[ s ] validTxIn₁ s tx

  1. This could indicate that validTxIn₂ should be changed so that it allows for applying a list of transactions before the final transaction; the downside would then be that the transaction isn't applied to the given state but to some intermediate one. We expect to have more insight into this matter once we have proved more theorems. ↩