diff --git a/formal-spec/Leios/Base.agda b/formal-spec/Leios/Base.agda index f2c0430a..3402ba76 100644 --- a/formal-spec/Leios/Base.agda +++ b/formal-spec/Leios/Base.agda @@ -21,7 +21,7 @@ record BaseAbstract : Type₁ where initSlot : VTy → ℕ V-chkCerts : List PubKey → EndorserBlock × Cert → Bool - data Input : Type₁ where + data Input : Type where INIT : (EndorserBlock × Cert → Bool) → Input SUBMIT : RankingBlock → Input FTCH-LDG : Input diff --git a/formal-spec/Leios/Protocol.agda b/formal-spec/Leios/Protocol.agda index 3ca3fbc5..20fb11f5 100644 --- a/formal-spec/Leios/Protocol.agda +++ b/formal-spec/Leios/Protocol.agda @@ -69,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 diff --git a/formal-spec/Leios/Simple/Deterministic.agda b/formal-spec/Leios/Simple/Deterministic.agda index 45652645..c8cd7d2f 100644 --- a/formal-spec/Leios/Simple/Deterministic.agda +++ b/formal-spec/Leios/Simple/Deterministic.agda @@ -13,11 +13,11 @@ open import Data.List.Relation.Unary.Any using (here) open import Leios.SpecStructure -module Leios.Simple.Deterministic (⋯ : SpecStructure) (let open SpecStructure ⋯) where +module Leios.Simple.Deterministic (⋯ : SpecStructure 2) (let open SpecStructure ⋯) (Λ μ : ℕ) where -import Leios.Simple -open import Leios.Simple ⋯ hiding (_-⟦_/_⟧⇀_) -module ND = Leios.Simple ⋯ +import Leios.Simplified +open import Leios.Simplified ⋯ Λ μ hiding (_-⟦_/_⟧⇀_) +module ND = Leios.Simplified ⋯ Λ μ open import Class.Computational open import Class.Computational22 @@ -37,7 +37,7 @@ private variable s s' s0 s1 s2 s3 s4 s5 : LeiosState ks ks' : K.State msgs : List (FFDAbstract.Header ffdAbstract ⊎ FFDAbstract.Body ffdAbstract) eb : EndorserBlock - ebs : List EndorserBlock + rbs : List RankingBlock txs : List Tx V : VTy SD : StakeDistr @@ -61,15 +61,15 @@ data _-⟦Base⟧⇀_ : LeiosState → LeiosState → Type where Base₂a : ∀ {ebs} → let open LeiosState s renaming (BaseState to bs) in ∙ needsUpkeep Base - ∙ eb ∷ ebs ≡ filter (λ eb → isVote2Certified votingState eb × eb ∈ᴮ slice L slot 2) EBs - ∙ bs B.-⟦ B.SUBMIT (inj₁ eb) / B.EMPTY ⟧⇀ bs' + ∙ eb ∷ ebs ≡ filter (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs + ∙ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs' ─────────────────────────────────────────────────────────────────────── s -⟦Base⟧⇀ addUpkeep record s { BaseState = bs' } Base Base₂b : let open LeiosState s renaming (BaseState to bs) in ∙ needsUpkeep Base - ∙ [] ≡ filter (λ eb → isVote2Certified votingState eb × eb ∈ᴮ slice L slot 2) EBs - ∙ bs B.-⟦ B.SUBMIT (inj₂ ToPropose) / B.EMPTY ⟧⇀ bs' + ∙ [] ≡ filter (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs + ∙ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs' ─────────────────────────────────────────────────────────────────────── s -⟦Base⟧⇀ addUpkeep record s { BaseState = bs' } Base @@ -80,7 +80,7 @@ Base⇒ND (Base₂b x x₁ x₂) = Base₂b x x₁ x₂ opaque Base-total : LeiosState.needsUpkeep s Base → ∃[ s' ] s -⟦Base⟧⇀ s' Base-total {s = s} needsUpkeep with - (let open LeiosState s in filter (λ eb → isVote2Certified votingState eb × eb ∈ᴮ slice L slot 2) EBs) + (let open LeiosState s in filter (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs) in eq ... | [] = -, Base₂b needsUpkeep (sym eq) (proj₂ B.SUBMIT-total) ... | x ∷ l = -, Base₂a needsUpkeep (sym eq) (proj₂ B.SUBMIT-total) @@ -108,8 +108,8 @@ data _-⟦IB-Role⟧⇀_ : LeiosState → LeiosState → Type where s -⟦IB-Role⟧⇀ addUpkeep s IB-Role IB-Role⇒ND : s -⟦IB-Role⟧⇀ s' → just s ND.-⟦ SLOT / EMPTY ⟧⇀ s' -IB-Role⇒ND (IB-Role x x₁ x₂) = IB-Role x x₁ x₂ -IB-Role⇒ND (No-IB-Role x x₁) = No-IB-Role x x₁ +IB-Role⇒ND (IB-Role x x₁ x₂) = Roles (IB-Role x x₁ x₂) +IB-Role⇒ND (No-IB-Role x x₁) = Roles (No-IB-Role x x₁) opaque IB-Role-total : LeiosState.needsUpkeep s IB-Role → ∃[ s' ] s -⟦IB-Role⟧⇀ s' @@ -125,7 +125,7 @@ data _-⟦EB-Role⟧⇀_ : LeiosState → LeiosState → Type where EB-Role : let open LeiosState s renaming (FFDState to ffds) LI = map getIBRef $ filter (_∈ᴮ slice L slot (Λ + 1)) IBs - LE = map getEBRef $ filter (isVote1Certified votingState) $ + LE = map getEBRef $ filter (isVote1Certified s) $ filter (_∈ᴮ slice L slot (μ + 2)) EBs h = mkEB slot id π sk-EB LI LE in @@ -142,8 +142,8 @@ data _-⟦EB-Role⟧⇀_ : LeiosState → LeiosState → Type where s -⟦EB-Role⟧⇀ addUpkeep s EB-Role EB-Role⇒ND : s -⟦EB-Role⟧⇀ s' → just s ND.-⟦ SLOT / EMPTY ⟧⇀ s' -EB-Role⇒ND (EB-Role x x₁ x₂) = EB-Role x x₁ x₂ -EB-Role⇒ND (No-EB-Role x x₁) = No-EB-Role x x₁ +EB-Role⇒ND (EB-Role x x₁ x₂) = Roles (EB-Role x x₁ x₂) +EB-Role⇒ND (No-EB-Role x x₁) = Roles (No-EB-Role x x₁) opaque EB-Role-total : LeiosState.needsUpkeep s EB-Role → ∃[ s' ] s -⟦EB-Role⟧⇀ s' @@ -172,8 +172,8 @@ data _-⟦V1-Role⟧⇀_ : LeiosState → LeiosState → Type where s -⟦V1-Role⟧⇀ addUpkeep s V1-Role V1-Role⇒ND : s -⟦V1-Role⟧⇀ s' → just s ND.-⟦ SLOT / EMPTY ⟧⇀ s' -V1-Role⇒ND (V1-Role x x₁ x₂) = V1-Role x x₁ x₂ -V1-Role⇒ND (No-V1-Role x x₁) = No-V1-Role x x₁ +V1-Role⇒ND (V1-Role x x₁ x₂) = Roles (V1-Role x x₁ x₂) +V1-Role⇒ND (No-V1-Role x x₁) = Roles (No-V1-Role x x₁) V1-Role-Upkeep : s -⟦V1-Role⟧⇀ s' → LeiosState.needsUpkeep s V1-Role × ¬ LeiosState.needsUpkeep s' V1-Role V1-Role-Upkeep (V1-Role x x₁ x₂) = x , addUpkeep⇒¬needsUpkeep @@ -198,8 +198,8 @@ data _-⟦V2-Role⟧⇀_ : LeiosState → LeiosState → Type where s -⟦V2-Role⟧⇀ addUpkeep s V2-Role V2-Role⇒ND : s -⟦V2-Role⟧⇀ s' → just s ND.-⟦ SLOT / EMPTY ⟧⇀ s' -V2-Role⇒ND (V2-Role x x₁ x₂) = V2-Role x x₁ x₂ -V2-Role⇒ND (No-V2-Role x x₁) = No-V2-Role x x₁ +V2-Role⇒ND (V2-Role x x₁ x₂) = Roles (V2-Role x x₁ x₂) +V2-Role⇒ND (No-V2-Role x x₁) = Roles (No-V2-Role x x₁) V2-Role-Upkeep : s -⟦V2-Role⟧⇀ s' → LeiosState.needsUpkeep s V2-Role × ¬ LeiosState.needsUpkeep s' V2-Role V2-Role-Upkeep (V2-Role x x₁ x₂) = x , addUpkeep⇒¬needsUpkeep @@ -215,14 +215,14 @@ data _-⟦_/_⟧⇀_ : LeiosState → LeiosInput → LeiosOutput → LeiosState Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) s0 = record s { FFDState = ffds' - ; Ledger = constructLedger ebs + ; Ledger = constructLedger rbs ; slot = suc slot ; Upkeep = ∅ ; BaseState = bs' } ↑ L.filter isValid? msgs in ∙ Upkeep ≡ᵉ allUpkeep - ∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG ebs ⟧⇀ bs' + ∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs' ∙ ffds FFD.-⟦ Fetch / FetchRes msgs ⟧⇀ ffds' ∙ s0 -⟦Base⟧⇀ s1 ∙ s1 -⟦IB-Role⟧⇀ s2 @@ -244,7 +244,7 @@ data _-⟦_/_⟧⇀_ : LeiosState → LeiosInput → LeiosOutput → LeiosState Base₁ : ────────────────────────────────────────────────────────────── - s -⟦ SUBMIT txs / EMPTY ⟧⇀ record s { ToPropose = txs } + s -⟦ SUBMIT (inj₂ txs) / EMPTY ⟧⇀ record s { ToPropose = txs } -- Protocol rules @@ -275,7 +275,7 @@ module _ ⦃ Computational-B : Computational22 B._-⟦_/_⟧⇀_ String ⦄ instance Computational--⟦/⟧⇀ : Computational22 _-⟦_/_⟧⇀_ String Computational--⟦/⟧⇀ .computeProof s (INIT x) = failure "No handling of INIT here" - Computational--⟦/⟧⇀ .computeProof s (SUBMIT _) = success (-, Base₁) + Computational--⟦/⟧⇀ .computeProof s (SUBMIT _) = success {!(-, Base₁)!} Computational--⟦/⟧⇀ .computeProof s SLOT = let open LeiosState s in case (¿ Upkeep ≡ᵉ allUpkeep ¿ ,′ computeProof BaseState B.FTCH-LDG ,′ computeProof FFDState FFD.Fetch) of λ where (yes p , success ((B.BASE-LDG l , bs) , p₁) , success ((FFD.FetchRes msgs , ffds) , p₂)) → diff --git a/formal-spec/Leios/Simplified.agda b/formal-spec/Leios/Simplified.agda index 960eaefb..d5c38ac7 100644 --- a/formal-spec/Leios/Simplified.agda +++ b/formal-spec/Leios/Simplified.agda @@ -5,11 +5,16 @@ open import Leios.FFD open import Leios.SpecStructure open import Data.Fin.Patterns +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 ∷ []) @@ -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 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/VRF.agda b/formal-spec/Leios/VRF.agda index 11bfcc71..8aae1cff 100644 --- a/formal-spec/Leios/VRF.agda +++ b/formal-spec/Leios/VRF.agda @@ -17,7 +17,7 @@ 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 ≡ π @@ -39,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