chore: update DY*

Inria-Prosecco · Nov 29, 2024 · 4046566 · 4046566
1 parent ab03f26
commit 4046566
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 7 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
@@ -23,12 +23,11 @@ val my_mk_rand_trace_invariant:
   (ensures (
     let (b, tr_out) = my_mk_rand usg lab len tr in
     trace_invariant tr_out /\
-    1 <= DY.Core.Trace.Base.length tr_out /\
-    rand_generated_at tr_out (DY.Core.Trace.Base.length tr_out - 1) b
+    rand_just_generated tr_out b
   ))
   [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
+  let result = (Rand len (trace_length tr)) in
   add_entry_invariant (RandGen usg (lab result) len) tr;
   reveal_opaque (`%my_mk_rand) (my_mk_rand)
 #pop-options

diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst
@@ -29,7 +29,7 @@ let dy_asp #ci tr = {
     match credential_to_principal cred with
     | None -> False
     | Some who ->
-      token.time <= (DY.Core.Trace.Base.length tr) /\
+      token.time `on_trace` tr /\
       is_signature_key_vk (prefix tr token.time) who vk
   );
   valid_successor = (fun (vk_old, cred_old) (vk_new, cred_new) ->