WIP: add reference implementation

formal-spec/Class/Computational22.agda

@@ -0,0 +1,35 @@
+{-# OPTIONS --safe #-}
+
+--------------------------------------------------------------------------------
+-- Variant of `Computational` for relations with two inputs and outputs
+--------------------------------------------------------------------------------
+
+module Class.Computational22 where
+
+open import Leios.Prelude
+open import Class.Computational
+
+private variable
+  S I O Err : Type
+
+module _ (STS : S → I → O → S → Type) where
+  record Computational22 Err : Type₁ where
+    constructor MkComputational
+    field
+      computeProof : (s : S) (i : I) → ComputationResult Err (∃[ (o , s') ] STS s i o s')
+
+    compute : S → I → ComputationResult Err (O × S)
+    compute s i = map proj₁ $ computeProof s i
+
+    field
+      completeness : ∀ s i o s' → STS s i o s' → compute s i ≡ success (o , s')
+
+  STS' : S × I → O × S → Type
+  STS' (s , i) (o , s') = STS s i o s'
+
+  module _ ⦃ _ : Computational22 Err ⦄ where
+    open Computational22 it
+    instance
+      comp22⇒comp : Computational STS' Err
+      comp22⇒comp .Computational.computeProof (s , i)          = computeProof s i
+      comp22⇒comp .Computational.completeness (s , i) (o , s') = completeness s i o s'

formal-spec/Everything.agda

@@ -1,6 +1,4 @@
-{-# OPTIONS --erasure #-}
-
 module Everything where
 
-open import Leios.SimpleSpec
+open import Leios.Simple
 open import Leios.Network

formal-spec/Leios/Base.agda

@@ -16,10 +16,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 : EndorserBlock ⊎ List Tx → Input -- maybe we have both
     FTCH-LDG : Input
 
@@ -31,6 +31,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

formal-spec/Leios/FFD.agda

@@ -22,6 +22,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

formal-spec/Leios/Prelude.agda

@@ -11,9 +11,25 @@ open import Class.HasOrder public
 open import Class.Hashable public
 open import Prelude.InferenceRules public
 
+import Data.List as L
+
 fromTo : ℕ → ℕ → List ℕ
 fromTo m n = map (_+ m) (upTo (n ∸ m))
 
 slice : (L : ℕ) → ⦃ NonZero L ⦄ → ℕ → ℕ → ℙ ℕ
 slice L s x = fromList (fromTo s' (s' + (L ∸ 1)))
   where s' = ((s / L) ∸ x) * L -- equivalent to the formula in the paper
+
+filter : {A : Set} → (P : A → Type) ⦃ _ : P ⁇¹ ⦄ → List A → List A
+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))

formal-spec/Leios/Simple.agda

@@ -0,0 +1,295 @@
+{-# OPTIONS --safe #-}
+
+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
+
+open import Tactic.Defaults
+open import Tactic.Derive.DecEq
+
+module Leios.Simple (⋯ : SpecStructure) (let open SpecStructure ⋯) where
+
+open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot)
+open GenFFD
+
+-- High level structure:
+
+
+--                                      (simple) Leios
+--                                        /         |
+-- +-------------------------------------+          |
+-- | Header Diffusion     Body Diffusion |          |
+-- +-------------------------------------+       Base Protocol
+--                                        \      /
+--                                        Network
+
+data LeiosInput : Type where
+  INIT     : VTy → LeiosInput
+  SUBMIT   : List Tx → LeiosInput
+  SLOT     : LeiosInput
+  FTCH-LDG : LeiosInput
+
+data LeiosOutput : Type where
+  FTCH-LDG : List Tx → LeiosOutput
+  EMPTY    : LeiosOutput
+
+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 ∷ [])
+
+record LeiosState : Type where
+  field V         : VTy
+        SD        : StakeDistr
+        FFDState  : FFD.State
+        Ledger    : List Tx -- TODO: maybe be more generic here
+        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
+
+  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
+
+  -- TODO: stop once a single reference doesn't resolve
+  constructLedger : List EndorserBlock → List Tx
+  constructLedger = concatMap lookupTxs
+
+  needsUpkeep : SlotUpkeep → Set
+  needsUpkeep = _∉ Upkeep
+
+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
+  { V           = V
+  ; SD          = SD
+  ; FFDState    = FFD.initFFDState
+  ; Ledger      = []
+  ; ToPropose   = []
+  ; IBs         = []
+  ; EBs         = []
+  ; Vs          = []
+  ; slot        = initSlot V
+  ; IBHeaders   = []
+  ; IBBodies    = []
+  ; Upkeep      = ∅
+  ; BaseState   = bs
+  ; votingState = initVotingState
+  }
+
+-- some predicates about EBs
+module _ (s : LeiosState) (eb : EndorserBlock) where
+  open EndorserBlockOSig eb
+  open LeiosState s
+
+  vote2Eligible : Type
+  vote2Eligible = length ebRefs ≥ lengthˢ candidateEBs / 2 -- should this be `>`?
+                × fromList ebRefs ⊆ candidateEBs
+    where candidateEBs : ℙ Hash
+          candidateEBs = mapˢ getEBRef $ filterˢ (_∈ᴮ slice L slot (μ + 3)) (fromList EBs)
+
+  allIBRefsKnown : Type
+  allIBRefsKnown = ∀[ ref ∈ fromList ibRefs ] ref ∈ˡ map getIBRef IBs
+
+stake : LeiosState → ℕ
+stake record { SD = SD } = case lookupᵐ? SD id of λ where
+  (just s) → s
+  nothing  → 0
+
+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
+      }
+
+infix 25 _↑_
+_↑_ : LeiosState → List (Header ⊎ Body) → LeiosState
+_↑_ = foldr (flip upd)
+
+open FFD hiding (_-⟦_/_⟧⇀_)
+
+private variable s      : LeiosState
+                 ffds'  : FFD.State
+                 π      : VrfPf
+                 bs'    : B.State
+                 ks ks' : K.State
+                 msgs   : List (FFDAbstract.Header ffdAbstract ⊎ FFDAbstract.Body ffdAbstract)
+                 eb     : EndorserBlock
+                 ebs    : List EndorserBlock
+                 txs    : List Tx
+                 V      : VTy
+                 SD     : StakeDistr
+                 pks    : List PubKey
+
+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 ebs ⟧⇀ bs'
+       ∙ ffds FFD.-⟦ Fetch / FetchRes msgs ⟧⇀ ffds'
+       ───────────────────────────────────────────────────────────────────────
+       just s -⟦ SLOT / EMPTY ⟧⇀ record s
+           { FFDState  = ffds'
+           ; Ledger    = constructLedger ebs
+           ; slot      = suc slot
+           ; BaseState = bs'
+           ; 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 txs / EMPTY ⟧⇀ record s { ToPropose = txs }
+
+  Base₂a  : let open LeiosState s renaming (BaseState to bs) in
+          ∙ needsUpkeep Base
+          ∙ eb ∈ filter (λ eb → isVote2Certified votingState eb × eb ∈ᴮ slice L slot 2) EBs
+          ∙ bs B.-⟦ B.SUBMIT (inj₁ 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 votingState eb × eb ∈ᴮ slice L slot 2) EBs
+          ∙ bs B.-⟦ B.SUBMIT (inj₂ ToPropose) / B.EMPTY ⟧⇀ bs'
+          ───────────────────────────────────────────────────────────────────────
+          just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base
+
+  -- Protocol rules
+
+  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'
+          ─────────────────────────────────────────────────────────────────────────
+          just s -⟦ SLOT / EMPTY ⟧⇀ 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 votingState) $
+                           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'
+          ─────────────────────────────────────────────────────────────────────────
+          just s -⟦ SLOT / EMPTY ⟧⇀ 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'
+          ─────────────────────────────────────────────────────────────────────────
+          just s -⟦ SLOT / EMPTY ⟧⇀ 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'
+          ─────────────────────────────────────────────────────────────────────────
+          just s -⟦ SLOT / EMPTY ⟧⇀ 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) π)
+          ───────────────────────────────────────────────
+          just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s IB-Role
+
+  No-EB-Role : let open LeiosState s in
+          ∙ needsUpkeep EB-Role
+          ∙ (∀ π → ¬ canProduceEB slot sk-EB (stake s) π)
+          ───────────────────────────────────────────────
+          just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s EB-Role
+
+  No-V1-Role : let open LeiosState s in
+          ∙ needsUpkeep V1-Role
+          ∙ ¬ canProduceV1 slot sk-V (stake s)
+          ─────────────────────────────────────────────
+          just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s V1-Role
+
+  No-V2-Role : let open LeiosState s in
+          ∙ needsUpkeep V2-Role
+          ∙ ¬ canProduceV2 slot sk-V (stake s)
+          ─────────────────────────────────────────────
+          just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s V2-Role