Test: Regression test for Pulse fn extraction with .fsti interface

Adds a minimal test case that verifies Pulse fn declarations in .fsti interface
files are correctly extracted to C via KaRaMeL. Previously, such functions were
silently dropped due to the interleaver not recognizing DeclToBeDesugared as an
interface declaration (fixed in FStarC.ToSyntax.Interleave.fst).

The test defines:
- pure_add: a pure function (control — always worked)
- pulse_read_ref: a Pulse fn reading a ref (was dropped, now extracted)

Both must appear in the generated .c file. The .c.expected file is checked
against actual KaRaMeL output by mk/test.mk's automatic diff mechanism.

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

Author: 2 people

test/bug-reports/ExtractPulseFnIface.c.expected

@@ -0,0 +1,17 @@
+/* krml header omitted for test repeatability */
+
+
+#include "ExtractPulseFnIface.h"
+
+extern krml_checked_int_t Prims_op_Addition(krml_checked_int_t x, krml_checked_int_t y);
+
+krml_checked_int_t ExtractPulseFnIface_pure_add(krml_checked_int_t x, krml_checked_int_t y)
+{
+  return Prims_op_Addition(x, y);
+}
+
+krml_checked_int_t ExtractPulseFnIface_pulse_read_ref(krml_checked_int_t *r)
+{
+  return *r;
+}
+

test/bug-reports/ExtractPulseFnIface.fst

@@ -0,0 +1,19 @@
+module ExtractPulseFnIface
+#lang-pulse
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Reference
+module R = Pulse.Lib.Reference
+
+let pure_add (x y : int) : int = x + y
+
+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)
+{
+  let x = !r;
+  x
+}

test/bug-reports/ExtractPulseFnIface.fsti

@@ -0,0 +1,21 @@
+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. *)
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Reference
+module R = Pulse.Lib.Reference
+
+val pure_add (x y : int) : int
+
+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)