Give each record type the size its ABI assigns it

[nikswamy]

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

Base: main. Depends on nothing; reviewable on its own.

sizeof(T) committed to no particular value, so any arithmetic over sizes was unbounded.
Carries clang's ABI size on the record definition and emits it, in the record's own
module, as a refinement-typed constant that sizeof sites refer to. Introducing the size
once on the type is what keeps this sound — stating it at each site would let two sites
claim different sizes. A refinement-typed constant rather than an SMTPat lemma, because
a trigger for a ground fact contains no variable. Non-record types still size opaquely.

Commits

• Give each record type the size its ABI assigns it

Testing

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

[gebner]

!diff

[github-actions]

Generated F* output diff

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

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 +++
 {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}/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_sized_struct_anon_1.fst           |   4 ++++
 {base => head}/sizeof/Union_int_or_double_anon_1.fst                |   4 ++++
 {base => head}/sizeof/Union_zero_sized_union_anon_1.fst             |   4 ++++
 /dev/null => head/sizeof_abi/Func_SizesAreKnown.fst                 |  20 ++++++++++++++++++
 /dev/null => head/sizeof_abi/Func_SizesAreKnown.fsti                |   7 ++++++
 /dev/null => head/sizeof_abi/Struct__OUTER.fst                      | 144 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/sizeof_abi/Struct__PAIR.fst                       | 110 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 /dev/null => head/sizeof_abi/TranslationErrors.fst                  |   1 +
 /dev/null => head/sizeof_abi/Typedef_EITHER.fst                     |  12 +++++++++++
 /
... (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 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
+val union_uops_anon_1__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof union_uops_anon_1)})
 [@@pulse_eager_unfold] let predicate union_uops_anon_1__pred
       ([@@@mkey] this: union_uops_anon_1)
       (p: perm) =
diff --git base/generic_selection/Struct_generic_slots.fst head/generic_selection/Struct_generic_slots.fst
index 345a064..f0d92da 100644
--- base/generic_selection/Struct_generic_slots.fst
+++ head/generic_selection/Struct_generic_slots.fst
@@ -11,6 +11,10 @@ assume val struct_generic_slots__sizeof_pos (a: Type0 { a == struct_generic_slot
     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_generic_slots__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 16 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof
+    struct_generic_slots)})
 [@@pulse_eager_unfold] let predicate struct_generic_slots__pred
       ([@@@mkey] this: struct_generic_slots)
       (p: perm) =
diff --git base/global_header_addr/Struct_hs.fst head/global_header_addr/Struct_hs.fst
index 3e36d8e..e1da282 100644
--- base/global_header_addr/Struct_hs.fst
+++ head/global_header_addr/Struct_hs.fst
@@ -10,6 +10,9 @@ assume val struct_hs__sizeof_pos (a: Type0 { a == struct_hs }) :
     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_hs__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 4 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_hs)})
 [@@pulse_eager_unfold] let predicate struct_hs__pred ([@@@mkey] this: struct_hs) (p: perm) =
   ((Typedef_uint32_t.ty_uint32_t__pred this.struct_hs__x p))
 [@@pulse_eager_unfold] let predicate struct_hs__uninit_pred ([@@@mkey] this: struct_hs) =
diff --git base/global_header_addr/Struct_ms.fst head/global_header_addr/Struct_ms.fst
index 2538a69..e306ef3 100644
--- base/global_header_addr/Struct_ms.fst
+++ head/global_header_addr/Struct_ms.fst
@@ -10,6 +10,9 @@ assume val struct_ms__sizeof_pos (a: Type0 { a == struct_ms }) :
     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_ms__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 4 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_ms)})
 [@@pulse_eager_unfold] let predicate struct_ms__pred ([@@@mkey] this: struct_ms) (p: perm) =
   ((Typedef_uint32_t.ty_uint32_t__pred this.struct_ms__x p))
 [@@pulse_eager_unfold] let predicate struct_ms__uninit_pred ([@@@mkey] this: struct_ms) =
diff --git base/global_purity/Struct_point.fst head/global_purity/Struct_point.fst
index e14022f..0f41fb1 100644
--- base/global_purity/Struct_point.fst
+++ head/global_purity/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) =
   ((Typedef_int32_t.ty_int32_t__pred this.struct_point__x p) **
     (Typedef_int32_t.ty_int32_t__pred this.struct_point__y p))
diff --git base/inline_array_aliasing/Struct_mixed.fst head/inline_array_aliasing/Struct_mixed.fst
index ad357c9..55b554a 100644
--- base/inline_array_aliasing/Struct_mixed.fst
+++ head/inline_array_aliasing/Struct_mixed.fst
@@ -11,6 +11,9 @@ assume val struct_mixed__sizeof_pos (a: Type0 { a == struct_mixed }) :
     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_mixed__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 40 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_mixed)})
 [@@erasable] noeq type struct_mixed__spec = {
   struct_mixed__spec__p_0: (full_array_spec Int32.t);
 }
diff --git base/inner_struct/Struct_foo.fst head/inner_struct/Struct_foo.fst
index 3fcc8b7..cbdfca7 100644
--- base/inner_struct/Struct_foo.fst
+++ head/inner_struct/Struct_foo.fst
@@ -11,6 +11,9 @@ assume val struct_foo__sizeof_pos (a: Type0 { a == struct_foo }) :
     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_foo__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_foo)})
 [@@pulse_eager_unfold] let predicate struct_foo__pred ([@@@mkey] this: struct_foo) (p: perm) = emp
 [@@pulse_eager_unfold] let predicate struct_foo__uninit_pred ([@@@mkey] this: struct_foo) = emp
 assume val struct_foo__aux_raw_unfolded ([@@@mkey] x: (ref struct_foo)) (p: perm) : slprop
diff --git base/inner_struct/Struct_foo2.fst head/inner_struct/Struct_foo2.fst
index 1165bd3..adbb69a 100644
--- base/inner_struct/Struct_foo2.fst
+++ head/inner_struct/Struct_foo2.fst
@@ -10,6 +10,9 @@ assume val struct_foo2__sizeof_pos (a: Type0 { a == struct_foo2 }) :
     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_foo2__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 4 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_foo2)})
 [@@pulse_eager_unfold] let predicate struct_foo2__pred ([@@@mkey] this: struct_foo2) (p: perm) = emp
 [@@pulse_eager_unfold] let predicate struct_foo2__uninit_pred ([@@@mkey] this: struct_foo2) = emp
 assume val struct_foo2__aux_raw_unfolded ([@@@mkey] x: (ref struct_foo2)) (p: perm) : slprop
diff --git base/inner_struct/Struct_xy.fst head/inner_struct/Struct_xy.fst
index b6ee880..a1e733a 100644
--- base/inner_struct/Struct_xy.fst
+++ head/inner_struct/Struct_xy.fst
@@ -11,6 +11,9 @@ assume val struct_xy__sizeof_pos (a: Type0 { a == struct_xy }) :
     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_xy__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 8 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_xy)})
 [@@pulse_eager_unfold] let predicate struct_xy__pred ([@@@mkey] this: struct_xy) (p: perm) = emp
 [@@pulse_eager_unfold] let predicate struct_xy__uninit_pred ([@@@mkey] this: struct_xy) = emp
 assume val struct_xy__aux_raw_unfolded ([@@@mkey] x: (ref struct_xy)) (p: perm) : slprop
diff --git base/issue28/Struct__point.fst head/issue28/Struct__point.fst
index cb9953b..176b3e1 100644
--- base/issue28/Struct__point.fst
+++ head/issue28/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) =
diff --git base/malloc/Struct_point_anon_1.fst head/malloc/Struct_point_anon_1.fst
index e18dc94..6894a0b 100644
--- base/malloc/Struct_point_anon_1.fst
+++ head/malloc/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/memset/Struct_triple.fst head/memset/Struct_triple.fst
index 63dbd91..8e7d19f 100644
--- base/memset/Struct_triple.fst
+++ head/memset/Struct_triple.fst
@@ -12,6 +12,9 @@ assume val struct_triple__sizeof_pos (a: Type0 { a == struct_triple }) :
     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_triple__c_sizeof
+: (n: FStar.SizeT.t{FStar.SizeT.v n == 12 /\ n == (Pulse.Lib.C.Sizeof.c_sizeof struct_triple)})
 [@@pulse_eager_unfold] let predicate struct_triple__pred ([@@@mkey] this: struct_triple) (p: perm) =
   emp

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