Remove --cmi flag, fix auto-paren lexer for compound bracket tokens

- Remove --cmi from all Makefiles (flag no longer recognized by F*)
- Fix make_auto_paren_lexer to track DOT_LPAREN, DOT_LBRACK,
  DOT_LBRACK_BAR, DOT_LENS_PAREN_LEFT, LENS_PAREN_LEFT, BAR_RBRACK,
  and LENS_PAREN_RIGHT for depth counting. Without this, qualified-open
  syntax like US.(expr) in if/match conditions caused the scanner to
  lose track of nesting depth and consume the entire file.

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

Author: Lef Ioannidis

cond-hoisting.md

@@ -0,0 +1,75 @@
+# Stateful If/Match Conditions
+
+## Problem
+
+`if` and `match` conditions were `term` (pure F\* expressions). Hoisting only
+descends into `Tv_App` arguments, so stateful operations nested inside F\*-level
+`if`/`match` within a condition were invisible:
+
+```
+if (if true then !r = 0 else false) { ... }   // fails: !r buried in Tv_Match
+```
+
+## Solution
+
+Change `Tm_If.b` and `Tm_Match.sc` from `term` to `st_term`, following the
+existing `Tm_While.condition` pattern. A token-stream preprocessor makes
+parentheses optional for backward compatibility.
+
+## Files Changed
+
+### Parser & Sugar
+
+| File | Change |
+|------|--------|
+| `pulseparser.mly` — `ifStmt`, `matchStmt` | `IF LPAREN pulseStmt RPAREN`, `MATCH LPAREN pulseStmt RPAREN` |
+| `PulseSyntaxExtension_Parser.ml` — `make_auto_paren_lexer` | Token preprocessor: auto-inserts `LPAREN`/`RPAREN` when omitted. Detects `LBRACE` at depth 0 as end-of-condition. Passes through F\*-level `if/then` and `match/with` unmodified. |
+| `PulseSyntaxExtension.Sugar.fst` — `If.head`, `Match.head` | `A.term` → `stmt` |
+| `PulseSyntaxExtension.Desugar.fst` — `If`/`Match` cases | `desugar_term` → `desugar_stmt` |
+| `PulseSyntaxExtension.SyntaxWrapper.fsti` — `tm_if`, `tm_match` | Parameter type `term` → `st_term` |
+| `PulseSyntaxExtension_SyntaxWrapper.ml` — `tm_if`, `tm_match` | Wrap with `Tm_STApp`/return as needed |
+
+### AST & Naming
+
+| File | Change |
+|------|--------|
+| `Pulse.Syntax.Base.fsti` — `Tm_If.b`, `Tm_Match.sc` | `term` → `st_term` |
+| `Pulse.Syntax.Base.fst` — `eq_st_term'` | `eq_tm` → `eq_st_term` for `b`/`sc` |
+| `Pulse.Syntax.Naming.fsti` — `freevars_st'`, `ln_st'`, `subst_st_term'` | `*_term` → `*_st_term` for `b`/`sc` (follows `Tm_While.condition`) |
+| `Pulse.Syntax.Naming.fst` — `close_open_inverse_st'` | Same pattern |
+| `Pulse.Typing.FV.fst` — `freevars_close_st_term'` | Same pattern |
+| `Pulse.Syntax.Printer.fst` — `print_st_head` | `term_to_string b` → `st_term_to_string b` |
+| `Pulse.ElimGoto.fst` — `Tm_If`/`Tm_Match` cases | `elab_term` → `elab_st_term` for `b`/`sc` |
+
+### Checker
+
+| File | Function | Change |
+|------|----------|--------|
+| `Pulse.Checker.If.fst` | `check_if_term` (new) | Pure path: extracts `term` from `Tm_Return`, uses original `check_equiv_emp` logic |
+| | `check` | Dispatches: `Tm_Return` → `check_if_term`, other → checks `b` via `check g b ...`, composes with `compose_checker_result_t` |
+| `Pulse.Checker.Match.fst` | `check_match_term` (new) | Pure path: `compute_tot_term_type_and_u` on extracted term |
+| | `check` | Dispatches: `Tm_Return` → `check_match_term`, other → checks `sc` via `check g sc ...`, composes |
+| `Pulse.Checker.fst` | `maybe_elaborate_stateful_head` | Restored `Tm_If`/`Tm_Match` cases: extracts F\* term from `Tm_Return`, runs `hoist_stateful_apps`, rebuilds as `st_term` |
+
+### Extraction
+
+| File | Change |
+|------|--------|
+| `Pulse.Extract.Main.fst` — `Tm_If`, `Tm_Match` | Uniform `extract_dv g b` / `extract_dv g sc` — no `Tm_Return` special-case |
+| `Pulse_Extract_CompilerLib.ml` — `mk_if` | Binds monadic condition to fresh variable via `mk_let`, then branches on it |
+
+### Test
+
+| File | Purpose |
+|------|---------|
+| `test/StatefulIfCondition.fst` | Regression: `if !r = 0 { }`, `if (if true { !r = 0 } else { false }) { }`, `match Some 1 { }` |
+
+## Token Preprocessor Logic
+
+`make_auto_paren_lexer` wraps the base lexer. On `IF`/`MATCH`:
+
+1. If next token is `LPAREN` → pass through (already parenthesized)
+2. Otherwise, buffer tokens tracking `()`/`[]` nesting depth:
+   - `LBRACE` at depth 0 → insert `LPAREN` before buffered tokens, `RPAREN` after
+   - `RETURNS`/`ENSURES` at depth 0 → same (annotation before body)
+   - `THEN`/`WITH` at depth 0 → F\*-level syntax, no modification

mk/test.mk

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

pulse2rust/dpe/c.Makefile

@@ -16,7 +16,7 @@ INCLUDE_PATHS += $(DICE_DIR)/external $(DICE_DIR)/dpe $(DICE_DIR)/engine $(DICE_
 INCLUDE_PATHS += $(PULSE_ROOT)/out/lib/pulse
 ROOTS := $(DICE_DIR)/dpe/DPE.fst
 # ALREADY_CACHED_LIST = *,-HACL,-EverCrypt,-Spec.Hash.Definitions,-L0Core
-OTHERFLAGS += --warn_error -342 --cmi
+OTHERFLAGS += --warn_error -342
 DEPFLAGS += --extract '+EverCrypt +L0Core'
 all: verify extract
 

pulse2rust/tests/Makefile

@@ -26,7 +26,7 @@ OTHERFLAGS += --include $(PULSE_EXAMPLES_ROOT)/dice/common/hacl-c/_cache
 OTHERFLAGS += --include $(PULSE_ROOT)/test
 OTHERFLAGS += --include $(PULSE_ROOT)/test/_cache
 
-OTHERFLAGS += --warn_error -342 --cmi
+OTHERFLAGS += --warn_error -342
 OTHERFLAGS += --include $(PULSE_ROOT)/out/lib/pulse
 
 include $(PULSE_ROOT)/mk/boot.mk

share/pulse/examples/dice/c.Makefile

@@ -7,7 +7,7 @@ PULSE_ROOT ?= ../../../..
 SRC=.
 CACHE_DIR=_cache
 OTHERFLAGS += --include $(PULSE_ROOT)/out/lib/pulse
-OTHERFLAGS += --warn_error -342 --cmi
+OTHERFLAGS += --warn_error -342
 OUTPUT_DIR=_output
 CODEGEN=krml
 TAG=dicec

share/pulse/examples/dice/cbor/Makefile

@@ -11,13 +11,13 @@ OTHERFLAGS += --include ../_cache
 # Note: ^ a bit of a hack. This directory can work independently of the
 # DPE directory above, but in a test we first run verify on DPE which
 # involves verifying everything here already, so this saves some time.
-OTHERFLAGS += --warn_error -342 --cmi
+OTHERFLAGS += --warn_error -342
 OUTPUT_DIR=_output
 CODEGEN=krml
 TAG=cbor
 ROOTS=$(shell find $(SRC) -type f -name '*.fst' -o -name '*.fsti')
 DEPFLAGS=--extract '* -FStar -Pulse -PulseCore'
-OTHERFLAGS += --cmi --already_cached '*,-CBOR.Pulse.Type,-CDDLExtractionTest'
+OTHERFLAGS += --already_cached '*,-CBOR.Pulse.Type,-CDDLExtractionTest'
 include $(PULSE_ROOT)/mk/boot.mk
 
 .DEFAULT_GOAL := myall

src/checker/Pulse.Checker.If.fst

@@ -48,15 +48,18 @@ let check
   (pre:term)
   (post_hint:post_hint_opt g)
   (res_ppname:ppname)
-  (b:term)
+  (b:st_term)
   (e1 e2:st_term)
   (check:check_t)
   : T.Tac (checker_result_t g pre post_hint) =
 
   let g = Pulse.Typing.Env.push_context g "check_if" e1.range in
 
-  let b =
-    check_tot_term g b tm_bool in
+  let b : term =
+    match b.term with
+    | Tm_Return { term=bt } -> check_tot_term g bt tm_bool
+    | _ -> fail g (Some b.range) "check_if: expected a pure condition (Tm_Return); stateful conditions should have been elaborated away"
+  in
 
   let hyp = fresh g in
 
@@ -129,7 +132,8 @@ let check
 
   let c_typing = comp_typing_from_post_hint c post_hint' in
 
-  let if_st = wrst c (Tm_If { b; then_=e1; else_=e2; post=None }) in
+  let b_st = mk_term (Tm_Return { expected_type = tm_bool; insert_eq = false; term = b }) e1.range in
+  let if_st = wrst c (Tm_If { b=b_st; then_=e1; else_=e2; post=None }) in
   let d : st_typing_in_ctxt g pre (PostHint post_hint') =
     (| if_st, c |) in
 

src/checker/Pulse.Checker.If.fsti

@@ -27,7 +27,7 @@ val check
   (pre:term)
   (post_hint:post_hint_opt g)
   (res_ppname:ppname)
-  (b:term)
+  (b:st_term)
   (e1 e2:st_term)
   (check:check_t)
   : T.Tac (checker_result_t g pre post_hint)

src/checker/Pulse.Checker.Match.fst

@@ -481,14 +481,19 @@ let check
         (pre:term)
         (post_hint:post_hint_for_env g)
         (res_ppname:ppname)
-        (sc:term)
+        (sc0:st_term)
         (brs:list branch)
         (check:check_t)
   : T.Tac (checker_result_t g pre (PostHint post_hint))
   =
 
   let g = Pulse.Typing.Env.push_context_no_range g "check_match" in
 
+  let sc : term =
+    match sc0.term with
+    | Tm_Return { term=sct } -> sct
+    | _ -> fail g (Some sc0.range) "check_match: expected a pure scrutinee (Tm_Return); stateful scrutinees should have been elaborated away"
+  in
   let sc_range = Pulse.RuntimeUtils.range_of_term sc in // save range, it gets lost otherwise
   let orig_brs = brs in
   let nbr = L.length brs in
@@ -538,7 +543,8 @@ let check
   (* Provable *)
   assume (L.map (fun br -> elab_pat br.pat) brs == elab_pats');
   let c_typing = comp_typing_from_post_hint c post_hint in
-  let t = wtag (Some (ctag_of_comp_st c)) (Tm_Match {sc; returns_=None; brs}) in
+  let sc_st = mk_term (Tm_Return { expected_type = sc_ty; insert_eq = false; term = sc }) sc_range in
+  let t = wtag (Some (ctag_of_comp_st c)) (Tm_Match {sc=sc_st; returns_=None; brs}) in
 
   checker_result_for_st_typing (| t, c |) res_ppname
 #pop-options

src/checker/Pulse.Checker.Match.fsti

@@ -31,7 +31,7 @@ val check
         (pre:term)
         (post_hint:post_hint_for_env g)
         (res_ppname:ppname)
-        (sc:term)
+        (sc:st_term)
         (brs:list branch)
         (check:check_t)
   : T.Tac (checker_result_t g pre (PostHint post_hint))