diff --git a/formal-spec/Leios/Abstract.agda b/formal-spec/Leios/Abstract.agda index 1c35e9f..0ee2c1f 100644 --- a/formal-spec/Leios/Abstract.agda +++ b/formal-spec/Leios/Abstract.agda @@ -11,7 +11,7 @@ record LeiosAbstract : Type₁ where BodyHash VrfPf PrivKey Sig Hash : Type -- these could have been byte strings, but this is safer ⦃ DecEq-Hash ⦄ : DecEq Hash Vote : Type - vote : Hash → Vote + vote : PrivKey → Hash → Vote sign : PrivKey → Hash → Sig ⦃ Hashable-Txs ⦄ : Hashable (List Tx) Hash L Λ μ : ℕ diff --git a/formal-spec/Leios/Base.agda b/formal-spec/Leios/Base.agda index fbdf18e..c8be4e5 100644 --- a/formal-spec/Leios/Base.agda +++ b/formal-spec/Leios/Base.agda @@ -2,8 +2,10 @@ open import Leios.Prelude open import Leios.Abstract +open import Leios.VRF -module Leios.Base (a : LeiosAbstract) (open LeiosAbstract a) where +module Leios.Base (a : LeiosAbstract) (open LeiosAbstract a) (vrf' : LeiosVRF a) + (let open LeiosVRF vrf') where open import Leios.Blocks a using (EndorserBlock) @@ -12,15 +14,23 @@ StakeDistr = PoolID ⇀ ℕ record BaseAbstract : Type₁ where field Cert : Type + VTy : Type + initSlot : VTy → ℕ + V-chkCerts : List PubKey → EndorserBlock × Cert → Type data Input : Type₁ where INIT : (EndorserBlock × Cert → Type) → Input SUBMIT : EndorserBlock ⊎ List Tx → Input -- maybe we have both + FTCH-LDG : Input data Output : Type where STAKE : StakeDistr → Output EMPTY : Output + BASE-LDG : List EndorserBlock → Output record Functionality : Type₁ where field State : Type _⇀⟦_⟧_ : State → Input → State × Output → Type + + open Input public + open Output public diff --git a/formal-spec/Leios/Blocks.agda b/formal-spec/Leios/Blocks.agda index 4d521c2..3ed7a79 100644 --- a/formal-spec/Leios/Blocks.agda +++ b/formal-spec/Leios/Blocks.agda @@ -74,6 +74,16 @@ mkIBHeader slot id π pKey txs = record { signature = sign pKey (hash h) ; IBHea getIBRef : ⦃ Hashable IBHeader Hash ⦄ → InputBlock → IBRef getIBRef = hash ∘ InputBlock.header +-- TODO +record ibHeaderValid (h : IBHeader) : Type where +record ibBodyValid (b : IBBody) : Type where + +ibHeaderValid? : (h : IBHeader) → Dec (ibHeaderValid h) +ibHeaderValid? _ = yes record {} + +ibBodyValid? : (b : IBBody) → Dec (ibBodyValid b) +ibBodyValid? _ = yes record {} + -------------------------------------------------------------------------------- -- Endorser Blocks -------------------------------------------------------------------------------- @@ -113,12 +123,25 @@ getEBRef : ⦃ Hashable PreEndorserBlock Hash ⦄ → EndorserBlock → EBRef getEBRef = hash -- TODO --- record ebValid (eb : EndorserBlock) : Type where +record ebValid (eb : EndorserBlock) : Type where -- field lotteryPfValid : {!!} -- signatureValid : {!!} -- ibRefsValid : {!!} -- ebRefsValid : {!!} +ebValid? : (eb : EndorserBlock) → Dec (ebValid eb) +ebValid? _ = yes record {} + +-------------------------------------------------------------------------------- +-- Votes +-------------------------------------------------------------------------------- + +-- TODO +record vsValid (vs : List Vote) : Type where + +vsValid? : (vs : List Vote) → Dec (vsValid vs) +vsValid? _ = yes record {} + -------------------------------------------------------------------------------- -- FFD for Leios Blocks -------------------------------------------------------------------------------- @@ -135,11 +158,42 @@ module GenFFD ⦃ _ : IsBlock (List Vote) ⦄ where ID : Type ID = ℕ × PoolID - match : Header → Body → Type - match (ibHeader h) (ibBody b) = bodyHash ≡ hash b + matchIB : IBHeader → IBBody → Type + matchIB h b = bodyHash ≡ hash b + where open IBHeaderOSig h; open IBBody b + + matchIB? : ∀ (h : IBHeader) → (b : IBBody) → Dec (matchIB h b) + matchIB? h b = bodyHash ≟ hash b where open IBHeaderOSig h; open IBBody b + + match : Header → Body → Type + match (ibHeader h) (ibBody b) = matchIB h b match _ _ = ⊥ + headerValid : Header → Type + headerValid (ibHeader h) = ibHeaderValid h + headerValid (ebHeader h) = ebValid h + headerValid (vHeader h) = vsValid h + + headerValid? : (h : Header) → Dec (headerValid h) + headerValid? (ibHeader h) = ibHeaderValid? h + headerValid? (ebHeader h) = ebValid? h + headerValid? (vHeader h) = vsValid? h + + bodyValid : Body → Type + bodyValid (ibBody b) = ibBodyValid b + + bodyValid? : (b : Body) → Dec (bodyValid b) + bodyValid? (ibBody b) = ibBodyValid? b + + isValid : Header ⊎ Body → Type + isValid (inj₁ h) = headerValid h + isValid (inj₂ b) = bodyValid b + + isValid? : ∀ (x : Header ⊎ Body) → Dec (isValid x) + isValid? (inj₁ h) = headerValid? h + isValid? (inj₂ b) = bodyValid? b + -- can we express uniqueness wrt pipelines as a property? msgID : Header → ID msgID (ibHeader h) = (slotNumber h , producerID h) diff --git a/formal-spec/Leios/FFD.agda b/formal-spec/Leios/FFD.agda index e38f9ad..ac5919e 100644 --- a/formal-spec/Leios/FFD.agda +++ b/formal-spec/Leios/FFD.agda @@ -20,4 +20,8 @@ record FFDAbstract : Type₁ where record Functionality : Type₁ where field State : Type + initFFDState : State stepRel : Input → State → State × Output → Type + + open Input public + open Output public diff --git a/formal-spec/Leios/KeyRegistration.agda b/formal-spec/Leios/KeyRegistration.agda new file mode 100644 index 0000000..7807330 --- /dev/null +++ b/formal-spec/Leios/KeyRegistration.agda @@ -0,0 +1,23 @@ +{-# OPTIONS --safe #-} + +open import Leios.Prelude +open import Leios.Abstract +open import Leios.VRF + +module Leios.KeyRegistration (a : LeiosAbstract) (open LeiosAbstract a) + (vrf : LeiosVRF a) (let open LeiosVRF vrf) where + +record KeyRegistrationAbstract : Type₁ where + + data Input : Type₁ where + INIT : PubKey → PubKey → PubKey → Input + + data Output : Type where + PUBKEYS : List PubKey → Output + + record Functionality : Type₁ where + field State : Type + _⇀⟦_⟧_ : State → Input → State × Output → Type + + open Input public + open Output public diff --git a/formal-spec/Leios/SimpleSpec.agda b/formal-spec/Leios/SimpleSpec.agda index feb4043..564f7a3 100644 --- a/formal-spec/Leios/SimpleSpec.agda +++ b/formal-spec/Leios/SimpleSpec.agda @@ -1,24 +1,35 @@ --- {-# OPTIONS --safe #-} -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --safe #-} open import Leios.Prelude open import Leios.Abstract open import Leios.FFD open import Leios.VRF +import Leios.Voting + import Leios.Base import Leios.Blocks +import Leios.KeyRegistration + +import Data.List as L +import Data.List.Relation.Unary.Any as A module Leios.SimpleSpec (a : LeiosAbstract) (let open LeiosAbstract a) (let open Leios.Blocks a) ⦃ IsBlock-Vote : IsBlock (List Vote) ⦄ ⦃ Hashable-IBHeaderOSig : ∀ {b} → Hashable (IBHeaderOSig b) Hash ⦄ ⦃ Hashable-PreEndorserBlock : Hashable PreEndorserBlock Hash ⦄ - (id : PoolID) (pKey : PrivKey) (FFD' : FFDAbstract.Functionality ffdAbstract) - (vrf : LeiosVRF a) (let open LeiosVRF vrf) (pubKey : PubKey) - (let open Leios.Base a) (B' : BaseAbstract) (BF' : BaseAbstract.Functionality B') where + (id : PoolID) (FFD' : FFDAbstract.Functionality ffdAbstract) + (vrf' : LeiosVRF a) (let open LeiosVRF vrf') + (sk-IB sk-EB sk-V : PrivKey) + (pk-IB pk-EB pk-V : PubKey) + (let open Leios.Base a vrf') (B' : BaseAbstract) (BF : BaseAbstract.Functionality B') + (let open Leios.KeyRegistration a vrf') (K' : KeyRegistrationAbstract) (KF : KeyRegistrationAbstract.Functionality K') where + +module B = BaseAbstract.Functionality BF +module K = KeyRegistrationAbstract.Functionality KF +module FFD = FFDAbstract.Functionality FFD' renaming (stepRel to _⇀⟦_⟧_) -module B = BaseAbstract B' -module BF = BaseAbstract.Functionality BF' -module FFD = FFDAbstract.Functionality FFD' using (State) renaming (stepRel to _⇀⟦_⟧_) +open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot) +open GenFFD -- High level structure: @@ -31,10 +42,6 @@ module FFD = FFDAbstract.Functionality FFD' using (State) renaming (stepRel to _ -- \ / -- Network -postulate VTy FTCHTy : Type - initSlot : VTy → ℕ - initFFDState : FFD.State - data LeiosInput : Type where INIT : VTy → LeiosInput SUBMIT : EndorserBlock ⊎ List Tx → LeiosInput @@ -42,44 +49,60 @@ data LeiosInput : Type where FTCH-LDG : LeiosInput data LeiosOutput : Type where - FTCH-LDG : FTCHTy → LeiosOutput - EMPTY : LeiosOutput + FTCH-LDG : List Tx → LeiosOutput + EMPTY : LeiosOutput record LeiosState : Type where - field V : VTy - SD : StakeDistr - FFDState : FFD.State - Ledger : List Tx + 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 : ℕ + IBs : List InputBlock + EBs : List EndorserBlock + Vs : List (List Vote) + slot : ℕ + IBHeaders : List IBHeader + IBBodies : List IBBody + + lookupEB : EBRef → Maybe EndorserBlock + lookupEB r = find (λ b → getEBRef b ≟ r) EBs + + lookupIB : IBRef → Maybe InputBlock + lookupIB r = find (λ b → getIBRef b ≟ r) IBs + + lookupTxs : EndorserBlock → List Tx + lookupTxs eb = do + eb′ ← mapMaybe lookupEB $ ebRefs eb + ib ← mapMaybe lookupIB $ ibRefs eb′ + txs $ body ib + where open EndorserBlockOSig + open IBBody + open InputBlock + + constructLedger : List EndorserBlock → List Tx + constructLedger = concatMap lookupTxs initLeiosState : VTy → StakeDistr → LeiosState initLeiosState V SD = record { V = V ; SD = SD - ; FFDState = initFFDState + ; FFDState = FFD.initFFDState ; Ledger = [] ; ToPropose = [] ; IBs = [] ; EBs = [] ; Vs = [] ; slot = initSlot V + ; IBHeaders = [] + ; IBBodies = [] } -postulate canProduceV1 : ℕ → Type - canProduceV2 : ℕ → Type - -- some predicates about EBs module _ (s : LeiosState) (eb : EndorserBlock) where open EndorserBlockOSig eb open LeiosState s - postulate isVote1Certified : Type -- Q: what's the threshold? (pg 7, (5)) - postulate isVote2Certified : Type - vote2Eligible : Type vote2Eligible = length ebRefs ≥ lengthˢ candidateEBs / 2 -- should this be `>`? × fromList ebRefs ⊆ candidateEBs @@ -89,9 +112,6 @@ module _ (s : LeiosState) (eb : EndorserBlock) where allIBRefsKnown : Type allIBRefsKnown = ∀[ ref ∈ fromList ibRefs ] ref ∈ˡ map getIBRef IBs -postulate instance isVote1Certified? : ∀ {s eb} → isVote1Certified s eb ⁇ - isVote2Certified? : ∀ {s eb} → isVote2Certified s eb ⁇ - private variable s : LeiosState ffds' : FFD.State π : VrfPf @@ -101,88 +121,127 @@ stake record { SD = SD } = case lookupᵐ? SD id of λ where (just s) → s nothing → 0 -data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutput → Type where - - -- Initialization - - Init : ∀ {V bs bs' SD} → - ∙ {!!} -- create & register the IB/EB lottery and voting keys with key reg - ∙ bs BF.⇀⟦ B.INIT {!V_chkCerts!} ⟧ (bs' , B.STAKE SD) - ────────────────────────────────────────────────────── - nothing ⇀⟦ INIT V ⟧ (initLeiosState V SD , EMPTY) - - -- Network and Ledger - - -- fix: we need to do Slot before every other SLOT transition - Slot : ∀ {msgs} → let open LeiosState s renaming (FFDState to ffds) - l = {!!} -- construct ledger l - in - ∙ FFDAbstract.Fetch FFD.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.FetchRes msgs) - ────────────────────────────────────────────────────────────────────── - just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' ; Ledger = l } , EMPTY) - - Ftch : ∀ {l} → - ──────────────────────────────────── - just s ⇀⟦ FTCH-LDG ⟧ (s , FTCH-LDG l) - - -- 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₁ : ∀ {txs} → let open LeiosState s in - ──────────────────────────────────────────────────────────────────── - just s ⇀⟦ SUBMIT (inj₂ txs) ⟧ (record s { ToPropose = txs } , EMPTY) - - Base₂a : ∀ {bs bs' eb} → let open LeiosState s in - ∙ eb ∈ filterˢ (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) (fromList EBs) - ∙ bs BF.⇀⟦ B.SUBMIT (inj₁ eb) ⟧ (bs' , B.EMPTY) - ──────────────────────────────────────────────────────────────────────────────────── - just s ⇀⟦ SUBMIT (inj₁ eb) ⟧ (s , EMPTY) - - Base₂b : ∀ {bs bs'} → let open LeiosState s renaming (ToPropose to txs) in - ∙ ∅ ≡ filterˢ (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) (fromList EBs) - ∙ bs BF.⇀⟦ B.SUBMIT (inj₂ txs) ⟧ (bs' , B.EMPTY) - ──────────────────────────────────────────────────────────────────────────────────── - just s ⇀⟦ SUBMIT (inj₂ txs) ⟧ (s , EMPTY) - - -- Protocol rules - - IB-Role : let open LeiosState s renaming (ToPropose to txs; FFDState to ffds) - b = GenFFD.ibBody (record { txs = txs }) - h = GenFFD.ibHeader (mkIBHeader slot id π pKey txs) - in - ∙ canProduceIB slot pKey (stake s) -- TODO: let π be the corresponding proof - ∙ FFDAbstract.Send h (just b) FFD.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes) - ───────────────────────────────────────────────────────────────────────── - just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) - - EB-Role : let open LeiosState s renaming (FFDState to ffds) - LI = map {F = List} getIBRef $ setToList $ filterˢ (_∈ᴮ slice L slot (Λ + 1)) (fromList IBs) - LE = map getEBRef $ setToList $ filterˢ (isVote1Certified s) $ - filterˢ (_∈ᴮ slice L slot (μ + 2)) (fromList EBs) - h = mkEB slot id π pKey LI LE - in - ∙ canProduceEB slot pKey (stake s) - ∙ FFDAbstract.Send (GenFFD.ebHeader h) nothing FFD.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes) - ────────────────────────────────────────────────────────────────────────────────────────── - just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) - - V1-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filterˢ (allIBRefsKnown s) $ filterˢ (_∈ᴮ slice L slot (μ + 1)) (fromList EBs) - votes = map (vote ∘ hash) (setToList EBs') - in - ∙ canProduceV1 slot - ∙ FFDAbstract.Send (GenFFD.vHeader votes) nothing FFD.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes) - ───────────────────────────────────────────────────────────────────────────────────────────── - just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) - - V2-Role : let open LeiosState s renaming (FFDState to ffds) - EBs' = filterˢ (vote2Eligible s) $ filterˢ (_∈ᴮ slice L slot 1) (fromList EBs) - votes = map (vote ∘ hash) (setToList EBs') - in - ∙ canProduceV2 slot - ∙ FFDAbstract.Send (GenFFD.vHeader votes) nothing FFD.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes) - ───────────────────────────────────────────────────────────────────────────────────────────── - just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) +module _ (s : LeiosState) where + + open LeiosState s + + upd : Header ⊎ Body → LeiosState + upd (inj₁ (ebHeader eb)) = record s { EBs = eb ∷ EBs } + upd (inj₁ (vHeader vs)) = record s { Vs = vs ∷ Vs } + upd (inj₁ (ibHeader h)) with A.any? (matchIB? h) IBBodies + ... | yes p = + record s + { IBs = record { header = h ; body = A.lookup p } ∷ IBs + ; IBBodies = IBBodies A.─ p + } + ... | no _ = + record s + { IBHeaders = h ∷ IBHeaders + } + upd (inj₂ (ibBody b)) with A.any? (flip matchIB? b) IBHeaders + ... | yes p = + record s + { IBs = record { header = A.lookup p ; body = b } ∷ IBs + ; IBHeaders = IBHeaders A.─ p + } + ... | no _ = + record s + { IBBodies = b ∷ IBBodies + } + +_↑_ : LeiosState → List (Header ⊎ Body) → LeiosState +_↑_ = foldr (flip upd) + +module _ (open Leios.Voting a) (va : VotingAbstract LeiosState) (open VotingAbstract va) + ⦃ _ : ∀ {vs} {eb} → isVote1Certified vs eb ⁇ ⦄ + ⦃ _ : ∀ {vs} {eb} → isVote2Certified vs eb ⁇ ⦄ where + + data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutput → Type where + + -- Initialization + + Init : ∀ {V bs bs' SD ks ks' pks} → + ∙ ks K.⇀⟦ K.INIT pk-IB pk-EB pk-V ⟧ (ks' , K.PUBKEYS pks) + ∙ bs B.⇀⟦ B.INIT (V-chkCerts pks) ⟧ (bs' , B.STAKE SD) + ───────────────────────────────────────────────────────── + nothing ⇀⟦ INIT V ⟧ (initLeiosState V SD , EMPTY) + + -- Network and Ledger + + Slot : ∀ {bs bs' msgs ebs} → let open LeiosState s renaming (FFDState to ffds) in + ∙ bs B.⇀⟦ B.FTCH-LDG ⟧ (bs' , B.BASE-LDG ebs) + ∙ FFD.Fetch FFD.⇀⟦ ffds ⟧ (ffds' , FFD.FetchRes msgs) + ──────────────────────────────────────────────────────────────────────────── + just s ⇀⟦ SLOT ⟧ + (record s + { FFDState = ffds' + ; Ledger = constructLedger ebs + ; slot = suc slot + } ↑ L.filter isValid? msgs + , EMPTY) + + Ftch : let open LeiosState s in + ────────────────────────────────────────── + just s ⇀⟦ FTCH-LDG ⟧ (s , FTCH-LDG Ledger) + + -- 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₁ : ∀ {txs} → let open LeiosState s in + ──────────────────────────────────────────────────────────────────── + just s ⇀⟦ SUBMIT (inj₂ txs) ⟧ (record s { ToPropose = txs } , EMPTY) + + Base₂a : ∀ {bs bs' eb} → let open LeiosState s in + ∙ eb ∈ filterˢ (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) (fromList EBs) + ∙ bs B.⇀⟦ B.SUBMIT (inj₁ eb) ⟧ (bs' , B.EMPTY) + ──────────────────────────────────────────────────────────────────────────────────── + just s ⇀⟦ SUBMIT (inj₁ eb) ⟧ (s , EMPTY) + + Base₂b : ∀ {bs bs'} → let open LeiosState s renaming (ToPropose to txs) in + ∙ ∅ ≡ filterˢ (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) (fromList EBs) + ∙ bs B.⇀⟦ B.SUBMIT (inj₂ txs) ⟧ (bs' , B.EMPTY) + ──────────────────────────────────────────────────────────────────────────────────── + just s ⇀⟦ SUBMIT (inj₂ txs) ⟧ (s , EMPTY) + + -- Protocol rules + + IB-Role : let open LeiosState s renaming (ToPropose to txs; FFDState to ffds) + b = ibBody (record { txs = txs }) + h = ibHeader (mkIBHeader slot id π sk-IB txs) + in + ∙ canProduceIB slot sk-IB (stake s) π + ∙ FFD.Send h (just b) FFD.⇀⟦ ffds ⟧ (ffds' , FFD.SendRes) + ────────────────────────────────────────────────────────────────────── + just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) + + EB-Role : let open LeiosState s renaming (FFDState to ffds) + LI = map {F = List} getIBRef $ setToList $ filterˢ (_∈ᴮ slice L slot (Λ + 1)) (fromList IBs) + LE = map getEBRef $ setToList $ filterˢ (isVote1Certified s) $ + filterˢ (_∈ᴮ slice L slot (μ + 2)) (fromList EBs) + h = mkEB slot id π sk-EB LI LE + in + ∙ canProduceEB slot sk-EB (stake s) π + ∙ FFD.Send (ebHeader h) nothing FFD.⇀⟦ ffds ⟧ (ffds' , FFD.SendRes) + ─────────────────────────────────────────────────────────────────────────────────────── + just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) + + V1-Role : let open LeiosState s renaming (FFDState to ffds) + EBs' = filterˢ (allIBRefsKnown s) $ filterˢ (_∈ᴮ slice L slot (μ + 1)) (fromList EBs) + votes = map (vote sk-V ∘ hash) (setToList EBs') + in + ∙ canProduceV1 slot sk-V (stake s) + ∙ FFD.Send (vHeader votes) nothing FFD.⇀⟦ ffds ⟧ (ffds' , FFD.SendRes) + ────────────────────────────────────────────────────────────────────────────────────────── + just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) + + V2-Role : let open LeiosState s renaming (FFDState to ffds) + EBs' = filterˢ (vote2Eligible s) $ filterˢ (_∈ᴮ slice L slot 1) (fromList EBs) + votes = map (vote sk-V ∘ hash) (setToList EBs') + in + ∙ canProduceV2 slot sk-V (stake s) + ∙ FFD.Send (vHeader votes) nothing FFD.⇀⟦ ffds ⟧ (ffds' , FFD.SendRes) + ────────────────────────────────────────────────────────────────────────────────────────── + just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) diff --git a/formal-spec/Leios/VRF.agda b/formal-spec/Leios/VRF.agda index 109e205..8e751c7 100644 --- a/formal-spec/Leios/VRF.agda +++ b/formal-spec/Leios/VRF.agda @@ -17,16 +17,22 @@ record LeiosVRF : Type₁ where open VRF vrf public -- transforming slot numbers into VRF seeds - field genIBInput genEBInput : ℕ → ℕ + field genIBInput genEBInput genVInput : ℕ → ℕ - canProduceIB : ℕ → PrivKey → ℕ → Type - canProduceIB slot k stake = proj₁ (eval k (genIBInput slot)) < stake + canProduceIB : ℕ → PrivKey → ℕ → VrfPf → Type + canProduceIB slot k stake π = let (val , pf) = eval k (genIBInput slot) in val < stake × pf ≡ π canProduceIBPub : ℕ → ℕ → PubKey → VrfPf → ℕ → Type canProduceIBPub slot val k pf stake = verify k (genIBInput slot) val pf × val < stake - canProduceEB : ℕ → PrivKey → ℕ → Type - canProduceEB slot k stake = proj₁ (eval k (genEBInput slot)) < stake + canProduceEB : ℕ → PrivKey → ℕ → VrfPf → Type + canProduceEB slot k stake π = let (val , pf) = eval k (genEBInput slot) in val < stake × pf ≡ π canProduceEBPub : ℕ → ℕ → PubKey → VrfPf → ℕ → Type canProduceEBPub slot val k pf stake = verify k (genEBInput slot) val pf × val < stake + + canProduceV1 : ℕ → PrivKey → ℕ → Type + canProduceV1 slot k stake = proj₁ (eval k (genVInput slot)) < stake + + canProduceV2 : ℕ → PrivKey → ℕ → Type + canProduceV2 slot k stake = proj₁ (eval k (genVInput slot)) < stake diff --git a/formal-spec/Leios/Voting.agda b/formal-spec/Leios/Voting.agda new file mode 100644 index 0000000..7e9fcf2 --- /dev/null +++ b/formal-spec/Leios/Voting.agda @@ -0,0 +1,12 @@ +{-# OPTIONS --safe #-} + +open import Leios.Prelude +open import Leios.Abstract + +module Leios.Voting (a : LeiosAbstract) (open LeiosAbstract a) where + +open import Leios.Blocks a using (EndorserBlock) + +record VotingAbstract (b : Type) : Type₁ where + field isVote1Certified : b → EndorserBlock → Type + isVote2Certified : b → EndorserBlock → Type