EpochStep

{-# OPTIONS --safe #-}

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

module Ledger.Conway.Specification.Chain.Properties.EpochStep
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs)
  where

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.Prelude
open Block

Claim (New enact state only if new epoch).

Informally.

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.

Formally.

enact-change⇒newEpoch : (b : Block) {cs cs'  : ChainState}
  → _ ⊢ cs ⇀⦇ b ,CHAIN⦈ cs' → EnactStateOf cs ≢ EnactStateOf cs'
  → Type

enact-change⇒newEpoch b {cs} h es≢es' =
  epoch (b .bheader .bhbody .slot) ≡ sucᵉ (LastEpochOf cs)
  where
    open Block
    open BHeader
    open BHBody

Proof. (coming soon)