Epoch

{-# OPTIONS --safe #-}

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

module Ledger.Conway.Conformance.Epoch
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs) (open AbstractFunctions abs)
  where

open import Ledger.Prelude
open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Conformance.Equivalence txs abs
open import Ledger.Conway.Conformance.Equivalence.Convert
open import Ledger.Conway.Conformance.Equivalence.Deposits txs abs
open import Ledger.Conway.Conformance.Ledger txs abs
open import Ledger.Conway.Specification.Ratify govStructure
open import Ledger.Conway.Conformance.Certs govStructure
open import Ledger.Conway.Conformance.Rewards txs abs
import Ledger.Conway.Specification.Epoch txs abs as EpochSpec

record EpochState : Type where
  constructor ⟦_,_,_,_,_⟧ᵉ'
  field
    acnt       : Acnt
    ss         : Snapshots
    ls         : LState
    es         : EnactState
    fut        : RatifyState

record NewEpochState : Type where
  field
    lastEpoch   : Epoch
    bprev       : BlocksMade
    bcur        : BlocksMade
    epochState  : EpochState
    ru          : Maybe RewardUpdate
    pd          : KeyHash ⇀ Coin

instance
  unquoteDecl HasCast-EpochState HasCast-NewEpochState = derive-HasCast
    ( (quote EpochState     , HasCast-EpochState)
    ∷ [ (quote NewEpochState  , HasCast-NewEpochState)])

  EpochStateFromConf : EpochState ⭆ EpochSpec.EpochState
  EpochStateFromConf .convⁱ _ epochState =
    let open EpochState epochState in
    $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1003}{\htmlId{1687}{\htmlClass{Field}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1025}{\htmlId{1694}{\htmlClass{Field}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#562}{\htmlId{1699}{\htmlClass{Function}{\text{conv}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1052}{\htmlId{1704}{\htmlClass{Field}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1076}{\htmlId{1709}{\htmlClass{Field}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1104}{\htmlId{1714}{\htmlClass{Field}{\text{fut}}}}\, \end{pmatrix}$

  EpochStateToConf : EpochSpec.EpochState ⭆ EpochState
  EpochStateToConf .convⁱ deposits epochSt =
    let open EpochSpec.EpochState epochSt in
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#2323}{\htmlId{1872}{\htmlClass{Field}{\text{acnt}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#2345}{\htmlId{1879}{\htmlClass{Field}{\text{ss}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Deposits.html#12903}{\htmlId{1884}{\htmlClass{Function}{\text{certDeposits}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#2372}{\htmlId{1897}{\htmlClass{Field}{\text{ls}}}}\, \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#380}{\htmlId{1900}{\htmlClass{Function Operator}{\text{⊢conv}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#2372}{\htmlId{1906}{\htmlClass{Field}{\text{ls}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#2396}{\htmlId{1911}{\htmlClass{Field}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#2424}{\htmlId{1916}{\htmlClass{Field}{\text{fut}}}}\, \end{pmatrix}$

  NewEpochStateFromConf : NewEpochState ⭆ EpochSpec.NewEpochState
  NewEpochStateFromConf .convⁱ _ newEpochState =
    let open NewEpochState newEpochState in
    $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Epoch.html#1176}{\htmlId{2090}{\htmlClass{Field}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1200}{\htmlId{2102}{\htmlClass{Field}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1229}{\htmlId{2110}{\htmlClass{Field}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#562}{\htmlId{2117}{\htmlClass{Function}{\text{conv}}}}\, \,\href{Ledger.Conway.Conformance.Epoch.html#1258}{\htmlId{2122}{\htmlClass{Field}{\text{epochState}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1287}{\htmlId{2135}{\htmlClass{Field}{\text{ru}}}}\, \\ \,\href{Ledger.Conway.Conformance.Epoch.html#1324}{\htmlId{2140}{\htmlClass{Field}{\text{pd}}}}\, \end{pmatrix}$

  NewEpochStateToConf : EpochSpec.NewEpochState ⭆ NewEpochState
  NewEpochStateToConf .convⁱ deposits newEpochSt =
    let open EpochSpec.NewEpochState newEpochSt in
    $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Epoch.html#4319}{\htmlId{2318}{\htmlClass{Field}{\text{lastEpoch}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#4372}{\htmlId{2330}{\htmlClass{Field}{\text{bcur}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#4343}{\htmlId{2337}{\htmlClass{Field}{\text{bprev}}}}\, \\ \,\href{Ledger.Conway.Conformance.Equivalence.Convert.html#562}{\htmlId{2345}{\htmlClass{Function}{\text{conv}}}}\, \,\href{Ledger.Conway.Specification.Epoch.html#4401}{\htmlId{2350}{\htmlClass{Field}{\text{epochState}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#4430}{\htmlId{2363}{\htmlClass{Field}{\text{ru}}}}\, \\ \,\href{Ledger.Conway.Specification.Epoch.html#4467}{\htmlId{2368}{\htmlClass{Field}{\text{pd}}}}\, \end{pmatrix}$