IsValid predicates

formal-spec/Leios/Blocks.agda

@@ -12,6 +12,7 @@ record IsBlock (B : Type) : Type where
   field slotNumber : B → ℕ
         producerID : B → PoolID
         lotteryPf  : B → VrfPf
+        signature  : B → Sig
 
   infix 4 _∈ᴮ_
 
@@ -51,7 +52,7 @@ record InputBlock : Type where
   open IBHeaderOSig header public
 
 instance
-  IsBlock-IBHeaderOSig : ∀ {b} → IsBlock (IBHeaderOSig b)
+  IsBlock-IBHeaderOSig : IsBlock IBHeader
   IsBlock-IBHeaderOSig = record { IBHeaderOSig }
 
   Hashable-IBBody : Hashable IBBody Hash
@@ -74,22 +75,6 @@ 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 {}
-
-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
 --------------------------------------------------------------------------------
@@ -110,8 +95,8 @@ instance
   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-EndorserBlockOSig : IsBlock EndorserBlock
+  IsBlock-EndorserBlockOSig = record { 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 }
@@ -128,25 +113,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
@@ -176,30 +147,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/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
@@ -71,8 +72,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
@@ -87,8 +88,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
@@ -97,9 +204,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

@@ -85,7 +85,6 @@ module Protocol where
                   EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs
                   votes = map (vote sk-V ∘ hash) EBs'
             in
-            ∙ needsUpkeep V-Role
             ∙ canProduceV slot sk-V (stake s)
             ∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
             ─────────────────────────────────────────────────────────────────────────
@@ -123,7 +122,7 @@ module Protocol 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'
          ────────────────────────────────────────────────────────────────
-         nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs'
+         nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' pks
 ```
 #### Network and Ledger
 ```agda
@@ -138,7 +137,7 @@ module Protocol where
              ; Ledger    = constructLedger rbs
              ; slot      = suc slot
              ; Upkeep    = ∅
-             } ↑ L.filter isValid? msgs
+             } ↑ L.filter (isValid? s) msgs
 ```
 ```agda
     Ftch :

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/VRF.agda

@@ -9,9 +9,14 @@ record VRF (Dom Range PubKey : Type) : Type₁ where
   field isKeyPair : PubKey → PrivKey → Type
         eval : PrivKey → Dom → Range × VrfPf
         verify : PubKey → Dom → Range → VrfPf → Type
+        verify? : (pk : PubKey) → (d : Dom) → (r : Range) → (pf : VrfPf) → Dec (verify pk d r pf)
 
 record LeiosVRF : Type₁ where
   field PubKey : Type
+        poolID : PubKey → PoolID
+        verifySig : PubKey → Sig → Type
+        verifySig? : (pk : PubKey) → (sig : Sig) → Dec (verifySig pk sig)
+
         vrf : VRF ℕ ℕ PubKey
 
   open VRF vrf public