l for log, not t for trace

mit-plv · Apr 5, 2024 · 2173acf · 2173acf
1 parent 53de382
commit 2173acf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Bedrock/End2End/X25519/GarageDoorTop.v b/src/Bedrock/End2End/X25519/GarageDoorTop.v
@@ -172,7 +172,7 @@ Definition only_mmio_satisfying P t :=
 Local Notation labeled_transitions := stateful.
 Local Notation boot_seq := BootSeq.
 
-Definition protocol_spec t := exists s s', labeled_transitions protocol_step s s' t.
+Definition protocol_spec l := exists s s', labeled_transitions protocol_step s s' l.
 Definition io_spec : list LogItem -> Prop := only_mmio_satisfying (boot_seq +++ protocol_spec).
 
 Import ExprImpEventLoopSpec.