Completeness for ValidAction

Author: yveshauser

formal-spec/Leios/Trace/Verifier.agda

@@ -14,7 +14,9 @@ data Action : Type where
   IB-Role-Action EB-Role-Action V-Role-Action : Action
   No-IB-Role-Action No-EB-Role-Action No-V-Role-Action : Action
   Ftch-Action Slot-Action : Action
-  -- Base₁-Action Base₂a-Action Base₂b-Action : Action
+  Base₁-Action : Action
+  Base₂a-Action : EndorserBlock → Action
+  Base₂b-Action : Action
 
 Actions = List (Action × LeiosInput)
 
@@ -69,27 +71,25 @@ data ValidAction : Action → LeiosState → LeiosInput → Type where
   Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs)
              (msgs , (ffds' , _)) = fetch-total {ffds}
          in .(Upkeep ≡ᵉ allUpkeep) →
-            .(bs B.-⟦ B.FTCH-LDG / B.BASE-LDG [] ⟧⇀ tt) → -- TODO: rbs ≠ []
+            .(bs B.-⟦ B.FTCH-LDG / B.BASE-LDG [] ⟧⇀ tt) →
             .(ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds') →
             ValidAction Slot-Action s SLOT
 
   Ftch : ValidAction Ftch-Action s FTCH-LDG
 
-{-
   Base₁ : ∀ {txs} → ValidAction Base₁-Action s (SUBMIT (inj₂ txs))
 
   Base₂a : ∀ {eb} → 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 (this eb) / B.EMPTY ⟧⇀ tt) →
-              ValidAction Base₂a-Action s SLOT
+              ValidAction (Base₂a-Action eb) s SLOT
 
   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 (that ToPropose) / B.EMPTY ⟧⇀ tt) →
               ValidAction Base₂b-Action s SLOT
--}
 
 private variable
   i : LeiosInput
@@ -130,9 +130,9 @@ private variable
      } ↑ L.filter isValid? msgs
   , EMPTY)
 ⟦ Ftch {s} ⟧ = s , FTCH-LDG (LeiosState.Ledger s)
--- ⟦ Base₁ {s} {txs} ⟧ = record s { ToPropose = txs } , EMPTY
--- ⟦ Base₂a {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY
--- ⟦ Base₂b {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY
+⟦ Base₁ {s} {txs} ⟧ = record s { ToPropose = txs } , EMPTY
+⟦ Base₂a {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY
+⟦ Base₂b {s} x x₁ x₂ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY
 
 instance
   Dec-ValidAction : ValidAction ⁇³
@@ -200,31 +200,29 @@ instance
   Dec-ValidAction {Ftch-Action} {s} {SLOT} .dec = no λ ()
   Dec-ValidAction {Ftch-Action} {s} {INIT _} .dec = no λ ()
   Dec-ValidAction {Ftch-Action} {s} {SUBMIT _} .dec = no λ ()
-{-
   Dec-ValidAction {Base₁-Action} {s} {SUBMIT (inj₁ ebs)} .dec = no λ ()
   Dec-ValidAction {Base₁-Action} {s} {SUBMIT (inj₂ txs)} .dec = yes (Base₁ {s} {txs})
   Dec-ValidAction {Base₁-Action} {s} {SLOT} .dec = no λ ()
   Dec-ValidAction {Base₁-Action} {s} {FTCH-LDG} .dec = no λ ()
   Dec-ValidAction {Base₁-Action} {s} {INIT _} .dec = no λ ()
-  Dec-ValidAction {Base₂a-Action} {s} {SLOT} .dec
+  Dec-ValidAction {Base₂a-Action eb} {s} {SLOT} .dec
     with dec | dec | dec
   ... | yes x | yes y | yes z = yes (Base₂a x y z)
   ... | no ¬p | _ | _ = no λ where (Base₂a p _ _) → ⊥-elim (¬p (recompute dec p))
-  ... | _ | no ¬p | _ = no λ where (Base₂a _ p _) → ⊥-elim (¬p {!!}) -- (recompute dec p))
+  ... | _ | no ¬p | _ = no λ where (Base₂a {s} {eb} _ p _) → ⊥-elim (¬p (recompute dec p))
   ... | _ | _ | no ¬p = no λ where (Base₂a _ _ p) → ⊥-elim (¬p (recompute dec p))
-  Dec-ValidAction {Base₂a-Action} {s} {SUBMIT _} .dec = no λ ()
-  Dec-ValidAction {Base₂a-Action} {s} {FTCH-LDG} .dec = no λ ()
-  Dec-ValidAction {Base₂a-Action} {s} {INIT _} .dec = no λ ()
+  Dec-ValidAction {Base₂a-Action _} {s} {SUBMIT _} .dec = no λ ()
+  Dec-ValidAction {Base₂a-Action _} {s} {FTCH-LDG} .dec = no λ ()
+  Dec-ValidAction {Base₂a-Action _} {s} {INIT _} .dec = no λ ()
   Dec-ValidAction {Base₂b-Action} {s} {SLOT} .dec
     with dec | dec | dec
   ... | yes x | yes y | yes z = yes (Base₂b x y z)
   ... | no ¬p | _ | _ = no λ where (Base₂b p _ _) → ⊥-elim (¬p (recompute dec p))
-  ... | _ | no ¬p | _ = no λ where (Base₂b _ p _) → ⊥-elim (¬p {!!}) -- (recompute dec p))
+  ... | _ | no ¬p | _ = no λ where (Base₂b _ p _) → ⊥-elim (¬p (recompute dec p))
   ... | _ | _ | no ¬p = no λ where (Base₂b _ _ p) → ⊥-elim (¬p (recompute dec p))
   Dec-ValidAction {Base₂b-Action} {s} {SUBMIT _} .dec = no λ ()
   Dec-ValidAction {Base₂b-Action} {s} {FTCH-LDG} .dec = no λ ()
   Dec-ValidAction {Base₂b-Action} {s} {INIT _} .dec = no λ ()
--}
 
 mutual
   data ValidTrace : Actions → Type where
@@ -251,9 +249,9 @@ Irr-ValidAction (No-EB-Role x x₁) (No-EB-Role x₂ x₃) = refl
 Irr-ValidAction (No-V-Role _ _) (No-V-Role _ _)     = refl
 Irr-ValidAction (Slot x x₁ x₂) (Slot x₃ x₄ x₅) = refl
 Irr-ValidAction Ftch Ftch = refl
--- Irr-ValidAction Base₁ Base₁ = refl
--- Irr-ValidAction (Base₂a x x₁ x₂) (Base₂a x₃ x₄ x₅) = {!refl!}
--- Irr-ValidAction (Base₂b x x₁ x₂) (Base₂b x₃ x₄ x₅) = refl
+Irr-ValidAction Base₁ Base₁ = refl
+Irr-ValidAction (Base₂a x x₁ x₂) (Base₂a x₃ x₄ x₅) = refl
+Irr-ValidAction (Base₂b x x₁ x₂) (Base₂b x₃ x₄ x₅) = refl
 
 Irr-ValidTrace : ∀ {αs} → Irrelevant (ValidTrace αs)
 Irr-ValidTrace [] [] = refl
@@ -275,35 +273,32 @@ instance
                   $ subst (λ x → ValidAction α x i) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vα
   ... | yes vα = yes $ _ / _ ∷ vαs ⊣ vα
 
-{-
 getLabel : just s -⟦ i / o ⟧⇀ s′ → Action
 getLabel (Slot _ _ _) = Slot-Action
 getLabel Ftch = Ftch-Action
 getLabel Base₁ = Base₁-Action
-getLabel (Base₂a _ _ _) = Base₂a-Action
+getLabel (Base₂a {s} {eb} _ _ _) = Base₂a-Action eb
 getLabel (Base₂b _ _ _) = Base₂b-Action
 getLabel (Roles (IB-Role _ _ _)) = IB-Role-Action
 getLabel (Roles (EB-Role _ _ _)) = EB-Role-Action
 getLabel (Roles (V-Role _ _ _)) = V-Role-Action
 getLabel (Roles (No-IB-Role _ _)) = No-IB-Role-Action
 getLabel (Roles (No-EB-Role _ _)) = No-EB-Role-Action
 getLabel (Roles (No-V-Role _ _)) = No-V-Role-Action
--}
 
 ValidAction-sound : (va : ValidAction α s i) → let (s′ , o) = ⟦ va ⟧ in just s -⟦ i / o ⟧⇀ s′
 ValidAction-sound (Slot {s} x x₁ x₂) = Slot {s} {rbs = []} (recompute dec x) (recompute dec x₁) (recompute dec x₂)
 ValidAction-sound Ftch = Ftch
--- ValidAction-sound (Base₁ {s} {txs}) = Base₁ {s} {txs}
--- ValidAction-sound (Base₂a {s} x x₁ x₂) = Base₂a {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)
--- ValidAction-sound (Base₂b {s} x x₁ x₂) = Base₂b {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)
+ValidAction-sound (Base₁ {s} {txs}) = Base₁ {s} {txs}
+ValidAction-sound (Base₂a {s} x x₁ x₂) = Base₂a {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)
+ValidAction-sound (Base₂b {s} x x₁ x₂) = Base₂b {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂)
 ValidAction-sound (IB-Role {s} x x₁ x₂) = Roles (IB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂))
 ValidAction-sound (EB-Role {s} x x₁ x₂) = Roles (EB-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂))
 ValidAction-sound (V-Role {s} x x₁ x₂) = Roles (V-Role {s} (recompute dec x) (recompute dec x₁) (recompute dec x₂))
 ValidAction-sound (No-IB-Role {s} x x₁) = Roles (No-IB-Role {s} x x₁)
 ValidAction-sound (No-EB-Role {s} x x₁) = Roles (No-EB-Role {s} x x₁)
 ValidAction-sound (No-V-Role {s} x x₁)  = Roles (No-V-Role {s} x x₁)
 
-{-
 ValidAction-complete : (st : just s -⟦ i / o ⟧⇀ s′) → ValidAction (getLabel st) s i
 ValidAction-complete {s} {s′} (Roles (IB-Role {s} {π} {ffds'} x x₁ x₂)) =
   let open LeiosState s renaming (FFDState to ffds)
@@ -327,8 +322,10 @@ ValidAction-complete {s} (Roles (No-IB-Role x x₁)) = No-IB-Role {s} x x₁
 ValidAction-complete {s} (Roles (No-EB-Role x x₁)) = No-EB-Role {s} x x₁
 ValidAction-complete {s} (Roles (No-V-Role x x₁))  = No-V-Role {s} x x₁
 ValidAction-complete {s} Ftch = Ftch {s}
--- ValidAction-complete {s} Base₁ = Base₁ {s}
--- ValidAction-complete {s} (Base₂a x x₁ x₂) = Base₂a {s} x x₁ x₂
--- ValidAction-complete {s} (Base₂b x x₁ x₂) = Base₂b {s} x x₁ x₂
-ValidAction-complete {s} (Slot x x₁ x₂) = Slot {s} x x₁ {!!}
--}
+ValidAction-complete {s} Base₁ = Base₁ {s}
+ValidAction-complete {s} (Base₂a x x₁ x₂) = Base₂a {s} x x₁ x₂
+ValidAction-complete {s} (Base₂b x x₁ x₂) = Base₂b {s} x x₁ x₂
+ValidAction-complete {s} (Slot {s} x x₁ x₂) =
+  let open LeiosState s renaming (FFDState to ffds)
+      (_ , (_ , pr)) = fetch-total {ffds}
+  in Slot {s} x x₁ pr