module Ledger.Core.Foreign.Epoch where

open import Ledger.Prelude
open import Ledger.Prelude.Foreign.HSTypes
open import Tactic.Derive.HsType

open import Ledger.Core.Specification.Epoch public

open import Data.Integer as ℤ
open import Data.Rational as ℚ

HSGlobalConstants : GlobalConstants
HSGlobalConstants = record {
  Network = ℕ
  ; SlotsPerEpochᶜ = 4320
  ; ActiveSlotCoeff = ℤ.1ℤ ℚ./ 20
  ; RandomnessStabilisationWindowᶜ = 10
  ; StabilityWindowᶜ = 10
  ; MaxLovelaceSupplyᶜ = 1
  ; Quorum = 1
  ; NetworkId = 0
  ; MaxKESEvoᶜ = 10
  ; SlotsPerKESPeriodᶜ = 864  -- derives a key age of 4 epochs
  }

HSEpochStructure : EpochStructure
HSEpochStructure = ℕEpochStructure HSGlobalConstants

open EpochStructure HSEpochStructure

unquoteDecl =
  hsTypeAlias Epoch