chore: update DY*

Inria-Prosecco · Nov 20, 2024 · 6f93999 · 6f93999
1 parent 99093da
commit 6f93999
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 5 deletions.
diff --git a/flake.lock b/flake.lock
diff --git a/fstar/symbolic/MLS.Symbolic.MyMkRand.fst b/fstar/symbolic/MLS.Symbolic.MyMkRand.fst
@@ -9,7 +9,7 @@ val my_mk_rand: usg:usage -> lab:(bytes -> label) -> len:nat{len <> 0} -> tracef
 let my_mk_rand usg lab len =
   let* time = get_time in
   let result = (Rand len time) in
-  add_event (RandGen usg (lab result) len);*
+  add_entry (RandGen usg (lab result) len);*
   return result
 
 /// Generating a random bytestrings always preserve the trace invariant.
@@ -29,7 +29,7 @@ val my_mk_rand_trace_invariant:
   [SMTPat (my_mk_rand usg lab len tr); SMTPat (trace_invariant tr)]
 let my_mk_rand_trace_invariant #invs usg lab len tr =
   let result = (Rand len (DY.Core.Trace.Base.length tr)) in
-  add_event_invariant (RandGen usg (lab result) len) tr;
+  add_entry_invariant (RandGen usg (lab result) len) tr;
   reveal_opaque (`%my_mk_rand) (my_mk_rand)
 #pop-options