Pulse tests: do not define KRML_HOME for CI; add divergent or decreases clauses

[tahina-pro]

Summary

This branch tracks two recent F* changes so that KaRaMeL's Pulse test suite
(build-and-test-pulse) keeps building and passing against F* master:

• Add FSTAR_USE_KRML_EXE; migrate from KRML_HOME to KRML_EXE FStar#4349 — F* migrated from KRML_HOME to KRML_EXE.
• Pulse: split stt into terminating stt and divergent stt_div FStar#4358 — Pulse split its computation type stt into a
  terminating stt (surface keyword fn) and a possibly-divergent stt_div
  (surface keyword divergent fn).

Changes

1. CI: do not use KRML_HOME (follows FStarLang/FStar#4349)

.github/workflows/ci.yml — the test-pulse job no longer needs KRML_HOME. The current test/pulse/Makefile uses the proper Karamel executable for KRML_EXE.

2. test/pulse: adapt to the Pulse stt/stt_div split (follows FStarLang/FStar#4358)

Root cause. After #4358, a while loop (or fn rec) with no decreases
measure is a divergent (stt_div) computation. A plain fn must be
terminating (stt), so it can no longer contain a measure-free loop and now
fails with:

Error 228: Cannot compose computations in this divergent block:
  - This computation has effect: 'stt_div'
  - The continuation has effect: 'stt'

This broke Inline.fst, InlineLoopCond.fst, Goto.fst and Break.fst.

Fix. Following the same conventions F* used to migrate its own Pulse
libraries and examples in #4358:

• Genuinely non-terminating loops are marked divergent fn.
• Terminating loops get a decreases measure (placed after the
  invariant/ensures clauses) so they stay plain terminating fns.

File · function	Loop nature	Fix
InlineLoopCond.test, InlineLoopCond.test_ok	Infinite — immutable condition, empty body	divergent fn
Break.break_continue_and_return	Infinite — a continue path never advances the counter	divergent fn
Break.simple_break	Terminating (break-only body)	decreases (if !k then 1 else 0)
Break.find_zero_with_break	Terminating count up to sz	decreases (SizeT.v sz - SizeT.v (!i))
Goto.find_zero	Terminating count up to sz	decreases (SizeT.v sz - SizeT.v (!i))
Inline.tst	Terminating count up to uu__k	bound invariant pure (v (!i) <= v uu__k) + decreases (v uu__k - v (!i))

Testing

make -kj$(nproc) test-pulse (the exact CI target) passes from a clean state:
all CHECK, EXTRACT, KRML and DIFF steps succeed.

Extraction is unaffected — stt_div extracts like stt — so the generated C
is unchanged and no *.expected.c files needed updating.

Notes

• No changes outside .github/workflows/ci.yml and test/pulse/.

[tahina-pro]

Thanks Jonathan!