Skip to content

Commit 2ccae64

Browse files
yveshauserWhatisRT
yveshauser
and
WhatisRT
authored
Linear Leios trace verifier (#22)
Co-authored-by: whatisRT <[email protected]>
1 parent df9ec30 commit 2ccae64

File tree

8 files changed

+458
-27
lines changed

8 files changed

+458
-27
lines changed

‎formal-spec/Everything.agda‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -46,13 +46,14 @@ open import Leios.Foreign.Types
4646
open import Leios.Foreign.Util
4747
open import Leios.KeyRegistration
4848
open import Leios.Linear
49+
open import Leios.Linear.Trace.Verifier
50+
open import Leios.Linear.Trace.Verifier.Test
4951
-- open import Leios.Network
5052
open import Leios.Prelude
5153
open import Leios.Protocol
52-
-- open import Leios.Short
53-
-- TODO: drop Deterministic
54+
open import Leios.Short
5455
-- open import Leios.Short.Deterministic
55-
-- open import Leios.Short.Trace.Verifier
56+
open import Leios.Short.Trace.Verifier
5657
-- open import Leios.Short.Trace.Verifier.Test
5758
-- open import Leios.Simplified
5859
-- open import Leios.Simplified.Deterministic
@@ -66,3 +67,5 @@ open import StateMachine
6667
-- Networking
6768
open import Network.BasicBroadcast
6869
-- open import Network.Leios
70+
71+
open import Prelude.Result

‎formal-spec/Leios/Defaults.agda‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -137,7 +137,7 @@ instance
137137
hhs .hash = IBHeaderOSig.bodyHash
138138

139139
hpe : Hashable PreEndorserBlock (List ℕ)
140-
hpe .hash = L.concat ∘ EndorserBlockOSig.ibRefs
140+
hpe .hash = EndorserBlockOSig.txs
141141

142142
record FFDBuffers : Type where
143143
field inIBs : List InputBlock

‎formal-spec/Leios/Linear.lagda.md‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,7 @@ mempool.
124124
→ let open LeiosState s
125125
in
126126
∙ getCurrentEBHash s ≡ just ebHash
127-
∙ find (λ (s , eb) → hash eb ≟ ebHash) EBs' ≡ just (slot' , eb)
127+
∙ find (λ (_ , eb') → hash eb' ≟ ebHash) EBs' ≡ just (slot' , eb)
128128
∙ hash eb ∉ VotedEBs
129129
∙ ¬ isEquivocated s eb
130130
∙ isValid s (inj₁ (ebHeader eb))
@@ -143,7 +143,7 @@ Predicate needed for slot transition. Special care needs to be taken when starti
143143
genesis.
144144
```agda
145145
allDone : LeiosState → Type
146-
allDone record { Upkeep = u } = fromList u ≡ᵉ fromList (EB-Role ∷ VT-Role ∷ Base ∷ [])
146+
allDone record { Upkeep = u } = VT-Role ∈ˡ u × EB-Role ∈ˡ u × Base ∈ˡ u
147147
```
148148
### Linear Leios transitions
149149
The relation describing the transition given input and state
@@ -214,11 +214,11 @@ Note: Submitted data to the base chain is only taken into account
214214
──────────────────────────────────────────────────────────────────────────────
215215
s -⟦ honestOutputI (rcvˡ (-, SLOT)) / honestInputO' (sndˡ (-, FFD-IN i)) ⟧⇀ s'
216216
217-
Roles₂ : ∀ {x u s'} → let open LeiosState s in
218-
∙ ¬ (s ↝ (s' , x))
219-
∙ needsUpkeep u
217+
Roles₂ : ∀ {u} → let open LeiosState in
218+
∙ ¬ (∃[ s'×i ] (s ↝ s'×i × Upkeep (addUpkeep s u) ≡ Upkeep (proj₁ s'×i)))
219+
∙ needsUpkeep s u
220220
∙ u ≢ Base
221-
──────────────────────────────────────────────────────────────
221+
─────────────────────────────────────────────────────────────────────────
222222
s -⟦ honestOutputI (rcvˡ (-, SLOT)) / nothing ⟧⇀ addUpkeep s u
223223
```
224224
<!--
@@ -229,6 +229,10 @@ ShortLeios .Machine.stepRel = _-⟦_/_⟧⇀_
229229
230230
open import Prelude.STS.GenPremises
231231
232+
instance
233+
Dec-isValid : ∀ {s x} → isValid s x ⁇
234+
Dec-isValid {s} {x} = ⁇ isValid? s x
235+
232236
unquoteDecl EB-Role-premises = genPremises EB-Role-premises (quote _↝_.EB-Role)
233237
unquoteDecl VT-Role-premises = genPremises VT-Role-premises (quote _↝_.VT-Role)
234238

‎formal-spec/Leios/Linear/Trace/Verifier.agda‎

Lines changed: 264 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,264 @@
1+
open import Leios.Prelude hiding (id; _>>=_; return; _⊗_)
2+
open import Leios.Config
3+
open import Leios.SpecStructure using (SpecStructure)
4+
5+
open import Prelude.Result
6+
open import CategoricalCrypto hiding (id; _∘_)
7+
8+
open import Data.List.Properties
9+
open import Data.Maybe.Properties
10+
open import Data.Product.Properties
11+
12+
module Leios.Linear.Trace.Verifier (params : Params) where
13+
14+
-- SpecStructure is not a module parameter, as the type for VrfPf needs to be known
15+
open import Leios.Defaults params using (d-SpecStructure; isb; hpe) public
16+
open SpecStructure d-SpecStructure hiding (Hashable-IBHeader; Hashable-EndorserBlock; isVoteCertified) public
17+
18+
module Defaults
19+
(Lhdr Lvote Ldiff : ℕ)
20+
(splitTxs : List Tx → List Tx × List Tx)
21+
(validityCheckTime : EndorserBlock → ℕ)
22+
where
23+
24+
open import Leios.Linear d-SpecStructure params Lhdr Lvote Ldiff splitTxs validityCheckTime public
25+
open FFD hiding (_-⟦_/_⟧⇀_)
26+
open GenFFD
27+
open Types params
28+
29+
data Action : Type where
30+
EB-Role-Action : ℕ → EndorserBlock → Action
31+
VT-Role-Action : ℕ → EndorserBlock → ℕ → Action
32+
Ftch-Action : ℕ → Action
33+
Slot₁-Action : ℕ → Action
34+
Slot₂-Action : ℕ → Action
35+
Base₁-Action : ℕ → Action
36+
Base₂-Action : ℕ → Action
37+
No-EB-Role-Action : ℕ → Action
38+
No-VT-Role-Action : ℕ → Action
39+
40+
TestTrace = List (Action × (FFDT Out ⊎ BaseT Out ⊎ IOT In))
41+
42+
private variable
43+
s s′ : LeiosState
44+
σ : Action
45+
σs : TestTrace
46+
ib : InputBlock
47+
eb : EndorserBlock
48+
ebs : List EndorserBlock
49+
vt : List Vote
50+
i : FFDT Out ⊎ BaseT Out ⊎ IOT In
51+
o : FFDT In
52+
53+
open LeiosState
54+
55+
getAction : ∀ {i o} → s -⟦ i / o ⟧⇀ s′ → Action
56+
getAction (Slot₁ {s} _) = Slot₁-Action (slot s)
57+
getAction (Slot₂ {s}) = Slot₂-Action (slot s)
58+
getAction (Ftch {s}) = Ftch-Action (slot s)
59+
getAction (Base₁ {s}) = Base₁-Action (slot s)
60+
getAction (Base₂ {s} _) = Base₂-Action (slot s)
61+
getAction (Roles₁ (VT-Role {s} {eb = eb} {slot' = slot'} _)) = VT-Role-Action (slot s) eb slot'
62+
getAction (Roles₁ (EB-Role {s} {eb = eb} _)) = EB-Role-Action (slot s) eb
63+
getAction (Roles₂ {u = Base} (_ , _ , x)) = ⊥-elim (x refl)
64+
getAction (Roles₂ {s} {u = EB-Role} _) = No-EB-Role-Action (slot s)
65+
getAction (Roles₂ {s} {u = VT-Role} _) = No-VT-Role-Action (slot s)
66+
67+
getSlot : Action → ℕ
68+
getSlot (EB-Role-Action x _) = x
69+
getSlot (VT-Role-Action x _ _) = x
70+
getSlot (No-EB-Role-Action x) = x
71+
getSlot (No-VT-Role-Action x) = x
72+
getSlot (Ftch-Action x) = x
73+
getSlot (Slot₁-Action x) = x
74+
getSlot (Slot₂-Action x) = x
75+
getSlot (Base₁-Action x) = x
76+
getSlot (Base₂-Action x) = x
77+
78+
79+
data Err-verifyAction (σ : Action) (i : FFDT Out ⊎ BaseT Out ⊎ IOT In) (s : LeiosState) : Type where
80+
E-Err-Slot : getSlot σ ≢ slot s → Err-verifyAction σ i s
81+
E-Err-CanProduceIB : (∀ π → ¬ canProduceIB (slot s) sk-IB (stake s) π) → Err-verifyAction σ i s
82+
dummyErr : Err-verifyAction σ i s
83+
84+
-- NOTE: this goes backwards, from the current state to the initial state
85+
data _—→_ : LeiosState → LeiosState → Type where
86+
87+
ActionStep : ∀ {s i o s′} →
88+
∙ s -⟦ i / o ⟧⇀ s′
89+
───────────────────
90+
s′ —→ s
91+
92+
open import Prelude.Closures _—→_
93+
94+
toRcvType : FFDT Out ⊎ BaseT Out ⊎ IOT In → ∃ (Channel.rcvType ((FFD ⊗ BaseC) ⊗ ((IO ⊗ Adv) ᵀ)))
95+
toRcvType (inj₁ i) = honestOutputI (rcvˡ (-, i))
96+
toRcvType (inj₂ (inj₁ i)) = honestOutputI (rcvʳ (-, i))
97+
toRcvType (inj₂ (inj₂ i)) = honestInputI (-, i)
98+
99+
infix 0 _≈_ _≈¹_
100+
101+
data _≈¹_ : Action × (FFDT Out ⊎ BaseT Out ⊎ IOT In) → s′ —→ s → Type where
102+
103+
FromAction :
104+
∀ i {s′ o}
105+
→ (σ : s -⟦ toRcvType i / o ⟧⇀ s′)
106+
→ (getAction σ , i) ≈¹ ActionStep σ
107+
108+
data ValidStep (es : Action × (FFDT Out ⊎ BaseT Out ⊎ IOT In)) (s : LeiosState) : Type where
109+
Valid : (tr : s′ —→ s) → es ≈¹ tr → ValidStep es s
110+
111+
data _≈_ : TestTrace → s′ —↠ s → Type where
112+
113+
FromAction :
114+
∀ i {σs s′ s₀ o} {tr : s —↠ s₀}
115+
→ σs ≈ tr
116+
→ (σ : s -⟦ toRcvType i / o ⟧⇀ s′)
117+
→ (getAction σ , i) ∷ σs ≈ s′ —→⟨ ActionStep σ ⟩ tr
118+
119+
Done : [] ≈ s ∎
120+
121+
data ValidTrace (es : TestTrace) (s : LeiosState) : Type where
122+
Valid : (tr : s′ —↠ s) → es ≈ tr → ValidTrace es s
123+
124+
getNewState : ∀ {es s} → ValidTrace es s → LeiosState
125+
getNewState (Valid {s′ = s} _ _) = s
126+
127+
data Err-verifyTrace : TestTrace → LeiosState → Type where
128+
Err-StepOk : Err-verifyTrace σs s → Err-verifyTrace ((σ , i) ∷ σs) s
129+
Err-Action : Err-verifyAction σ i s′ → Err-verifyTrace ((σ , i) ∷ σs) s
130+
131+
Ok' : ∀ {s i o s′} → (σ : s -⟦ toRcvType i / o ⟧⇀ s′)
132+
→ Result (Err-verifyAction (getAction σ) i s) (ValidStep (getAction σ , i) s)
133+
Ok' a = Ok (Valid _ (FromAction _ a))
134+
135+
just≢nothing : ∀ {ℓ} {A : Type ℓ} {x} → (Maybe A ∋ just x) ≡ nothing → ⊥
136+
just≢nothing = λ ()
137+
138+
nothing≢just : ∀ {ℓ} {A : Type ℓ} {x} → nothing ≡ (Maybe A ∋ just x) → ⊥
139+
nothing≢just = λ ()
140+
141+
P : EBRef → ℕ × EndorserBlock → Type
142+
P h (_ , eb) = hash eb ≡ h
143+
144+
P? : (h : EBRef) → ((s , eb) : ℕ × EndorserBlock) → Dec (P h (s , eb))
145+
P? h (_ , eb) = hash eb ≟ h
146+
147+
not-found : LeiosState → EBRef → Type
148+
not-found s k = find (P? k) (LeiosState.EBs' s) ≡ nothing
149+
150+
subst' : ∀ {s ebHash ebHash₁ slot' slot'' eb eb₁}
151+
→ getCurrentEBHash s ≡ just ebHash₁
152+
→ find (λ (_ , eb') → hash eb' ≟ ebHash₁) (LeiosState.EBs' s) ≡ just (slot'' , eb₁)
153+
→ getCurrentEBHash s ≡ just ebHash
154+
→ find (λ (_ , eb') → hash eb' ≟ ebHash) (LeiosState.EBs' s) ≡ just (slot' , eb)
155+
→ (eb₁ , ebHash₁ , slot'') ≡ (eb , ebHash , slot')
156+
subst' {s} {ebHash = ebHash} {eb = eb} eq₁₁ eq₁₂ eq₂₁ eq₂₂
157+
with getCurrentEBHash s | eq₁₁ | eq₂₁
158+
... | _ | refl | refl
159+
with find (λ (_ , eb') → hash eb' ≟ ebHash) (LeiosState.EBs' s) | eq₁₂ | eq₂₂
160+
... | _ | refl | refl = refl
161+
162+
Base≢EB-Role : SlotUpkeep.Base ≢ SlotUpkeep.EB-Role
163+
Base≢EB-Role = λ ()
164+
165+
Base≢VT-Role : SlotUpkeep.Base ≢ SlotUpkeep.VT-Role
166+
Base≢VT-Role = λ ()
167+
168+
instance
169+
Dec-↝ : ∀ {s u} → (∃[ s'×i ] (s ↝ s'×i × (u ∷ LeiosState.Upkeep s) ≡ LeiosState.Upkeep (proj₁ s'×i))) ⁇
170+
Dec-↝ {s} {EB-Role} .dec
171+
with toProposeEB s _ in eq₁
172+
... | nothing = no λ where (_ , EB-Role (p , _) , _) → nothing≢just (trans (sym eq₁) p)
173+
... | just eb
174+
with ¿ canProduceEB (LeiosState.slot s) sk-EB (stake s) _ ¿
175+
... | yes q = yes (_ , EB-Role (eq₁ , q) , refl)
176+
... | no ¬q = no λ where (_ , EB-Role (_ , q) , _) → ¬q q
177+
Dec-↝ {s} {VT-Role} .dec
178+
with getCurrentEBHash s in eq₂
179+
... | nothing = no λ where (_ , VT-Role (p , _) , _) → nothing≢just (trans (sym eq₂) p)
180+
... | just ebHash
181+
with find (λ (_ , eb') → hash eb' ≟ ebHash) (LeiosState.EBs' s) in eq₃
182+
... | nothing = no λ where
183+
(_ , VT-Role (x , y , _) , _) →
184+
let ji = just-injective (trans (sym x) eq₂)
185+
in just≢nothing $ trans (sym y) (subst (not-found s) (sym ji) eq₃)
186+
... | just (slot' , eb)
187+
with ¿ VT-Role-premises {s} {eb} {ebHash} {slot'} .proj₁ ¿
188+
... | yes p = yes ((rememberVote (addUpkeep s VT-Role) eb , Send (vtHeader [ vote sk-VT (hash eb) ]) nothing) ,
189+
VT-Role p , refl)
190+
... | no ¬p = no λ where (_ , VT-Role (x , y , p) , _) → ¬p $ subst
191+
(λ where (eb , ebHash , slot) → VT-Role-premises {s} {eb} {ebHash} {slot} .proj₁)
192+
(subst' {s} x y eq₂ eq₃) (x , y , p)
193+
Dec-↝ {s} {Base} .dec = no λ where
194+
(_ , EB-Role _ , x) → Base≢EB-Role (∷-injectiveˡ (trans x refl))
195+
(_ , VT-Role _ , x) → Base≢VT-Role (∷-injectiveˡ (trans x refl))
196+
197+
open import Prelude.STS.GenPremises
198+
unquoteDecl Roles₂-premises = genPremises Roles₂-premises (quote Roles₂)
199+
200+
verifyStep' : (a : Action) → (i : FFDT Out ⊎ BaseT Out ⊎ IOT In) → (s : LeiosState) → getSlot a ≡ slot s
201+
→ Result (Err-verifyAction a i s) (ValidStep (a , i) s)
202+
verifyStep' (EB-Role-Action n ebs) (inj₁ SLOT) s refl
203+
with ¿ EB-Role-premises {s = s} .proj₁ ¿
204+
... | yes h = Ok' (Roles₁ (EB-Role h))
205+
... | _ = Err dummyErr
206+
verifyStep' (EB-Role-Action _ _) (inj₁ FTCH) _ _ = Err dummyErr
207+
verifyStep' (EB-Role-Action _ _) (inj₁ (FFD-OUT _)) _ _ = Err dummyErr
208+
verifyStep' (VT-Role-Action .(slot s) eb slot') (inj₁ SLOT) s refl
209+
with ¿ VT-Role-premises {s = s} {eb = eb} {ebHash = hash eb} {slot' = slot'} .proj₁ ¿
210+
... | yes p = Ok' (Roles₁ (VT-Role {ebHash = hash eb} {slot' = slot'} p))
211+
... | no ¬h = Err dummyErr
212+
verifyStep' (VT-Role-Action _ _ _) (inj₁ FTCH) _ _ = Err dummyErr
213+
verifyStep' (VT-Role-Action _ _ _) (inj₁ (FFD-OUT _)) _ _ = Err dummyErr
214+
verifyStep' (VT-Role-Action _ _ _) (inj₂ _) _ refl = Err dummyErr
215+
216+
-- This has a different IO pattern, not sure if we want to model that here
217+
-- For now we'll just fail
218+
verifyStep' (Ftch-Action n) _ _ _ = Err dummyErr
219+
220+
verifyStep' (Slot₁-Action n) (inj₁ SLOT) _ _ = Err dummyErr
221+
verifyStep' (Slot₁-Action n) (inj₁ FTCH) _ _ = Err dummyErr
222+
verifyStep' (Slot₁-Action n) (inj₁ (FFD-OUT msgs)) s refl with ¿ Slot₁-premises {s = s} .proj₁ ¿
223+
... | yes p = Ok' (Slot₁ {s = s} {msgs = msgs} p)
224+
... | no _ = Err dummyErr
225+
verifyStep' (Slot₂-Action n) (inj₁ _) _ _ = Err dummyErr
226+
verifyStep' (Slot₂-Action n) (inj₂ (inj₁ (BASE-LDG rbs))) s refl = Ok' (Slot₂ {s = s} {rbs = rbs})
227+
verifyStep' (Slot₂-Action n) (inj₂ (inj₂ y)) s refl = Err dummyErr
228+
229+
-- Different IO pattern again
230+
verifyStep' (Base₁-Action n) (inj₂ (inj₂ (SubmitTxs txs))) s refl = Ok' Base₁
231+
verifyStep' (Base₂-Action n) (inj₁ SLOT) s refl with ¿ Base₂-premises {s = s} .proj₁ ¿
232+
... | yes p = Ok' (Base₂ p)
233+
... | no _ = Err dummyErr
234+
verifyStep' (Base₂-Action n) _ s refl = Err dummyErr
235+
verifyStep' (No-EB-Role-Action n) (inj₁ SLOT) s refl
236+
with ¿ Roles₂-premises {s = s} {u = EB-Role} .proj₁ ¿
237+
... | yes p = Ok' (Roles₂ p)
238+
... | no ¬p = Err dummyErr
239+
verifyStep' (No-EB-Role-Action n) _ s refl = Err dummyErr
240+
verifyStep' (No-VT-Role-Action n) (inj₁ SLOT) s refl
241+
with ¿ Roles₂-premises {s = s} {u = VT-Role} .proj₁ ¿
242+
... | yes p = Ok' (Roles₂ p)
243+
... | no ¬p = Err dummyErr
244+
verifyStep' (No-VT-Role-Action n) _ s refl = Err dummyErr
245+
verifyStep' (EB-Role-Action .(slot s) x) (inj₂ y) s refl = Err dummyErr
246+
verifyStep' (Slot₁-Action x₁) (inj₂ y) s x = Err dummyErr
247+
verifyStep' (Base₁-Action .(slot s)) (inj₁ x) s refl = Err dummyErr
248+
verifyStep' (Base₁-Action .(slot s)) (inj₂ y) s refl = Err dummyErr
249+
250+
verifyStep : (a : Action) → (i : FFDT Out ⊎ BaseT Out ⊎ IOT In) → (s : LeiosState) → Result (Err-verifyAction a i s) (ValidStep (a , i) s)
251+
verifyStep a i s = case getSlot a ≟ slot s of λ where
252+
(yes p) → verifyStep' a i s p
253+
(no ¬p) → Err (E-Err-Slot λ p → ⊥-elim (¬p p))
254+
255+
verifyTrace : ∀ (σs : TestTrace) → (s : LeiosState) → Result (Err-verifyTrace σs s) (ValidTrace σs s)
256+
verifyTrace [] s = Ok (Valid (s ∎) Done)
257+
verifyTrace ((a , i) ∷ σs) s = do
258+
σs ← mapErr Err-StepOk (verifyTrace σs s)
259+
x ← mapErr Err-Action (verifyStep a i (getNewState σs))
260+
return (σs Valid∷ʳ x)
261+
where
262+
open Monad-Result
263+
_Valid∷ʳ_ : ∀ {e es s} → (σs : ValidTrace es s) → ValidStep e (getNewState σs) → ValidTrace (e ∷ es) s
264+
Valid tr x Valid∷ʳ Valid (ActionStep as) (FromAction a _) = Valid (_ —→⟨ ActionStep as ⟩ tr) (FromAction a x as)

0 commit comments

Comments
 (0)