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 BM : BaseAbstract.BaseMachine B' ⦃ Hashable-RankingBlock ⦄ : Hashable RankingBlock Hash open Leios.KeyRegistration a vrf' public
12345678 field K' : KeyRegistrationAbstract KF : KeyRegistrationAbstract.Functionality K' module B = BaseAbstract.BaseMachine BM module K = KeyRegistrationAbstract.Functionality KF module FFD = FFDAbstract.Functionality FFD' open Leios.Voting public
12 field va : VotingAbstract EndorserBlock open VotingAbstract va public
1234567891011 field getEBCert : ∀ {s eb} → isVoteCertified s eb → EBCert -- Whether validation of the given EB has completed by the given slot. -- Replaces the former `validityCheckTime : EndorserBlock → ℕ` oracle: -- validation latency is a property of the node and its environment, -- not of the EB alone, so the spec only assumes an observable -- completion predicate (monotone in the slot in intended -- instantiations). Eventually to be provided by an asynchronous -- validation functionality (Valid/Invalid/InProgress with bounded -- InProgress). isValidityChecked : ℕ → EndorserBlock → Type isValidityChecked? : ∀ n eb → Dec (isValidityChecked n eb)