diff --git a/formal-spec/Everything.agda b/formal-spec/Everything.agda index c3524651..e2f5ecda 100644 --- a/formal-spec/Everything.agda +++ b/formal-spec/Everything.agda @@ -1,5 +1,3 @@ -{-# OPTIONS --erasure #-} - module Everything where open import Leios.Simplified diff --git a/formal-spec/Leios/Base.agda b/formal-spec/Leios/Base.agda index b7585992..3402ba76 100644 --- a/formal-spec/Leios/Base.agda +++ b/formal-spec/Leios/Base.agda @@ -19,10 +19,10 @@ record BaseAbstract : Type₁ where field Cert : Type VTy : Type initSlot : VTy → ℕ - V-chkCerts : List PubKey → EndorserBlock × Cert → Type + V-chkCerts : List PubKey → EndorserBlock × Cert → Bool - data Input : Type₁ where - INIT : (EndorserBlock × Cert → Type) → Input + data Input : Type where + INIT : (EndorserBlock × Cert → Bool) → Input SUBMIT : RankingBlock → Input FTCH-LDG : Input @@ -34,6 +34,7 @@ record BaseAbstract : Type₁ where record Functionality : Type₁ where field State : Type _-⟦_/_⟧⇀_ : State → Input → Output → State → Type + SUBMIT-total : ∀ {s b} → ∃[ s' ] s -⟦ SUBMIT b / EMPTY ⟧⇀ s' open Input public open Output public diff --git a/formal-spec/Leios/FFD.agda b/formal-spec/Leios/FFD.agda index b7bcdd64..027adaa0 100644 --- a/formal-spec/Leios/FFD.agda +++ b/formal-spec/Leios/FFD.agda @@ -21,6 +21,7 @@ record FFDAbstract : Type₁ where field State : Type initFFDState : State _-⟦_/_⟧⇀_ : State → Input → Output → State → Type + FFD-total : ∀ {ffds i o} → ∃[ ffds' ] ffds -⟦ i / o ⟧⇀ ffds' open Input public open Output public diff --git a/formal-spec/Leios/Prelude.agda b/formal-spec/Leios/Prelude.agda index 37a83203..7c56b261 100644 --- a/formal-spec/Leios/Prelude.agda +++ b/formal-spec/Leios/Prelude.agda @@ -36,3 +36,10 @@ filter P = L.filter ¿ P ¿¹ instance IsSet-List : {A : Set} → IsSet (List A) A IsSet-List .toSet A = fromList A + +open import Data.List.Relation.Unary.Any +open Properties + +finite⇒A≡∅⊎∃a∈A : {X : Type} → {A : ℙ X} → finite A → (A ≡ᵉ ∅) ⊎ Σ[ a ∈ X ] a ∈ A +finite⇒A≡∅⊎∃a∈A ([] , h) = inj₁ (∅-least (λ a∈A → ⊥-elim (case Equivalence.to h a∈A of λ ()))) +finite⇒A≡∅⊎∃a∈A (x ∷ _ , h) = inj₂ (x , Equivalence.from h (here refl)) diff --git a/formal-spec/Leios/Protocol.agda b/formal-spec/Leios/Protocol.agda index 4122de74..20fb11f5 100644 --- a/formal-spec/Leios/Protocol.agda +++ b/formal-spec/Leios/Protocol.agda @@ -4,7 +4,7 @@ open import Leios.Prelude hiding (id) open import Leios.FFD open import Leios.SpecStructure -module Leios.Protocol (⋯ : SpecStructure) (let open SpecStructure ⋯) (SlotUpkeep : Type) where +module Leios.Protocol {n} (⋯ : SpecStructure n) (let open SpecStructure ⋯) (SlotUpkeep : Type) where open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot) open GenFFD @@ -31,19 +31,20 @@ data LeiosOutput : Type where EMPTY : LeiosOutput record LeiosState : Type where - field V : VTy - SD : StakeDistr - FFDState : FFD.State - Ledger : List Tx - ToPropose : List Tx - IBs : List InputBlock - EBs : List EndorserBlock - Vs : List (List Vote) - slot : ℕ - IBHeaders : List IBHeader - IBBodies : List IBBody - Upkeep : ℙ SlotUpkeep - BaseState : B.State + field V : VTy + SD : StakeDistr + FFDState : FFD.State + Ledger : List Tx + ToPropose : List Tx + IBs : List InputBlock + EBs : List EndorserBlock + Vs : List (List Vote) + slot : ℕ + IBHeaders : List IBHeader + IBBodies : List IBBody + Upkeep : ℙ SlotUpkeep + BaseState : B.State + votingState : VotingState lookupEB : EBRef → Maybe EndorserBlock lookupEB r = find (λ b → getEBRef b ≟ r) EBs @@ -68,6 +69,7 @@ record LeiosState : Type where addUpkeep : LeiosState → SlotUpkeep → LeiosState addUpkeep s u = let open LeiosState s in record s { Upkeep = Upkeep ∪ ❴ u ❵ } +{-# INJECTIVE_FOR_INFERENCE addUpkeep #-} initLeiosState : VTy → StakeDistr → B.State → LeiosState initLeiosState V SD bs = record @@ -84,6 +86,7 @@ initLeiosState V SD bs = record ; IBBodies = [] ; Upkeep = ∅ ; BaseState = bs + ; votingState = initVotingState } -- some predicates about EBs diff --git a/formal-spec/Leios/Simplified.agda b/formal-spec/Leios/Simplified.agda index 474339af..d5c38ac7 100644 --- a/formal-spec/Leios/Simplified.agda +++ b/formal-spec/Leios/Simplified.agda @@ -3,12 +3,18 @@ open import Leios.Prelude hiding (id) open import Leios.FFD open import Leios.SpecStructure +open import Data.Fin.Patterns -module Leios.Simplified (⋯ : SpecStructure) (let open SpecStructure ⋯) (Λ μ : ℕ) where +open import Tactic.Defaults +open import Tactic.Derive.DecEq + +module Leios.Simplified (⋯ : SpecStructure 2) (let open SpecStructure ⋯) (Λ μ : ℕ) where data SlotUpkeep : Type where Base IB-Role EB-Role V1-Role V2-Role : SlotUpkeep +unquoteDecl DecEq-SlotUpkeep = derive-DecEq ((quote SlotUpkeep , DecEq-SlotUpkeep) ∷ []) + allUpkeep : ℙ SlotUpkeep allUpkeep = fromList (Base ∷ IB-Role ∷ EB-Role ∷ V1-Role ∷ V2-Role ∷ []) @@ -18,12 +24,11 @@ open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot) open FFD hiding (_-⟦_/_⟧⇀_) open GenFFD -record VotingAbstract : Type₁ where - field isVote1Certified : LeiosState → EndorserBlock → Type - isVote2Certified : LeiosState → EndorserBlock → Type +isVote1Certified : LeiosState → EndorserBlock → Type +isVote1Certified s eb = isVoteCertified (LeiosState.votingState s) (0F , eb) - ⦃ isVote1Certified⁇ ⦄ : ∀ {vs eb} → isVote1Certified vs eb ⁇ - ⦃ isVote2Certified⁇ ⦄ : ∀ {vs eb} → isVote2Certified vs eb ⁇ +isVote2Certified : LeiosState → EndorserBlock → Type +isVote2Certified s eb = isVoteCertified (LeiosState.votingState s) (1F , eb) -- Predicates about EBs module _ (s : LeiosState) (eb : EndorserBlock) where @@ -36,145 +41,144 @@ module _ (s : LeiosState) (eb : EndorserBlock) where where candidateEBs : ℙ Hash candidateEBs = mapˢ getEBRef $ filterˢ (_∈ᴮ slice L slot (μ + 3)) (fromList EBs) -module Protocol (va : VotingAbstract) (let open VotingAbstract va) where - - private variable s s' : LeiosState - ffds' : FFD.State - π : VrfPf - bs' : B.State - ks ks' : K.State - msgs : List (FFDAbstract.Header ffdAbstract ⊎ FFDAbstract.Body ffdAbstract) - eb : EndorserBlock - rbs : List RankingBlock - txs : List Tx - V : VTy - SD : StakeDistr - pks : List PubKey - - data _↝_ : LeiosState → LeiosState → Type where - - IB-Role : let open LeiosState s renaming (FFDState to ffds) - b = ibBody (record { txs = ToPropose }) - h = ibHeader (mkIBHeader slot id π sk-IB ToPropose) - in - ∙ needsUpkeep IB-Role - ∙ canProduceIB slot sk-IB (stake s) π - ∙ ffds FFD.-⟦ Send h (just b) / SendRes ⟧⇀ ffds' - ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } IB-Role - - EB-Role : let open LeiosState s renaming (FFDState to ffds) - LI = map getIBRef $ filter (_∈ᴮ slice L slot (Λ + 1)) IBs - LE = map getEBRef $ filter (isVote1Certified s) $ - filter (_∈ᴮ slice L slot (μ + 2)) EBs - h = mkEB slot id π sk-EB LI LE - in - ∙ needsUpkeep EB-Role - ∙ canProduceEB slot sk-EB (stake s) π - ∙ ffds FFD.-⟦ Send (ebHeader h) nothing / SendRes ⟧⇀ ffds' - ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } EB-Role - - V1-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot (μ + 1)) EBs - votes = map (vote sk-V ∘ hash) EBs' - in - ∙ needsUpkeep V1-Role - ∙ canProduceV slot sk-V (stake s) - ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds' - ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } V1-Role - - V2-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filter (vote2Eligible s) $ filter (_∈ᴮ slice L slot 1) EBs - votes = map (vote sk-V ∘ hash) EBs' - in - ∙ needsUpkeep V2-Role - ∙ canProduceV slot sk-V (stake s) - ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds' - ───────────────────────────────────────────────────────────────────────── - s ↝ addUpkeep record s { FFDState = ffds' } V2-Role - - -- Note: Base doesn't need a negative rule, since it can always be invoked - - No-IB-Role : let open LeiosState s in - ∙ needsUpkeep IB-Role - ∙ ¬ canProduceIB slot sk-IB (stake s) π - ───────────────────────────────────────────── - s ↝ addUpkeep s IB-Role - - No-EB-Role : let open LeiosState s in - ∙ needsUpkeep EB-Role - ∙ ¬ canProduceEB slot sk-EB (stake s) π - ───────────────────────────────────────────── - s ↝ addUpkeep s EB-Role - - No-V1-Role : let open LeiosState s in - ∙ needsUpkeep V1-Role - ∙ ¬ canProduceV slot sk-V (stake s) - ───────────────────────────────────────────── - s ↝ addUpkeep s V1-Role - - No-V2-Role : let open LeiosState s in - ∙ needsUpkeep V2-Role - ∙ ¬ canProduceV slot sk-V (stake s) - ───────────────────────────────────────────── - s ↝ addUpkeep s V2-Role - - data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → LeiosState → Type where - - -- Initialization - - Init : - ∙ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks' - ∙ initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs' - ──────────────────────────────────────────────────────────────── - nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' - - -- Network and Ledger - - Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) in - ∙ Upkeep ≡ᵉ allUpkeep - ∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs' - ∙ ffds FFD.-⟦ Fetch / FetchRes msgs ⟧⇀ ffds' - ─────────────────────────────────────────────────────────────────────── - just s -⟦ SLOT / EMPTY ⟧⇀ record s - { FFDState = ffds' - ; Ledger = constructLedger rbs - ; slot = suc slot - ; Upkeep = ∅ - } ↑ L.filter isValid? msgs - - Ftch : - ──────────────────────────────────────────────────────── - just s -⟦ FTCH-LDG / FTCH-LDG (LeiosState.Ledger s) ⟧⇀ s - - -- Base chain - -- - -- Note: Submitted data to the base chain is only taken into account - -- if the party submitting is the block producer on the base chain - -- for the given slot - - Base₁ : - ─────────────────────────────────────────────────────────────────── - just s -⟦ SUBMIT (inj₂ txs) / EMPTY ⟧⇀ record s { ToPropose = txs } - - Base₂a : let open LeiosState s renaming (BaseState to bs) in - ∙ needsUpkeep Base - ∙ eb ∈ filter (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs - ∙ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs' - ─────────────────────────────────────────────────────────────────────── - just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base - - Base₂b : let open LeiosState s renaming (BaseState to bs) in - ∙ needsUpkeep Base - ∙ [] ≡ filter (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs - ∙ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs' - ─────────────────────────────────────────────────────────────────────── - just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s Base - - -- Protocol rules - - Roles : ∙ s ↝ s' - ───────────────────────────── - just s -⟦ SLOT / EMPTY ⟧⇀ s' +private variable s s' : LeiosState + ffds' : FFD.State + π : VrfPf + bs' : B.State + ks ks' : K.State + msgs : List (FFDAbstract.Header ffdAbstract ⊎ FFDAbstract.Body ffdAbstract) + eb : EndorserBlock + rbs : List RankingBlock + txs : List Tx + V : VTy + SD : StakeDistr + pks : List PubKey + +data _↝_ : LeiosState → LeiosState → Type where + + IB-Role : let open LeiosState s renaming (FFDState to ffds) + b = ibBody (record { txs = ToPropose }) + h = ibHeader (mkIBHeader slot id π sk-IB ToPropose) + in + ∙ needsUpkeep IB-Role + ∙ canProduceIB slot sk-IB (stake s) π + ∙ ffds FFD.-⟦ Send h (just b) / SendRes ⟧⇀ ffds' + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } IB-Role + + EB-Role : let open LeiosState s renaming (FFDState to ffds) + LI = map getIBRef $ filter (_∈ᴮ slice L slot (Λ + 1)) IBs + LE = map getEBRef $ filter (isVote1Certified s) $ + filter (_∈ᴮ slice L slot (μ + 2)) EBs + h = mkEB slot id π sk-EB LI LE + in + ∙ needsUpkeep EB-Role + ∙ canProduceEB slot sk-EB (stake s) π + ∙ ffds FFD.-⟦ Send (ebHeader h) nothing / SendRes ⟧⇀ ffds' + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } EB-Role + + V1-Role : let open LeiosState s renaming (FFDState to ffds) + EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot (μ + 1)) EBs + votes = map (vote sk-V ∘ hash) EBs' + in + ∙ needsUpkeep V1-Role + ∙ canProduceV1 slot sk-V (stake s) + ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds' + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } V1-Role + + V2-Role : let open LeiosState s renaming (FFDState to ffds) + EBs' = filter (vote2Eligible s) $ filter (_∈ᴮ slice L slot 1) EBs + votes = map (vote sk-V ∘ hash) EBs' + in + ∙ needsUpkeep V2-Role + ∙ canProduceV2 slot sk-V (stake s) + ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds' + ───────────────────────────────────────────────────────────────────────── + s ↝ addUpkeep record s { FFDState = ffds' } V2-Role + + -- Note: Base doesn't need a negative rule, since it can always be invoked + + No-IB-Role : let open LeiosState s in + ∙ needsUpkeep IB-Role + ∙ (∀ π → ¬ canProduceIB slot sk-IB (stake s) π) + ───────────────────────────────────────────── + s ↝ addUpkeep s IB-Role + + No-EB-Role : let open LeiosState s in + ∙ needsUpkeep EB-Role + ∙ (∀ π → ¬ canProduceEB slot sk-EB (stake s) π) + ───────────────────────────────────────────── + s ↝ addUpkeep s EB-Role + + No-V1-Role : let open LeiosState s in + ∙ needsUpkeep V1-Role + ∙ ¬ canProduceV1 slot sk-V (stake s) + ───────────────────────────────────────────── + s ↝ addUpkeep s V1-Role + + No-V2-Role : let open LeiosState s in + ∙ needsUpkeep V2-Role + ∙ ¬ canProduceV2 slot sk-V (stake s) + ───────────────────────────────────────────── + s ↝ addUpkeep s V2-Role + +data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → LeiosState → Type where + + -- Initialization + + Init : + ∙ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks' + ∙ initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs' + ──────────────────────────────────────────────────────────────── + nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' + + -- Network and Ledger + + Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) in + ∙ Upkeep ≡ᵉ allUpkeep + ∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs' + ∙ ffds FFD.-⟦ Fetch / FetchRes msgs ⟧⇀ ffds' + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ record s + { FFDState = ffds' + ; Ledger = constructLedger rbs + ; slot = suc slot + ; Upkeep = ∅ + ; BaseState = bs' + } ↑ L.filter isValid? msgs + + Ftch : + ──────────────────────────────────────────────────────── + just s -⟦ FTCH-LDG / FTCH-LDG (LeiosState.Ledger s) ⟧⇀ s + + -- Base chain + -- + -- Note: Submitted data to the base chain is only taken into account + -- if the party submitting is the block producer on the base chain + -- for the given slot + + Base₁ : + ─────────────────────────────────────────────────────────────────── + just s -⟦ SUBMIT (inj₂ txs) / EMPTY ⟧⇀ record s { ToPropose = txs } + + Base₂a : let open LeiosState s renaming (BaseState to bs) in + ∙ needsUpkeep Base + ∙ eb ∈ filter (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs + ∙ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs' + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base + + Base₂b : let open LeiosState s renaming (BaseState to bs) in + ∙ needsUpkeep Base + ∙ [] ≡ filter (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs + ∙ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs' + ─────────────────────────────────────────────────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base + + -- Protocol rules + + Roles : ∙ s ↝ s' + ───────────────────────────── + just s -⟦ SLOT / EMPTY ⟧⇀ s' diff --git a/formal-spec/Leios/SpecStructure.agda b/formal-spec/Leios/SpecStructure.agda index 798d6397..0ab4317a 100644 --- a/formal-spec/Leios/SpecStructure.agda +++ b/formal-spec/Leios/SpecStructure.agda @@ -8,10 +8,13 @@ open import Leios.VRF import Leios.Base import Leios.Blocks import Leios.KeyRegistration +import Leios.Voting + +open import Data.Fin module Leios.SpecStructure where -record SpecStructure : Type₁ where +record SpecStructure (rounds : ℕ) : Type₁ where field a : LeiosAbstract open LeiosAbstract a public @@ -43,3 +46,8 @@ record SpecStructure : Type₁ where module B = BaseAbstract.Functionality BF module K = KeyRegistrationAbstract.Functionality KF module FFD = FFDAbstract.Functionality FFD' + + open Leios.Voting public + + field va : VotingAbstract (Fin rounds × EndorserBlock) + open VotingAbstract va public diff --git a/formal-spec/Leios/UniformShort.agda b/formal-spec/Leios/UniformShort.agda index aa9c8051..ceaedf02 100644 --- a/formal-spec/Leios/UniformShort.agda +++ b/formal-spec/Leios/UniformShort.agda @@ -3,8 +3,10 @@ open import Leios.Prelude hiding (id) open import Leios.FFD open import Leios.SpecStructure +open import Data.Fin.Patterns -module Leios.UniformShort (⋯ : SpecStructure) (let open SpecStructure ⋯) where +module Leios.UniformShort (⋯ : SpecStructure 1) + (let open SpecStructure ⋯ renaming (isVoteCertified to isVoteCertified')) where data SlotUpkeep : Type where Base IB-Role EB-Role V-Role : SlotUpkeep @@ -18,11 +20,10 @@ open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot) open FFD hiding (_-⟦_/_⟧⇀_) open GenFFD -record VotingAbstract : Type₁ where - field isVoteCertified : LeiosState → EndorserBlock → Type - ⦃ isVoteCertified⁇ ⦄ : ∀ {vs eb} → isVoteCertified vs eb ⁇ +isVoteCertified : LeiosState → EndorserBlock → Type +isVoteCertified s eb = isVoteCertified' (LeiosState.votingState s) (0F , eb) -module Protocol (va : VotingAbstract) (let open VotingAbstract va) where +module Protocol where private variable s s' : LeiosState ffds' : FFD.State diff --git a/formal-spec/Leios/VRF.agda b/formal-spec/Leios/VRF.agda index 1133a46d..8aae1cff 100644 --- a/formal-spec/Leios/VRF.agda +++ b/formal-spec/Leios/VRF.agda @@ -17,11 +17,17 @@ record LeiosVRF : Type₁ where open VRF vrf public -- transforming slot numbers into VRF seeds - field genIBInput genEBInput genVInput : ℕ → ℕ + field genIBInput genEBInput genVInput genV1Input genV2Input : ℕ → ℕ canProduceIB : ℕ → PrivKey → ℕ → VrfPf → Type canProduceIB slot k stake π = let (val , pf) = eval k (genIBInput slot) in val < stake × pf ≡ π + Dec-canProduceIB : ∀ {slot k stake} → (∃[ π ] canProduceIB slot k stake π) ⊎ (∀ π → ¬ canProduceIB slot k stake π) + Dec-canProduceIB {slot} {k} {stake} with eval k (genIBInput slot) + ... | (val , pf) = case ¿ val < stake ¿ of λ where + (yes p) → inj₁ (pf , p , refl) + (no ¬p) → inj₂ (λ π (h , _) → ¬p h) + canProduceIBPub : ℕ → ℕ → PubKey → VrfPf → ℕ → Type canProduceIBPub slot val k pf stake = verify k (genIBInput slot) val pf × val < stake @@ -33,3 +39,9 @@ record LeiosVRF : Type₁ where canProduceV : ℕ → PrivKey → ℕ → Type canProduceV slot k stake = proj₁ (eval k (genVInput slot)) < stake + + canProduceV1 : ℕ → PrivKey → ℕ → Type + canProduceV1 slot k stake = proj₁ (eval k (genV1Input slot)) < stake + + canProduceV2 : ℕ → PrivKey → ℕ → Type + canProduceV2 slot k stake = proj₁ (eval k (genV2Input slot)) < stake diff --git a/formal-spec/Leios/Voting.agda b/formal-spec/Leios/Voting.agda new file mode 100644 index 00000000..b12e7bc5 --- /dev/null +++ b/formal-spec/Leios/Voting.agda @@ -0,0 +1,12 @@ +{-# OPTIONS --safe #-} + +open import Leios.Prelude + +module Leios.Voting where + +record VotingAbstract (X : Type) : Type₁ where + field VotingState : Type + initVotingState : VotingState + isVoteCertified : VotingState → X → Type + + ⦃ isVoteCertified⁇ ⦄ : ∀ {vs x} → isVoteCertified vs x ⁇ diff --git a/nix/agda.nix b/nix/agda.nix index 395fea5b..0174e2d9 100644 --- a/nix/agda.nix +++ b/nix/agda.nix @@ -70,8 +70,8 @@ let src = pkgs.fetchFromGitHub { repo = "iog-agda-prelude"; owner = "input-output-hk"; - rev = "ee289f9a0b2ec0a3bfc43c3f678a17c174b397e6"; - sha256 = "sha256-noLUBl9d/vDNbAzWfnBrWoATlBrVG1DwzRV7/2uRHoE="; + rev = "e4f83fa59142baaad4944910217be05ebf6e2f22"; + sha256 = "sha256-ytTOvz97lTHTiVdpmS3HUfTp/LH1Xey9bSh9zaBuacU="; }; meta = { }; libraryFile = "iog-prelude.agda-lib";