Skip to content

Pass a caller's pointer slot through an untyped out-parameter - #225

Draft
nikswamy wants to merge 4 commits into
nswamy/pal-pr28-nullable-caller-transferfrom
nswamy/pal-pr11-core-ref-out-cell
Draft

Pass a caller's pointer slot through an untyped out-parameter#225
nikswamy wants to merge 4 commits into
nswamy/pal-pr28-nullable-caller-transferfrom
nswamy/pal-pr11-core-ref-out-cell

Conversation

@nikswamy

@nikswamy nikswamy commented Aug 19, 2026

Copy link
Copy Markdown
Contributor

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

Base: nswamy/pal-pr28-nullable-caller-transfer — a stacked PR. It depends on nswamy/pal-pr28-nullable-caller-transfer, nswamy/pal-pr13-sizeof-abi, 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-pr28-nullable-caller-transfer also carries the commits from nswamy/pal-pr13-sizeof-abi until those land.

f((void const **)&typedLocal) is how every acquire-a-buffer interface is spelled; the
cast was dropped and a ref (ref T) reached a ref core_ref parameter, which is
ill-typed. ref_to_core erases the type of a pointer value and says nothing about the
slot that holds one, so core_cell is added for that view, with the shifts that move
ownership across it — asymmetric, because an out-parameter goes in empty and comes back
full, and accepting either an uninitialized slot or one just set to NULL. Casts are
stripped before the argument's type is inferred, or inference reports the type the cast
asks for and the shift is never emitted. What the acquired buffer means is still the
contract's business.

Commits

  • Model the cell that holds a raw pointer
  • Pass a caller's pointer slot through an untyped out-parameter
  • Name both directions of the raw pointer cast

Testing

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

@nikswamy2
nikswamy2 force-pushed the nswamy/pal-pr11-core-ref-out-cell branch from 8874d8b to cd02620 Compare August 20, 2026 05:41
nikswamy and others added 4 commits August 20, 2026 12:56
@nikswamy @gebner
Give each record type the size its ABI assigns it
31a249b 
`sizeof(T)` translated to `Pulse.Lib.C.Sizeof.c_sizeof T`, which commits
to no particular value. That is fine for comparing a size against itself,
but it leaves any arithmetic over sizes unbounded: a proof cannot show
that `sizeof(A) + n + sizeof(B)` does not overflow `size_t` when the two
sizes could be anything.

clang already knows what the target ABI gives every complete record type.
Carry that number on the record's definition and emit it, in the record's
own generated module, as a refinement-typed constant that `sizeof` sites
then refer to:

    assume val struct__pair__c_sizeof
      : (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == c_sizeof struct__pair})

Introducing the size once, on the type, is what keeps this sound. Stating
it at each `sizeof` site instead would let two sites claim different sizes
for the same type. A refinement-typed constant rather than a lemma with an
`SMTPat` because the size of a specific type is a ground fact, and a
trigger for it would contain no variable, which Z3 warns about and F* then
rejects.

Non-record types are unaffected and still size opaquely.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d
(cherry picked from commit 7973441)
@nikswamy @gebner
Model the cell that holds a raw pointer
6c3ec4e 
`ref_to_core` erases the type of a pointer value. It does not say anything
about the slot that holds one, which is what an untyped out-parameter hands
its callee: the same machine word, viewed at a different type.

Add `core_cell` for that view, with the shifts that move ownership across it.
An out-parameter goes in empty and comes back full, so the two halves are not
symmetric; and the slot a caller passes has almost always just been set to
NULL rather than left uninitialized, so the empty half accepts either.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d
(cherry picked from commit 2640b37)
@nikswamy @gebner
Pass a caller's pointer slot through an untyped out-parameter
3d10b6d 
`f((void const ** )&typedLocal)` is how every acquire-a-buffer interface is
spelled. Until now the cast was dropped and a `ref (ref T)` reached a
`ref core_ref` parameter, which is ill-typed.

Emit the cell view instead, and walk the ownership across it around the call
in the same way nullable arguments are already handled. Casts have to be
stripped before the argument's type is inferred, or inference reports the
type the cast asks for and the shift is never emitted.

What the acquired buffer means is still the contract's business: only the
callee's `_ensures`, written in terms of `core_to_ref`, licenses reading it
at a type.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d
(cherry picked from commit d677cee)
@nikswamy @gebner
Name both directions of the raw pointer cast
1070a85 
A caller that recovers a typed pointer from a slot the callee wrote often has
to name the raw address again -- to say which loan it is holding, say. Only
one direction of the round trip was stated, so that step could not be taken.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 981f7d3c-6a91-47ad-84d7-7aadf747123d
(cherry picked from commit 068411a)
@gebner
gebner force-pushed the nswamy/pal-pr11-core-ref-out-cell branch from cd02620 to 1070a85 Compare August 20, 2026 19:56
@gebner

gebner commented Aug 26, 2026

Copy link
Copy Markdown
Contributor

!diff

@github-actions

github-actions Bot commented Aug 26, 2026

Copy link
Copy Markdown

Generated F* output diff

Effect of this pull request on the F* code pal generates for the test suite (4f0c689 → 1070a85).

Summary 
 {base => head}/addr_global/Struct_ops_anon_1.fst                    |   3 +++
 {base => head}/anon_struct/Struct_baz.fst                           |   3 +++
 {base => head}/anon_struct/Struct_baz_anon_1.fst                    |   3 +++
 {base => head}/anon_struct/Struct_profile.fst                       |   3 +++
 {base => head}/anon_struct/Struct_profiles.fst                      |   3 +++
 {base => head}/anon_struct/Struct_profiles_anon_1.fst               |   4 ++++
 {base => head}/antiquot/Struct_my_pair_anon_1.fst                   |   4 ++++
 {base => head}/antiquot/Union_my_union_anon_1.fst                   |   4 ++++
 {base => head}/array_addressof_loses_index/Struct_containercopy.fst |   4 ++++
 {base => head}/array_test/Struct_b32_struct_anon_1.fst              |   4 ++++
 {base => head}/array_test/Struct_two_arrays_anon_1.fst              |   4 ++++
 {base => head}/array_test/Struct_uptr_struct_anon_1.fst             |   4 ++++
 {base => head}/array_update/Struct_entry.fst                        |   3 +++
 {base => head}/array_update/Struct_point.fst                        |   3 +++
 {base => head}/arrayptr_ref/Struct_SUBRANGE_anon_1.fst              |   4 ++++
 {base => head}/bitfields/Struct_bits.fst                            |   3 +++
 {base => head}/bitfields/Struct_flags.fst                           |   3 +++
 {base => head}/bitfields/Struct_tdef.fst                            |   3 +++
 {base => head}/char_array_padding/Struct_entry_anon_1.fst           |   4 ++++
 {base => head}/container_field_read/Struct_pair.fst                 |   3 +++
 {base => head}/container_of/Struct_ack_tracker.fst                  |   3 +++
 {base => head}/container_of/Struct_packet_space.fst                 |   4 ++++
 {base => head}/containing_record/Struct_inner.fst                   |   3 +++
 {base => head}/containing_record/Struct_outer.fst                   |   3 +++
 {base => head}/core_ref_back_pointer_cycle/Struct_bar.fst           |   3 +++
 {base => head}/core_ref_back_pointer_cycle/Struct_inner.fst         |   3 +++
 {base => head}/core_ref_chain/Struct_a.fst                          |   3 +++
 {base => head}/core_ref_chain/Struct_b.fst                          |   3 +++
 /dev/null => head/core_ref_out_cell/Func_acquire.fst                |  16 ++++++++++++++
 /dev/null => head/core_ref_out_cell/Func_release.fst                |  12 +++++++++++
 /dev/null => head/core_ref_out_cell/Func_use.fst                    |  22 +++++++++++++++++++
 /dev/null => head/core_ref_out_cell/Func_use.fsti                   |   7 ++++++
 /dev/null => head/core_ref_out_cell/Struct_hdr.fst                  |  98 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/core_ref_out_cell/TranslationErrors.fst           |   1 +
 /dev/null => head/core_ref_out_cell/Typedef_PAL_RAW_CPTR.fst        |  16 ++++++++++++++
 /dev/null => head/core_ref_out_cell/diagnostics.json                |   1 +
 {base => head}/core_ref_struct/Struct_child.fst                     |   3 +++
 {base => head}/core_ref_struct/Struct_parent.fst                    |   3 +++
 {base => head}/core_ref_use/Struct_bar.fst                          |   3 +++
 {base => head}/core_ref_use/Struct_inner.fst                        |   3 +++
 {base => head}/core_ref_use_ptr/Struct_bar.fst                      |   3 +++
 {base => head}/core_ref_use_ptr/Struct_inner.fst                    |   3 +++
 {base => head}/default_test/Struct_point_anon_1.fst                 |   3 +++
 {base => head}/do_while/Struct_counter.fst                          |   3 +++
 {base => head}/dpe/Struct__engine_record_t.fst                      |   4 ++++
 {base => head}/dpe/Struct__profile_descriptor_t.fst                 |   4 ++++
 {base => head}/dpe/Struct_context_t_anon_1.fst                      |   4 ++++
 {base => head}/dpe/Struct_l1_context_t_anon_1.fst                   |   4 ++++
 {base => head}/dpe/Union__u_context_t.fst                           |   3 +++
 {base => head}/eager_unfold_struct/Struct_point.fst                 |   3 +++
 {base => head}/float_double/Struct_float_pair_anon_1.fst            |   4 ++++
 {base => head}/fnptr_core_ref/Struct_callbacks.fst                  |   3 +++
 {base => head}/fnptr_core_ref/Struct_parent.fst                     |   3 +++
 {base => head}/fnptr_core_ref/Struct_typedef_callbacks.fst          |   4 ++++
 {base => head}/fnptr_core_ref/Struct_typedef_parent.fst             |   4 ++++
 {base => head}/forward_struct/Struct_point.fst                      |   3 +++
 {base => head}/func_pointer/Struct_itemx.fst                        |   3 +++
 {base => head}/func_pointer/Struct_mo_a.fst                         |   3 +++
 {base => head}/func_pointer/Struct_mo_b.fst                         |   3 +++
 {base => head}/func_pointer/Struct_mo_ops.fst                       |   3 +++
 {base => head}/func_pointer/Struct_ops.fst                          |   3 +++
 {base => head}/func_pointer/Struct_ops_c.fst                        |   3 +++
 {base => head}/func_pointer/Struct_vtable2.fst                      |   3 +++
 {base => head}/func_pointer/Union_op_or_int.fst                     |   3 +++
 {base => head}/func_pointer2/Struct_ops_anon_1.fst                  |   3 +++
 {base => head}/func_pointer2/Union_uops_anon_1.fst                  |   3 +++
 {base => head}/generic_selection/Struct_generic_slots.fst           |   4 ++++
 {base => head}/global_header_addr/Struct_hs.fst                     |   3 +++
 {base => head}/global_header_addr/Struct_ms.fst                     |   3 +++
 {base => head}/global_purity/Struct_point.fst                       |   3 +++
 {base => head}/inline_array_aliasing/Struct_mixed.fst               |   3 +++
 {base => head}/inner_struct/Struct_foo.fst                          |   3 +++
 {base => head}/inner_struct/Struct_foo2.fst                         |   3 +++
 {base => head}/inner_struct/Struct_xy.fst                           |   3 +++
 {base => head}/issue28/Struct__point.fst                            |   3 +++
 {base => head}/malloc/Struct_point_anon_1.fst                       |   3 +++
 {base => head}/memset/Struct_triple.fst                             |   3 +++
 {base => head}/memset/Struct_withbuf.fst                            |   3 +++
 {base => head}/nested_unions/Struct_stru.fst                        |   3 +++
 {base => head}/nested_unions/Union_ab.fst                           |   3 +++
 {base => head}/nested_unions/Union_nested.fst                       |   3 +++
 {base => head}/nested_unions/Union_nested2.fst                      |   3 +++
 {base => head}/nullable_out/Struct_pair.fst                         |   3 +++
 {base => head}/nullable_out_struct/Struct_pair.fst                  |   3 +++
 {base => head}/packet_space_connection/Struct_connection.fst        |   3 +++
 {base => head}/packet_space_connection/Struct_packet_space.fst      |   4 ++++
 {base => head}/pointer_view/Struct_node.fst                         |   3 +++
 {base => head}/recursive_struct/Struct_node.fst                     |   3 +++
 {base => head}/refine_struct/Struct_b32_struct.fst                  |   3 +++
 {base => head}/refine_struct/Struct_forward_refined.fst             |   4 ++++
 {base => head}/refine_struct/Struct_selfref.fst                     |   3 +++
 {base => head}/refine_struct/Struct_wrapper.fst                     |   3 +++
 {base => head}/refine_typedef_pred/Struct_foo.fst                   |   3 +++
 {base => head}/simple_struct/Struct_simple.fst                      |   3 +++
 {base => head}/sizeof/Func_size_of_two_ints_positive.fst            |   2 +-
 {base => head}/sizeof/Func_size_of_union_positive.fst               |   2 +-
 {base => head}/sizeof/Func_size_of_zero_sized_struct.fst            |   2 +-
 {base => head}/sizeof/Func_size_of_zero_sized_union.fst             |   2 +-
 {base => head}/sizeof/Struct_two_ints_anon_1.fst                    |   4 ++++
 {base => head}/sizeof/Struct_zero_s
... (summary truncated)

Full diff: full diff artifact

Diff 
diff --git base/addr_global/Struct_ops_anon_1.fst head/addr_global/Struct_ops_anon_1.fst
index 48f6313..cd69db8 100644
--- base/addr_global/Struct_ops_anon_1.fst
+++ head/addr_global/Struct_ops_anon_1.fst
@@ -13,6 +13,9 @@ assume val struct_ops_anon_1__sizeof_pos (a: Type0 { a == struct_ops_anon_1 }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_ops_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_ops_anon_1)})
 [@@pulse_eager_unfold] let predicate struct_ops_anon_1__pred
       ([@@@mkey] this: struct_ops_anon_1)
       (p: perm) =
diff --git base/anon_struct/Struct_baz.fst head/anon_struct/Struct_baz.fst
index 9914752..83af7ab 100644
--- base/anon_struct/Struct_baz.fst
+++ head/anon_struct/Struct_baz.fst
@@ -11,6 +11,9 @@ assume val struct_baz__sizeof_pos (a: Type0 { a == struct_baz }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_baz__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_baz)})
 [@@pulse_eager_unfold] let predicate struct_baz__pred ([@@@mkey] this: struct_baz) (p: perm) =
   ((Struct_baz_anon_1.struct_baz_anon_1__pred this.struct_baz__foo p) **
     (Struct_baz_anon_1.struct_baz_anon_1__pred this.struct_baz__bar p))
diff --git base/anon_struct/Struct_baz_anon_1.fst head/anon_struct/Struct_baz_anon_1.fst
index ee6a2fe..1794f0a 100644
--- base/anon_struct/Struct_baz_anon_1.fst
+++ head/anon_struct/Struct_baz_anon_1.fst
@@ -10,6 +10,9 @@ assume val struct_baz_anon_1__sizeof_pos (a: Type0 { a == struct_baz_anon_1 }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_baz_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 4 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_baz_anon_1)})
 [@@pulse_eager_unfold] let predicate struct_baz_anon_1__pred
       ([@@@mkey] this: struct_baz_anon_1)
       (p: perm) =
diff --git base/anon_struct/Struct_profile.fst head/anon_struct/Struct_profile.fst
index 40966a6..61687ab 100644
--- base/anon_struct/Struct_profile.fst
+++ head/anon_struct/Struct_profile.fst
@@ -10,6 +10,9 @@ assume val struct_profile__sizeof_pos (a: Type0 { a == struct_profile }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_profile__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_profile)})
 [@@erasable] noeq type struct_profile__spec = {
   struct_profile__spec__name_0: Int8.t;
 }
diff --git base/anon_struct/Struct_profiles.fst head/anon_struct/Struct_profiles.fst
index d1ac978..8084e92 100644
--- base/anon_struct/Struct_profiles.fst
+++ head/anon_struct/Struct_profiles.fst
@@ -11,6 +11,9 @@ assume val struct_profiles__sizeof_pos (a: Type0 { a == struct_profiles }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_profiles__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 32 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_profiles)})
 [@@erasable] noeq type struct_profiles__spec = {
   struct_profiles__spec__vivify1_0: Struct_profile.struct_profile__spec;
   struct_profiles__spec__stack_0: Struct_profiles_anon_1.struct_profiles_anon_1__spec;
diff --git base/anon_struct/Struct_profiles_anon_1.fst head/anon_struct/Struct_profiles_anon_1.fst
index acc62f2..67c800e 100644
--- base/anon_struct/Struct_profiles_anon_1.fst
+++ head/anon_struct/Struct_profiles_anon_1.fst
@@ -12,6 +12,10 @@ assume val struct_profiles_anon_1__sizeof_pos (a: Type0 { a == struct_profiles_a
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_profiles_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 24 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_profiles_anon_1)})
 [@@erasable] noeq type struct_profiles_anon_1__spec = {
   struct_profiles_anon_1__spec__begin_0: (ref Typedef_profile.ty_profile);
   struct_profiles_anon_1__spec__begin_1: Typedef_profile.ty_profile;
diff --git base/antiquot/Struct_my_pair_anon_1.fst head/antiquot/Struct_my_pair_anon_1.fst
index fc6196a..28a8205 100644
--- base/antiquot/Struct_my_pair_anon_1.fst
+++ head/antiquot/Struct_my_pair_anon_1.fst
@@ -11,6 +11,10 @@ assume val struct_my_pair_anon_1__sizeof_pos (a: Type0 { a == struct_my_pair_ano
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_my_pair_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_my_pair_anon_1)})
 [@@pulse_eager_unfold] let predicate struct_my_pair_anon_1__pred
       ([@@@mkey] this: struct_my_pair_anon_1)
       (p: perm) =
diff --git base/antiquot/Union_my_union_anon_1.fst head/antiquot/Union_my_union_anon_1.fst
index a73eab1..12bd05f 100644
--- base/antiquot/Union_my_union_anon_1.fst
+++ head/antiquot/Union_my_union_anon_1.fst
@@ -12,6 +12,10 @@ assume val union_my_union_anon_1__sizeof_pos (a: Type0 { a == union_my_union_ano
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val union_my_union_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    union_my_union_anon_1)})
 [@@pulse_eager_unfold] let predicate union_my_union_anon_1__pred
       ([@@@mkey] this: union_my_union_anon_1)
       (p: perm) =
diff --git base/array_addressof_loses_index/Struct_containercopy.fst head/array_addressof_loses_index/Struct_containercopy.fst
index b584ab6..11d1270 100644
--- base/array_addressof_loses_index/Struct_containercopy.fst
+++ head/array_addressof_loses_index/Struct_containercopy.fst
@@ -10,6 +10,10 @@ assume val struct_containercopy__sizeof_pos (a: Type0 { a == struct_containercop
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_containercopy__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_containercopy)})
 [@@erasable] noeq type struct_containercopy__spec = {
   struct_containercopy__spec__elements_0: (full_array_spec Int32.t);
 }
diff --git base/array_test/Struct_b32_struct_anon_1.fst head/array_test/Struct_b32_struct_anon_1.fst
index 3da738e..763b07f 100644
--- base/array_test/Struct_b32_struct_anon_1.fst
+++ head/array_test/Struct_b32_struct_anon_1.fst
@@ -10,6 +10,10 @@ assume val struct_b32_struct_anon_1__sizeof_pos (a: Type0 { a == struct_b32_stru
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_b32_struct_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_b32_struct_anon_1)})
 [@@erasable] noeq type struct_b32_struct_anon_1__spec = {
   struct_b32_struct_anon_1__spec__x_0: (full_array_spec UInt8.t);
 }
diff --git base/array_test/Struct_two_arrays_anon_1.fst head/array_test/Struct_two_arrays_anon_1.fst
index 45ba05a..d50a0fa 100644
--- base/array_test/Struct_two_arrays_anon_1.fst
+++ head/array_test/Struct_two_arrays_anon_1.fst
@@ -11,6 +11,10 @@ assume val struct_two_arrays_anon_1__sizeof_pos (a: Type0 { a == struct_two_arra
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_two_arrays_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_two_arrays_anon_1)})
 [@@erasable] noeq type struct_two_arrays_anon_1__spec = {
   struct_two_arrays_anon_1__spec__x_0: (full_array_spec Int32.t);
   struct_two_arrays_anon_1__spec__y_0: (full_array_spec Int32.t);
diff --git base/array_test/Struct_uptr_struct_anon_1.fst head/array_test/Struct_uptr_struct_anon_1.fst
index ecd2b54..86c0aa0 100644
--- base/array_test/Struct_uptr_struct_anon_1.fst
+++ head/array_test/Struct_uptr_struct_anon_1.fst
@@ -10,6 +10,10 @@ assume val struct_uptr_struct_anon_1__sizeof_pos (a: Type0 { a == struct_uptr_st
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_uptr_struct_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_uptr_struct_anon_1)})
 [@@erasable] noeq type struct_uptr_struct_anon_1__spec = {
   struct_uptr_struct_anon_1__spec__x_0: (full_array_spec UInt32.t);
 }
diff --git base/array_update/Struct_entry.fst head/array_update/Struct_entry.fst
index c021ef0..8c2943f 100644
--- base/array_update/Struct_entry.fst
+++ head/array_update/Struct_entry.fst
@@ -11,6 +11,9 @@ assume val struct_entry__sizeof_pos (a: Type0 { a == struct_entry }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_entry__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_entry)})
 [@@pulse_eager_unfold] let predicate struct_entry__pred ([@@@mkey] this: struct_entry) (p: perm) =
   ((Typedef_uint64_t.ty_uint64_t__pred this.struct_entry__value p) **
     (Typedef_uint64_t.ty_uint64_t__pred this.struct_entry__time p))
diff --git base/array_update/Struct_point.fst head/array_update/Struct_point.fst
index 0ffcce9..6c32153 100644
--- base/array_update/Struct_point.fst
+++ head/array_update/Struct_point.fst
@@ -11,6 +11,9 @@ assume val struct_point__sizeof_pos (a: Type0 { a == struct_point }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_point__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_point)})
 [@@pulse_eager_unfold] let predicate struct_point__pred ([@@@mkey] this: struct_point) (p: perm) =
   emp
 [@@pulse_eager_unfold] let predicate struct_point__uninit_pred ([@@@mkey] this: struct_point) = emp
diff --git base/arrayptr_ref/Struct_SUBRANGE_anon_1.fst head/arrayptr_ref/Struct_SUBRANGE_anon_1.fst
index d5998d2..4b2da4d 100644
--- base/arrayptr_ref/Struct_SUBRANGE_anon_1.fst
+++ head/arrayptr_ref/Struct_SUBRANGE_anon_1.fst
@@ -11,6 +11,10 @@ assume val struct_subrange_anon_1__sizeof_pos (a: Type0 { a == struct_subrange_a
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_subrange_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_subrange_anon_1)})
 [@@pulse_eager_unfold] let predicate struct_subrange_anon_1__pred
       ([@@@mkey] this: struct_subrange_anon_1)
       (p: perm) =
diff --git base/bitfields/Struct_bits.fst head/bitfields/Struct_bits.fst
index f64bad2..8252080 100644
--- base/bitfields/Struct_bits.fst
+++ head/bitfields/Struct_bits.fst
@@ -11,6 +11,9 @@ assume val struct_bits__sizeof_pos (a: Type0 { a == struct_bits }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_bits__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 1 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_bits)})
 [@@pulse_eager_unfold] let predicate struct_bits__pred ([@@@mkey] this: struct_bits) (p: perm) = emp
 [@@pulse_eager_unfold] let predicate struct_bits__uninit_pred ([@@@mkey] this: struct_bits) = emp
 assume val struct_bits__aux_raw_unfolded ([@@@mkey] x: (ref struct_bits)) (p: perm) : slprop
diff --git base/bitfields/Struct_flags.fst head/bitfields/Struct_flags.fst
index e4e739a..7b2ee2b 100644
--- base/bitfields/Struct_flags.fst
+++ head/bitfields/Struct_flags.fst
@@ -12,6 +12,9 @@ assume val struct_flags__sizeof_pos (a: Type0 { a == struct_flags }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_flags__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_flags)})
 [@@pulse_eager_unfold] let predicate struct_flags__pred ([@@@mkey] this: struct_flags) (p: perm) =
   emp
 [@@pulse_eager_unfold] let predicate struct_flags__uninit_pred ([@@@mkey] this: struct_flags) = emp
diff --git base/bitfields/Struct_tdef.fst head/bitfields/Struct_tdef.fst
index fe69327..ef13a63 100644
--- base/bitfields/Struct_tdef.fst
+++ head/bitfields/Struct_tdef.fst
@@ -10,6 +10,9 @@ assume val struct_tdef__sizeof_pos (a: Type0 { a == struct_tdef }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_tdef__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 2 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_tdef)})
 [@@pulse_eager_unfold] let predicate struct_tdef__pred ([@@@mkey] this: struct_tdef) (p: perm) =
   ((Typedef_uint16_t.ty_uint16_t__pred this.struct_tdef__a p))
 [@@pulse_eager_unfold] let predicate struct_tdef__uninit_pred ([@@@mkey] this: struct_tdef) =
diff --git base/char_array_padding/Struct_entry_anon_1.fst head/char_array_padding/Struct_entry_anon_1.fst
index b5f0c04..610d7de 100644
--- base/char_array_padding/Struct_entry_anon_1.fst
+++ head/char_array_padding/Struct_entry_anon_1.fst
@@ -10,6 +10,10 @@ assume val struct_entry_anon_1__sizeof_pos (a: Type0 { a == struct_entry_anon_1
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_entry_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_entry_anon_1)})
 [@@pulse_eager_unfold] let predicate struct_entry_anon_1__pred
       ([@@@mkey] this: struct_entry_anon_1)
       (p: perm) =
diff --git base/container_field_read/Struct_pair.fst head/container_field_read/Struct_pair.fst
index 3fafbb9..91619cd 100644
--- base/container_field_read/Struct_pair.fst
+++ head/container_field_read/Struct_pair.fst
@@ -11,6 +11,9 @@ assume val struct_pair__sizeof_pos (a: Type0 { a == struct_pair }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_pair__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_pair)})
 [@@pulse_eager_unfold] let predicate struct_pair__pred ([@@@mkey] this: struct_pair) (p: perm) =
   ((Typedef_int32_t.ty_int32_t__pred this.struct_pair__first p) **
     (Typedef_int32_t.ty_int32_t__pred this.struct_pair__second p))
diff --git base/container_of/Struct_ack_tracker.fst head/container_of/Struct_ack_tracker.fst
index e7738ac..4d1a352 100644
--- base/container_of/Struct_ack_tracker.fst
+++ head/container_of/Struct_ack_tracker.fst
@@ -10,6 +10,9 @@ assume val struct_ack_tracker__sizeof_pos (a: Type0 { a == struct_ack_tracker })
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_ack_tracker__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 4 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_ack_tracker)})
 [@@pulse_eager_unfold] let predicate struct_ack_tracker__pred
       ([@@@mkey] this: struct_ack_tracker)
       (p: perm) =
diff --git base/container_of/Struct_packet_space.fst head/container_of/Struct_packet_space.fst
index 559a3ab..d77b603 100644
--- base/container_of/Struct_packet_space.fst
+++ head/container_of/Struct_packet_space.fst
@@ -13,6 +13,10 @@ assume val struct_packet_space__sizeof_pos (a: Type0 { a == struct_packet_space
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_packet_space__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 32 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_packet_space)})
 [@@erasable] noeq type struct_packet_space__spec = {
   struct_packet_space__spec__back_0: Typedef_int32_t.ty_int32_t;
 }
diff --git base/containing_record/Struct_inner.fst head/containing_record/Struct_inner.fst
index ff4f081..47d1101 100644
--- base/containing_record/Struct_inner.fst
+++ head/containing_record/Struct_inner.fst
@@ -10,6 +10,9 @@ assume val struct_inner__sizeof_pos (a: Type0 { a == struct_inner }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_inner__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 4 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_inner)})
 [@@pulse_eager_unfold] let predicate struct_inner__pred ([@@@mkey] this: struct_inner) (p: perm) =
   ((Typedef_int32_t.ty_int32_t__pred this.struct_inner__marker p))
 [@@pulse_eager_unfold] let predicate struct_inner__uninit_pred ([@@@mkey] this: struct_inner) =
diff --git base/containing_record/Struct_outer.fst head/containing_record/Struct_outer.fst
index e6716f8..840c951 100644
--- base/containing_record/Struct_outer.fst
+++ head/containing_record/Struct_outer.fst
@@ -11,6 +11,9 @@ assume val struct_outer__sizeof_pos (a: Type0 { a == struct_outer }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_outer__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_outer)})
 [@@pulse_eager_unfold] let predicate struct_outer__pred ([@@@mkey] this: struct_outer) (p: perm) =
   ((Typedef_int32_t.ty_int32_t__pred this.struct_outer__value p) **
     (Struct_inner.struct_inner__pred this.struct_outer__node p))
diff --git base/core_ref_back_pointer_cycle/Struct_bar.fst head/core_ref_back_pointer_cycle/Struct_bar.fst
index 728d84f..320f7a0 100644
--- base/core_ref_back_pointer_cycle/Struct_bar.fst
+++ head/core_ref_back_pointer_cycle/Struct_bar.fst
@@ -11,6 +11,9 @@ assume val struct_bar__sizeof_pos (a: Type0 { a == struct_bar }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_bar__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 24 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_bar)})
 [@@erasable] noeq type struct_bar__spec = {
   struct_bar__spec__other_0: Int64.t;
   struct_bar__spec__myinner_0: Struct_inner.struct_inner__spec;
diff --git base/core_ref_back_pointer_cycle/Struct_inner.fst head/core_ref_back_pointer_cycle/Struct_inner.fst
index 1647587..e4a9d34 100644
--- base/core_ref_back_pointer_cycle/Struct_inner.fst
+++ head/core_ref_back_pointer_cycle/Struct_inner.fst
@@ -11,6 +11,9 @@ assume val struct_inner__sizeof_pos (a: Type0 { a == struct_inner }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_inner__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_inner)})
 [@@erasable] noeq type struct_inner__spec = {
   struct_inner__spec__a_0: Int32.t;
 }
diff --git base/core_ref_chain/Struct_a.fst head/core_ref_chain/Struct_a.fst
index 0162aa5..8c12308 100644
--- base/core_ref_chain/Struct_a.fst
+++ head/core_ref_chain/Struct_a.fst
@@ -11,6 +11,9 @@ assume val struct_a__sizeof_pos (a: Type0 { a == struct_a }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_a__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_a)})
 [@@pulse_eager_unfold] let predicate struct_a__pred ([@@@mkey] this: struct_a) (p: perm) = emp
 [@@pulse_eager_unfold] let predicate struct_a__uninit_pred ([@@@mkey] this: struct_a) = emp
 assume val struct_a__aux_raw_unfolded ([@@@mkey] x: (ref struct_a)) (p: perm) : slprop
diff --git base/core_ref_chain/Struct_b.fst head/core_ref_chain/Struct_b.fst
index cb25c47..3e3ea77 100644
--- base/core_ref_chain/Struct_b.fst
+++ head/core_ref_chain/Struct_b.fst
@@ -11,6 +11,9 @@ assume val struct_b__sizeof_pos (a: Type0 { a == struct_b }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_b__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_b)})
 [@@erasable] noeq type struct_b__spec = {
   struct_b__spec__pa_0: Struct_a.struct_a;
 }
diff --git head/core_ref_out_cell/Func_acquire.fst head/core_ref_out_cell/Func_acquire.fst
new file mode 100644
index 0000000..0b04e31
--- /dev/null
+++ head/core_ref_out_cell/Func_acquire.fst
@@ -0,0 +1,16 @@
+module Func_acquire
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_acquire (var_n: UInt32.t) (var_buf: (ref Typedef_PAL_RAW_CPTR.ty_pal_raw_cptr))
+  requires ((Pulse.Lib.Reference.pts_to_uninit var_buf))
+  returns return_1 : Int32.t
+  ensures
+    exists* (val_buf_0: Typedef_PAL_RAW_CPTR.ty_pal_raw_cptr).
+    ((Pulse.Lib.Reference.pts_to var_buf #1.0R val_buf_0) **
+      (Typedef_PAL_RAW_CPTR.ty_pal_raw_cptr__pred (!var_buf) 1.0R))
+  ensures
+    (exists* (hv: Struct_hdr.struct_hdr).
+pts_to (Pulse.Lib.C.CoreRef.core_to_ref Struct_hdr.struct_hdr ((!var_buf))) hv)
+{ assume pure False; unreachable () }
\ No newline at end of file
diff --git head/core_ref_out_cell/Func_release.fst head/core_ref_out_cell/Func_release.fst
new file mode 100644
index 0000000..b475319
--- /dev/null
+++ head/core_ref_out_cell/Func_release.fst
@@ -0,0 +1,12 @@
+module Func_release
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_release (var_h: (ref Struct_hdr.struct_hdr))
+  requires
+    exists* (val_h_0: Struct_hdr.struct_hdr).
+    ((Pulse.Lib.Reference.pts_to var_h #1.0R val_h_0) **
+      (Struct_hdr.struct_hdr__pred (!var_h) 1.0R))
+  returns return_1 : unit
+{ assume pure False; unreachable () }
\ No newline at end of file
diff --git head/core_ref_out_cell/Func_use.fst head/core_ref_out_cell/Func_use.fst
new file mode 100644
index 0000000..ef47567
--- /dev/null
+++ head/core_ref_out_cell/Func_use.fst
@@ -0,0 +1,22 @@
+module Func_use
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_use ()
+  returns return_1 : Int32.t
+{
+  let mut var_h : (ref Struct_hdr.struct_hdr);
+  var_h := null;
+  let mut var_out : Struct_hdr.struct_hdr;
+  let mut var_s : Int32.t;
+  Pulse.Lib.C.CoreRef.to_core_cell_out (var_h);
+  var_s :=
+    (Func_acquire.func_acquire
+      (UInt32.uint_to_t (SizeT.v Struct_hdr.struct_hdr__c_sizeof))
+      (Pulse.Lib.C.CoreRef.core_cell var_h));
+  Pulse.Lib.C.CoreRef.of_core_cell (var_h);
+  var_out := (!(!var_h));
+  (Func_release.func_release (!var_h));
+  return (!(Struct_hdr.struct_hdr__get_a var_out));
+}
\ No newline at end of file
diff --git head/core_ref_out_cell/Func_use.fsti head/core_ref_out_cell/Func_use.fsti
new file mode 100644
index 0000000..dff9175
--- /dev/null
+++ head/core_ref_out_cell/Func_use.fsti
@@ -0,0 +1,7 @@
+module Func_use
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+divergent fn func_use ()
+returns return_1 : Int32.t
\ No newline at end of file
diff --git head/core_ref_out_cell/Struct_hdr.fst head/core_ref_out_cell/Struct_hdr.fst
new file mode 100644
index 0000000..032c0d9
--- /dev/null
+++ head/core_ref_out_cell/Struct_hdr.fst
@@ -0,0 +1,98 @@
+module Struct_hdr
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+noeq type struct_hdr = {
+  struct_hdr__a: Int32.t;
+  struct_hdr__b: Int32.t;
+}
+assume val struct_hdr__sizeof_pos (a: Type0 { a == struct_hdr }) :
+    Lemma
+    ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
+    [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_hdr__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_hdr)})
+[@@pulse_eager_unfold] let predicate struct_hdr__pred ([@@@mkey] this: struct_hdr) (p: perm) = emp
+[@@pulse_eager_unfold] let predicate struct_hdr__uninit_pred ([@@@mkey] this: struct_hdr) = emp
+assume val struct_hdr__aux_raw_unfolded ([@@@mkey] x: (ref struct_hdr)) (p: perm) : slprop
+assume val struct_hdr__a_1 (x: (ref struct_hdr)) : GTot (ref Int32.t)
+assume val struct_hdr__b_1 (x: (ref struct_hdr)) : GTot (ref Int32.t)
+assume val struct_hdr__a_container (r: (ref Int32.t)) : (ref struct_hdr)
+assume val struct_hdr__a_container_inv (p: (ref struct_hdr)) :
+    Lemma
+      (ensures (struct_hdr__a_container (struct_hdr__a_1 p)) == p)
+      [SMTPat (struct_hdr__a_container (struct_hdr__a_1 p))]
+assume val struct_hdr__a_proj_container_inv (r: (ref Int32.t)) :
+    Lemma
+      (ensures (struct_hdr__a_1 (struct_hdr__a_container r)) == r)
+      [SMTPat (struct_hdr__a_1 (struct_hdr__a_container r))]
+assume val struct_hdr__b_container (r: (ref Int32.t)) : (ref struct_hdr)
+assume val struct_hdr__b_container_inv (p: (ref struct_hdr)) :
+    Lemma
+      (ensures (struct_hdr__b_container (struct_hdr__b_1 p)) == p)
+      [SMTPat (struct_hdr__b_container (struct_hdr__b_1 p))]
+assume val struct_hdr__b_proj_container_inv (r: (ref Int32.t)) :
+    Lemma
+      (ensures (struct_hdr__b_1 (struct_hdr__b_container r)) == r)
+      [SMTPat (struct_hdr__b_1 (struct_hdr__b_container r))]
+assume val struct_hdr__a_proj_null :
+    (squash
+      ((struct_hdr__a_1 (Pulse.Lib.Reference.null #(struct_hdr))) ==
+        (Pulse.Lib.Reference.null #(Int32.t))))
+[@@pulse_intro]
+assume val struct_hdr__aux_raw_unfold (x: (ref struct_hdr)) (#p: perm) (vx: struct_hdr) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to x #p vx)
+      (fun _ ->
+        ((struct_hdr__aux_raw_unfolded x p) **
+          (Pulse.Lib.Reference.pts_to (struct_hdr__a_1 x) #p vx.struct_hdr__a) **
+          (Pulse.Lib.Reference.pts_to (struct_hdr__b_1 x) #p vx.struct_hdr__b))))
+[@@pulse_intro]
+assume val struct_hdr__aux_raw_fold (x: (ref struct_hdr)) (#p: perm) v_a v_b :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_hdr__aux_raw_unfolded x p) **
+        (Pulse.Lib.Reference.pts_to (struct_hdr__a_1 x) #p v_a) **
+        (Pulse.Lib.Reference.pts_to (struct_hdr__b_1 x) #p v_b))
+      (fun _ -> (Pulse.Lib.Reference.pts_to x #p { struct_hdr__a=v_a; struct_hdr__b=v_b; })))
+[@@pulse_intro]
+assume val struct_hdr__aux_raw_fold_uninit (x: (ref struct_hdr)) :
+    (stt_ghost
+      unit
+      emp_inames
+      ((struct_hdr__aux_raw_unfolded x 1.0R) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_hdr__a_1 x)) **
+        (Pulse.Lib.Reference.pts_to_uninit (struct_hdr__b_1 x)))
+      (fun _ -> (Pulse.Lib.Reference.pts_to_uninit x)))
+assume val struct_hdr__aux_raw_unfold_uninit (x: (ref struct_hdr)) :
+    (stt_ghost
+      unit
+      emp_inames
+      (Pulse.Lib.Reference.pts_to_uninit x)
+      (fun _ ->
+        ((struct_hdr__aux_raw_unfolded x 1.0R) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_hdr__a_1 x)) **
+          (Pulse.Lib.Reference.pts_to_uninit (struct_hdr__b_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_hdr__get_a (x: (ref struct_hdr)) (#p: perm) :
+    (stt_atomic
+      (ref Int32.t)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_hdr__aux_raw_unfolded x p)
+      (fun vx' -> ((struct_hdr__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_hdr__a_1 x)))))
+[@@pulse_impure_spec_no_proof_required]
+assume val struct_hdr__get_b (x: (ref struct_hdr)) (#p: perm) :
+    (stt_atomic
+      (ref Int32.t)
+      #PulseCore.Observability.Neutral
+      emp_inames
+      (struct_hdr__aux_raw_unfolded x p)
+      (fun vx' -> ((struct_hdr__aux_raw_unfolded x p) ** (rewrites_to vx' (struct_hdr__b_1 x)))))
+instance has_zero_default_struct_hdr : (has_zero_default struct_hdr) =
+  { zero_default = { struct_hdr__a = (Int32.int_to_t 0); struct_hdr__b = (Int32.int_to_t 0); } }
\ No newline at end of file
diff --git head/core_ref_out_cell/TranslationErrors.fst head/core_ref_out_cell/TranslationErrors.fst
new file mode 100644
index 0000000..bf62561
--- /dev/null
+++ head/core_ref_out_cell/TranslationErrors.fst
@@ -0,0 +1 @@
+module TranslationErrors
diff --git head/core_ref_out_cell/Typedef_PAL_RAW_CPTR.fst head/core_ref_out_cell/Typedef_PAL_RAW_CPTR.fst
new file mode 100644
index 0000000..7e075aa
--- /dev/null
+++ head/core_ref_out_cell/Typedef_PAL_RAW_CPTR.fst
@@ -0,0 +1,16 @@
+module Typedef_PAL_RAW_CPTR
+open Pulse
+open Pulse.Lib.C
+#lang-pulse
+
+unfold
+let ty_pal_raw_cptr : Type = core_ref
+[@@pulse_eager_unfold] let predicate ty_pal_raw_cptr__pred
+      ([@@@mkey] this: ty_pal_raw_cptr)
+      (p: perm) =
+  emp
+[@@pulse_eager_unfold] let predicate ty_pal_raw_cptr__uninit_pred
+      ([@@@mkey] this: ty_pal_raw_cptr) =
+  emp
+instance has_zero_default_ty_pal_raw_cptr : (has_zero_default ty_pal_raw_cptr) =
+  { zero_default = core_null }
\ No newline at end of file
diff --git head/core_ref_out_cell/diagnostics.json head/core_ref_out_cell/diagnostics.json
new file mode 100644
index 0000000..9e26dfe
--- /dev/null
+++ head/core_ref_out_cell/diagnostics.json
@@ -0,0 +1 @@
+{}
\ No newline at end of file
diff --git base/core_ref_struct/Struct_child.fst head/core_ref_struct/Struct_child.fst
index b3ceda1..86f20d7 100644
--- base/core_ref_struct/Struct_child.fst
+++ head/core_ref_struct/Struct_child.fst
@@ -11,6 +11,9 @@ assume val struct_child__sizeof_pos (a: Type0 { a == struct_child }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_child__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_child)})
 [@@pulse_eager_unfold] let predicate struct_child__pred ([@@@mkey] this: struct_child) (p: perm) =
   emp
 [@@pulse_eager_unfold] let predicate struct_child__uninit_pred ([@@@mkey] this: struct_child) = emp
diff --git base/core_ref_struct/Struct_parent.fst head/core_ref_struct/Struct_parent.fst
index e781ecb..2eb5b2d 100644
--- base/core_ref_struct/Struct_parent.fst
+++ head/core_ref_struct/Struct_parent.fst
@@ -11,6 +11,9 @@ assume val struct_parent__sizeof_pos (a: Type0 { a == struct_parent }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_parent__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_parent)})
 [@@erasable] noeq type struct_parent__spec = {
   struct_parent__spec__down_0: Struct_child.struct_child;
 }
diff --git base/core_ref_use/Struct_bar.fst head/core_ref_use/Struct_bar.fst
index 728d84f..320f7a0 100644
--- base/core_ref_use/Struct_bar.fst
+++ head/core_ref_use/Struct_bar.fst
@@ -11,6 +11,9 @@ assume val struct_bar__sizeof_pos (a: Type0 { a == struct_bar }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_bar__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 24 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_bar)})
 [@@erasable] noeq type struct_bar__spec = {
   struct_bar__spec__other_0: Int64.t;
   struct_bar__spec__myinner_0: Struct_inner.struct_inner__spec;
diff --git base/core_ref_use/Struct_inner.fst head/core_ref_use/Struct_inner.fst
index 1647587..e4a9d34 100644
--- base/core_ref_use/Struct_inner.fst
+++ head/core_ref_use/Struct_inner.fst
@@ -11,6 +11,9 @@ assume val struct_inner__sizeof_pos (a: Type0 { a == struct_inner }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_inner__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_inner)})
 [@@erasable] noeq type struct_inner__spec = {
   struct_inner__spec__a_0: Int32.t;
 }
diff --git base/core_ref_use_ptr/Struct_bar.fst head/core_ref_use_ptr/Struct_bar.fst
index 9caee14..b03b445 100644
--- base/core_ref_use_ptr/Struct_bar.fst
+++ head/core_ref_use_ptr/Struct_bar.fst
@@ -11,6 +11,9 @@ assume val struct_bar__sizeof_pos (a: Type0 { a == struct_bar }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_bar__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_bar)})
 [@@erasable] noeq type struct_bar__spec = {
   struct_bar__spec__other_0: Int64.t;
   struct_bar__spec__myinner_0: Struct_inner.struct_inner;
diff --git base/core_ref_use_ptr/Struct_inner.fst head/core_ref_use_ptr/Struct_inner.fst
index 1647587..e4a9d34 100644
--- base/core_ref_use_ptr/Struct_inner.fst
+++ head/core_ref_use_ptr/Struct_inner.fst
@@ -11,6 +11,9 @@ assume val struct_inner__sizeof_pos (a: Type0 { a == struct_inner }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_inner__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_inner)})
 [@@erasable] noeq type struct_inner__spec = {
   struct_inner__spec__a_0: Int32.t;
 }
diff --git base/default_test/Struct_point_anon_1.fst head/default_test/Struct_point_anon_1.fst
index e18dc94..6894a0b 100644
--- base/default_test/Struct_point_anon_1.fst
+++ head/default_test/Struct_point_anon_1.fst
@@ -11,6 +11,9 @@ assume val struct_point_anon_1__sizeof_pos (a: Type0 { a == struct_point_anon_1
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_point_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_point_anon_1)})
 [@@pulse_eager_unfold] let predicate struct_point_anon_1__pred
       ([@@@mkey] this: struct_point_anon_1)
       (p: perm) =
diff --git base/do_while/Struct_counter.fst head/do_while/Struct_counter.fst
index 33a0dc4..71611eb 100644
--- base/do_while/Struct_counter.fst
+++ head/do_while/Struct_counter.fst
@@ -10,6 +10,9 @@ assume val struct_counter__sizeof_pos (a: Type0 { a == struct_counter }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_counter__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 4 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_counter)})
 [@@pulse_eager_unfold] let predicate struct_counter__pred
       ([@@@mkey] this: struct_counter)
       (p: perm) =
diff --git base/dpe/Struct__engine_record_t.fst head/dpe/Struct__engine_record_t.fst
index 9391114..91d72cf 100644
--- base/dpe/Struct__engine_record_t.fst
+++ head/dpe/Struct__engine_record_t.fst
@@ -16,6 +16,10 @@ assume val struct__engine_record_t__sizeof_pos (a: Type0 { a == struct__engine_r
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct__engine_record_t__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 56 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct__engine_record_t)})
 [@@erasable] noeq type struct__engine_record_t__spec = {
   struct__engine_record_t__spec__l0_image_header_0: (full_array_spec Typedef_uint8_t.ty_uint8_t);
   struct__engine_record_t__spec__l0_image_header_sig_0:
diff --git base/dpe/Struct__profile_descriptor_t.fst head/dpe/Struct__profile_descriptor_t.fst
index b2e48a8..d624264 100644
--- base/dpe/Struct__profile_descriptor_t.fst
+++ head/dpe/Struct__profile_descriptor_t.fst
@@ -80,6 +80,10 @@ assume val struct__profile_descriptor_t__sizeof_pos
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct__profile_descriptor_t__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 312 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct__profile_descriptor_t)})
 [@@erasable] noeq type struct__profile_descriptor_t__spec = {
   struct__profile_descriptor_t__spec__name_0: Int8.t;
   struct__profile_descriptor_t__spec__session_protocol_0: Int8.t;
diff --git base/dpe/Struct_context_t_anon_1.fst head/dpe/Struct_context_t_anon_1.fst
index 4297766..9ddd1fc 100644
--- base/dpe/Struct_context_t_anon_1.fst
+++ head/dpe/Struct_context_t_anon_1.fst
@@ -11,6 +11,10 @@ assume val struct_context_t_anon_1__sizeof_pos (a: Type0 { a == struct_context_t
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_context_t_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 64 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_context_t_anon_1)})
 [@@pulse_eager_unfold] let predicate struct_context_t_anon_1__pred
       ([@@@mkey] this: struct_context_t_anon_1)
       (p: perm) =
diff --git base/dpe/Struct_l1_context_t_anon_1.fst head/dpe/Struct_l1_context_t_anon_1.fst
index 81d2308..c7ce2a4 100644
--- base/dpe/Struct_l1_context_t_anon_1.fst
+++ head/dpe/Struct_l1_context_t_anon_1.fst
@@ -16,6 +16,10 @@ assume val struct_l1_context_t_anon_1__sizeof_pos (a: Type0 { a == struct_l1_con
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_l1_context_t_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 56 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_l1_context_t_anon_1)})
 [@@erasable] noeq type struct_l1_context_t_anon_1__spec = {
   struct_l1_context_t_anon_1__spec__deviceid_pub_0: (full_array_spec Typedef_uint8_t.ty_uint8_t);
   struct_l1_context_t_anon_1__spec__aliaskey_priv_0: (full_array_spec Typedef_uint8_t.ty_uint8_t);
diff --git base/dpe/Union__u_context_t.fst head/dpe/Union__u_context_t.fst
index 4190041..5e68245 100644
--- base/dpe/Union__u_context_t.fst
+++ head/dpe/Union__u_context_t.fst
@@ -13,6 +13,9 @@ assume val union__u_context_t__sizeof_pos (a: Type0 { a == union__u_context_t })
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val union__u_context_t__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 56 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof union__u_context_t)})
 [@@pulse_eager_unfold] let predicate union__u_context_t__pred
       ([@@@mkey] this: union__u_context_t)
       (p: perm) =
diff --git base/eager_unfold_struct/Struct_point.fst head/eager_unfold_struct/Struct_point.fst
index 0ffcce9..6c32153 100644
--- base/eager_unfold_struct/Struct_point.fst
+++ head/eager_unfold_struct/Struct_point.fst
@@ -11,6 +11,9 @@ assume val struct_point__sizeof_pos (a: Type0 { a == struct_point }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_point__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_point)})
 [@@pulse_eager_unfold] let predicate struct_point__pred ([@@@mkey] this: struct_point) (p: perm) =
   emp
 [@@pulse_eager_unfold] let predicate struct_point__uninit_pred ([@@@mkey] this: struct_point) = emp
diff --git base/float_double/Struct_float_pair_anon_1.fst head/float_double/Struct_float_pair_anon_1.fst
index f1a36e9..1e66a55 100644
--- base/float_double/Struct_float_pair_anon_1.fst
+++ head/float_double/Struct_float_pair_anon_1.fst
@@ -11,6 +11,10 @@ assume val struct_float_pair_anon_1__sizeof_pos (a: Type0 { a == struct_float_pa
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_float_pair_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_float_pair_anon_1)})
 [@@pulse_eager_unfold] let predicate struct_float_pair_anon_1__pred
       ([@@@mkey] this: struct_float_pair_anon_1)
       (p: perm) =
diff --git base/fnptr_core_ref/Struct_callbacks.fst head/fnptr_core_ref/Struct_callbacks.fst
index 5445ee7..5c0f0e4 100644
--- base/fnptr_core_ref/Struct_callbacks.fst
+++ head/fnptr_core_ref/Struct_callbacks.fst
@@ -10,6 +10,9 @@ assume val struct_callbacks__sizeof_pos (a: Type0 { a == struct_callbacks }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_callbacks__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_callbacks)})
 [@@pulse_eager_unfold] let predicate struct_callbacks__pred
       ([@@@mkey] this: struct_callbacks)
       (p: perm) =
diff --git base/fnptr_core_ref/Struct_parent.fst head/fnptr_core_ref/Struct_parent.fst
index c304d1c..ac2f3d6 100644
--- base/fnptr_core_ref/Struct_parent.fst
+++ head/fnptr_core_ref/Struct_parent.fst
@@ -11,6 +11,9 @@ assume val struct_parent__sizeof_pos (a: Type0 { a == struct_parent }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_parent__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_parent)})
 [@@pulse_eager_unfold] let predicate struct_parent__pred ([@@@mkey] this: struct_parent) (p: perm) =
   ((Typedef_uint32_t.ty_uint32_t__pred this.struct_parent__value p) **
     (Struct_callbacks.struct_callbacks__pred this.struct_parent__callbacks p))
diff --git base/fnptr_core_ref/Struct_typedef_callbacks.fst head/fnptr_core_ref/Struct_typedef_callbacks.fst
index 4efb0d7..3a99be5 100644
--- base/fnptr_core_ref/Struct_typedef_callbacks.fst
+++ head/fnptr_core_ref/Struct_typedef_callbacks.fst
@@ -10,6 +10,10 @@ assume val struct_typedef_callbacks__sizeof_pos (a: Type0 { a == struct_typedef_
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_typedef_callbacks__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_typedef_callbacks)})
 [@@pulse_eager_unfold] let predicate struct_typedef_callbacks__pred
       ([@@@mkey] this: struct_typedef_callbacks)
       (p: perm) =
diff --git base/fnptr_core_ref/Struct_typedef_parent.fst head/fnptr_core_ref/Struct_typedef_parent.fst
index 757c41e..24bbfbf 100644
--- base/fnptr_core_ref/Struct_typedef_parent.fst
+++ head/fnptr_core_ref/Struct_typedef_parent.fst
@@ -11,6 +11,10 @@ assume val struct_typedef_parent__sizeof_pos (a: Type0 { a == struct_typedef_par
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_typedef_parent__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_typedef_parent)})
 [@@pulse_eager_unfold] let predicate struct_typedef_parent__pred
       ([@@@mkey] this: struct_typedef_parent)
       (p: perm) =
diff --git base/forward_struct/Struct_point.fst head/forward_struct/Struct_point.fst
index 0ffcce9..6c32153 100644
--- base/forward_struct/Struct_point.fst
+++ head/forward_struct/Struct_point.fst
@@ -11,6 +11,9 @@ assume val struct_point__sizeof_pos (a: Type0 { a == struct_point }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_point__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_point)})
 [@@pulse_eager_unfold] let predicate struct_point__pred ([@@@mkey] this: struct_point) (p: perm) =
   emp
 [@@pulse_eager_unfold] let predicate struct_point__uninit_pred ([@@@mkey] this: struct_point) = emp
diff --git base/func_pointer/Struct_itemx.fst head/func_pointer/Struct_itemx.fst
index 045e5c0..d65fe8c 100644
--- base/func_pointer/Struct_itemx.fst
+++ head/func_pointer/Struct_itemx.fst
@@ -11,6 +11,9 @@ assume val struct_itemx__sizeof_pos (a: Type0 { a == struct_itemx }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_itemx__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_itemx)})
 [@@pulse_eager_unfold] let predicate struct_itemx__pred ([@@@mkey] this: struct_itemx) (p: perm) =
   emp
 [@@pulse_eager_unfold] let predicate struct_itemx__uninit_pred ([@@@mkey] this: struct_itemx) = emp
diff --git base/func_pointer/Struct_mo_a.fst head/func_pointer/Struct_mo_a.fst
index 1a71ccd..90de7a9 100644
--- base/func_pointer/Struct_mo_a.fst
+++ head/func_pointer/Struct_mo_a.fst
@@ -10,6 +10,9 @@ assume val struct_mo_a__sizeof_pos (a: Type0 { a == struct_mo_a }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_mo_a__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 4 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_mo_a)})
 [@@pulse_eager_unfold] let predicate struct_mo_a__pred ([@@@mkey] this: struct_mo_a) (p: perm) =
   ((Typedef_int32_t.ty_int32_t__pred this.struct_mo_a__x p))
 [@@pulse_eager_unfold] let predicate struct_mo_a__uninit_pred ([@@@mkey] this: struct_mo_a) =
diff --git base/func_pointer/Struct_mo_b.fst head/func_pointer/Struct_mo_b.fst
index c4c398d..c0277b6 100644
--- base/func_pointer/Struct_mo_b.fst
+++ head/func_pointer/Struct_mo_b.fst
@@ -10,6 +10,9 @@ assume val struct_mo_b__sizeof_pos (a: Type0 { a == struct_mo_b }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_mo_b__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 4 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_mo_b)})
 [@@pulse_eager_unfold] let predicate struct_mo_b__pred ([@@@mkey] this: struct_mo_b) (p: perm) =
   ((Typedef_int32_t.ty_int32_t__pred this.struct_mo_b__y p))
 [@@pulse_eager_unfold] let predicate struct_mo_b__uninit_pred ([@@@mkey] this: struct_mo_b) =
diff --git base/func_pointer/Struct_mo_ops.fst head/func_pointer/Struct_mo_ops.fst
index e2a363b..f2fe94e 100644
--- base/func_pointer/Struct_mo_ops.fst
+++ head/func_pointer/Struct_mo_ops.fst
@@ -24,6 +24,9 @@ assume val struct_mo_ops__sizeof_pos (a: Type0 { a == struct_mo_ops }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_mo_ops__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 32 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_mo_ops)})
 [@@pulse_eager_unfold] let predicate struct_mo_ops__pred ([@@@mkey] this: struct_mo_ops) (p: perm) =
   emp
 [@@pulse_eager_unfold] let predicate struct_mo_ops__uninit_pred ([@@@mkey] this: struct_mo_ops) =
diff --git base/func_pointer/Struct_ops.fst head/func_pointer/Struct_ops.fst
index 61fce81..6e59750 100644
--- base/func_pointer/Struct_ops.fst
+++ head/func_pointer/Struct_ops.fst
@@ -13,6 +13,9 @@ assume val struct_ops__sizeof_pos (a: Type0 { a == struct_ops }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_ops__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_ops)})
 [@@pulse_eager_unfold] let predicate struct_ops__pred ([@@@mkey] this: struct_ops) (p: perm) = emp
 [@@pulse_eager_unfold] let predicate struct_ops__uninit_pred ([@@@mkey] this: struct_ops) = emp
 assume val struct_ops__aux_raw_unfolded ([@@@mkey] x: (ref struct_ops)) (p: perm) : slprop
diff --git base/func_pointer/Struct_ops_c.fst head/func_pointer/Struct_ops_c.fst
index 256e3b2..de182fa 100644
--- base/func_pointer/Struct_ops_c.fst
+++ head/func_pointer/Struct_ops_c.fst
@@ -13,6 +13,9 @@ assume val struct_ops_c__sizeof_pos (a: Type0 { a == struct_ops_c }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_ops_c__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_ops_c)})
 [@@pulse_eager_unfold] let predicate struct_ops_c__pred ([@@@mkey] this: struct_ops_c) (p: perm) =
   emp
 [@@pulse_eager_unfold] let predicate struct_ops_c__uninit_pred ([@@@mkey] this: struct_ops_c) = emp
diff --git base/func_pointer/Struct_vtable2.fst head/func_pointer/Struct_vtable2.fst
index 9be4500..6657d44 100644
--- base/func_pointer/Struct_vtable2.fst
+++ head/func_pointer/Struct_vtable2.fst
@@ -15,6 +15,9 @@ assume val struct_vtable2__sizeof_pos (a: Type0 { a == struct_vtable2 }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_vtable2__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_vtable2)})
 [@@pulse_eager_unfold] let predicate struct_vtable2__pred
       ([@@@mkey] this: struct_vtable2)
       (p: perm) =
diff --git base/func_pointer/Union_op_or_int.fst head/func_pointer/Union_op_or_int.fst
index 57b0bb7..c56905d 100644
--- base/func_pointer/Union_op_or_int.fst
+++ head/func_pointer/Union_op_or_int.fst
@@ -16,6 +16,9 @@ assume val union_op_or_int__sizeof_pos (a: Type0 { a == union_op_or_int }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val union_op_or_int__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof union_op_or_int)})
 [@@pulse_eager_unfold] let predicate union_op_or_int__pred
       ([@@@mkey] this: union_op_or_int)
       (p: perm) =
diff --git base/func_pointer2/Struct_ops_anon_1.fst head/func_pointer2/Struct_ops_anon_1.fst
index 5a1299b..b0f6e25 100644
--- base/func_pointer2/Struct_ops_anon_1.fst
+++ head/func_pointer2/Struct_ops_anon_1.fst
@@ -10,6 +10,9 @@ assume val struct_ops_anon_1__sizeof_pos (a: Type0 { a == struct_ops_anon_1 }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume
+val struct_ops_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_ops_anon_1)})
 [@@pulse_eager_unfold] let predicate struct_ops_anon_1__pred
       ([@@@mkey] this: struct_ops_anon_1)
       (p: perm) =
diff --git base/func_pointer2/Union_uops_anon_1.fst head/func_pointer2/Union_uops_anon_1.fst
index fdbbd29..df84240 100644
--- base/func_pointer2/Union_uops_anon_1.fst
+++ head/func_pointer2/Union_uops_anon_1.fst
@@ -12,6 +12,9 @@ assume val union_uops_anon_1__sizeof_pos (a: Type0 { a == union_uops_anon_1 }) :
     Lemma
     ((FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a)) > 0)
     [SMTPat (FStar.SizeT.v (Pulse.Lib.C.Sizeof.c_sizeof a))]
+assume

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@nikswamy @gebner