Chains

A chain is simply a sequence of blocks.

Chain = List Block

The genesis block is just the start of any chain, so it’s simpler to consider any empty chain to consist of just the genesis block.

genesisChain = Chain ∋ []

instance HasEpoch-Chain = HasEpoch Chain ∋ λ where ._∙epoch → λ where
  []      → 0
  (b ∷ _) → b .epoch

Not all chains are valid though: each subsequent block must reference the latest block by hash and cannot decrease the epoch number.

record _-connects-to-_ (b : Block) (ch : Chain) : Type where
  constructor connects∶
  field hashesMatch   : b .parentHash ≡ ch ♯
        epochAdvances : b .epoch > ch ∙epoch

data ValidChain : Chain → Type where
  [] :
      ───────────────────────
      ValidChain genesisChain

  _∷_⊣_ :
    ∀ b →
    ∙ ValidChain ch
    ∙ b -connects-to- ch
      ────────────────────
      ValidChain (b ∷ ch)