Cleanup various things

formal-spec/Everything.agda

@@ -1,5 +1,3 @@
-{-# OPTIONS --erasure #-}
-
 module Everything where
 
 open import Leios.Simplified

formal-spec/Leios/Base.agda

@@ -19,10 +19,10 @@ record BaseAbstract : Type₁ where
   field Cert : Type
         VTy : Type
         initSlot : VTy → ℕ
-        V-chkCerts : List PubKey → EndorserBlock × Cert → Type
+        V-chkCerts : List PubKey → EndorserBlock × Cert → Bool
 
-  data Input : Type₁ where
-    INIT   : (EndorserBlock × Cert → Type) → Input
+  data Input : Type where
+    INIT   : (EndorserBlock × Cert → Bool) → Input
     SUBMIT : RankingBlock → Input
     FTCH-LDG : Input
 
@@ -34,6 +34,7 @@ record BaseAbstract : Type₁ where
   record Functionality : Type₁ where
     field State : Type
           _-⟦_/_⟧⇀_ : State → Input → Output → State → Type
+          SUBMIT-total : ∀ {s b} → ∃[ s' ] s -⟦ SUBMIT b / EMPTY ⟧⇀ s'
 
     open Input public
     open Output public

formal-spec/Leios/FFD.agda

@@ -21,6 +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'
 
     open Input public
     open Output public

formal-spec/Leios/Prelude.agda

@@ -36,3 +36,10 @@ filter P = L.filter ¿ P ¿¹
 instance
   IsSet-List : {A : Set} → IsSet (List A) A
   IsSet-List .toSet A = fromList A
+
+open import Data.List.Relation.Unary.Any
+open Properties
+
+finite⇒A≡∅⊎∃a∈A : {X : Type} → {A : ℙ X} → finite A → (A ≡ᵉ ∅) ⊎ Σ[ a ∈ X ] a ∈ A
+finite⇒A≡∅⊎∃a∈A ([]    , h) = inj₁ (∅-least (λ a∈A → ⊥-elim (case Equivalence.to h a∈A of λ ())))
+finite⇒A≡∅⊎∃a∈A (x ∷ _ , h) = inj₂ (x , Equivalence.from h (here refl))

formal-spec/Leios/Protocol.agda

@@ -69,6 +69,7 @@ record LeiosState : Type where
 
 addUpkeep : LeiosState → SlotUpkeep → LeiosState
 addUpkeep s u = let open LeiosState s in record s { Upkeep = Upkeep ∪ ❴ u ❵ }
+{-# INJECTIVE_FOR_INFERENCE addUpkeep #-}
 
 initLeiosState : VTy → StakeDistr → B.State → LeiosState
 initLeiosState V SD bs = record