Comprehensive extraction regression test for Pulse fn interleaving

ExtractPulseFnIface: expanded test covering all interleaving patterns
between .fsti and .fst for DeclToBeDesugared (Pulse fn) declarations:

1. val + let (basic, always worked)
2. fn in .fsti matched by fn in .fst
3. Private helper in .fst before interface fns (skip, not mark private)
4. Out-of-order exposed definitions (fsti: write_and_return, assign_ref;
   fst: assign_ref first, then let write_and_return = assign_ref)
5. let alias in .fst implementing fn in .fsti
6. let definition in .fsti interleaved before fn declarations

Verifies that all 8 functions extract to C with correct visibility:
- private_helper → static (private)
- all interface-exposed fns → public
- function pointer aliases → correct

Also comments out --cmi in mk/test.mk since --cmi is now default in fstar2.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: nikswamy

mk/test.mk

@@ -25,7 +25,7 @@ include $(PULSE_ROOT)/mk/locate.mk
 
 HINTS_ENABLED?=
 
-OTHERFLAGS += --cmi
+# OTHERFLAGS += --cmi  # now default in fstar2
 # This warning is really useless.
 OTHERFLAGS += --warn_error -321
 OTHERFLAGS += --warn_error @247 # couldn't write a checked file? FAIL RIGHT NOW

test/bug-reports/ExtractPulseFnIface.c.expected

@@ -15,3 +15,32 @@ krml_checked_int_t ExtractPulseFnIface_pulse_read_ref(krml_checked_int_t *r)
   return *r;
 }
 
+krml_checked_int_t ExtractPulseFnIface_double(krml_checked_int_t x)
+{
+  return ExtractPulseFnIface_pure_add(x, x);
+}
+
+static void private_helper(krml_checked_int_t *r, krml_checked_int_t v)
+{
+  *r = v;
+}
+
+void ExtractPulseFnIface_pulse_write_ref(krml_checked_int_t *r, krml_checked_int_t v)
+{
+  private_helper(r, v);
+}
+
+krml_checked_int_t ExtractPulseFnIface_assign_ref(krml_checked_int_t *r, krml_checked_int_t v)
+{
+  *r = v;
+  return v;
+}
+
+krml_checked_int_t
+(*ExtractPulseFnIface_write_and_return)(krml_checked_int_t *x0, krml_checked_int_t x1) =
+  ExtractPulseFnIface_assign_ref;
+
+krml_checked_int_t
+(*ExtractPulseFnIface_pulse_read_ref2)(krml_checked_int_t *x0) =
+  ExtractPulseFnIface_pulse_read_ref;
+

test/bug-reports/ExtractPulseFnIface.fst

@@ -5,8 +5,10 @@ open Pulse.Lib.Pervasives
 open Pulse.Lib.Reference
 module R = Pulse.Lib.Reference
 
+// Pattern 1: val + let (basic)
 let pure_add (x y : int) : int = x + y
 
+// Pattern 2: fn matched by fn
 fn pulse_read_ref
   (r: ref int)
   (#v: Ghost.erased int)
@@ -17,3 +19,47 @@ fn pulse_read_ref
   let x = !r;
   x
 }
+
+// Pattern 3: Private helper NOT in .fsti — interleaver must skip past
+// interface entries to avoid marking this as KrmlPrivate erroneously.
+fn private_helper
+  (r: ref int)
+  (v: int)
+  (#old: Ghost.erased int)
+  requires R.pts_to r old
+  ensures R.pts_to r v
+{
+  r := v
+}
+
+// Pattern 3 (continued): exposed fn after private helper
+fn pulse_write_ref
+  (r: ref int)
+  (v: int)
+  (#old: Ghost.erased int)
+  requires R.pts_to r old
+  ensures R.pts_to r v
+{
+  private_helper r v
+}
+
+// Pattern 4: Out-of-order — .fsti has write_and_return BEFORE assign_ref,
+// but .fst defines assign_ref first and write_and_return as an alias.
+// The interleaver must skip past write_and_return in the interface to
+// match assign_ref, then come back for write_and_return.
+fn assign_ref
+  (r: ref int)
+  (v: int)
+  (#old: Ghost.erased int)
+  requires R.pts_to r old
+  returns x: int
+  ensures R.pts_to r v ** pure (x == v)
+{
+  r := v;
+  v
+}
+
+let write_and_return = assign_ref
+
+// Pattern 5: let alias in .fst implementing fn in .fsti
+let pulse_read_ref2 = pulse_read_ref

test/bug-reports/ExtractPulseFnIface.fsti

@@ -1,21 +1,66 @@
 module ExtractPulseFnIface
 #lang-pulse
 
-(** Interface for ExtractPulseFnIface.
-    Tests that a Pulse fn declared in .fsti extracts to C correctly.
-    Regression test: previously, fn declarations in .fsti were not
-    recognized by the interleaver, causing the implementation to be
-    tagged KrmlPrivate and silently dropped by KaRaMeL. *)
+(** Regression test for interleaving DeclToBeDesugared (Pulse fn) in .fsti/.fst.
+    Tests that all patterns extract to C correctly without KrmlPrivate.
+
+    Patterns tested:
+    1. val + let (basic, always worked)
+    2. fn in .fsti + fn in .fst (basic DeclToBeDesugared matching)
+    3. Private helper in .fst before interface fns (skip, not mark private)
+    4. Out-of-order exposed definitions (fsti: write, assign; fst: assign, let write=assign)
+    5. let alias in .fst implementing fn in .fsti
+    6. fn in .fsti with let definitions before fn declarations *)
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Reference
 module R = Pulse.Lib.Reference
 
+// Pattern 1: val + let (basic)
 val pure_add (x y : int) : int
 
+// Pattern 2: fn in .fsti matched by fn in .fst
 fn pulse_read_ref
   (r: ref int)
   (#v: Ghost.erased int)
   requires R.pts_to r v
   returns x: int
   ensures R.pts_to r v ** pure (x == Ghost.reveal v)
+
+// Pattern 6: let definition in .fsti before fn declarations
+let double (x: int) : int = pure_add x x
+
+// Pattern 3: .fst will have a private helper before this fn
+fn pulse_write_ref
+  (r: ref int)
+  (v: int)
+  (#old: Ghost.erased int)
+  requires R.pts_to r old
+  ensures R.pts_to r v
+
+// Pattern 4: Out-of-order — .fsti has write_and_return before assign_ref,
+// but .fst defines assign_ref first (as the primary fn) and then
+// let write_and_return = assign_ref as an alias.
+fn write_and_return
+  (r: ref int)
+  (v: int)
+  (#old: Ghost.erased int)
+  requires R.pts_to r old
+  returns x: int
+  ensures R.pts_to r v ** pure (x == v)
+
+fn assign_ref
+  (r: ref int)
+  (v: int)
+  (#old: Ghost.erased int)
+  requires R.pts_to r old
+  returns x: int
+  ensures R.pts_to r v ** pure (x == v)
+
+// Pattern 5: fn in .fsti, let alias in .fst
+fn pulse_read_ref2
+  (r: ref int)
+  (#v: Ghost.erased int)
+  requires R.pts_to r v
+  returns x: int
+  ensures R.pts_to r v ** pure (x == Ghost.reveal v)