Trace verifier (#3)

Author: yveshauser

.github/workflows/formal-spec.yaml

@@ -35,7 +35,7 @@ jobs:
         uses: actions/checkout@v4
 
       - name: 💾 Cache Nix store
-        uses: actions/cache@v3.0.8
+        uses: actions/cache@v4
         id: nix-cache
         with:
           path: /tmp/nixcache

formal-spec/Everything.agda

@@ -1,8 +1,31 @@
 module Everything where
 
-open import Leios.Simplified
-open import Leios.Simplified.Deterministic
+open import CategoricalCrypto
+open import Class.Computational22
+open import Leios.Abstract
+open import Leios.Base
+open import Leios.Blocks
+open import Leios.Defaults
+open import Leios.FFD
+open import Leios.Foreign.BaseTypes
+open import Leios.Foreign.HsTypes
+open import Leios.Foreign.Types
+open import Leios.Foreign.Util
+open import Leios.KeyRegistration
+open import Leios.Network
+open import Leios.Prelude
+open import Leios.Protocol
 open import Leios.Short
 open import Leios.Short.Deterministic
-open import Leios.Network
-open import Leios.Foreign.Types
+open import Leios.Simplified
+open import Leios.Simplified.Deterministic
+open import Leios.Simplified.Deterministic.Test
+open import Leios.SpecStructure
+open import Leios.Traces
+open import Leios.Trace.Decidable
+open import Leios.Trace.Verifier
+open import Leios.Trace.Verifier.Test
+open import Leios.UniformShort
+open import Leios.Voting
+open import Leios.VRF
+open import StateMachine

formal-spec/Leios/Abstract.agda

@@ -6,11 +6,15 @@ open import Leios.Prelude
 
 record LeiosAbstract : Type₁ where
   field Tx : Type
+        ⦃ DecEq-Tx ⦄ : DecEq Tx
         PoolID : Type
         ⦃ DecEq-PoolID ⦄ : DecEq PoolID
         BodyHash VrfPf PrivKey Sig Hash : Type -- these could have been byte strings, but this is safer
         ⦃ DecEq-Hash ⦄ : DecEq Hash
+        ⦃ DecEq-VrfPf ⦄ : DecEq VrfPf
+        ⦃ DecEq-Sig ⦄ : DecEq Sig
         Vote : Type
+        ⦃ DecEq-Vote ⦄ : DecEq Vote
         vote : PrivKey → Hash → Vote
         sign : PrivKey → Hash → Sig
         ⦃ Hashable-Txs ⦄ : Hashable (List Tx) Hash

formal-spec/Leios/Base.agda

@@ -34,6 +34,7 @@ record BaseAbstract : Type₁ where
   record Functionality : Type₁ where
     field State : Type
           _-⟦_/_⟧⇀_ : State → Input → Output → State → Type
+          ⦃ Dec-_-⟦_/_⟧⇀_ ⦄ : {s : State} → {i : Input} → {o : Output} → {s' : State} → (s -⟦ i / o ⟧⇀ s') ⁇
           SUBMIT-total : ∀ {s b} → ∃[ s' ] s -⟦ SUBMIT b / EMPTY ⟧⇀ s'
 
     open Input public

formal-spec/Leios/Blocks.agda

@@ -3,6 +3,8 @@
 open import Leios.Prelude
 open import Leios.Abstract
 open import Leios.FFD
+open import Tactic.Defaults
+open import Tactic.Derive.DecEq
 
 module Leios.Blocks (a : LeiosAbstract) (let open LeiosAbstract a) where
 
@@ -20,26 +22,22 @@ record IsBlock (B : Type) : Type where
 
 open IsBlock ⦃...⦄ public
 
-OSig : Bool → Type
-OSig true  = Sig
-OSig false = ⊤
-
 IBRef = Hash
 EBRef = Hash
 
 --------------------------------------------------------------------------------
 -- Input Blocks
 --------------------------------------------------------------------------------
 
-record IBHeaderOSig (b : Bool) : Type where
+record IBHeaderOSig (sig : Type) : Type where
   field slotNumber : ℕ
         producerID : PoolID
         lotteryPf  : VrfPf
         bodyHash   : Hash
-        signature  : OSig b
+        signature  : sig
 
-IBHeader    = IBHeaderOSig true
-PreIBHeader = IBHeaderOSig false
+IBHeader    = IBHeaderOSig Sig
+PreIBHeader = IBHeaderOSig ⊤
 
 record IBBody : Type where
   field txs : List Tx
@@ -50,28 +48,38 @@ record InputBlock : Type where
 
   open IBHeaderOSig header public
 
+unquoteDecl DecEq-IBBody DecEq-IBHeaderOSig DecEq-InputBlock =
+  derive-DecEq (
+      (quote IBBody , DecEq-IBBody)
+    ∷ (quote IBHeaderOSig , DecEq-IBHeaderOSig)
+    ∷ (quote InputBlock , DecEq-InputBlock) ∷ [])
+
 instance
-  IsBlock-IBHeaderOSig : ∀ {b} → IsBlock (IBHeaderOSig b)
-  IsBlock-IBHeaderOSig = record { IBHeaderOSig }
+  IsBlock-IBHeader : IsBlock IBHeader
+  IsBlock-IBHeader = record { IBHeaderOSig }
 
   Hashable-IBBody : Hashable IBBody Hash
   Hashable-IBBody .hash b = hash (b .IBBody.txs)
 
+  Hashable-IBHeader : ⦃ Hashable PreIBHeader Hash ⦄ → Hashable IBHeader Hash
+  Hashable-IBHeader .hash b = hash {T = PreIBHeader}
+    record { IBHeaderOSig b hiding (signature) ; signature = _ }
+
   IsBlock-InputBlock : IsBlock InputBlock
   IsBlock-InputBlock = record { InputBlock }
 
 mkIBHeader : ⦃ Hashable PreIBHeader Hash ⦄ → ℕ → PoolID → VrfPf → PrivKey → List Tx → IBHeader
 mkIBHeader slot id π pKey txs = record { signature = sign pKey (hash h) ; IBHeaderOSig h }
   where
-    h : IBHeaderOSig false
+    h : IBHeaderOSig ⊤
     h = record { slotNumber = slot
                ; producerID = id
                ; lotteryPf  = π
                ; bodyHash   = hash txs
                ; signature  = _
                }
 
-getIBRef : ⦃ Hashable IBHeader Hash ⦄ → InputBlock → IBRef
+getIBRef : ⦃ Hashable PreIBHeader Hash ⦄ → InputBlock → IBRef
 getIBRef = hash ∘ InputBlock.header
 
 -- TODO
@@ -94,24 +102,26 @@ ibValid? record { header = h ; body = b } = ibHeaderValid? h ×-dec ibBodyValid?
 -- Endorser Blocks
 --------------------------------------------------------------------------------
 
-record EndorserBlockOSig (b : Bool) : Type where
+record EndorserBlockOSig (sig : Type) : Type where
   field slotNumber : ℕ
         producerID : PoolID
         lotteryPf  : VrfPf
         ibRefs     : List IBRef
         ebRefs     : List EBRef
-        signature  : OSig b
+        signature  : sig
 
-EndorserBlock    = EndorserBlockOSig true
-PreEndorserBlock = EndorserBlockOSig false
+EndorserBlock    = EndorserBlockOSig Sig
+PreEndorserBlock = EndorserBlockOSig ⊤
 
 instance
   Hashable-EndorserBlock : ⦃ Hashable PreEndorserBlock Hash ⦄ → Hashable EndorserBlock Hash
   Hashable-EndorserBlock .hash b = hash {T = PreEndorserBlock}
     record { EndorserBlockOSig b hiding (signature) ; signature = _ }
 
-  IsBlock-EndorserBlockOSig : ∀ {b} → IsBlock (EndorserBlockOSig b)
-  IsBlock-EndorserBlockOSig {b} = record { EndorserBlockOSig }
+  IsBlock-EndorserBlock : IsBlock EndorserBlock
+  IsBlock-EndorserBlock = record { EndorserBlockOSig }
+
+unquoteDecl DecEq-EndorserBlockOSig = derive-DecEq ((quote EndorserBlockOSig , DecEq-EndorserBlockOSig) ∷ [])
 
 mkEB : ⦃ Hashable PreEndorserBlock Hash ⦄ → ℕ → PoolID → VrfPf → PrivKey → List IBRef → List EBRef → EndorserBlock
 mkEB slot id π pKey LI LE = record { signature = sign pKey (hash b) ; EndorserBlockOSig b }
@@ -161,6 +171,9 @@ module GenFFD ⦃ _ : IsBlock (List Vote) ⦄ where
   data Body : Type where
     ibBody : IBBody → Body
 
+  unquoteDecl DecEq-Header DecEq-Body =
+    derive-DecEq ((quote Header , DecEq-Header) ∷ (quote Body , DecEq-Body) ∷ [])
+
   ID : Type
   ID = ℕ × PoolID
 

formal-spec/Leios/Foreign/Defaults.agda renamed to formal-spec/Leios/Defaults.agda

@@ -1,17 +1,18 @@
-{-# OPTIONS --safe #-}
+{-# OPTIONS --allow-unsolved-metas #-}
 
 open import Leios.Prelude
 open import Leios.Abstract
 open import Leios.SpecStructure
 open import Axiom.Set.Properties th
 
 open import Data.Nat.Show as N
-open import Data.Integer
+open import Data.Integer hiding (_≟_)
 open import Data.String as S using (intersperse)
 open import Function.Related.TypeIsomorphisms
 open import Relation.Binary.Structures
 
-import Data.Sum
+open import Tactic.Defaults
+open import Tactic.Derive.DecEq
 
 open Equivalence
 
@@ -21,7 +22,7 @@ open Equivalence
 -- As parameters the module expects
 -- * numberOfParties: the total number of participants
 -- * SUT-id: the number of the SUT (system under test)
-module Leios.Foreign.Defaults (numberOfParties : ℕ) (SUT-id : Fin numberOfParties) where
+module Leios.Defaults (numberOfParties : ℕ) (SUT-id : Fin numberOfParties) where
 
 instance
   htx : Hashable (List ℕ) String
@@ -90,6 +91,7 @@ d-BaseFunctionality =
   record
     { State = ⊤
     ; _-⟦_/_⟧⇀_ = λ _ _ _ _ → ⊤
+    ; Dec-_-⟦_/_⟧⇀_ = ⁇ (yes tt)
     ; SUBMIT-total = tt , tt
     }
 
@@ -104,7 +106,7 @@ instance
       ; lotteryPf = λ _ → tt
       }
 
-  hhs : ∀ {b} → Hashable (IBHeaderOSig b) String
+  hhs : Hashable PreIBHeader String
   hhs = record { hash = IBHeaderOSig.bodyHash }
 
   hpe : Hashable PreEndorserBlock String
@@ -119,6 +121,8 @@ record FFDState : Type where
         outEBs : List EndorserBlock
         outVTs : List (List Vote)
 
+unquoteDecl DecEq-FFDState = derive-DecEq ((quote FFDState , DecEq-FFDState) ∷ [])
+
 open GenFFD.Header
 open GenFFD.Body
 open FFDState
@@ -142,22 +146,54 @@ data SimpleFFD : FFDState → FFDAbstract.Input ffdAbstract → FFDAbstract.Outp
 
   Fetch : ∀ {s} → SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes (flushIns s)) (record s { inIBs = [] ; inEBs = [] ; inVTs = [] })
 
-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
+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} {ibHeader h} {nothing} = s , BadSendIB
+send-total {s} {ebHeader eb} {just _} = s , BadSendEB
+send-total {s} {vHeader 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)
+
+send-complete : ∀ {s h b s'} → SimpleFFD s (FFDAbstract.Send h b) FFDAbstract.SendRes s' → s' ≡ proj₁ (send-total {s} {h} {b})
+send-complete SendIB = refl
+send-complete SendEB = refl
+send-complete SendVS = refl
+send-complete BadSendIB = refl
+send-complete BadSendEB = refl
+send-complete BadSendVS = refl
 
-simple-total {s} {ibHeader h} {nothing} = s , BadSendIB
-simple-total {s} {ebHeader eb} {just _} = s , BadSendEB
-simple-total {s} {vHeader vs} {just _} = s , BadSendVS
+fetch-complete₁ : ∀ {s r s'} → SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes r) s' → s' ≡ proj₁ (proj₂ (fetch-total {s}))
+fetch-complete₁ Fetch = refl
+
+fetch-complete₂ : ∀ {s r s'} → SimpleFFD s FFDAbstract.Fetch (FFDAbstract.FetchRes r) s' → r ≡ proj₁ (fetch-total {s})
+fetch-complete₂ Fetch = refl
+
+instance
+  Dec-SimpleFFD : ∀ {s i o s'} → SimpleFFD s i o s' ⁇
+  Dec-SimpleFFD {s} {FFDAbstract.Send h b} {FFDAbstract.SendRes} {s'} with s' ≟ proj₁ (send-total {s} {h} {b})
+  ... | yes p rewrite p = ⁇ yes (proj₂ send-total)
+  ... | no ¬p = ⁇ no λ x → ⊥-elim (¬p (send-complete x))
+  Dec-SimpleFFD {_} {FFDAbstract.Send _ _} {FFDAbstract.FetchRes _} {_} = ⁇ no λ ()
+  Dec-SimpleFFD {s} {FFDAbstract.Fetch} {FFDAbstract.FetchRes r} {s'}
+    with s' ≟ proj₁ (proj₂ (fetch-total {s}))
+      | r ≟ proj₁ (fetch-total {s})
+  ... | yes p | yes q rewrite p rewrite q = ⁇ yes (proj₂ (proj₂ (fetch-total {s})))
+  ... | yes p | no ¬q = ⁇ no λ x → ⊥-elim (¬q (fetch-complete₂ x))
+  ... | no ¬p | _ = ⁇ no λ x → ⊥-elim (¬p (fetch-complete₁ x))
+  Dec-SimpleFFD {_} {FFDAbstract.Fetch} {FFDAbstract.SendRes} {_} = ⁇ no λ ()
 
 d-FFDFunctionality : FFDAbstract.Functionality ffdAbstract
 d-FFDFunctionality =
   record
     { State = FFDState
     ; initFFDState = record { inIBs = []; inEBs = []; inVTs = []; outIBs = []; outEBs = []; outVTs = [] }
     ; _-⟦_/_⟧⇀_ = SimpleFFD
-    ; FFD-Send-total = simple-total
+    ; Dec-_-⟦_/_⟧⇀_ = Dec-SimpleFFD
+    ; FFD-Send-total = send-total
     }
 
 open import Leios.Voting public
@@ -181,6 +217,8 @@ d-VotingAbstract-2 =
 st : SpecStructure 1
 st = record
       { a = d-Abstract
+      ; Hashable-PreIBHeader = hhs
+      ; Hashable-PreEndorserBlock = hpe
       ; id = SUT-id
       ; FFD' = d-FFDFunctionality
       ; vrf' = d-VRF
@@ -201,6 +239,8 @@ st = record
 st-2 : SpecStructure 2
 st-2 = record
       { a = d-Abstract
+      ; Hashable-PreIBHeader = hhs
+      ; Hashable-PreEndorserBlock = hpe
       ; id = SUT-id
       ; FFD' = d-FFDFunctionality
       ; vrf' = d-VRF
@@ -249,4 +289,31 @@ maximalFin (ℕ.suc n) {a} with toℕ a N.<? n
 open FunTot (completeFin numberOfParties) (maximalFin numberOfParties)
 
 sd : TotalMap (Fin numberOfParties) ℕ
-sd = Fun⇒TotalMap toℕ
+sd = Fun⇒TotalMap (const 100000000)
+
+open import Class.Computational
+open import Class.Computational22
+
+open Computational22
+open BaseAbstract
+open FFDAbstract
+
+open GenFFD.Header using (ibHeader; ebHeader; vHeader)
+open GenFFD.Body using (ibBody)
+open FFDState
+
+instance
+  Computational-B : Computational22 (BaseAbstract.Functionality._-⟦_/_⟧⇀_ d-BaseFunctionality) String
+  Computational-B .computeProof s (INIT x) = success ((STAKE sd , tt) , tt)
+  Computational-B .computeProof s (SUBMIT x) = success ((EMPTY , tt) , tt)
+  Computational-B .computeProof s FTCH-LDG = success (((BASE-LDG []) , tt) , tt)
+  Computational-B .completeness _ _ _ _ _ = {!!} -- TODO: Completeness proof
+
+  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 Fetch = success ((FetchRes (flushIns s) , record s {inIBs = []; inEBs = []; inVTs = []}) , Fetch)
+
+  Computational-FFD .computeProof _ _ = failure "FFD error"
+  Computational-FFD .completeness _ _ _ _ _ = {!!} -- TODO:Completeness proof

formal-spec/Leios/FFD.agda

@@ -6,6 +6,8 @@ open import Leios.Prelude
 
 record FFDAbstract : Type₁ where
   field Header Body ID : Type
+        ⦃ DecEq-Header ⦄ : DecEq Header
+        ⦃ DecEq-Body ⦄ : DecEq Body
         match : Header → Body → Type
         msgID : Header → ID
 
@@ -21,6 +23,7 @@ record FFDAbstract : Type₁ where
     field State : Type
           initFFDState : State
           _-⟦_/_⟧⇀_ : State → Input → Output → State → Type
+          ⦃ Dec-_-⟦_/_⟧⇀_ ⦄ : {s : State} → {i : Input} → {o : Output} → {s' : State} → (s -⟦ i / o ⟧⇀ s') ⁇
           FFD-Send-total : ∀ {ffds h b} → ∃[ ffds' ] ffds -⟦ Send h b / SendRes ⟧⇀ ffds'
 
     open Input public