Skip to content

Commit b3df2e8

Browse files
yveshauserWhatisRT
yveshauser
and
WhatisRT
authored
Conformance testing (#4)
Co-authored-by: whatisRT <andre.knispel@iohk.io>
1 parent 377e998 commit b3df2e8

File tree

13 files changed

+149
-241
lines changed

13 files changed

+149
-241
lines changed

‎formal-spec/Everything.agda‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,6 @@ open import Leios.Traces
2525
open import Leios.Trace.Decidable
2626
open import Leios.Trace.Verifier
2727
open import Leios.Trace.Verifier.Test
28-
open import Leios.UniformShort
2928
open import Leios.Voting
3029
open import Leios.VRF
3130
open import StateMachine

‎formal-spec/Leios/Blocks.agda‎

Lines changed: 1 addition & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ record IsBlock (B : Type) : Type where
1414
field slotNumber : B → ℕ
1515
producerID : B → PoolID
1616
lotteryPf : B → VrfPf
17+
signature : B → Sig
1718

1819
infix 4 _∈ᴮ_
1920

@@ -82,22 +83,6 @@ mkIBHeader slot id π pKey txs = record { signature = sign pKey (hash h) ; IBHea
8283
getIBRef : ⦃ Hashable PreIBHeader Hash ⦄ → InputBlock → IBRef
8384
getIBRef = hash ∘ InputBlock.header
8485

85-
-- TODO
86-
record ibHeaderValid (h : IBHeader) : Type where
87-
record ibBodyValid (b : IBBody) : Type where
88-
89-
ibHeaderValid? : (h : IBHeader) → Dec (ibHeaderValid h)
90-
ibHeaderValid? _ = yes record {}
91-
92-
ibBodyValid? : (b : IBBody) → Dec (ibBodyValid b)
93-
ibBodyValid? _ = yes record {}
94-
95-
ibValid : InputBlock → Type
96-
ibValid record { header = h ; body = b } = ibHeaderValid h × ibBodyValid b
97-
98-
ibValid? : (ib : InputBlock) → Dec (ibValid ib)
99-
ibValid? record { header = h ; body = b } = ibHeaderValid? h ×-dec ibBodyValid? b
100-
10186
--------------------------------------------------------------------------------
10287
-- Endorser Blocks
10388
--------------------------------------------------------------------------------
@@ -138,25 +123,11 @@ mkEB slot id π pKey LI LE = record { signature = sign pKey (hash b) ; EndorserB
138123
getEBRef : ⦃ Hashable PreEndorserBlock Hash ⦄ → EndorserBlock → EBRef
139124
getEBRef = hash
140125

141-
-- TODO
142-
record ebValid (eb : EndorserBlock) : Type where
143-
-- field lotteryPfValid : {!!}
144-
-- signatureValid : {!!}
145-
-- ibRefsValid : {!!}
146-
-- ebRefsValid : {!!}
147-
148-
ebValid? : (eb : EndorserBlock) → Dec (ebValid eb)
149-
ebValid? _ = yes record {}
150-
151126
--------------------------------------------------------------------------------
152127
-- Votes
153128
--------------------------------------------------------------------------------
154129

155-
-- TODO
156-
record vsValid (vs : List Vote) : Type where
157130

158-
vsValid? : (vs : List Vote) → Dec (vsValid vs)
159-
vsValid? _ = yes record {}
160131

161132
--------------------------------------------------------------------------------
162133
-- FFD for Leios Blocks
@@ -189,30 +160,6 @@ module GenFFD ⦃ _ : IsBlock (List Vote) ⦄ where
189160
match (ibHeader h) (ibBody b) = matchIB h b
190161
match _ _ = ⊥
191162

192-
headerValid : Header → Type
193-
headerValid (ibHeader h) = ibHeaderValid h
194-
headerValid (ebHeader h) = ebValid h
195-
headerValid (vHeader h) = vsValid h
196-
197-
headerValid? : (h : Header) → Dec (headerValid h)
198-
headerValid? (ibHeader h) = ibHeaderValid? h
199-
headerValid? (ebHeader h) = ebValid? h
200-
headerValid? (vHeader h) = vsValid? h
201-
202-
bodyValid : Body → Type
203-
bodyValid (ibBody b) = ibBodyValid b
204-
205-
bodyValid? : (b : Body) → Dec (bodyValid b)
206-
bodyValid? (ibBody b) = ibBodyValid? b
207-
208-
isValid : Header ⊎ Body → Type
209-
isValid (inj₁ h) = headerValid h
210-
isValid (inj₂ b) = bodyValid b
211-
212-
isValid? : ∀ (x : Header ⊎ Body) → Dec (isValid x)
213-
isValid? (inj₁ h) = headerValid? h
214-
isValid? (inj₂ b) = bodyValid? b
215-
216163
-- can we express uniqueness wrt pipelines as a property?
217164
msgID : Header → ID
218165
msgID (ibHeader h) = (slotNumber h , producerID h)

‎formal-spec/Leios/Foreign/Types.agda‎

Lines changed: 16 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,10 @@ module Leios.Foreign.Types where
1919
{-# LANGUAGE DuplicateRecordFields #-}
2020
#-}
2121

22-
open import Leios.Defaults 2 fzero -- TODO: parameters
22+
numberOfParties : ℕ
23+
numberOfParties = 2
24+
25+
open import Leios.Defaults numberOfParties fzero
2326
renaming (EndorserBlock to EndorserBlockAgda; IBHeader to IBHeaderAgda)
2427

2528
dropDash : S.String → S.String
@@ -52,8 +55,8 @@ instance
5255
{ to = λ (record { slotNumber = s ; producerID = p ; bodyHash = h }) →
5356
record { slotNumber = s ; producerID = toℕ p ; bodyHash = h}
5457
; from = λ (record { slotNumber = s ; producerID = p ; bodyHash = h }) →
55-
case p <? 2 of λ where
56-
(yes q) → record { slotNumber = s ; producerID = #_ p {2} {fromWitness q} ; lotteryPf = tt ; bodyHash = h ; signature = tt }
58+
case p <? numberOfParties of λ where
59+
(yes q) → record { slotNumber = s ; producerID = #_ p {numberOfParties} {fromWitness q} ; lotteryPf = tt ; bodyHash = h ; signature = tt }
5760
(no _) → error "Conversion to Fin not possible!"
5861
}
5962

@@ -87,8 +90,8 @@ instance
8790
{ to = λ (record { slotNumber = s ; producerID = p ; ibRefs = refs }) →
8891
record { slotNumber = s ; producerID = toℕ p ; ibRefs = refs }
8992
; from = λ (record { slotNumber = s ; producerID = p ; ibRefs = refs }) →
90-
case p <? 2 of λ where
91-
(yes q) → record { slotNumber = s ; producerID = #_ p {2} {fromWitness q} ; lotteryPf = tt ; signature = tt ; ibRefs = refs ; ebRefs = [] }
93+
case p <? numberOfParties of λ where
94+
(yes q) → record { slotNumber = s ; producerID = #_ p {numberOfParties} {fromWitness q} ; lotteryPf = tt ; signature = tt ; ibRefs = refs ; ebRefs = [] }
9295
(no _) → error "Conversion to Fin not possible!"
9396
}
9497

@@ -143,9 +146,16 @@ instance
143146

144147
open import Class.Computational as C
145148
open import Class.Computational22
146-
open import Leios.Short.Deterministic st public
147149

148150
open Computational22
151+
open BaseAbstract
152+
open FFDAbstract
153+
154+
open GenFFD.Header using (ibHeader; ebHeader; vHeader)
155+
open GenFFD.Body using (ibBody)
156+
open FFDState
157+
158+
open import Leios.Short.Deterministic st public
149159

150160
stepHs : HsType (LeiosState → LeiosInput → C.ComputationResult String (LeiosOutput × LeiosState))
151161
stepHs = to (compute Computational--⟦/⟧⇀)

‎formal-spec/Leios/Protocol.agda‎

Lines changed: 109 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ record LeiosState : Type where
4545
Upkeep : ℙ SlotUpkeep
4646
BaseState : B.State
4747
votingState : VotingState
48+
PubKeys : List PubKey
4849

4950
lookupEB : EBRef → Maybe EndorserBlock
5051
lookupEB r = find (λ b → getEBRef b ≟ r) EBs
@@ -74,8 +75,8 @@ addUpkeep : LeiosState → SlotUpkeep → LeiosState
7475
addUpkeep s u = let open LeiosState s in record s { Upkeep = Upkeep ∪ ❴ u ❵ }
7576
{-# INJECTIVE_FOR_INFERENCE addUpkeep #-}
7677

77-
initLeiosState : VTy → StakeDistr → B.State → LeiosState
78-
initLeiosState V SD bs = record
78+
initLeiosState : VTy → StakeDistr → B.State → List PubKey → LeiosState
79+
initLeiosState V SD bs pks = record
7980
{ V = V
8081
; SD = SD
8182
; FFDState = FFD.initFFDState
@@ -90,8 +91,114 @@ initLeiosState V SD bs = record
9091
; Upkeep = ∅
9192
; BaseState = bs
9293
; votingState = initVotingState
94+
; PubKeys = pks
9395
}
9496

97+
stake' : PoolID → LeiosState → ℕ
98+
stake' pid record { SD = SD } = TotalMap.lookup SD pid
99+
100+
stake'' : PubKey → LeiosState → ℕ
101+
stake'' pk = stake' (poolID pk)
102+
103+
stake : LeiosState → ℕ
104+
stake = stake' id
105+
106+
lookupPubKeyAndStake : ∀ {B} → ⦃ _ : IsBlock B ⦄ → LeiosState → B → Maybe (PubKey × ℕ)
107+
lookupPubKeyAndStake s b =
108+
L.head $
109+
L.map (λ pk → (pk , stake'' pk s)) $
110+
L.filter ((producerID b ≟_) ∘ poolID) (LeiosState.PubKeys s)
111+
112+
module _ (s : LeiosState) where
113+
114+
record ibHeaderValid (h : IBHeader) (pk : PubKey) (st : ℕ) : Type where
115+
field lotteryPfValid : verify pk (slotNumber h) st (lotteryPf h)
116+
signatureValid : verifySig pk (signature h)
117+
118+
record ibBodyValid (b : IBBody) : Type where
119+
120+
ibHeaderValid? : (h : IBHeader) (pk : PubKey) (st : ℕ) → Dec (ibHeaderValid h pk st)
121+
ibHeaderValid? h pk st
122+
with verify? pk (slotNumber h) st (lotteryPf h)
123+
... | no ¬p = no (¬p ∘ ibHeaderValid.lotteryPfValid)
124+
... | yes p
125+
with verifySig? pk (signature h)
126+
... | yes q = yes (record { lotteryPfValid = p ; signatureValid = q })
127+
... | no ¬q = no (¬q ∘ ibHeaderValid.signatureValid)
128+
129+
ibBodyValid? : (b : IBBody) → Dec (ibBodyValid b)
130+
ibBodyValid? _ = yes record {}
131+
132+
ibValid : InputBlock → Type
133+
ibValid record { header = h ; body = b }
134+
with lookupPubKeyAndStake s h
135+
... | just (pk , pid) = ibHeaderValid h pk (stake'' pk s) × ibBodyValid b
136+
... | nothing = ⊥
137+
138+
ibValid? : (ib : InputBlock) → Dec (ibValid ib)
139+
ibValid? record { header = h ; body = b }
140+
with lookupPubKeyAndStake s h
141+
... | just (pk , pid) = ibHeaderValid? h pk (stake'' pk s) ×-dec ibBodyValid? b
142+
... | nothing = no λ x → x
143+
144+
record ebValid (eb : EndorserBlock) (pk : PubKey) (st : ℕ) : Type where
145+
field lotteryPfValid : verify pk (slotNumber eb) st (lotteryPf eb)
146+
signatureValid : verifySig pk (signature eb)
147+
-- TODO
148+
-- ibRefsValid : ?
149+
-- ebRefsValid : ?
150+
151+
ebValid? : (eb : EndorserBlock) (pk : PubKey) (st : ℕ) → Dec (ebValid eb pk st)
152+
ebValid? h pk st
153+
with verify? pk (slotNumber h) st (lotteryPf h)
154+
... | no ¬p = no (¬p ∘ ebValid.lotteryPfValid)
155+
... | yes p
156+
with verifySig? pk (signature h)
157+
... | yes q = yes (record { lotteryPfValid = p ; signatureValid = q })
158+
... | no ¬q = no (¬q ∘ ebValid.signatureValid)
159+
160+
-- TODO
161+
record vsValid (vs : List Vote) : Type where
162+
163+
vsValid? : (vs : List Vote) → Dec (vsValid vs)
164+
vsValid? _ = yes record {}
165+
166+
headerValid : Header → Type
167+
headerValid (ibHeader h)
168+
with lookupPubKeyAndStake s h
169+
... | just (pk , pid) = ibHeaderValid h pk (stake'' pk s)
170+
... | nothing = ⊥
171+
headerValid (ebHeader h)
172+
with lookupPubKeyAndStake s h
173+
... | just (pk , pid) = ebValid h pk (stake'' pk s)
174+
... | nothing = ⊥
175+
headerValid (vHeader h) = vsValid h
176+
177+
headerValid? : (h : Header) → Dec (headerValid h)
178+
headerValid? (ibHeader h)
179+
with lookupPubKeyAndStake s h
180+
... | just (pk , pid) = ibHeaderValid? h pk (stake'' pk s)
181+
... | nothing = no λ x → x
182+
headerValid? (ebHeader h)
183+
with lookupPubKeyAndStake s h
184+
... | just (pk , pid) = ebValid? h pk (stake'' pk s)
185+
... | nothing = no λ x → x
186+
headerValid? (vHeader h) = vsValid? h
187+
188+
bodyValid : Body → Type
189+
bodyValid (ibBody b) = ibBodyValid b
190+
191+
bodyValid? : (b : Body) → Dec (bodyValid b)
192+
bodyValid? (ibBody b) = ibBodyValid? b
193+
194+
isValid : Header ⊎ Body → Type
195+
isValid (inj₁ h) = headerValid h
196+
isValid (inj₂ b) = bodyValid b
197+
198+
isValid? : ∀ (x : Header ⊎ Body) → Dec (isValid x)
199+
isValid? (inj₁ h) = headerValid? h
200+
isValid? (inj₂ b) = bodyValid? b
201+
95202
-- some predicates about EBs
96203
module _ (s : LeiosState) (eb : EndorserBlock) where
97204
open EndorserBlockOSig eb
@@ -100,9 +207,6 @@ module _ (s : LeiosState) (eb : EndorserBlock) where
100207
allIBRefsKnown : Type
101208
allIBRefsKnown = ∀[ ref ∈ fromList ibRefs ] ref ∈ˡ map getIBRef IBs
102209

103-
stake : LeiosState → ℕ
104-
stake record { SD = SD } = TotalMap.lookup SD id
105-
106210
module _ (s : LeiosState) where
107211

108212
open LeiosState s

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -126,7 +126,7 @@ data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → Leios
126126
∙ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks'
127127
∙ initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs'
128128
────────────────────────────────────────────────────────────────
129-
nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs'
129+
nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' pks
130130
```
131131
#### Network and Ledger
132132
```agda
@@ -141,7 +141,7 @@ data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → Leios
141141
; Ledger = constructLedger rbs
142142
; slot = suc slot
143143
; Upkeep = ∅
144-
} ↑ L.filter isValid? msgs
144+
} ↑ L.filter (isValid? s) msgs
145145
```
146146
```agda
147147
Ftch :

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ data _⊢_ : LeiosInput → LeiosState → Type where
5656
∙ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks'
5757
∙ initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs'
5858
────────────────────────────────────────────────────────────────
59-
INIT V ⊢ initLeiosState V SD bs'
59+
INIT V ⊢ initLeiosState V SD bs' pks
6060

6161
data _-⟦Base⟧⇀_ : LeiosState → LeiosState → Type where
6262

@@ -242,7 +242,7 @@ data _-⟦_/_⟧⇀_ : LeiosState → LeiosInput → LeiosOutput → LeiosState
242242
; slot = suc slot
243243
; Upkeep = ∅
244244
; BaseState = bs'
245-
} ↑ L.filter isValid? msgs
245+
} ↑ L.filter (isValid? s) msgs
246246
in
247247
∙ Upkeep ≡ᵉ allUpkeep
248248
∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs'
@@ -284,7 +284,7 @@ _-⟦_/_⟧ⁿᵈ*⇀_ = ReflexiveTransitiveClosure _-⟦_/_⟧ⁿᵈ⇀_
284284
let
285285
s0 = _
286286
upkeep≡∅ : LeiosState.Upkeep s0 ≡ ∅
287-
upkeep≡∅ = sym (↑-preserves-Upkeep {x = L.filter isValid? msgs})
287+
upkeep≡∅ = sym (↑-preserves-Upkeep {x = L.filter (isValid? s) msgs})
288288
needsAllUpkeep : ∀ {u} → LeiosState.needsUpkeep s0 u
289289
needsAllUpkeep {u} = subst (u ∉_) (sym upkeep≡∅) Properties.∉-∅
290290
needsUpkeep1 : ∀ {u} → u ≢ Base → LeiosState.needsUpkeep s1 u

‎formal-spec/Leios/Simplified.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -132,7 +132,7 @@ data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → Leios
132132
∙ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks'
133133
∙ initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs'
134134
────────────────────────────────────────────────────────────────
135-
nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs'
135+
nothing -⟦ INIT V / EMPTY ⟧⇀ initLeiosState V SD bs' pks
136136

137137
-- Network and Ledger
138138

@@ -147,7 +147,7 @@ data _-⟦_/_⟧⇀_ : Maybe LeiosState → LeiosInput → LeiosOutput → Leios
147147
; slot = suc slot
148148
; Upkeep = ∅
149149
; BaseState = bs'
150-
} ↑ L.filter isValid? msgs
150+
} ↑ L.filter (isValid? s) msgs
151151

152152
Ftch :
153153
────────────────────────────────────────────────────────

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ data _⊢_ : LeiosInput → LeiosState → Type where
5656
∙ ks K.-⟦ K.INIT pk-IB pk-EB pk-V / K.PUBKEYS pks ⟧⇀ ks'
5757
∙ initBaseState B.-⟦ B.INIT (V-chkCerts pks) / B.STAKE SD ⟧⇀ bs'
5858
────────────────────────────────────────────────────────────────
59-
INIT V ⊢ initLeiosState V SD bs'
59+
INIT V ⊢ initLeiosState V SD bs' pks
6060

6161
data _-⟦Base⟧⇀_ : LeiosState → LeiosState → Type where
6262

@@ -274,7 +274,7 @@ data _-⟦_/_⟧⇀_ : LeiosState → LeiosInput → LeiosOutput → LeiosState
274274
; slot = suc slot
275275
; Upkeep = ∅
276276
; BaseState = bs'
277-
} ↑ L.filter isValid? msgs
277+
} ↑ L.filter (isValid? s) msgs
278278
in
279279
∙ Upkeep ≡ᵉ allUpkeep
280280
∙ bs B.-⟦ B.FTCH-LDG / B.BASE-LDG rbs ⟧⇀ bs'
@@ -317,7 +317,7 @@ _-⟦_/_⟧ⁿᵈ*⇀_ = ReflexiveTransitiveClosure _-⟦_/_⟧ⁿᵈ⇀_
317317
let
318318
s0 = _
319319
upkeep≡∅ : LeiosState.Upkeep s0 ≡ ∅
320-
upkeep≡∅ = sym (↑-preserves-Upkeep {x = L.filter isValid? msgs})
320+
upkeep≡∅ = sym (↑-preserves-Upkeep {x = L.filter (isValid? s) msgs})
321321
needsAllUpkeep : ∀ {u} → LeiosState.needsUpkeep s0 u
322322
needsAllUpkeep {u} = subst (u ∉_) (sym upkeep≡∅) Properties.∉-∅
323323
needsUpkeep1 : ∀ {u} → u ≢ Base → LeiosState.needsUpkeep s1 u

0 commit comments

Comments
 (0)