Conformance testing

formal-spec/Everything.agda

@@ -25,7 +25,6 @@ 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/Blocks.agda

@@ -14,6 +14,7 @@ record IsBlock (B : Type) : Type where
   field slotNumber : B → ℕ
         producerID : B → PoolID
         lotteryPf  : B → VrfPf
+        signature  : B → Sig
 
   infix 4 _∈ᴮ_
 
@@ -82,22 +83,6 @@ mkIBHeader slot id π pKey txs = record { signature = sign pKey (hash h) ; IBHea
 getIBRef : ⦃ Hashable PreIBHeader 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 {}
-
-ibValid : InputBlock → Type
-ibValid record { header = h ; body = b } = ibHeaderValid h × ibBodyValid b
-
-ibValid? : (ib : InputBlock) → Dec (ibValid ib)
-ibValid? record { header = h ; body = b } = ibHeaderValid? h ×-dec ibBodyValid? b
-
 --------------------------------------------------------------------------------
 -- Endorser Blocks
 --------------------------------------------------------------------------------
@@ -138,25 +123,11 @@ mkEB slot id π pKey LI LE = record { signature = sign pKey (hash b) ; EndorserB
 getEBRef : ⦃ Hashable PreEndorserBlock Hash ⦄ → EndorserBlock → EBRef
 getEBRef = hash
 
--- TODO
-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
@@ -189,30 +160,6 @@ module GenFFD ⦃ _ : IsBlock (List Vote) ⦄ where
   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/Foreign/Types.agda

@@ -19,7 +19,10 @@ module Leios.Foreign.Types where
   {-# LANGUAGE DuplicateRecordFields #-}
 #-}
 
-open import Leios.Defaults 2 fzero -- TODO: parameters
+numberOfParties : ℕ
+numberOfParties = 2
+
+open import Leios.Defaults numberOfParties fzero
   renaming (EndorserBlock to EndorserBlockAgda; IBHeader to IBHeaderAgda)
 
 dropDash : S.String → S.String
@@ -52,8 +55,8 @@ instance
     { 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 <? 2 of λ where
-          (yes q) → record { slotNumber = s ; producerID = #_ p {2} {fromWitness q} ; lotteryPf = tt ; bodyHash = h ; signature = tt }
+        case p <? numberOfParties of λ where
+          (yes q) → record { slotNumber = s ; producerID = #_ p {numberOfParties} {fromWitness q} ; lotteryPf = tt ; bodyHash = h ; signature = tt }
           (no _) → error "Conversion to Fin not possible!"
     }
 
@@ -87,8 +90,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 <? 2 of λ where
-          (yes q) → record { slotNumber = s ; producerID = #_ p {2} {fromWitness q} ; lotteryPf = tt ; signature = tt ; ibRefs = refs ; ebRefs = [] }
+        case p <? numberOfParties of λ where
+          (yes q) → record { slotNumber = s ; producerID = #_ p {numberOfParties} {fromWitness q} ; lotteryPf = tt ; signature = tt ; ibRefs = refs ; ebRefs = [] }
           (no _) → error "Conversion to Fin not possible!"
       }
 
@@ -143,9 +146,16 @@ 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
+
+open import Leios.Short.Deterministic st public
 
 stepHs : HsType (LeiosState → LeiosInput → C.ComputationResult String (LeiosOutput × LeiosState))
 stepHs = to (compute Computational--⟦/⟧⇀)

formal-spec/Leios/Protocol.agda

@@ -45,6 +45,7 @@ record LeiosState : Type where
         Upkeep      : ℙ SlotUpkeep
         BaseState   : B.State
         votingState : VotingState
+        PubKeys     : List PubKey
 
   lookupEB : EBRef → Maybe EndorserBlock
   lookupEB r = find (λ b → getEBRef b ≟ r) EBs
@@ -74,8 +75,8 @@ 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
+initLeiosState : VTy → StakeDistr → B.State → List PubKey → LeiosState
+initLeiosState V SD bs pks = record
   { V           = V
   ; SD          = SD
   ; FFDState    = FFD.initFFDState
@@ -90,8 +91,114 @@ initLeiosState V SD bs = record
   ; Upkeep      = ∅
   ; BaseState   = bs
   ; votingState = initVotingState
+  ; PubKeys     = pks
   }
 
+stake' : PoolID → LeiosState → ℕ
+stake' pid record { SD = SD } = TotalMap.lookup SD pid
+
+stake'' : PubKey → LeiosState → ℕ
+stake'' pk = stake' (poolID pk)
+
+stake : LeiosState → ℕ
+stake = stake' id
+
+lookupPubKeyAndStake : ∀ {B} → ⦃ _ : IsBlock B ⦄ → LeiosState → B → Maybe (PubKey × ℕ)
+lookupPubKeyAndStake s b =
+  L.head $
+    L.map (λ pk → (pk , stake'' pk s)) $
+      L.filter ((producerID b ≟_) ∘ poolID) (LeiosState.PubKeys s)
+
+module _ (s : LeiosState)  where
+
+  record ibHeaderValid (h : IBHeader) (pk : PubKey) (st : ℕ) : Type where
+    field lotteryPfValid : verify pk (slotNumber h) st (lotteryPf h)
+          signatureValid : verifySig pk (signature h)
+
+  record ibBodyValid (b : IBBody) : Type where
+
+  ibHeaderValid? : (h : IBHeader) (pk : PubKey) (st : ℕ) → Dec (ibHeaderValid h pk st)
+  ibHeaderValid? h pk st
+    with verify? pk (slotNumber h) st (lotteryPf h)
+  ... | no ¬p = no (¬p ∘ ibHeaderValid.lotteryPfValid)
+  ... | yes p
+    with verifySig? pk (signature h)
+  ... | yes q = yes (record { lotteryPfValid = p ; signatureValid = q })
+  ... | no ¬q = no (¬q ∘ ibHeaderValid.signatureValid)
+
+  ibBodyValid? : (b : IBBody) → Dec (ibBodyValid b)
+  ibBodyValid? _ = yes record {}
+
+  ibValid : InputBlock → Type
+  ibValid record { header = h ; body = b }
+    with lookupPubKeyAndStake s h
+  ... | just (pk , pid) = ibHeaderValid h pk (stake'' pk s) × ibBodyValid b
+  ... | nothing = ⊥
+
+  ibValid? : (ib : InputBlock) → Dec (ibValid ib)
+  ibValid? record { header = h ; body = b }
+    with lookupPubKeyAndStake s h
+  ... | just (pk , pid) = ibHeaderValid? h pk (stake'' pk s) ×-dec ibBodyValid? b
+  ... | nothing = no λ x → x
+
+  record ebValid (eb : EndorserBlock) (pk : PubKey) (st : ℕ) : Type where
+    field lotteryPfValid : verify pk (slotNumber eb) st (lotteryPf eb)
+          signatureValid : verifySig pk (signature eb)
+    -- TODO
+    -- ibRefsValid : ?
+    -- ebRefsValid : ?
+
+  ebValid? : (eb : EndorserBlock) (pk : PubKey) (st : ℕ) → Dec (ebValid eb pk st)
+  ebValid? h pk st
+    with verify? pk (slotNumber h) st (lotteryPf h)
+  ... | no ¬p = no (¬p ∘ ebValid.lotteryPfValid)
+  ... | yes p
+    with verifySig? pk (signature h)
+  ... | yes q = yes (record { lotteryPfValid = p ; signatureValid = q })
+  ... | no ¬q = no (¬q ∘ ebValid.signatureValid)
+
+  -- TODO
+  record vsValid (vs : List Vote) : Type where
+
+  vsValid? : (vs : List Vote) → Dec (vsValid vs)
+  vsValid? _ = yes record {}
+
+  headerValid : Header → Type
+  headerValid (ibHeader h)
+    with lookupPubKeyAndStake s h
+  ... | just (pk , pid) = ibHeaderValid h pk (stake'' pk s)
+  ... | nothing = ⊥
+  headerValid (ebHeader h)
+    with lookupPubKeyAndStake s h
+  ... | just (pk , pid) = ebValid h pk (stake'' pk s)
+  ... | nothing = ⊥
+  headerValid (vHeader h)  = vsValid h
+
+  headerValid? : (h : Header) → Dec (headerValid h)
+  headerValid? (ibHeader h)
+    with lookupPubKeyAndStake s h
+  ... | just (pk , pid) = ibHeaderValid? h pk (stake'' pk s)
+  ... | nothing = no λ x → x
+  headerValid? (ebHeader h)
+    with lookupPubKeyAndStake s h
+  ... | just (pk , pid) = ebValid? h pk (stake'' pk s)
+  ... | nothing = no λ x → x
+  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
+
 -- some predicates about EBs
 module _ (s : LeiosState) (eb : EndorserBlock) where
   open EndorserBlockOSig eb
@@ -100,9 +207,6 @@ module _ (s : LeiosState) (eb : EndorserBlock) where
   allIBRefsKnown : Type
   allIBRefsKnown = ∀[ ref ∈ fromList ibRefs ] ref ∈ˡ map getIBRef IBs
 
-stake : LeiosState → ℕ
-stake record { SD = SD } = TotalMap.lookup SD id
-
 module _ (s : LeiosState) where
 
   open LeiosState s

formal-spec/Leios/Short.lagda.md

@@ -126,7 +126,7 @@ data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → Leios
        ∙ 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'
+       nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' pks
 ```
 #### Network and Ledger
 ```agda
@@ -141,7 +141,7 @@ data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → Leios
            ; Ledger    = constructLedger rbs
            ; slot      = suc slot
            ; Upkeep    = ∅
-           } ↑ L.filter isValid? msgs
+           } ↑ L.filter (isValid? s) msgs
 ```
 ```agda
   Ftch :

formal-spec/Leios/Short/Deterministic.agda

@@ -56,7 +56,7 @@ data _⊢_ : LeiosInput → LeiosState → Type where
        ∙ 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'
        ────────────────────────────────────────────────────────────────
-       INIT V ⊢ initLeiosState V SD bs'
+       INIT V ⊢ initLeiosState V SD bs' pks
 
 data _-⟦Base⟧⇀_ : LeiosState → LeiosState → Type where
 
@@ -242,7 +242,7 @@ data _-⟦_/_⟧⇀_ : LeiosState → LeiosInput → LeiosOutput → LeiosState
                     ; slot     = suc slot
                     ; Upkeep   = ∅
                     ; BaseState = bs'
-                    } ↑ L.filter isValid? msgs
+                    } ↑ L.filter (isValid? s) msgs
        in
        ∙ Upkeep ≡ᵉ allUpkeep
        ∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs'
@@ -284,7 +284,7 @@ _-⟦_/_⟧ⁿᵈ*⇀_ = ReflexiveTransitiveClosure _-⟦_/_⟧ⁿᵈ⇀_
   let
     s0 = _
     upkeep≡∅ : LeiosState.Upkeep s0 ≡ ∅
-    upkeep≡∅ = sym (↑-preserves-Upkeep {x = L.filter isValid? msgs})
+    upkeep≡∅ = sym (↑-preserves-Upkeep {x = L.filter (isValid? s) msgs})
     needsAllUpkeep : ∀ {u} → LeiosState.needsUpkeep s0 u
     needsAllUpkeep {u} = subst (u ∉_) (sym upkeep≡∅) Properties.∉-∅
     needsUpkeep1 : ∀ {u} → u ≢ Base → LeiosState.needsUpkeep s1 u

formal-spec/Leios/Simplified.agda

@@ -132,7 +132,7 @@ data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → Leios
        ∙ 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'
+       nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' pks
 
   -- Network and Ledger
 
@@ -147,7 +147,7 @@ data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → Leios
            ; slot      = suc slot
            ; Upkeep    = ∅
            ; BaseState = bs'
-           } ↑ L.filter isValid? msgs
+           } ↑ L.filter (isValid? s) msgs
 
   Ftch :
        ────────────────────────────────────────────────────────

formal-spec/Leios/Simplified/Deterministic.agda

@@ -56,7 +56,7 @@ data _⊢_ : LeiosInput → LeiosState → Type where
        ∙ 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'
        ────────────────────────────────────────────────────────────────
-       INIT V ⊢ initLeiosState V SD bs'
+       INIT V ⊢ initLeiosState V SD bs' pks
 
 data _-⟦Base⟧⇀_ : LeiosState → LeiosState → Type where
 
@@ -274,7 +274,7 @@ data _-⟦_/_⟧⇀_ : LeiosState → LeiosInput → LeiosOutput → LeiosState
                     ; slot     = suc slot
                     ; Upkeep   = ∅
                     ; BaseState = bs'
-                    } ↑ L.filter isValid? msgs
+                    } ↑ L.filter (isValid? s) msgs
        in
        ∙ Upkeep ≡ᵉ allUpkeep
        ∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs'
@@ -317,7 +317,7 @@ _-⟦_/_⟧ⁿᵈ*⇀_ = ReflexiveTransitiveClosure _-⟦_/_⟧ⁿᵈ⇀_
   let
     s0 = _
     upkeep≡∅ : LeiosState.Upkeep s0 ≡ ∅
-    upkeep≡∅ = sym (↑-preserves-Upkeep {x = L.filter isValid? msgs})
+    upkeep≡∅ = sym (↑-preserves-Upkeep {x = L.filter (isValid? s) msgs})
     needsAllUpkeep : ∀ {u} → LeiosState.needsUpkeep s0 u
     needsAllUpkeep {u} = subst (u ∉_) (sym upkeep≡∅) Properties.∉-∅
     needsUpkeep1 : ∀ {u} → u ≢ Base → LeiosState.needsUpkeep s1 u