Ghost arguments for function pointers

[hei411]

A function whose contract uses _ghost_arg could not have its address taken.
The emitted __fp wrapper gave the ghost no binder, so its name was free and,
being unregistered, was lowered as a C-variable read (!var_v) — the interface
did not typecheck. An indirect call site had nowhere to put a ghost either:
call_div takes one erased witness, and a plain call emitted hide ().

This widens that witness. Where it was the elim tuple alone it is now
(elims & ghosts), the wrapper projects the ghost bindings out of the second
component, and a call site emits hide (elims, (_, .., _)).

Three things are worth flagging for review:

• The struct field must repeat the _ghost_args. An indirect call has no
  callee declaration; its only information is the static type it is calling
  through. So ghost_args is now carried on TypeT::FnPtr as well as on
  FnDecl. It is not part of the pointer's F* type and vtype_eq ignores
  it, so it does not affect assignability — annotations are needed only where
  you call, never where you assign. The same applies to a local
  function-pointer variable, which can carry _ghost_arg too.

• The ghost tuple's spine is written out, not left as one hole. Pulse
  solves a hole standing for a tuple leaf but not one standing for a whole
  tuple, since snd (reveal ?u) is inert until ?u is a real Mktuple2.

• The (elims & ghosts) pair is introduced only when ghosts exist.
  Unconditionally pairing would give every ordinary function pointer a unit
  ghost slot that nothing constrains, which a call site could then fill only by
  writing () literally.

Nested projection out of the widened witness relies on FStarLang/FStar#4492,
which is in the pinned nightly.

test/ghost_fnptr/ covers one ghost, two ghosts, a mixed case with two owned
pointers and two ghosts (witness nested on both sides), a no-ghost control,
calls through a global struct ops, and a call through a local function
pointer. It also exercises a field-level _refine carrying a deliberately
weaker is_valid, reached via FuncPtr.weaken, so that a returned
struct ops * hands out a callable m with no of_fn_div_valid at the call
site.

[github-actions]

Generated F* output diff

Effect of this pull request on the F* code pal generates for the test suite (a9ebbed → f9940f4).

Summary

 {base => head}/addr_global/Func_call_via_addr_of_global_struct.fst               |   2 +-
 {base => head}/addr_global/Funcptr_add.fst                                       |   4 +-
 {base => head}/addr_global/Funcptr_add.fsti                                      |   2 +-
 {base => head}/anon_struct/Func_frob.fst                                         |   6 +--
 {base => head}/anon_struct/Func_frob.fsti                                        |   4 +-
 {base => head}/anon_struct/Func_use_profiles.fst                                 |   4 +-
 {base => head}/anon_struct/Func_use_profiles.fsti                                |   4 +-
 {base => head}/anon_struct/Struct_profiles_anon_1.fst                            |  45 ++++++++------------
 {base => head}/antiquot/Func_test_declare.fst                                    |   4 +-
 {base => head}/antiquot/Func_test_declare.fsti                                   |   4 +-
 {base => head}/array_addressof_loses_index/Func_get_via_addressof_const.fst      |   4 +-
 {base => head}/array_addressof_loses_index/Func_get_via_addressof_const.fsti     |   4 +-
 {base => head}/array_typedef_pointer/Typedef_PCE.fst                             |   2 +-
 {base => head}/array_typedef_pointer/Typedef_PE.fst                              |   2 +-
 {base => head}/bitfields/Func_read_a.fst                                         |   4 +-
 {base => head}/bitfields/Func_read_a.fsti                                        |   4 +-
 {base => head}/bitfields/Func_read_flag.fst                                      |   4 +-
 {base => head}/bitfields/Func_read_flag.fsti                                     |   6 +--
 {base => head}/bitfields/Func_read_full.fst                                      |   4 +-
 {base => head}/bitfields/Func_read_full.fsti                                     |   4 +-
 {base => head}/bitfields/Func_read_nibble.fst                                    |   4 +-
 {base => head}/bitfields/Func_read_nibble.fsti                                   |   6 +--
 {base => head}/bitfields/Func_read_tdef.fst                                      |   4 +-
 {base => head}/bitfields/Func_read_tdef.fsti                                     |   6 +--
 {base => head}/bitfields/Func_set_a.fst                                          |   4 +-
 {base => head}/bitfields/Func_set_a.fsti                                         |   4 +-
 {base => head}/bitfields/Func_tdef_in_range.fst                                  |   4 +-
 {base => head}/bitfields/Func_tdef_in_range.fsti                                 |   6 +--
 {base => head}/bitfields/Func_write_a.fst                                        |   4 +-
 {base => head}/bitfields/Func_write_a.fsti                                       |   4 +-
 {base => head}/bitfields/Func_write_flag.fst                                     |   4 +-
 {base => head}/bitfields/Func_write_flag.fsti                                    |   6 +--
 {base => head}/bitfields/Func_write_nibble.fst                                   |   4 +-
 {base => head}/bitfields/Func_write_nibble.fsti                                  |   6 +--
 {base => head}/bitfields/Func_write_tdef.fst                                     |   4 +-
 {base => head}/bitfields/Func_write_tdef.fsti                                    |   6 +--
 {base => head}/container_of/Struct_packet_space.fst                              |   6 +--
 {base => head}/core_ref_chain/Struct_b.fst                                       |   6 +--
 {base => head}/core_ref_chain/Typedef_a_owned.fst                                |   2 +-
 {base => head}/core_ref_struct/Func_get_data.fst                                 |   4 +-
 {base => head}/core_ref_struct/Func_get_data.fsti                                |   4 +-
 {base => head}/core_ref_struct/Func_has_parent.fst                               |   4 +-
 {base => head}/core_ref_struct/Func_has_parent.fsti                              |   4 +-
 {base => head}/core_ref_struct/Func_set_data.fst                                 |   4 +-
 {base => head}/core_ref_struct/Func_set_data.fsti                                |   4 +-
 {base => head}/core_ref_struct/Struct_parent.fst                                 |   6 +--
 {base => head}/core_ref_use/Func_store.fst                                       |   4 +-
 {base => head}/core_ref_use/Func_store.fsti                                      |   4 +-
 {base => head}/core_ref_use/Func_via_back.fst                                    |   4 +-
 {base => head}/core_ref_use/Func_via_back.fsti                                   |   4 +-
 {base => head}/core_ref_use_ptr/Func_store.fst                                   |   4 +-
 {base => head}/core_ref_use_ptr/Func_store.fsti                                  |   4 +-
 {base => head}/core_ref_use_ptr/Func_via_inner.fst                               |   4 +-
 {base => head}/core_ref_use_ptr/Func_via_inner.fsti                              |   4 +-
 {base => head}/core_ref_use_ptr/Struct_bar.fst                                   |   6 +--
 {base => head}/do_while/Func_f.fst                                               |   4 +-
 {base => head}/do_while/Func_f.fsti                                              |   4 +-
 {base => head}/dpe/Func_authenticate_l0_image.fst                                |   2 +-
 {base => head}/dpe/Func_authenticate_l0_image.fsti                               |   2 +-
 {base => head}/dpe/Func_compute_cdi.fst                                          |   2 +-
 {base => head}/dpe/Func_compute_cdi.fsti                                         |   2 +-
 {base => head}/dpe/Func_derive_child_from_context.fst                            |   2 +-
 {base => head}/dpe/Func_derive_child_from_context.fsti                           |   2 +-
 {base => head}/dpe/Func_engine_main.fst                                          |   2 +-
 {base => head}/dpe/Func_engine_main.fsti                                         |   2 +-
 {base => head}/dpe/Typedef_context_obj.fst                                       |   2 +-
 {base => head}/eager_unfold_struct/Func_set_x.fst                                |   4 +-
 {base => head}/eager_unfold_struct/Func_set_x.fsti                               |   4 +-
 {base => head}/enum_constant_in_contract/Func_classify.fst                       |   2 +-
 {base => head}/enum_constant_in_contract/Func_classify.fsti                      |   2 +-
 {base => head}/extern_func_ptr/Func_use_extern_fp.fst                            |   2 +-
 {base => head}/extern_func_ptr/Funcptr_ext_add.fst                               |   4 +-
 {base => head}/extern_func_ptr/Funcptr_ext_add.fsti                              |   2 +-
 {base => head}/fnptr_slprop_spec/Func_call_via_o.fst                             |   2 +-
 {base => head}/fnptr_slprop_spec/Func_call_via_o_mixed.fst                       |   2 +-
 {base => head}/fnptr_slprop_spec/Funcptr_impl_both.fst                           |   5 ++-
 {base => head}/fnptr_slprop_spec/Funcptr_impl_both.fsti                          |   3 +-
 {base => head}/fnptr_slprop_spec/Funcptr_impl_mixed.fst                          |   4 +-
 {base => head}/fnptr_slprop_spec/Funcptr_impl_mixed.fsti                         |   2 +-
 {base => head}/fnptr_slprop_spec/Funcptr_impl_pre.fst                            |   4 +-
 {base => head}/fnptr_slprop_spec/Funcptr_impl_pre.fsti                           |   2 +-
 /dev/null => head/fnptr_spec/Func_call_dep.fst                                   |  32 ++++++++++++++
 /dev/null => head/fnptr_spec/Func_call_dep.fsti                                  |  16 +++++++
 /dev/null => head/fnptr_spec/Func_call_mixed.fst                                 |  48 +++++++++++++++++++++
 /dev/null => head/fnptr_spec/Func_call_mixed.fsti                                |  30 +++++++++++++
 /dev/null => head/fnptr_spec/Func_call_ok.fst                                    |  32 ++++++++++++++
 /dev/null => head/fnptr_spec/Func_call_ok.fsti                                   | 
... (summary truncated)

Full diff: full diff artifact

Diff

diff --git base/addr_global/Func_call_via_addr_of_global_struct.fst head/addr_global/Func_call_via_addr_of_global_struct.fst
index 3f21c5d..2f6b788 100644
--- base/addr_global/Func_call_via_addr_of_global_struct.fst
+++ head/addr_global/Func_call_via_addr_of_global_struct.fst
@@ -17,7 +17,7 @@ divergent fn func_call_via_addr_of_global_struct ()
       _
       (!(Struct_ops_anon_1.struct_ops_anon_1__get_op (!var_p)))
       (2l, 3l)
-      (hide ())));
+      _));
   Pulse.Lib.C.FuncPtr.drop_is_valid _ _ _;
   drop_ (exists* q. pts_to Global_g_ops.addr_var_g_ops #q _);
   return return_1;
diff --git base/addr_global/Funcptr_add.fst head/addr_global/Funcptr_add.fst
index 4ebd91a..c588c5b 100644
--- base/addr_global/Funcptr_add.fst
+++ head/addr_global/Funcptr_add.fst
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 
 
-divergent fn func_add__fp (x_fp: (Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)) (y_fp: erased unit)
+divergent fn func_add__fp (x_fp: (Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)) (y_fp: erased (unit & unit))
   requires ((Pulse.Lib.C.FuncPtr.prevent_lifting
       (let var_a = (fst x_fp) in
         let var_b = (snd x_fp) in
@@ -29,5 +29,5 @@ divergent fn func_add__fp (x_fp: (Typedef_int32_t.ty_int32_t & Typedef_int32_t.t
                 ((id #int (Int32.v var_b)) < 100)))) ==> (((return_1 =
                 (var_a `Int32.add` var_b))))))))
 {
-  Func_add.func_add (fst x_fp) (snd x_fp)
+    Func_add.func_add (fst x_fp) (snd x_fp)
 }
\ No newline at end of file
diff --git base/addr_global/Funcptr_add.fsti head/addr_global/Funcptr_add.fsti
index 6d913a3..e5ed181 100644
--- base/addr_global/Funcptr_add.fsti
+++ head/addr_global/Funcptr_add.fsti
@@ -5,7 +5,7 @@ open Pulse.Lib.C
 
 
 
-divergent fn func_add__fp (x_fp: (Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)) (y_fp: erased unit)
+divergent fn func_add__fp (x_fp: (Typedef_int32_t.ty_int32_t & Typedef_int32_t.ty_int32_t)) (y_fp: erased (unit & unit))
   requires ((Pulse.Lib.C.FuncPtr.prevent_lifting
       (let var_a = (fst x_fp) in
         let var_b = (snd x_fp) in
diff --git base/anon_struct/Func_frob.fst head/anon_struct/Func_frob.fst
index 604ab24..937c132 100644
--- base/anon_struct/Func_frob.fst
+++ head/anon_struct/Func_frob.fst
@@ -6,13 +6,11 @@ open Pulse.Lib.C
 divergent fn func_frob (var_b: (ref Struct_baz.struct_baz))
   requires
     exists* (val_b_0: Struct_baz.struct_baz).
-    ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
-      (Struct_baz.struct_baz__pred (!var_b) 1.0R))
+    ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred val_b_0 1.0R))
   returns return_1 : Int32.t
   ensures
     exists* (val_b_0: Struct_baz.struct_baz).
-    ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
-      (Struct_baz.struct_baz__pred (!var_b) 1.0R))
+    ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred val_b_0 1.0R))
   ensures
     (with_pure
       ((!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_foo var_b))) =
diff --git base/anon_struct/Func_frob.fsti head/anon_struct/Func_frob.fsti
index ce430af..59d7f0b 100644
--- base/anon_struct/Func_frob.fsti
+++ head/anon_struct/Func_frob.fsti
@@ -6,11 +6,11 @@ open Pulse.Lib.C
 divergent fn func_frob (var_b: (ref Struct_baz.struct_baz))
 requires
   exists* (val_b_0: Struct_baz.struct_baz).
-  ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred (!var_b) 1.0R))
+  ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred val_b_0 1.0R))
 returns return_1 : Int32.t
 ensures
   exists* (val_b_0: Struct_baz.struct_baz).
-  ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred (!var_b) 1.0R))
+  ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) ** (Struct_baz.struct_baz__pred val_b_0 1.0R))
 ensures
   (with_pure
     ((!(Struct_baz_anon_1.struct_baz_anon_1__get_x (Struct_baz.struct_baz__get_foo var_b))) =
diff --git base/anon_struct/Func_use_profiles.fst head/anon_struct/Func_use_profiles.fst
index ed56271..f97d2df 100644
--- base/anon_struct/Func_use_profiles.fst
+++ head/anon_struct/Func_use_profiles.fst
@@ -9,14 +9,14 @@ divergent fn func_use_profiles (var_p: (ref Typedef_profiles.ty_profiles))
     (val_p_0: Typedef_profiles.ty_profiles)
     (val_p_1: Struct_profiles.struct_profiles__spec).
     ((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
-      (Typedef_profiles.ty_profiles__pred (!var_p) 1.0R val_p_1))
+      (Typedef_profiles.ty_profiles__pred val_p_0 1.0R val_p_1))
   returns return_1 : unit
   ensures
     exists*
     (val_p_0: Typedef_profiles.ty_profiles)
     (val_p_1: Struct_profiles.struct_profiles__spec).
     ((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
-      (Typedef_profiles.ty_profiles__pred (!var_p) 1.0R val_p_1))
+      (Typedef_profiles.ty_profiles__pred val_p_0 1.0R val_p_1))
 {
   let mut var_p = var_p;
 }
\ No newline at end of file
diff --git base/anon_struct/Func_use_profiles.fsti head/anon_struct/Func_use_profiles.fsti
index 06a4fbb..e0e2e67 100644
--- base/anon_struct/Func_use_profiles.fsti
+++ head/anon_struct/Func_use_profiles.fsti
@@ -7,9 +7,9 @@ divergent fn func_use_profiles (var_p: (ref Typedef_profiles.ty_profiles))
 requires
   exists* (val_p_0: Typedef_profiles.ty_profiles) (val_p_1: Struct_profiles.struct_profiles__spec).
   ((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
-    (Typedef_profiles.ty_profiles__pred (!var_p) 1.0R val_p_1))
+    (Typedef_profiles.ty_profiles__pred val_p_0 1.0R val_p_1))
 returns return_1 : unit
 ensures
   exists* (val_p_0: Typedef_profiles.ty_profiles) (val_p_1: Struct_profiles.struct_profiles__spec).
   ((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
-    (Typedef_profiles.ty_profiles__pred (!var_p) 1.0R val_p_1))
\ No newline at end of file
+    (Typedef_profiles.ty_profiles__pred val_p_0 1.0R val_p_1))
\ No newline at end of file
diff --git base/anon_struct/Struct_profiles_anon_1.fst head/anon_struct/Struct_profiles_anon_1.fst
index d8322eb..3800d0f 100644
--- base/anon_struct/Struct_profiles_anon_1.fst
+++ head/anon_struct/Struct_profiles_anon_1.fst
@@ -32,11 +32,11 @@ let predicate struct_profiles_anon_1__pred
       #p
       val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_0) **
     (Pulse.Lib.Reference.pts_to
-      (!(this).struct_profiles_anon_1__begin)
+      val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_0
       #p
       val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_1) **
     (Typedef_profile.ty_profile__pred
-      (!(!(this).struct_profiles_anon_1__begin))
+      val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_1
       p
       val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_2) **
     (Pulse.Lib.Reference.pts_to
@@ -44,11 +44,11 @@ let predicate struct_profiles_anon_1__pred
       #p
       val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_0) **
     (Pulse.Lib.Reference.pts_to
-      (!(this).struct_profiles_anon_1__end)
+      val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_0
       #p
       val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_1) **
     (Typedef_profile.ty_profile__pred
-      (!(!(this).struct_profiles_anon_1__end))
+      val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_1
       p
       val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_2) **
     (Pulse.Lib.Reference.pts_to
@@ -56,11 +56,11 @@ let predicate struct_profiles_anon_1__pred
       #p
       val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_0) **
     (Pulse.Lib.Reference.pts_to
-      (!(this).struct_profiles_anon_1__allocated)
+      val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_0
       #p
       val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_1) **
     (Typedef_profile.ty_profile__pred
-      (!(!(this).struct_profiles_anon_1__allocated))
+      val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_1
       p
       val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_2))
 [@@pulse_eager_unfold] let predicate struct_profiles_anon_1__uninit_pred
@@ -80,11 +80,11 @@ struct_profiles_anon_1__pred_unfold
   #p
   val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_0)
   ensures (Pulse.Lib.Reference.pts_to
-  (!(this).struct_profiles_anon_1__begin)
+  val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_0
   #p
   val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_1)
   ensures (Typedef_profile.ty_profile__pred
-  (!(!(this).struct_profiles_anon_1__begin))
+  val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_1
   p
   val_profiles_anon_1_0.struct_profiles_anon_1__spec__begin_2)
   ensures (Pulse.Lib.Reference.pts_to
@@ -92,11 +92,11 @@ struct_profiles_anon_1__pred_unfold
   #p
   val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_0)
   ensures (Pulse.Lib.Reference.pts_to
-  (!(this).struct_profiles_anon_1__end)
+  val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_0
   #p
   val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_1)
   ensures (Typedef_profile.ty_profile__pred
-  (!(!(this).struct_profiles_anon_1__end))
+  val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_1
   p
   val_profiles_anon_1_0.struct_profiles_anon_1__spec__end_2)
   ensures (Pulse.Lib.Reference.pts_to
@@ -104,11 +104,11 @@ struct_profiles_anon_1__pred_unfold
   #p
   val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_0)
   ensures (Pulse.Lib.Reference.pts_to
-  (!(this).struct_profiles_anon_1__allocated)
+  val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_0
   #p
   val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_1)
   ensures (Typedef_profile.ty_profile__pred
-  (!(!(this).struct_profiles_anon_1__allocated))
+  val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_1
   p
   val_profiles_anon_1_0.struct_profiles_anon_1__spec__allocated_2)
 {
@@ -129,23 +129,14 @@ struct_profiles_anon_1__pred_fold
     (val_allocated_1: Typedef_profile.ty_profile)
     (val_allocated_2: Struct_profile.struct_profile__spec)
   requires (Pulse.Lib.Reference.pts_to (this).struct_profiles_anon_1__begin #p val_begin_0)
-  requires (Pulse.Lib.Reference.pts_to (!(this).struct_profiles_anon_1__begin) #p val_begin_1)
-  requires (Typedef_profile.ty_profile__pred
-  (!(!(this).struct_profiles_anon_1__begin))
-  p
-  val_begin_2)
+  requires (Pulse.Lib.Reference.pts_to val_begin_0 #p val_begin_1)
+  requires (Typedef_profile.ty_profile__pred val_begin_1 p val_begin_2)
   requires (Pulse.Lib.Reference.pts_to (this).struct_profiles_anon_1__end #p val_end_0)
-  requires (Pulse.Lib.Reference.pts_to (!(this).struct_profiles_anon_1__end) #p val_end_1)
-  requires (Typedef_profile.ty_profile__pred (!(!(this).struct_profiles_anon_1__end)) p val_end_2)
+  requires (Pulse.Lib.Reference.pts_to val_end_0 #p val_end_1)
+  requires (Typedef_profile.ty_profile__pred val_end_1 p val_end_2)
   requires (Pulse.Lib.Reference.pts_to (this).struct_profiles_anon_1__allocated #p val_allocated_0)
-  requires (Pulse.Lib.Reference.pts_to
-  (!(this).struct_profiles_anon_1__allocated)
-  #p
-  val_allocated_1)
-  requires (Typedef_profile.ty_profile__pred
-  (!(!(this).struct_profiles_anon_1__allocated))
-  p
-  val_allocated_2)
+  requires (Pulse.Lib.Reference.pts_to val_allocated_0 #p val_allocated_1)
+  requires (Typedef_profile.ty_profile__pred val_allocated_1 p val_allocated_2)
   ensures struct_profiles_anon_1__pred this p ({
       struct_profiles_anon_1__spec__begin_0 = val_begin_0;
       struct_profiles_anon_1__spec__begin_1 = val_begin_1;
diff --git base/antiquot/Func_test_declare.fst head/antiquot/Func_test_declare.fst
index c20cae0..1aed9e5 100644
--- base/antiquot/Func_test_declare.fst
+++ head/antiquot/Func_test_declare.fst
@@ -7,7 +7,7 @@ divergent fn func_test_declare (var_x: (ref Typedef_my_pair.ty_my_pair))
   requires
     exists* (val_x_0: Typedef_my_pair.ty_my_pair).
     ((Pulse.Lib.Reference.pts_to var_x #1.0R val_x_0) **
-      (Typedef_my_pair.ty_my_pair__pred (!var_x) 1.0R))
+      (Typedef_my_pair.ty_my_pair__pred val_x_0 1.0R))
   requires
     (with_pure
       ((id #int (Int32.v (!(Struct_my_pair_anon_1.struct_my_pair_anon_1__get_a var_x)))) = 0))
@@ -15,7 +15,7 @@ divergent fn func_test_declare (var_x: (ref Typedef_my_pair.ty_my_pair))
   ensures
     exists* (val_x_0: Typedef_my_pair.ty_my_pair).
     ((Pulse.Lib.Reference.pts_to var_x #1.0R val_x_0) **
-      (Typedef_my_pair.ty_my_pair__pred (!var_x) 1.0R))
+      (Typedef_my_pair.ty_my_pair__pred val_x_0 1.0R))
   ensures
     (with_pure
       ((id #int (Int32.v (!(Struct_my_pair_anon_1.struct_my_pair_anon_1__get_a var_x)))) = 0))
diff --git base/antiquot/Func_test_declare.fsti head/antiquot/Func_test_declare.fsti
index a5d3f39..d7cc547 100644
--- base/antiquot/Func_test_declare.fsti
+++ head/antiquot/Func_test_declare.fsti
@@ -7,7 +7,7 @@ divergent fn func_test_declare (var_x: (ref Typedef_my_pair.ty_my_pair))
 requires
   exists* (val_x_0: Typedef_my_pair.ty_my_pair).
   ((Pulse.Lib.Reference.pts_to var_x #1.0R val_x_0) **
-    (Typedef_my_pair.ty_my_pair__pred (!var_x) 1.0R))
+    (Typedef_my_pair.ty_my_pair__pred val_x_0 1.0R))
 requires
   (with_pure
     ((id #int (Int32.v (!(Struct_my_pair_anon_1.struct_my_pair_anon_1__get_a var_x)))) = 0))
@@ -15,7 +15,7 @@ returns return_1 : unit
 ensures
   exists* (val_x_0: Typedef_my_pair.ty_my_pair).
   ((Pulse.Lib.Reference.pts_to var_x #1.0R val_x_0) **
-    (Typedef_my_pair.ty_my_pair__pred (!var_x) 1.0R))
+    (Typedef_my_pair.ty_my_pair__pred val_x_0 1.0R))
 ensures
   (with_pure
     ((id #int (Int32.v (!(Struct_my_pair_anon_1.struct_my_pair_anon_1__get_a var_x)))) = 0))
\ No newline at end of file
diff --git base/array_addressof_loses_index/Func_get_via_addressof_const.fst head/array_addressof_loses_index/Func_get_via_addressof_const.fst
index 61c04c5..1e54a3c 100644
--- base/array_addressof_loses_index/Func_get_via_addressof_const.fst
+++ head/array_addressof_loses_index/Func_get_via_addressof_const.fst
@@ -9,14 +9,14 @@ divergent fn func_get_via_addressof_const (var_c: (ref Typedef_containercopy.ty_
     (val_c_0: Typedef_containercopy.ty_containercopy)
     (val_c_1: Struct_containercopy.struct_containercopy__spec).
     ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-      (Typedef_containercopy.ty_containercopy__pred (!var_c) 1.0R val_c_1))
+      (Typedef_containercopy.ty_containercopy__pred val_c_0 1.0R val_c_1))
   returns return_1 : (array Int32.t)
   ensures
     exists*
     (val_c_0: Typedef_containercopy.ty_containercopy)
     (val_c_1: Struct_containercopy.struct_containercopy__spec).
     ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-      (Typedef_containercopy.ty_containercopy__pred (!var_c) 1.0R val_c_1))
+      (Typedef_containercopy.ty_containercopy__pred val_c_0 1.0R val_c_1))
 {
   let mut var_c = var_c;
   return
diff --git base/array_addressof_loses_index/Func_get_via_addressof_const.fsti head/array_addressof_loses_index/Func_get_via_addressof_const.fsti
index b856456..b84cc8a 100644
--- base/array_addressof_loses_index/Func_get_via_addressof_const.fsti
+++ head/array_addressof_loses_index/Func_get_via_addressof_const.fsti
@@ -9,11 +9,11 @@ requires
   (val_c_0: Typedef_containercopy.ty_containercopy)
   (val_c_1: Struct_containercopy.struct_containercopy__spec).
   ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-    (Typedef_containercopy.ty_containercopy__pred (!var_c) 1.0R val_c_1))
+    (Typedef_containercopy.ty_containercopy__pred val_c_0 1.0R val_c_1))
 returns return_1 : (array Int32.t)
 ensures
   exists*
   (val_c_0: Typedef_containercopy.ty_containercopy)
   (val_c_1: Struct_containercopy.struct_containercopy__spec).
   ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-    (Typedef_containercopy.ty_containercopy__pred (!var_c) 1.0R val_c_1))
\ No newline at end of file
+    (Typedef_containercopy.ty_containercopy__pred val_c_0 1.0R val_c_1))
\ No newline at end of file
diff --git base/array_typedef_pointer/Typedef_PCE.fst head/array_typedef_pointer/Typedef_PCE.fst
index 3e2dd9b..a524e0f 100644
--- base/array_typedef_pointer/Typedef_PCE.fst
+++ head/array_typedef_pointer/Typedef_PCE.fst
@@ -9,7 +9,7 @@ let ty_pce : Type = (ref Typedef_E.ty_e)
       ([@@@mkey] this: ty_pce)
       (p: perm)
       (val_this_0: Typedef_E.ty_e) =
-  ((Pulse.Lib.Reference.pts_to this #p val_this_0) ** (Typedef_E.ty_e__pred (!this) p))
+  ((Pulse.Lib.Reference.pts_to this #p val_this_0) ** (Typedef_E.ty_e__pred val_this_0 p))
 [@@pulse_eager_unfold] let predicate ty_pce__uninit_pred ([@@@mkey] this: ty_pce) =
   ((Pulse.Lib.Reference.pts_to_uninit this))
 instance has_zero_default_ty_pce : (has_zero_default ty_pce) = { zero_default = null }
\ No newline at end of file
diff --git base/array_typedef_pointer/Typedef_PE.fst head/array_typedef_pointer/Typedef_PE.fst
index 35e5aa9..16a21a2 100644
--- base/array_typedef_pointer/Typedef_PE.fst
+++ head/array_typedef_pointer/Typedef_PE.fst
@@ -9,7 +9,7 @@ let ty_pe : Type = (ref Typedef_E.ty_e)
       ([@@@mkey] this: ty_pe)
       (p: perm)
       (val_this_0: Typedef_E.ty_e) =
-  ((Pulse.Lib.Reference.pts_to this #p val_this_0) ** (Typedef_E.ty_e__pred (!this) p))
+  ((Pulse.Lib.Reference.pts_to this #p val_this_0) ** (Typedef_E.ty_e__pred val_this_0 p))
 [@@pulse_eager_unfold] let predicate ty_pe__uninit_pred ([@@@mkey] this: ty_pe) =
   ((Pulse.Lib.Reference.pts_to_uninit this))
 instance has_zero_default_ty_pe : (has_zero_default ty_pe) = { zero_default = null }
\ No newline at end of file
diff --git base/bitfields/Func_read_a.fst head/bitfields/Func_read_a.fst
index 0f37290..7199801 100644
--- base/bitfields/Func_read_a.fst
+++ head/bitfields/Func_read_a.fst
@@ -7,12 +7,12 @@ divergent fn func_read_a (var_s: (ref Struct_flags.struct_flags))
   requires
     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))
+      (Struct_flags.struct_flags__pred val_s_0 1.0R))
   returns return_1 : UInt32.t
   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))
+      (Struct_flags.struct_flags__pred val_s_0 1.0R))
   ensures (with_pure (return_1 = (!(Struct_flags.struct_flags__get_a var_s))))
 {
   let mut var_s = var_s;
diff --git base/bitfields/Func_read_a.fsti head/bitfields/Func_read_a.fsti
index f067204..68e069d 100644
--- base/bitfields/Func_read_a.fsti
+++ head/bitfields/Func_read_a.fsti
@@ -7,10 +7,10 @@ divergent fn func_read_a (var_s: (ref Struct_flags.struct_flags))
 requires
   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))
+    (Struct_flags.struct_flags__pred val_s_0 1.0R))
 returns return_1 : UInt32.t
 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))
+    (Struct_flags.struct_flags__pred val_s_0 1.0R))
 ensures (with_pure (return_1 = (!(Struct_flags.struct_flags__get_a var_s))))
\ No newline at end of file
diff --git base/bitfields/Func_read_flag.fst head/bitfields/Func_read_flag.fst
index 0719ee6..4495c26 100644
--- base/bitfields/Func_read_flag.fst
+++ head/bitfields/Func_read_flag.fst
@@ -7,12 +7,12 @@ divergent fn func_read_flag (var_s: (ref Struct_bits.struct_bits))
   requires
     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))
+      (Struct_bits.struct_bits__pred val_s_0 1.0R))
   returns return_1 : bool
   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))
+      (Struct_bits.struct_bits__pred val_s_0 1.0R))
   ensures (with_pure (return_1 = (!(Struct_bits.struct_bits__get_flag var_s))))
 {
   let mut var_s = var_s;
diff --git base/bitfields/Func_read_flag.fsti head/bitfields/Func_read_flag.fsti
index fecfbe3..37a3653 100644
--- base/bitfields/Func_read_flag.fsti
+++ head/bitfields/Func_read_flag.fsti
@@ -6,11 +6,9 @@ open Pulse.Lib.C
 divergent fn func_read_flag (var_s: (ref Struct_bits.struct_bits))
 requires
   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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
 returns return_1 : bool
 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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
 ensures (with_pure (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..f9d5d7d 100644
--- base/bitfields/Func_read_full.fst
+++ head/bitfields/Func_read_full.fst
@@ -7,12 +7,12 @@ divergent fn func_read_full (var_s: (ref Struct_flags.struct_flags))
   requires
     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))
+      (Struct_flags.struct_flags__pred val_s_0 1.0R))
   returns return_1 : UInt32.t
   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))
+      (Struct_flags.struct_flags__pred val_s_0 1.0R))
   ensures (with_pure (return_1 = (!(Struct_flags.struct_flags__get_full var_s))))
 {
   let mut var_s = var_s;
diff --git base/bitfields/Func_read_full.fsti head/bitfields/Func_read_full.fsti
index 986c490..ef0f74c 100644
--- base/bitfields/Func_read_full.fsti
+++ head/bitfields/Func_read_full.fsti
@@ -7,10 +7,10 @@ divergent fn func_read_full (var_s: (ref Struct_flags.struct_flags))
 requires
   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))
+    (Struct_flags.struct_flags__pred val_s_0 1.0R))
 returns return_1 : UInt32.t
 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))
+    (Struct_flags.struct_flags__pred val_s_0 1.0R))
 ensures (with_pure (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..a156e3d 100644
--- base/bitfields/Func_read_nibble.fst
+++ head/bitfields/Func_read_nibble.fst
@@ -7,12 +7,12 @@ divergent fn func_read_nibble (var_s: (ref Struct_bits.struct_bits))
   requires
     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))
+      (Struct_bits.struct_bits__pred val_s_0 1.0R))
   returns return_1 : UInt8.t
   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))
+      (Struct_bits.struct_bits__pred val_s_0 1.0R))
   ensures (with_pure (return_1 = (!(Struct_bits.struct_bits__get_nibble var_s))))
 {
   let mut var_s = var_s;
diff --git base/bitfields/Func_read_nibble.fsti head/bitfields/Func_read_nibble.fsti
index ed8fabb..96ac5e2 100644
--- base/bitfields/Func_read_nibble.fsti
+++ head/bitfields/Func_read_nibble.fsti
@@ -6,11 +6,9 @@ open Pulse.Lib.C
 divergent fn func_read_nibble (var_s: (ref Struct_bits.struct_bits))
 requires
   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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
 returns return_1 : UInt8.t
 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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
 ensures (with_pure (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..c463c5d 100644
--- base/bitfields/Func_read_tdef.fst
+++ head/bitfields/Func_read_tdef.fst
@@ -7,12 +7,12 @@ divergent fn func_read_tdef (var_s: (ref Struct_tdef.struct_tdef))
   requires
     exists* (val_s_0: 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))
+      (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
   returns return_1 : Typedef_uint16_t.ty_uint16_t
   ensures
     exists* (val_s_0: 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))
+      (Struct_tdef.struct_tdef__pred val_s_0 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))))
 {
diff --git base/bitfields/Func_read_tdef.fsti head/bitfields/Func_read_tdef.fsti
index af5c5e5..c886040 100644
--- base/bitfields/Func_read_tdef.fsti
+++ head/bitfields/Func_read_tdef.fsti
@@ -6,12 +6,10 @@ open Pulse.Lib.C
 divergent fn func_read_tdef (var_s: (ref Struct_tdef.struct_tdef))
 requires
   exists* (val_s_0: 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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
 returns return_1 : Typedef_uint16_t.ty_uint16_t
 ensures
   exists* (val_s_0: 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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 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
diff --git base/bitfields/Func_set_a.fst head/bitfields/Func_set_a.fst
index d913f13..0dfa9e0 100644
--- base/bitfields/Func_set_a.fst
+++ head/bitfields/Func_set_a.fst
@@ -7,12 +7,12 @@ divergent fn func_set_a (var_s: (ref Struct_flags.struct_flags))
   requires
     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))
+      (Struct_flags.struct_flags__pred val_s_0 1.0R))
   returns return_1 : unit
   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))
+      (Struct_flags.struct_flags__pred val_s_0 1.0R))
   ensures (with_pure ((id #int (UInt32.v (!(Struct_flags.struct_flags__get_a var_s)))) = 5))
 {
   let mut var_s = var_s;
diff --git base/bitfields/Func_set_a.fsti head/bitfields/Func_set_a.fsti
index bc3a634..b6c1740 100644
--- base/bitfields/Func_set_a.fsti
+++ head/bitfields/Func_set_a.fsti
@@ -7,10 +7,10 @@ divergent fn func_set_a (var_s: (ref Struct_flags.struct_flags))
 requires
   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))
+    (Struct_flags.struct_flags__pred val_s_0 1.0R))
 returns return_1 : unit
 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))
+    (Struct_flags.struct_flags__pred val_s_0 1.0R))
 ensures (with_pure ((id #int (UInt32.v (!(Struct_flags.struct_flags__get_a var_s)))) = 5))
\ No newline at end of file
diff --git base/bitfields/Func_tdef_in_range.fst head/bitfields/Func_tdef_in_range.fst
index 19ec482..8ecfb68 100644
--- base/bitfields/Func_tdef_in_range.fst
+++ head/bitfields/Func_tdef_in_range.fst
@@ -7,12 +7,12 @@ divergent fn func_tdef_in_range (var_s: (ref Struct_tdef.struct_tdef))
   requires
     exists* (val_s_0: 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))
+      (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
   returns return_1 : unit
   ensures
     exists* (val_s_0: 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))
+      (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
 {
   let mut var_s = var_s;
   assert (with_pure ((id #int (UInt16.v (!(Struct_tdef.struct_tdef__get_a (!var_s))))) <= 3));
diff --git base/bitfields/Func_tdef_in_range.fsti head/bitfields/Func_tdef_in_range.fsti
index 3d27218..97d12ea 100644
--- base/bitfields/Func_tdef_in_range.fsti
+++ head/bitfields/Func_tdef_in_range.fsti
@@ -6,10 +6,8 @@ open Pulse.Lib.C
 divergent fn func_tdef_in_range (var_s: (ref Struct_tdef.struct_tdef))
 requires
   exists* (val_s_0: 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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
 returns return_1 : unit
 ensures
   exists* (val_s_0: 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))
\ No newline at end of file
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
\ No newline at end of file
diff --git base/bitfields/Func_write_a.fst head/bitfields/Func_write_a.fst
index a57ca6f..269a5c8 100644
--- base/bitfields/Func_write_a.fst
+++ head/bitfields/Func_write_a.fst
@@ -7,12 +7,12 @@ divergent fn func_write_a (var_s: (ref Struct_flags.struct_flags)) (var_v: UInt3
   requires
     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))
+      (Struct_flags.struct_flags__pred val_s_0 1.0R))
   returns return_1 : unit
   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))
+      (Struct_flags.struct_flags__pred val_s_0 1.0R))
   ensures
     (with_pure
       ((id #int (UInt32.v (!(Struct_flags.struct_flags__get_a var_s)))) =
diff --git base/bitfields/Func_write_a.fsti head/bitfields/Func_write_a.fsti
index b73bba6..da2a65c 100644
--- base/bitfields/Func_write_a.fsti
+++ head/bitfields/Func_write_a.fsti
@@ -7,12 +7,12 @@ divergent fn func_write_a (var_s: (ref Struct_flags.struct_flags)) (var_v: UInt3
 requires
   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))
+    (Struct_flags.struct_flags__pred val_s_0 1.0R))
 returns return_1 : unit
 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))
+    (Struct_flags.struct_flags__pred val_s_0 1.0R))
 ensures
   (with_pure
     ((id #int (UInt32.v (!(Struct_flags.struct_flags__get_a var_s)))) =
diff --git base/bitfields/Func_write_flag.fst head/bitfields/Func_write_flag.fst
index bd19896..1bba047 100644
--- base/bitfields/Func_write_flag.fst
+++ head/bitfields/Func_write_flag.fst
@@ -7,12 +7,12 @@ divergent fn func_write_flag (var_s: (ref Struct_bits.struct_bits)) (var_v: bool
   requires
     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))
+      (Struct_bits.struct_bits__pred val_s_0 1.0R))
   returns return_1 : unit
   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))
+      (Struct_bits.struct_bits__pred val_s_0 1.0R))
   ensures (with_pure ((!(Struct_bits.struct_bits__get_flag var_s)) = var_v))
 {
   let mut var_s = var_s;
diff --git base/bitfields/Func_write_flag.fsti head/bitfields/Func_write_flag.fsti
index b621d8f..ffa6053 100644
--- base/bitfields/Func_write_flag.fsti
+++ head/bitfields/Func_write_flag.fsti
@@ -6,11 +6,9 @@ open Pulse.Lib.C
 divergent fn func_write_flag (var_s: (ref Struct_bits.struct_bits)) (var_v: bool)
 requires
   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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
 returns return_1 : unit
 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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
 ensures (with_pure ((!(Struct_bits.struct_bits__get_flag var_s)) = var_v))
\ No newline at end of file
diff --git base/bitfields/Func_write_nibble.fst head/bitfields/Func_write_nibble.fst
index 61bcea2..f158d2a 100644
--- base/bitfields/Func_write_nibble.fst
+++ head/bitfields/Func_write_nibble.fst
@@ -7,12 +7,12 @@ divergent fn func_write_nibble (var_s: (ref Struct_bits.struct_bits)) (var_v: UI
   requires
     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))
+      (Struct_bits.struct_bits__pred val_s_0 1.0R))
   returns return_1 : unit
   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))
+      (Struct_bits.struct_bits__pred val_s_0 1.0R))
   ensures
     (with_pure
       ((id #int (UInt8.v (!(Struct_bits.struct_bits__get_nibble var_s)))) =
diff --git base/bitfields/Func_write_nibble.fsti head/bitfields/Func_write_nibble.fsti
index c54541d..6d8f5ec 100644
--- base/bitfields/Func_write_nibble.fsti
+++ head/bitfields/Func_write_nibble.fsti
@@ -6,13 +6,11 @@ open Pulse.Lib.C
 divergent fn func_write_nibble (var_s: (ref Struct_bits.struct_bits)) (var_v: UInt8.t)
 requires
   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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
 returns return_1 : unit
 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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_bits.struct_bits__pred val_s_0 1.0R))
 ensures
   (with_pure
     ((id #int (UInt8.v (!(Struct_bits.struct_bits__get_nibble var_s)))) =
diff --git base/bitfields/Func_write_tdef.fst head/bitfields/Func_write_tdef.fst
index 6bab42f..f9409f6 100644
--- base/bitfields/Func_write_tdef.fst
+++ head/bitfields/Func_write_tdef.fst
@@ -9,13 +9,13 @@ divergent fn func_write_tdef
   requires
     exists* (val_s_0: 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))
+      (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
   requires ((Typedef_uint16_t.ty_uint16_t__pred var_v 1.0R))
   returns return_1 : unit
   ensures
     exists* (val_s_0: 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))
+      (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
   ensures ((Typedef_uint16_t.ty_uint16_t__pred var_v 1.0R))
   ensures
     (with_pure
diff --git base/bitfields/Func_write_tdef.fsti head/bitfields/Func_write_tdef.fsti
index 54cae02..c97a741 100644
--- base/bitfields/Func_write_tdef.fsti
+++ head/bitfields/Func_write_tdef.fsti
@@ -8,14 +8,12 @@ divergent fn func_write_tdef
   (var_v: Typedef_uint16_t.ty_uint16_t)
 requires
   exists* (val_s_0: 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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
 requires ((Typedef_uint16_t.ty_uint16_t__pred var_v 1.0R))
 returns return_1 : unit
 ensures
   exists* (val_s_0: 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))
+  ((Pulse.Lib.Reference.pts_to var_s #1.0R val_s_0) ** (Struct_tdef.struct_tdef__pred val_s_0 1.0R))
 ensures ((Typedef_uint16_t.ty_uint16_t__pred var_v 1.0R))
 ensures
   (with_pure
diff --git base/container_of/Struct_packet_space.fst head/container_of/Struct_packet_space.fst
index 709a26b..a862c52 100644
--- base/container_of/Struct_packet_space.fst
+++ head/container_of/Struct_packet_space.fst
@@ -26,7 +26,7 @@ let predicate struct_packet_space__pred
       (this).struct_packet_space__back
       #p
       val_packet_space_0.struct_packet_space__spec__back_0) **
-    (Typedef_int32_t.ty_int32_t__pred (!(this).struct_packet_space__back) p))
+    (Typedef_int32_t.ty_int32_t__pred val_packet_space_0.struct_packet_space__spec__back_0 p))
 [@@pulse_eager_unfold] let predicate struct_packet_space__uninit_pred
       ([@@@mkey] this: struct_packet_space) =
   ((Typedef_ack_tracker_t.ty_ack_tracker_t__uninit_pred (this).struct_packet_space__tracker) **
@@ -45,7 +45,7 @@ struct_packet_space__pred_unfold
   (this).struct_packet_space__back
   #p
   val_packet_space_0.struct_packet_space__spec__back_0)
-  ensures (Typedef_int32_t.ty_int32_t__pred (!(this).struct_packet_space__back) p)
+  ensures (Typedef_int32_t.ty_int32_t__pred val_packet_space_0.struct_packet_space__spec__back_0 p)
 {
   unfold struct_packet_space__pred this p val_packet_space_0
 }
@@ -58,7 +58,7 @@ struct_packet_space__pred_fold
   requires (Typedef_ack_tracker_t.ty_ack_tracker_t__pred (this).struct_packet_space__tracker p)
   requires (Typedef_int32_t.ty_int32_t__pred (this).struct_packet_space__id p)
   requires (Pulse.Lib.Reference.pts_to (this).struct_packet_space__back #p val_back_0)
-  requires (Typedef_int32_t.ty_int32_t__pred (!(this).struct_packet_space__back) p)
+  requires (Typedef_int32_t.ty_int32_t__pred val_back_0 p)
   ensures struct_packet_space__pred this p ({
       struct_packet_space__spec__back_0 = val_back_0;
     })
diff --git base/core_ref_chain/Struct_b.fst head/core_ref_chain/Struct_b.fst
index dd11a81..6f84e07 100644
--- base/core_ref_chain/Struct_b.fst
+++ head/core_ref_chain/Struct_b.fst
@@ -16,7 +16,7 @@ assume val struct_b__sizeof_pos (a: Type0 { a == struct_b }) :
 }
 let predicate struct_b__pred ([@@@mkey] this: struct_b) (p: perm) (val_b_0: struct_b__spec) =
   ((Pulse.Lib.Reference.pts_to (this).struct_b__pa #p val_b_0.struct_b__spec__pa_0) **
-    (Struct_a.struct_a__pred (!(this).struct_b__pa) p))
+    (Struct_a.struct_a__pred val_b_0.struct_b__spec__pa_0 p))
 [@@pulse_eager_unfold] let predicate struct_b__uninit_pred ([@@@mkey] this: struct_b) =
   ((Pulse.Lib.Reference.pts_to_uninit (this).struct_b__pa))
 [@@pulse_intro]
@@ -27,7 +27,7 @@ struct_b__pred_unfold
     (val_b_0: struct_b__spec)
   requires struct_b__pred this p val_b_0
   ensures (Pulse.Lib.Reference.pts_to (this).struct_b__pa #p val_b_0.struct_b__spec__pa_0)
-  ensures (Struct_a.struct_a__pred (!(this).struct_b__pa) p)
+  ensures (Struct_a.struct_a__pred val_b_0.struct_b__spec__pa_0 p)
 {
   unfold struct_b__pred this p val_b_0
 }
@@ -38,7 +38,7 @@ struct_b__pred_fold
     (p: perm)
     (val_pa_0: Struct_a.struct_a)
   requires (Pulse.Lib.Reference.pts_to (this).struct_b__pa #p val_pa_0)
-  requires (Struct_a.struct_a__pred (!(this).struct_b__pa) p)
+  requires (Struct_a.struct_a__pred val_pa_0 p)
   ensures struct_b__pred this p ({
       struct_b__spec__pa_0 = val_pa_0;
     })
diff --git base/core_ref_chain/Typedef_a_owned.fst head/core_ref_chain/Typedef_a_owned.fst
index 4cd8dcc..62c0aa2 100644
--- base/core_ref_chain/Typedef_a_owned.fst
+++ head/core_ref_chain/Typedef_a_owned.fst
@@ -10,7 +10,7 @@ let ty_a_owned : Type = (ref Struct_a.struct_a)
       (p: perm)
       (val_this_0: Struct_a.struct_a) =
   ((Pulse.Lib.Reference.pts_to this #p val_this_0) **
-    (Struct_a.struct_a__pred (!this) p) **
+    (Struct_a.struct_a__pred val_this_0 p) **
     (exists* (bv: Struct_b.struct_b).
 pts_to (Pulse.Lib.C.CoreRef.core_to_ref Struct_b.struct_b
 (((!this)).Struct_a.struct_a__pb)) bv))
diff --git base/core_ref_struct/Func_get_data.fst head/core_ref_struct/Func_get_data.fst
index 0e276eb..71393e8 100644
--- base/core_ref_struct/Func_get_data.fst
+++ head/core_ref_struct/Func_get_data.fst
@@ -7,12 +7,12 @@ divergent fn func_get_data (var_c: (ref Struct_child.struct_child))
   requires
     exists* (val_c_0: Struct_child.struct_child).
     ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-      (Struct_child.struct_child__pred (!var_c) 1.0R))
+      (Struct_child.struct_child__pred val_c_0 1.0R))
   returns return_1 : Int32.t
   ensures
     exists* (val_c_0: Struct_child.struct_child).
     ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-      (Struct_child.struct_child__pred (!var_c) 1.0R))
+      (Struct_child.struct_child__pred val_c_0 1.0R))
 {
   let mut var_c = var_c;
   return (!(Struct_child.struct_child__get_data (!var_c)));
diff --git base/core_ref_struct/Func_get_data.fsti head/core_ref_struct/Func_get_data.fsti
index e2e9e6f..b16f35a 100644
--- base/core_ref_struct/Func_get_data.fsti
+++ head/core_ref_struct/Func_get_data.fsti
@@ -7,9 +7,9 @@ divergent fn func_get_data (var_c: (ref Struct_child.struct_child))
 requires
   exists* (val_c_0: Struct_child.struct_child).
   ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-    (Struct_child.struct_child__pred (!var_c) 1.0R))
+    (Struct_child.struct_child__pred val_c_0 1.0R))
 returns return_1 : Int32.t
 ensures
   exists* (val_c_0: Struct_child.struct_child).
   ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-    (Struct_child.struct_child__pred (!var_c) 1.0R))
\ No newline at end of file
+    (Struct_child.struct_child__pred val_c_0 1.0R))
\ No newline at end of file
diff --git base/core_ref_struct/Func_has_parent.fst head/core_ref_struct/Func_has_parent.fst
index 45f3aa9..3fb9356 100644
--- base/core_ref_struct/Func_has_parent.fst
+++ head/core_ref_struct/Func_has_parent.fst
@@ -7,12 +7,12 @@ divergent fn func_has_parent (var_c: (ref Struct_child.struct_child))
   requires
     exists* (val_c_0: Struct_child.struct_child).
     ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-      (Struct_child.struct_child__pred (!var_c) 1.0R))
+      (Struct_child.struct_child__pred val_c_0 1.0R))
   returns return_1 : bool
   ensures
     exists* (val_c_0: Struct_child.struct_child).
     ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-      (Struct_child.struct_child__pred (!var_c) 1.0R))
+      (Struct_child.struct_child__pred val_c_0 1.0R))
 {
   let mut var_c = var_c;
   return (not (Pulse.Lib.C.CoreRef.core_is_null (!(Struct_child.struct_child__get_up (!var_c)))));
diff --git base/core_ref_struct/Func_has_parent.fsti head/core_ref_struct/Func_has_parent.fsti
index 8aec117..34ff227 100644
--- base/core_ref_struct/Func_has_parent.fsti
+++ head/core_ref_struct/Func_has_parent.fsti
@@ -7,9 +7,9 @@ divergent fn func_has_parent (var_c: (ref Struct_child.struct_child))
 requires
   exists* (val_c_0: Struct_child.struct_child).
   ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-    (Struct_child.struct_child__pred (!var_c) 1.0R))
+    (Struct_child.struct_child__pred val_c_0 1.0R))
 returns return_1 : bool
 ensures
   exists* (val_c_0: Struct_child.struct_child).
   ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-    (Struct_child.struct_child__pred (!var_c) 1.0R))
\ No newline at end of file
+    (Struct_child.struct_child__pred val_c_0 1.0R))
\ No newline at end of file
diff --git base/core_ref_struct/Func_set_data.fst head/core_ref_struct/Func_set_data.fst
index 1c0d2e5..6f3cd33 100644
--- base/core_ref_struct/Func_set_data.fst
+++ head/core_ref_struct/Func_set_data.fst
@@ -7,12 +7,12 @@ divergent fn func_set_data (var_c: (ref Struct_child.struct_child)) (var_v: Int3
   requires
     exists* (val_c_0: Struct_child.struct_child).
     ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-      (Struct_child.struct_child__pred (!var_c) 1.0R))
+      (Struct_child.struct_child__pred val_c_0 1.0R))
   returns return_1 : unit
   ensures
     exists* (val_c_0: Struct_child.struct_child).
     ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-      (Struct_child.struct_child__pred (!var_c) 1.0R))
+      (Struct_child.struct_child__pred val_c_0 1.0R))
 {
   let mut var_c = var_c;
   let mut var_v = var_v;
diff --git base/core_ref_struct/Func_set_data.fsti head/core_ref_struct/Func_set_data.fsti
index 5646f81..8ac597e 100644
--- base/core_ref_struct/Func_set_data.fsti
+++ head/core_ref_struct/Func_set_data.fsti
@@ -7,9 +7,9 @@ divergent fn func_set_data (var_c: (ref Struct_child.struct_child)) (var_v: Int3
 requires
   exists* (val_c_0: Struct_child.struct_child).
   ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-    (Struct_child.struct_child__pred (!var_c) 1.0R))
+    (Struct_child.struct_child__pred val_c_0 1.0R))
 returns return_1 : unit
 ensures
   exists* (val_c_0: Struct_child.struct_child).
   ((Pulse.Lib.Reference.pts_to var_c #1.0R val_c_0) **
-    (Struct_child.struct_child__pred (!var_c) 1.0R))
\ No newline at end of file
+    (Struct_child.struct_child__pred val_c_0 1.0R))
\ No newline at end of file
diff --git base/core_ref_struct/Struct_parent.fst head/core_ref_struct/Struct_parent.fst
index a825e3f..4c5b50e 100644
--- base/core_ref_struct/Struct_parent.fst
+++ head/core_ref_struct/Struct_parent.fst
@@ -22,7 +22,7 @@ let predicate struct_parent__pred
       (this).struct_parent__down
       #p
       val_parent_0.struct_parent__spec__down_0) **
-    (Struct_child.struct_child__pred (!(this).struct_parent__down) p))
+    (Struct_child.struct_child__pred val_parent_0.struct_parent__spec__down_0 p))
 [@@pulse_eager_unfold] let predicate struct_parent__uninit_pred ([@@@mkey] this: struct_parent) =
   ((Pulse.Lib.Reference.pts_to_uninit (this).struct_parent__down))
 [@@pulse_intro]
@@ -36,7 +36,7 @@ struct_parent__pred_unfold
   (this).struct_parent__down
   #p
   val_parent_0.struct_parent__spec__down_0)
-  ensures (Struct_child.struct_child__pred (!(this).struct_parent__down) p)
+  ensures (Struct_child.struct_child__pred val_parent_0.struct_parent__spec__down_0 p)
 {
   unfold struct_parent__pred this p val_parent_0
 }
@@ -47,7 +47,7 @@ struct_parent__pred_fold
     (p: perm)
     (val_down_0: Struct_child.struct_child)
   requires (Pulse.Lib.Reference.pts_to (this).struct_parent__down #p val_down_0)
-  requires (Struct_child.struct_child__pred (!(this).struct_parent__down) p)
+  requires (Struct_child.struct_child__pred val_down_0 p)
   ensures struct_parent__pred this p ({
       struct_parent__spec__down_0 = val_down_0;
     })
diff --git base/core_ref_use/Func_store.fst head/core_ref_use/Func_store.fst
index 41eeb79..55bf01b 100644
--- base/core_ref_use/Func_store.fst
+++ head/core_ref_use/Func_store.fst
@@ -7,12 +7,12 @@ divergent fn func_store (var_b: (ref Struct_bar.struct_bar))
   requires
     exists* (val_b_0: Struct_bar.struct_bar) (val_b_1: Struct_bar.struct_bar__spec).
     ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
-      (Struct_bar.struct_bar__pred (!var_b) 1.0R val_b_1))
+      (Struct_bar.struct_bar__pred val_b_0 1.0R val_b_1))
   returns return_1 : unit
   ensures
     exists* (val_b_0: Struct_bar.struct_bar) (val_b_1: Struct_bar.struct_bar__spec).
     ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
-      (Struct_bar.struct_bar__pred (!var_b) 1.0R val_b_1))
+      (Struct_bar.struct_bar__pred val_b_0 1.0R val_b_1))
 {
   let mut var_b = var_b;
   let mut var_c : core_ref;
diff --git base/core_ref_use/Func_store.fsti head/core_ref_use/Func_store.fsti
index 4879ddf..3fe949b 100644
--- base/core_ref_use/Func_store.fsti
+++ head/core_ref_use/Func_store.fsti
@@ -7,9 +7,9 @@ divergent fn func_store (var_b: (ref Struct_bar.struct_bar))
 requires
   exists* (val_b_0: Struct_bar.struct_bar) (val_b_1: Struct_bar.struct_bar__spec).
   ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
-    (Struct_bar.struct_bar__pred (!var_b) 1.0R val_b_1))
+    (Struct_bar.struct_bar__pred val_b_0 1.0R val_b_1))
 returns return_1 : unit
 ensures
   exists* (val_b_0: Struct_bar.struct_bar) (val_b_1: Struct_bar.struct_bar__spec).
   ((Pulse.Lib.Reference.pts_to var_b #1.0R val_b_0) **
-    (Struct_bar.struct_bar__pred (!var_b) 1.0R val_b_1))
\ No newline at end of file
+    (Struct_bar.struct_bar__pred val_b_0 1.0R val_b_1))
\ No newline at end of file
diff --git base/core_ref_use/Func_via_back.fst head/core_ref_use/Func_via_back.fst
index 7942298..ad92041 100644
--- base/core_ref_use/Func_via_back.fst
+++ head/core_ref_use/Func_via_back.fst
@@ -7,7 +7,7 @@ divergent fn func_via_back (var_p: (ref Struct_inner.struct_inner))
   requires
     exists* (val_p_0: Struct_inner.struct_inner) (val_p_1: Struct_inner.struct_inner__spec).
     ((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
-      (Struct_inner.struct_inner__pred (!var_p) 1.0R val_p_1))
+      (Struct_inner.struct_inner__pred val_p_0 1.0R val_p_1))
   requires
     (exists* (bv: Struct_bar.struct_bar).
 pts_to (Pulse.Lib.C.CoreRef.core_to_ref Struct_bar.struct_bar
@@ -16,7 +16,7 @@ pts_to (Pulse.Lib.C.CoreRef.core_to_ref Struct_bar.struct_bar
   ensures
     exists* (val_p_0: Struct_inner.struct_inner) (val_p_1: Struct_inner.struct_inner__spec).
     ((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
-      (Struct_inner.struct_inner__pred (!var_p) 1.0R val_p_1))
+      (Struct_inner.struct_inner__pred val_p_0 1.0R val_p_1))
   ensures
     (exists* (bv: Struct_bar.struct_bar).
 pts_to (Pulse.Lib.C.CoreRef.core_to_ref Struct_bar.struct_bar
diff --git base/core_ref_use/Func_via_back.fsti head/core_ref_use/Func_via_back.fsti
index fdfb719..5995994 100644
--- base/core_ref_use/Func_via_back.fsti
+++ head/core_ref_use/Func_via_back.fsti
@@ -7,7 +7,7 @@ divergent fn func_via_back (var_p: (ref Struct_inner.struct_inner))
 requires
   exists* (val_p_0: Struct_inner.struct_inner) (val_p_1: Struct_inner.struct_inner__spec).
   ((Pulse.Lib.Reference.pts_to var_p #1.0R val_p_0) **
-    (Struct_inner.struct_inner__pred (!var_p) 1.0R val_p_1))
+    (Struct_inner.struct_inner__pred val_p_0 1.0R val_p_1))
 requires
   (exists* (bv: Struct_bar.struct_bar).

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

[hei411]

Follow-up: call sites now infer the witness instead of computing it syntactically.

Previously the erased c witness was read off the declared type of the variable being called through, which put the witness in the variable's interface: a variable could only hold callees agreeing on _plain annotations and ghost arity. Call sites now emit _.

Three changes together:

1. c is the pair (ELIMS & GHOSTS), each side right-nested binary — eta_expanded_pair is binary, and F*'s a & b & c is a flat tuple3, so only a right-nested spine can be solved. Unconditional, so every fnptr of a given C type shares one c.
2. The wrapper's requires destructures by pattern, not fst/snd. Not interchangeable: a pattern on an unsolved witness is a stuck match, so the prover defers and eta solves the spine; projections look matchable immediately, so the prover commits and is stuck with a non-invertible fst (reveal ?w) =?= val_a_0.
3. emit_fnptr_spec_core handles decl.ghost_args, which it previously ignored.

Two consequences of that match, both commented in-place since neither is guessable: Pulse's spec-level ! doesn't cross a match branch (it degrades to the stateful read), and with_pure is left partially applied there. The requires therefore uses the witness binding name and pure. Neither applies to the ensures, which must stay definitionally equal to the callee's post — so each ownership group is emitted twice, deliberately. The body eta-expands in a single rewrite each; per-level works to depth 1 then fails on the inner Ghost projection.

assign_across_shapes/call_across_shapes put four callees in one variable — elim/ghost counts (2,0), (0,0), (0,1), (0,2) — so both halves disagree and the ghost side is empty, singular and nested. test/func_pointer needed 11 hand-written witness types updated to erased (unit & unit).

Drive-by: dropped the _ghost_args from the struct ops fields — pal-ghost-arg is only read for a FunctionDecl, never a FieldDecl, so they were silently ignored no-ops — and corrected the header comment that claimed otherwise.

[gebner]

!diff

[hei411]

Two commits: a revert of emit.rs back to main, then a re-implementation without the HashMap.

The encoding is unchanged — c is ((elims) & (ghosts)), right-nested binary, inferred as _ at call sites. What's gone is deref_subst (a map keyed on rendered expressions) and the hack that emitted every param group twice.

deref_subst existed because the witness leaves must be bound by pattern: a projection like fst (fst (reveal ?w)) isn't an invertible head, so call sites fail with Error 228. That pattern desugars to a match, and Pulse's !r-in-a-spec rewrite won't traverse into a match branch.

But !var_a was redundant: emit_type_slprop_inner binds the pointee as val_a_0 two lines earlier. Recursing with that binding instead of Deref(this) means ! is never emitted under the match, so the problem can't arise. That takes one emitter-only IR node, ExprT::SpecVal. Refinements fall out for free, and requires/ensures now share docs, which kills the emit-twice hack. subst_this_rvalue gains a small SpecSubst param so its existing traversal also covers user-written _requires; no new walker. The pure-for-with_pure switch stays — that breakage is the missing continuation, not !.

Side effect: every function now spells pointee ownership val_a_0 instead of (!var_a). Uniform and semantically identical; the only thing it broke was extract_base_ident, which has to see through SpecVal.

Validated by diffing against the pre-revert output — Funcptr_* modules are byte-identical, all other diffs are that one substitution. make test green.

[hei411]

This PR also closes #277

[hei411]

Writing a new PR for this