Skip to content

Commit 871c01f

Browse files
WhatisRTWhatisRT
authoredFeb 14, 2025·
Add reference implementation (#111)
* Move module parameters into a bundled record * WIP: add reference implementation * Post-rebase fixing * Delete files unnecessary here * Revert "Delete files unnecessary here" This reverts commit 9ea66a45f0e141b5567669668a697ad58728c39e. * Add necessary functions to execute the Computational instance * Add missing file * Make some progress on the correctness proofs * Prove `Base-total'` * Fix performance problems, finish `computeProof` * Add tests from the demo * Add top-level import * Rename: Simple -> Simplified
1 parent 0994fdd commit 871c01f

File tree

9 files changed

+737
-0
lines changed

9 files changed

+737
-0
lines changed
 

‎formal-spec/Class/Computational22.agda

+11
Original file line numberDiff line numberDiff line change
@@ -33,3 +33,14 @@ module _ (STS : S → I → O → S → Type) where
3333
comp22⇒comp : Computational STS' Err
3434
comp22⇒comp .Computational.computeProof (s , i) = computeProof s i
3535
comp22⇒comp .Computational.completeness (s , i) (o , s') = completeness s i o s'
36+
37+
module _ {STS : S → I → O → S → Type} ⦃ _ : Computational22 STS Err ⦄ where
38+
open Computational22 it
39+
40+
-- basically `traverse`
41+
computeTrace : S → List I → ComputationResult Err (List O × S)
42+
computeTrace s [] = success ([] , s)
43+
computeTrace s (x ∷ is) = do
44+
(o , s') ← compute s x
45+
(os , s'') ← computeTrace s' is
46+
return (o ∷ os , s'')

‎formal-spec/Everything.agda

+1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
module Everything where
22

33
open import Leios.Simplified
4+
open import Leios.Simplified.Deterministic
45
open import Leios.Short
56
open import Leios.Network

‎formal-spec/Leios/Protocol.agda

+19
Original file line numberDiff line numberDiff line change
@@ -128,6 +128,25 @@ module _ (s : LeiosState) where
128128
{ IBBodies = b ∷ IBBodies
129129
}
130130

131+
module _ {s s'} where
132+
open LeiosState s'
133+
134+
upd-preserves-Upkeep : ∀ {x} → LeiosState.Upkeep s ≡ LeiosState.Upkeep s'
135+
→ LeiosState.Upkeep s ≡ LeiosState.Upkeep (upd s' x)
136+
upd-preserves-Upkeep {inj₁ (ibHeader x)} refl with A.any? (matchIB? x) IBBodies
137+
... | yes p = refl
138+
... | no ¬p = refl
139+
upd-preserves-Upkeep {inj₁ (ebHeader x)} refl = refl
140+
upd-preserves-Upkeep {inj₁ (vHeader x)} refl = refl
141+
upd-preserves-Upkeep {inj₂ (ibBody x)} refl with A.any? (flip matchIB? x) IBHeaders
142+
... | yes p = refl
143+
... | no ¬p = refl
144+
131145
infix 25 _↑_
132146
_↑_ : LeiosState → List (Header ⊎ Body) → LeiosState
133147
_↑_ = foldr (flip upd)
148+
149+
↑-preserves-Upkeep : ∀ {s x} → LeiosState.Upkeep s ≡ LeiosState.Upkeep (s ↑ x)
150+
↑-preserves-Upkeep {x = []} = refl
151+
↑-preserves-Upkeep {s = s} {x = x ∷ x₁} =
152+
upd-preserves-Upkeep {s = s} {x = x} (↑-preserves-Upkeep {x = x₁})

‎formal-spec/Leios/Simplified/Deterministic.agda

+357
Large diffs are not rendered by default.

‎formal-spec/Leios/Simplified/Deterministic/Test.agda

+94
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
--------------------------------------------------------------------------------
2+
-- Deterministic variant of simple Leios
3+
--------------------------------------------------------------------------------
4+
5+
open import Leios.Prelude hiding (id)
6+
open import Prelude.Init using (∃₂-syntax)
7+
open import Leios.FFD
8+
9+
import Data.List as L
10+
open import Data.List.Relation.Unary.Any using (here)
11+
12+
open import Leios.SpecStructure
13+
open import Leios.Trace using (st-2)
14+
15+
module Leios.Simplified.Deterministic.Test (Λ μ : ℕ) where
16+
17+
open SpecStructure st-2
18+
19+
import Leios.Simplified
20+
open import Leios.Simplified st-2 Λ μ hiding (_-⟦_/_⟧⇀_) renaming (initLeiosState to initLeiosState')
21+
module ND = Leios.Simplified st-2 Λ μ
22+
23+
open import Class.Computational
24+
open import Class.Computational22
25+
open import StateMachine
26+
27+
open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot)
28+
open GenFFD
29+
30+
open FFD hiding (_-⟦_/_⟧⇀_)
31+
32+
private variable s s' s0 s1 s2 s3 s4 s5 : LeiosState
33+
i : LeiosInput
34+
o : LeiosOutput
35+
ffds' : FFD.State
36+
π : VrfPf
37+
bs' : B.State
38+
ks ks' : K.State
39+
msgs : List (FFDAbstract.Header ffdAbstract ⊎ FFDAbstract.Body ffdAbstract)
40+
eb : EndorserBlock
41+
rbs : List RankingBlock
42+
txs : List Tx
43+
V : VTy
44+
SD : StakeDistr
45+
pks : List PubKey
46+
47+
open Computational22 ⦃...⦄
48+
open import Leios.Simplified.Deterministic st-2 Λ μ
49+
50+
instance
51+
Computational-B : Computational22 B._-⟦_/_⟧⇀_ String
52+
Computational-B .computeProof s (BaseAbstract.Input.INIT x) =
53+
success ((BaseAbstract.Output.STAKE {!!} , tt) , tt)
54+
Computational-B .computeProof s (BaseAbstract.Input.SUBMIT x) =
55+
success ((BaseAbstract.Output.EMPTY , tt) , tt)
56+
Computational-B .computeProof s BaseAbstract.Input.FTCH-LDG =
57+
success ((BaseAbstract.Output.BASE-LDG [] , tt) , tt)
58+
Computational-B .completeness = {!!}
59+
60+
Computational-FFD : Computational22 FFD._-⟦_/_⟧⇀_ String
61+
Computational-FFD .computeProof s (FFDAbstract.Send x x₁) = success ((FFDAbstract.SendRes , tt) , tt)
62+
Computational-FFD .computeProof s FFDAbstract.Fetch = success ((FFDAbstract.FetchRes [] , tt) , tt)
63+
Computational-FFD .completeness = {!!}
64+
65+
comp = Computational--⟦/⟧⇀ ⦃ Computational-B ⦄ ⦃ Computational-FFD ⦄
66+
67+
initLeiosState : VTy → StakeDistr → B.State → LeiosState
68+
initLeiosState v sd bs = record (initLeiosState' v sd bs) { Upkeep = allUpkeep }
69+
70+
module _ v sd bs where opaque
71+
unfolding List-Modelᵈ V2-Role-total
72+
73+
computeProofTy : (s : LeiosState) (i : LeiosInput)
74+
→ ComputationResult String (Σ[ (o , s') ∈ LeiosOutput × LeiosState ] s -⟦ i / o ⟧⇀ s')
75+
computeProofTy = computeProof ⦃ comp ⦄
76+
77+
compute-≡ : (s : LeiosState) (i : LeiosInput)
78+
→ compute ⦃ comp ⦄ s i ≡ map ⦃ Functor-ComputationResult ⦄ proj₁ (computeProof ⦃ comp ⦄ s i)
79+
compute-≡ s i = refl
80+
81+
test₁ : ∀ tx
82+
→ Σ[ x ∈ LeiosOutput × LeiosState ] compute (initLeiosState v sd bs) (SUBMIT (inj₂ [ tx ]))
83+
≡ success x
84+
test₁ tx = -, refl
85+
86+
test₂ : Σ[ x ∈ LeiosOutput × LeiosState ] compute (initLeiosState v sd bs) SLOT
87+
≡ success x
88+
test₂ = -, refl
89+
90+
test₃ : Tx → Set
91+
test₃ tx = {!proj₁ test₂!}
92+
93+
trace : ComputationResult String (List LeiosOutput × LeiosState)
94+
trace = computeTrace (initLeiosState v sd bs) (SLOT ∷ SLOT ∷ [])

‎formal-spec/Leios/Trace.agda

+28
Original file line numberDiff line numberDiff line change
@@ -123,6 +123,14 @@ d-VotingAbstract =
123123
; isVoteCertified = λ _ _ → ⊤
124124
}
125125

126+
d-VotingAbstract-2 : VotingAbstract (Fin 2 × EndorserBlock)
127+
d-VotingAbstract-2 =
128+
record
129+
{ VotingState = ⊤
130+
; initVotingState = tt
131+
; isVoteCertified = λ _ _ → ⊤
132+
}
133+
126134
st : SpecStructure 1
127135
st = record
128136
{ a = d-Abstract
@@ -143,6 +151,26 @@ st = record
143151
; va = d-VotingAbstract
144152
}
145153

154+
st-2 : SpecStructure 2
155+
st-2 = record
156+
{ a = d-Abstract
157+
; id = zero
158+
; FFD' = d-FFDFunctionality
159+
; vrf' = d-VRF
160+
; sk-IB = tt
161+
; sk-EB = tt
162+
; sk-V = tt
163+
; pk-IB = tt
164+
; pk-EB = tt
165+
; pk-V = tt
166+
; B' = d-Base
167+
; BF = d-BaseFunctionality
168+
; initBaseState = tt
169+
; K' = d-KeyRegistration
170+
; KF = d-KeyRegistrationFunctionality
171+
; va = d-VotingAbstract-2
172+
}
173+
146174
open import Leios.Short st public
147175

148176
sd : TotalMap (Fin 1) ℕ

‎formal-spec/Leios/UniformShort.agda

+157
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,157 @@
1+
{-# OPTIONS --safe #-}
2+
3+
open import Leios.Prelude hiding (id)
4+
open import Leios.FFD
5+
open import Leios.SpecStructure
6+
open import Data.Fin.Patterns
7+
8+
module Leios.UniformShort (⋯ : SpecStructure 1)
9+
(let open SpecStructure ⋯ renaming (isVoteCertified to isVoteCertified')) where
10+
11+
data SlotUpkeep : Type where
12+
Base IB-Role EB-Role V-Role : SlotUpkeep
13+
14+
allUpkeep : ℙ SlotUpkeep
15+
allUpkeep = fromList (Base ∷ IB-Role ∷ EB-Role ∷ V-Role ∷ [])
16+
17+
open import Leios.Protocol (⋯) SlotUpkeep public
18+
19+
open BaseAbstract B' using (Cert; V-chkCerts; VTy; initSlot)
20+
open FFD hiding (_-⟦_/_⟧⇀_)
21+
open GenFFD
22+
23+
isVoteCertified : LeiosState → EndorserBlock → Type
24+
isVoteCertified s eb = isVoteCertified' (LeiosState.votingState s) (0F , eb)
25+
26+
module Protocol where
27+
28+
private variable s s' : LeiosState
29+
ffds' : FFD.State
30+
π : VrfPf
31+
bs' : B.State
32+
ks ks' : K.State
33+
msgs : List (FFDAbstract.Header ffdAbstract ⊎ FFDAbstract.Body ffdAbstract)
34+
eb : EndorserBlock
35+
rbs : List RankingBlock
36+
txs : List Tx
37+
V : VTy
38+
SD : StakeDistr
39+
pks : List PubKey
40+
41+
-- Uniform Short Pipeline:
42+
--
43+
-- 1. If elected, propose IB
44+
-- 2. Wait
45+
-- 3. Wait
46+
-- 4. If elected, propose EB
47+
-- 5. If elected, vote
48+
-- If elected, propose RB
49+
50+
data _↝_ : LeiosState → LeiosState → Type where
51+
52+
IB-Role : let open LeiosState s renaming (FFDState to ffds)
53+
b = ibBody (record { txs = ToPropose })
54+
h = ibHeader (mkIBHeader slot id π sk-IB ToPropose)
55+
in
56+
∙ needsUpkeep IB-Role
57+
∙ canProduceIB slot sk-IB (stake s) π
58+
∙ ffds FFD.-⟦ Send h (just b) / SendRes ⟧⇀ ffds'
59+
─────────────────────────────────────────────────────────────────────────
60+
s ↝ addUpkeep record s { FFDState = ffds' } IB-Role
61+
62+
EB-Role : let open LeiosState s renaming (FFDState to ffds)
63+
LI = map getIBRef $ filter (_∈ᴮ slice L slot 3) IBs
64+
h = mkEB slot id π sk-EB LI []
65+
in
66+
∙ needsUpkeep EB-Role
67+
∙ canProduceEB slot sk-EB (stake s) π
68+
∙ ffds FFD.-⟦ Send (ebHeader h) nothing / SendRes ⟧⇀ ffds'
69+
─────────────────────────────────────────────────────────────────────────
70+
s ↝ addUpkeep record s { FFDState = ffds' } EB-Role
71+
72+
V-Role : let open LeiosState s renaming (FFDState to ffds)
73+
EBs' = filter (allIBRefsKnown s) $ filter (_∈ᴮ slice L slot 1) EBs
74+
votes = map (vote sk-V ∘ hash) EBs'
75+
in
76+
∙ needsUpkeep V-Role
77+
∙ canProduceV slot sk-V (stake s)
78+
∙ ffds FFD.-⟦ Send (vHeader votes) nothing / SendRes ⟧⇀ ffds'
79+
─────────────────────────────────────────────────────────────────────────
80+
s ↝ addUpkeep record s { FFDState = ffds' } V-Role
81+
82+
No-IB-Role : let open LeiosState s in
83+
∙ needsUpkeep IB-Role
84+
∙ ¬ canProduceIB slot sk-IB (stake s) π
85+
─────────────────────────────────────────────
86+
s ↝ addUpkeep s IB-Role
87+
88+
No-EB-Role : let open LeiosState s in
89+
∙ needsUpkeep EB-Role
90+
∙ ¬ canProduceEB slot sk-EB (stake s) π
91+
─────────────────────────────────────────────
92+
s ↝ addUpkeep s EB-Role
93+
94+
No-V-Role : let open LeiosState s in
95+
∙ needsUpkeep V-Role
96+
∙ ¬ canProduceV slot sk-V (stake s)
97+
─────────────────────────────────────────────
98+
s ↝ addUpkeep s V-Role
99+
100+
data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → LeiosState → Type where
101+
102+
-- Initialization
103+
104+
Init :
105+
∙ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks'
106+
∙ initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs'
107+
────────────────────────────────────────────────────────────────
108+
nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs'
109+
110+
-- Network and Ledger
111+
112+
Slot : let open LeiosState s renaming (FFDState to ffds; BaseState to bs) in
113+
∙ Upkeep ≡ᵉ allUpkeep
114+
∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs'
115+
∙ ffds FFD.-⟦ Fetch / FetchRes msgs ⟧⇀ ffds'
116+
───────────────────────────────────────────────────────────────────────
117+
just s -⟦ SLOT / EMPTY ⟧⇀ record s
118+
{ FFDState = ffds'
119+
; BaseState = bs'
120+
; Ledger = constructLedger rbs
121+
; slot = suc slot
122+
; Upkeep = ∅
123+
} ↑ L.filter isValid? msgs
124+
125+
Ftch :
126+
────────────────────────────────────────────────────────
127+
just s -⟦ FTCH-LDG / FTCH-LDG (LeiosState.Ledger s) ⟧⇀ s
128+
129+
-- Base chain
130+
--
131+
-- Note: Submitted data to the base chain is only taken into account
132+
-- if the party submitting is the block producer on the base chain
133+
-- for the given slot
134+
135+
Base₁ :
136+
───────────────────────────────────────────────────────────────────
137+
just s -⟦ SUBMIT (inj₂ txs) / EMPTY ⟧⇀ record s { ToPropose = txs }
138+
139+
Base₂a : let open LeiosState s renaming (BaseState to bs) in
140+
∙ needsUpkeep Base
141+
∙ eb ∈ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs
142+
∙ bs B.-⟦ B.SUBMIT (this eb) / B.EMPTY ⟧⇀ bs'
143+
───────────────────────────────────────────────────────────────────────
144+
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base
145+
146+
Base₂b : let open LeiosState s renaming (BaseState to bs) in
147+
∙ needsUpkeep Base
148+
∙ [] ≡ filter (λ eb → isVoteCertified s eb × eb ∈ᴮ slice L slot 2) EBs
149+
∙ bs B.-⟦ B.SUBMIT (that ToPropose) / B.EMPTY ⟧⇀ bs'
150+
───────────────────────────────────────────────────────────────────────
151+
just s -⟦ SLOT / EMPTY ⟧⇀ addUpkeep record s { BaseState = bs' } Base
152+
153+
-- Protocol rules
154+
155+
Roles : ∙ s ↝ s'
156+
─────────────────────────────
157+
just s -⟦ SLOT / EMPTY ⟧⇀ s'

‎formal-spec/Leios/VRF.agda

+14
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,12 @@ record LeiosVRF : Type₁ where
3434
canProduceEB : ℕ → PrivKey → ℕ → VrfPf → Type
3535
canProduceEB slot k stake π = let (val , pf) = eval k (genEBInput slot) in val < stake × pf ≡ π
3636

37+
Dec-canProduceEB : ∀ {slot k stake} → (∃[ π ] canProduceEB slot k stake π) ⊎ (∀ π → ¬ canProduceEB slot k stake π)
38+
Dec-canProduceEB {slot} {k} {stake} with eval k (genEBInput slot)
39+
... | (val , pf) = case ¿ val < stake ¿ of λ where
40+
(yes p) → inj₁ (pf , p , refl)
41+
(no ¬p) → inj₂ (λ π (h , _) → ¬p h)
42+
3743
canProduceEBPub : ℕ → ℕ → PubKey → VrfPf → ℕ → Type
3844
canProduceEBPub slot val k pf stake = verify k (genEBInput slot) val pf × val < stake
3945

@@ -43,5 +49,13 @@ record LeiosVRF : Type₁ where
4349
canProduceV1 : ℕ → PrivKey → ℕ → Type
4450
canProduceV1 slot k stake = proj₁ (eval k (genV1Input slot)) < stake
4551

52+
Dec-canProduceV1 : ∀ {slot k stake} → Dec (canProduceV1 slot k stake)
53+
Dec-canProduceV1 {slot} {k} {stake} with eval k (genV1Input slot)
54+
... | (val , pf) = ¿ val < stake ¿
55+
4656
canProduceV2 : ℕ → PrivKey → ℕ → Type
4757
canProduceV2 slot k stake = proj₁ (eval k (genV2Input slot)) < stake
58+
59+
Dec-canProduceV2 : ∀ {slot k stake} → Dec (canProduceV2 slot k stake)
60+
Dec-canProduceV2 {slot} {k} {stake} with eval k (genV2Input slot)
61+
... | (val , pf) = ¿ val < stake ¿

‎formal-spec/StateMachine.agda

+56
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
{-# OPTIONS --safe #-}
2+
3+
module StateMachine where
4+
5+
open import Agda.Primitive using () renaming (Set to Type)
6+
7+
open import Prelude.Init hiding (map)
8+
open import Prelude.InferenceRules
9+
10+
open import Class.Bifunctor
11+
12+
private
13+
variable S I O : Type
14+
s s' s'' : S
15+
i : I
16+
is : List I
17+
o : O
18+
os : List O
19+
STS : S → I → O → S → Type
20+
21+
module _ (_-⟦_/_⟧⇀_ : S → I → O → S → Type) where
22+
data _-⟦_/_⟧*⇀_ : S → List I → List O → S → Type where
23+
24+
BS-base :
25+
─────────────────
26+
s -⟦ [] / [] ⟧*⇀ s
27+
28+
BS-ind :
29+
∙ s -⟦ i / o ⟧⇀ s'
30+
∙ s' -⟦ is / os ⟧*⇀ s''
31+
───────────────────────────────────────
32+
s -⟦ i ∷ is / o ∷ os ⟧*⇀ s''
33+
34+
ReflexiveTransitiveClosure = _-⟦_/_⟧*⇀_
35+
36+
data IdSTS {S} : S → ⊤ → ⊤ → S → Type where
37+
Id-nop : IdSTS s _ _ s
38+
39+
Invariant : (S → I → O → S → Type) → (S → Type) → Type
40+
Invariant _-⟦_/_⟧⇀_ P = ∀ {s i o s'} → s -⟦ i / o ⟧⇀ s' → P s → P s'
41+
42+
Total : (S → I → O → S → Type) → Type
43+
Total _-⟦_/_⟧⇀_ = ∀ {s i} → ∃₂[ o , s' ] s -⟦ i / o ⟧⇀ s'
44+
45+
STS⇒RTC : STS s i o s' → ReflexiveTransitiveClosure STS s (i ∷ []) (o ∷ []) s'
46+
STS⇒RTC sts = BS-ind sts BS-base
47+
48+
RTC-preserves-inv : ∀ {P} → Invariant STS P → Invariant (ReflexiveTransitiveClosure STS) P
49+
RTC-preserves-inv inv (BS-base) = id
50+
RTC-preserves-inv inv (BS-ind p₁ p₂) = RTC-preserves-inv inv p₂ ∘ inv p₁
51+
52+
RTC-total : Total STS → Total (ReflexiveTransitiveClosure STS)
53+
RTC-total SS-total {s} {[]} = ([] , s , BS-base)
54+
RTC-total SS-total {s} {i ∷ is} = case SS-total of λ where
55+
(o , s' , H) → case RTC-total SS-total of λ where
56+
(os , s'' , H') → (o ∷ os , s'' , BS-ind H H')

0 commit comments

Comments
 (0)
Please sign in to comment.