1module Leios.SpecStructure where
1record SpecStructure : Type₁ where
1234 field a : LeiosAbstract open LeiosAbstract a public open Leios.Blocks a public
1234567 field ⦃ IsBlock-Vote ⦄ : IsBlock (List Vote) ⦃ Hashable-PreEndorserBlock ⦄ : Hashable PreEndorserBlock Hash id : PoolID FFD' : FFDAbstract.Functionality ffdAbstract vrf' : LeiosVRF a open LeiosVRF vrf' public
1234 field sk-EB sk-VT : PrivKey pk-EB pk-VT : PubKey open Leios.Base a vrf' public
12345 field B' : BaseAbstract BF : BaseAbstract.Functionality B' initBaseState : BaseAbstract.Functionality.State BF open Leios.KeyRegistration a vrf' public
12345678 field K' : KeyRegistrationAbstract KF : KeyRegistrationAbstract.Functionality K' module B = BaseAbstract.Functionality BF module K = KeyRegistrationAbstract.Functionality KF module FFD = FFDAbstract.Functionality FFD' open Leios.Voting public
12 field va : VotingAbstract EndorserBlock open VotingAbstract va public
1 field getEBCert : ∀ {s eb} → isVoteCertified s eb → EBCert