Emit a result-determining postcondition as rewrites_to by nikswamy · Pull Request #240 · FStarLang/pal

nikswamy · 2026-08-19T04:10:28Z

Part of the upstreaming of nswamy/pal-c-project-integration (PR26 of 35 PRs) — see PR_PLAN.md on that branch for the whole plan and the dependency graph.

Base: nswamy/pal-pr25-rvalue-member — a stacked PR. It depends on nswamy/pal-pr25-rvalue-member, nswamy/pal-pr28-nullable-caller-transfer, so only the commits listed below are its own; it will be retargeted at main once its parents land.

It has more than one parent, so the diff against nswamy/pal-pr25-rvalue-member also carries the commits from nswamy/pal-pr28-nullable-caller-transfer until those land.

_ensures(return == E) with E free of return fixes the result outright, and Pulse has
a better form for exactly that: rewrites_to, read as a substitution. That is what a
conditional needs — a call inside a branch binds its result to a branch-local name, the
branch's postcondition closes over it existentially, and Pulse's join gives up on an
exists*, leaving a match on the guard that nothing afterwards can take a resource out
of. With rewrites_to the local never reaches the postcondition.

Commits

Emit a result-determining postcondition as rewrites_to

Testing

Verified: make rust lib, test/check-template.sh, cargo fmt --check, clang-format --dry-run --Werror, and F* verification of test/compound_literal_member, test/nullable_out, test/nullable_out_struct, test/rvalue_member, test/rvalue_member_branch.

The type pre-pass elaborated every parameter type in the environment the function started with, so a _refine on one parameter could not mention any other. Push each parameter into the environment as its type is elaborated, which is the order C itself gives them. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 60e9210)

C lets a declaration and its definition name the same parameter differently, and _Use_decl_annotations_ then gives the definition the declaration's annotations -- including a _refine carried in a parameter's type. merge already mapped the declaration's names onto the definition's for _requires and _ensures; it did not do the same for the refinements inside argument types, so a refinement mentioning the declaration's SequenceLayout was checked in a scope that binds Layout. Behind that was an ordering problem. The scope check ran between prune and merge, and until merge runs a declaration and its definition are still two separate declarations, so the definition legitimately carries annotations written against names it does not bind. The check was asking a question that has no answer yet. It now runs after merge, which is the first point at which the two have been reconciled. Found on a deserializer whose header names a parameter SequenceLayout and whose definition names it Layout. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit f1ded6e)

An _Out_opt_ parameter is a pointer the caller may pass as NULL, and the callee writes through it only after testing it. Three things were missing. The existential for the pointee now lives inside unless_null, so the null branch does not have to name a value that is not there. The intro and elim rules are stated once per pointer flavor rather than through the typeclass, so the prover is not left with an unsolved has_is_null constraint. And the null test itself now eliminates the guard on entry to each branch. Pulse cannot discharge the slprop it infers when it joins two branches: the join is a match on the test, and the branch hypothesis does not reduce it. So on the way out of each branch we restate the guarded resource, leaving both branches at the same slprop and nothing for Pulse to join. The restatement is an assert rather than a call, because the value at a pointer is only resolved against the context in a slprop position, never in a term passed as an argument. Branches that return, break, continue or jump need no restatement -- nothing joins them -- and would be wrong to receive one, since the code after an early return on null is entitled to the opened resource. Splitting Nullable into an interface keeps unless_null abstract, so a caller never sees the match on the null test. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit f6e105b)

A guarded optional-output write is rarely in tail position, so Pulse has to infer the postcondition of the `if`. It does that by matching the two branches' resources conjunct by conjunct and wrapping whatever is left over in a dependent match on the guard -- which the prover then cannot discharge, even though the branch hypothesis fixes the guard. Closing the guarded pointer back into `unless_null` handled the first conjunct that fails to match. This is the second: a borrowed structure the branch reads through. Reading a member splits the parameter into per-member ownership, so the reading branch offers `Struct_X__aux_raw_unfolded x ** pts_to (field_1 x) v` where the other branch still offers `pts_to x v`, and the matcher has no rule relating the two. Restate the borrowed parameter's entry-state resources at the end of both branches, so the two sides settle on one shape before the join looks at them. The restatement has to avoid existentials: the matcher gives up immediately on an existentially quantified conjunct, which would trade this failure for a worse one. A `const` parameter's value is already named by the signature's implicits, so it can be quoted directly; a plain one is bound existentially in the signature, so the body names it with a `with` binder placed after the parameter redeclarations, where it scopes over every guarded branch in the function. Each conjunct gets its own `assert`, because `!p` cannot resolve from under a binder introduced by the same statement. test/nullable_out_struct covers it: two optional outputs filled from members of a shared borrowed structure, which is the shape a deserializer with optional outputs has. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit c1c8f8d)

Closing a null test on a `const` nullable pointer asserts the guarded resource back, so the value it names has to be the one the signature will accept: `preserves unless_null p (.. 'val_p_0)` asks for the value the caller handed in, not for some value. The payload was instead named off the local the null test binds, and was additionally re-quantified with `exists*`. The signature never bound those names, so the assertion could not be discharged from the guarded hypothesis and the prover fell back to the null introduction, surfacing much later as an unprovable `test_null` obligation. Let a `Standard` naming carry an explicit base identifier and have the nullable payload set it to the parameter in `Const` mode, where it also stops re-quantifying. Non-const nullable inputs, whose values are bound existentially anyway, keep deriving the base from the expression. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit c2065fb)

A callee with an optional pointer states its half of the bargain under a guard: it asks for unless_null p (..) and gives back unless_null p (..). That is right for the callee and wrong for its caller, which knows which side of the test its own argument is on and wants the resource, or nothing, rather than a guarded maybe. The guard is deliberately opaque, so neither end of it opens by itself, and until now a caller that supplied an optional output never got the storage back -- it could not read what it had just asked to be written -- while a caller that declined one was told it had leaked a resource that was never there. Neither is unusual. A directory footer conversion wants three of the five fields its base header conversion can give it, which is three recoveries and two discards in a single call. Declining is the easy half: the pointer is null, the resource is nothing, and the guard is discarded. Supplying takes a fact rather than a resource -- eliminating the guard needs to know the pointer is not null, and the only evidence of that is the resource now inside the guard. So the fact is established before the call, while the resource is still in the open, and carried across as a pure proposition. Which lemma establishes it follows from the callee's parameter mode: an out parameter is handed uninitialized storage, anything else an initialized cell. Two arguments look identical here and are not: one whose ownership PAL emitted, which it may take back, and one whose ownership was written by hand in the enclosing contract, which it may not. A _nullable argument is the forwarding case, where the caller cannot say which way the test goes and the guard has to travel on untouched; a _plain one carries ownership PAL never emitted, and opening it would take the enclosing contract's own guard apart. Both are left alone. An optional array argument is still opened by hand. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit ffe5256)

…al-pr26-rewrites-to

A clause that fixes a function's result outright -- `_ensures(return == E)`, with `E` free of `return` -- said the same thing as any other equality, and was proved the same way: look it up when the result is needed. Pulse has a better form for exactly this. `rewrites_to` is read as a substitution: the bound result is replaced by `E` throughout the context and the goal. That is what a conditional needs. A call inside a branch binds its result to a branch-local name, so the branch's postcondition closes over it existentially; Pulse's join gives up on an `exists*` and leaves a `match` on the guard that nothing after the conditional can take a resource out of. With `rewrites_to` the local never reaches the postcondition -- it has already been rewritten to a term the caller can see -- and the branches join normally. Recognise the shape and emit it that way. Elaboration wraps a boolean clause in the coercion that renders it as an slprop, so look through that first; an unrecognised expression form answers "mentions return" and costs the caller the better form rather than soundness. The new test exercises this together with the two preceding fixes: it projects a call result twice, once inside a null-guarded branch. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d (cherry picked from commit 97ab222)

gebner · 2026-08-26T21:13:15Z

!diff

github-actions · 2026-08-26T21:35:52Z

Generated F* output diff

Effect of this pull request on the F* code pal generates for the test suite (b6a4795 → 1a8c0f7).

Summary

 {base => head}/addr_global/Func_add.fst                                              |   2 +-
 {base => head}/addr_global/Func_add.fsti                                             |   2 +-
 {base => head}/anon_struct/Func_frob.fst                                             |   6 +++---
 {base => head}/anon_struct/Func_frob.fsti                                            |   6 +++---
 {base => head}/array_deref/Func_deref_read.fst                                       |   2 +-
 {base => head}/array_deref/Func_deref_read.fsti                                      |   2 +-
 {base => head}/assign_expr/Func_chain_assign.fst                                     |   2 +-
 {base => head}/assign_expr/Func_chain_assign.fsti                                    |   2 +-
 {base => head}/assign_expr/Func_compound_assign_rvalue.fst                           |   2 +-
 {base => head}/assign_expr/Func_compound_assign_rvalue.fsti                          |   2 +-
 {base => head}/binary_ops/Func_test_add_assign.fst                                   |   2 +-
 {base => head}/binary_ops/Func_test_add_assign.fsti                                  |   2 +-
 {base => head}/binary_ops/Func_test_and_assign.fst                                   |   2 +-
 {base => head}/binary_ops/Func_test_and_assign.fsti                                  |   2 +-
 {base => head}/binary_ops/Func_test_chain.fst                                        |   2 +-
 {base => head}/binary_ops/Func_test_chain.fsti                                       |   2 +-
 {base => head}/binary_ops/Func_test_mul_assign.fst                                   |   2 +-
 {base => head}/binary_ops/Func_test_mul_assign.fsti                                  |   2 +-
 {base => head}/binary_ops/Func_test_or_assign.fst                                    |   2 +-
 {base => head}/binary_ops/Func_test_or_assign.fsti                                   |   2 +-
 {base => head}/binary_ops/Func_test_shl_assign.fst                                   |   2 +-
 {base => head}/binary_ops/Func_test_shl_assign.fsti                                  |   2 +-
 {base => head}/binary_ops/Func_test_shr_assign.fst                                   |   2 +-
 {base => head}/binary_ops/Func_test_shr_assign.fsti                                  |   2 +-
 {base => head}/binary_ops/Func_test_sub_assign.fst                                   |   2 +-
 {base => head}/binary_ops/Func_test_sub_assign.fsti                                  |   2 +-
 {base => head}/binary_ops/Func_test_xor_assign.fst                                   |   2 +-
 {base => head}/binary_ops/Func_test_xor_assign.fsti                                  |   2 +-
 {base => head}/bitfields/Func_read_a.fst                                             |   2 +-
 {base => head}/bitfields/Func_read_a.fsti                                            |   2 +-
 {base => head}/bitfields/Func_read_b_by_value.fst                                    |   2 +-
 {base => head}/bitfields/Func_read_b_by_value.fsti                                   |   2 +-
 {base => head}/bitfields/Func_read_flag.fst                                          |   2 +-
 {base => head}/bitfields/Func_read_flag.fsti                                         |   2 +-
 {base => head}/bitfields/Func_read_full.fst                                          |   2 +-
 {base => head}/bitfields/Func_read_full.fsti                                         |   2 +-
 {base => head}/bitfields/Func_read_nibble.fst                                        |   2 +-
 {base => head}/bitfields/Func_read_nibble.fsti                                       |   2 +-
 {base => head}/bitfields/Func_read_tdef.fst                                          |   2 +-
 {base => head}/bitfields/Func_read_tdef.fsti                                         |   2 +-
 {base => head}/bitops/Func_test_bitand.fst                                           |   2 +-
 {base => head}/bitops/Func_test_bitand.fsti                                          |   2 +-
 {base => head}/bitops/Func_test_bitnot.fst                                           |   2 +-
 {base => head}/bitops/Func_test_bitnot.fsti                                          |   2 +-
 {base => head}/bitops/Func_test_bitor.fst                                            |   2 +-
 {base => head}/bitops/Func_test_bitor.fsti                                           |   2 +-
 {base => head}/bitops/Func_test_bitxor.fst                                           |   2 +-
 {base => head}/bitops/Func_test_bitxor.fsti                                          |   2 +-
 {base => head}/bool_cast/Func_cast_pointer_to_bool.fst                               |   6 +++---
 {base => head}/bool_cast/Func_cast_pointer_to_bool.fsti                              |   6 +++---
 {base => head}/c_assert/Func_checked_add.fst                                         |   2 +-
 {base => head}/c_assert/Func_checked_add.fsti                                        |   2 +-
 {base => head}/complex_arith/Func_square.fst                                         |   2 +-
 {base => head}/complex_arith/Func_square.fsti                                        |   2 +-
 {base => head}/complex_arith/Func_sum.fst                                            |   2 +-
 {base => head}/complex_arith/Func_sum.fsti                                           |   2 +-
 {base => head}/compound_literal_member/Func_sequence_value_is_valid.fst              |   6 +++---
 {base => head}/compound_literal_member/Func_sequence_value_is_valid.fsti             |   6 +++---
 {base => head}/compound_ops/Func_test_u32_pre_decr_wrap.fst                          |   2 +-
 {base => head}/compound_ops/Func_test_u32_pre_decr_wrap.fsti                         |   2 +-
 {base => head}/compound_ops/Func_test_u64_post_decr_wrap.fst                         |   2 +-
 {base => head}/compound_ops/Func_test_u64_post_decr_wrap.fsti                        |   2 +-
 {base => head}/const_read/Func_read_val.fst                                          |   2 +-
 {base => head}/const_read/Func_read_val.fsti                                         |   2 +-
 {base => head}/decl_ref/Func_get_answer.fst                                          |   2 +-
 {base => head}/decl_ref/Func_get_answer.fsti                                         |   2 +-
 {base => head}/decl_ref/Func_get_offset.fst                                          |   2 +-
 {base => head}/decl_ref/Func_get_offset.fsti                                         |   2 +-
 {base => head}/do_while/Func_f.fst                                                   |   5 +++--
 {base => head}/do_while/Func_f.fsti                                                  |   5 +++--
 {base => head}/extern_func_ptr/Func_ext_add.fst                                      |   2 +-
 {base => head}/for_loop/Func_multiply_for.fst                                        |   2 +-
 {base => head}/for_loop/Func_multiply_for.fsti                                       |   2 +-
 {base => head}/func_call_guard/Func_read_val.fst                                     |   2 +-
 {base => head}/func_call_guard/Func_read_val.fsti                                    |   2 +-
 {base => head}/func_pointer/Func_add.fst                                             |   2 +-
 {base => head}/func_pointer/Func_add.fsti                                            |   2 +-
 {base => head}/func_pointer/Func_add_t.fst                                           |   2 +-
 {base => head}/func_pointer/Func_add_t.fsti                                          |   2 +-
 {base => head}/func_pointer/Func_apply.fst                                           |   2 +-
 {base => head}/func_pointer/Func_apply.fsti                                          |   2 +-
 {base => head}/func_pointer/Func_apply1.fst                                          |   2 +-
 {base => head}/func_pointer/Func_apply1.fsti                                         |   2 +-
 {base => head}/func_pointer/Func_apply_t.fst                                        
... (summary truncated)

Full diff: full diff artifact

Diff

diff --git base/addr_global/Func_add.fst head/addr_global/Func_add.fst
index 4265272..88d3a83 100644
--- base/addr_global/Func_add.fst
+++ head/addr_global/Func_add.fst
@@ -16,7 +16,7 @@ divergent fn func_add (var_a: Typedef_int32_t.ty_int32_t) (var_b: Typedef_int32_
   ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
+  ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/addr_global/Func_add.fsti head/addr_global/Func_add.fsti
index 10a4abc..8764ddf 100644
--- base/addr_global/Func_add.fsti
+++ head/addr_global/Func_add.fsti
@@ -16,4 +16,4 @@ returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
\ No newline at end of file
diff --git base/anon_struct/Func_frob.fst head/anon_struct/Func_frob.fst
index 604ab24..5b97c65 100644
--- base/anon_struct/Func_frob.fst
+++ head/anon_struct/Func_frob.fst
@@ -18,9 +18,9 @@ divergent fn func_frob (var_b: (ref Struct_baz.struct_baz))
       ((!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_foo var_b))) =
         (!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_bar var_b)))))
   ensures
-    (with_pure
-      (return_1 =
-        (!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_foo var_b)))))
+    (rewrites_to
+      return_1
+      ((!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_foo var_b)))))
 {
   let mut var_b = var_b;
   (Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_bar (!var_b))) :=
diff --git base/anon_struct/Func_frob.fsti head/anon_struct/Func_frob.fsti
index ce430af..46ae9c0 100644
--- base/anon_struct/Func_frob.fsti
+++ head/anon_struct/Func_frob.fsti
@@ -16,6 +16,6 @@ ensures
     ((!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_foo var_b))) =
       (!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_bar var_b)))))
 ensures
-  (with_pure
-    (return_1 =
-      (!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_foo var_b)))))
\ No newline at end of file
+  (rewrites_to
+    return_1
+    ((!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_foo var_b)))))
\ No newline at end of file
diff --git base/array_deref/Func_deref_read.fst head/array_deref/Func_deref_read.fst
index 69c752a..89db856 100644
--- base/array_deref/Func_deref_read.fst
+++ head/array_deref/Func_deref_read.fst
@@ -9,7 +9,7 @@ divergent fn func_deref_read (var_p: (array Int32.t))
   returns return_1 : Int32.t
   ensures exists* (val_p_0: (full_array_spec Int32.t)). ((array_pts_to_full var_p 1.0R val_p_0))
   ensures (with_pure ((reveal (length_of var_p)) = (old (reveal (length_of var_p)))))
-  ensures (with_pure (return_1 = ((array_read var_p 0sz))))
+  ensures (rewrites_to return_1 (((array_read var_p 0sz))))
 {
   let mut var_p = var_p;
   return ((array_read (!var_p) 0sz));
diff --git base/array_deref/Func_deref_read.fsti head/array_deref/Func_deref_read.fsti
index 6c10659..106b601 100644
--- base/array_deref/Func_deref_read.fsti
+++ head/array_deref/Func_deref_read.fsti
@@ -9,4 +9,4 @@ requires (with_pure (1 <= (reveal (length_of var_p))))
 returns return_1 : Int32.t
 ensures exists* (val_p_0: (full_array_spec Int32.t)). ((array_pts_to_full var_p 1.0R val_p_0))
 ensures (with_pure ((reveal (length_of var_p)) = (old (reveal (length_of var_p)))))
-ensures (with_pure (return_1 = ((array_read var_p 0sz))))
\ No newline at end of file
+ensures (rewrites_to return_1 (((array_read var_p 0sz))))
\ No newline at end of file
diff --git base/assign_expr/Func_chain_assign.fst head/assign_expr/Func_chain_assign.fst
index 6285a37..6c1ee61 100644
--- base/assign_expr/Func_chain_assign.fst
+++ head/assign_expr/Func_chain_assign.fst
@@ -9,7 +9,7 @@ divergent fn func_chain_assign (var_val: Typedef_int32_t.ty_int32_t)
   returns return_1 : Typedef_int32_t.ty_int32_t
   ensures ((Typedef_int32_t.ty_int32_t__pred var_val 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = var_val))
+  ensures (rewrites_to return_1 (var_val))
 {
   let mut var_val = var_val;
   let mut var_a : Typedef_int32_t.ty_int32_t;
diff --git base/assign_expr/Func_chain_assign.fsti head/assign_expr/Func_chain_assign.fsti
index b9622c0..33ce3cd 100644
--- base/assign_expr/Func_chain_assign.fsti
+++ head/assign_expr/Func_chain_assign.fsti
@@ -9,4 +9,4 @@ requires (with_pure ((0 < (id #int (Int32.v var_val))) && ((id #int (Int32.v var
 returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred var_val 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = var_val))
\ No newline at end of file
+ensures (rewrites_to return_1 (var_val))
\ No newline at end of file
diff --git base/assign_expr/Func_compound_assign_rvalue.fst head/assign_expr/Func_compound_assign_rvalue.fst
index f0d43bc..c898b49 100644
--- base/assign_expr/Func_compound_assign_rvalue.fst
+++ head/assign_expr/Func_compound_assign_rvalue.fst
@@ -9,7 +9,7 @@ divergent fn func_compound_assign_rvalue (var_x: Typedef_int32_t.ty_int32_t)
   returns return_1 : Typedef_int32_t.ty_int32_t
   ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_x `Int32.add` var_x)))
+  ensures (rewrites_to return_1 ((var_x `Int32.add` var_x)))
 {
   let mut var_x = var_x;
   let mut var_y : Typedef_int32_t.ty_int32_t;
diff --git base/assign_expr/Func_compound_assign_rvalue.fsti head/assign_expr/Func_compound_assign_rvalue.fsti
index 5607939..c1f2ad0 100644
--- base/assign_expr/Func_compound_assign_rvalue.fsti
+++ head/assign_expr/Func_compound_assign_rvalue.fsti
@@ -9,4 +9,4 @@ requires (with_pure ((0 < (id #int (Int32.v var_x))) && ((id #int (Int32.v var_x
 returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_x `Int32.add` var_x)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_x `Int32.add` var_x)))
\ No newline at end of file
diff --git base/binary_ops/Func_test_add_assign.fst head/binary_ops/Func_test_add_assign.fst
index 09222be..82a879f 100644
--- base/binary_ops/Func_test_add_assign.fst
+++ head/binary_ops/Func_test_add_assign.fst
@@ -18,7 +18,7 @@ divergent fn func_test_add_assign
   ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
+  ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/binary_ops/Func_test_add_assign.fsti head/binary_ops/Func_test_add_assign.fsti
index 281e789..45e68b7 100644
--- base/binary_ops/Func_test_add_assign.fsti
+++ head/binary_ops/Func_test_add_assign.fsti
@@ -18,4 +18,4 @@ returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
\ No newline at end of file
diff --git base/binary_ops/Func_test_and_assign.fst head/binary_ops/Func_test_and_assign.fst
index 4f908c0..b816054 100644
--- base/binary_ops/Func_test_and_assign.fst
+++ head/binary_ops/Func_test_and_assign.fst
@@ -12,7 +12,7 @@ divergent fn func_test_and_assign
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `UInt32.logand` var_b)))
+  ensures (rewrites_to return_1 ((var_a `UInt32.logand` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/binary_ops/Func_test_and_assign.fsti head/binary_ops/Func_test_and_assign.fsti
index fb5d997..6c6608c 100644
--- base/binary_ops/Func_test_and_assign.fsti
+++ head/binary_ops/Func_test_and_assign.fsti
@@ -12,4 +12,4 @@ returns return_1 : Typedef_uint32_t.ty_uint32_t
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `UInt32.logand` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `UInt32.logand` var_b)))
\ No newline at end of file
diff --git base/binary_ops/Func_test_chain.fst head/binary_ops/Func_test_chain.fst
index f37e13b..1daf8c2 100644
--- base/binary_ops/Func_test_chain.fst
+++ head/binary_ops/Func_test_chain.fst
@@ -9,7 +9,7 @@ divergent fn func_test_chain (var_x: Typedef_int32_t.ty_int32_t)
   returns return_1 : Typedef_int32_t.ty_int32_t
   ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = ((var_x `Int32.add` var_x) `Int32.add` var_x)))
+  ensures (rewrites_to return_1 (((var_x `Int32.add` var_x) `Int32.add` var_x)))
 {
   let mut var_x = var_x;
   let mut var_a : Typedef_int32_t.ty_int32_t;
diff --git base/binary_ops/Func_test_chain.fsti head/binary_ops/Func_test_chain.fsti
index 44b9a11..8fed988 100644
--- base/binary_ops/Func_test_chain.fsti
+++ head/binary_ops/Func_test_chain.fsti
@@ -9,4 +9,4 @@ requires (with_pure ((0 < (id #int (Int32.v var_x))) && ((id #int (Int32.v var_x
 returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred var_x 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = ((var_x `Int32.add` var_x) `Int32.add` var_x)))
\ No newline at end of file
+ensures (rewrites_to return_1 (((var_x `Int32.add` var_x) `Int32.add` var_x)))
\ No newline at end of file
diff --git base/binary_ops/Func_test_mul_assign.fst head/binary_ops/Func_test_mul_assign.fst
index ed4c3dc..1f60f61 100644
--- base/binary_ops/Func_test_mul_assign.fst
+++ head/binary_ops/Func_test_mul_assign.fst
@@ -18,7 +18,7 @@ divergent fn func_test_mul_assign
   ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `Int32.mul` var_b)))
+  ensures (rewrites_to return_1 ((var_a `Int32.mul` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/binary_ops/Func_test_mul_assign.fsti head/binary_ops/Func_test_mul_assign.fsti
index fc70ce0..a684ef2 100644
--- base/binary_ops/Func_test_mul_assign.fsti
+++ head/binary_ops/Func_test_mul_assign.fsti
@@ -18,4 +18,4 @@ returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `Int32.mul` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `Int32.mul` var_b)))
\ No newline at end of file
diff --git base/binary_ops/Func_test_or_assign.fst head/binary_ops/Func_test_or_assign.fst
index b82aae0..2391016 100644
--- base/binary_ops/Func_test_or_assign.fst
+++ head/binary_ops/Func_test_or_assign.fst
@@ -12,7 +12,7 @@ divergent fn func_test_or_assign
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `UInt32.logor` var_b)))
+  ensures (rewrites_to return_1 ((var_a `UInt32.logor` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/binary_ops/Func_test_or_assign.fsti head/binary_ops/Func_test_or_assign.fsti
index 4b98ab9..a82ab9d 100644
--- base/binary_ops/Func_test_or_assign.fsti
+++ head/binary_ops/Func_test_or_assign.fsti
@@ -12,4 +12,4 @@ returns return_1 : Typedef_uint32_t.ty_uint32_t
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `UInt32.logor` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `UInt32.logor` var_b)))
\ No newline at end of file
diff --git base/binary_ops/Func_test_shl_assign.fst head/binary_ops/Func_test_shl_assign.fst
index 4bfa060..4e1453e 100644
--- base/binary_ops/Func_test_shl_assign.fst
+++ head/binary_ops/Func_test_shl_assign.fst
@@ -13,7 +13,7 @@ divergent fn func_test_shl_assign
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `UInt32.shift_left` var_b)))
+  ensures (rewrites_to return_1 ((var_a `UInt32.shift_left` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/binary_ops/Func_test_shl_assign.fsti head/binary_ops/Func_test_shl_assign.fsti
index 308d72f..5904dbb 100644
--- base/binary_ops/Func_test_shl_assign.fsti
+++ head/binary_ops/Func_test_shl_assign.fsti
@@ -13,4 +13,4 @@ returns return_1 : Typedef_uint32_t.ty_uint32_t
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `UInt32.shift_left` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `UInt32.shift_left` var_b)))
\ No newline at end of file
diff --git base/binary_ops/Func_test_shr_assign.fst head/binary_ops/Func_test_shr_assign.fst
index 1adfe08..15483e8 100644
--- base/binary_ops/Func_test_shr_assign.fst
+++ head/binary_ops/Func_test_shr_assign.fst
@@ -13,7 +13,7 @@ divergent fn func_test_shr_assign
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `UInt32.shift_right` var_b)))
+  ensures (rewrites_to return_1 ((var_a `UInt32.shift_right` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/binary_ops/Func_test_shr_assign.fsti head/binary_ops/Func_test_shr_assign.fsti
index c0304e1..49a107f 100644
--- base/binary_ops/Func_test_shr_assign.fsti
+++ head/binary_ops/Func_test_shr_assign.fsti
@@ -13,4 +13,4 @@ returns return_1 : Typedef_uint32_t.ty_uint32_t
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `UInt32.shift_right` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `UInt32.shift_right` var_b)))
\ No newline at end of file
diff --git base/binary_ops/Func_test_sub_assign.fst head/binary_ops/Func_test_sub_assign.fst
index dfadb04..064120c 100644
--- base/binary_ops/Func_test_sub_assign.fst
+++ head/binary_ops/Func_test_sub_assign.fst
@@ -18,7 +18,7 @@ divergent fn func_test_sub_assign
   ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `Int32.sub` var_b)))
+  ensures (rewrites_to return_1 ((var_a `Int32.sub` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/binary_ops/Func_test_sub_assign.fsti head/binary_ops/Func_test_sub_assign.fsti
index 74a7d18..7b1551b 100644
--- base/binary_ops/Func_test_sub_assign.fsti
+++ head/binary_ops/Func_test_sub_assign.fsti
@@ -18,4 +18,4 @@ returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `Int32.sub` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `Int32.sub` var_b)))
\ No newline at end of file
diff --git base/binary_ops/Func_test_xor_assign.fst head/binary_ops/Func_test_xor_assign.fst
index b08a688..188ab00 100644
--- base/binary_ops/Func_test_xor_assign.fst
+++ head/binary_ops/Func_test_xor_assign.fst
@@ -12,7 +12,7 @@ divergent fn func_test_xor_assign
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `UInt32.logxor` var_b)))
+  ensures (rewrites_to return_1 ((var_a `UInt32.logxor` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/binary_ops/Func_test_xor_assign.fsti head/binary_ops/Func_test_xor_assign.fsti
index 1e65d9f..79266f4 100644
--- base/binary_ops/Func_test_xor_assign.fsti
+++ head/binary_ops/Func_test_xor_assign.fsti
@@ -12,4 +12,4 @@ returns return_1 : Typedef_uint32_t.ty_uint32_t
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `UInt32.logxor` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `UInt32.logxor` var_b)))
\ No newline at end of file
diff --git base/bitfields/Func_read_a.fst head/bitfields/Func_read_a.fst
index 0f37290..5855ad4 100644
--- base/bitfields/Func_read_a.fst
+++ head/bitfields/Func_read_a.fst
@@ -13,7 +13,7 @@ divergent fn func_read_a (var_s: (ref Struct_flags.struct_flags))
     exists* (val_s_0: Struct_flags.struct_flags).
     ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
       (Struct_flags.struct_flags__pred (!var_s) 1.0R))
-  ensures (with_pure (return_1 = (!(Struct_flags.struct_flags__get_a var_s))))
+  ensures (rewrites_to return_1 ((!(Struct_flags.struct_flags__get_a var_s))))
 {
   let mut var_s = var_s;
   return (!(Struct_flags.struct_flags__get_a (!var_s)));
diff --git base/bitfields/Func_read_a.fsti head/bitfields/Func_read_a.fsti
index f067204..d243663 100644
--- base/bitfields/Func_read_a.fsti
+++ head/bitfields/Func_read_a.fsti
@@ -13,4 +13,4 @@ ensures
   exists* (val_s_0: Struct_flags.struct_flags).
   ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
     (Struct_flags.struct_flags__pred (!var_s) 1.0R))
-ensures (with_pure (return_1 = (!(Struct_flags.struct_flags__get_a var_s))))
\ No newline at end of file
+ensures (rewrites_to return_1 ((!(Struct_flags.struct_flags__get_a var_s))))
\ No newline at end of file
diff --git base/bitfields/Func_read_b_by_value.fst head/bitfields/Func_read_b_by_value.fst
index 342c18e..f766b3e 100644
--- base/bitfields/Func_read_b_by_value.fst
+++ head/bitfields/Func_read_b_by_value.fst
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 divergent fn func_read_b_by_value (var_s: Struct_flags.struct_flags)
   returns return_1 : UInt32.t
-  ensures (with_pure (return_1 = (var_s).Struct_flags.struct_flags__b))
+  ensures (rewrites_to return_1 ((var_s).Struct_flags.struct_flags__b))
 {
   let mut var_s = var_s;
   return (!(Struct_flags.struct_flags__get_b var_s));
diff --git base/bitfields/Func_read_b_by_value.fsti head/bitfields/Func_read_b_by_value.fsti
index fc1c696..440ca6c 100644
--- base/bitfields/Func_read_b_by_value.fsti
+++ head/bitfields/Func_read_b_by_value.fsti
@@ -5,4 +5,4 @@ open Pulse.Lib.C
 
 divergent fn func_read_b_by_value (var_s: Struct_flags.struct_flags)
 returns return_1 : UInt32.t
-ensures (with_pure (return_1 = (var_s).Struct_flags.struct_flags__b))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_s).Struct_flags.struct_flags__b))
\ No newline at end of file
diff --git base/bitfields/Func_read_flag.fst head/bitfields/Func_read_flag.fst
index 0719ee6..4e24fd5 100644
--- base/bitfields/Func_read_flag.fst
+++ head/bitfields/Func_read_flag.fst
@@ -13,7 +13,7 @@ divergent fn func_read_flag (var_s: (ref Struct_bits.struct_bits))
     exists* (val_s_0: Struct_bits.struct_bits).
     ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
       (Struct_bits.struct_bits__pred (!var_s) 1.0R))
-  ensures (with_pure (return_1 = (!(Struct_bits.struct_bits__get_flag var_s))))
+  ensures (rewrites_to return_1 ((!(Struct_bits.struct_bits__get_flag var_s))))
 {
   let mut var_s = var_s;
   return (!(Struct_bits.struct_bits__get_flag (!var_s)));
diff --git base/bitfields/Func_read_flag.fsti head/bitfields/Func_read_flag.fsti
index fecfbe3..ef40dff 100644
--- base/bitfields/Func_read_flag.fsti
+++ head/bitfields/Func_read_flag.fsti
@@ -13,4 +13,4 @@ ensures
   exists* (val_s_0: Struct_bits.struct_bits).
   ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
     (Struct_bits.struct_bits__pred (!var_s) 1.0R))
-ensures (with_pure (return_1 = (!(Struct_bits.struct_bits__get_flag var_s))))
\ No newline at end of file
+ensures (rewrites_to return_1 ((!(Struct_bits.struct_bits__get_flag var_s))))
\ No newline at end of file
diff --git base/bitfields/Func_read_full.fst head/bitfields/Func_read_full.fst
index da3cbdc..906ce54 100644
--- base/bitfields/Func_read_full.fst
+++ head/bitfields/Func_read_full.fst
@@ -13,7 +13,7 @@ divergent fn func_read_full (var_s: (ref Struct_flags.struct_flags))
     exists* (val_s_0: Struct_flags.struct_flags).
     ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
       (Struct_flags.struct_flags__pred (!var_s) 1.0R))
-  ensures (with_pure (return_1 = (!(Struct_flags.struct_flags__get_full var_s))))
+  ensures (rewrites_to return_1 ((!(Struct_flags.struct_flags__get_full var_s))))
 {
   let mut var_s = var_s;
   return (!(Struct_flags.struct_flags__get_full (!var_s)));
diff --git base/bitfields/Func_read_full.fsti head/bitfields/Func_read_full.fsti
index 986c490..ac14af1 100644
--- base/bitfields/Func_read_full.fsti
+++ head/bitfields/Func_read_full.fsti
@@ -13,4 +13,4 @@ ensures
   exists* (val_s_0: Struct_flags.struct_flags).
   ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
     (Struct_flags.struct_flags__pred (!var_s) 1.0R))
-ensures (with_pure (return_1 = (!(Struct_flags.struct_flags__get_full var_s))))
\ No newline at end of file
+ensures (rewrites_to return_1 ((!(Struct_flags.struct_flags__get_full var_s))))
\ No newline at end of file
diff --git base/bitfields/Func_read_nibble.fst head/bitfields/Func_read_nibble.fst
index 6389432..ddb107a 100644
--- base/bitfields/Func_read_nibble.fst
+++ head/bitfields/Func_read_nibble.fst
@@ -13,7 +13,7 @@ divergent fn func_read_nibble (var_s: (ref Struct_bits.struct_bits))
     exists* (val_s_0: Struct_bits.struct_bits).
     ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
       (Struct_bits.struct_bits__pred (!var_s) 1.0R))
-  ensures (with_pure (return_1 = (!(Struct_bits.struct_bits__get_nibble var_s))))
+  ensures (rewrites_to return_1 ((!(Struct_bits.struct_bits__get_nibble var_s))))
 {
   let mut var_s = var_s;
   return (!(Struct_bits.struct_bits__get_nibble (!var_s)));
diff --git base/bitfields/Func_read_nibble.fsti head/bitfields/Func_read_nibble.fsti
index ed8fabb..7478289 100644
--- base/bitfields/Func_read_nibble.fsti
+++ head/bitfields/Func_read_nibble.fsti
@@ -13,4 +13,4 @@ ensures
   exists* (val_s_0: Struct_bits.struct_bits).
   ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
     (Struct_bits.struct_bits__pred (!var_s) 1.0R))
-ensures (with_pure (return_1 = (!(Struct_bits.struct_bits__get_nibble var_s))))
\ No newline at end of file
+ensures (rewrites_to return_1 ((!(Struct_bits.struct_bits__get_nibble var_s))))
\ No newline at end of file
diff --git base/bitfields/Func_read_tdef.fst head/bitfields/Func_read_tdef.fst
index fd1e6a8..73c5c76 100644
--- base/bitfields/Func_read_tdef.fst
+++ head/bitfields/Func_read_tdef.fst
@@ -14,7 +14,7 @@ divergent fn func_read_tdef (var_s: (ref Struct_tdef.struct_tdef))
     ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
       (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
   ensures ((Typedef_uint16_t.ty_uint16_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (!(Struct_tdef.struct_tdef__get_a var_s))))
+  ensures (rewrites_to return_1 ((!(Struct_tdef.struct_tdef__get_a var_s))))
 {
   let mut var_s = var_s;
   return (!(Struct_tdef.struct_tdef__get_a (!var_s)));
diff --git base/bitfields/Func_read_tdef.fsti head/bitfields/Func_read_tdef.fsti
index af5c5e5..26ef0a5 100644
--- base/bitfields/Func_read_tdef.fsti
+++ head/bitfields/Func_read_tdef.fsti
@@ -14,4 +14,4 @@ ensures
   ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) **
     (Struct_tdef.struct_tdef__pred (!var_s) 1.0R))
 ensures ((Typedef_uint16_t.ty_uint16_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (!(Struct_tdef.struct_tdef__get_a var_s))))
\ No newline at end of file
+ensures (rewrites_to return_1 ((!(Struct_tdef.struct_tdef__get_a var_s))))
\ No newline at end of file
diff --git base/bitops/Func_test_bitand.fst head/bitops/Func_test_bitand.fst
index 30d8d6b..a5ced79 100644
--- base/bitops/Func_test_bitand.fst
+++ head/bitops/Func_test_bitand.fst
@@ -12,7 +12,7 @@ divergent fn func_test_bitand
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `UInt32.logand` var_b)))
+  ensures (rewrites_to return_1 ((var_a `UInt32.logand` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/bitops/Func_test_bitand.fsti head/bitops/Func_test_bitand.fsti
index 2ff1953..f309c1a 100644
--- base/bitops/Func_test_bitand.fsti
+++ head/bitops/Func_test_bitand.fsti
@@ -12,4 +12,4 @@ returns return_1 : Typedef_uint32_t.ty_uint32_t
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `UInt32.logand` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `UInt32.logand` var_b)))
\ No newline at end of file
diff --git base/bitops/Func_test_bitnot.fst head/bitops/Func_test_bitnot.fst
index 7afd3a0..746e6de 100644
--- base/bitops/Func_test_bitnot.fst
+++ head/bitops/Func_test_bitnot.fst
@@ -8,7 +8,7 @@ divergent fn func_test_bitnot (var_a: Typedef_uint32_t.ty_uint32_t)
   returns return_1 : Typedef_uint32_t.ty_uint32_t
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (UInt32.lognot var_a)))
+  ensures (rewrites_to return_1 ((UInt32.lognot var_a)))
 {
   let mut var_a = var_a;
   return (UInt32.lognot (!var_a));
diff --git base/bitops/Func_test_bitnot.fsti head/bitops/Func_test_bitnot.fsti
index a42903b..959f96e 100644
--- base/bitops/Func_test_bitnot.fsti
+++ head/bitops/Func_test_bitnot.fsti
@@ -8,4 +8,4 @@ requires ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
 returns return_1 : Typedef_uint32_t.ty_uint32_t
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (UInt32.lognot var_a)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((UInt32.lognot var_a)))
\ No newline at end of file
diff --git base/bitops/Func_test_bitor.fst head/bitops/Func_test_bitor.fst
index a21ca4d..8a1c3d2 100644
--- base/bitops/Func_test_bitor.fst
+++ head/bitops/Func_test_bitor.fst
@@ -12,7 +12,7 @@ divergent fn func_test_bitor
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `UInt32.logor` var_b)))
+  ensures (rewrites_to return_1 ((var_a `UInt32.logor` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/bitops/Func_test_bitor.fsti head/bitops/Func_test_bitor.fsti
index 4cc3798..d95c689 100644
--- base/bitops/Func_test_bitor.fsti
+++ head/bitops/Func_test_bitor.fsti
@@ -12,4 +12,4 @@ returns return_1 : Typedef_uint32_t.ty_uint32_t
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `UInt32.logor` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `UInt32.logor` var_b)))
\ No newline at end of file
diff --git base/bitops/Func_test_bitxor.fst head/bitops/Func_test_bitxor.fst
index e4ebb9b..7db4d48 100644
--- base/bitops/Func_test_bitxor.fst
+++ head/bitops/Func_test_bitxor.fst
@@ -12,7 +12,7 @@ divergent fn func_test_bitxor
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `UInt32.logxor` var_b)))
+  ensures (rewrites_to return_1 ((var_a `UInt32.logxor` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/bitops/Func_test_bitxor.fsti head/bitops/Func_test_bitxor.fsti
index d8d483f..f212223 100644
--- base/bitops/Func_test_bitxor.fsti
+++ head/bitops/Func_test_bitxor.fsti
@@ -12,4 +12,4 @@ returns return_1 : Typedef_uint32_t.ty_uint32_t
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_a 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_b 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `UInt32.logxor` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `UInt32.logxor` var_b)))
\ No newline at end of file
diff --git base/bool_cast/Func_cast_pointer_to_bool.fst head/bool_cast/Func_cast_pointer_to_bool.fst
index f67cd53..38292cf 100644
--- base/bool_cast/Func_cast_pointer_to_bool.fst
+++ head/bool_cast/Func_cast_pointer_to_bool.fst
@@ -5,9 +5,9 @@ open Pulse.Lib.C
 
 divergent fn func_cast_pointer_to_bool (var_x: (ref Int32.t))
   returns return_1 : bool
-  ensures (with_pure (return_1 = (not (Pulse.Lib.Reference.is_null var_x))))
-  ensures (with_pure (return_1 = (not (Pulse.Lib.Reference.is_null var_x))))
-  ensures (with_pure (return_1 = (not (var_x `Pulse.Lib.C.Ref.ref_eq` null))))
+  ensures (rewrites_to return_1 ((not (Pulse.Lib.Reference.is_null var_x))))
+  ensures (rewrites_to return_1 ((not (Pulse.Lib.Reference.is_null var_x))))
+  ensures (rewrites_to return_1 ((not (var_x `Pulse.Lib.C.Ref.ref_eq` null))))
 {
   let mut var_x = var_x;
   return (not (Pulse.Lib.Reference.is_null (!var_x)));
diff --git base/bool_cast/Func_cast_pointer_to_bool.fsti head/bool_cast/Func_cast_pointer_to_bool.fsti
index 1b181c4..6174473 100644
--- base/bool_cast/Func_cast_pointer_to_bool.fsti
+++ head/bool_cast/Func_cast_pointer_to_bool.fsti
@@ -5,6 +5,6 @@ open Pulse.Lib.C
 
 divergent fn func_cast_pointer_to_bool (var_x: (ref Int32.t))
 returns return_1 : bool
-ensures (with_pure (return_1 = (not (Pulse.Lib.Reference.is_null var_x))))
-ensures (with_pure (return_1 = (not (Pulse.Lib.Reference.is_null var_x))))
-ensures (with_pure (return_1 = (not (var_x `Pulse.Lib.C.Ref.ref_eq` null))))
\ No newline at end of file
+ensures (rewrites_to return_1 ((not (Pulse.Lib.Reference.is_null var_x))))
+ensures (rewrites_to return_1 ((not (Pulse.Lib.Reference.is_null var_x))))
+ensures (rewrites_to return_1 ((not (var_x `Pulse.Lib.C.Ref.ref_eq` null))))
\ No newline at end of file
diff --git base/c_assert/Func_checked_add.fst head/c_assert/Func_checked_add.fst
index 6c9356e..160e42b 100644
--- base/c_assert/Func_checked_add.fst
+++ head/c_assert/Func_checked_add.fst
@@ -18,7 +18,7 @@ divergent fn func_checked_add
   ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
+  ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/c_assert/Func_checked_add.fsti head/c_assert/Func_checked_add.fsti
index 3d3416c..124d6f9 100644
--- base/c_assert/Func_checked_add.fsti
+++ head/c_assert/Func_checked_add.fsti
@@ -18,4 +18,4 @@ returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
\ No newline at end of file
diff --git base/complex_arith/Func_square.fst head/complex_arith/Func_square.fst
index 8ebe2d1..ae874a2 100644
--- base/complex_arith/Func_square.fst
+++ head/complex_arith/Func_square.fst
@@ -7,7 +7,7 @@ divergent fn func_square (var_x: Int32.t)
   requires
     (with_pure (Let_int_fits.func_int_fits ((id #int (Int32.v var_x)) * (id #int (Int32.v var_x)))))
   returns return_1 : Int32.t
-  ensures (with_pure (return_1 = (var_x `Int32.mul` var_x)))
+  ensures (rewrites_to return_1 ((var_x `Int32.mul` var_x)))
 {
   let mut var_x = var_x;
   return ((!var_x) `Int32.mul` (!var_x));
diff --git base/complex_arith/Func_square.fsti head/complex_arith/Func_square.fsti
index 2e1ae30..6e8a25c 100644
--- base/complex_arith/Func_square.fsti
+++ head/complex_arith/Func_square.fsti
@@ -7,4 +7,4 @@ divergent fn func_square (var_x: Int32.t)
 requires
   (with_pure (Let_int_fits.func_int_fits ((id #int (Int32.v var_x)) * (id #int (Int32.v var_x)))))
 returns return_1 : Int32.t
-ensures (with_pure (return_1 = (var_x `Int32.mul` var_x)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_x `Int32.mul` var_x)))
\ No newline at end of file
diff --git base/complex_arith/Func_sum.fst head/complex_arith/Func_sum.fst
index 97dcb7e..518770d 100644
--- base/complex_arith/Func_sum.fst
+++ head/complex_arith/Func_sum.fst
@@ -7,7 +7,7 @@ divergent fn func_sum (var_x: Int32.t) (var_y: Int32.t)
   requires
     (with_pure (Let_int_fits.func_int_fits ((id #int (Int32.v var_x)) + (id #int (Int32.v var_y)))))
   returns return_1 : Int32.t
-  ensures (with_pure (return_1 = (var_x `Int32.add` var_y)))
+  ensures (rewrites_to return_1 ((var_x `Int32.add` var_y)))
 {
   let mut var_x = var_x;
   let mut var_y = var_y;
diff --git base/complex_arith/Func_sum.fsti head/complex_arith/Func_sum.fsti
index 7fff28b..286ec98 100644
--- base/complex_arith/Func_sum.fsti
+++ head/complex_arith/Func_sum.fsti
@@ -7,4 +7,4 @@ divergent fn func_sum (var_x: Int32.t) (var_y: Int32.t)
 requires
   (with_pure (Let_int_fits.func_int_fits ((id #int (Int32.v var_x)) + (id #int (Int32.v var_y)))))
 returns return_1 : Int32.t
-ensures (with_pure (return_1 = (var_x `Int32.add` var_y)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_x `Int32.add` var_y)))
\ No newline at end of file
diff --git base/compound_literal_member/Func_sequence_value_is_valid.fst head/compound_literal_member/Func_sequence_value_is_valid.fst
index 3348c43..9278b81 100644
--- base/compound_literal_member/Func_sequence_value_is_valid.fst
+++ head/compound_literal_member/Func_sequence_value_is_valid.fst
@@ -8,9 +8,9 @@ divergent fn func_sequence_value_is_valid (var_value: Typedef_SEQUENCE_VALUE.ty_
   returns return_1 : bool
   ensures ((Typedef_SEQUENCE_VALUE.ty_sequence_value__pred var_value 1.0R))
   ensures
-    (with_pure
-      (return_1 =
-        (not
+    (rewrites_to
+      return_1
+      ((not
           ((id #int (UInt64.v (var_value).Struct__SEQUENCE_VALUE.struct__sequence_value__value)) =
             0))))
 {
diff --git base/compound_literal_member/Func_sequence_value_is_valid.fsti head/compound_literal_member/Func_sequence_value_is_valid.fsti
index f6413fc..392694a 100644
--- base/compound_literal_member/Func_sequence_value_is_valid.fsti
+++ head/compound_literal_member/Func_sequence_value_is_valid.fsti
@@ -8,8 +8,8 @@ requires ((Typedef_SEQUENCE_VALUE.ty_sequence_value__pred var_value 1.0R))
 returns return_1 : bool
 ensures ((Typedef_SEQUENCE_VALUE.ty_sequence_value__pred var_value 1.0R))
 ensures
-  (with_pure
-    (return_1 =
-      (not
+  (rewrites_to
+    return_1
+    ((not
         ((id #int (UInt64.v (var_value).Struct__SEQUENCE_VALUE.struct__sequence_value__value)) =
           0))))
\ No newline at end of file
diff --git base/compound_ops/Func_test_u32_pre_decr_wrap.fst head/compound_ops/Func_test_u32_pre_decr_wrap.fst
index 374f65d..6edfaa9 100644
--- base/compound_ops/Func_test_u32_pre_decr_wrap.fst
+++ head/compound_ops/Func_test_u32_pre_decr_wrap.fst
@@ -6,7 +6,7 @@ open Pulse.Lib.C
 divergent fn func_test_u32_pre_decr_wrap ()
   returns return_1 : Typedef_uint32_t.ty_uint32_t
   ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = 4294967295ul))
+  ensures (rewrites_to return_1 (4294967295ul))
 {
   let mut var_a : Typedef_uint32_t.ty_uint32_t;
   var_a := (id #UInt32.t (Int.Cast.int32_to_uint32 0l));
diff --git base/compound_ops/Func_test_u32_pre_decr_wrap.fsti head/compound_ops/Func_test_u32_pre_decr_wrap.fsti
index 9908e18..b76d60d 100644
--- base/compound_ops/Func_test_u32_pre_decr_wrap.fsti
+++ head/compound_ops/Func_test_u32_pre_decr_wrap.fsti
@@ -6,4 +6,4 @@ open Pulse.Lib.C
 divergent fn func_test_u32_pre_decr_wrap ()
 returns return_1 : Typedef_uint32_t.ty_uint32_t
 ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = 4294967295ul))
\ No newline at end of file
+ensures (rewrites_to return_1 (4294967295ul))
\ No newline at end of file
diff --git base/compound_ops/Func_test_u64_post_decr_wrap.fst head/compound_ops/Func_test_u64_post_decr_wrap.fst
index 195e076..b8343ba 100644
--- base/compound_ops/Func_test_u64_post_decr_wrap.fst
+++ head/compound_ops/Func_test_u64_post_decr_wrap.fst
@@ -6,7 +6,7 @@ open Pulse.Lib.C
 divergent fn func_test_u64_post_decr_wrap ()
   returns return_1 : Typedef_uint64_t.ty_uint64_t
   ensures ((Typedef_uint64_t.ty_uint64_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (UInt64.uint_to_t 18446744073709551615)))
+  ensures (rewrites_to return_1 ((UInt64.uint_to_t 18446744073709551615)))
 {
   let mut var_a : Typedef_uint64_t.ty_uint64_t;
   var_a := (id #UInt64.t (Int.Cast.int32_to_uint64 0l));
diff --git base/compound_ops/Func_test_u64_post_decr_wrap.fsti head/compound_ops/Func_test_u64_post_decr_wrap.fsti
index d6bc3bc..9fa4043 100644
--- base/compound_ops/Func_test_u64_post_decr_wrap.fsti
+++ head/compound_ops/Func_test_u64_post_decr_wrap.fsti
@@ -6,4 +6,4 @@ open Pulse.Lib.C
 divergent fn func_test_u64_post_decr_wrap ()
 returns return_1 : Typedef_uint64_t.ty_uint64_t
 ensures ((Typedef_uint64_t.ty_uint64_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (UInt64.uint_to_t 18446744073709551615)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((UInt64.uint_to_t 18446744073709551615)))
\ No newline at end of file
diff --git base/const_read/Func_read_val.fst head/const_read/Func_read_val.fst
index a5ac951..ef7e3ce 100644
--- base/const_read/Func_read_val.fst
+++ head/const_read/Func_read_val.fst
@@ -6,7 +6,7 @@ open Pulse.Lib.C
 divergent fn func_read_val (var_x: (ref Int32.t))
   preserves (Pulse.Lib.Reference.pts_to var_x #'p_x_0 'val_x_0)
   returns return_1 : Int32.t
-  ensures (with_pure (return_1 = (!var_x)))
+  ensures (rewrites_to return_1 ((!var_x)))
 {
   let mut var_x = var_x;
   return (!(!var_x));
diff --git base/const_read/Func_read_val.fsti head/const_read/Func_read_val.fsti
index cd71e23..9ba9415 100644
--- base/const_read/Func_read_val.fsti
+++ head/const_read/Func_read_val.fsti
@@ -6,4 +6,4 @@ open Pulse.Lib.C
 divergent fn func_read_val (var_x: (ref Int32.t))
 preserves (Pulse.Lib.Reference.pts_to var_x #'p_x_0 'val_x_0)
 returns return_1 : Int32.t
-ensures (with_pure (return_1 = (!var_x)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((!var_x)))
\ No newline at end of file
diff --git base/decl_ref/Func_get_answer.fst head/decl_ref/Func_get_answer.fst
index 7598bb3..0c4fb8a 100644
--- base/decl_ref/Func_get_answer.fst
+++ head/decl_ref/Func_get_answer.fst
@@ -6,7 +6,7 @@ open Pulse.Lib.C
 divergent fn func_get_answer ()
   returns return_1 : Typedef_int32_t.ty_int32_t
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = Global_ANSWER.var_answer))
+  ensures (rewrites_to return_1 (Global_ANSWER.var_answer))
 {
   return Global_ANSWER.var_answer;
 }
\ No newline at end of file
diff --git base/decl_ref/Func_get_answer.fsti head/decl_ref/Func_get_answer.fsti
index 3feffe0..7fa5ce5 100644
--- base/decl_ref/Func_get_answer.fsti
+++ head/decl_ref/Func_get_answer.fsti
@@ -6,4 +6,4 @@ open Pulse.Lib.C
 divergent fn func_get_answer ()
 returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = Global_ANSWER.var_answer))
\ No newline at end of file
+ensures (rewrites_to return_1 (Global_ANSWER.var_answer))
\ No newline at end of file
diff --git base/decl_ref/Func_get_offset.fst head/decl_ref/Func_get_offset.fst
index 13ed435..46a890d 100644
--- base/decl_ref/Func_get_offset.fst
+++ head/decl_ref/Func_get_offset.fst
@@ -6,7 +6,7 @@ open Pulse.Lib.C
 divergent fn func_get_offset ()
   returns return_1 : Typedef_int32_t.ty_int32_t
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = Global_OFFSET.var_offset))
+  ensures (rewrites_to return_1 (Global_OFFSET.var_offset))
 {
   return Global_OFFSET.var_offset;
 }
\ No newline at end of file
diff --git base/decl_ref/Func_get_offset.fsti head/decl_ref/Func_get_offset.fsti
index f85f4b6..501435f 100644
--- base/decl_ref/Func_get_offset.fsti
+++ head/decl_ref/Func_get_offset.fsti
@@ -6,4 +6,4 @@ open Pulse.Lib.C
 divergent fn func_get_offset ()
 returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = Global_OFFSET.var_offset))
\ No newline at end of file
+ensures (rewrites_to return_1 (Global_OFFSET.var_offset))
\ No newline at end of file
diff --git base/do_while/Func_f.fst head/do_while/Func_f.fst
index 67ae61c..c5479ff 100644
--- base/do_while/Func_f.fst
+++ head/do_while/Func_f.fst
@@ -22,8 +22,9 @@ divergent fn func_f (var_s: (ref Struct_counter.struct_counter))
       ((id #int (Int32.v (!(Struct_counter.struct_counter__get_x var_s)))) =
         ((id #int (Int32.v (old (!(Struct_counter.struct_counter__get_x var_s))))) + 1)))
   ensures
-    (with_pure
-      (return_1 = ((id #int (Int32.v (!(Struct_counter.struct_counter__get_x var_s)))) < 10)))
+    (rewrites_to
+      return_1
+      (((id #int (Int32.v (!(Struct_counter.struct_counter__get_x var_s)))) < 10)))
 {
   let mut var_s = var_s;
   (Struct_counter.struct_counter__get_x (!var_s)) :=
diff --git base/do_while/Func_f.fsti head/do_while/Func_f.fsti
index c8a3ee7..3866ed4 100644
--- base/do_while/Func_f.fsti
+++ head/do_while/Func_f.fsti
@@ -22,5 +22,6 @@ ensures
     ((id #int (Int32.v (!(Struct_counter.struct_counter__get_x var_s)))) =
       ((id #int (Int32.v (old (!(Struct_counter.struct_counter__get_x var_s))))) + 1)))
 ensures
-  (with_pure
-    (return_1 = ((id #int (Int32.v (!(Struct_counter.struct_counter__get_x var_s)))) < 10)))
\ No newline at end of file
+  (rewrites_to
+    return_1
+    (((id #int (Int32.v (!(Struct_counter.struct_counter__get_x var_s)))) < 10)))
\ No newline at end of file
diff --git base/extern_func_ptr/Func_ext_add.fst head/extern_func_ptr/Func_ext_add.fst
index dd9da75..e997a40 100644
--- base/extern_func_ptr/Func_ext_add.fst
+++ head/extern_func_ptr/Func_ext_add.fst
@@ -16,5 +16,5 @@ divergent fn func_ext_add (var_a: Typedef_int32_t.ty_int32_t) (var_b: Typedef_in
   ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
+  ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
 { assume pure False; unreachable () }
\ No newline at end of file
diff --git base/for_loop/Func_multiply_for.fst head/for_loop/Func_multiply_for.fst
index 218eeb8..fcaef67 100644
--- base/for_loop/Func_multiply_for.fst
+++ head/for_loop/Func_multiply_for.fst
@@ -16,7 +16,7 @@ divergent fn func_multiply_for
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_x 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred var_y 1.0R))
   ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_x `Pulse.Lib.C.UInt32.mul_wrap` var_y)))
+  ensures (rewrites_to return_1 ((var_x `Pulse.Lib.C.UInt32.mul_wrap` var_y)))
 {
   let mut var_x = var_x;
   let mut var_y = var_y;
diff --git base/for_loop/Func_multiply_for.fsti head/for_loop/Func_multiply_for.fsti
index 7fc65a7..cf2cb47 100644
--- base/for_loop/Func_multiply_for.fsti
+++ head/for_loop/Func_multiply_for.fsti
@@ -16,4 +16,4 @@ returns return_1 : Typedef_uint32_t.ty_uint32_t
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_x 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred var_y 1.0R))
 ensures ((Typedef_uint32_t.ty_uint32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_x `Pulse.Lib.C.UInt32.mul_wrap` var_y)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_x `Pulse.Lib.C.UInt32.mul_wrap` var_y)))
\ No newline at end of file
diff --git base/func_call_guard/Func_read_val.fst head/func_call_guard/Func_read_val.fst
index a5ac951..ef7e3ce 100644
--- base/func_call_guard/Func_read_val.fst
+++ head/func_call_guard/Func_read_val.fst
@@ -6,7 +6,7 @@ open Pulse.Lib.C
 divergent fn func_read_val (var_x: (ref Int32.t))
   preserves (Pulse.Lib.Reference.pts_to var_x #'p_x_0 'val_x_0)
   returns return_1 : Int32.t
-  ensures (with_pure (return_1 = (!var_x)))
+  ensures (rewrites_to return_1 ((!var_x)))
 {
   let mut var_x = var_x;
   return (!(!var_x));
diff --git base/func_call_guard/Func_read_val.fsti head/func_call_guard/Func_read_val.fsti
index cd71e23..9ba9415 100644
--- base/func_call_guard/Func_read_val.fsti
+++ head/func_call_guard/Func_read_val.fsti
@@ -6,4 +6,4 @@ open Pulse.Lib.C
 divergent fn func_read_val (var_x: (ref Int32.t))
 preserves (Pulse.Lib.Reference.pts_to var_x #'p_x_0 'val_x_0)
 returns return_1 : Int32.t
-ensures (with_pure (return_1 = (!var_x)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((!var_x)))
\ No newline at end of file
diff --git base/func_pointer/Func_add.fst head/func_pointer/Func_add.fst
index 4265272..88d3a83 100644
--- base/func_pointer/Func_add.fst
+++ head/func_pointer/Func_add.fst
@@ -16,7 +16,7 @@ divergent fn func_add (var_a: Typedef_int32_t.ty_int32_t) (var_b: Typedef_int32_
   ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
+  ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/func_pointer/Func_add.fsti head/func_pointer/Func_add.fsti
index 10a4abc..8764ddf 100644
--- base/func_pointer/Func_add.fsti
+++ head/func_pointer/Func_add.fsti
@@ -16,4 +16,4 @@ returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
\ No newline at end of file
diff --git base/func_pointer/Func_add_t.fst head/func_pointer/Func_add_t.fst
index f76d1de..3c0fbd2 100644
--- base/func_pointer/Func_add_t.fst
+++ head/func_pointer/Func_add_t.fst
@@ -16,7 +16,7 @@ fn func_add_t (var_a: Typedef_int32_t.ty_int32_t) (var_b: Typedef_int32_t.ty_int
   ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
+  ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
 {
   let mut var_a = var_a;
   let mut var_b = var_b;
diff --git base/func_pointer/Func_add_t.fsti head/func_pointer/Func_add_t.fsti
index a40677d..d929fac 100644
--- base/func_pointer/Func_add_t.fsti
+++ head/func_pointer/Func_add_t.fsti
@@ -16,4 +16,4 @@ returns return_1 : Typedef_int32_t.ty_int32_t
 ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
\ No newline at end of file
diff --git base/func_pointer/Func_apply.fst head/func_pointer/Func_apply.fst
index 235ecd1..a19ea90 100644
--- base/func_pointer/Func_apply.fst
+++ head/func_pointer/Func_apply.fst
@@ -28,7 +28,7 @@ divergent fn func_apply
   ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
   ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-  ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
+  ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
 {
   let mut var_op = var_op;
   let mut var_a = var_a;
diff --git base/func_pointer/Func_apply.fsti head/func_pointer/Func_apply.fsti
index 62a2e6d..51af08f 100644
--- base/func_pointer/Func_apply.fsti
+++ head/func_pointer/Func_apply.fsti
@@ -28,4 +28,4 @@ ensures
 ensures ((Typedef_int32_t.ty_int32_t__pred var_a 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred var_b 1.0R))
 ensures ((Typedef_int32_t.ty_int32_t__pred return_1 1.0R))
-ensures (with_pure (return_1 = (var_a `Int32.add` var_b)))
\ No newline at end of file
+ensures (rewrites_to return_1 ((var_a `Int32.add` var_b)))
\ No newline at end of file
diff --git base/func_pointer/Func_apply1.fst head/func_pointer/Func_apply1.fst
index f8db71c..899db16 100644
--- base/func_pointer/Func_apply1.fst
+++ head/func_pointer/Func_apply1.fst
@@ -18,7 +18,7 @@ divergent fn func_apply1

Diff truncated; see the links above for the full version.

nikswamy and others added 8 commits August 18, 2026 15:26

Merge branch 'nswamy/pal-pr28-nullable-caller-transfer' into nswamy/p…

2e051d4

…al-pr26-rewrites-to

Navigation Menu

Uh oh!

Emit a result-determining postcondition as rewrites_to - #240

Emit a result-determining postcondition as rewrites_to#240
nikswamy wants to merge 8 commits into
nswamy/pal-pr25-rvalue-memberfrom
nswamy/pal-pr26-rewrites-to

nikswamy commented Aug 19, 2026

Uh oh!

gebner commented Aug 26, 2026

Uh oh!

github-actions Bot commented Aug 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

nikswamy commented Aug 19, 2026

Commits

Testing

Uh oh!

gebner commented Aug 26, 2026

Uh oh!

github-actions Bot commented Aug 26, 2026

Generated F* output diff

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants