Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions data/simulation/trace.shared.d.ts
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,7 @@ interface GeneratedEndorserBlock extends GeneratedBlockEvent {
id: string;
pipeline: number;
input_blocks: BlockRef[];
endorser_blocks: BlockRef[];
}

interface GeneratedVote extends GeneratedBlockEvent {
Expand Down
7 changes: 7 additions & 0 deletions data/simulation/trace.shared.schema.json
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,12 @@
},
"type": "array"
},
"endorser_blocks": {
"items": {
"$ref": "#/definitions/BlockRef"
},
"type": "array"
},
"pipeline": {
"type": "number"
},
Expand All @@ -127,6 +133,7 @@
"required": [
"id",
"input_blocks",
"endorser_blocks",
"pipeline",
"producer",
"size_bytes",
Expand Down
1 change: 1 addition & 0 deletions leios-trace-hs/src/LeiosEvents.hs
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,7 @@ data Event where
, pipeline :: !PipelineNo
, bytes :: !Word64
, input_blocks :: ![BlockRef]
, endorser_blocks :: ![BlockRef]
} ->
Event
RBGenerated ::
Expand Down
8 changes: 4 additions & 4 deletions leios-trace-verifier/Parser.agda
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@ data Event : Type where
RBReceived : Maybe Node → Node → Maybe Bytes → Maybe Time → String → Maybe (List String) → Event
IBEnteredState EBEnteredState VTBundleEnteredState RBEnteredState : String → String → Word64 → Event
IBGenerated : String → String → SlotNo → PipelineNo → Bytes → Bytes → Maybe String → Event
EBGenerated : String → String → Word64 → PipelineNo → Word64 → List BlockRef → Event
EBGenerated : String → String → Word64 → PipelineNo → Word64 → List BlockRef → List BlockRef → Event
RBGenerated : String → String → Word64 → Word64 → Nullable Endorsement → Maybe (List Endorsement) → Word64 → Nullable BlockRef → Event
VTBundleGenerated : String → String → Word64 → PipelineNo → Word64 → Map String Word64 → Event

Expand Down Expand Up @@ -160,7 +160,7 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String
with p ≟ SUT
... | yes _ = just (IB , primWord64ToNat s)
... | no _ = nothing
winningSlot record { message = EBGenerated p _ s _ _ _ }
winningSlot record { message = EBGenerated p _ s _ _ _ _ }
with p ≟ SUT
... | yes _ = just (EB , primWord64ToNat s)
... | no _ = nothing
Expand Down Expand Up @@ -279,13 +279,13 @@ module _ (numberOfParties : ℕ) (sutId : ℕ) (stakeDistr : List (Pair String
actions with p ≟ SUT
... | yes _ = (inj₁ (IB-Role-Action (primWord64ToNat s) , SLOT)) ∷ []
... | no _ = []
traceEvent→action l record { message = EBGenerated p i s _ _ ibs } =
traceEvent→action l record { message = EBGenerated p i s _ _ ibs ebs } =
let eb = record
{ slotNumber = primWord64ToNat s
; producerID = nodeId p
; lotteryPf = tt
; ibRefs = map (blockRefToNat (refs l) ∘ BlockRef.id) ibs
; ebRefs = []
; ebRefs = map (blockRefToNat (refs l) ∘ BlockRef.id) ebs
; signature = tt
}
in record l { refs = (i , EB-Blk eb) ∷ refs l } , actions
Expand Down
2 changes: 1 addition & 1 deletion leios-trace-verifier/examples/valid/agda-2.jsonl
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@
{"message":{"slot":8,"type":"IBGenerated","producer":"node-0","id":"0-8","rb_ref":"-7674734470404649268","pipeline":0,"size_bytes":98608,"tx_payload_bytes":98304},"time_s":8.01}
#
# ∷ inj₁ (EB-Role-Action 8 ((3 ∷ 4 ∷ 5 ∷ []) ∷ []) , SLOT)
{"message":{"slot":8,"type":"EBGenerated","producer":"node-0","id":"0-8","input_blocks":[],"pipeline":0,"size_bytes":1616},"time_s":8.02}
{"message":{"slot":8,"type":"EBGenerated","producer":"node-0","id":"0-8","input_blocks":[],"endorser_blocks":[],"pipeline":0,"size_bytes":1616},"time_s":8.02}
#
# ∷ inj₁ (VT-Role-Action 8 , SLOT)
{"message":{"slot":8,"type":"VTBundleGenerated","producer":"node-0","id":"0-8","votes":{},"pipeline":0,"size_bytes":105},"time_s":8.03}
Expand Down
1 change: 1 addition & 0 deletions leios-trace-verifier/hs-src/test/Spec/Transition.hs
Original file line number Diff line number Diff line change
Expand Up @@ -214,6 +214,7 @@ transition GenerateEB =
pipeline <- uses stageLength $ (slot `div`) . fromIntegral
bytes <- lift arbitrary
input_blocks <- lift . sublistOf =<< uses ibs (fmap BlockRef . S.toList)
endorser_blocks <- lift . sublistOf =<< uses ebs (fmap BlockRef . S.toList)
pure [EBGenerated{..}]
transition ReceiveEB =
do
Expand Down
1 change: 1 addition & 0 deletions simulation/src/LeiosProtocol/Short/Sim.hs
Original file line number Diff line number Diff line change
Expand Up @@ -355,6 +355,7 @@ sharedEvent leios nodeNames e = case e of
Shared.EBGenerated
{ bytes = fromIntegral (messageSizeBytes eb)
, input_blocks = map (Shared.BlockRef . T.pack . mkStringId) eb.inputBlocks
, endorser_blocks = map (Shared.BlockRef . T.pack . mkStringId) eb.endorseBlocksEarlierPipeline
, pipeline = coerce $ endorseBlockPipeline leios eb
, ..
}
Expand Down