Skip to content

Commit df8b215

Browse files
yveshauseryveshauser
authored
More verbose errors for trace verifier (#366)
1 parent 2923d5b commit df8b215

File tree

10 files changed

+255
-127
lines changed

10 files changed

+255
-127
lines changed

‎flake.lock‎

Lines changed: 4 additions & 4 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎flake.nix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
url = "github:input-output-hk/iogx";
88
};
99

10-
leios-spec.url = "github:input-output-hk/ouroboros-leios-formal-spec?rev=9741f8a27a55d562b33d0b4ac4f9334fc9fba9e0";
10+
leios-spec.url = "github:input-output-hk/ouroboros-leios-formal-spec?rev=5f1b814dbe8abd4fda4c817899432754d43f929d";
1111
};
1212

1313

‎leios-trace-verifier/Parser.agda‎

Lines changed: 131 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -10,16 +10,19 @@ import Data.String as S
1010
open import Agda.Builtin.Word using (Word64; primWord64ToNat)
1111
open import Foreign.Haskell.Pair
1212

13+
open import Tactic.Defaults
14+
open import Tactic.Derive.Show
15+
1316
module Parser where
1417

1518
{-# FOREIGN GHC
1619
{-# LANGUAGE OverloadedStrings #-}
1720
#-}
1821

1922
postulate
20-
Int : Set
23+
Int : Set
2124
Micro : Set
22-
Map : Set → Set → Set
25+
Map : Set → Set → Set
2326
elems : ∀ {k v} → Map k v → List v
2427
trunc : Micro → ℕ
2528

@@ -43,10 +46,10 @@ postulate
4346
{-# COMPILE GHC elems = elems' #-}
4447
{-# COMPILE GHC trunc = trunc' #-}
4548

46-
Bytes = Word64
47-
SlotNo = Word64
49+
Bytes = Word64
50+
SlotNo = Word64
4851
PipelineNo = Word64
49-
Time = Micro
52+
Time = Micro
5053

5154
data NetworkAction : Type where
5255
Sent Received : NetworkAction
@@ -117,7 +120,7 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String
117120

118121
nodeId : String → Fin numberOfParties
119122
nodeId s with S.readMaybe 10 (S.fromList (drop (S.length nodePrefix) $ S.toList s))
120-
... | nothing = error ("Unknown node: " S.++ s)
123+
... | nothing = error ("Unknown node: " ◇ s)
121124
... | just n = from-id n
122125

123126
open FunTot (completeFin numberOfParties) (maximalFin numberOfParties)
@@ -130,7 +133,7 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String
130133
(no _) → error "Expected total map"
131134

132135
to-nodeId : ℕ → String
133-
to-nodeId n = nodePrefix S.++ show n
136+
to-nodeId n = nodePrefix ◇ show n
134137

135138
SUT : String
136139
SUT = to-nodeId sutId
@@ -190,20 +193,35 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String
190193

191194
record State : Type where
192195
field refs : AssocList String Blk
193-
ib-lottery : List ℕ
194-
eb-lottery : List ℕ
195-
vt-lottery : List ℕ
196196

197197
instance
198198
hhx : Hashable InputBlock (List ℕ)
199199
hhx .hash record { header = h } = hash h
200200

201+
_ = Show-List
202+
_ = Show-×
203+
204+
unquoteDecl Show-IBHeaderOSig Show-IBBody Show-InputBlock = derive-Show $
205+
(quote IBHeaderOSig , Show-IBHeaderOSig)
206+
∷ (quote IBBody , Show-IBBody)
207+
∷ (quote InputBlock , Show-InputBlock)
208+
∷ []
209+
210+
unquoteDecl Show-EndorserBlockOSig = derive-Show [ (quote EndorserBlockOSig , Show-EndorserBlockOSig) ]
211+
unquoteDecl Show-Blk = derive-Show [ (quote Blk , Show-Blk) ]
212+
213+
del : String
214+
del = ", "
215+
216+
nl : String
217+
nl = "\n"
218+
201219
blockRefToNat : AssocList String Blk → String → IBRef
202220
blockRefToNat refs r with refs ⁉ r
203221
... | just (IB-Blk ib) = hash ib
204-
... | just (EB-Blk _) = error "IB expected"
205-
... | just (VT-Blk _) = error "IB expected"
206-
... | nothing = error "IB expected"
222+
... | just (EB-Blk eb) = error $ "IB expected, got EB instead, " ◇ show eb
223+
... | just (VT-Blk vt) = error $ "IB expected, got VT instead"
224+
... | nothing = error $ "IB expected, got nothing (" ◇ r ◇ " / " ◇ show refs ◇ ")"
207225

208226
open State
209227

@@ -246,35 +264,44 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String
246264
traceEvent→action l record { message = EBEnteredState _ _ _ } = l , []
247265
traceEvent→action l record { message = VTBundleEnteredState _ _ _ } = l , []
248266
traceEvent→action l record { message = RBEnteredState _ _ _ } = l , []
249-
traceEvent→action l record { message = IBGenerated p i s _ _ _ _}
250-
with p ≟ SUT
251-
... | yes _ = record l { ib-lottery = (primWord64ToNat s) ∷ ib-lottery l } , (inj₁ (IB-Role-Action (primWord64ToNat s) , SLOT)) ∷ []
252-
... | no _ = let ib = record { header =
253-
record { slotNumber = primWord64ToNat s
254-
; producerID = nodeId p
255-
; lotteryPf = tt
256-
; bodyHash = [] -- TODO: txs
257-
; signature = tt
258-
}
259-
; body = record { txs = [] } } -- TODO: add transactions
260-
in record l { refs = (i , IB-Blk ib) ∷ refs l } , []
261-
traceEvent→action l record { message = EBGenerated p i s _ _ ibs }
262-
with p ≟ SUT
263-
... | yes _ = l , (inj₁ (EB-Role-Action (primWord64ToNat s) [] , SLOT)) ∷ []
264-
... | no _ = let eb = record
265-
{ slotNumber = primWord64ToNat s
266-
; producerID = nodeId p
267-
; lotteryPf = tt
268-
; ibRefs = map (blockRefToNat (refs l) ∘ BlockRef.id) ibs
269-
; ebRefs = []
270-
; signature = tt
271-
}
272-
in record l { refs = (i , EB-Blk eb) ∷ refs l } , []
273-
traceEvent→action l record { message = VTBundleGenerated p i s _ _ vts }
274-
with p ≟ SUT
275-
... | yes _ = l , (inj₁ (VT-Role-Action (primWord64ToNat s) , SLOT)) ∷ []
276-
... | no _ = let vt = map (const tt) (elems vts)
277-
in record l { refs = (i , VT-Blk vt) ∷ refs l } , []
267+
traceEvent→action l record { message = IBGenerated p i s _ _ _ _} =
268+
let ib = record { header =
269+
record { slotNumber = primWord64ToNat s
270+
; producerID = nodeId p
271+
; lotteryPf = tt
272+
; bodyHash = [] -- TODO: txs
273+
; signature = tt
274+
}
275+
; body = record { txs = [] } } -- TODO: add transactions
276+
in record l { refs = (i , IB-Blk ib) ∷ refs l } , actions
277+
where
278+
actions : List (Action × LeiosInput ⊎ FFDUpdate)
279+
actions with p ≟ SUT
280+
... | yes _ = (inj₁ (IB-Role-Action (primWord64ToNat s) , SLOT)) ∷ []
281+
... | no _ = []
282+
traceEvent→action l record { message = EBGenerated p i s _ _ ibs } =
283+
let eb = record
284+
{ slotNumber = primWord64ToNat s
285+
; producerID = nodeId p
286+
; lotteryPf = tt
287+
; ibRefs = map (blockRefToNat (refs l) ∘ BlockRef.id) ibs
288+
; ebRefs = []
289+
; signature = tt
290+
}
291+
in record l { refs = (i , EB-Blk eb) ∷ refs l } , actions
292+
where
293+
actions : List (Action × LeiosInput ⊎ FFDUpdate)
294+
actions with p ≟ SUT
295+
... | yes _ = (inj₁ (EB-Role-Action (primWord64ToNat s) [] , SLOT)) ∷ []
296+
... | no _ = []
297+
traceEvent→action l record { message = VTBundleGenerated p i s _ _ vts } =
298+
let vt = map (const tt) (elems vts)
299+
in record l { refs = (i , VT-Blk vt) ∷ refs l } , actions
300+
where
301+
actions : List (Action × LeiosInput ⊎ FFDUpdate)
302+
actions with p ≟ SUT
303+
... | yes _ = (inj₁ (VT-Role-Action (primWord64ToNat s) , SLOT)) ∷ []
304+
... | no _ = []
278305
traceEvent→action l record { message = RBGenerated _ _ _ _ _ _ _ _ } = l , []
279306

280307
mapAccuml : {A B S : Set} → (S → A → S × B) → S → List A → S × List B
@@ -284,45 +311,70 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String
284311
(s'' , ys) = mapAccuml f s' xs
285312
in s'' , y ∷ ys
286313

287-
result : ∀ {E A : Type} → (f : A → String) → (g : E → String) → Result E A → String
314+
result : ∀ {E A S : Type} → (f : A → S) → (g : E → S) → Result E A → S
288315
result f g (Ok x) = f x
289316
result f g (Err x) = g x
290317

318+
{-
319+
unquoteDecl Show-FFDBuffers = derive-Show [ (quote FFDBuffers , Show-FFDBuffers) ]
320+
unquoteDecl Show-Action = derive-Show [ (quote Action , Show-Action) ]
321+
-}
322+
291323
instance
292-
Show-EndorserBlock : Show EndorserBlock
293-
Show-EndorserBlock .show _ = "EndorserBlock"
324+
Show-FFDBuffers : Show FFDBuffers
325+
Show-FFDBuffers .show _ = "ffd buffers"
294326

295327
Show-Action : Show Action
296-
Show-Action .show (IB-Role-Action x) = "IB-Role-Action " S.++ show x
297-
Show-Action .show (EB-Role-Action x _) = "EB-Role-Action " S.++ show x
298-
Show-Action .show (VT-Role-Action x) = "VT-Role-Action " S.++ show x
299-
Show-Action .show (No-IB-Role-Action x) = "No-IB-Role-Action " S.++ show x
300-
Show-Action .show (No-EB-Role-Action x) = "No-EB-Role-Action " S.++ show x
301-
Show-Action .show (No-VT-Role-Action x) = "No-VT-Role-Action " S.++ show x
302-
Show-Action .show (Ftch-Action x) = "Ftch-Action " S.++ show x
303-
Show-Action .show (Slot-Action x) = "Slot-Action " S.++ show x
304-
Show-Action .show (Base₁-Action x) = "Base₁-Action " S.++ show x
305-
Show-Action .show (Base₂a-Action x _) = "Base₂a-Action " S.++ show x
306-
Show-Action .show (Base₂b-Action x) = "Base₂b-Action " S.++ show x
307-
308-
Show-Update : Show FFDUpdate
309-
Show-Update .show (IB-Recv-Update _) = "IB-Recv-Update"
310-
Show-Update .show (EB-Recv-Update _) = "EB-Recv-Update"
311-
Show-Update .show (VT-Recv-Update _) = "VT-Recv-Update"
328+
Show-Action .show (IB-Role-Action x) = "IB-Role-Action " ◇ show x
329+
Show-Action .show (EB-Role-Action x _) = "EB-Role-Action " ◇ show x
330+
Show-Action .show (VT-Role-Action x) = "VT-Role-Action " ◇ show x
331+
Show-Action .show (No-IB-Role-Action x) = "No-IB-Role-Action " ◇ show x
332+
Show-Action .show (No-EB-Role-Action x) = "No-EB-Role-Action " ◇ show x
333+
Show-Action .show (No-VT-Role-Action x) = "No-VT-Role-Action " ◇ show x
334+
Show-Action .show (Ftch-Action x) = "Ftch-Action " ◇ show x
335+
Show-Action .show (Slot-Action x) = "Slot-Action " ◇ show x
336+
Show-Action .show (Base₁-Action x) = "Base₁-Action " ◇ show x
337+
Show-Action .show (Base₂a-Action x _) = "Base₂a-Action " ◇ show x
338+
Show-Action .show (Base₂b-Action x) = "Base₂b-Action " ◇ show x
339+
340+
instance
341+
Show-NonZero : ∀ {n : ℕ} → Show (NonZero n)
342+
Show-NonZero .show record { nonZero = _ } = "NonZero"
343+
344+
Show-SD : ∀ {n : ℕ} → Show (TotalMap (Fin n) ℕ)
345+
Show-SD .show _ = "stake distribution"
346+
347+
unquoteDecl Show-BlockType = derive-Show [ (quote BlockType , Show-BlockType) ]
348+
349+
instance
350+
Show-sum : Show (EndorserBlock ⊎ List Tx)
351+
Show-sum .show (inj₁ x) = show x
352+
Show-sum .show (inj₂ y) = show y
353+
354+
unquoteDecl Show-FFDUpdate = derive-Show [ (quote FFDUpdate , Show-FFDUpdate) ]
355+
unquoteDecl Show-Params = derive-Show [ (quote Params , Show-Params) ]
356+
unquoteDecl Show-Upkeep = derive-Show [ (quote SlotUpkeep , Show-Upkeep) ]
357+
unquoteDecl Show-Upkeep-Stage = derive-Show [ (quote StageUpkeep , Show-Upkeep-Stage) ]
358+
unquoteDecl Show-LeiosState = derive-Show [ (quote LeiosState , Show-LeiosState) ]
359+
unquoteDecl Show-LeiosInput = derive-Show [ (quote LeiosInput , Show-LeiosInput) ]
312360

313361
s₀ : LeiosState
314362
s₀ = initLeiosState tt sd tt ((SUT-id , tt) ∷ [])
315363

316-
format-Err-verifyAction : ∀ {α i s} → Err-verifyAction α i s → String
317-
format-Err-verifyAction {α} (E-Err e) = "Invalid Action: Slot " S.++ show α
364+
format-Err-verifyAction : ∀ {α i s} → Err-verifyAction α i s → Pair String String
365+
format-Err-verifyAction {α} {i} {s} (E-Err e) =
366+
"Invalid Action: Slot " ◇ show α ,
367+
"Parameters: " ◇ show params ◇ nl ◇
368+
"Input: " ◇ show i ◇ nl ◇
369+
"LeiosState: " ◇ show s
318370

319-
format-Err-verifyUpdate : ∀ {μ s} → Err-verifyUpdate μ s → String
320-
format-Err-verifyUpdate {μ} (E-Err _) = "Invalid Update: " S.++ show μ
371+
format-Err-verifyUpdate : ∀ {μ s} → Err-verifyUpdate μ s → Pair String String
372+
format-Err-verifyUpdate {μ} (E-Err _) = "Invalid Update" , show μ
321373

322-
format-error : ∀ {αs s} → Err-verifyTrace αs s → String
323-
format-error {inj₁ (α , i) ∷ []} {s} (Err-StepOk x) = "error step: " S.++ show α
374+
format-error : ∀ {αs s} → Err-verifyTrace αs s → Pair String String
375+
format-error {inj₁ (α , i) ∷ []} {s} (Err-StepOk x) = "Error step" , show α
324376
format-error {inj₁ (α , i) ∷ αs} {s} (Err-StepOk x) = format-error x
325-
format-error {inj₂ μ ∷ []} {s} (Err-UpdateOk x) = "error update: " S.++ show μ
377+
format-error {inj₂ μ ∷ []} {s} (Err-UpdateOk x) = "Error update" , show μ
326378
format-error {inj₂ μ ∷ αs} {s} (Err-UpdateOk x) = format-error x
327379
format-error {inj₁ (α , i) ∷ []} {s} (Err-Action x) = format-Err-verifyAction x
328380
format-error {inj₁ (α , i) ∷ αs} {s} (Err-Action x) = format-Err-verifyAction x
@@ -332,12 +384,18 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String
332384
opaque
333385
unfolding List-Model
334386

335-
verifyTrace : Pair ℕ String
336-
verifyTrace =
337-
let n₀ = record { refs = [] ; ib-lottery = [] ; eb-lottery = [] ; vt-lottery = [] }
387+
verifyTrace' : LeiosState → Pair ℕ (Pair String String)
388+
verifyTrace' s =
389+
let n₀ = record { refs = [] }
338390
l' = proj₂ $ mapAccuml traceEvent→action n₀ l
339391
αs = L.reverse (L.concat l')
340-
tr = checkTrace αs s₀
341-
in L.length αs , result (λ _ → "ok") format-error tr
392+
tr = checkTrace αs s
393+
in L.length αs , result (λ _ → ("ok" , "")) format-error tr
342394

395+
verifyTrace : Pair ℕ (Pair String String)
396+
verifyTrace = verifyTrace' s₀
343397
{-# COMPILE GHC verifyTrace as verifyTrace #-}
398+
399+
verifyTraceFromSlot : ℕ → Pair ℕ (Pair String String)
400+
verifyTraceFromSlot n = verifyTrace' (record s₀ { slot = n })
401+
{-# COMPILE GHC verifyTraceFromSlot as verifyTraceFromSlot #-}

‎leios-trace-verifier/examples/valid/agda-1.jsonl‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
# Test 1 from Agda: https://github.com/input-output-hk/ouroboros-leios-formal-spec/blob/9741f8a27a55d562b33d0b4ac4f9334fc9fba9e0/formal-spec/Leios/Short/Trace/Verifier/Test.agda#L37
22
#
33
# inj₁ (Slot-Action 0 , SLOT) ∷ inj₁ (Base₂b-Action 0 , SLOT) ∷ []
4+
{"message":{"node":"node-0","slot":0,"type":"NoIBGenerated"},"time_s":0}
45
{"message":{"node":"node-0","slot":0,"type":"Slot"},"time_s":0.04}

‎leios-trace-verifier/examples/valid/agda-2.jsonl‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,15 @@
33
# -- slot 0
44
# inj₁ (Base₂b-Action 0 , SLOT)
55
# ∷ inj₁ (Slot-Action 0 , SLOT)
6+
{"message":{"slot":0,"type":"NoIBGenerated","node":"node-0"},"time_s":0.01}
67
{"message":{"slot":0,"type":"Slot","node":"node-0"},"time_s":0.01}
78
#
89
# -- slot 1
910
# ∷ inj₁ (IB-Role-Action 1 , SLOT)
1011
{"message":{"slot":1,"type":"IBGenerated","producer":"node-0","id":"0-1","rb_ref":"genesis","pipeline":0,"size_bytes":98608,"tx_payload_bytes":98304},"time_s":1.01}
1112
#
1213
# ∷ inj₁ (VT-Role-Action 1 , SLOT)
13-
{"message":{"slot":1,"type":"VTBundleGenerated","producer":"node-0","id":"0-1","votes":{},"pipeline":0,"size_bytes":105},"time_s":1.02}
14+
#{"message":{"slot":1,"type":"VTBundleGenerated","producer":"node-0","id":"0-1","votes":{},"pipeline":0,"size_bytes":105},"time_s":1.02}
1415
#
1516
# Create an RB for later referencing by the SUT.
1617
{"message":{"slot":1,"type":"RBGenerated","producer":"node-1","id":"-7674734470404649268","endorsement":null,"parent":null,"size_bytes":1025,"tx_payload_bytes":0},"time_s":1.03}
@@ -41,10 +42,10 @@
4142
{"message":{"type":"RBReceived","recipient":"node-0","id":"-7674734470404649268"},"time_s":2.03}
4243
#
4344
# ∷ inj₁ (EB-Role-Action 2 [] , SLOT)
44-
{"message":{"slot":2,"type":"EBGenerated","producer":"node-0","id":"0-2","input_blocks":[],"pipeline":0,"size_bytes":1616},"time_s":2.04}
45+
#{"message":{"slot":2,"type":"EBGenerated","producer":"node-0","id":"0-2","input_blocks":[],"pipeline":0,"size_bytes":1616},"time_s":2.04}
4546
#
4647
# ∷ inj₁ (VT-Role-Action 2 , SLOT)
47-
{"message":{"slot":2,"type":"VTBundleGenerated","producer":"node-0","id":"0-2","votes":{},"pipeline":0,"size_bytes":105},"time_s":2.05}
48+
#{"message":{"slot":2,"type":"VTBundleGenerated","producer":"node-0","id":"0-2","votes":{},"pipeline":0,"size_bytes":105},"time_s":2.05}
4849
#
4950
# ∷ inj₁ (Base₂b-Action 2 , SLOT)
5051
# ∷ inj₁ (Slot-Action 2 , SLOT)
@@ -80,10 +81,10 @@
8081
{"message":{"slot":4,"type":"IBGenerated","producer":"node-0","id":"0-4","rb_ref":"-7674734470404649268","pipeline":0,"size_bytes":98608,"tx_payload_bytes":98304},"time_s":4.01}
8182
#
8283
# ∷ inj₁ (EB-Role-Action 4 [] , SLOT)
83-
{"message":{"slot":4,"type":"EBGenerated","producer":"node-0","id":"0-4","input_blocks":[],"pipeline":0,"size_bytes":1616},"time_s":4.02}
84+
#{"message":{"slot":4,"type":"EBGenerated","producer":"node-0","id":"0-4","input_blocks":[],"pipeline":0,"size_bytes":1616},"time_s":4.02}
8485
#
8586
# ∷ inj₁ (VT-Role-Action 4 , SLOT)
86-
{"message":{"slot":4,"type":"VTBundleGenerated","producer":"node-0","id":"0-4","votes":{},"pipeline":0,"size_bytes":105},"time_s":4.03}
87+
#{"message":{"slot":4,"type":"VTBundleGenerated","producer":"node-0","id":"0-4","votes":{},"pipeline":0,"size_bytes":105},"time_s":4.03}
8788
#
8889
# ∷ inj₁ (Base₂b-Action 4 , SLOT)
8990
# ∷ inj₁ (Slot-Action 4 , SLOT)

‎leios-trace-verifier/hs-src/app/Main.hs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,9 +34,10 @@ main =
3434
. decodeJSONL
3535
<$> BSL.readFile logFile
3636
hPutStrLn stderr $ "Applying " <> show (fst result) <> " actions"
37-
unless (snd result == "ok") $
37+
unless (fst (snd result) == "ok") $
3838
do
39-
putStrLn . T.unpack $ snd result
39+
putStrLn . T.unpack $ fst (snd result)
40+
putStrLn . T.unpack $ snd (snd result)
4041
exitFailure
4142

4243
data Command = Command

0 commit comments

Comments
 (0)