Skip to content

Commit c4dc61a

Browse files
yveshauseryveshauser
authored
Mapping of simulation log to Agda data types (#263)
1 parent e46c617 commit c4dc61a

File tree

6 files changed

+222
-59
lines changed

6 files changed

+222
-59
lines changed

‎flake.lock

+4-4
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎flake.nix

+1-1
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?ref=1bea2eaedf3cc38448a11819f3e2a7ab75b24735";
10+
leios-spec.url = "github:input-output-hk/ouroboros-leios-formal-spec?rev=d5b6b6bc4d1e532c21c215ca9d15ac3f352a6bfb";
1111
};
1212

1313

‎leios-trace-verifier/Parser.agda

+182-43
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,47 @@
1+
open import Prelude.AssocList
2+
3+
open import Leios.Config
14
open import Leios.Prelude hiding (id)
5+
open import Leios.Foreign.Util
6+
7+
open import Data.Bool using (if_then_else_)
8+
import Data.Nat.Show as S
9+
import Data.String as S
10+
open import Agda.Builtin.Word using (Word64; primWord64ToNat)
11+
open import Foreign.Haskell.Pair
212

313
module Parser where
414

515
{-# FOREIGN GHC
616
{-# LANGUAGE OverloadedStrings #-}
717
#-}
818

19+
postulate
20+
Int : Set
21+
Micro : Set
22+
Map : Set → Set → Set
23+
elems : ∀ {k v} → Map k v → List v
24+
trunc : Micro → ℕ
25+
926
{-# FOREIGN GHC
1027
import Data.Word
1128
import Data.Fixed
12-
import Data.Map
29+
import qualified Data.Map as M
1330
import qualified Data.ByteString.Lazy.Char8 as BSL8
1431
import LeiosEvents
15-
#-}
1632
17-
postulate
18-
Int : Set
19-
Word64 : Set
20-
Micro : Set
21-
Map : Set → Set → Set
33+
elems' :: () -> () -> M.Map k v -> [v]
34+
elems' _ _ = M.elems
35+
36+
trunc' :: Micro -> Integer
37+
trunc' = floor
38+
#-}
2239

23-
{-# COMPILE GHC Word64 = type Data.Word.Word64 #-}
2440
{-# COMPILE GHC Micro = type Data.Fixed.Micro #-}
25-
{-# COMPILE GHC Map = type Data.Map.Map #-}
41+
{-# COMPILE GHC Map = type M.Map #-}
2642
{-# COMPILE GHC Int = type Int #-}
43+
{-# COMPILE GHC elems = elems' #-}
44+
{-# COMPILE GHC trunc = trunc' #-}
2745

2846
Bytes = Word64
2947
SlotNo = Word64
@@ -57,7 +75,7 @@ data Event : Type where
5775
IBEnteredState EBEnteredState VTBundleEnteredState RBEnteredState : String → String → Word64 → Event
5876
IBGenerated : String → String → SlotNo → Maybe Bytes → Maybe Bytes → Maybe String → Event
5977
EBGenerated : String → String → Word64 → Word64 → List BlockRef → Event
60-
RBGenerated : String → Maybe String → Maybe Int → Word64 → Maybe Word64 → Maybe Endorsement → Maybe (List Endorsement) → Maybe Word64 → Event
78+
RBGenerated : String → Maybe String → Maybe Int → Word64 → Maybe Word64 → Maybe Endorsement → Maybe (List Endorsement) → Maybe Word64 → Maybe BlockRef → Event
6179
VTBundleGenerated : String → String → Word64 → Word64 → Map String Word64 → Event
6280

6381
{-# COMPILE GHC Event = data Event (Cpu | IBSent | EBSent | VTBundleSent | RBSent | IBReceived | EBReceived | VTBundleReceived | RBReceived
@@ -69,36 +87,157 @@ record TraceEvent : Type where
6987

7088
{-# COMPILE GHC TraceEvent = data TraceEvent (TraceEvent) #-}
7189

72-
open import Leios.SpecStructure using (SpecStructure)
73-
open import Leios.Trace.Verifier
74-
75-
open import Leios.Defaults 2 fzero using (st)
76-
open import Leios.Short st
77-
78-
EventLog = List TraceEvent
79-
80-
traceEvent→action : TraceEvent → Maybe (Action × LeiosInput)
81-
traceEvent→action record { message = Cpu x x₁ x₂ } = nothing
82-
traceEvent→action record { message = IBSent x x₁ x₂ x₃ x₄ x₅ } = nothing
83-
traceEvent→action record { message = EBSent x x₁ x₂ x₃ x₄ x₅ } = nothing
84-
traceEvent→action record { message = VTBundleSent x x₁ x₂ x₃ x₄ x₅ } = nothing
85-
traceEvent→action record { message = RBSent x x₁ x₂ x₃ x₄ x₅ } = nothing
86-
traceEvent→action record { message = IBReceived x x₁ x₂ x₃ x₄ x₅ } = nothing
87-
traceEvent→action record { message = EBReceived x x₁ x₂ x₃ x₄ x₅ } = nothing
88-
traceEvent→action record { message = VTBundleReceived x x₁ x₂ x₃ x₄ x₅ } = nothing
89-
traceEvent→action record { message = RBReceived x x₁ x₂ x₃ x₄ x₅ } = nothing
90-
traceEvent→action record { message = IBEnteredState x x₁ x₂ } = nothing
91-
traceEvent→action record { message = EBEnteredState x x₁ x₂ } = nothing
92-
traceEvent→action record { message = VTBundleEnteredState x x₁ x₂ } = nothing
93-
traceEvent→action record { message = RBEnteredState x x₁ x₂ } = nothing
94-
traceEvent→action record { message = IBGenerated p _ s _ _ _ } = just (IB-Role-Action , SLOT)
95-
traceEvent→action record { message = EBGenerated p _ s _ ibs } = just (EB-Role-Action , SLOT)
96-
traceEvent→action record { message = RBGenerated x x₁ x₂ x₃ x₄ x₅ x₆ x₇ } = nothing
97-
traceEvent→action record { message = VTBundleGenerated x x₁ x₂ x₃ x₄ } = just (V-Role-Action , SLOT)
98-
99-
verifyTrace : EventLog → Bool
100-
verifyTrace l =
101-
let αs = L.catMaybes $ L.map traceEvent→action l
102-
in ¿ ValidTrace αs ¿ᵇ
103-
104-
{-# COMPILE GHC verifyTrace as verifyTrace #-}
90+
module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String ℕ)) (sl : ℕ) where
91+
92+
from-id : ℕ → Fin numberOfParties
93+
from-id n =
94+
case n <? numberOfParties of λ where
95+
(yes p) → #_ n {numberOfParties} {fromWitness p}
96+
(no _) → error "Conversion to Fin not possible!"
97+
98+
nodePrefix : String
99+
nodePrefix = "node-"
100+
101+
SUT-id : Fin numberOfParties
102+
SUT-id = from-id sutId
103+
104+
instance
105+
sl-NonZero : NonZero sl
106+
sl-NonZero with sl ≟ 0
107+
... | yes _ = error "Stage length is 0"
108+
... | no ¬p = ≢-nonZero ¬p
109+
110+
nodeId : String → Fin numberOfParties
111+
nodeId s with S.readMaybe 10 (S.fromList (drop (S.length nodePrefix) $ S.toList s))
112+
... | nothing = error ("Unknown node: " S.++ s)
113+
... | just n = from-id n
114+
115+
open FunTot (completeFin numberOfParties) (maximalFin numberOfParties)
116+
117+
sd : TotalMap (Fin numberOfParties) ℕ
118+
sd =
119+
let (r , l) = fromListᵐ (L.map (λ (x , y) → (nodeId x , y)) stakeDistr)
120+
in case (¿ total r ¿) of λ where
121+
(yes p) → record { rel = r ; left-unique-rel = l ; total-rel = p }
122+
(no _) → error "Expected total map"
123+
124+
params : Params
125+
params =
126+
record
127+
{ numberOfParties = numberOfParties
128+
; sutId = SUT-id
129+
; stakeDistribution = sd
130+
; stageLength = sl
131+
}
132+
133+
open import Leios.Short.Trace.Verifier params
134+
135+
to-nodeId : ℕ → String
136+
to-nodeId n = nodePrefix S.++ show n
137+
138+
SUT : String
139+
SUT = to-nodeId sutId
140+
141+
EventLog = List TraceEvent
142+
143+
data Blk : Type where
144+
IB-Blk : InputBlock → Blk
145+
EB-Blk : EndorserBlock → Blk
146+
VT-Blk : List Vote → Blk
147+
148+
record State : Type where
149+
field refs : AssocList String Blk
150+
currentSlot : ℕ
151+
152+
instance
153+
hhx : Hashable InputBlock (List ℕ)
154+
hhx .hash record { header = h } = hash h
155+
156+
blockRefToNat : AssocList String Blk → String → IBRef
157+
blockRefToNat refs r with refs ⁉ r
158+
... | just (IB-Blk ib) = hash ib
159+
... | just (EB-Blk _) = error "IB expected"
160+
... | just (VT-Blk _) = error "IB expected"
161+
... | nothing = error "IB expected"
162+
163+
open State
164+
165+
traceEvent→action : State → TraceEvent → State × List ((Action × LeiosInput) ⊎ FFDUpdate)
166+
traceEvent→action l record { message = Cpu _ _ _ ; time_s = t }
167+
with trunc t ≟ suc (currentSlot l)
168+
... | yes p =
169+
record l { currentSlot = suc (currentSlot l) }
170+
, (inj₁ (Base₂b-Action , SLOT)) ∷ (inj₁ (Slot-Action (currentSlot l) , SLOT)) ∷ []
171+
... | no _ = l , []
172+
traceEvent→action l record { message = IBSent _ _ _ _ _ _ } = l , []
173+
traceEvent→action l record { message = EBSent _ _ _ _ _ _ } = l , []
174+
traceEvent→action l record { message = VTBundleSent _ _ _ _ _ _ } = l , []
175+
traceEvent→action l record { message = RBSent _ _ _ _ _ _ } = l , []
176+
traceEvent→action l record { message = IBReceived _ p _ _ (just i) _ }
177+
with p ≟ SUT | refs l ⁉ i
178+
... | yes _ | just (IB-Blk ib) = l , inj₂ (IB-Recv-Update ib) ∷ []
179+
... | _ | _ = l , []
180+
traceEvent→action l record { message = IBReceived _ _ _ _ nothing _ } = l , []
181+
traceEvent→action l record { message = EBReceived _ p _ _ (just i) _ }
182+
with p ≟ SUT | refs l ⁉ i
183+
... | yes _ | just (EB-Blk eb) = l , inj₂ (EB-Recv-Update eb) ∷ []
184+
... | _ | _ = l , []
185+
traceEvent→action l record { message = EBReceived _ _ _ _ nothing _ } = l , []
186+
traceEvent→action l record { message = VTBundleReceived _ p _ _ (just i) _ }
187+
with p ≟ SUT | refs l ⁉ i
188+
... | yes _ | just (VT-Blk vt) = l , inj₂ (VT-Recv-Update vt) ∷ []
189+
... | _ | _ = l , []
190+
traceEvent→action l record { message = VTBundleReceived _ _ _ _ nothing _ } = l , []
191+
traceEvent→action l record { message = RBReceived _ _ _ _ _ _ } = l , []
192+
traceEvent→action l record { message = IBEnteredState _ _ _ } = l , []
193+
traceEvent→action l record { message = EBEnteredState _ _ _ } = l , []
194+
traceEvent→action l record { message = VTBundleEnteredState _ _ _ } = l , []
195+
traceEvent→action l record { message = RBEnteredState _ _ _ } = l , []
196+
traceEvent→action l record { message = IBGenerated p i s _ _ _ }
197+
with p ≟ SUT
198+
... | yes _ = l , (inj₁ (IB-Role-Action (primWord64ToNat s) , SLOT)) ∷ []
199+
... | no _ = let ib = record { header =
200+
record { slotNumber = primWord64ToNat s
201+
; producerID = nodeId p
202+
; lotteryPf = tt
203+
; bodyHash = [] -- TODO: txs
204+
; signature = tt
205+
}
206+
; body = record { txs = [] } } -- TODO: add transactions
207+
in record l { refs = (i , IB-Blk ib) ∷ refs l } , []
208+
traceEvent→action l record { message = EBGenerated p i s _ ibs }
209+
with p ≟ SUT
210+
... | yes _ = l , (inj₁ (EB-Role-Action (primWord64ToNat s) [] , SLOT)) ∷ []
211+
... | no _ = let eb = record
212+
{ slotNumber = primWord64ToNat s
213+
; producerID = nodeId p
214+
; lotteryPf = tt
215+
; ibRefs = map (blockRefToNat (refs l) ∘ BlockRef.id) ibs
216+
; ebRefs = []
217+
; signature = tt
218+
}
219+
in record l { refs = (i , EB-Blk eb) ∷ refs l } , []
220+
traceEvent→action l record { message = VTBundleGenerated p i s _ vts }
221+
with p ≟ SUT
222+
... | yes _ = l , (inj₁ (VT-Role-Action (primWord64ToNat s) , SLOT)) ∷ []
223+
... | no _ = let vt = map (const tt) (elems vts)
224+
in record l { refs = (i , VT-Blk vt) ∷ refs l } , []
225+
traceEvent→action l record { message = RBGenerated _ _ _ _ _ _ _ _ _ } = l , []
226+
227+
mapAccuml : {A B S : Set} → (S → A → S × B) → S → List A → S × List B
228+
mapAccuml f s [] = s , []
229+
mapAccuml f s (x ∷ xs) =
230+
let (s' , y) = f s x
231+
(s'' , ys) = mapAccuml f s' xs
232+
in s'' , y ∷ ys
233+
234+
opaque
235+
unfolding List-Model
236+
237+
verifyTrace : EventLog → ℕ
238+
verifyTrace l =
239+
let s₀ = record { refs = [] ; currentSlot = 0 }
240+
αs = L.reverse $ L.concat $ proj₂ (mapAccuml traceEvent→action s₀ l)
241+
in if ¿ ValidTrace αs ¿ᵇ then L.length l else 0
242+
243+
{-# COMPILE GHC verifyTrace as verifyTrace #-}

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

+30-8
Original file line numberDiff line numberDiff line change
@@ -1,34 +1,56 @@
1+
{-# LANGUAGE DataKinds #-}
12
{-# LANGUAGE OverloadedStrings #-}
23
{-# LANGUAGE RecordWildCards #-}
34

45
module Main where
56

67
import Data.ByteString.Lazy as BSL
8+
import Data.Map
9+
import Data.Yaml
10+
import LeiosConfig (Config (..))
711
import LeiosEvents
12+
import LeiosTopology (LocationKind (..), Node (..), NodeInfo (..), NodeName (..), Topology (..))
813
import Lib
914
import Options.Applicative
1015

1116
main :: IO ()
1217
main =
1318
do
1419
Command{..} <- execParser commandParser
15-
BSL.readFile logFile >>= print . verifyTrace . decodeJSONL
20+
(top :: Topology CLUSTER) <- decodeFileThrow topologyFile
21+
(config :: Config) <- decodeFileThrow configFile
22+
let nrNodes = toInteger $ Prelude.length (elems $ nodes top)
23+
let nodeNames = Prelude.map unNodeName (keys $ nodes top)
24+
let stakes = Prelude.map (toInteger . stake . nodeInfo) (elems $ nodes top)
25+
let stakeDistribution = Prelude.zip nodeNames stakes
26+
let stageLength = toInteger (leiosStageLengthSlots config)
27+
BSL.readFile logFile
28+
>>= print
29+
. verifyTrace
30+
nrNodes
31+
idSut
32+
stakeDistribution
33+
stageLength
34+
. decodeJSONL
1635

17-
newtype Command = Command
36+
data Command = Command
1837
{ logFile :: FilePath
38+
, configFile :: FilePath
39+
, topologyFile :: FilePath
40+
, idSut :: Integer
1941
}
2042
deriving (Eq, Ord, Read, Show)
2143

2244
commandParser :: ParserInfo Command
2345
commandParser =
2446
info (com <**> helper) $
2547
fullDesc
26-
<> progDesc "Short Leios trace verifier"
27-
<> header "parser - a Short Leios trace verifier"
48+
<> progDesc "Leios trace verifier"
49+
<> header "parser - a Leios trace verifier"
2850
where
2951
com =
3052
Command
31-
<$> strOption
32-
( long "trace-file"
33-
<> help "Short Leios simulation trace log file"
34-
)
53+
<$> strOption (long "trace-file" <> help "Short Leios simulation trace log file")
54+
<*> strOption (long "config-file" <> help "Short Leios configuration file")
55+
<*> strOption (long "topology-file" <> help "Short Leios topology file")
56+
<*> option auto (long "idSut" <> help "Id of system under test (SUT)")

‎leios-trace-verifier/hs-src/trace-parser.cabal

+4-2
Original file line numberDiff line numberDiff line change
@@ -34,12 +34,14 @@ executable parser
3434
build-depends:
3535
, base
3636
, bytestring
37+
, containers
3738
, leios-trace-hs
3839
, trace-parser
3940
, optparse-applicative
41+
, yaml
4042

41-
default-language: Haskell2010
42-
ghc-options: -Wall
43+
default-language: Haskell2010
44+
ghc-options: -Wall
4345

4446
library
4547
import: globalOptions

‎nix/project.nix

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ let
1515
"https://chap.intersectmbo.org/" = inputs.iogx.inputs.CHaP;
1616
};
1717
name = "ouroboros-leios";
18-
compiler-nix-name = lib.mkDefault "ghc98";
18+
compiler-nix-name = lib.mkDefault "ghc982";
1919
# modules = [{ packages = { }; } { packages = { }; } ];
2020
});
2121

0 commit comments

Comments
 (0)