From 6349ed81275d8d1018e9e62369964a44cd634b07 Mon Sep 17 00:00:00 2001 From: Yves Hauser Date: Fri, 8 Nov 2024 17:12:35 +0100 Subject: [PATCH] keys --- formal-spec/Leios/KeyRegistration.agda | 2 +- formal-spec/Leios/SimpleSpec.agda | 53 +++++++++++++++----------- formal-spec/Leios/VRF.agda | 8 ++-- 3 files changed, 36 insertions(+), 27 deletions(-) diff --git a/formal-spec/Leios/KeyRegistration.agda b/formal-spec/Leios/KeyRegistration.agda index 0371575..f4debf9 100644 --- a/formal-spec/Leios/KeyRegistration.agda +++ b/formal-spec/Leios/KeyRegistration.agda @@ -8,7 +8,7 @@ module Leios.KeyRegistration (a : LeiosAbstract) (open LeiosAbstract a) record KeyRegistrationAbstract : Type₁ where data Input : Type₁ where - INIT : PubKey → Input + INIT : PubKey → PubKey → PubKey → Input data Output : Type where PUBKEYS : List PubKey → Output diff --git a/formal-spec/Leios/SimpleSpec.agda b/formal-spec/Leios/SimpleSpec.agda index 016b840..f2a6e25 100644 --- a/formal-spec/Leios/SimpleSpec.agda +++ b/formal-spec/Leios/SimpleSpec.agda @@ -9,14 +9,15 @@ import Leios.Base import Leios.Blocks import Leios.KeyRegistration -import Data.List.Relation.Unary.Any as L +import Data.List as L +import Data.List.Relation.Unary.Any as A module Leios.SimpleSpec (a : LeiosAbstract) (let open LeiosAbstract a) (let open Leios.Blocks a) ⦃ IsBlock-Vote : IsBlock (List Vote) ⦄ ⦃ Hashable-IBHeaderOSig : ∀ {b} → Hashable (IBHeaderOSig b) Hash ⦄ ⦃ Hashable-PreEndorserBlock : Hashable PreEndorserBlock Hash ⦄ - (id : PoolID) (pKey : PrivKey) (FFD' : FFDAbstract.Functionality ffdAbstract) - (vrf' : LeiosVRF a) (let open LeiosVRF vrf') (pubKey : PubKey) + (id : PoolID) (FFD' : FFDAbstract.Functionality ffdAbstract) + (vrf' : LeiosVRF a) (let open LeiosVRF vrf') (let open Leios.Base a) (B' : BaseAbstract) (BF : BaseAbstract.Functionality B') (let open Leios.KeyRegistration a vrf') (K' : KeyRegistrationAbstract) (KF : KeyRegistrationAbstract.Functionality K') where @@ -123,16 +124,17 @@ module _ (s : LeiosState) (eb : EndorserBlock) where postulate instance isVote1Certified? : ∀ {s eb} → isVote1Certified s eb ⁇ isVote2Certified? : ∀ {s eb} → isVote2Certified s eb ⁇ -private variable s : LeiosState - ffds' : FFD.State - π : VrfPf +private variable s : LeiosState + ffds' : FFD.State + sk-IB sk-EB sk-V : PrivKey + pk-IB pk-EB pk-V : PubKey + π : VrfPf stake : LeiosState → ℕ stake record { SD = SD } = case lookupᵐ? SD id of λ where (just s) → s nothing → 0 - module _ (s : LeiosState) where open LeiosState s @@ -141,21 +143,21 @@ module _ (s : LeiosState) where upd : Header ⊎ Body → LeiosState upd (inj₁ (ebHeader eb)) = record s { EBs = eb ∷ EBs } upd (inj₁ (vHeader vs)) = record s { Vs = vs ∷ Vs } - upd (inj₁ (ibHeader h)) with L.any? (matchIB? h) IBBodies + upd (inj₁ (ibHeader h)) with A.any? (matchIB? h) IBBodies ... | yes p = record s - { IBs = record { header = h ; body = L.lookup p } ∷ IBs - ; IBBodies = IBBodies L.─ p + { IBs = record { header = h ; body = A.lookup p } ∷ IBs + ; IBBodies = IBBodies A.─ p } ... | no _ = record s { IBHeaders = h ∷ IBHeaders } - upd (inj₂ (ibBody b)) with L.any? (flip matchIB? b) IBHeaders + upd (inj₂ (ibBody b)) with A.any? (flip matchIB? b) IBHeaders ... | yes p = record s - { IBs = record { header = L.lookup p ; body = b } ∷ IBs - ; IBHeaders = IBHeaders L.─ p } + { IBs = record { header = A.lookup p ; body = b } ∷ IBs + ; IBHeaders = IBHeaders A.─ p } ... | no _ = record s { IBBodies = b ∷ IBBodies @@ -166,15 +168,17 @@ _↑_ = foldr (flip upd) postulate V_chkCerts : List PubKey → EndorserBlock × B.Cert → Type + isValid : Header ⊎ Body → Type + isValid? : ∀ (b : Header ⊎ Body) → Dec (isValid b) data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutput → Type where -- Initialization - Init : ∀ {V bs bs' SD ks ks' pk pks} → - ∙ ks ⇀⟦ K.INIT pk ⟧ᴷ (ks' , K.PUBKEYS pks) -- create & register the IB/EB lottery and voting keys with key reg + Init : ∀ {V bs bs' SD ks ks' pks} → + ∙ ks ⇀⟦ K.INIT pk-IB pk-EB pk-V ⟧ᴷ (ks' , K.PUBKEYS pks) ∙ bs ⇀⟦ B.INIT (V_chkCerts pks) ⟧ᴮ (bs' , B.STAKE SD) - ─────────────────────────────────────────────────────── + ───────────────────────────────────────────────────────── nothing ⇀⟦ INIT V ⟧ (initLeiosState V SD , EMPTY) -- Network and Ledger @@ -183,8 +187,13 @@ data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutpu Slot : ∀ {bs bs' msgs ebs} → let open LeiosState s renaming (FFDState to ffds) in ∙ bs ⇀⟦ B.FTCH-LDG ⟧ᴮ (bs' , B.BASE-LDG ebs) ∙ FFDAbstract.Fetch ⇀⟦ ffds ⟧ᴺ (ffds' , FFDAbstract.FetchRes msgs) - ────────────────────────────────────────────────────────────────────────────────────────────── - just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' ; Ledger = constructLedger ebs } ↑ msgs , EMPTY) + ──────────────────────────────────────────────────────────────────────────── + just s ⇀⟦ SLOT ⟧ + (record s + { FFDState = ffds' + ; Ledger = constructLedger ebs + } ↑ L.filter isValid? msgs + , EMPTY) Ftch : let open LeiosState s in ────────────────────────────────────────── @@ -216,9 +225,9 @@ data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutpu IB-Role : let open LeiosState s renaming (ToPropose to txs; FFDState to ffds) b = GenFFD.ibBody (record { txs = txs }) - h = GenFFD.ibHeader (mkIBHeader slot id π pKey txs) + h = GenFFD.ibHeader (mkIBHeader slot id π sk-IB txs) in - ∙ canProduceIB slot pKey (stake s) -- TODO: let π be the corresponding proof + ∙ canProduceIB slot sk-IB (stake s) π ∙ FFDAbstract.Send h (just b) ⇀⟦ ffds ⟧ᴺ (ffds' , FFDAbstract.SendRes) ────────────────────────────────────────────────────────────────────── just s ⇀⟦ SLOT ⟧ (record s { FFDState = ffds' } , EMPTY) @@ -227,9 +236,9 @@ data _⇀⟦_⟧_ : Maybe LeiosState → LeiosInput → LeiosState × LeiosOutpu LI = map {F = List} getIBRef $ setToList $ filterˢ (_∈ᴮ slice L slot (Λ + 1)) (fromList IBs) LE = map getEBRef $ setToList $ filterˢ (isVote1Certified s) $ filterˢ (_∈ᴮ slice L slot (μ + 2)) (fromList EBs) - h = mkEB slot id π pKey LI LE + h = mkEB slot id π sk-EB LI LE in - ∙ canProduceEB slot pKey (stake s) + ∙ canProduceEB slot sk-EB (stake s) π ∙ FFDAbstract.Send (GenFFD.ebHeader h) nothing ⇀⟦ 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 index 109e205..6067b23 100644 --- a/formal-spec/Leios/VRF.agda +++ b/formal-spec/Leios/VRF.agda @@ -19,14 +19,14 @@ record LeiosVRF : Type₁ where -- transforming slot numbers into VRF seeds field genIBInput genEBInput : ℕ → ℕ - canProduceIB : ℕ → PrivKey → ℕ → Type - canProduceIB slot k stake = proj₁ (eval k (genIBInput slot)) < stake + canProduceIB : ℕ → PrivKey → ℕ → VrfPf → Type + canProduceIB slot k stake π = let (val , pf) = eval k (genIBInput slot) in val < stake × pf ≡ π 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 + canProduceEB : ℕ → PrivKey → ℕ → VrfPf → Type + canProduceEB slot k stake π = let (val , pf) = eval k (genEBInput slot) in val < stake × pf ≡ π canProduceEBPub : ℕ → ℕ → PubKey → VrfPf → ℕ → Type canProduceEBPub slot val k pf stake = verify k (genEBInput slot) val pf × val < stake