Renaming V-Role to VT-Role

Author: yveshauser

formal-spec/Leios/Short.lagda.md

@@ -27,12 +27,12 @@ module Leios.Short (⋯ : SpecStructure 1)
 ```
 ```agda
 data SlotUpkeep : Type where
-  Base IB-Role EB-Role V-Role : SlotUpkeep
+  Base IB-Role EB-Role VT-Role : SlotUpkeep
 
 unquoteDecl DecEq-SlotUpkeep = derive-DecEq ((quote SlotUpkeep , DecEq-SlotUpkeep) ∷ [])
 
 allUpkeep : ℙ SlotUpkeep
-allUpkeep = (((∅ ∪ ❴ IB-Role ❵) ∪ ❴ EB-Role ❵) ∪ ❴ V-Role ❵) ∪ ❴ Base ❵
+allUpkeep = fromList (IB-Role ∷ EB-Role ∷ VT-Role ∷ Base ∷ [])
 ```
 ```agda
 open import Leios.Protocol (⋯) SlotUpkeep public
@@ -88,11 +88,11 @@ data _↝_ : LeiosState → LeiosState → Type where
                 EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs
                 votes = map (vote sk-V ∘ hash) EBs'
           in
-          ∙ needsUpkeep V-Role
+          ∙ needsUpkeep VT-Role
           ∙ canProduceV slot sk-V (stake s)
           ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
           ─────────────────────────────────────────────────────────────────────────
-          s ↝ addUpkeep record s { FFDState = ffds' } V-Role
+          s ↝ addUpkeep record s { FFDState = ffds' } VT-Role
 ```
 #### Negative Block/Vote production rules
 ```agda
@@ -111,10 +111,10 @@ data _↝_ : LeiosState → LeiosState → Type where
 ```
 ```agda
   No-VT-Role : let open LeiosState s in
-             ∙ needsUpkeep V-Role
+             ∙ needsUpkeep VT-Role
              ∙ ¬ canProduceV slot sk-V (stake s)
              ─────────────────────────────────────────────
-             s ↝ addUpkeep s V-Role
+             s ↝ addUpkeep s VT-Role
 ```
 ### Uniform short-pipeline
 ```agda

formal-spec/Leios/Short/Deterministic.agda

@@ -190,18 +190,18 @@ data _-⟦V-Role⟧⇀_ : LeiosState → LeiosState → Type where
           ∙ canProduceV slot sk-V (stake s)
           ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
           ────────────────────────────────────────────────────────────────────
-          s -⟦V-Role⟧⇀ addUpkeep record s { FFDState = ffds' } V-Role
+          s -⟦V-Role⟧⇀ addUpkeep record s { FFDState = ffds' } VT-Role
 
   No-V-Role : let open LeiosState s in
           ∙ ¬ canProduceV slot sk-V (stake s)
           ────────────────────────────────────────
-          s -⟦V-Role⟧⇀ addUpkeep s V-Role
+          s -⟦V-Role⟧⇀ addUpkeep s VT-Role
 
-V-Role⇒ND : LeiosState.needsUpkeep s V-Role → s -⟦V-Role⟧⇀ s' → just s ND.-⟦ SLOT / EMPTY ⟧⇀ s'
+V-Role⇒ND : LeiosState.needsUpkeep s VT-Role → s -⟦V-Role⟧⇀ s' → just s ND.-⟦ SLOT / EMPTY ⟧⇀ s'
 V-Role⇒ND u (V-Role x₁ x₂) = Roles (VT-Role u x₁ x₂)
 V-Role⇒ND u (No-V-Role x₁) = Roles (No-VT-Role u x₁)
 
-V-Role-Upkeep : ∀ {u} → u ≢ V-Role → LeiosState.needsUpkeep s u → s -⟦V-Role⟧⇀ s'
+V-Role-Upkeep : ∀ {u} → u ≢ VT-Role → LeiosState.needsUpkeep s u → s -⟦V-Role⟧⇀ s'
                   → LeiosState.needsUpkeep s' u
 V-Role-Upkeep u≢V-Role h (V-Role _ _) u∈su = case Equivalence.from ∈-∪ u∈su of λ where
   (inj₁ x) → h x
@@ -216,7 +216,7 @@ opaque
     (yes p) → -, V-Role p (proj₂ FFD.FFD-Send-total)
     (no ¬p) → -, No-V-Role ¬p
 
-  V-Role-total' : ∃[ ffds ] s -⟦V-Role⟧⇀ addUpkeep record s { FFDState = ffds } V-Role
+  V-Role-total' : ∃[ ffds ] s -⟦V-Role⟧⇀ addUpkeep record s { FFDState = ffds } VT-Role
   V-Role-total' {s = s} = let open LeiosState s in case Dec-canProduceV of λ where
     (yes p) → -, V-Role    p (proj₂ FFD.FFD-Send-total)
     (no ¬p) → -, No-V-Role ¬p

formal-spec/Leios/Trace/Decidable.agda

@@ -53,18 +53,18 @@ module _ {s : LeiosState} (let open LeiosState s renaming (FFDState to ffds; Bas
           let EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs
               votes = map (vote sk-V ∘ hash) EBs'
           in
-          { _ : auto∶ needsUpkeep V-Role }
+          { _ : auto∶ needsUpkeep VT-Role }
           { _ : auto∶ canProduceV slot sk-V (stake s) }
           { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds' } →
           ─────────────────────────────────────────────────────────────────────────
-          s ↝ addUpkeep record s { FFDState = ffds' } V-Role
+          s ↝ addUpkeep record s { FFDState = ffds' } VT-Role
   V-Role? {_} {p} {q} {r} = VT-Role (toWitness p) (toWitness q) (toWitness r)
 
   No-V-Role? :
-             { _ : auto∶ needsUpkeep V-Role }
+             { _ : auto∶ needsUpkeep VT-Role }
              { _ : auto∶ ¬ canProduceV slot sk-V (stake s) } →
              ─────────────────────────────────────────────
-             s ↝ addUpkeep s V-Role
+             s ↝ addUpkeep s VT-Role
   No-V-Role? {p} {q} = No-VT-Role (toWitness p) (toWitness q)
 
   {-

formal-spec/Leios/Trace/Verifier.agda

@@ -48,7 +48,7 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where
                  EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs
                  votes = map (vote sk-V ∘ hash) EBs'
                  ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing})
-             in .(needsUpkeep V-Role) →
+             in .(needsUpkeep VT-Role) →
                 .(canProduceV slot sk-V (stake s)) →
                 .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') →
                 ValidAction VT-Role-Action s SLOT
@@ -64,7 +64,7 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where
                   ValidAction No-EB-Role-Action s SLOT
 
   No-VT-Role : let open LeiosState s
-               in needsUpkeep V-Role →
+               in needsUpkeep VT-Role →
                   (¬ canProduceV slot sk-V (stake s)) →
                   ValidAction No-VT-Role-Action s SLOT
 
@@ -113,12 +113,12 @@ private variable
       EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs
       votes = map (vote sk-V ∘ hash) EBs'
       ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing})
-  in addUpkeep record s { FFDState = ffds' } V-Role , EMPTY
+  in addUpkeep record s { FFDState = ffds' } VT-Role , EMPTY
 ⟦ No-IB-Role {s} _ _ ⟧ = addUpkeep s IB-Role , EMPTY
 ⟦ No-EB-Role {s} _ _ ⟧ = addUpkeep s EB-Role , EMPTY
-⟦ No-VT-Role {s} _ _ ⟧ = addUpkeep s V-Role , EMPTY
+⟦ No-VT-Role {s} _ _ ⟧ = addUpkeep s VT-Role , EMPTY
 ⟦ Slot {s} _ _ _ ⟧ =
-  let open LeiosState s renaming (FFDState to ffds; BaseState to bs)
+  let open LeiosState s renaming (FFDState to ffds)
       (msgs , (ffds' , _)) = fetch-total {ffds}
   in
   (record s
@@ -277,10 +277,24 @@ private
   opaque
     unfolding List-Model
 
-    test : Bool
-    test = ¿ ValidTrace ((IB-Role-Action , SLOT) ∷ []) ¿ᵇ
+    test₁ : Bool
+    test₁ = ¿ ValidTrace ((IB-Role-Action , SLOT) ∷ []) ¿ᵇ
+
+    _ : test₁ ≡ true
+    _ = refl
 
-    _ : test ≡ true
+    test₂ : Bool
+    test₂ =
+      let t = L.reverse $
+              (IB-Role-Action , SLOT)
+            ∷ (EB-Role-Action , SLOT)
+            ∷ (VT-Role-Action , SLOT)
+            ∷ (Base₂b-Action  , SLOT)
+            ∷ (Slot-Action    , SLOT)
+            ∷ []
+      in ¿ ValidTrace t ¿ᵇ
+
+    _ : test₂ ≡ true
     _ = refl
 
 getLabel : just s -⟦ i / o ⟧⇀ s′ → Action