diff --git a/.github/workflows/formal-spec.yaml b/.github/workflows/formal-spec.yaml
index c222ea7..20fd843 100644
--- a/.github/workflows/formal-spec.yaml
+++ b/.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
diff --git a/formal-spec/Everything.agda b/formal-spec/Everything.agda
index 6024936..bf4d9fc 100644
--- a/formal-spec/Everything.agda
+++ b/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
diff --git a/formal-spec/Leios/Abstract.agda b/formal-spec/Leios/Abstract.agda
index f8fd193..af62ad8 100644
--- a/formal-spec/Leios/Abstract.agda
+++ b/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
diff --git a/formal-spec/Leios/Base.agda b/formal-spec/Leios/Base.agda
index fc9cbbb..9987cd7 100644
--- a/formal-spec/Leios/Base.agda
+++ b/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
diff --git a/formal-spec/Leios/Blocks.agda b/formal-spec/Leios/Blocks.agda
index 29a2116..a2d509b 100644
--- a/formal-spec/Leios/Blocks.agda
+++ b/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,10 +22,6 @@ record IsBlock (B : Type) : Type where
 
 open IsBlock ⦃...⦄ public
 
-OSig : Bool → Type
-OSig true  = Sig
-OSig false = ⊤
-
 IBRef = Hash
 EBRef = Hash
 
@@ -31,15 +29,15 @@ 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,20 +48,30 @@ 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  = π
@@ -71,7 +79,7 @@ mkIBHeader slot id π pKey txs = record { signature = sign pKey (hash h) ; IBHea
                ; 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
 
diff --git a/formal-spec/Leios/Foreign/Defaults.agda b/formal-spec/Leios/Defaults.agda
similarity index 61%
rename from formal-spec/Leios/Foreign/Defaults.agda
rename to formal-spec/Leios/Defaults.agda
index 3ca74fd..7d799a7 100644
--- a/formal-spec/Leios/Foreign/Defaults.agda
+++ b/formal-spec/Leios/Defaults.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe #-}
+{-# OPTIONS --allow-unsolved-metas #-}
 
 open import Leios.Prelude
 open import Leios.Abstract
@@ -6,12 +6,13 @@ 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,14 +146,45 @@ 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 =
@@ -157,7 +192,8 @@ d-FFDFunctionality =
     { 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
diff --git a/formal-spec/Leios/FFD.agda b/formal-spec/Leios/FFD.agda
index 23f9827..1ca95ae 100644
--- a/formal-spec/Leios/FFD.agda
+++ b/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
diff --git a/formal-spec/Leios/Foreign/Types.agda b/formal-spec/Leios/Foreign/Types.agda
index 5a03def..70c978c 100644
--- a/formal-spec/Leios/Foreign/Types.agda
+++ b/formal-spec/Leios/Foreign/Types.agda
@@ -19,10 +19,7 @@ module Leios.Foreign.Types where
   {-# LANGUAGE DuplicateRecordFields #-}
 #-}
 
-numberOfParties : ℕ
-numberOfParties = 2
-
-open import Leios.Foreign.Defaults numberOfParties fzero
+open import Leios.Defaults 2 fzero -- TODO: parameters
   renaming (EndorserBlock to EndorserBlockAgda; IBHeader to IBHeaderAgda)
 
 dropDash : S.String → S.String
@@ -49,13 +46,14 @@ data IBHeader = IBHeader {slotNumber :: Integer, producerID :: Integer, bodyHash
 
 instance
   HsTy-IBHeader = MkHsType IBHeaderAgda IBHeader
+
   Conv-IBHeader : Convertible IBHeaderAgda IBHeader
   Conv-IBHeader = record
     { to = λ (record { slotNumber = s ; producerID = p ; bodyHash = h }) →
         record { slotNumber = s ; producerID = toℕ p ; bodyHash = h}
     ; from = λ (record { slotNumber = s ; producerID = p ; bodyHash = h }) →
-        case p <? numberOfParties of λ where
-          (yes q) → record { slotNumber = s ; producerID = #_ p {numberOfParties} {fromWitness q} ; lotteryPf = tt ; bodyHash = h ; signature = tt }
+        case p <? 2 of λ where
+          (yes q) → record { slotNumber = s ; producerID = #_ p {2} {fromWitness q} ; lotteryPf = tt ; bodyHash = h ; signature = tt }
           (no _) → error "Conversion to Fin not possible!"
     }
 
@@ -89,8 +87,8 @@ instance
       { to = λ (record { slotNumber = s ; producerID = p ; ibRefs = refs }) →
           record { slotNumber = s ; producerID = toℕ p ; ibRefs = refs }
       ; from = λ (record { slotNumber = s ; producerID = p ; ibRefs = refs }) →
-        case p <? numberOfParties of λ where
-          (yes q) → record { slotNumber = s ; producerID = #_ p {numberOfParties} {fromWitness q} ; lotteryPf = tt ; signature = tt ; ibRefs = refs ; ebRefs = [] }
+        case p <? 2 of λ where
+          (yes q) → record { slotNumber = s ; producerID = #_ p {2} {fromWitness q} ; lotteryPf = tt ; signature = tt ; ibRefs = refs ; ebRefs = [] }
           (no _) → error "Conversion to Fin not possible!"
       }
 
@@ -121,16 +119,17 @@ instance
   HsTy-FFDState = autoHsType FFDState
   Conv-FFDState = autoConvert FFDState
 
-  HsTy-Fin = MkHsType (Fin numberOfParties) ℕ
+  HsTy-Fin : ∀ {n} → HasHsType (Fin n)
+  HsTy-Fin .HasHsType.HsType = ℕ
 
-  Conv-Fin : HsConvertible (Fin numberOfParties)
-  Conv-Fin =
+  Conv-Fin : ∀ {n} → HsConvertible (Fin n)
+  Conv-Fin {n} =
     record
       { to = toℕ
-      ; from = λ p →
-                 case p <? numberOfParties of λ where
-                   (yes q) → #_ p {numberOfParties} {fromWitness q}
-                   (no _) → error "Conversion to Fin not possible!"
+      ; from = λ m →
+          case m <? n of λ where
+            (yes p) → #_ m {n} {fromWitness p}
+            (no _) → error "Conversion to Fin not possible!"
       }
 
   HsTy-LeiosState = autoHsType LeiosState
@@ -144,32 +143,9 @@ instance
 
 open import Class.Computational as C
 open import Class.Computational22
+open import Leios.Short.Deterministic st public
 
 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 _ _ _ _ _ = error "Computational-B completeness"
-
-  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 _ _ _ _ _ = error "Computational-FFD completeness"
-
-open import Leios.Short.Deterministic st as D public
 
 stepHs : HsType (LeiosState → LeiosInput → C.ComputationResult String (LeiosOutput × LeiosState))
 stepHs = to (compute Computational--⟦/⟧⇀)
diff --git a/formal-spec/Leios/Protocol.agda b/formal-spec/Leios/Protocol.agda
index 9e40070..916fe07 100644
--- a/formal-spec/Leios/Protocol.agda
+++ b/formal-spec/Leios/Protocol.agda
@@ -67,6 +67,9 @@ record LeiosState : Type where
   needsUpkeep : SlotUpkeep → Set
   needsUpkeep = _∉ Upkeep
 
+  Dec-needsUpkeep : ∀ {u : SlotUpkeep} → ⦃ DecEq SlotUpkeep ⦄ → needsUpkeep u ⁇
+  Dec-needsUpkeep {u} .dec = ¬? (u ∈? Upkeep)
+
 addUpkeep : LeiosState → SlotUpkeep → LeiosState
 addUpkeep s u = let open LeiosState s in record s { Upkeep = Upkeep ∪ ❴ u ❵ }
 {-# INJECTIVE_FOR_INFERENCE addUpkeep #-}
diff --git a/formal-spec/Leios/Short.lagda.md b/formal-spec/Leios/Short.lagda.md
index a3daf80..696a9c3 100644
--- a/formal-spec/Leios/Short.lagda.md
+++ b/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
@@ -84,15 +84,15 @@ data _↝_ : LeiosState → LeiosState → Type where
           s ↝ addUpkeep record s { FFDState = ffds' } EB-Role
 ```
 ```agda
-  V-Role  : let open LeiosState s renaming (FFDState to ffds)
+  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'
           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
@@ -110,11 +110,11 @@ data _↝_ : LeiosState → LeiosState → Type where
              s ↝ addUpkeep s EB-Role
 ```
 ```agda
-  No-V-Role  : let open LeiosState s in
-             ∙ needsUpkeep V-Role
+  No-VT-Role : let open LeiosState s in
+             ∙ needsUpkeep VT-Role
              ∙ ¬ canProduceV slot sk-V (stake s)
              ─────────────────────────────────────────────
-             s ↝ addUpkeep s V-Role
+             s ↝ addUpkeep s VT-Role
 ```
 ### Uniform short-pipeline
 ```agda
diff --git a/formal-spec/Leios/Short/Deterministic.agda b/formal-spec/Leios/Short/Deterministic.agda
index 33782ab..c5691e8 100644
--- a/formal-spec/Leios/Short/Deterministic.agda
+++ b/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 u (V-Role x₁ x₂) = Roles (V-Role u x₁ x₂)
-V-Role⇒ND u (No-V-Role x₁) = Roles (No-V-Role u x₁)
+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
diff --git a/formal-spec/Leios/Simplified/Deterministic/Test.agda b/formal-spec/Leios/Simplified/Deterministic/Test.agda
index a941eef..09f1d6a 100644
--- a/formal-spec/Leios/Simplified/Deterministic/Test.agda
+++ b/formal-spec/Leios/Simplified/Deterministic/Test.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 --------------------------------------------------------------------------------
 -- Deterministic variant of simple Leios
 --------------------------------------------------------------------------------
@@ -10,7 +12,7 @@ import Data.List as L
 open import Data.List.Relation.Unary.Any using (here)
 
 open import Leios.SpecStructure
-open import Leios.Trace using (st-2)
+open import Leios.Defaults 2 fzero using (st-2; isb; Computational-B; Computational-FFD)
 
 module Leios.Simplified.Deterministic.Test (Λ μ : ℕ) where
 
@@ -47,21 +49,6 @@ private variable s s' s0 s1 s2 s3 s4 s5 : LeiosState
 open Computational22 ⦃...⦄
 open import Leios.Simplified.Deterministic st-2 Λ μ
 
-instance
-  Computational-B : Computational22 B._-⟦_/_⟧⇀_ String
-  Computational-B .computeProof s (BaseAbstract.Input.INIT x) =
-    success ((BaseAbstract.Output.STAKE {!!} , tt) , tt)
-  Computational-B .computeProof s (BaseAbstract.Input.SUBMIT x) =
-    success ((BaseAbstract.Output.EMPTY , tt) , tt)
-  Computational-B .computeProof s BaseAbstract.Input.FTCH-LDG =
-    success ((BaseAbstract.Output.BASE-LDG [] , tt) , tt)
-  Computational-B .completeness = {!!}
-
-  Computational-FFD : Computational22 FFD._-⟦_/_⟧⇀_ String
-  Computational-FFD .computeProof s (FFDAbstract.Send x x₁) = success ((FFDAbstract.SendRes , tt) , tt)
-  Computational-FFD .computeProof s FFDAbstract.Fetch       = success ((FFDAbstract.FetchRes [] , tt) , tt)
-  Computational-FFD .completeness = {!!}
-
 comp = Computational--⟦/⟧⇀ ⦃ Computational-B ⦄ ⦃ Computational-FFD ⦄
 
 initLeiosState : VTy → StakeDistr → B.State → LeiosState
diff --git a/formal-spec/Leios/SpecStructure.agda b/formal-spec/Leios/SpecStructure.agda
index 0ab4317..5c14b9f 100644
--- a/formal-spec/Leios/SpecStructure.agda
+++ b/formal-spec/Leios/SpecStructure.agda
@@ -21,7 +21,7 @@ record SpecStructure (rounds : ℕ) : Type₁ where
   open Leios.Blocks a public
 
   field ⦃ IsBlock-Vote ⦄ : IsBlock (List Vote)
-        ⦃ Hashable-IBHeaderOSig ⦄ : ∀ {b} → Hashable (IBHeaderOSig b) Hash
+        ⦃ Hashable-PreIBHeader ⦄ : Hashable PreIBHeader Hash
         ⦃ Hashable-PreEndorserBlock ⦄ : Hashable PreEndorserBlock Hash
         id : PoolID
         FFD' : FFDAbstract.Functionality ffdAbstract
diff --git a/formal-spec/Leios/Trace/Decidable.agda b/formal-spec/Leios/Trace/Decidable.agda
new file mode 100644
index 0000000..2163a69
--- /dev/null
+++ b/formal-spec/Leios/Trace/Decidable.agda
@@ -0,0 +1,107 @@
+open import Leios.Prelude hiding (id)
+open import Leios.SpecStructure using (SpecStructure)
+
+module Leios.Trace.Decidable (⋯ : SpecStructure 1) (let open SpecStructure ⋯) where
+
+open import Leios.Short ⋯ renaming (isVoteCertified to isVoteCertified')
+open B hiding (_-⟦_/_⟧⇀_)
+open FFD hiding (_-⟦_/_⟧⇀_)
+
+module _ {s : LeiosState} (let open LeiosState s renaming (FFDState to ffds; BaseState to bs)) where
+
+  IB-Role? : ∀ {π ffds'} →
+           let b = GenFFD.ibBody (record { txs = ToPropose })
+               h = GenFFD.ibHeader (mkIBHeader slot id π sk-IB ToPropose)
+           in
+           { _ : auto∶ needsUpkeep IB-Role }
+           { _ : auto∶ canProduceIB slot sk-IB (stake s) π }
+           { _ : auto∶ ffds FFD.-⟦ FFD.Send h (just b) / FFD.SendRes ⟧⇀ ffds' } →
+           ─────────────────────────────────────────────────────────────────────────
+           s ↝ addUpkeep record s { FFDState = ffds' } IB-Role
+  IB-Role? {_} {_} {p} {q} {r} = IB-Role (toWitness p) (toWitness q) (toWitness r)
+
+  {-
+  No-IB-Role? :
+              { _ : auto∶ needsUpkeep IB-Role }
+              { _ : auto∶ ∀ π → ¬ canProduceIB slot sk-IB (stake s) π } →
+              ─────────────────────────────────────────────
+              s ↝ addUpkeep s IB-Role
+  No-IB-Role? {p} {q} = No-IB-Role (toWitness p) (toWitness q)
+  -}
+
+  EB-Role? : ∀ {π ffds'} →
+           let LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs
+               h = mkEB slot id π sk-EB LI []
+           in
+           { _ : auto∶ needsUpkeep EB-Role }
+           { _ : auto∶ canProduceEB slot sk-EB (stake s) π }
+           { _ : auto∶ ffds FFD.-⟦ FFD.Send (GenFFD.ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds' } →
+           ─────────────────────────────────────────────────────────────────────────
+           s ↝ addUpkeep record s { FFDState = ffds' } EB-Role
+  EB-Role? {_} {_} {p} {q} {r} = EB-Role (toWitness p) (toWitness q) (toWitness r)
+
+  {-
+  No-EB-Role? :
+              { _ : auto∶ needsUpkeep EB-Role }
+              { _ : auto∶ ∀ π → ¬ canProduceEB slot sk-EB (stake s) π } →
+              ─────────────────────────────────────────────
+              s ↝ addUpkeep s EB-Role
+  No-EB-Role? {_} {p} {q} = No-EB-Role (toWitness p) (toWitness q)
+  -}
+
+  V-Role? : ∀ {ffds'} →
+          let EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs
+              votes = map (vote sk-V ∘ hash) EBs'
+          in
+          { _ : 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' } VT-Role
+  V-Role? {_} {p} {q} {r} = VT-Role (toWitness p) (toWitness q) (toWitness r)
+
+  No-V-Role? :
+             { _ : auto∶ needsUpkeep VT-Role }
+             { _ : auto∶ ¬ canProduceV slot sk-V (stake s) } →
+             ─────────────────────────────────────────────
+             s ↝ addUpkeep s VT-Role
+  No-V-Role? {p} {q} = No-VT-Role (toWitness p) (toWitness q)
+
+  {-
+  Init? : ∀ {ks pks ks' SD bs' V} →
+        { _ : auto∶ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks' }
+        { _ : initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs' } →
+        ────────────────────────────────────────────────────────────────
+        nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs'
+  Init? = ?
+  -}
+
+  Base₂a? : ∀ {eb bs'} →
+          { _ : auto∶ needsUpkeep Base }
+          { _ : auto∶ eb ∈ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs }
+          { _ : auto∶ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs' } →
+          ───────────────────────────────────────────────────────────────────────
+          just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base
+  Base₂a? {_} {_} {p} {q} {r} = Base₂a (toWitness p) (toWitness q) (toWitness r)
+
+  Base₂b? : ∀ {bs'} →
+          { _ : auto∶ needsUpkeep Base }
+          { _ : auto∶ [] ≡ filter (λ eb → isVoteCertified' s eb × eb ∈ᴮ slice L slot 2) EBs }
+          { _ : auto∶ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs' } →
+          ───────────────────────────────────────────────────────────────────────
+          just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base
+  Base₂b? {_} {p} {q} {r} = Base₂b (toWitness p) (toWitness q) (toWitness r)
+
+  Slot? : ∀ {rbs bs' msgs ffds'} →
+         { _ : auto∶ Upkeep ≡ᵉ allUpkeep }
+         { _ : auto∶ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs' }
+         { _ : auto∶ ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds' } →
+         ───────────────────────────────────────────────────────────────────────
+         just s -⟦ SLOT / EMPTY ⟧⇀ record s
+             { FFDState  = ffds'
+             ; BaseState = bs'
+             ; Ledger    = constructLedger rbs
+             ; slot      = suc slot
+             ; Upkeep    = ∅
+             } ↑ L.filter GenFFD.isValid? msgs
+  Slot? {_} {_} {_} {_} {p} {q} {r} = Slot (toWitness p) (toWitness q) (toWitness r)
diff --git a/formal-spec/Leios/Trace/Verifier.agda b/formal-spec/Leios/Trace/Verifier.agda
new file mode 100644
index 0000000..8a315e8
--- /dev/null
+++ b/formal-spec/Leios/Trace/Verifier.agda
@@ -0,0 +1,439 @@
+open import Leios.Prelude hiding (id)
+
+module Leios.Trace.Verifier (numberOfParties : ℕ) (SUT-id : Fin numberOfParties) where
+
+open import Leios.SpecStructure using (SpecStructure)
+open import Leios.Defaults numberOfParties SUT-id using (st; sd; LeiosState; initLeiosState; isb; hpe; hhs; htx; SendIB; FFDState; Dec-SimpleFFD; send-total; fetch-total)
+open SpecStructure st hiding (Hashable-IBHeader; Hashable-EndorserBlock; isVoteCertified)
+
+open import Leios.Short st hiding (LeiosState; initLeiosState)
+open import Prelude.Closures _↝_
+open GenFFD
+
+data FFDUpdate : Type where
+  IB-Recv-Update : InputBlock → FFDUpdate
+  EB-Recv-Update : EndorserBlock → FFDUpdate
+  VT-Recv-Update : List Vote → FFDUpdate
+
+data Action : Type where
+  IB-Role-Action : ℕ → Action
+  EB-Role-Action : ℕ → List String → Action
+  VT-Role-Action : ℕ → Action
+  No-IB-Role-Action No-EB-Role-Action No-VT-Role-Action : Action
+  Ftch-Action : Action
+  Slot-Action : ℕ → Action
+  Base₁-Action : Action
+  Base₂a-Action : EndorserBlock → Action
+  Base₂b-Action : Action
+
+Actions = List (Action × LeiosInput)
+
+private variable
+  s s′ : LeiosState
+  α : Action
+
+data ValidUpdate : FFDUpdate → LeiosState → Type where
+
+  IB-Recv : ∀ {ib} →
+    ValidUpdate (IB-Recv-Update ib) s
+
+  EB-Recv : ∀ {eb} →
+    ValidUpdate (EB-Recv-Update eb) s
+
+  VT-Recv : ∀ {vt} →
+    ValidUpdate (VT-Recv-Update vt) s
+
+data ValidAction : Action → LeiosState → LeiosInput → Type where
+
+  IB-Role : let open LeiosState s renaming (FFDState to ffds)
+                b = record { txs = ToPropose }
+                h = mkIBHeader slot id tt sk-IB ToPropose
+                ffds' = proj₁ (send-total {ffds} {ibHeader h} {just (ibBody b)})
+            in .(needsUpkeep IB-Role) →
+               .(canProduceIB slot sk-IB (stake s) tt) →
+               .(ffds FFD.-⟦ FFD.Send (ibHeader h) (just (ibBody b)) / FFD.SendRes ⟧⇀ ffds') →
+               ValidAction (IB-Role-Action slot) s SLOT
+
+  EB-Role : let open LeiosState s renaming (FFDState to ffds)
+                LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs
+                h = mkEB slot id tt sk-EB LI []
+                ffds' = proj₁ (send-total {ffds} {ebHeader h} {nothing})
+            in .(needsUpkeep EB-Role) →
+               .(canProduceEB slot sk-EB (stake s) tt) →
+               .(ffds FFD.-⟦ FFD.Send (ebHeader h) nothing / FFD.SendRes ⟧⇀ ffds') →
+               ValidAction (EB-Role-Action slot LI) s SLOT
+
+  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})
+            in .(needsUpkeep VT-Role) →
+               .(canProduceV slot sk-V (stake s)) →
+               .(ffds FFD.-⟦ FFD.Send (vHeader votes) nothing / FFD.SendRes ⟧⇀ ffds') →
+               ValidAction (VT-Role-Action slot) s SLOT
+
+  No-IB-Role : let open LeiosState s
+               in needsUpkeep IB-Role →
+                  (∀ π → ¬ canProduceIB slot sk-IB (stake s) π) →
+                  ValidAction No-IB-Role-Action s SLOT
+
+  No-EB-Role : let open LeiosState s
+               in needsUpkeep EB-Role →
+                  (∀ π → ¬ canProduceEB slot sk-EB (stake s) π) →
+                  ValidAction No-EB-Role-Action s SLOT
+
+  No-VT-Role : let open LeiosState s
+               in needsUpkeep VT-Role →
+                  (¬ canProduceV slot sk-V (stake s)) →
+                  ValidAction No-VT-Role-Action s SLOT
+
+  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) →
+            .(ffds FFD.-⟦ FFD.Fetch / FFD.FetchRes msgs ⟧⇀ ffds') →
+            ValidAction (Slot-Action slot) 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 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
+  o : LeiosOutput
+
+⟦_⟧ : ValidAction α s i → LeiosState × LeiosOutput
+⟦ IB-Role {s} _ _ _ ⟧ =
+  let open LeiosState s renaming (FFDState to ffds)
+      b = record { txs = ToPropose }
+      h = mkIBHeader slot id tt sk-IB ToPropose
+      ffds' = proj₁ (send-total {ffds} {ibHeader h} {just (ibBody b)})
+  in addUpkeep record s { FFDState = ffds' } IB-Role , EMPTY
+⟦ EB-Role {s} _ _ _ ⟧ =
+  let open LeiosState s renaming (FFDState to ffds)
+      LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs
+      h = mkEB slot id tt sk-EB LI []
+      ffds' = proj₁ (send-total {ffds} {ebHeader h} {nothing})
+  in addUpkeep record s { FFDState = ffds' } EB-Role , EMPTY
+⟦ VT-Role {s} _ _ _ ⟧ =
+  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})
+  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 VT-Role , EMPTY
+⟦ Slot {s} _ _ _ ⟧ =
+  let open LeiosState s renaming (FFDState to ffds)
+      (msgs , (ffds' , _)) = fetch-total {ffds}
+  in
+  (record s
+     { FFDState  = ffds'
+     ; BaseState = tt
+     ; Ledger    = constructLedger []
+     ; slot      = suc slot
+     ; Upkeep    = ∅
+     } ↑ L.filter isValid? msgs
+  , EMPTY)
+⟦ Ftch {s} ⟧ = s , FTCH-LDG (LeiosState.Ledger s)
+⟦ Base₁ {s} {txs} ⟧ = record s { ToPropose = txs } , EMPTY
+⟦ Base₂a {s} _ _ _ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY
+⟦ Base₂b {s} _ _ _ ⟧ = addUpkeep record s { BaseState = tt } Base , EMPTY
+
+ValidAction→Eq-Slot : ∀ {s sl} → ValidAction (Slot-Action sl) s SLOT → sl ≡ LeiosState.slot s
+ValidAction→Eq-Slot (Slot _ _ _) = refl
+
+ValidAction→Eq-IB : ∀ {s sl} → ValidAction (IB-Role-Action sl) s SLOT → sl ≡ LeiosState.slot s
+ValidAction→Eq-IB (IB-Role _ _ _) = refl
+
+ValidAction→Eq-EB : ∀ {s sl ibs} →
+  let open LeiosState s
+  in ValidAction (EB-Role-Action sl ibs) s SLOT → sl ≡ slot × ibs ≡ (map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs)
+ValidAction→Eq-EB (EB-Role _ _ _) = refl , refl
+
+ValidAction→Eq-VT : ∀ {s sl} → ValidAction (VT-Role-Action sl) s SLOT → sl ≡ LeiosState.slot s
+ValidAction→Eq-VT (VT-Role _ _ _) = refl
+
+instance
+  Dec-ValidAction : ValidAction ⁇³
+  Dec-ValidAction {IB-Role-Action sl} {s} {SLOT} .dec
+    with sl ≟ LeiosState.slot s
+  ... | no ¬p = no λ x → ⊥-elim (¬p (ValidAction→Eq-IB x))
+  ... | yes p rewrite p
+    with dec | dec | dec
+  ... | yes x | yes y | yes z = yes (IB-Role x y z)
+  ... | no ¬p | _ | _ = no λ where (IB-Role p _ _) → ⊥-elim (¬p (recompute dec p))
+  ... | _ | no ¬p | _ = no λ where (IB-Role _ p _) → ⊥-elim (¬p (recompute dec p))
+  ... | _ | _ | no ¬p = no λ where (IB-Role _ _ p) → ⊥-elim (¬p (recompute dec p))
+  Dec-ValidAction {IB-Role-Action _} {s} {INIT _} .dec = no λ ()
+  Dec-ValidAction {IB-Role-Action _} {s} {SUBMIT _} .dec = no λ ()
+  Dec-ValidAction {IB-Role-Action _} {s} {FTCH-LDG} .dec = no λ ()
+  Dec-ValidAction {EB-Role-Action sl ibs} {s} {SLOT} .dec
+    with sl ≟ LeiosState.slot s | ibs ≟ (map getIBRef $ filter (_∈ᴮ slice L (LeiosState.slot s) 3) (LeiosState.IBs s))
+  ... | no ¬p | _ = no λ x → ⊥-elim (¬p (proj₁ $ ValidAction→Eq-EB x))
+  ... | _ | no ¬q = no λ x → ⊥-elim (¬q (proj₂ $ ValidAction→Eq-EB x))
+  ... | yes p | yes q rewrite p rewrite q
+    with dec | dec | dec
+  ... | yes x | yes y | yes z = yes (EB-Role x y z)
+  ... | no ¬p | _ | _ = no λ where (EB-Role p _ _) → ⊥-elim (¬p (recompute dec p))
+  ... | _ | no ¬p | _ = no λ where (EB-Role _ p _) → ⊥-elim (¬p (recompute dec p))
+  ... | _ | _ | no ¬p = no λ where (EB-Role _ _ p) → ⊥-elim (¬p (recompute dec p))
+  Dec-ValidAction {EB-Role-Action _ _} {s} {INIT _} .dec = no λ ()
+  Dec-ValidAction {EB-Role-Action _ _} {s} {SUBMIT _} .dec = no λ ()
+  Dec-ValidAction {EB-Role-Action _ _} {s} {FTCH-LDG} .dec = no λ ()
+  Dec-ValidAction {VT-Role-Action sl} {s} {SLOT} .dec
+    with sl ≟ LeiosState.slot s
+  ... | no ¬p = no λ x → ⊥-elim (¬p (ValidAction→Eq-VT x))
+  ... | yes p rewrite p
+    with dec | dec | dec
+  ... | yes x | yes y | yes z = yes (VT-Role x y z)
+  ... | no ¬p | _ | _ = no λ where (VT-Role p _ _) → ⊥-elim (¬p (recompute dec p))
+  ... | _ | no ¬p | _ = no λ where (VT-Role _ p _) → ⊥-elim (¬p (recompute dec p))
+  ... | _ | _ | no ¬p = no λ where (VT-Role _ _ p) → ⊥-elim (¬p (recompute dec p))
+  Dec-ValidAction {VT-Role-Action _} {s} {INIT _} .dec = no λ ()
+  Dec-ValidAction {VT-Role-Action _} {s} {SUBMIT _} .dec = no λ ()
+  Dec-ValidAction {VT-Role-Action _} {s} {FTCH-LDG} .dec = no λ ()
+  Dec-ValidAction {No-IB-Role-Action} {s} {SLOT} .dec
+    with dec | dec
+  ... | yes p | yes q = yes (No-IB-Role p q)
+  ... | no ¬p | _ = no λ where (No-IB-Role p _) → ⊥-elim (¬p p)
+  ... | _ | no ¬q = no λ where (No-IB-Role _ q) → ⊥-elim (¬q q)
+  Dec-ValidAction {No-IB-Role-Action} {s} {INIT _} .dec = no λ ()
+  Dec-ValidAction {No-IB-Role-Action} {s} {SUBMIT _} .dec = no λ ()
+  Dec-ValidAction {No-IB-Role-Action} {s} {FTCH-LDG} .dec = no λ ()
+  Dec-ValidAction {No-EB-Role-Action} {s} {SLOT} .dec
+    with dec | dec
+  ... | yes p | yes q = yes (No-EB-Role p q)
+  ... | no ¬p | _ = no λ where (No-EB-Role p _) → ⊥-elim (¬p p)
+  ... | _ | no ¬q = no λ where (No-EB-Role _ q) → ⊥-elim (¬q q)
+  Dec-ValidAction {No-EB-Role-Action} {s} {INIT _} .dec = no λ ()
+  Dec-ValidAction {No-EB-Role-Action} {s} {SUBMIT _} .dec = no λ ()
+  Dec-ValidAction {No-EB-Role-Action} {s} {FTCH-LDG} .dec = no λ ()
+  Dec-ValidAction {No-VT-Role-Action} {s} {SLOT} .dec
+    with dec | dec
+  ... | yes p | yes q = yes (No-VT-Role p q)
+  ... | no ¬p | _ = no λ where (No-VT-Role p _) → ⊥-elim (¬p p)
+  ... | _ | no ¬q = no λ where (No-VT-Role _ q) → ⊥-elim (¬q q)
+  Dec-ValidAction {No-VT-Role-Action} {s} {INIT _} .dec = no λ ()
+  Dec-ValidAction {No-VT-Role-Action} {s} {SUBMIT _} .dec = no λ ()
+  Dec-ValidAction {No-VT-Role-Action} {s} {FTCH-LDG} .dec = no λ ()
+  Dec-ValidAction {Slot-Action sl} {s} {SLOT} .dec
+    with sl ≟ LeiosState.slot s
+  ... | no ¬p = no λ x → ⊥-elim (¬p (ValidAction→Eq-Slot x))
+  ... | yes p rewrite p
+    with dec | dec | dec
+  ... | yes x | yes y | yes z = yes (Slot x y z)
+  ... | no ¬p | _ | _ = no λ where (Slot p _ _) → ⊥-elim (¬p (recompute dec p))
+  ... | _ | no ¬p | _ = no λ where (Slot _ p _) → ⊥-elim (¬p (recompute dec p))
+  ... | _ | _ | no ¬p = no λ where (Slot _ _ p) → ⊥-elim (¬p (recompute dec p))
+  Dec-ValidAction {Slot-Action _} {s} {INIT _} .dec = no λ ()
+  Dec-ValidAction {Slot-Action _} {s} {SUBMIT _} .dec = no λ ()
+  Dec-ValidAction {Slot-Action _} {s} {FTCH-LDG} .dec = no λ ()
+  Dec-ValidAction {Ftch-Action} {s} {FTCH-LDG} .dec = yes Ftch
+  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 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 {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₂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))
+  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 λ ()
+
+instance
+  Dec-ValidUpdate : ValidUpdate ⁇²
+  Dec-ValidUpdate {IB-Recv-Update _} .dec = yes IB-Recv
+  Dec-ValidUpdate {EB-Recv-Update _} .dec = yes EB-Recv
+  Dec-ValidUpdate {VT-Recv-Update _} .dec = yes VT-Recv
+
+mutual
+  data ValidTrace : List ((Action × LeiosInput) ⊎ FFDUpdate) → Type where
+    [] :
+      ─────────────
+      ValidTrace []
+
+    _/_∷_⊣_ : ∀ α i {αs} →
+      ∀ (tr : ValidTrace αs) →
+      ∙ ValidAction α (proj₁ ⟦ tr ⟧∗) i
+        ───────────────────
+        ValidTrace (inj₁ (α , i) ∷ αs)
+
+    _↥_ : ∀ {f αs} →
+      ∀ (tr : ValidTrace αs) →
+        (vu : ValidUpdate f (proj₁ ⟦ tr ⟧∗)) →
+        ───────────────────
+        ValidTrace (inj₂ f ∷ αs)
+
+
+  ⟦_⟧∗ : ∀ {αs : List ((Action × LeiosInput) ⊎ FFDUpdate)} → ValidTrace αs → LeiosState × LeiosOutput
+  ⟦_⟧∗ [] = initLeiosState tt sd tt , EMPTY
+  ⟦_⟧∗ (_ / _ ∷ _ ⊣ vα) = ⟦ vα ⟧
+  ⟦ _↥_ {IB-Recv-Update ib} tr vu ⟧∗ =
+    let (s , o) = ⟦ tr ⟧∗
+    in record s { FFDState = record (LeiosState.FFDState s) { inIBs = ib ∷ FFDState.inIBs (LeiosState.FFDState s)}} , o
+  ⟦ _↥_ {EB-Recv-Update eb} tr vu ⟧∗ =
+    let (s , o) = ⟦ tr ⟧∗
+    in record s { FFDState = record (LeiosState.FFDState s) { inEBs = eb ∷ FFDState.inEBs (LeiosState.FFDState s)}} , o
+  ⟦ _↥_ {VT-Recv-Update vt} tr vu ⟧∗ =
+    let (s , o) = ⟦ tr ⟧∗
+    in record s { FFDState = record (LeiosState.FFDState s) { inVTs = vt ∷ FFDState.inVTs (LeiosState.FFDState s)}} , o
+
+
+Irr-ValidAction : Irrelevant (ValidAction α s i)
+Irr-ValidAction (IB-Role _ _ _) (IB-Role _ _ _) = refl
+Irr-ValidAction (EB-Role _ _ _) (EB-Role _ _ _) = refl
+Irr-ValidAction (VT-Role _ _ _) (VT-Role _ _ _) = refl
+Irr-ValidAction (No-IB-Role _ _) (No-IB-Role _ _) = refl
+Irr-ValidAction (No-EB-Role _ _) (No-EB-Role _ _) = refl
+Irr-ValidAction (No-VT-Role _ _) (No-VT-Role _ _) = refl
+Irr-ValidAction (Slot _ _ _) (Slot _ _ _) = refl
+Irr-ValidAction Ftch Ftch = refl
+Irr-ValidAction Base₁ Base₁ = refl
+Irr-ValidAction (Base₂a _ _ _) (Base₂a _ _ _) = refl
+Irr-ValidAction (Base₂b _ _ _) (Base₂b _ _ _) = refl
+
+Irr-ValidUpdate : ∀ {f} → Irrelevant (ValidUpdate f s)
+Irr-ValidUpdate IB-Recv IB-Recv = refl
+Irr-ValidUpdate EB-Recv EB-Recv = refl
+Irr-ValidUpdate VT-Recv VT-Recv = refl
+
+Irr-ValidTrace : ∀ {αs} → Irrelevant (ValidTrace αs)
+Irr-ValidTrace [] [] = refl
+Irr-ValidTrace (α / i ∷ vαs ⊣ vα) (.α / .i ∷ vαs′ ⊣ vα′)
+  rewrite Irr-ValidTrace vαs vαs′ | Irr-ValidAction vα vα′
+  = refl
+Irr-ValidTrace (vαs ↥ u) (vαs′ ↥ u′)
+  rewrite Irr-ValidTrace vαs vαs′ | Irr-ValidUpdate u u′
+  = refl
+
+instance
+  Dec-ValidTrace : ValidTrace ⁇¹
+  Dec-ValidTrace {tr} .dec with tr
+  ... | [] = yes []
+  ... | inj₁ (α , i) ∷ αs
+    with ¿ ValidTrace αs ¿
+  ... | no ¬vαs = no λ where (_ / _ ∷ vαs ⊣ _) → ¬vαs vαs
+  ... | yes vαs
+    with ¿ ValidAction α (proj₁ ⟦ vαs ⟧∗) i ¿
+  ... | no ¬vα = no λ where
+    (_ / _ ∷ 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
+  ... | yes vαs
+    with ¿ ValidUpdate u (proj₁ ⟦ vαs ⟧∗) ¿
+  ... | yes vu = yes (vαs ↥ vu)
+  ... | no ¬vu = no λ where
+    (tr ↥ vu) → ¬vu $ subst (λ x → ValidUpdate u x) (cong (proj₁ ∘ ⟦_⟧∗) $ Irr-ValidTrace tr vαs) vu
+
+data _⇑_ : LeiosState → LeiosState → Type where
+
+  UpdateIB : ∀ {s ib} → let open LeiosState s renaming (FFDState to ffds) in
+    s ⇑ record s { FFDState = record ffds { inIBs = ib ∷ FFDState.inIBs ffds } }
+
+  UpdateEB : ∀ {s eb} → let open LeiosState s renaming (FFDState to ffds) in
+    s ⇑ record s { FFDState = record ffds { inEBs = eb ∷ FFDState.inEBs ffds } }
+
+  UpdateVT : ∀ {s vt} → let open LeiosState s renaming (FFDState to ffds) in
+    s ⇑ record s { FFDState = record ffds { inVTs = vt ∷ FFDState.inVTs ffds } }
+
+data LocalStep : LeiosState → LeiosState → Type where
+
+  StateStep : ∀ {s i o s′} →
+    ∙ just s -⟦ i / o ⟧⇀ s′
+      ───────────────────
+      LocalStep s s′
+
+  UpdateState : ∀ {s s′} →
+    ∙ s ⇑ s′
+      ───────────────────
+      LocalStep s s′
+
+  -- TODO: add base layer update
+
+getLabel : just s -⟦ i / o ⟧⇀ s′ → Action
+getLabel (Slot {s} _ _ _)            = Slot-Action (LeiosState.slot s)
+getLabel Ftch                        = Ftch-Action
+getLabel Base₁                       = Base₁-Action
+getLabel (Base₂a {s} {eb} _ _ _)     = Base₂a-Action eb
+getLabel (Base₂b _ _ _)              = Base₂b-Action
+getLabel (Roles (IB-Role {s} _ _ _)) = IB-Role-Action (LeiosState.slot s)
+getLabel (Roles (EB-Role {s} _ _ _)) = let open LeiosState s in EB-Role-Action slot (map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs)
+getLabel (Roles (VT-Role {s} _ _ _)) = VT-Role-Action (LeiosState.slot s)
+getLabel (Roles (No-IB-Role _ _))    = No-IB-Role-Action
+getLabel (Roles (No-EB-Role _ _))    = No-EB-Role-Action
+getLabel (Roles (No-VT-Role _ _))    = No-VT-Role-Action
+
+ValidAction-sound : (va : ValidAction α s i) → let (s′ , o) = ⟦ va ⟧ in just s -⟦ i / o ⟧⇀ s′
+ValidAction-sound (Slot x x₁ x₂)    = Slot {rbs = []} (recompute dec x) (recompute dec x₁) (recompute dec x₂)
+ValidAction-sound Ftch              = Ftch
+ValidAction-sound Base₁             = Base₁
+ValidAction-sound (Base₂a x x₁ x₂)  = Base₂a (recompute dec x) (recompute dec x₁) (recompute dec x₂)
+ValidAction-sound (Base₂b x x₁ x₂)  = Base₂b (recompute dec x) (recompute dec x₁) (recompute dec x₂)
+ValidAction-sound (IB-Role x x₁ x₂) = Roles (IB-Role (recompute dec x) (recompute dec x₁) (recompute dec x₂))
+ValidAction-sound (EB-Role x x₁ x₂) = Roles (EB-Role (recompute dec x) (recompute dec x₁) (recompute dec x₂))
+ValidAction-sound (VT-Role x x₁ x₂) = Roles (VT-Role (recompute dec x) (recompute dec x₁) (recompute dec x₂))
+ValidAction-sound (No-IB-Role x x₁) = Roles (No-IB-Role x x₁)
+ValidAction-sound (No-EB-Role x x₁) = Roles (No-EB-Role x x₁)
+ValidAction-sound (No-VT-Role x x₁) = Roles (No-VT-Role 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₁ _)) =
+  let open LeiosState s renaming (FFDState to ffds)
+      b = record { txs = ToPropose }
+      h = mkIBHeader slot id tt sk-IB ToPropose
+      pr = proj₂ (send-total {ffds} {ibHeader h} {just (ibBody b)})
+  in IB-Role {s} x x₁ pr
+ValidAction-complete {s} (Roles (EB-Role x x₁ _)) =
+  let open LeiosState s renaming (FFDState to ffds)
+      LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs
+      h = mkEB slot id tt sk-EB LI []
+      pr = proj₂ (send-total {ffds} {ebHeader h} {nothing})
+  in EB-Role {s} x x₁ pr
+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})
+  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₁
+ValidAction-complete (Roles (No-VT-Role x x₁)) = No-VT-Role x x₁
+ValidAction-complete Ftch                      = Ftch
+ValidAction-complete Base₁                     = Base₁
+ValidAction-complete (Base₂a x x₁ x₂)          = Base₂a x x₁ x₂
+ValidAction-complete (Base₂b x x₁ x₂)          = Base₂b x x₁ x₂
+ValidAction-complete {s} (Slot x x₁ _)         = Slot x x₁ (proj₂ (proj₂ (fetch-total {LeiosState.FFDState s})))
diff --git a/formal-spec/Leios/Trace/Verifier/Test.agda b/formal-spec/Leios/Trace/Verifier/Test.agda
new file mode 100644
index 0000000..9ba2423
--- /dev/null
+++ b/formal-spec/Leios/Trace/Verifier/Test.agda
@@ -0,0 +1,44 @@
+open import Leios.Prelude hiding (id)
+
+module Leios.Trace.Verifier.Test where
+
+open import Leios.Trace.Verifier 2 fzero
+open import Leios.Defaults 2 fzero
+
+private
+  opaque
+    unfolding List-Model
+
+    test₁ : Bool
+    test₁ = ¿ ValidTrace (inj₁ (IB-Role-Action 0 , SLOT) ∷ []) ¿ᵇ
+
+    _ : test₁ ≡ true
+    _ = refl
+
+    test₂ : Bool
+    test₂ =
+      let t = L.reverse $
+              inj₁ (IB-Role-Action 0    , SLOT)
+            ∷ inj₁ (EB-Role-Action 0 [] , SLOT)
+            ∷ inj₁ (VT-Role-Action 0    , SLOT)
+            ∷ inj₁ (Base₂b-Action       , SLOT)
+            ∷ inj₁ (Slot-Action    0    , SLOT)
+            ∷ inj₁ (IB-Role-Action 1    , SLOT)
+            ∷ inj₁ (EB-Role-Action 1 [] , SLOT)
+            ∷ inj₁ (VT-Role-Action 1    , SLOT)
+            ∷ inj₁ (Base₂b-Action       , SLOT)
+            ∷ inj₁ (Slot-Action    1    , SLOT)
+            ∷ inj₂ (IB-Recv-Update
+                (record { header =
+                  record { slotNumber = 1
+                         ; producerID = fsuc fzero
+                         ; lotteryPf = tt
+                         ; bodyHash = "0,1,2"
+                         ; signature = tt
+                         }
+                        ; body = record { txs = 0 ∷ 1 ∷ 2 ∷ [] }}))
+            ∷ []
+      in ¿ ValidTrace t ¿ᵇ
+
+    _ : test₂ ≡ true
+    _ = refl