Formal specification: Ledger construction

formal-spec/Leios/Abstract.agda

@@ -11,7 +11,7 @@ record LeiosAbstract : Type₁ where
         BodyHash VrfPf PrivKey Sig Hash : Type -- these could have been byte strings, but this is safer
         ⦃ DecEq-Hash ⦄ : DecEq Hash
         Vote : Type
-        vote : Hash → Vote
+        vote : PrivKey → Hash → Vote
         sign : PrivKey → Hash → Sig
         ⦃ Hashable-Txs ⦄ : Hashable (List Tx) Hash
         L Λ μ : ℕ

formal-spec/Leios/Base.agda

@@ -2,8 +2,10 @@
 
 open import Leios.Prelude
 open import Leios.Abstract
+open import Leios.VRF
 
-module Leios.Base (a : LeiosAbstract) (open LeiosAbstract a) where
+module Leios.Base (a : LeiosAbstract) (open LeiosAbstract a) (vrf' : LeiosVRF a)
+  (let open LeiosVRF vrf') where
 
 open import Leios.Blocks a using (EndorserBlock)
 
@@ -12,15 +14,23 @@ StakeDistr = PoolID ⇀ ℕ
 
 record BaseAbstract : Type₁ where
   field Cert : Type
+        VTy : Type
+        initSlot : VTy → ℕ
+        V-chkCerts : List PubKey → EndorserBlock × Cert → Type
 
   data Input : Type₁ where
     INIT   : (EndorserBlock × Cert → Type) → Input
     SUBMIT : EndorserBlock ⊎ List Tx → Input -- maybe we have both
+    FTCH-LDG : Input
 
   data Output : Type where
     STAKE : StakeDistr → Output
     EMPTY : Output
+    BASE-LDG : List EndorserBlock → Output
 
   record Functionality : Type₁ where
     field State : Type
           _⇀⟦_⟧_ : State → Input → State × Output → Type
+
+    open Input public
+    open Output public

formal-spec/Leios/Blocks.agda

@@ -74,6 +74,16 @@ mkIBHeader slot id π pKey txs = record { signature = sign pKey (hash h) ; IBHea
 getIBRef : ⦃ Hashable IBHeader Hash ⦄ → InputBlock → IBRef
 getIBRef = hash ∘ InputBlock.header
 
+-- TODO
+record ibHeaderValid (h : IBHeader) : Type where
+record ibBodyValid (b : IBBody) : Type where
+
+ibHeaderValid? : (h : IBHeader) → Dec (ibHeaderValid h)
+ibHeaderValid? _ = yes record {}
+
+ibBodyValid? : (b : IBBody) → Dec (ibBodyValid b)
+ibBodyValid? _ = yes record {}
+
 --------------------------------------------------------------------------------
 -- Endorser Blocks
 --------------------------------------------------------------------------------
@@ -113,12 +123,25 @@ getEBRef : ⦃ Hashable PreEndorserBlock Hash ⦄ → EndorserBlock → EBRef
 getEBRef = hash
 
 -- TODO
--- record ebValid (eb : EndorserBlock) : Type where
+record ebValid (eb : EndorserBlock) : Type where
 --   field lotteryPfValid : {!!}
 --         signatureValid : {!!}
 --         ibRefsValid : {!!}
 --         ebRefsValid : {!!}
 
+ebValid? : (eb : EndorserBlock) → Dec (ebValid eb)
+ebValid? _ = yes record {}
+
+--------------------------------------------------------------------------------
+-- Votes
+--------------------------------------------------------------------------------
+
+-- TODO
+record vsValid (vs : List Vote) : Type where
+
+vsValid? : (vs : List Vote) → Dec (vsValid vs)
+vsValid? _ = yes record {}
+
 --------------------------------------------------------------------------------
 -- FFD for Leios Blocks
 --------------------------------------------------------------------------------
@@ -135,11 +158,42 @@ module GenFFD ⦃ _ : IsBlock (List Vote) ⦄ where
   ID : Type
   ID = ℕ × PoolID
 
-  match : Header → Body → Type
-  match (ibHeader h) (ibBody b) = bodyHash ≡ hash b
+  matchIB : IBHeader → IBBody → Type
+  matchIB h b = bodyHash ≡ hash b
+    where open IBHeaderOSig h; open IBBody b
+
+  matchIB? :  ∀ (h : IBHeader) → (b : IBBody) → Dec (matchIB h b)
+  matchIB? h b = bodyHash ≟ hash b
     where open IBHeaderOSig h; open IBBody b
+
+  match : Header → Body → Type
+  match (ibHeader h) (ibBody b) = matchIB h b
   match _ _ = ⊥
 
+  headerValid : Header → Type
+  headerValid (ibHeader h) = ibHeaderValid h
+  headerValid (ebHeader h) = ebValid h
+  headerValid (vHeader h)  = vsValid h
+
+  headerValid? : (h : Header) → Dec (headerValid h)
+  headerValid? (ibHeader h) = ibHeaderValid? h
+  headerValid? (ebHeader h) = ebValid? h
+  headerValid? (vHeader h)  = vsValid? h
+
+  bodyValid : Body → Type
+  bodyValid (ibBody b) = ibBodyValid b
+
+  bodyValid? : (b : Body) → Dec (bodyValid b)
+  bodyValid? (ibBody b) = ibBodyValid? b
+
+  isValid : Header ⊎ Body → Type
+  isValid (inj₁ h) = headerValid h
+  isValid (inj₂ b) = bodyValid b
+
+  isValid? : ∀ (x : Header ⊎ Body) → Dec (isValid x)
+  isValid? (inj₁ h) = headerValid? h
+  isValid? (inj₂ b) = bodyValid? b
+
   -- can we express uniqueness wrt pipelines as a property?
   msgID : Header → ID
   msgID (ibHeader h) = (slotNumber h , producerID h)

formal-spec/Leios/FFD.agda

@@ -20,4 +20,8 @@ record FFDAbstract : Type₁ where
 
   record Functionality : Type₁ where
     field State : Type
+          initFFDState : State
           stepRel : Input → State → State × Output → Type
+
+    open Input public
+    open Output public

formal-spec/Leios/KeyRegistration.agda

@@ -0,0 +1,23 @@
+{-# OPTIONS --safe #-}
+
+open import Leios.Prelude
+open import Leios.Abstract
+open import Leios.VRF
+
+module Leios.KeyRegistration (a : LeiosAbstract) (open LeiosAbstract a)
+  (vrf : LeiosVRF a) (let open LeiosVRF vrf) where
+
+record KeyRegistrationAbstract : Type₁ where
+
+  data Input : Type₁ where
+    INIT : PubKey → PubKey → PubKey → Input
+
+  data Output : Type where
+    PUBKEYS : List PubKey → Output
+
+  record Functionality : Type₁ where
+    field State : Type
+          _⇀⟦_⟧_ : State → Input → State × Output → Type
+
+    open Input public
+    open Output public