EpochStep

{-# OPTIONS --safe #-}

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

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

open import Ledger.Conway.Chain txs abs
open import Ledger.Conway.Enact govStructure
open import Ledger.Conway.Epoch txs abs
open import Ledger.Prelude
open Block

  - *Informally*. Let and be `ChainState`{.AgdaRecord}s and a `Block`{.AgdaRecord}. If `⇀⦇`{.AgdaDatatype} `,CHAIN⦈`{.AgdaDatatype} and if the enact states of and differ, then the epoch of the slot of is the successor of the last epoch of . - *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 .slot) ≡ sucᵉ (LastEpochOf cs)

- *Proof*. *To appear* (in the module of the [formal ledger repository](\repourl)).