Merge branch 'main' into twal/more_trace_

src/core/DY.Core.Label.fst

@@ -110,7 +110,7 @@ val is_corrupt_later:
   [SMTPat (is_corrupt tr1 l); SMTPat (tr1 <$ tr2)]
 let is_corrupt_later tr1 tr2 l =
   reveal_opaque (`%is_corrupt) (is_corrupt);
-  fmap_trace_later (forget_label ()) tr1 tr2;
+  fmap_trace_later forget_label tr1 tr2;
   label_is_corrupt_later l (trace_forget_labels tr1) (trace_forget_labels tr2)
 
 /// A label `l1` can flow to a label `l2` when `l2` will always be more secret than `l1` in the future,
@@ -133,12 +133,12 @@ let intro_label_equal l1 l2 pf =
   reveal_opaque (`%can_flow) can_flow;
   reveal_opaque (`%is_corrupt) is_corrupt;
   introduce forall tr. l1.is_corrupt tr == l2.is_corrupt tr with (
-    pf (fmap_trace (forget_label unknown_label) tr);
+    pf (fmap_trace (replace_label unknown_label) tr);
     // These two lines prove surjectivity of `trace_forget_labels`
     // by showing that fmap_trace (forget_label public) is a right-inverse
     // (we could replace `unknown_label` with anything)
-    fmap_trace_compose (forget_label unknown_label) (forget_label ()) (forget_label ()) tr;
-    fmap_trace_identity (forget_label ()) tr;
+    fmap_trace_compose (replace_label unknown_label) forget_label forget_label tr;
+    fmap_trace_identity forget_label tr;
     FStar.PropositionalExtensionality.apply (l1.is_corrupt tr) (l2.is_corrupt tr)
   );
   assert(l1.is_corrupt `FStar.FunctionalExtensionality.feq` l2.is_corrupt);

src/core/DY.Core.Trace.Base.fst

@@ -551,14 +551,19 @@ let event_exists_fmap_trace #a #b f tr ev =
     event_at_fmap_trace f tr i ev
   )
 
-val forget_label:
+val replace_label:
   #a:Type -> #b:Type ->
   b ->
   a -> b
-let forget_label #a #b x _ = x
+let replace_label #a #b x _ = x
+
+val forget_label:
+  #a:Type ->
+  a -> unit
+let forget_label #a = replace_label ()
 
 val trace_forget_labels:
   trace ->
   trace_ unit
 let trace_forget_labels tr =
-  fmap_trace (forget_label ()) tr
+  fmap_trace forget_label tr