Implement defer construct for resource cleanup

Add 'defer pre { handler }; body' construct that executes handler
whenever execution leaves body (both normal fall-through and goto/return).

- Syntax: Tm_Defer with handler_pre (slprop), handler, and body
- Parser: 'defer' keyword with slprop pre and braced handler block
- ElimGoto: preserve defer blocks, conditionalize body but not handler
- Extraction: defer extracted as sequential composition (body then handler)

Author: gebner

src/checker/Pulse.Checker.Defer.fst

@@ -0,0 +1,75 @@
+(*
+   Copyright 2026 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module Pulse.Checker.Defer
+
+open Pulse.Syntax
+open Pulse.Typing
+open Pulse.Checker.Pure
+open Pulse.Checker.Base
+open Pulse.Checker.Prover
+
+module T = FStar.Tactics.V2
+module P = Pulse.Syntax.Printer
+module RU = Pulse.RuntimeUtils
+
+#push-options "--z3rlimit_factor 10 --fuel 0 --ifuel 0"
+let check
+  (g:env)
+  (pre:term)
+  (post_hint:post_hint_opt g)
+  (res_ppname:ppname)
+  (t:st_term { Tm_Defer? t.term })
+  (check:check_t)
+: T.Tac (checker_result_t g pre post_hint)
+= allow_invert post_hint;
+  match post_hint with
+  | NoHint | TypeHint _ ->
+    fail g (Some t.range)
+      "defer requires an annotated post-condition"
+
+  | PostHint post ->
+    let g = push_context "check_defer" t.range g in
+    let Tm_Defer { handler_pre=cpre; handler; body } = t.term in
+    // Check handler_pre is a valid slprop
+    let cpre = check_slprop g cpre in
+    // Extend env: push BindingPost so goto labels see cpre
+    let g' = push_post g cpre in
+    // Extend post_hint: body's postcondition must include cpre
+    let body_post : post_hint_for_env g' =
+      { post with post = tm_star post.post cpre } in
+    // Check body with extended env and post_hint
+    let (| body', c_body |) = apply_checker_result_k (check g' pre (PostHint body_post) res_ppname body) res_ppname in
+    // The body's postcondition should be (post ** cpre)
+    // Now check the handler with cpre as (part of) precondition
+    let post_hint_for_handler: post_hint_for_env g = {
+      g;
+      effect_annot = body_post.effect_annot;
+      ret_ty = tm_unit;
+      u = u0;
+      post = tm_emp;
+    } in
+    let (| handler, c_handler |) = apply_checker_result_k (check g cpre (PostHint post_hint_for_handler) ppname_default handler) ppname_default in
+    // After body, context is (post ** cpre); handler consumes cpre
+    // Overall defer comp has the original post (without cpre)
+    let t = wtag (Some (ctag_of_comp_st c_body)) (Tm_Defer { handler_pre = cpre; handler; body=body' }) in
+    let c = C_ST { u=comp_u c_body; res=comp_res c_body; pre; post=post.post } in
+    let c'' = match_comp_res_with_post_hint t c post_hint in
+    prove_post_hint
+      (try_frame_pre false #g (|t, c''|) res_ppname)
+      post_hint
+      t.range
+#pop-options

src/checker/Pulse.Checker.Defer.fsti

@@ -0,0 +1,32 @@
+(*
+   Copyright 2026 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module Pulse.Checker.Defer
+
+module T = FStar.Tactics.V2
+
+open Pulse.Syntax
+open Pulse.Typing
+open Pulse.Checker.Base
+
+val check
+  (g:env)
+  (pre:term)
+  (post_hint:post_hint_opt g)
+  (res_ppname:ppname)
+  (t:st_term { Tm_Defer? t.term })
+  (check:check_t)
+  : T.Tac (checker_result_t g pre post_hint)

src/checker/Pulse.Checker.fst

@@ -44,6 +44,7 @@ module Admit = Pulse.Checker.Admit
 module Return = Pulse.Checker.Return
 module Rewrite = Pulse.Checker.Rewrite
 module ForwardJumpLabel = Pulse.Checker.ForwardJumpLabel
+module Defer = Pulse.Checker.Defer
 module Goto = Pulse.Checker.Goto
 module PCP = Pulse.Checker.Pure
 
@@ -455,6 +456,9 @@ let rec check
 
       | Tm_Goto _ ->
         Goto.check g pre post_hint res_ppname t
+
+      | Tm_Defer _ ->
+        Defer.check g pre post_hint res_ppname t check
     in
 
     let (| x, g1, t, pre', k |) = r in

src/checker/Pulse.ElimGoto.fst

@@ -302,6 +302,16 @@ let rec conditionalize (g: env) (t: st_term) (cond: cond_params) : T.Tac (option
       | None -> body)
     | _ -> None
   )
+  | Tm_Defer { handler_pre; handler; body } -> (
+    match conditionalize g body cond, conditionalize g handler cond with
+    | None, None -> None
+    | Some body, None ->
+      Some { t with term = Tm_Defer { handler_pre; handler = add_write_if_necessary g handler cond; body } }
+    | None, Some handler ->
+      Some { t with term = Tm_Defer { handler_pre; handler; body = add_write_if_necessary g body cond } }
+    | Some body, Some handler ->
+      Some { t with term = Tm_Defer { handler_pre; handler; body } }
+  )
 
 let rec elim_gotos (g: env) (t: st_term) : T.Tac st_term =
   match t.term with
@@ -372,6 +382,10 @@ let rec elim_gotos (g: env) (t: st_term) : T.Tac st_term =
     { t with term = Tm_WithLocalArray { binder; initializer; length; body } }
   | Tm_ProofHintWithBinders { hint_type; binders; t } ->
     T.fail "elim_gotos: Unexpected constructor: ProofHintWithBinders should have been desugared away"
+  | Tm_Defer { handler_pre; handler; body } ->
+    let handler = elim_gotos g handler in
+    let body = elim_gotos g body in
+    { t with term = Tm_Defer { handler_pre; handler; body } }
   | Tm_ForwardJumpLabel { lbl; body; post } ->
     let cond_var = fresh g in
     let g' = push_goto g cond_var lbl (goto_comp_of_block_comp post) in

src/checker/Pulse.Extract.Main.fst

@@ -174,6 +174,9 @@ let rec simplify_st_term (g:env) (e:st_term) : T.Tac st_term =
   | Tm_Goto _
   | Tm_ProofHintWithBinders _ -> e
 
+  | Tm_Defer { handler_pre; handler; body } ->
+    ret (Tm_Defer { handler_pre; handler = simplify_st_term g handler; body = simplify_st_term g body })
+
   | Tm_Abs { b; q; ascription; body } ->
     ret (Tm_Abs { b; q; ascription; body = with_open b body })
 
@@ -335,6 +338,9 @@ let rec erase_ghost_subterms (g:env) (p:st_term) : T.Tac st_term =
       ret (Tm_ForwardJumpLabel { lbl; body = e; post })
 
     | Tm_Goto _ -> p
+
+    | Tm_Defer { handler_pre; handler; body } ->
+      ret (Tm_Defer { handler_pre; handler = erase_ghost_subterms g handler; body = erase_ghost_subterms g body })
 
   end
 
@@ -552,6 +558,12 @@ let rec extract_dv g (p:st_term) : T.Tac R.term =
           }) (close_term body x)), R.Q_Explicit;
         ]
 
+    | Tm_Defer { handler_pre; handler; body } ->
+      let body = extract_dv g body in
+      let handler = extract_dv g handler in
+      let b = R.pack_binder { sort = ECL.unit_ty; ppname = T.seal "_"; attrs = []; qual = R.Q_Explicit } in
+      ECL.mk_let b body handler
+
   end
 
 and extract_dv_branch g (b:Pulse.Syntax.Base.branch) : T.Tac R.branch =

src/checker/Pulse.Syntax.Base.fst

@@ -282,6 +282,10 @@ let rec eq_st_term (t1 t2:st_term)
     | Tm_Goto { lbl=l1; arg=a1 },
       Tm_Goto { lbl=l2; arg=a2 } ->
       eq_tm l1 l2 && eq_tm a1 a2
+
+    | Tm_Defer { handler_pre=p1; handler=h1; body=b1 },
+      Tm_Defer { handler_pre=p2; handler=h2; body=b2 } ->
+      eq_tm p1 p2 && eq_st_term h1 h2 && eq_st_term b1 b2
 
     | _ -> false
 

src/checker/Pulse.Syntax.Base.fsti

@@ -312,6 +312,11 @@ type st_term' =
       lbl: term; // either var or named
       arg: term;
     }
+  | Tm_Defer {
+      handler_pre: slprop;
+      handler: st_term;
+      body: st_term;
+    }
 and st_term = {
     term : st_term';
     range : range;

src/checker/Pulse.Syntax.Builder.fst

@@ -54,6 +54,7 @@ let tm_admit ctag u typ post = Tm_Admit { ctag; u; typ; post }
 let tm_pragma_with_options o b = Tm_PragmaWithOptions { options=o; body=b }
 let tm_forward_jump_label body lbl post = Tm_ForwardJumpLabel { body; lbl; post }
 let tm_goto lbl arg = Tm_Goto { lbl; arg }
+let tm_defer handler_pre handler body = Tm_Defer { handler_pre; handler; body }
 let with_range t r = { term = t; range = r; effect_tag = default_effect_hint; source=Sealed.seal true; seq_lhs=Sealed.seal false; }
 let tm_assert_with_binders bs p t = Tm_ProofHintWithBinders { hint_type=ASSERT { p; elaborated=false }; binders=bs; t }
 let mk_assert_hint_type p = ASSERT { p; elaborated=false }

src/checker/Pulse.Syntax.Naming.fst

@@ -233,6 +233,11 @@ let rec close_open_inverse_st'  (t:st_term)
     | Tm_Goto { lbl; arg } ->
       close_open_inverse' lbl x i;
       close_open_inverse' arg x i
+
+    | Tm_Defer { handler_pre; handler; body } ->
+      close_open_inverse' handler_pre x i;
+      close_open_inverse_st' handler x i;
+      close_open_inverse_st' body x i
 #pop-options
 
 let close_open_inverse (t:term) (x:var { ~(x `Set.mem` freevars t) } )

src/checker/Pulse.Syntax.Naming.fsti

@@ -168,6 +168,9 @@ let rec freevars_st (t:st_term)
     | Tm_Goto { lbl; arg } ->
       freevars lbl ++ freevars arg
 
+    | Tm_Defer { handler_pre; handler; body } ->
+      freevars handler_pre ++ freevars_st handler ++ freevars_st body
+
 and freevars_branches (t:list branch) : Set.set var =
   match t with
   | [] -> empty
@@ -356,6 +359,9 @@ let rec ln_st' (t:st_term) (i:int)
     | Tm_Goto { lbl; arg } ->
       ln' lbl i && ln' arg i
 
+    | Tm_Defer { handler_pre; handler; body } ->
+      ln' handler_pre i && ln_st' handler i && ln_st' body i
+
 and ln_branch' (b : branch) (i:int) : Tot bool (decreases b) =
   ln_pattern' b.pat i &&
   ln_st' b.e (i + pattern_shift_n b.pat)
@@ -609,6 +615,9 @@ let rec subst_st_term (t:st_term) (ss:subst)
     | Tm_Goto { lbl; arg } ->
       Tm_Goto { lbl=subst_term lbl ss; arg=subst_term arg ss }
 
+    | Tm_Defer { handler_pre; handler; body } ->
+      Tm_Defer { handler_pre=subst_term handler_pre ss; handler=subst_st_term handler ss; body=subst_st_term body ss }
+
     in
     { t with term = t' }