Various fixes and other changes

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

@@ -4,7 +4,7 @@ open import Leios.Prelude hiding (id)
 open import Leios.FFD
 open import Leios.SpecStructure
 
-module Leios.Protocol (⋯ : SpecStructure) (let open SpecStructure ⋯) (SlotUpkeep : Type) where
+module Leios.Protocol {n} (⋯ : SpecStructure n) (let open SpecStructure ⋯) (SlotUpkeep : Type) where
 
 open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot)
 open GenFFD
@@ -31,19 +31,20 @@ data LeiosOutput : Type where
   EMPTY    : LeiosOutput
 
 record LeiosState : Type where
-  field V         : VTy
-        SD        : StakeDistr
-        FFDState  : FFD.State
-        Ledger    : List Tx
-        ToPropose : List Tx
-        IBs       : List InputBlock
-        EBs       : List EndorserBlock
-        Vs        : List (List Vote)
-        slot      : ℕ
-        IBHeaders : List IBHeader
-        IBBodies  : List IBBody
-        Upkeep    : ℙ SlotUpkeep
-        BaseState : B.State
+  field V           : VTy
+        SD          : StakeDistr
+        FFDState    : FFD.State
+        Ledger      : List Tx
+        ToPropose   : List Tx
+        IBs         : List InputBlock
+        EBs         : List EndorserBlock
+        Vs          : List (List Vote)
+        slot        : ℕ
+        IBHeaders   : List IBHeader
+        IBBodies    : List IBBody
+        Upkeep      : ℙ SlotUpkeep
+        BaseState   : B.State
+        votingState : VotingState
 
   lookupEB : EBRef → Maybe EndorserBlock
   lookupEB r = find (λ b → getEBRef b ≟ r) EBs
@@ -68,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
@@ -84,6 +86,7 @@ initLeiosState V SD bs = record
   ; IBBodies    = []
   ; Upkeep      = ∅
   ; BaseState   = bs
+  ; votingState = initVotingState
   }
 
 -- some predicates about EBs

formal-spec/Leios/SpecStructure.agda

@@ -8,10 +8,13 @@ open import Leios.VRF
 import Leios.Base
 import Leios.Blocks
 import Leios.KeyRegistration
+import Leios.Voting
+
+open import Data.Fin
 
 module Leios.SpecStructure where
 
-record SpecStructure : Type₁ where
+record SpecStructure (rounds : ℕ) : Type₁ where
   field a : LeiosAbstract
 
   open LeiosAbstract a public
@@ -43,3 +46,8 @@ record SpecStructure : Type₁ where
   module B   = BaseAbstract.Functionality BF
   module K   = KeyRegistrationAbstract.Functionality KF
   module FFD = FFDAbstract.Functionality FFD'
+
+  open Leios.Voting public
+
+  field va : VotingAbstract (Fin rounds × EndorserBlock)
+  open VotingAbstract va public

formal-spec/Leios/UniformShort.agda

@@ -3,8 +3,10 @@
 open import Leios.Prelude hiding (id)
 open import Leios.FFD
 open import Leios.SpecStructure
+open import Data.Fin.Patterns
 
-module Leios.UniformShort (⋯ : SpecStructure) (let open SpecStructure ⋯) where
+module Leios.UniformShort (⋯ : SpecStructure 1)
+  (let open SpecStructure ⋯ renaming (isVoteCertified to isVoteCertified')) where
 
 data SlotUpkeep : Type where
   Base IB-Role EB-Role V-Role : SlotUpkeep
@@ -18,11 +20,10 @@ open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot)
 open FFD hiding (_-⟦_/_⟧⇀_)
 open GenFFD
 
-record VotingAbstract : Type₁ where
-  field isVoteCertified : LeiosState → EndorserBlock → Type
-        ⦃ isVoteCertified⁇ ⦄ : ∀ {vs eb} → isVoteCertified vs eb ⁇
+isVoteCertified : LeiosState → EndorserBlock → Type
+isVoteCertified s eb = isVoteCertified' (LeiosState.votingState s) (0F , eb)
 
-module Protocol (va : VotingAbstract) (let open VotingAbstract va) where
+module Protocol where
 
   private variable s s'   : LeiosState
                    ffds'  : FFD.State

formal-spec/Leios/VRF.agda

@@ -17,11 +17,17 @@ record LeiosVRF : Type₁ where
   open VRF vrf public
 
   -- transforming slot numbers into VRF seeds
-  field genIBInput genEBInput genVInput : ℕ → ℕ
+  field genIBInput genEBInput genVInput genV1Input genV2Input : ℕ → ℕ
 
   canProduceIB : ℕ → PrivKey → ℕ → VrfPf → Type
   canProduceIB slot k stake π = let (val , pf) = eval k (genIBInput slot) in val < stake × pf ≡ π
 
+  Dec-canProduceIB : ∀ {slot k stake} → (∃[ π ] canProduceIB slot k stake π) ⊎ (∀ π → ¬ canProduceIB slot k stake π)
+  Dec-canProduceIB {slot} {k} {stake} with eval k (genIBInput slot)
+  ... | (val , pf) = case ¿ val < stake ¿ of λ where
+    (yes p) → inj₁ (pf , p , refl)
+    (no ¬p) → inj₂ (λ π (h , _) → ¬p h)
+
   canProduceIBPub : ℕ → ℕ → PubKey → VrfPf → ℕ → Type
   canProduceIBPub slot val k pf stake = verify k (genIBInput slot) val pf × val < stake
 
@@ -33,3 +39,9 @@ record LeiosVRF : Type₁ where
 
   canProduceV : ℕ → PrivKey → ℕ → Type
   canProduceV slot k stake = proj₁ (eval k (genVInput slot)) < stake
+
+  canProduceV1 : ℕ → PrivKey → ℕ → Type
+  canProduceV1 slot k stake = proj₁ (eval k (genV1Input slot)) < stake
+
+  canProduceV2 : ℕ → PrivKey → ℕ → Type
+  canProduceV2 slot k stake = proj₁ (eval k (genV2Input slot)) < stake

formal-spec/Leios/Voting.agda

@@ -0,0 +1,12 @@
+{-# OPTIONS --safe #-}
+
+open import Leios.Prelude
+
+module Leios.Voting where
+
+record VotingAbstract (X : Type) : Type₁ where
+  field VotingState     : Type
+        initVotingState : VotingState
+        isVoteCertified : VotingState → X → Type
+
+        ⦃ isVoteCertified⁇ ⦄ : ∀ {vs x} → isVoteCertified vs x ⁇

nix/agda.nix

@@ -70,8 +70,8 @@ let
     src = pkgs.fetchFromGitHub {
       repo = "iog-agda-prelude";
       owner = "input-output-hk";
-      rev = "ee289f9a0b2ec0a3bfc43c3f678a17c174b397e6";
-      sha256 = "sha256-noLUBl9d/vDNbAzWfnBrWoATlBrVG1DwzRV7/2uRHoE=";
+      rev = "e4f83fa59142baaad4944910217be05ebf6e2f22";
+      sha256 = "sha256-ytTOvz97lTHTiVdpmS3HUfTp/LH1Xey9bSh9zaBuacU=";
     };
     meta = { };
     libraryFile = "iog-prelude.agda-lib";