Renaming vHeader to vtHeader

Author: yveshauser

formal-spec/Leios/Blocks.agda

@@ -137,7 +137,7 @@ module GenFFD ⦃ _ : IsBlock (List Vote) ⦄ where
   data Header : Type where
     ibHeader : IBHeader → Header
     ebHeader : EndorserBlock → Header
-    vHeader  : List Vote → Header
+    vtHeader : List Vote → Header
 
   data Body : Type where
     ibBody : IBBody → Body
@@ -164,7 +164,7 @@ module GenFFD ⦃ _ : IsBlock (List Vote) ⦄ where
   msgID : Header → ID
   msgID (ibHeader h) = (slotNumber h , producerID h)
   msgID (ebHeader h) = (slotNumber h , producerID h) -- NOTE: this isn't in the paper
-  msgID (vHeader  h) = (slotNumber h , producerID h) -- NOTE: this isn't in the paper
+  msgID (vtHeader  h) = (slotNumber h , producerID h) -- NOTE: this isn't in the paper
 
 ffdAbstract : ⦃ _ : IsBlock (List Vote) ⦄ → FFDAbstract
 ffdAbstract = record { GenFFD }

formal-spec/Leios/Defaults.agda

@@ -131,7 +131,7 @@ open FFDState
 
 flushIns : FFDState → List (GenFFD.Header ⊎ GenFFD.Body)
 flushIns record { inIBs = ibs ; inEBs = ebs ; inVTs = vts } =
-  flushIBs ibs ++ L.map (inj₁ ∘ ebHeader) ebs ++ L.map (inj₁ ∘ vHeader) vts
+  flushIBs ibs ++ L.map (inj₁ ∘ ebHeader) ebs ++ L.map (inj₁ ∘ vtHeader) vts
   where
     flushIBs : List InputBlock → List (GenFFD.Header ⊎ GenFFD.Body)
     flushIBs [] = []
@@ -140,22 +140,22 @@ flushIns record { inIBs = ibs ; inEBs = ebs ; inVTs = vts } =
 data SimpleFFD : FFDState → FFDAbstract.Input ffdAbstract → FFDAbstract.Output ffdAbstract → FFDState → Type where
   SendIB : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (ibHeader h) (just (ibBody b))) FFDAbstract.SendRes (record s { outIBs = record {header = h; body = b} ∷ outIBs s})
   SendEB : ∀ {s eb} → SimpleFFD s (FFDAbstract.Send (ebHeader eb) nothing) FFDAbstract.SendRes (record s { outEBs = eb ∷ outEBs s})
-  SendVS : ∀ {s vs} → SimpleFFD s (FFDAbstract.Send (vHeader vs) nothing) FFDAbstract.SendRes (record s { outVTs = vs ∷ outVTs s})
+  SendVS : ∀ {s vs} → SimpleFFD s (FFDAbstract.Send (vtHeader vs) nothing) FFDAbstract.SendRes (record s { outVTs = vs ∷ outVTs s})
 
   BadSendIB : ∀ {s h} → SimpleFFD s (FFDAbstract.Send (ibHeader h) nothing) FFDAbstract.SendRes s
   BadSendEB : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (ebHeader h) (just b)) FFDAbstract.SendRes s
-  BadSendVS : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (vHeader h) (just b)) FFDAbstract.SendRes s
+  BadSendVS : ∀ {s h b} → SimpleFFD s (FFDAbstract.Send (vtHeader h) (just b)) FFDAbstract.SendRes s
 
   Fetch : ∀ {s} → SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes (flushIns s)) (record s { inIBs = [] ; inEBs = [] ; inVTs = [] })
 
 send-total : ∀ {s h b} → ∃[ s' ] (SimpleFFD s (FFDAbstract.Send h b) FFDAbstract.SendRes s')
 send-total {s} {ibHeader h} {just (ibBody b)} = record s { outIBs = record {header = h; body = b} ∷ outIBs s} , SendIB
 send-total {s} {ebHeader eb} {nothing} = record s { outEBs = eb ∷ outEBs s} , SendEB
-send-total {s} {vHeader vs} {nothing} = record s { outVTs = vs ∷ outVTs s} , SendVS
+send-total {s} {vtHeader vs} {nothing} = record s { outVTs = vs ∷ outVTs s} , SendVS
 
 send-total {s} {ibHeader h} {nothing} = s , BadSendIB
 send-total {s} {ebHeader eb} {just _} = s , BadSendEB
-send-total {s} {vHeader vs} {just _} = s , BadSendVS
+send-total {s} {vtHeader vs} {just _} = s , BadSendVS
 
 fetch-total : ∀ {s} → ∃[ x ] (∃[ s' ] (SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes x) s'))
 fetch-total {s} = flushIns s , (record s { inIBs = [] ; inEBs = [] ; inVTs = [] } , Fetch)

formal-spec/Leios/Foreign/Types.agda

@@ -132,7 +132,7 @@ open Computational22
 open BaseAbstract
 open FFDAbstract
 
-open GenFFD.Header using (ibHeader; ebHeader; vHeader)
+open GenFFD.Header using (ibHeader; ebHeader; vtHeader)
 open GenFFD.Body using (ibBody)
 open FFDState
 
@@ -153,7 +153,7 @@ instance
   Computational-FFD : Computational22 (FFDAbstract.Functionality._-⟦_/_⟧⇀_ d-FFDFunctionality) String
   Computational-FFD .computeProof s (Send (ibHeader h) (just (ibBody b))) = success ((SendRes , record s {outIBs = record {header = h; body = b} ∷ outIBs s}) , SendIB)
   Computational-FFD .computeProof s (Send (ebHeader h) nothing) = success ((SendRes , record s {outEBs = h ∷ outEBs s}) , SendEB)
-  Computational-FFD .computeProof s (Send (vHeader h) nothing) = success ((SendRes , record s {outVTs = h ∷ outVTs s}) , SendVS)
+  Computational-FFD .computeProof s (Send (vtHeader h) nothing) = success ((SendRes , record s {outVTs = h ∷ outVTs s}) , SendVS)
   Computational-FFD .computeProof s Fetch = success ((FetchRes (flushIns s) , record s {inIBs = []; inEBs = []; inVTs = []}) , Fetch)
 
   Computational-FFD .computeProof _ _ = failure "FFD error"

formal-spec/Leios/Protocol.agda

@@ -172,7 +172,7 @@ module _ (s : LeiosState)  where
     with lookupPubKeyAndStake s h
   ... | just (pk , pid) = ebValid h pk (stake'' pk s)
   ... | nothing = ⊥
-  headerValid (vHeader h)  = vsValid h
+  headerValid (vtHeader h) = vsValid h
 
   headerValid? : (h : Header) → Dec (headerValid h)
   headerValid? (ibHeader h)
@@ -183,7 +183,7 @@ module _ (s : LeiosState)  where
     with lookupPubKeyAndStake s h
   ... | just (pk , pid) = ebValid? h pk (stake'' pk s)
   ... | nothing = no λ x → x
-  headerValid? (vHeader h) = vsValid? h
+  headerValid? (vtHeader h) = vsValid? h
 
   bodyValid : Body → Type
   bodyValid (ibBody b) = ibBodyValid b
@@ -213,7 +213,7 @@ module _ (s : LeiosState) where
 
   upd : Header ⊎ Body → LeiosState
   upd (inj₁ (ebHeader eb)) = record s { EBs = eb ∷ EBs }
-  upd (inj₁ (vHeader vs)) = record s { Vs = vs ∷ Vs }
+  upd (inj₁ (vtHeader vs)) = record s { Vs = vs ∷ Vs }
   upd (inj₁ (ibHeader h)) with A.any? (matchIB? h) IBBodies
   ... | yes p =
     record s
@@ -244,7 +244,7 @@ module _ {s s'} where
   ... | yes p = refl
   ... | no ¬p = refl
   upd-preserves-Upkeep {inj₁ (ebHeader x)} refl = refl
-  upd-preserves-Upkeep {inj₁ (vHeader x)} refl = refl
+  upd-preserves-Upkeep {inj₁ (vtHeader x)} refl = refl
   upd-preserves-Upkeep {inj₂ (ibBody x)} refl with A.any? (flip matchIB? x) IBHeaders
   ... | yes p = refl
   ... | no ¬p = refl

formal-spec/Leios/Short.lagda.md

@@ -90,7 +90,7 @@ data _↝_ : LeiosState → LeiosState → Type where
           in
           ∙ needsUpkeep VT-Role
           ∙ canProduceV slot sk-V (stake s)
-          ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
+          ∙ ffds FFD.-⟦ Send (vtHeader votes) nothing / SendRes ⟧⇀ ffds'
           ─────────────────────────────────────────────────────────────────────────
           s ↝ addUpkeep record s { FFDState = ffds' } VT-Role
 ```

formal-spec/Leios/Short/Decidable.agda

@@ -55,7 +55,7 @@ module _ {s : LeiosState} (let open LeiosState s renaming (FFDState to ffds; Bas
           in
           { _ : auto∶ needsUpkeep VT-Role }
           { _ : auto∶ canProduceV slot sk-V (stake s) }
-          { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds' } →
+          { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.vtHeader votes) nothing / FFD.SendRes ⟧⇀ ffds' } →
           ─────────────────────────────────────────────────────────────────────────
           s ↝ addUpkeep record s { FFDState = ffds' } VT-Role
   V-Role? {_} {p} {q} {r} = VT-Role (toWitness p) (toWitness q) (toWitness r)

formal-spec/Leios/Short/Deterministic.agda

@@ -188,7 +188,7 @@ data _-⟦V-Role⟧⇀_ : LeiosState → LeiosState → Type where
                votes = map (vote sk-V ∘ hash) EBs'
           in
           ∙ canProduceV slot sk-V (stake s)
-          ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
+          ∙ ffds FFD.-⟦ Send (vtHeader votes) nothing / SendRes ⟧⇀ ffds'
           ────────────────────────────────────────────────────────────────────
           s -⟦V-Role⟧⇀ addUpkeep record s { FFDState = ffds' } VT-Role
 
@@ -226,7 +226,7 @@ upd-Upkeep {record { IBBodies = bds }} {inj₁ (ibHeader h)} with A.any? (matchI
 ... | yes p = refl
 ... | no ¬p = refl
 upd-Upkeep {_} {inj₁ (ebHeader _)} = refl
-upd-Upkeep {_} {inj₁ (vHeader _)} = refl
+upd-Upkeep {_} {inj₁ (vtHeader _)} = refl
 upd-Upkeep {record { IBHeaders = hds }} {inj₂ (ibBody b)} with A.any? (flip matchIB? b) hds
 ... | yes p = refl
 ... | no ¬p = refl

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

@@ -70,10 +70,10 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where
   VT-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'
-                ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing})
+                ffds' = proj₁ (send-total {ffds} {vtHeader votes} {nothing})
             in .(needsUpkeep VT-Role) →
                .(canProduceV slot sk-V (stake s)) →
-               .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') →
+               .(ffds FFD.-⟦ FFD.Send (vtHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') →
                ValidAction (VT-Role-Action slot) s SLOT
 
   No-IB-Role : let open LeiosState s
@@ -135,7 +135,7 @@ private variable
   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'
-      ffds' = proj₁ (send-total {ffds} {vHeader votes} {nothing})
+      ffds' = proj₁ (send-total {ffds} {vtHeader votes} {nothing})
   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
@@ -353,7 +353,6 @@ instance
     (_ / _ ∷ tr ⊣ vα) → ¬vα
                   $ subst (λ x → ValidAction α x i) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vα
   ... | yes vα = yes $ _ / _ ∷ vαs ⊣ vα
-
   Dec-ValidTrace {tr} .dec | inj₂ u ∷ αs
     with ¿ ValidTrace αs ¿
   ... | no ¬vαs = no λ where (vαs ↥ _) → ¬vαs vαs
@@ -383,7 +382,7 @@ data _⇑_ : LeiosState → LeiosState → Type where
 
   UpdateVT : ∀ {s h ffds'} →
     let open LeiosState s renaming (FFDState to ffds)
-        vt = FFD.Send (vHeader h) nothing
+        vt = FFD.Send (vtHeader h) nothing
     in
     ∙ ffds FFD.-⟦ vt / FFD.SendRes ⟧⇀ ffds'
       ─────────────────────────────────────
@@ -446,7 +445,7 @@ ValidAction-complete {s} (Roles (VT-Role x x₁ _))  =
   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'
-      pr = proj₂ (send-total {ffds} {vHeader votes} {nothing})
+      pr = proj₂ (send-total {ffds} {vtHeader votes} {nothing})
   in VT-Role {s} x x₁ pr
 ValidAction-complete (Roles (No-IB-Role x x₁)) = No-IB-Role x x₁
 ValidAction-complete (Roles (No-EB-Role x x₁)) = No-EB-Role x x₁

formal-spec/Leios/Simplified.agda

@@ -84,7 +84,7 @@ data _↝_ : LeiosState → LeiosState → Type where
           in
           ∙ needsUpkeep V1-Role
           ∙ canProduceV1 slot sk-V (stake s)
-          ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
+          ∙ ffds FFD.-⟦ Send (vtHeader votes) nothing / SendRes ⟧⇀ ffds'
           ─────────────────────────────────────────────────────────────────────────
           s ↝ addUpkeep record s { FFDState = ffds' } V1-Role
 
@@ -94,7 +94,7 @@ data _↝_ : LeiosState → LeiosState → Type where
           in
           ∙ needsUpkeep V2-Role
           ∙ canProduceV2 slot sk-V (stake s)
-          ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
+          ∙ ffds FFD.-⟦ Send (vtHeader votes) nothing / SendRes ⟧⇀ ffds'
           ─────────────────────────────────────────────────────────────────────────
           s ↝ addUpkeep record s { FFDState = ffds' } V2-Role
 

formal-spec/Leios/Simplified/Deterministic.agda

@@ -190,7 +190,7 @@ data _-⟦V1-Role⟧⇀_ : LeiosState → LeiosState → Type where
                 votes = map (vote sk-V ∘ hash) EBs'
           in
           ∙ canProduceV1 slot sk-V (stake s)
-          ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
+          ∙ ffds FFD.-⟦ Send (vtHeader votes) nothing / SendRes ⟧⇀ ffds'
           ────────────────────────────────────────────────────────────────────
           s -⟦V1-Role⟧⇀ addUpkeep record s { FFDState = ffds' } V1-Role
 
@@ -230,7 +230,7 @@ data _-⟦V2-Role⟧⇀_ : LeiosState → LeiosState → Type where
                 votes = map (vote sk-V ∘ hash) EBs'
           in
           ∙ canProduceV2 slot sk-V (stake s)
-          ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
+          ∙ ffds FFD.-⟦ Send (vtHeader votes) nothing / SendRes ⟧⇀ ffds'
           ────────────────────────────────────────────────────────────────────
           s -⟦V2-Role⟧⇀ addUpkeep record s { FFDState = ffds' } V2-Role