From 20d5ae49ae3560dbfadbfa3484db21ab14ac2496 Mon Sep 17 00:00:00 2001
From: Fabian Hauck <contact@fabianhauck.de>
Date: Wed, 30 Oct 2024 16:29:45 +0100
Subject: [PATCH] cleanup: various cleanups (#83)

- Start trace printing at index 0
- Make EXAMPLE_DIRS in Makefile rewritable
- Use COMPARSE_HOME in .fst.config.json file
---
 .fst.config.json                  | 2 +-
 Makefile                          | 2 +-
 src/lib/utils/DY.Lib.Printing.fst | 8 ++++----
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/.fst.config.json b/.fst.config.json
index ae94312..cc3fcb7 100644
--- a/.fst.config.json
+++ b/.fst.config.json
@@ -1,7 +1,7 @@
 { "fstar_exe":"fstar.exe",
   "options":["--cache_dir", "cache", "--hint_dir", "hints", "--use_hints", "--record_hints"],
   "include_dirs":[
-    "../comparse/src",
+    "${COMPARSE_HOME}/src",
     "src/core",
     "src/lib",
     "src/lib/comparse",
diff --git a/Makefile b/Makefile
index 6dd81cf..589085f 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,7 @@ COMPARSE_HOME 	?= $(DY_HOME)/../comparse
 INNER_SOURCE_DIRS = core lib lib/comparse lib/crypto lib/event lib/hpke lib/state lib/utils
 SOURCE_DIRS = $(addprefix $(DY_HOME)/src/, $(INNER_SOURCE_DIRS))
 INNER_EXAMPLE_DIRS = nsl_pk iso_dh
-EXAMPLE_DIRS = $(addprefix $(DY_HOME)/examples/, $(INNER_EXAMPLE_DIRS))
+EXAMPLE_DIRS ?= $(addprefix $(DY_HOME)/examples/, $(INNER_EXAMPLE_DIRS))
 
 INCLUDE_DIRS = $(SOURCE_DIRS) $(EXAMPLE_DIRS) $(COMPARSE_HOME)/src
 FSTAR_INCLUDE_DIRS = $(addprefix --include , $(INCLUDE_DIRS))
diff --git a/src/lib/utils/DY.Lib.Printing.fst b/src/lib/utils/DY.Lib.Printing.fst
index 609f5f6..a34dc06 100644
--- a/src/lib/utils/DY.Lib.Printing.fst
+++ b/src/lib/utils/DY.Lib.Printing.fst
@@ -194,23 +194,23 @@ let trace_event_to_string printers tr_event i =
   | MsgSent msg -> (
     let msg_str = option_to_string printers.message_to_string msg in
     Printf.sprintf "{\"TraceID\": %d, \"Type\": \"Message\", \"Content\": \"%s\"}\n"
-      i msg_str
+      (i-1) msg_str
   )
   | RandGen usg lab len -> (
     Printf.sprintf "{\"TraceID\": %d, \"Type\": \"Nonce\", \"Usage\": %s}\n" 
-    i (usage_to_string usg)
+      (i-1) (usage_to_string usg)
   )
   | Corrupt time -> ""
   | SetState prin sess_id full_content -> (
     let content_str = state_to_string printers.state_to_string full_content in
     Printf.sprintf "{\"TraceID\": %d, \"Type\": \"Session\", \"SessionID\": %d, \"Principal\": \"%s\", \"Content\": \"%s\"}\n"
-      i sess_id.the_id prin content_str
+      (i-1) sess_id.the_id prin content_str
   )
   | Event prin tag content -> (
     let printer = find_printer printers.event_to_string tag in
     let content_str = option_to_string printer content in
     Printf.sprintf "{\"TraceID\": %d, \"Type\": \"Event\", \"Principal\": \"%s\", \"Tag\": \"%s\", \"Content\": \"%s\"}\n" 
-      i prin tag content_str
+      (i-1) prin tag content_str
   )
 
 /// Helper function for `trace_to_string` to avoid calling `length` for each trace event,