Properties

This section is part of the Ledger.Conway.Specification.Properties module of the formal ledger specification in which we define some types and functions used to check the validity of transactions and blocks of the Cardano blockchain.

{-# 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

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.¹

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)

activeDReps : Epoch → NewEpochState → ℙ Credential
activeDReps currentEpoch s = dom (filterᵐ (λ (_ , e) → currentEpoch ≤ e) (DRepsOf s))

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

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

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#3332}{\htmlId{3502}{\htmlClass{Bound}{\text{slot}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2077}{\htmlId{3509}{\htmlClass{Function}{\text{constitution}}}}\, \,\htmlId{3522}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{3523}{\htmlClass{Field}{\text{proj₁}}}}\, \,\htmlId{3529}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#650}{\htmlId{3530}{\htmlClass{Field}{\text{proj₂}}}}\, \\ \,\href{Ledger.Conway.Specification.Enact.html#2182}{\htmlId{3538}{\htmlClass{Function}{\text{pparams}}}}\, \,\htmlId{3546}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{3547}{\htmlClass{Field}{\text{proj₁}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#2207}{\htmlId{3555}{\htmlClass{Function}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.PParams.html#1725}{\htmlId{3560}{\htmlClass{Field}{\text{Acnt.treasury}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#2134}{\htmlId{3574}{\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. ↩