Lef/ternary hoisting

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))

src/checker/Pulse.Checker.fst

@@ -188,19 +188,39 @@ let maybe_elaborate_stateful_head (g:env) (t:st_term)
       b in
     Pulse.Checker.Base.hoist g (Inr t) true rebuild
   | Tm_If {b; then_=e1; else_=e2; post} ->
-    let rebuild (b:either term st_term {Inl? b})
-    : T.Tac st_term
-    = let Inl b = b in
-      {t with term=Tm_If { b; then_=e1; else_=e2; post }}
-    in
-    Pulse.Checker.Base.hoist g (Inl b) true rebuild  
+    (match b.term with
+     | Tm_Return { expected_type; insert_eq; term=bt } ->
+       let rebuild (bt':either term st_term {Inl? bt'})
+       : T.Tac st_term
+       = let Inl bt' = bt' in
+         let b' = { b with term = Tm_Return { expected_type; insert_eq; term = bt' } } in
+         {t with term=Tm_If { b=b'; then_=e1; else_=e2; post }}
+       in
+       Pulse.Checker.Base.hoist g (Inl bt) true rebuild
+     | _ ->
+       // Stateful condition: transform into let _cond = b; if (return _cond) { e1 } else { e2 }
+       let binder = mk_binder_ppname Pulse.Typing.tm_bool (mk_ppname_no_range "_if_cond") in
+       let bv0 = Pulse.Syntax.Pure.tm_bvar { bv_index = 0; bv_ppname = ppname_default } in
+       let pure_b = mk_term (Tm_Return { expected_type = Pulse.Typing.tm_bool; insert_eq = false; term = bv0 }) b.range in
+       let inner_if = {t with term = Tm_If { b = pure_b; then_ = e1; else_ = e2; post }} in
+       Some (mk_term (Tm_Bind { binder; head = b; body = inner_if }) t.range))
   | Tm_Match {sc; returns_=post_match; brs} ->
-    let rebuild (sc:either term st_term {Inl? sc})
-    : T.Tac st_term
-    = let Inl sc = sc in
-      { t with term=Tm_Match {sc; returns_=post_match; brs} }
-    in
-    Pulse.Checker.Base.hoist g (Inl sc) true rebuild
+    (match sc.term with
+     | Tm_Return { expected_type; insert_eq; term=sct } ->
+       let rebuild (sct':either term st_term {Inl? sct'})
+       : T.Tac st_term
+       = let Inl sct' = sct' in
+         let sc' = { sc with term = Tm_Return { expected_type; insert_eq; term = sct' } } in
+         { t with term=Tm_Match {sc=sc'; returns_=post_match; brs} }
+       in
+       Pulse.Checker.Base.hoist g (Inl sct) true rebuild
+     | _ ->
+       // Stateful scrutinee: transform into let _sc = sc; match (return _sc) { brs }
+       let binder = mk_binder_ppname Pulse.Syntax.Pure.tm_unknown (mk_ppname_no_range "_match_sc") in
+       let bv0 = Pulse.Syntax.Pure.tm_bvar { bv_index = 0; bv_ppname = ppname_default } in
+       let pure_sc = mk_term (Tm_Return { expected_type = Pulse.Syntax.Pure.tm_unknown; insert_eq = false; term = bv0 }) sc.range in
+       let inner_match = {t with term = Tm_Match { sc = pure_sc; returns_ = post_match; brs }} in
+       Some (mk_term (Tm_Bind { binder; head = sc; body = inner_match }) t.range))
   | Tm_WithLocal { binder; initializer=Some initializer; body } ->
     let rebuild (sc:either term st_term {Inl? sc})
     : T.Tac st_term

src/checker/Pulse.ElimGoto.fst

@@ -86,7 +86,11 @@ let mk_if_cond (g: env) (t: st_term) (cond: nvar) : T.Tac st_term =
     binder = mk_binder_ppname_inline tm_bool (fst cond);
     head = mk_read u0 tm_bool (term_of_nvar cond);
     body = wtag t.effect_tag <| Tm_If {
-      b = close_term (term_of_nvar cond) (snd cond);
+      b = wtag (as_effect_hint STT) <| Tm_Return {
+        expected_type = tm_bool;
+        insert_eq = false;
+        term = close_term (term_of_nvar cond) (snd cond);
+      };
       then_ = wtag t.effect_tag <| Tm_Return {
         expected_type = tm_unit;
         insert_eq = false;
@@ -247,7 +251,11 @@ let rec conditionalize (g: env) (t: st_term) (cond: cond_params) : T.Tac (option
             binder = mk_binder_ppname_inline tm_bool ppname_default;
             body = (fun t -> close_st_term t y) <| wtag condition.effect_tag <|
               Tm_If {
-                b = term_of_nvar (ppname_default, y);
+                b = wtag (as_effect_hint STT) <| Tm_Return {
+                  expected_type = tm_bool;
+                  insert_eq = false;
+                  term = term_of_nvar (ppname_default, y);
+                };
                 then_ = wtag condition.effect_tag <| Tm_Return {
                   expected_type = tm_bool;
                   insert_eq = false;

src/checker/Pulse.Extract.Main.fst

@@ -206,10 +206,10 @@ let rec simplify_st_term (g:env) (e:st_term) : T.Tac st_term =
     ret (Tm_TotBind { binder; head; body = with_open binder body })
 
   | Tm_If { b; then_; else_; post } ->
-    ret (Tm_If { b; then_ = simplify_st_term g then_; else_ = simplify_st_term g else_; post })
+    ret (Tm_If { b = simplify_st_term g b; then_ = simplify_st_term g then_; else_ = simplify_st_term g else_; post })
 
   | Tm_Match { sc; returns_; brs } ->
-    ret (Tm_Match { sc; returns_; brs = T.map (simplify_branch g) brs })
+    ret (Tm_Match { sc = simplify_st_term g sc; returns_; brs = T.map (simplify_branch g) brs })
 
   | Tm_While { invariant; loop_requires; meas; condition; body } ->
     let condition = simplify_st_term g condition in
@@ -298,11 +298,13 @@ let rec erase_ghost_subterms (g:env) (p:st_term) : T.Tac st_term =
            ret (Tm_TotBind { binder; head; body })
 
     | Tm_If { b; then_; else_; post } ->
+      let b = erase_ghost_subterms g b in
       let then_ = erase_ghost_subterms g then_ in
       let else_ = erase_ghost_subterms g else_ in
       ret (Tm_If { b; then_; else_; post })
 
     | Tm_Match { sc; brs; returns_ } ->
+      let sc = erase_ghost_subterms g sc in
       let brs = T.map (erase_ghost_subterms_branch g) brs in
       ret (Tm_Match { sc; brs; returns_ })
 
@@ -468,11 +470,13 @@ let rec extract_dv g (p:st_term) : T.Tac R.term =
       ECL.mk_let b' e1 (close_term e2 x._2)
 
     | Tm_If { b; then_; else_ } ->
+      let b = extract_dv g b in
       let then_ = extract_dv g then_ in
       let else_ = extract_dv g else_ in
       ECL.mk_if b then_ else_
 
     | Tm_Match { sc; brs } ->
+      let sc = extract_dv g sc in
       R.pack_ln (R.Tv_Match sc None (T.map (extract_dv_branch g) brs))
 
     | Tm_While { condition; body } ->

src/checker/Pulse.Syntax.Base.fst

@@ -215,14 +215,14 @@ let rec eq_st_term (t1 t2:st_term)
 
     | Tm_If { b=g1; then_=ethen1; else_=eelse1; post=p1},
       Tm_If { b=g2; then_=ethen2; else_=eelse2; post=p2} ->
-      eq_tm g1 g2 &&
+      eq_st_term g1 g2 &&
       eq_st_term ethen1 ethen2 &&
       eq_st_term eelse1 eelse2 &&
       eq_tm_opt p1 p2
 
     | Tm_Match {sc=sc1; returns_=r1; brs=br1},
       Tm_Match {sc=sc2; returns_=r2; brs=br2} ->
-      eq_tm sc1 sc2 &&
+      eq_st_term sc1 sc2 &&
       eq_tm_opt r1 r2 &&
       eq_list_dec t1 t2 eq_branch br1 br2
 

src/checker/Pulse.Syntax.Base.fsti

@@ -241,13 +241,13 @@ type st_term' =
       body:st_term;
     }
   | Tm_If {
-      b:term;
+      b:st_term;
       then_:st_term;
       else_:st_term;
       post:option slprop;
     }
   | Tm_Match {
-      sc:term;
+      sc:st_term;
       returns_:option slprop;
       brs: list branch;
     }

src/checker/Pulse.Syntax.Naming.fst

@@ -184,13 +184,13 @@ let rec close_open_inverse_st'  (t:st_term)
       close_open_inverse_st' body x i
 
     | Tm_If { b; then_; else_; post } ->
-      close_open_inverse' b x i;    
+      close_open_inverse_st' b x i;    
       close_open_inverse_st' then_ x i;    
       close_open_inverse_st' else_ x i;
       close_open_inverse_opt' post x (i + 1)
 
     | Tm_Match { sc; returns_; brs } ->
-      close_open_inverse' sc x i;
+      close_open_inverse_st' sc x i;
       close_open_inverse_opt' returns_ x i;
       admit(); // need map dec fusion
       ()