Linear Leios trace verifier

formal-spec/Everything.agda

@@ -46,11 +46,11 @@ open import Leios.Foreign.Types
 open import Leios.Foreign.Util
 open import Leios.KeyRegistration
 open import Leios.Linear
+open import Leios.Linear.Trace.Verifier
 -- open import Leios.Network
 open import Leios.Prelude
 open import Leios.Protocol
 -- open import Leios.Short
--- TODO: drop Deterministic
 -- open import Leios.Short.Deterministic
 -- open import Leios.Short.Trace.Verifier
 -- open import Leios.Short.Trace.Verifier.Test
@@ -66,3 +66,5 @@ open import StateMachine
 -- Networking
 open import Network.BasicBroadcast
 -- open import Network.Leios
+
+open import Prelude.Result

formal-spec/Leios/Defaults.agda

@@ -137,7 +137,7 @@ instance
   hhs .hash = IBHeaderOSig.bodyHash
 
   hpe : Hashable PreEndorserBlock (List ℕ)
-  hpe .hash = L.concat ∘ EndorserBlockOSig.ibRefs
+  hpe .hash = EndorserBlockOSig.txs
 
 record FFDBuffers : Type where
   field inIBs : List InputBlock

formal-spec/Leios/Linear.lagda.md

@@ -102,7 +102,7 @@ isEquivocated s eb = Any (areEquivocated eb) (toSet (LeiosState.EBs s))
 rememberVote : LeiosState → EndorserBlock → LeiosState
 rememberVote s@(record { VotedEBs = vebs }) eb = record s { VotedEBs = hash eb ∷ vebs }
 
-data _↝_ : LeiosState → LeiosState × FFDAbstract.Input ffdAbstract → Type where
+data _↝_ : LeiosState → LeiosState × Maybe (FFDAbstract.Input ffdAbstract) → Type where
 ```
 #### Positive rules
 
@@ -117,14 +117,20 @@ mempool.
           ∙ toProposeEB s π ≡ just eb
           ∙ canProduceEB slot sk-EB (stake s) π
           ──────────────────────────────────────────────────────
-          s ↝ (addUpkeep s EB-Role , Send (ebHeader eb) nothing)
+          s ↝ (addUpkeep s EB-Role , just (Send (ebHeader eb) nothing))
+
+  No-EB-Role : let open LeiosState s in
+             ∙ needsUpkeep EB-Role
+             ∙ (∀ π → ¬ canProduceEB slot sk-EB (stake s) π)
+             ─────────────────────────────────────────────
+             s ↝ (addUpkeep s EB-Role , nothing)
 ```
 ```agda
   VT-Role : ∀ {ebHash slot'}
           → let open LeiosState s
           in
           ∙ getCurrentEBHash s ≡ just ebHash
-          ∙ find (λ (s , eb) → hash eb ≟ ebHash) EBs' ≡ just (slot' , eb)
+          ∙ find (λ (_ , eb') → hash eb' ≟ ebHash) EBs' ≡ just (slot' , eb)
           ∙ hash eb ∉ VotedEBs
           ∙ ¬ isEquivocated s eb
           ∙ isValid s (inj₁ (ebHeader eb))
@@ -134,16 +140,22 @@ mempool.
           ∙ validityCheckTime eb ≤ 3 * Lhdr + Lvote
           ∙ EndorserBlockOSig.txs eb ≢ []
           ∙ needsUpkeep VT-Role
-          ∙ canProduceV (slotNumber eb) sk-VT (stake s)
+          ∙ canProduceV slot sk-VT (stake s)
           ───────────────────────────────────────────────────────
           s ↝ ( rememberVote (addUpkeep s VT-Role) eb
-              , Send (vtHeader [ vote sk-VT (hash eb) ]) nothing)
+              , just (Send (vtHeader [ vote sk-VT (hash eb) ]) nothing))
+
+  No-VT-Role : let open LeiosState s in
+             ∙ needsUpkeep VT-Role
+             ∙ ¬ canProduceV slot sk-VT (stake s)
+             ─────────────────────────────────────────────
+             s ↝ (addUpkeep s VT-Role , nothing)
 ```
 Predicate needed for slot transition. Special care needs to be taken when starting from
 genesis.
 ```agda
 allDone : LeiosState → Type
-allDone record { Upkeep = u } = fromList u ≡ᵉ fromList (EB-Role ∷ VT-Role ∷ Base ∷ [])
+allDone record { Upkeep = u } = u ≡ᵉ fromList (VT-Role ∷ EB-Role ∷ Base ∷ [])
 ```
 ### Linear Leios transitions
 The relation describing the transition given input and state
@@ -168,7 +180,7 @@ data _-⟦_/_⟧⇀_ : MachineType (FFD ⊗ BaseC) (IO ⊗ Adv) LeiosState where
         ───────────────────────────────────────────────────────────────────────────────────
         s -⟦ honestOutputI (rcvˡ (-, FFD-OUT msgs)) / honestInputO' (sndʳ (-, FTCH-LDG)) ⟧⇀
           record s { slot         = suc slot
-                   ; Upkeep       = []
+                   ; Upkeep       = ∅
                    } ↑ L.filter (isValid? s) msgs
 
   Slot₂ : let open LeiosState s in
@@ -209,13 +221,12 @@ Note: Submitted data to the base chain is only taken into account
 #### Protocol rules
 ```agda
   Roles₁ :
-         ∙ s ↝ (s' , i)
+         ∙ s ↝ (s' , just i)
          ──────────────────────────────────────────────────────────────────────────────
          s -⟦ honestOutputI (rcvˡ (-, SLOT)) / honestInputO' (sndˡ (-, FFD-IN i)) ⟧⇀ s'
 
-  Roles₂ : ∀ {x u s'} → let open LeiosState s in
-         ∙ ¬ (s ↝ (s' , x))
-         ∙ needsUpkeep u
+  Roles₂ : ∀ {u} → let open LeiosState s in
+         ∙ s ↝ (s' , nothing)
          ∙ u ≢ Base
          ──────────────────────────────────────────────────────────────
          s -⟦ honestOutputI (rcvˡ (-, SLOT)) / nothing ⟧⇀ addUpkeep s u
@@ -228,8 +239,15 @@ ShortLeios .Machine.stepRel = _-⟦_/_⟧⇀_
 
 open import Prelude.STS.GenPremises
 
+{-
+instance
+  Dec-isValid : ∀ {s x} → isValid s x ⁇
+  Dec-isValid {s} {x} .dec = isValid? s x
+-}
+
 unquoteDecl EB-Role-premises = genPremises EB-Role-premises (quote _↝_.EB-Role)
 unquoteDecl VT-Role-premises = genPremises VT-Role-premises (quote _↝_.VT-Role)
+unquoteDecl No-VT-Role-premises = genPremises No-VT-Role-premises (quote _↝_.No-VT-Role)
 
 unquoteDecl Slot₁-premises = genPremises Slot₁-premises (quote Slot₁)
 unquoteDecl Slot₂-premises = genPremises Slot₂-premises (quote Slot₂)

formal-spec/Leios/Linear/Trace/Verifier.agda

@@ -0,0 +1,224 @@
+open import Leios.Prelude hiding (id; _>>=_; return)
+open import Leios.Config
+open import Leios.SpecStructure using (SpecStructure)
+
+open import Prelude.Result
+open import CategoricalCrypto hiding (id; _∘_)
+
+module Leios.Linear.Trace.Verifier (params : Params) where
+
+-- SpecStructure is not a module parameter, as the type for VrfPf needs to be known
+open import Leios.Defaults params using (d-SpecStructure; isb; hpe) public
+open SpecStructure d-SpecStructure hiding (Hashable-IBHeader; Hashable-EndorserBlock; isVoteCertified) public
+
+module Defaults
+  (Lhdr Lvote Ldiff : ℕ)
+  (splitTxs : List Tx → List Tx × List Tx)
+  (validityCheckTime : EndorserBlock → ℕ)
+  where
+
+  open import Leios.Linear d-SpecStructure params Lhdr Lvote Ldiff splitTxs validityCheckTime public
+  open GenFFD
+  open Types params
+
+  data Action : Type where
+    EB-Role-Action    : ℕ → EndorserBlock → Action
+    VT-Role-Action    : ℕ → EndorserBlock → ℕ → Action
+    Ftch-Action       : ℕ → Action
+    Slot₁-Action      : ℕ → Action
+    Slot₂-Action      : ℕ → Action
+    Base₁-Action      : ℕ → Action
+    Base₂-Action      : ℕ → Action
+    No-EB-Role-Action : ℕ → Action
+    No-VT-Role-Action : ℕ → Action
+
+  TestTrace = List (Action × (FFDT Out ⊎ BaseT Out ⊎ IOT In))
+
+  private variable
+    s s′ : LeiosState
+    σ    : Action
+    σs   : TestTrace
+    ib   : InputBlock
+    eb   : EndorserBlock
+    ebs  : List EndorserBlock
+    vt   : List Vote
+    i    : FFDT Out ⊎ BaseT Out ⊎ IOT In
+    o    : FFDT In
+
+  open LeiosState
+
+  getAction : ∀ {i o} → s -⟦ i / o ⟧⇀ s′ → Action
+  getAction (Slot₁ {s} _)                      = Slot₁-Action (slot s)
+  getAction (Slot₂ {s})                        = Slot₂-Action (slot s)
+  getAction (Ftch {s})                         = Ftch-Action (slot s)
+  getAction (Base₁ {s})                        = Base₁-Action (slot s)
+  getAction (Base₂ {s} _)                      = Base₂-Action (slot s)
+  getAction (Roles₁ (VT-Role {s} {eb = eb} {slot' = slot'} _)) = VT-Role-Action (slot s) eb slot'
+  getAction (Roles₁ (EB-Role {s} {eb = eb} _)) = EB-Role-Action (slot s) eb
+  getAction (Roles₂ {u = Base} (_ , x))        = ⊥-elim (x refl)
+  getAction (Roles₂ {s} {u = EB-Role} _)       = No-EB-Role-Action (slot s)
+  getAction (Roles₂ {s} {u = VT-Role} _)       = No-VT-Role-Action (slot s)
+
+  getSlot : Action → ℕ
+  getSlot (EB-Role-Action x _) = x
+  getSlot (VT-Role-Action x _ _) = x
+  getSlot (No-EB-Role-Action x) = x
+  getSlot (No-VT-Role-Action x) = x
+  getSlot (Ftch-Action x) = x
+  getSlot (Slot₁-Action x) = x
+  getSlot (Slot₂-Action x) = x
+  getSlot (Base₁-Action x) = x
+  getSlot (Base₂-Action x) = x
+
+
+  data Err-verifyAction (σ : Action) (i : FFDT Out ⊎ BaseT Out ⊎ IOT In) (s : LeiosState) : Type where
+    E-Err-Slot : getSlot σ ≢ slot s → Err-verifyAction σ i s
+    E-Err-CanProduceIB : (∀ π → ¬ canProduceIB (slot s) sk-IB (stake s) π) → Err-verifyAction σ i s
+    dummyErr : Err-verifyAction σ i s
+
+  -- NOTE: this goes backwards, from the current state to the initial state
+  data _—→_ : LeiosState → LeiosState → Type where
+
+    ActionStep : ∀ {s i o s′} →
+      ∙ s -⟦ i / o ⟧⇀ s′
+        ───────────────────
+        s′ —→ s
+
+  open import Prelude.Closures _—→_
+
+  infix 0 _≈_ _≈¹_
+
+  data _≈¹_ : Action × (FFDT Out ⊎ BaseT Out ⊎ IOT In) → s′ —→ s → Type where
+
+    FromAction¹ :
+      ∀ i {s′ o}
+        → (σ : s -⟦ honestOutputI (rcvˡ (-, i)) / o ⟧⇀ s′)
+        → (getAction σ , inj₁ i) ≈¹ ActionStep σ
+
+    FromAction² :
+      ∀ i {s′ o}
+        → (σ : s -⟦ honestOutputI (rcvʳ (-, i)) / o ⟧⇀ s′)
+        → (getAction σ , inj₂ (inj₁ i)) ≈¹ ActionStep σ
+
+    FromAction³ :
+      ∀ i {s′ o}
+        → (σ : s -⟦ honestInputI (-, i) / o ⟧⇀ s′)
+        → (getAction σ , inj₂ (inj₂ i)) ≈¹ ActionStep σ
+
+  data ValidStep (es : Action × (FFDT Out ⊎ BaseT Out ⊎ IOT In)) (s : LeiosState) : Type where
+    Valid : (tr : s′ —→ s) → es ≈¹ tr → ValidStep es s
+
+  data _≈_ : TestTrace → s′ —↠ s → Type where
+
+    FromAction-FFD :
+      ∀ i {σs s′ s₀ o} {tr : s —↠ s₀}
+        → σs ≈ tr
+        → (σ : s -⟦ honestOutputI (rcvˡ (-, i)) / o ⟧⇀ s′)
+        → (getAction σ , inj₁ i) ∷ σs ≈ s′ —→⟨ ActionStep σ ⟩ tr
+
+    FromAction-Base :
+      ∀ i {σs s′ s₀ o} {tr : s —↠ s₀}
+        → σs ≈ tr
+        → (σ : s -⟦ honestOutputI (rcvʳ (-, i)) / o ⟧⇀ s′)
+        → (getAction σ , inj₂ (inj₁ i)) ∷ σs ≈ s′ —→⟨ ActionStep σ ⟩ tr
+
+    FromAction-IO :
+      ∀ i {σs s′ s₀ o} {tr : s —↠ s₀}
+        → σs ≈ tr
+        → (σ : s -⟦ honestInputI (-, i) / o ⟧⇀ s′)
+        → (getAction σ , inj₂ (inj₂ i)) ∷ σs ≈ s′ —→⟨ ActionStep σ ⟩ tr
+
+    Done : [] ≈ s ∎
+
+  data ValidTrace (es : TestTrace) (s : LeiosState) : Type where
+    Valid : (tr : s′ —↠ s) → es ≈ tr → ValidTrace es s
+
+  getNewState : ∀ {es s} → ValidTrace es s → LeiosState
+  getNewState (Valid {s′ = s} _ _) = s
+
+  data Err-verifyTrace : TestTrace → LeiosState → Type where
+    Err-StepOk   : Err-verifyTrace σs s → Err-verifyTrace ((σ , i) ∷ σs) s
+    Err-Action   : Err-verifyAction σ i s′ → Err-verifyTrace ((σ , i) ∷ σs) s
+
+  Ok' : ∀ {s i o s′} → (σ : s -⟦ honestOutputI (rcvˡ (-, i)) / o ⟧⇀ s′)
+      → Result (Err-verifyAction (getAction σ) (inj₁ i) s) (ValidStep (getAction σ , inj₁ i) s)
+  Ok' a = Ok (Valid _ (FromAction¹ _ a))
+
+  Ok'' : ∀ {s i o s′} → (σ : s -⟦ honestOutputI (rcvʳ (-, i)) / o ⟧⇀ s′)
+      → Result (Err-verifyAction (getAction σ) (inj₂ (inj₁ i)) s) (ValidStep (getAction σ , inj₂ (inj₁ i)) s)
+  Ok'' a = Ok (Valid _ (FromAction² _ a))
+
+  Ok''' : ∀ {s i o s′} → (σ : s -⟦ honestInputI (-, i) / o ⟧⇀ s′)
+    → Result (Err-verifyAction (getAction σ) (inj₂ (inj₂ i)) s) (ValidStep (getAction σ , inj₂ (inj₂ i)) s)
+  Ok''' a = Ok (Valid _ (FromAction³ _ a))
+
+  open import Relation.Nullary.Negation
+
+  verifyStep' : (a : Action) → (i : FFDT Out ⊎ BaseT Out ⊎ IOT In) → (s : LeiosState) → getSlot a ≡ slot s
+              → Result (Err-verifyAction a i s) (ValidStep (a , i) s)
+  verifyStep' (EB-Role-Action n ebs) (inj₁ SLOT) s refl with ¿ EB-Role-premises {s = s} .proj₁ ¿
+  ... | yes h = Ok' (Roles₁ (EB-Role h))
+  ... | _ = Err dummyErr
+  verifyStep' (EB-Role-Action _ _) (inj₁ FTCH) _ _ = Err dummyErr
+  verifyStep' (EB-Role-Action _ _) (inj₁ (FFD-OUT _)) _ _ = Err dummyErr
+  verifyStep' (VT-Role-Action .(slot s) eb slot') (inj₁ SLOT) s refl
+    with ¿ VT-Role-premises {s = s} {eb = eb} {ebHash = hash eb} {slot' = slot'} .proj₁ ¿
+       | isValid? s (inj₁ (ebHeader eb)) -- TODO:  why not covered above?
+  ... | yes (x , x₁ , x₂ , x₃ , x₄ , x₅ , x₆ , x₇ , x₈ , x₉ , x₁₀) | yes h = Ok' (Roles₁ (VT-Role {ebHash = hash eb} {slot' = slot'} ((x , x₁ , x₂ , x₃ , h , x₄ , x₅ , x₆ , x₇ , x₈ , x₉ , x₁₀))))
+  ... | yes (x , x₁ , x₂ , x₃ , x₄ , x₅ , x₆ , x₇ , x₈ , x₉ , x₁₀) | no _ = Err dummyErr
+  ... | no ¬h | _ = Err dummyErr
+  verifyStep' (VT-Role-Action _ _ _) (inj₁ FTCH) _ _ = Err dummyErr
+  verifyStep' (VT-Role-Action _ _ _) (inj₁ (FFD-OUT _)) _ _ = Err dummyErr
+  verifyStep' (VT-Role-Action _ _ _) (inj₂ _) _ refl = Err dummyErr
+
+  -- This has a different IO pattern, not sure if we want to model that here
+  -- For now we'll just fail
+  verifyStep' (Ftch-Action n) _ _ _ = Err dummyErr
+
+  verifyStep' (Slot₁-Action n) (inj₁ SLOT) _ _ = Err dummyErr
+  verifyStep' (Slot₁-Action n) (inj₁ FTCH) _ _ = Err dummyErr
+  verifyStep' (Slot₁-Action n) (inj₁ (FFD-OUT msgs)) s refl with ¿ Slot₁-premises {s = s} .proj₁ ¿
+  ... | yes p = Ok' (Slot₁ {s = s} {msgs = msgs} p)
+  ... | no _ = Err dummyErr
+  verifyStep' (Slot₂-Action n) (inj₁ _) _ _ = Err dummyErr
+  verifyStep' (Slot₂-Action n) (inj₂ (inj₁ (BASE-LDG rbs))) s refl = Ok'' (Slot₂ {s = s} {rbs = rbs})
+  verifyStep' (Slot₂-Action n) (inj₂ (inj₂ y)) s refl = Err dummyErr
+
+  -- Different IO pattern again
+  verifyStep' (Base₁-Action n) (inj₂ (inj₂ (SubmitTxs txs))) s refl = Ok''' Base₁
+  verifyStep' (Base₂-Action n) (inj₁ SLOT) s refl with ¿ Base₂-premises {s = s} .proj₁ ¿
+  ... | yes p = Ok' (Base₂ p)
+  ... | no _ = Err dummyErr
+  verifyStep' (Base₂-Action n) _ s refl = Err dummyErr
+  verifyStep' (No-EB-Role-Action n) (inj₁ SLOT) s refl
+    with ¿ needsUpkeep s EB-Role × (∀ π → ¬ canProduceEB (slot s) (EB , tt) (stake s) π) ¿
+  ... | yes p = Ok' (Roles₂ {s' = addUpkeep s EB-Role} {u = EB-Role} ((No-EB-Role p , λ () )))
+  ... | no ¬p = Err dummyErr
+  verifyStep' (No-EB-Role-Action n) _ s refl = Err dummyErr
+  verifyStep' (No-VT-Role-Action n) (inj₁ SLOT) s refl
+    with ¿ No-VT-Role-premises {s = s} .proj₁ ¿
+  ... | yes p = Ok' (Roles₂ {s' = addUpkeep s VT-Role} {u = VT-Role} (No-VT-Role p , λ ()))
+  ... | no ¬p = Err dummyErr
+  verifyStep' (No-VT-Role-Action n) _ s refl = Err dummyErr
+  verifyStep' (EB-Role-Action .(slot s) x) (inj₂ y) s refl = Err dummyErr
+  verifyStep' (Slot₁-Action x₁) (inj₂ y) s x = Err dummyErr
+  verifyStep' (Base₁-Action .(slot s)) (inj₁ x) s refl = Err dummyErr
+  verifyStep' (Base₁-Action .(slot s)) (inj₂ y) s refl = Err dummyErr
+
+  verifyStep : (a : Action) → (i : FFDT Out ⊎ BaseT Out ⊎ IOT In) → (s : LeiosState) → Result (Err-verifyAction a i s) (ValidStep (a , i) s)
+  verifyStep a i s = case getSlot a ≟ slot s of λ where
+    (yes p) → verifyStep' a i s p
+    (no ¬p) → Err (E-Err-Slot λ p → ⊥-elim (¬p p))
+
+  verifyTrace : ∀ (σs : TestTrace) → (s : LeiosState) → Result (Err-verifyTrace σs s) (ValidTrace σs s)
+  verifyTrace [] s = Ok (Valid (s ∎) Done)
+  verifyTrace ((a , i) ∷ σs) s = do
+    σs ← mapErr Err-StepOk (verifyTrace σs s)
+    x  ← mapErr Err-Action (verifyStep a i (getNewState σs))
+    return (σs Valid∷ʳ x)
+    where
+      open Monad-Result
+      _Valid∷ʳ_ : ∀ {e es s} → (σs : ValidTrace es s) → ValidStep e (getNewState σs) → ValidTrace (e ∷ es) s
+      Valid tr x Valid∷ʳ Valid (ActionStep as) (FromAction¹ a _) = Valid (_ —→⟨ ActionStep as ⟩ tr) (FromAction-FFD a x as)
+      Valid tr x Valid∷ʳ Valid (ActionStep as) (FromAction² a _) = Valid (_ —→⟨ ActionStep as ⟩ tr) (FromAction-Base a x as)
+      Valid tr x Valid∷ʳ Valid (ActionStep as) (FromAction³ a _) = Valid (_ —→⟨ ActionStep as ⟩ tr) (FromAction-IO a x as)