Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add a SlotUpkeep type to enforce dependencies between rules #75

Merged
merged 5 commits into from
Nov 19, 2024
Merged

Add a SlotUpkeep type to enforce dependencies between rules #75

Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
f1b89e0
Add `SlotUpkeep` to enforce dependencies between rules
WhatisRT Nov 18, 2024
80c112c
Simplify upkeep notation
WhatisRT Nov 18, 2024
464c5a8
Add negated rules so we don't get stuck when we can't produce a block
WhatisRT Nov 18, 2024
c962418
Keep track of the state of the base chain
WhatisRT Nov 18, 2024
2fd90dd
Fix `needsUpkeep`
WhatisRT Nov 19, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
113 changes: 82 additions & 31 deletions formal-spec/Leios/SimpleSpec.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ module Leios.SimpleSpec (a : LeiosAbstract) (let open LeiosAbstract a) (let open
(sk-IB sk-EB sk-V : PrivKey)
(pk-IB pk-EB pk-V : PubKey)
(let open Leios.Base a vrf') (B' : BaseAbstract) (BF : BaseAbstract.Functionality B')
(initBaseState : BaseAbstract.Functionality.State BF)
(let open Leios.KeyRegistration a vrf') (K' : KeyRegistrationAbstract) (KF : KeyRegistrationAbstract.Functionality K') where

module B = BaseAbstract.Functionality BF
Expand Down Expand Up @@ -59,6 +60,12 @@ data LeiosOutput : Type where
FTCH-LDG : List Tx → LeiosOutput
EMPTY : LeiosOutput

data SlotUpkeep : Type where
Base IB-Role EB-Role V1-Role V2-Role : SlotUpkeep

allUpkeep : ℙ SlotUpkeep
allUpkeep = fromList (Base ∷ IB-Role ∷ EB-Role ∷ V1-Role ∷ V2-Role ∷ [])

record LeiosState : Type where
field V : VTy
SD : StakeDistr
Expand All @@ -71,6 +78,8 @@ record LeiosState : Type where
slot : ℕ
IBHeaders : List IBHeader
IBBodies : List IBBody
Upkeep : ℙ SlotUpkeep
BaseState : B.State

lookupEB : EBRef → Maybe EndorserBlock
lookupEB r = find (λ b → getEBRef b ≟ r) EBs
Expand All @@ -90,8 +99,14 @@ record LeiosState : Type where
constructLedger : List EndorserBlock → List Tx
constructLedger = concatMap lookupTxs

initLeiosState : VTy → StakeDistr → LeiosState
initLeiosState V SD = record
needsUpkeep : SlotUpkeep → Set
needsUpkeep = _∉ Upkeep

addUpkeep : LeiosState → SlotUpkeep → LeiosState
addUpkeep s u = let open LeiosState s in record s { Upkeep = Upkeep ∪ ❴ u ❵ }

initLeiosState : VTy → StakeDistr → B.State → LeiosState
initLeiosState V SD bs = record
{ V = V
; SD = SD
; FFDState = FFD.initFFDState
Expand All @@ -103,6 +118,8 @@ initLeiosState V SD = record
; slot = initSlot V
; IBHeaders = []
; IBBodies = []
; Upkeep = ∅
; BaseState = bs
}

-- some predicates about EBs
Expand Down Expand Up @@ -161,7 +178,7 @@ open FFD hiding (_-⟦_/_⟧⇀_)
private variable s : LeiosState
ffds' : FFD.State
π : VrfPf
bs bs' : B.State
bs' : B.State
ks ks' : K.State
msgs : List (FFDAbstract.Header ffdAbstract ⊎ FFDAbstract.Body ffdAbstract)
eb : EndorserBlock
Expand All @@ -181,20 +198,22 @@ module _ (open Leios.Voting a) (va : VotingAbstract LeiosState) (open VotingAbst

Init :
∙ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks'
∙ bs B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs'
────────────────────────────────────────────────────────
nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD
∙ initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs'
────────────────────────────────────────────────────────────────
nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs'

-- Network and Ledger

Slot : let open LeiosState s renaming (FFDState to ffds) in
Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) in
∙ Upkeep ≡ᵉ allUpkeep
∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG ebs ⟧⇀ bs'
∙ ffds FFD.-⟦ Fetch / FetchRes msgs ⟧⇀ ffds'
──────────────────────────────────────────────────────
───────────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ record s
{ FFDState = ffds'
; Ledger = constructLedger ebs
; slot = suc slot
; Upkeep = ∅
} ↑ L.filter isValid? msgs

Ftch :
Expand All @@ -207,58 +226,90 @@ module _ (open Leios.Voting a) (va : VotingAbstract LeiosState) (open VotingAbst
-- if the party submitting is the block producer on the base chain
-- for the given slot

Base₁ :
────────────────────────────────────────────────────────────────────
just s -⟦ SUBMIT (inj₂ txs) / EMPTY ⟧⇀ record s { ToPropose = txs }

Base₂a : let open LeiosState s in
∙ eb ∈ filter (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs
∙ bs B.-⟦ B.SUBMIT (inj₁ eb) / B.EMPTY ⟧⇀ bs'
───────────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ s

Base₂b : let open LeiosState s in
∙ [] ≡ filter (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs
∙ bs B.-⟦ B.SUBMIT (inj₂ ToPropose) / B.EMPTY ⟧⇀ bs'
───────────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ s
Base₁ :
───────────────────────────────────────────────────────────────────
just s -⟦ SUBMIT (inj₂ txs) / EMPTY ⟧⇀ record s { ToPropose = txs }

Base₂a : let open LeiosState s renaming (BaseState to bs) in
∙ needsUpkeep Base
∙ eb ∈ filter (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs
∙ bs B.-⟦ B.SUBMIT (inj₁ eb) / B.EMPTY ⟧⇀ bs'
───────────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base

Base₂b : let open LeiosState s renaming (BaseState to bs) in
∙ needsUpkeep Base
∙ [] ≡ filter (λ eb → isVote2Certified s eb × eb ∈ᴮ slice L slot 2) EBs
∙ bs B.-⟦ B.SUBMIT (inj₂ ToPropose) / B.EMPTY ⟧⇀ bs'
───────────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s Base

-- Protocol rules

IB-Role : let open LeiosState s renaming (FFDState to ffds)
b = ibBody (record { txs = ToPropose })
h = ibHeader (mkIBHeader slot id π sk-IB ToPropose)
in
∙ needsUpkeep IB-Role
∙ canProduceIB slot sk-IB (stake s) π
∙ ffds FFD.-⟦ Send h (just b) / SendRes ⟧⇀ ffds'
─────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ record s { FFDState = ffds' }
─────────────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { FFDState = ffds' } IB-Role

EB-Role : let open LeiosState s renaming (FFDState to ffds)
LI = map getIBRef $ filter (_∈ᴮ slice L slot (Λ + 1)) IBs
LE = map getEBRef $ filter (isVote1Certified s) $
filter (_∈ᴮ slice L slot (μ + 2)) EBs
h = mkEB slot id π sk-EB LI LE
in
∙ needsUpkeep EB-Role
∙ canProduceEB slot sk-EB (stake s) π
∙ ffds FFD.-⟦ Send (ebHeader h) nothing / SendRes ⟧⇀ ffds'
───────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ record s { FFDState = ffds' }
─────────────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { FFDState = ffds' } EB-Role

V1-Role : let open LeiosState s renaming (FFDState to ffds)
EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot (μ + 1)) EBs
votes = map (vote sk-V ∘ hash) EBs'
in
∙ needsUpkeep V1-Role
∙ canProduceV1 slot sk-V (stake s)
∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
──────────────────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ record s { FFDState = ffds' }
─────────────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { FFDState = ffds' } V1-Role

V2-Role : let open LeiosState s renaming (FFDState to ffds)
EBs' = filter (vote2Eligible s) $ filter (_∈ᴮ slice L slot 1) EBs
votes = map (vote sk-V ∘ hash) EBs'
in
∙ needsUpkeep V2-Role
∙ canProduceV2 slot sk-V (stake s)
∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
──────────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ record s { FFDState = ffds' }
─────────────────────────────────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { FFDState = ffds' } V2-Role

-- Note: Base doesn't need a negative rule, since it can always be invoked

No-IB-Role : let open LeiosState s in
∙ needsUpkeep IB-Role
∙ ¬ canProduceIB slot sk-IB (stake s) π
─────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s IB-Role

No-EB-Role : let open LeiosState s in
∙ needsUpkeep EB-Role
∙ ¬ canProduceEB slot sk-EB (stake s) π
─────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s EB-Role

No-V1-Role : let open LeiosState s in
∙ needsUpkeep V1-Role
∙ ¬ canProduceV1 slot sk-V (stake s)
─────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s V1-Role

No-V2-Role : let open LeiosState s in
∙ needsUpkeep V2-Role
∙ ¬ canProduceV2 slot sk-V (stake s)
─────────────────────────────────────────────
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep s V2-Role
Loading