From 481094b1062b6e39f5a18aab210f66fa1b9667d8 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Thu, 16 Jul 2026 12:09:25 -0700
Subject: [PATCH 1/3] CI (Pulse tests) : use KRML_EXE instead of KRML_HOME
 (from FStarLang/FStar#4349)

---
 .github/workflows/ci.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index c42142c1..ab217e26 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -294,7 +294,9 @@ jobs:
         with:
           node-version: 16
 
-      - run: echo "KRML_HOME=$(pwd)/karamel" >> $GITHUB_ENV
+      - run: |
+         echo "FSTAR_USE_KRML_EXE=1" >> $GITHUB_ENV
+         echo "KRML_EXE=$(pwd)/karamel/out/bin/krml" >> $GITHUB_ENV
 
       - name: Karamel CI (test-pulse)
         working-directory: karamel

From bf377467df4b94d65d9a28b42998f57e6350fa47 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Thu, 16 Jul 2026 12:32:54 -0700
Subject: [PATCH 2/3] test/pulse: adapt to Pulse stt/stt_div split
 (FStarLang/FStar#4358)

F* PR 4358 splits Pulse's `stt` into terminating `stt` (`fn`) and
possibly-divergent `stt_div` (`divergent fn`). A measure-free `while`
loop is now divergent, so a plain `fn` containing one fails with
Error 228 ("Cannot compose computations in this divergent block").

Fix the affected pulse extraction tests:
- Genuinely non-terminating loops are marked `divergent fn`:
  InlineLoopCond.test and .test_ok (immutable condition, empty body)
  and Break.break_continue_and_return (a `continue` path that never
  advances the counter).
- Terminating loops get a `decreases` measure to stay plain `fn`:
  Inline.tst, Break.simple_break, Break.find_zero_with_break and
  Goto.find_zero (adding a bound invariant to Inline.tst as needed).

Extraction is unaffected (stt_div extracts like stt), so the expected
C output is unchanged.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: ec80b304-3585-492b-9f51-c0c9f8b9358f
---
 test/pulse/Break.fst          | 4 +++-
 test/pulse/Goto.fst           | 1 +
 test/pulse/Inline.fst         | 2 ++
 test/pulse/InlineLoopCond.fst | 4 ++--
 4 files changed, 8 insertions(+), 3 deletions(-)

diff --git a/test/pulse/Break.fst b/test/pulse/Break.fst
index 2b22a71b..61c03c00 100644
--- a/test/pulse/Break.fst
+++ b/test/pulse/Break.fst
@@ -9,12 +9,13 @@ fn simple_break ()
   while (!k)
     invariant live k
     ensures true
+    decreases (if !k then 1 else 0)
   {
     break;
   }
 }
 
-fn break_continue_and_return (which: UInt8.t)
+divergent fn break_continue_and_return (which: UInt8.t)
 {
   let mut i = 0ul;
   while (!i `UInt32.lt` 1000ul)
@@ -48,6 +49,7 @@ fn find_zero_with_break (a: array Int32.t) (sz: SizeT.t)
     invariant pure (SizeT.v !i <= SizeT.v sz /\
       (forall (j: nat). j < SizeT.v (!i) ==> Seq.index 'va j <> 0l))
     ensures (SizeT.v !i < SizeT.v sz /\ a.(!i) = 0l)
+    decreases (SizeT.v sz - SizeT.v (!i))
   {
     if (a.(!i) = 0l) {
       break;
diff --git a/test/pulse/Goto.fst b/test/pulse/Goto.fst
index e5bde886..1e1e30b0 100644
--- a/test/pulse/Goto.fst
+++ b/test/pulse/Goto.fst
@@ -29,6 +29,7 @@ fn find_zero (a: array Int32.t) (sz: SizeT.t)
     invariant live i
     invariant pure (SizeT.v !i <= SizeT.v sz /\
       (forall (j: nat). j < SizeT.v (!i) ==> Seq.index 'va j <> 0l))
+    decreases (SizeT.v sz - SizeT.v (!i))
   {
     if (a.(!i) = 0l) {
       return !i;
diff --git a/test/pulse/Inline.fst b/test/pulse/Inline.fst
index a79f9787..f9ff2a79 100644
--- a/test/pulse/Inline.fst
+++ b/test/pulse/Inline.fst
@@ -60,6 +60,8 @@ fn tst (shared : UInt32.t)
   let mut i = 0ul;
   while (!i <^ uu__k)
     invariant live i
+    invariant pure (v (!i) <= v uu__k)
+    decreases (Prims.op_Subtraction (v uu__k) (v (!i)))
   {
     i := !i +^ 1ul;
   };
diff --git a/test/pulse/InlineLoopCond.fst b/test/pulse/InlineLoopCond.fst
index fe47184f..96f326e8 100644
--- a/test/pulse/InlineLoopCond.fst
+++ b/test/pulse/InlineLoopCond.fst
@@ -3,7 +3,7 @@ module InlineLoopCond
 #lang-pulse
 open Pulse
 
-fn test (f : unit -> fn returns UInt32.t)
+divergent fn test (f : unit -> fn returns UInt32.t)
   returns UInt32.t
 {
   let uu__  = f ();
@@ -15,7 +15,7 @@ fn test (f : unit -> fn returns UInt32.t)
   0ul
 }
 
-fn test_ok (x : UInt32.t)
+divergent fn test_ok (x : UInt32.t)
   returns UInt32.t
 {
   (* This one could be inlined (it's not at the moment) *)

From 2117b1722564ba29f09538481f831c13550bd0f6 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Thu, 16 Jul 2026 15:04:57 -0700
Subject: [PATCH 3/3] KRML_EXE need not be set for build-and-test-pulse

---
 .github/workflows/ci.yml | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index ab217e26..c94c5a5a 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -294,10 +294,6 @@ jobs:
         with:
           node-version: 16
 
-      - run: |
-         echo "FSTAR_USE_KRML_EXE=1" >> $GITHUB_ENV
-         echo "KRML_EXE=$(pwd)/karamel/out/bin/krml" >> $GITHUB_ENV
-
       - name: Karamel CI (test-pulse)
         working-directory: karamel
         run: |