Add a VRF functionality to replace some postulates

input-output-hk · Oct 31, 2024 · efa02c0 · efa02c0
1 parent ed8f01e
commit efa02c0
Show file tree

Hide file tree

Showing 4 changed files with 46 additions and 7 deletions.
diff --git a/formal-spec/Leios/Abstract.agda b/formal-spec/Leios/Abstract.agda
@@ -5,6 +5,7 @@ open import Leios.Prelude
 record LeiosAbstract : Type₁ where
   field Tx : Type
         PoolID : Type
+        ⦃ DecEq-PoolID ⦄ : DecEq PoolID
         BodyHash VrfPf PrivKey Sig Hash : Type -- these could have been byte strings, but this is safer
         ⦃ DecEq-Hash ⦄ : DecEq Hash
         Vote : Type

diff --git a/formal-spec/Leios/BaseFunctionality.agda b/formal-spec/Leios/BaseFunctionality.agda
@@ -5,7 +5,10 @@ module Leios.BaseFunctionality (a : LeiosAbstract) (let open LeiosAbstract a) wh
 
 open import Leios.Blocks a
 
-postulate StakeDistr Cert : Type
+StakeDistr : Type
+StakeDistr = PoolID ⇀ ℕ
+
+postulate Cert : Type
 
 data Input : Type₁ where
   INIT   : (EndorserBlock × Cert → Type) → Input

diff --git a/formal-spec/Leios/SimpleSpec.agda b/formal-spec/Leios/SimpleSpec.agda
@@ -3,10 +3,12 @@
 open import Leios.Prelude
 open import Leios.Abstract
 open import Leios.FFD
+open import Leios.VRF
 import Leios.Blocks
 
 module Leios.SimpleSpec (a : LeiosAbstract) (let open LeiosAbstract a) (let open Leios.Blocks a)
-  (id : PoolID) (pKey : PrivKey) (FFD : FFDAbstract.Functionality ffdAbstract) where
+  (id : PoolID) (pKey : PrivKey) (FFD : FFDAbstract.Functionality ffdAbstract)
+  (vrf : LeiosVRF a) (let open LeiosVRF vrf) (pubKey : PubKey) where
 
 import Leios.BaseFunctionality
 
@@ -61,9 +63,7 @@ initLeiosState V SD = record
   ; slot     = initSlot V
   }
 
-postulate canProduceIB : ℕ → VrfPf → Type
-          canProduceEB : ℕ → VrfPf → Type
-          canProduceV1 : ℕ → Type
+postulate canProduceV1 : ℕ → Type
           canProduceV2 : ℕ → Type
 
 -- some predicates about EBs
@@ -90,6 +90,11 @@ private variable s     : LeiosState
 
 open LeiosState using (FFDState; MemPool)
 
+stake : LeiosState → ℕ
+stake record { SD = SD } = case lookupᵐ? SD id of λ where
+  (just s) → s
+  nothing  → 0
+
 data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutput → Type where
   Init : ∀ {V bs bs' SD} →
        ∙ {!!} -- create & register the IB/EB lottery and voting keys with key reg
@@ -117,7 +122,7 @@ data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutpu
                 b = GenFFD.ibBody (record { txs = txs })
                 h = GenFFD.ibHeader (mkIBHeader slot id π pKey txs)
           in
-          ∙ canProduceIB slot π
+          ∙ canProduceIB slot pKey (stake s)
           ∙ FFDAbstract.Send h (just b) FFD'.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes)
           ─────────────────────────────────────────────────────────────────────────
           just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY)
@@ -129,7 +134,7 @@ data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutpu
                 h = mkEB slot id π pKey LI LE
                 ffds = s .FFDState
           in
-          ∙ canProduceEB slot π
+          ∙ canProduceEB slot pKey (stake s)
           ∙ FFDAbstract.Send (GenFFD.ebHeader h) nothing FFD'.⇀⟦ ffds ⟧ (ffds' , FFDAbstract.SendRes)
           ──────────────────────────────────────────────────────────────────────────────────────────
           just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY)

diff --git a/formal-spec/Leios/VRF.agda b/formal-spec/Leios/VRF.agda
@@ -0,0 +1,30 @@
+open import Leios.Prelude
+open import Leios.Abstract
+
+module Leios.VRF (a : LeiosAbstract) (let open LeiosAbstract a) where
+
+record VRF (Dom Range PubKey : Type) : Type₁ where
+  field isKeyPair : PubKey → PrivKey → Type
+        eval : PrivKey → Dom → Range × VrfPf
+        verify : PubKey → Dom → Range → VrfPf → Type
+
+record LeiosVRF : Type₁ where
+  field PubKey : Type
+        vrf : VRF ℕ ℕ PubKey
+
+  open VRF vrf public
+
+  -- transforming slot numbers into VRF seeds
+  field genIBInput genEBInput : ℕ → ℕ
+
+  canProduceIB : ℕ → PrivKey → ℕ → Type
+  canProduceIB slot k stake = proj₁ (eval k (genIBInput slot)) < stake
+
+  canProduceIBPub : ℕ → ℕ → PubKey → VrfPf → ℕ → Type
+  canProduceIBPub slot val k pf stake = verify k (genIBInput slot) val pf × val < stake
+
+  canProduceEB : ℕ → PrivKey → ℕ → Type
+  canProduceEB slot k stake = proj₁ (eval k (genEBInput slot)) < stake
+
+  canProduceEBPub : ℕ → ℕ → PubKey → VrfPf → ℕ → Type
+  canProduceEBPub slot val k pf stake = verify k (genEBInput slot) val pf × val < stake