FFD implementation

Author: yveshauser

formal-spec/Leios/FFD.agda

@@ -21,7 +21,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'
+          FFD-Send-total : ∀ {ffds h b} → ∃[ ffds' ] ffds -⟦ Send h b / SendRes ⟧⇀ ffds'
 
     open Input public
     open Output public

formal-spec/Leios/Foreign/Export.agda

@@ -144,8 +144,8 @@ instance
   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 (record {inIBs = record { header = h; body = b} ∷ i; inEBs = e; inVTs = v}) Fetch = success ((FetchRes (inj₁ (ibHeader h) ∷ inj₂ (ibBody b) ∷ []) , record {inIBs = i; inEBs = e; inVTs = v}) , FetchIB)
-  Computational-FFD .computeProof (record {inIBs = []; inEBs = e; inVTs = v}) Fetch = success ((FetchRes [] , record {inIBs = []; inEBs = e; inVTs = v}) , EmptyIB)
+  Computational-FFD .computeProof s Fetch = success ((FetchRes (flushIns s) , record s {inIBs = []; inEBs = []; inVTs = []}) , Fetch)
+
   Computational-FFD .computeProof _ _ = failure "FFD error"
   Computational-FFD .completeness _ _ _ _ _ = error "Computational-FFD completeness"
 

formal-spec/Leios/Short/Deterministic.agda

@@ -115,7 +115,7 @@ IB-Role⇒ND (No-IB-Role x x₁) = Roles (No-IB-Role x x₁)
 opaque
   IB-Role-total : LeiosState.needsUpkeep s IB-Role → ∃[ s' ] s -⟦IB-Role⟧⇀ s'
   IB-Role-total {s = s} h = let open LeiosState s in case Dec-canProduceIB of λ where
-    (inj₁ (π , pf)) → -, IB-Role    h pf (proj₂ FFD.FFD-total)
+    (inj₁ (π , pf)) → -, IB-Role    h pf (proj₂ FFD.FFD-Send-total)
     (inj₂ pf)       → -, No-IB-Role h pf
 
 IB-Role-Upkeep : s -⟦IB-Role⟧⇀ s' → LeiosState.needsUpkeep s IB-Role × ¬ LeiosState.needsUpkeep s' IB-Role
@@ -147,7 +147,7 @@ EB-Role⇒ND (No-EB-Role x x₁) = Roles (No-EB-Role x x₁)
 opaque
   EB-Role-total : LeiosState.needsUpkeep s EB-Role → ∃[ s' ] s -⟦EB-Role⟧⇀ s'
   EB-Role-total {s = s} h = let open LeiosState s in case Dec-canProduceEB of λ where
-    (inj₁ (π , pf)) → -, EB-Role    h pf (proj₂ FFD.FFD-total)
+    (inj₁ (π , pf)) → -, EB-Role    h pf (proj₂ FFD.FFD-Send-total)
     (inj₂ pf)       → -, No-EB-Role h pf
 
 EB-Role-Upkeep : s -⟦EB-Role⟧⇀ s' → LeiosState.needsUpkeep s EB-Role × ¬ LeiosState.needsUpkeep s' EB-Role
@@ -179,7 +179,7 @@ V-Role⇒ND (No-V-Role x x₁) = Roles (No-V-Role x x₁)
 opaque
   V-Role-total : LeiosState.needsUpkeep s V-Role → ∃[ s' ] s -⟦V-Role⟧⇀ s'
   V-Role-total {s = s} h = let open LeiosState s in case Dec-canProduceV of λ where
-    (yes p) → -, V-Role h p (proj₂ FFD.FFD-total)
+    (yes p) → -, V-Role h p (proj₂ FFD.FFD-Send-total)
     (no ¬p) → -, No-V-Role h ¬p
 
 V-Role-Upkeep : s -⟦V-Role⟧⇀ s' → LeiosState.needsUpkeep s V-Role × ¬ LeiosState.needsUpkeep s' V-Role

formal-spec/Leios/Trace.agda

@@ -117,53 +117,41 @@ open GenFFD.Header
 open GenFFD.Body
 open FFDState
 
-data SimpleFFD : FFDState → FFDAbstract.Input ffdAbstract → FFDAbstract.Output ffdAbstract → FFDState → Type where
-  SendIB : ∀ {s h b o} → SimpleFFD s (FFDAbstract.Send (ibHeader h) (just (ibBody b))) o (record s { outIBs = record {header = h; body = b} ∷ outIBs s})
-  SendEB : ∀ {s eb o} → SimpleFFD s (FFDAbstract.Send (ebHeader eb) nothing) o (record s { outEBs = eb ∷ outEBs s})
-  SendVS : ∀ {s vs o} → SimpleFFD s (FFDAbstract.Send (vHeader vs) nothing) o (record s { outVTs = vs ∷ outVTs s})
-
-  BadSendIB : ∀ {s h o} → SimpleFFD s (FFDAbstract.Send (ibHeader h) nothing) o s
-  BadSendEB : ∀ {s h b o} → SimpleFFD s (FFDAbstract.Send (ebHeader h) (just b)) o s
-  BadSendVS : ∀ {s h b o} → SimpleFFD s (FFDAbstract.Send (vHeader h) (just b)) o s
-
-  FetchIB : ∀ {s ib o} → SimpleFFD record s {inIBs = ib ∷ inIBs s} FFDAbstract.Fetch o s
-  EmptyIB : ∀ {s o} → SimpleFFD record s {inIBs = []} FFDAbstract.Fetch o s
-
-{-
-  FetchEB : ∀ {s eb o} → SimpleFFD record s {inEBs = eb ∷ inEBs s} FFDAbstract.Fetch o s
-  EmptyEB : ∀ {s o} → SimpleFFD record s {inEBs = []} FFDAbstract.Fetch o s
-
-  FetchVT : ∀ {s x o} → SimpleFFD record s {inVTs = x ∷ inVTs s} FFDAbstract.Fetch o s
-  EmptyVT : ∀ {s o} → SimpleFFD record s {inVTs = []} FFDAbstract.Fetch o s
--}
+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
+  where
+    flushIBs : List InputBlock → List (GenFFD.Header ⊎ GenFFD.Body)
+    flushIBs [] = []
+    flushIBs (record {header = h; body = b} ∷ ibs) = inj₁ (ibHeader h) ∷ inj₂ (ibBody b) ∷ flushIBs ibs
 
-simple-total : ∀ {ffds i o} → ∃[ ffds' ] (SimpleFFD ffds i o ffds')
-simple-total {ffd} {FFDAbstract.Send (ibHeader h) (just (ibBody b))} {o} = record ffd { outIBs = record {header = h; body = b} ∷ outIBs ffd} , SendIB
-simple-total {ffd} {FFDAbstract.Send (ebHeader eb) nothing} {o} = record ffd { outEBs = eb ∷ outEBs ffd} , SendEB
-simple-total {ffd} {FFDAbstract.Send (vHeader vs) nothing} {o} = record ffd { outVTs = vs ∷ outVTs ffd} , SendVS
+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})
 
-simple-total {ffd} {FFDAbstract.Send (ibHeader h) nothing} {o} = ffd , BadSendIB
-simple-total {ffd} {FFDAbstract.Send (ebHeader eb) (just b)} {o} = ffd , BadSendEB
-simple-total {ffd} {FFDAbstract.Send (vHeader vs) (just b)} {o} = ffd , BadSendVS
+  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
 
-simple-total {record {inIBs = record {header = h; body = b} ∷ i; inEBs = e; inVTs = v}} {FFDAbstract.Fetch} {o} = record {inIBs = i; inEBs = e; inVTs = v} , FetchIB
-simple-total {record {inIBs = []; inEBs = e; inVTs = v}} {FFDAbstract.Fetch} {o} = record {inIBs = []; inEBs = e; inVTs = v} , EmptyIB
+  Fetch : ∀ {s} → SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes (flushIns s)) (record s { inIBs = [] ; inEBs = [] ; inVTs = [] })
 
-{-
-simple-total {record {inIBs = i; inEBs = eb ∷ e; inVTs = v}} {FFDAbstract.Fetch} {o} = record {inIBs = i; inEBs = e; inVTs = v} , FetchEB
-simple-total {record {inIBs = i; inEBs = []; inVTs = v}} {FFDAbstract.Fetch} {o} = record {inIBs = i; inEBs = []; inVTs = v} , EmptyEB
+simple-total : ∀ {s h b} → ∃[ s' ] (SimpleFFD s (FFDAbstract.Send h b) FFDAbstract.SendRes s')
+simple-total {s} {ibHeader h} {just (ibBody b)} = record s { outIBs = record {header = h; body = b} ∷ outIBs s} , SendIB
+simple-total {s} {ebHeader eb} {nothing} = record s { outEBs = eb ∷ outEBs s} , SendEB
+simple-total {s} {vHeader vs} {nothing} = record s { outVTs = vs ∷ outVTs s} , SendVS
 
-simple-total {record {inIBs = i; inEBs = e; inVTs = x ∷ v}} {FFDAbstract.Fetch} {o} = record {inIBs = i; inEBs = e; inVTs = v} , FetchVT
-simple-total {record {inIBs = i; inEBs = e; inVTs = []}} {FFDAbstract.Fetch} {o} = record {inIBs = ; inEBs = e; inVTs = []} , EmptyVT
--}
+simple-total {s} {ibHeader h} {nothing} = s , BadSendIB
+simple-total {s} {ebHeader eb} {just _} = s , BadSendEB
+simple-total {s} {vHeader vs} {just _} = s , BadSendVS
 
 d-FFDFunctionality : FFDAbstract.Functionality ffdAbstract
 d-FFDFunctionality =
   record
     { State = FFDState
     ; initFFDState = record { inIBs = []; inEBs = []; inVTs = []; outIBs = []; outEBs = []; outVTs = [] }
     ; _-⟦_/_⟧⇀_ = SimpleFFD
-    ; FFD-total = simple-total
+    ; FFD-Send-total = simple-total
     }
 
 open import Leios.Voting public