Short-pipeline Leios updates (#97)

input-output-hk · Dec 12, 2024 · 5a39ee3 · 5a39ee3
1 parent 84e8bba
commit 5a39ee3
Show file tree

Hide file tree

Showing 7 changed files with 34 additions and 24 deletions.
diff --git a/formal-spec/Leios/Base.agda b/formal-spec/Leios/Base.agda
@@ -12,6 +12,9 @@ open import Leios.Blocks a using (EndorserBlock)
 StakeDistr : Type
 StakeDistr = PoolID ⇀ ℕ
 
+RankingBlock : Type
+RankingBlock = These EndorserBlock (List Tx)
+
 record BaseAbstract : Type₁ where
   field Cert : Type
         VTy : Type
@@ -20,13 +23,13 @@ record BaseAbstract : Type₁ where
 
   data Input : Type₁ where
     INIT   : (EndorserBlock × Cert → Type) → Input
-    SUBMIT : EndorserBlock ⊎ List Tx → Input -- maybe we have both
+    SUBMIT : RankingBlock → Input
     FTCH-LDG : Input
 
   data Output : Type where
     STAKE : StakeDistr → Output
     EMPTY : Output
-    BASE-LDG : List EndorserBlock → Output
+    BASE-LDG : List RankingBlock → Output
 
   record Functionality : Type₁ where
     field State : Type

diff --git a/formal-spec/Leios/Blocks.agda b/formal-spec/Leios/Blocks.agda
@@ -84,6 +84,12 @@ ibHeaderValid? _ = yes record {}
 ibBodyValid? : (b : IBBody) → Dec (ibBodyValid b)
 ibBodyValid? _ = yes record {}
 
+ibValid : InputBlock → Type
+ibValid record { header = h ; body = b } = ibHeaderValid h × ibBodyValid b
+
+ibValid? : (ib : InputBlock) → Dec (ibValid ib)
+ibValid? record { header = h ; body = b } = ibHeaderValid? h ×-dec ibBodyValid? b
+
 --------------------------------------------------------------------------------
 -- Endorser Blocks
 --------------------------------------------------------------------------------

diff --git a/formal-spec/Leios/FFD.agda b/formal-spec/Leios/FFD.agda
@@ -3,7 +3,6 @@
 module Leios.FFD where
 
 open import Leios.Prelude
-open import Leios.Abstract
 
 record FFDAbstract : Type₁ where
   field Header Body ID : Type

diff --git a/formal-spec/Leios/Prelude.agda b/formal-spec/Leios/Prelude.agda
@@ -11,7 +11,17 @@ open import Class.HasOrder public
 open import Class.Hashable public
 open import Prelude.InferenceRules public
 
-import Data.List as L
+module T where
+  open import Data.These public
+open T public using (These; this; that)
+
+module L where
+  open import Data.List public
+open L public using (List; []; _∷_; _++_; catMaybes; head; length; sum; and; or; any)
+
+module A where
+  open import Data.List.Relation.Unary.Any public
+open A public using (here; there)
 
 fromTo : ℕ → ℕ → List ℕ
 fromTo m n = map (_+ m) (upTo (n ∸ m))

diff --git a/formal-spec/Leios/Protocol.agda b/formal-spec/Leios/Protocol.agda
@@ -2,10 +2,6 @@
 
 open import Leios.Prelude hiding (id)
 open import Leios.FFD
-
-import Data.List as L
-import Data.List.Relation.Unary.Any as A
-
 open import Leios.SpecStructure
 
 module Leios.Protocol (⋯ : SpecStructure) (let open SpecStructure ⋯) (SlotUpkeep : Type) where
@@ -64,8 +60,8 @@ record LeiosState : Type where
           open IBBody
           open InputBlock
 
-  constructLedger : List EndorserBlock → List Tx
-  constructLedger = concatMap lookupTxs
+  constructLedger : List RankingBlock → List Tx
+  constructLedger = L.concat ∘ L.map (T.mergeThese L._++_ ∘ T.map₁ lookupTxs)
 
   needsUpkeep : SlotUpkeep → Set
   needsUpkeep = _∉ Upkeep

diff --git a/formal-spec/Leios/Simplified.agda b/formal-spec/Leios/Simplified.agda
@@ -4,8 +4,6 @@ open import Leios.Prelude hiding (id)
 open import Leios.FFD
 open import Leios.SpecStructure
 
-import Data.List as L
-
 module Leios.Simplified (⋯ : SpecStructure) (let open SpecStructure ⋯) (Λ μ : ℕ) where
 
 data SlotUpkeep : Type where
@@ -47,7 +45,7 @@ module Protocol (va : VotingAbstract) (let open VotingAbstract va) where
                    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
@@ -137,12 +135,12 @@ module Protocol (va : VotingAbstract) (let open VotingAbstract va) where
 
     Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) 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'
          ───────────────────────────────────────────────────────────────────────
          just s -⟦ SLOT / EMPTY ⟧⇀ record s
              { FFDState = ffds'
-             ; Ledger   = constructLedger ebs
+             ; Ledger   = constructLedger rbs
              ; slot     = suc slot
              ; Upkeep   = ∅
              } ↑ L.filter isValid? msgs
@@ -164,14 +162,14 @@ module Protocol (va : VotingAbstract) (let open VotingAbstract va) where
     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 (inj₁ eb) / B.EMPTY ⟧⇀ bs'
+            ∙ 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 (inj₂ ToPropose) / B.EMPTY ⟧⇀ bs'
+            ∙ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs'
             ───────────────────────────────────────────────────────────────────────
             just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s Base
 

diff --git a/formal-spec/Leios/UniformShort.agda b/formal-spec/Leios/UniformShort.agda
@@ -4,8 +4,6 @@ open import Leios.Prelude hiding (id)
 open import Leios.FFD
 open import Leios.SpecStructure
 
-import Data.List as L
-
 module Leios.UniformShort (⋯ : SpecStructure) (let open SpecStructure ⋯) where
 
 data SlotUpkeep : Type where
@@ -33,7 +31,7 @@ module Protocol (va : VotingAbstract) (let open VotingAbstract va) where
                    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
@@ -112,12 +110,12 @@ module Protocol (va : VotingAbstract) (let open VotingAbstract va) where
 
     Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) 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'
          ───────────────────────────────────────────────────────────────────────
          just s -⟦ SLOT / EMPTY ⟧⇀ record s
              { FFDState = ffds'
-             ; Ledger   = constructLedger ebs
+             ; Ledger   = constructLedger rbs
              ; slot     = suc slot
              ; Upkeep   = ∅
              } ↑ L.filter isValid? msgs
@@ -139,14 +137,14 @@ module Protocol (va : VotingAbstract) (let open VotingAbstract va) where
     Base₂a  : let open LeiosState s renaming (BaseState to bs) in
             ∙ needsUpkeep Base
             ∙ eb ∈ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs
-            ∙ bs B.-⟦ B.SUBMIT (inj₁ eb) / B.EMPTY ⟧⇀ bs'
+            ∙ 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 → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs
-            ∙ bs B.-⟦ B.SUBMIT (inj₂ ToPropose) / B.EMPTY ⟧⇀ bs'
+            ∙ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs'
             ───────────────────────────────────────────────────────────────────────
             just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s Base