Fix cleanup: conditionalize handler, refine typing rule, revert test

- conditionalize: handle both body and handler like Tm_If handles
  branches; when one has a goto but the other doesn't, use
  add_write_if_necessary on the unchanged subterm
- T_Cleanup typing rule: add constraints relating c to c_body
  (same pre/u/res), allowing the checker to set the result post
- Revert test/Cleanup.fst to original 'cleanup live v { ... }' syntax

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

Author: gebner

src/checker/Pulse.ElimGoto.fst

@@ -304,9 +304,13 @@ let rec conditionalize (g: env) (t: st_term) (cond: cond_params) : T.Tac (option
     | _ -> None
   )
   | Tm_Cleanup { cleanup_pre; handler; body } -> (
-    match conditionalize g body cond with
-    | None -> None
-    | Some body ->
+    match conditionalize g body cond, conditionalize g handler cond with
+    | None, None -> None
+    | Some body, None ->
+      Some { t with term = Tm_Cleanup { cleanup_pre; handler = add_write_if_necessary g handler cond; body } }
+    | None, Some handler ->
+      Some { t with term = Tm_Cleanup { cleanup_pre; handler; body = add_write_if_necessary g body cond } }
+    | Some body, Some handler ->
       Some { t with term = Tm_Cleanup { cleanup_pre; handler; body } }
   )
 

src/checker/Pulse.Typing.fst

@@ -1144,9 +1144,11 @@ type st_typing : env -> st_term -> comp -> Type =
       cleanup_pre:slprop ->
       handler:st_term ->
       body:st_term ->
-      c_body:comp_st ->
+      c_body:comp_st { comp_post c_body == tm_star (comp_post c_body) cleanup_pre \/ True } ->
       c_handler:comp_st ->
-      c:comp_st ->
+      c:comp_st { comp_pre c == comp_pre c_body /\
+                  comp_u c == comp_u c_body /\
+                  comp_res c == comp_res c_body } ->
       st_typing (push_post g cleanup_pre) body c_body ->
       st_typing g handler c_handler ->
       st_typing g (wtag (Some (ctag_of_comp_st c)) (Tm_Cleanup { cleanup_pre; handler; body })) c

test/Cleanup.fst

@@ -14,7 +14,7 @@ fn without_cleanup (x: bool) {
 
 fn with_cleanup (x: bool) {
   let v = V.alloc 1uy 10sz;
-  cleanup (V.pts_to v (Seq.create 10 1uy)) { V.free v };
+  cleanup live v { V.free v };
   if (x) {
     return;
   };