Merge branch 'twal/no_label_injectivity' into twal/has_usage

REPROSEC · Oct 15, 2024 · 5108ef4 · 5108ef4
2 parents 9e216c3 + e27024b
commit 5108ef4
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 6 deletions.
diff --git a/src/core/DY.Core.Label.fst b/src/core/DY.Core.Label.fst
@@ -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 `public` 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);

diff --git a/src/core/DY.Core.Trace.Base.fst b/src/core/DY.Core.Trace.Base.fst
@@ -329,17 +329,22 @@ let rec fmap_trace f tr =
   | Snoc init last ->
     Snoc (fmap_trace f init) (fmap_trace_event f last)
 
-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
 
 val fmap_trace_identity:
   #a:Type ->