Native support for bit fields (#400)

This big PR adds support for bit fields in structs and unions to
the verified part of CompCert, namely the CompCert C and Clight
languages.

The compilation of bit field accesses to normal integer accesses +
shifts and masks is done and proved correct as part of the Cshmgen
pass.

The layout of bit fields in memory is done by the functions in module
Ctypes. It follows the ELF ABI layout algorithm. As a bonus, basic
soundness properties of the layout are shown, such as "two different
bit fields do not overlap" or "a bit field and a regular field do not
overlap".

All this replaces the previous emulation of bit fields by
source-to-source rewriting in the unverified front-end of CompCert
(module cparse/Bitfield.ml). This emulation was prone to errors (see
nonstandard layout instead.

The core idea for the PR is that expressions in l-value position
denote not just a block, a byte offset and a type, but also a bitfield
designator saying whether all the bits of the type are accessed
(designator Full) or only some of its bits (designator
Bits). Designators of the Bits kind appear when the l-value is a bit
field access; the bit width and bit offset in Bits are computed by the
functions in Ctypes that implement the layout algorithm.

Consequently, both in the semantics of CompCert C and Clight and in
the SimplExpr, SimplLocals and Cshmgen compilation passes, pairs of a
type and a bitfield designator are used in a number of places where a
single type was used before.

The introduction of bit fields has a big impact on static
initialization (module cfrontend/Initializers.v), which had to be
rewritten in large part, along with its soundness proof
(cfrontend/Initializersproof.v).

Both static initialization and run-time manipulation of bit fields are
tested in test/abi using differential testing against GCC and
randomly-generated structs.

This work exposed subtle interactions between bit fields and the
volatile modifier. Currently, the volatile modifier is ignored when
accessing a bit field (and a warning is printed at compile-time), just
like it is ignored when accessing a struct or union as a r-value.

Currently, the natural alignment of bit fields and their storage units
cannot be modified with the aligned attribute. _Alignas on bit fields
is rejected as per C11, and the packed modifier cannot be applied to a
struct containing bit fields.

1 files changed, 826 insertions, 371 deletions

diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 10ccbeff..00f7e331 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -12,7 +12,7 @@
 
 (** Compile-time evaluation of initializers for global C variables. *)
 
-Require Import Coqlib Maps.
+Require Import Zwf Coqlib Maps.
 Require Import Errors Integers Floats Values AST Memory Globalenvs Events Smallstep.
 Require Import Ctypes Cop Csyntax Csem.
 Require Import Initializers.
@@ -30,7 +30,7 @@ Variable ge: genv.
 
 Fixpoint simple (a: expr) : Prop :=
   match a with
-  | Eloc _ _ _ => True
+  | Eloc _ _ _ _ => True
   | Evar _ _ => True
   | Ederef r _ => simple r
   | Efield l1 _ _ => simple l1
@@ -65,38 +65,38 @@ Section SIMPLE_EXPRS.
 Variable e: env.
 Variable m: mem.
 
-Inductive eval_simple_lvalue: expr -> block -> ptrofs -> Prop :=
-  | esl_loc: forall b ofs ty,
-      eval_simple_lvalue (Eloc b ofs ty) b ofs
+Inductive eval_simple_lvalue: expr -> block -> ptrofs -> bitfield -> Prop :=
+  | esl_loc: forall b ofs bf ty,
+      eval_simple_lvalue (Eloc b ofs bf ty) b ofs bf
   | esl_var_local: forall x ty b,
       e!x = Some(b, ty) ->
-      eval_simple_lvalue (Evar x ty) b Ptrofs.zero
+      eval_simple_lvalue (Evar x ty) b Ptrofs.zero Full
   | esl_var_global: forall x ty b,
       e!x = None ->
       Genv.find_symbol ge x = Some b ->
-      eval_simple_lvalue (Evar x ty) b Ptrofs.zero
+      eval_simple_lvalue (Evar x ty) b Ptrofs.zero Full
   | esl_deref: forall r ty b ofs,
       eval_simple_rvalue r (Vptr b ofs) ->
-      eval_simple_lvalue (Ederef r ty) b ofs
-  | esl_field_struct: forall r f ty b ofs id co a delta,
+      eval_simple_lvalue (Ederef r ty) b ofs Full
+  | esl_field_struct: forall r f ty b ofs id co a delta bf,
       eval_simple_rvalue r (Vptr b ofs) ->
-      typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta ->
-      eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta))
-  | esl_field_union: forall r f ty b ofs id a,
+      typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK (delta, bf) ->
+      eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta)) bf
+  | esl_field_union: forall r f ty b ofs id co a delta bf,
       eval_simple_rvalue r (Vptr b ofs) ->
-      typeof r = Tunion id a ->
-      eval_simple_lvalue (Efield r f ty) b ofs
+      typeof r = Tunion id a -> ge.(genv_cenv)!id = Some co -> union_field_offset ge f (co_members co) = OK (delta, bf) ->
+      eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta)) bf
 
 with eval_simple_rvalue: expr -> val -> Prop :=
   | esr_val: forall v ty,
       eval_simple_rvalue (Eval v ty) v
-  | esr_rvalof: forall b ofs l ty v,
-      eval_simple_lvalue l b ofs ->
+  | esr_rvalof: forall b ofs bf l ty v,
+      eval_simple_lvalue l b ofs bf ->
       ty = typeof l ->
-      deref_loc ge ty m b ofs E0 v ->
+      deref_loc ge ty m b ofs bf E0 v ->
       eval_simple_rvalue (Evalof l ty) v
   | esr_addrof: forall b ofs l ty,
-      eval_simple_lvalue l b ofs ->
+      eval_simple_lvalue l b ofs Full ->
       eval_simple_rvalue (Eaddrof l ty) (Vptr b ofs)
   | esr_unop: forall op r1 ty v1 v,
       eval_simple_rvalue r1 v1 ->
@@ -153,7 +153,7 @@ End SIMPLE_EXPRS.
 Definition compat_eval (k: kind) (e: env) (a a': expr) (m: mem) : Prop :=
   typeof a = typeof a' /\
   match k with
-  | LV => forall b ofs, eval_simple_lvalue e m a' b ofs -> eval_simple_lvalue e m a b ofs
+  | LV => forall b ofs bf, eval_simple_lvalue e m a' b ofs bf -> eval_simple_lvalue e m a b ofs bf
   | RV => forall v, eval_simple_rvalue e m a' v -> eval_simple_rvalue e m a v
   end.
 
@@ -167,7 +167,7 @@ Lemma lred_compat:
   forall e l m l' m', lred ge e l m l' m' ->
   m = m' /\ compat_eval LV e l l' m.
 Proof.
-  induction 1; simpl; split; auto; split; auto; intros bx ofsx EV; inv EV.
+  induction 1; simpl; split; auto; split; auto; intros bx ofsx bf' EV; inv EV.
   apply esl_var_local; auto.
   apply esl_var_global; auto.
   constructor. constructor.
@@ -365,6 +365,22 @@ Proof.
   intros. eapply bool_val_inj; eauto. intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate.
 Qed.
 
+Lemma add_offset_match:
+  forall v b ofs delta,
+  Val.inject inj v (Vptr b ofs) ->
+  Val.inject inj
+    (if Archi.ptr64
+     then Val.addl v (Vlong (Int64.repr delta))
+     else Val.add v (Vint (Int.repr delta)))
+    (Vptr b (Ptrofs.add ofs (Ptrofs.repr delta))).
+Proof.
+  intros. inv H.
+- rewrite Ptrofs.add_assoc. rewrite (Ptrofs.add_commut (Ptrofs.repr delta0)).
+  unfold Val.addl, Val.add; destruct Archi.ptr64 eqn:SF;
+  econstructor; eauto; rewrite ! Ptrofs.add_assoc; f_equal; f_equal; symmetry; auto with ptrofs.
+- unfold Val.addl, Val.add; destruct Archi.ptr64; auto.
+Qed.
+
 (** Soundness of [constval] with respect to the big-step semantics *)
 
 Lemma constval_rvalue:
@@ -374,20 +390,22 @@ Lemma constval_rvalue:
   constval ge a = OK v' ->
   Val.inject inj v' v
 with constval_lvalue:
-  forall m a b ofs,
-  eval_simple_lvalue empty_env m a b ofs ->
+  forall m a b ofs bf,
+  eval_simple_lvalue empty_env m a b ofs bf ->
   forall v',
   constval ge a = OK v' ->
-  Val.inject inj v' (Vptr b ofs).
+  bf = Full /\ Val.inject inj v' (Vptr b ofs).
 Proof.
   (* rvalue *)
   induction 1; intros vres CV; simpl in CV; try (monadInv CV).
   (* val *)
   destruct v; monadInv CV; constructor.
   (* rval *)
-  inv H1; rewrite H2 in CV; try congruence. eauto. eauto.
+  assert (constval ge l = OK vres) by (destruct (access_mode ty); congruence).
+  exploit constval_lvalue; eauto. intros [A B]. subst bf.
+  inv H1; rewrite H3 in CV; congruence.
   (* addrof *)
-  eauto.
+  eapply constval_lvalue; eauto.
   (* unop *)
   destruct (sem_unary_operation op x (typeof r1) Mem.empty) as [v1'|] eqn:E; inv EQ0.
   exploit (sem_unary_operation_inj inj Mem.empty m).
@@ -438,28 +456,31 @@ Proof.
   (* lvalue *)
   induction 1; intros v' CV; simpl in CV; try (monadInv CV).
   (* var local *)
-  unfold empty_env in H. rewrite PTree.gempty in H. congruence.
+  split; auto. unfold empty_env in H. rewrite PTree.gempty in H. congruence.
   (* var_global *)
-  econstructor. unfold inj. rewrite H0. eauto. auto.
+  split; auto. econstructor. unfold inj. rewrite H0. eauto. auto.
   (* deref *)
-  eauto.
+  split; eauto.
   (* field struct *)
-  rewrite H0 in CV. monadInv CV. unfold lookup_composite in EQ; rewrite H1 in EQ; monadInv EQ.
-  exploit constval_rvalue; eauto. intro MV. inv MV.
-  replace x0 with delta by congruence. rewrite Ptrofs.add_assoc. rewrite (Ptrofs.add_commut (Ptrofs.repr delta0)).
-  simpl; destruct Archi.ptr64 eqn:SF;
-  econstructor; eauto; rewrite ! Ptrofs.add_assoc; f_equal; f_equal; symmetry; auto with ptrofs.
-  destruct Archi.ptr64; auto.
+  rewrite H0 in EQ. monadInv EQ. destruct x0; monadInv EQ2.
+  unfold lookup_composite in EQ0; rewrite H1 in EQ0; monadInv EQ0.
+  exploit constval_rvalue; eauto. intro MV.
+  split. congruence.
+  replace x with delta by congruence.
+  apply (add_offset_match _ _ _ _ MV).
   (* field union *)
-  rewrite H0 in CV. eauto.
+  rewrite H0 in EQ. monadInv EQ. destruct x0; monadInv EQ2.
+  unfold lookup_composite in EQ0; rewrite H1 in EQ0; monadInv EQ0.
+  exploit constval_rvalue; eauto. intro MV.
+  split. congruence.
+  replace x with delta by congruence. 
+  apply (add_offset_match _ _ _ _ MV).
 Qed.
 
 Lemma constval_simple:
   forall a v, constval ge a = OK v -> simple a.
 Proof.
   induction a; simpl; intros vx CV; try (monadInv CV); eauto.
-  destruct (typeof a); discriminate || eauto.
-  monadInv CV. eauto.
   destruct (access_mode ty); discriminate || eauto.
   intuition eauto.
 Qed.
@@ -476,331 +497,757 @@ Proof.
   intros [A [B C]]. intuition. eapply constval_rvalue; eauto.
 Qed.
 
-(** * Relational specification of the translation of initializers *)
-
-Definition tr_padding (frm to: Z) : list init_data :=
-  if zlt frm to then Init_space (to - frm) :: nil else nil.
-
-Inductive tr_init: type -> initializer -> list init_data -> Prop :=
-  | tr_init_sgl: forall ty a d,
-      transl_init_single ge ty a = OK d ->
-      tr_init ty (Init_single a) (d :: nil)
-  | tr_init_arr: forall tyelt nelt attr il d,
-      tr_init_array tyelt il (Z.max 0 nelt) d ->
-      tr_init (Tarray tyelt nelt attr) (Init_array il) d
-  | tr_init_str: forall id attr il co d,
-      lookup_composite ge id = OK co -> co_su co = Struct ->
-      tr_init_struct (Tstruct id attr) (co_members co) il 0 d ->
-      tr_init (Tstruct id attr) (Init_struct il) d
-  | tr_init_uni: forall id attr f i1 co ty1 d,
-      lookup_composite ge id = OK co -> co_su co = Union -> field_type f (co_members co) = OK ty1 ->
-      tr_init ty1 i1 d ->
-      tr_init (Tunion id attr) (Init_union f i1)
-              (d ++ tr_padding (sizeof ge ty1) (sizeof ge (Tunion id attr)))
-
-with tr_init_array: type -> initializer_list -> Z -> list init_data -> Prop :=
-  | tr_init_array_nil_0: forall ty,
-      tr_init_array ty Init_nil 0 nil
-  | tr_init_array_nil_pos: forall ty sz,
-      0 < sz ->
-      tr_init_array ty Init_nil sz (Init_space (sz * sizeof ge ty) :: nil)
-  | tr_init_array_cons: forall ty i il sz d1 d2,
-      tr_init ty i d1 -> tr_init_array ty il (sz - 1) d2 ->
-      tr_init_array ty (Init_cons i il) sz (d1 ++ d2)
-
-with tr_init_struct: type -> members -> initializer_list -> Z -> list init_data -> Prop :=
-  | tr_init_struct_nil: forall ty pos,
-      tr_init_struct ty nil Init_nil pos (tr_padding pos (sizeof ge ty))
-  | tr_init_struct_cons: forall ty f1 ty1 fl i1 il pos d1 d2,
-      let pos1 := align pos (alignof ge ty1) in
-      tr_init ty1 i1 d1 ->
-      tr_init_struct ty fl il (pos1 + sizeof ge ty1) d2 ->
-      tr_init_struct ty ((f1, ty1) :: fl) (Init_cons i1 il)
-                     pos (tr_padding pos pos1 ++ d1 ++ d2).
-
-Lemma transl_padding_spec:
-  forall frm to k, padding frm to k = rev (tr_padding frm to) ++ k.
-Proof.
-  unfold padding, tr_padding; intros. 
-  destruct (zlt frm to); auto.
-Qed.
-
-Lemma transl_init_rec_spec:
-  forall i ty k res,
-  transl_init_rec ge ty i k = OK res ->
-  exists d, tr_init ty i d /\ res = rev d ++ k
-
-with transl_init_array_spec:
-  forall il ty sz k res,
-  transl_init_array ge ty il sz k = OK res ->
-  exists d, tr_init_array ty il sz d /\ res = rev d ++ k
-
-with transl_init_struct_spec:
-  forall il ty fl pos k res,
-  transl_init_struct ge ty fl il pos k = OK res ->
-  exists d, tr_init_struct ty fl il pos d /\ res = rev d ++ k.
-
-Proof.
-Local Opaque sizeof.
-- destruct i; intros until res; intros TR; simpl in TR.
-+ monadInv TR. exists (x :: nil); split; auto. constructor; auto.
-+ destruct ty; try discriminate.
-  destruct (transl_init_array_spec _ _ _ _ _ TR) as (d & A & B).
-  exists d; split; auto. constructor; auto.
-+ destruct ty; try discriminate. monadInv TR. destruct (co_su x) eqn:SU; try discriminate.
-  destruct (transl_init_struct_spec _ _ _ _ _ _ EQ0) as (d & A & B).
-  exists d; split; auto. econstructor; eauto.
-+ destruct ty; try discriminate.
-  monadInv TR. destruct (co_su x) eqn:SU; monadInv EQ0.
-  destruct (transl_init_rec_spec _ _ _ _ EQ0) as (d & A & B).
-  exists (d ++ tr_padding (sizeof ge x0) (sizeof ge (Tunion i0 a))); split.
-  econstructor; eauto.
-  rewrite rev_app_distr, app_ass, B. apply transl_padding_spec. 
-
-- destruct il; intros until res; intros TR; simpl in TR.
-+ destruct (zeq sz 0). 
-  inv TR. exists (@nil init_data); split; auto. constructor.
-  destruct (zle 0 sz).
-  inv TR. econstructor; split. constructor. lia. auto.
-  discriminate.
-+ monadInv TR. 
-  destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1).
-  destruct (transl_init_array_spec _ _ _ _ _ EQ0) as (d2 & A2 & B2).
-  exists (d1 ++ d2); split. econstructor; eauto. 
-  subst res x. rewrite rev_app_distr, app_ass. auto.
+(** * Correctness of operations over the initialization state *)
+
+(** ** Properties of the in-memory bytes denoted by initialization data *)
+
+Local Notation boid := (Genv.bytes_of_init_data (genv_genv ge)).
+Local Notation boidl := (Genv.bytes_of_init_data_list (genv_genv ge)).
+
+Lemma boidl_app: forall il2 il1,
+  boidl (il1 ++ il2) = boidl il1 ++ boidl il2.
+Proof.
+  induction il1 as [ | il il1]; simpl. auto. rewrite app_ass. f_equal; auto.
+Qed.
+
+Corollary boidl_rev_cons: forall i il,
+  boidl (rev il ++ i :: nil) = boidl (rev il) ++ boid i.
+Proof.
+  intros. rewrite boidl_app. simpl. rewrite <- app_nil_end. auto.
+Qed. 
+
+Definition byte_of_int (n: int) := Byte.repr (Int.unsigned n).
+
+Lemma byte_of_int_of_byte: forall b, byte_of_int (int_of_byte b) = b.
+Proof.
+  intros. unfold int_of_byte, byte_of_int.
+  rewrite Int.unsigned_repr, Byte.repr_unsigned. auto.
+  assert(Byte.max_unsigned < Int.max_unsigned) by reflexivity.
+  generalize (Byte.unsigned_range_2 b). lia.
+Qed.
+
+Lemma inj_bytes_1: forall n,
+  inj_bytes (encode_int 1 n) = Byte (Byte.repr n) :: nil.
+Proof.
+  intros. unfold encode_int, bytes_of_int, rev_if_be. destruct Archi.big_endian; auto.
+Qed.
+
+Lemma inj_bytes_byte: forall b,
+  inj_bytes (encode_int 1 (Int.unsigned (int_of_byte b))) = Byte b :: nil.
+Proof.
+  intros. rewrite inj_bytes_1. do 2 f_equal. apply byte_of_int_of_byte.
+Qed.
+
+Lemma boidl_init_ints8: forall l,
+  boidl (map Init_int8 l) = inj_bytes (map byte_of_int l).
+Proof.
+  induction l as [ | i l]; simpl. auto. rewrite inj_bytes_1; simpl. f_equal; auto.
+Qed.
+
+Lemma boidl_init_bytes: forall l,
+  boidl (map Init_byte l) = inj_bytes l.
+Proof.
+  induction l as [ | b l]; simpl. auto. rewrite inj_bytes_byte, IHl. auto.
+Qed.
+
+Lemma boidl_ints8: forall i n,
+  boidl (repeat (Init_int8 i) n) = repeat (Byte (byte_of_int i)) n.
+Proof.
+  induction n; simpl. auto. rewrite inj_bytes_1. simpl; f_equal; auto.
+Qed.
+
+(** ** Properties of operations over list of initialization data *)
+
+Lemma add_rev_bytes_spec: forall l il,
+  add_rev_bytes l il = List.map Init_byte (List.rev l) ++ il.
+Proof.
+  induction l as [ | b l]; intros; simpl.
+- auto.
+- rewrite IHl. rewrite map_app. simpl. rewrite app_ass. auto.
+Qed.
+
+Lemma add_rev_bytes_spec': forall l il,
+  List.rev (add_rev_bytes l il) = List.rev il ++ List.map Init_byte l.
+Proof.
+  intros. rewrite add_rev_bytes_spec. rewrite rev_app_distr, map_rev, rev_involutive. auto.
+Qed.
+
+Lemma add_zeros_spec: forall n il,
+  0 <= n ->
+  add_zeros n il = List.repeat (Init_int8 Int.zero) (Z.to_nat n) ++ il.
+Proof.
+  intros.
+  unfold add_zeros; rewrite iter_nat_of_Z by auto; rewrite Zabs2Nat.abs_nat_nonneg by auto.
+  induction (Z.to_nat n); simpl. auto. f_equal; auto.
+Qed.
+
+Lemma decompose_spec: forall il depth bl il',
+  decompose il depth = OK (bl, il') ->
+  exists nl, il = List.map Init_int8 nl ++ il'
+          /\ bl = List.map byte_of_int (rev nl)
+          /\ List.length nl = Z.to_nat depth.
+Proof.
+  assert (REC: forall il accu depth bl il',
+               decompose_rec accu il depth = OK (bl, il') ->
+               exists nl, il = List.map Init_int8 nl ++ il'
+                       /\ bl = List.map byte_of_int (rev nl) ++ accu
+                       /\ List.length nl = Z.to_nat depth).
+  { induction il as [ | i il ]; intros until il'; intros D; simpl in D.
+  - destruct (zle depth 0); inv D.
+    exists (@nil int); simpl. rewrite Z_to_nat_neg by auto. auto.
+  - destruct (zle depth 0). 
+    + inv D. exists (@nil int); simpl. rewrite Z_to_nat_neg by auto. auto.
+    + destruct i; try discriminate.
+      apply IHil in D; destruct D as (nl & P & Q & R).
+      exists (i :: nl); simpl; split. congruence. split.
+      rewrite map_app. simpl. rewrite app_ass. exact Q.
+      rewrite R, <- Z2Nat.inj_succ by lia. f_equal; lia.
+  }
+  intros. apply REC in H. destruct H as (nl & P & Q & R). rewrite app_nil_r in Q.
+  exists nl; auto.
+Qed.
+
+Lemma list_repeat_app: forall (A: Type) (a: A) n2 n1,
+  List.repeat a n1 ++ List.repeat a n2 = List.repeat a (n1 + n2)%nat.
+Proof.
+  induction n1; simpl; congruence.
+Qed.
+
+Lemma list_rev_repeat: forall (A: Type) (a: A) n,
+  rev (List.repeat a n) = List.repeat a n.
+Proof.
+  induction n; simpl. auto. rewrite IHn. change (a :: nil) with (repeat a 1%nat).
+  rewrite list_repeat_app. rewrite Nat.add_comm. auto. 
+Qed.
+
+Lemma normalize_boidl: forall il depth il',
+  normalize il depth = OK il' ->
+  boidl (rev il') = boidl (rev il).
+Proof.
+  induction il as [ | i il]; simpl; intros depth il' AT.
+- destruct (zle depth 0); inv AT. auto.
+- destruct (zle depth 0). inv AT. auto.
+  destruct i;
+  try (monadInv AT; simpl;
+       rewrite ? add_rev_bytes_spec', ? boidl_rev_cons, ? boidl_app, ? boidl_init_bytes;
+       erewrite IHil by eauto; reflexivity).
+  set (n := Z.max 0 z) in *. destruct (zle n depth); monadInv AT.
+  + rewrite add_zeros_spec, rev_app_distr, ! boidl_app by lia.
+    erewrite IHil by eauto. f_equal.
+    rewrite list_rev_repeat. simpl. rewrite app_nil_r, boidl_ints8.
+    f_equal. unfold n. apply Z.max_case_strong; intros; auto. rewrite ! Z_to_nat_neg by lia. auto.
+  + rewrite add_zeros_spec, rev_app_distr, !boidl_app by lia.
+    simpl. rewrite boidl_rev_cons, list_rev_repeat. simpl.
+    rewrite app_ass, app_nil_r, !boidl_ints8. f_equal.
+    rewrite list_repeat_app. f_equal. rewrite <- Z2Nat.inj_add by lia.
+    unfold n. apply Z.max_case_strong; intros; f_equal; lia.
+Qed.
+
+Lemma trisection_boidl: forall il depth sz bytes1 bytes2 il',
+  trisection il depth sz = OK (bytes1, bytes2, il') ->
+  boidl (rev il) = boidl (rev il') ++ inj_bytes bytes2 ++ inj_bytes bytes1
+  /\ length bytes1 = Z.to_nat depth
+  /\ length bytes2 = Z.to_nat sz.
+Proof.
+  unfold trisection; intros. monadInv H.
+  apply normalize_boidl in EQ. rewrite <- EQ.
+  apply decompose_spec in EQ1. destruct EQ1 as (nl1 & A1 & B1 & C1).
+  apply decompose_spec in EQ0. destruct EQ0 as (nl2 & A2 & B2 & C2).
+  split.
+- rewrite A1, A2, !rev_app_distr, !boidl_app, app_ass.
+  rewrite <- !map_rev, !boidl_init_ints8. rewrite <- B1, <- B2. auto.
+- rewrite B1, B2, !map_length, !rev_length. auto.
+Qed. 
+
+Lemma store_init_data_loadbytes:
+  forall m b p i m',
+  Genv.store_init_data ge m b p i = Some m' ->
+  match i with Init_space _ => False | _ => True end ->
+  Mem.loadbytes m' b p (init_data_size i) = Some (boid i).
+Proof.
+  intros; destruct i; simpl in H; try apply (Mem.loadbytes_store_same _ _ _ _ _ _ H).
+- contradiction.
+- rewrite Genv.init_data_size_addrof. simpl.
+  destruct (Genv.find_symbol ge i) as [b'|]; try discriminate.
+  rewrite (Mem.loadbytes_store_same _ _ _ _ _ _ H).
+  unfold encode_val, Mptr; destruct Archi.ptr64; reflexivity.
+Qed.
+
+(** ** Validity and size of initialization data *)
+
+Definition idvalid (i: init_data) : Prop :=
+  match i with
+  | Init_addrof symb ofs => exists b, Genv.find_symbol ge symb = Some b
+  | _ => True
+  end.
+
+Fixpoint idlvalid (p: Z) (il: list init_data) {struct il} : Prop :=
+  match il with
+  | nil => True
+  | i1 :: il =>
+        (Genv.init_data_alignment i1 | p)
+     /\ idvalid i1
+     /\ idlvalid (p + init_data_size i1) il
+  end.
+
+Lemma idlvalid_app: forall l2 l1 pos,
+  idlvalid pos (l1 ++ l2) <-> idlvalid pos l1 /\ idlvalid (pos + init_data_list_size l1) l2.
+Proof.
+  induction l1 as [ | d l1]; intros; simpl.
+- rewrite Z.add_0_r; tauto.
+- rewrite IHl1. rewrite Z.add_assoc. tauto.
+Qed.
+
+Lemma add_rev_bytes_valid: forall il bl,
+  idlvalid 0 (rev il) -> idlvalid 0 (rev (add_rev_bytes bl il)).
+Proof.
+  intros. rewrite add_rev_bytes_spec, rev_app_distr, idlvalid_app. split; auto.
+  generalize (rev bl) (0 + init_data_list_size (rev il)). induction l; simpl; intros.
+  auto.
+  rewrite idlvalid_app; split; auto. simpl. auto using Z.divide_1_l.
+Qed.
+
+Lemma add_zeros_valid: forall il n,
+  0 <= n -> idlvalid 0 (rev il) -> idlvalid 0 (rev (add_zeros n il)).
+Proof.
+  intros. rewrite add_zeros_spec, rev_app_distr, idlvalid_app by auto.
+  split; auto.
+  generalize (Z.to_nat n) (0 + init_data_list_size (rev il)). induction n0; simpl; intros.
+  auto.
+  rewrite idlvalid_app; split; auto. simpl. auto using Z.divide_1_l.
+Qed.
 
-- destruct il; intros until res; intros TR; simpl in TR.
-+ destruct fl; inv TR. econstructor; split. constructor. apply transl_padding_spec.
-+ destruct fl as [ | [f1 ty1] fl ]; monadInv TR.
-  destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1).
-  destruct (transl_init_struct_spec _ _ _ _ _ _ EQ0) as (d2 & A2 & B2).
-  exists (tr_padding pos (align pos (alignof ge ty1)) ++ d1 ++ d2); split.
-  econstructor; eauto.
-  rewrite ! rev_app_distr. subst res x. rewrite ! app_ass. rewrite transl_padding_spec. auto.
+Lemma normalize_valid: forall il depth il',
+  normalize il depth = OK il' -> idlvalid 0 (rev il) -> idlvalid 0 (rev il').
+Proof.
+  induction il as [ | i il]; simpl; intros.
+- destruct (zle depth 0); inv H. simpl. tauto.
+- destruct (zle depth 0). inv H. auto.
+  rewrite idlvalid_app in H0; destruct H0.
+  destruct i; try (monadInv H; apply add_rev_bytes_valid; eapply IHil; eauto).
+  + monadInv H. simpl. rewrite idlvalid_app; split. eauto. simpl; auto using Z.divide_1_l. 
+  + destruct (zle (Z.max 0 z)); monadInv H.
+    * apply add_zeros_valid. lia. eauto.
+    * apply add_zeros_valid. lia. simpl. rewrite idlvalid_app; split. auto. simpl; auto using Z.divide_1_l.
 Qed.
 
-Theorem transl_init_spec:
-  forall ty i d, transl_init ge ty i = OK d -> tr_init ty i d.
+Lemma trisection_valid: forall il depth sz bytes1 bytes2 il',
+  trisection il depth sz = OK (bytes1, bytes2, il') ->
+  idlvalid 0 (rev il) ->
+  idlvalid 0 (rev il').
 Proof.
-  unfold transl_init; intros. monadInv H. 
-  exploit transl_init_rec_spec; eauto. intros (d & A & B). 
-  subst x. unfold rev'; rewrite <- rev_alt. 
-  rewrite rev_app_distr; simpl. rewrite rev_involutive. auto.
+  unfold trisection; intros. monadInv H.
+  apply decompose_spec in EQ1. destruct EQ1 as (nl1 & A1 & B1 & C1).
+  apply decompose_spec in EQ0. destruct EQ0 as (nl2 & A2 & B2 & C2).
+  exploit normalize_valid; eauto. rewrite A1, A2, !rev_app_distr, !idlvalid_app.
+  tauto.
+Qed.
+
+Lemma init_data_size_boid: forall i,
+  init_data_size i = Z.of_nat (length (boid i)).
+Proof.
+  intros. destruct i; simpl; rewrite ?length_inj_bytes, ?encode_int_length; auto.
+- rewrite repeat_length. rewrite Z_to_nat_max; auto.
+- destruct (Genv.find_symbol ge i), Archi.ptr64; reflexivity.
+Qed.
+
+Lemma init_data_list_size_boidl: forall il,
+  init_data_list_size il = Z.of_nat (length (boidl il)).
+Proof.
+  induction il as [ | i il]; simpl. auto. 
+  rewrite app_length, init_data_size_boid. lia.
+Qed.
+
+Lemma init_data_list_size_app: forall l1 l2,
+  init_data_list_size (l1 ++ l2) = init_data_list_size l1 + init_data_list_size l2.
+Proof.
+  induction l1 as [ | i l1]; intros; simpl. auto. rewrite IHl1; lia.
+Qed.
+
+(** ** Memory areas that are initialized to zeros *)
+
+Definition reads_as_zeros (m: mem) (b: block) (from to: Z) : Prop :=
+  forall i, from <= i < to -> Mem.loadbytes m b i 1 = Some (Byte Byte.zero :: nil).
+
+Lemma reads_as_zeros_mono: forall m b from1 from2 to1 to2,
+  reads_as_zeros m b from1 to1 -> from1 <= from2 -> to2 <= to1 ->
+  reads_as_zeros m b from2 to2.
+Proof.
+  intros; red; intros. apply H; lia.
+Qed.
+
+Remark reads_as_zeros_unchanged:
+  forall (P: block -> Z -> Prop) m b from to m',
+  reads_as_zeros m b from to ->
+  Mem.unchanged_on P m m' ->
+  (forall i, from <= i < to -> P b i) ->
+  reads_as_zeros m' b from to.
+Proof.
+  intros; red; intros. eapply Mem.loadbytes_unchanged_on; eauto.
+  intros; apply H1. lia.
+Qed.
+
+Lemma reads_as_zeros_loadbytes: forall m b from to,
+  reads_as_zeros m b from to ->
+  forall len pos, from <= pos -> pos + len <= to -> 0 <= len ->
+  Mem.loadbytes m b pos len = Some (repeat (Byte Byte.zero) (Z.to_nat len)).
+Proof.
+  intros until to; intros RZ.
+  induction len using (well_founded_induction (Zwf_well_founded 0)).
+  intros. destruct (zeq len 0).
+- subst len. rewrite Mem.loadbytes_empty by lia. auto.
+- replace (Z.to_nat len) with (S (Z.to_nat (len - 1))).
+  change (repeat (Byte Byte.zero) (S (Z.to_nat (len - 1))))
+    with ((Byte Byte.zero :: nil) ++ repeat (Byte Byte.zero) (Z.to_nat (len - 1))).
+  replace len with (1 + (len - 1)) at 1 by lia. 
+  apply Mem.loadbytes_concat; try lia.
+  + apply RZ. lia.
+  + apply H; unfold Zwf; lia.
+  + rewrite <- Z2Nat.inj_succ by lia. f_equal; lia. 
+Qed.
+
+Lemma reads_as_zeros_equiv: forall m b from to,
+  reads_as_zeros m b from to <-> Genv.readbytes_as_zero m b from (to - from).
+Proof.
+  intros; split; intros.
+- red; intros. set (len := Z.of_nat n).
+  replace n with (Z.to_nat len) by apply Nat2Z.id.
+  eapply reads_as_zeros_loadbytes; eauto. lia. lia.
+- red; intros. red in H. apply (H i 1%nat). lia. lia.
+Qed.
+
+(** ** Semantic correctness of state operations *)
+
+(** Semantic interpretation of states. *)
+
+Record match_state (s: state) (m: mem) (b: block) : Prop := {
+  match_range:
+    0 <= s.(curr) <= s.(total_size);
+  match_contents:
+    Mem.loadbytes m b 0 s.(curr) = Some (boidl (rev s.(init)));
+  match_valid:
+    idlvalid 0 (rev s.(init));
+  match_uninitialized:
+    reads_as_zeros m b s.(curr) s.(total_size)
+}.
+
+Lemma match_size: forall s m b,
+  match_state s m b ->
+  init_data_list_size (rev s.(init)) = s.(curr).
+Proof.
+  intros. rewrite init_data_list_size_boidl.
+  erewrite Mem.loadbytes_length by (eapply match_contents; eauto).
+  apply Z2Nat.id. eapply match_range; eauto.
+Qed.
+
+Lemma curr_pad_to: forall s pos,
+  curr s <= curr (pad_to s pos) /\ pos <= curr (pad_to s pos).
+Proof.
+  unfold pad_to; intros. destruct (zle pos (curr s)); simpl; lia.
+Qed.
+
+Lemma total_size_pad_to: forall s pos,
+  total_size (pad_to s pos) = total_size s.
+Proof.
+  unfold pad_to; intros. destruct (zle pos (curr s)); auto.
+Qed.
+
+Lemma pad_to_correct: forall pos s m b,
+  match_state s m b -> pos <= s.(total_size) ->
+  match_state (pad_to s pos) m b.
+Proof.
+  intros. unfold pad_to. destruct (zle pos (curr s)); auto.
+  destruct H; constructor; simpl; intros.
+- lia.
+- rewrite boidl_rev_cons. simpl.
+  replace pos with (s.(curr) + (pos - s.(curr))) at 1 by lia.
+  apply Mem.loadbytes_concat; try lia.
+    * auto.
+    * eapply reads_as_zeros_loadbytes; eauto. lia. lia. lia.
+- rewrite idlvalid_app. split; auto. simpl. intuition auto using Z.divide_1_l.
+- eapply reads_as_zeros_mono; eauto; lia.
+Qed.
+
+Lemma trisection_correct: forall s m b pos sz bytes1 bytes2 il,
+  match_state s m b ->
+  trisection s.(init) (s.(curr) - (pos + sz)) sz = OK (bytes1, bytes2, il) ->
+  0 <= pos -> pos + sz <= s.(curr) -> 0 <= sz ->
+  Mem.loadbytes m b 0 pos = Some (boidl (rev il))
+  /\ Mem.loadbytes m b pos sz = Some (inj_bytes bytes2)
+  /\ Mem.loadbytes m b (pos + sz) (s.(curr) - (pos + sz)) = Some (inj_bytes bytes1).
+Proof.
+  intros. apply trisection_boidl in H0. destruct H0 as (A & B & C).
+  set (depth := curr s - (pos + sz)) in *.
+  pose proof (match_contents _ _ _ H) as D.
+  replace (curr s) with ((pos + sz) + depth) in D by lia.
+  exploit Mem.loadbytes_split. eexact D. lia. lia.
+  rewrite Z.add_0_l. intros (bytes0 & bytes1' & LB0 & LB1 & E1).
+  exploit Mem.loadbytes_split. eexact LB0. lia. lia.
+  rewrite Z.add_0_l. intros (bytes3 & bytes2' & LB3 & LB2 & E2).
+  rewrite A in E1. rewrite <- app_ass in E1.
+  exploit list_append_injective_r. eexact E1.
+  { unfold inj_bytes; rewrite map_length. erewrite Mem.loadbytes_length; eauto. }
+  intros (E3 & E4).
+  rewrite E2 in E3.
+  exploit list_append_injective_r. eexact E3.
+  { unfold inj_bytes; rewrite map_length. erewrite Mem.loadbytes_length; eauto. }
+  intros (E5 & E6).
+  intuition congruence.
+Qed.
+
+Remark decode_int_zero_ext: forall n bytes,
+  0 <= n <= 4 -> n = Z.of_nat (length bytes) ->
+  Int.zero_ext (n * 8) (Int.repr (decode_int bytes)) = Int.repr (decode_int bytes).
+Proof.
+  intros.
+  assert (0 <= decode_int bytes < two_p (n * 8)).
+  { rewrite H0. replace (length bytes) with (length (rev_if_be bytes)). 
+    apply int_of_bytes_range.
+    apply rev_if_be_length. }
+  assert (two_p (n * 8) <= Int.modulus).
+  { apply (two_p_monotone (n * 8) 32); lia. } 
+  unfold Int.zero_ext.
+  rewrite Int.unsigned_repr by (unfold Int.max_unsigned; lia).
+  rewrite Zbits.Zzero_ext_mod by lia.
+  rewrite Zmod_small by auto. auto.
+Qed.
+
+Theorem load_int_correct: forall s m b pos isz i v,
+  match_state s m b ->
+  load_int s pos isz = OK i ->
+  Mem.load (chunk_for_carrier isz) m b pos = Some v ->
+  v = Vint i.
+Proof.
+  intros until v; intros MS RI LD.
+  exploit Mem.load_valid_access. eauto. intros [PERM ALIGN].
+  unfold load_int in RI. 
+  set (chunk := chunk_for_carrier isz) in *.
+  set (sz := size_chunk chunk) in *.
+  assert (sz > 0) by (apply size_chunk_pos).
+  set (s1 := pad_to s (pos + sz)) in *.
+  assert (pos + sz <= curr s1) by (apply curr_pad_to).
+  monadInv RI. InvBooleans. destruct x as [[bytes1 bytes2] il].
+  assert (MS': match_state s1 m b) by (apply pad_to_correct; auto).
+  exploit trisection_correct; eauto. lia.
+  intros (L1 & L2 & L3).
+  assert (LEN: Z.of_nat (length bytes2) = sz).
+  { apply Mem.loadbytes_length in L2. unfold inj_bytes in L2.
+    rewrite map_length in L2. rewrite L2. apply Z2Nat.id; lia. }
+  exploit Mem.loadbytes_load. eexact L2. exact ALIGN. rewrite LD. 
+  unfold decode_val. rewrite proj_inj_bytes. intros E; inv E; inv EQ0.
+  unfold chunk, chunk_for_carrier; destruct isz; f_equal.
+  - apply (decode_int_zero_ext 1). lia. auto.
+  - apply (decode_int_zero_ext 2). lia. auto.
+  - apply (decode_int_zero_ext 1). lia. auto.
+Qed.
+
+Remark loadbytes_concat_3: forall m b ofs1 len1 l1 ofs2 len2 l2 ofs3 len3 l3 len,
+  Mem.loadbytes m b ofs1 len1 = Some l1 ->
+  Mem.loadbytes m b ofs2 len2 = Some l2 ->
+  Mem.loadbytes m b ofs3 len3 = Some l3 ->
+  ofs2 = ofs1 + len1 -> ofs3 = ofs2 + len2 -> 0 <= len1 -> 0 <= len2 -> 0 <= len3 ->
+  len = len1 + len2 + len3 ->
+  Mem.loadbytes m b ofs1 len = Some (l1 ++ l2 ++ l3).
+Proof.
+  intros. rewrite H7, <- Z.add_assoc. apply Mem.loadbytes_concat. auto.
+  apply Mem.loadbytes_concat. rewrite <- H2; auto. rewrite <- H2, <- H3; auto.
+  lia. lia. lia. lia.
+Qed. 
+
+Theorem store_data_correct: forall s m b pos i s' m',
+  match_state s m b ->
+  store_data s pos i = OK s' ->
+  Genv.store_init_data ge m b pos i = Some m' ->
+  match i with Init_space _ => False | _ => True end ->
+  match_state s' m' b.
+Proof.
+  intros until m'; intros MS ST SI NOSPACE.
+  exploit Genv.store_init_data_aligned; eauto. intros ALIGN.
+  assert (VALID: idvalid i).
+  { destruct i; simpl; auto. simpl in SI. destruct (Genv.find_symbol ge i); try discriminate. exists b0; auto. }
+  unfold store_data in ST.
+  set (sz := init_data_size i) in *.
+  assert (sz >= 0) by (apply init_data_size_pos).
+  set (s1 := pad_to s (pos + sz)) in *.
+  monadInv ST. InvBooleans.
+  assert (U: Mem.unchanged_on (fun b i => ~(pos <= i < pos + sz)) m m').
+  { eapply Genv.store_init_data_unchanged. eauto. tauto. }
+  exploit store_init_data_loadbytes; eauto. fold sz. intros D.
+  destruct (zle (curr s) pos).
+- inv ST.
+  set (il := if zlt (curr s) pos then Init_space (pos - curr s) :: init s else init s).
+  assert (IL: boidl (rev il) = boidl (rev (init s)) ++ repeat (Byte Byte.zero) (Z.to_nat (pos - curr s))).
+  { unfold il; destruct (zlt (curr s) pos).
+  - simpl rev. rewrite boidl_rev_cons. simpl. auto.
+  - rewrite Z_to_nat_neg by lia. simpl. rewrite app_nil_r; auto.
+  }
+  constructor; simpl; intros.
+  + lia.
+  + rewrite boidl_rev_cons, IL, app_ass.
+    apply loadbytes_concat_3 with (len1 := curr s) (ofs2 := curr s) (len2 := pos - curr s) (ofs3 := pos) (len3 := sz); try lia.
+    * eapply Mem.loadbytes_unchanged_on; eauto.
+      intros. simpl. lia.
+      eapply match_contents; eauto.
+    * eapply Mem.loadbytes_unchanged_on; eauto.
+      intros. simpl. lia.
+      eapply reads_as_zeros_loadbytes. eapply match_uninitialized; eauto. lia. lia. lia.
+    * exact D.
+    * eapply match_range; eauto.
+  + rewrite idlvalid_app; split.
+    * unfold il; destruct (zlt (curr s) pos).
+      ** simpl; rewrite idlvalid_app; split. eapply match_valid; eauto. simpl. auto using Z.divide_1_l.
+      ** eapply match_valid; eauto.
+    * simpl.
+      replace (init_data_list_size (rev il)) with pos. tauto.
+      unfold il; destruct (zlt (curr s) pos).
+      ** simpl; rewrite init_data_list_size_app; simpl.
+         erewrite match_size by eauto. lia.
+      ** erewrite match_size by eauto. lia.
+  + eapply reads_as_zeros_unchanged; eauto.
+    eapply reads_as_zeros_mono. eapply match_uninitialized; eauto. lia. lia.
+    intros. simpl. lia.
+- monadInv ST. destruct x as [[bytes1 bytes2] il]. inv EQ0.
+  assert (pos + sz <= curr s1) by (apply curr_pad_to).
+  assert (MS': match_state s1 m b) by (apply pad_to_correct; auto).
+  exploit trisection_correct; eauto. lia.
+  intros (L1 & L2 & L3).
+  constructor; simpl; intros.
+  + eapply match_range; eauto.
+  + rewrite add_rev_bytes_spec, rev_app_distr; simpl; rewrite app_ass; simpl.
+    rewrite <- map_rev, rev_involutive.
+    rewrite boidl_app. simpl. rewrite boidl_init_bytes.
+    apply loadbytes_concat_3 with (len1 := pos) (ofs2 := pos) (len2 := sz) (ofs3 := pos + sz)
+                                  (len3 := curr s1 - (pos + sz)); try lia.
+    * eapply Mem.loadbytes_unchanged_on; eauto.
+      intros. simpl. lia.
+    * exact D.
+    * eapply Mem.loadbytes_unchanged_on; eauto.
+      intros. simpl. lia.
+  + apply add_rev_bytes_valid. simpl; rewrite idlvalid_app; split.
+    * eapply trisection_valid; eauto. eapply match_valid; eauto.
+    * rewrite init_data_list_size_boidl. erewrite Mem.loadbytes_length by eauto.
+      rewrite Z2Nat.id by lia. simpl. tauto.
+  + eapply reads_as_zeros_unchanged; eauto. eapply match_uninitialized; eauto.
+    intros. simpl. lia.
+Qed.
+
+Corollary store_int_correct: forall s m b pos isz n s' m',
+  match_state s m b ->
+  store_int s pos isz n = OK s' ->
+  Mem.store (chunk_for_carrier isz) m b pos (Vint n) = Some m' ->
+  match_state s' m' b.
+Proof.
+  intros. eapply store_data_correct; eauto.
+- destruct isz; exact H1.
+- destruct isz; exact I.
+Qed.
+
+Theorem init_data_list_of_state_correct: forall s m b il b' m1,
+  match_state s m b ->
+  init_data_list_of_state s = OK il ->
+  Mem.range_perm m1 b' 0 s.(total_size) Cur Writable ->
+  reads_as_zeros m1 b' 0 s.(total_size) ->
+  exists m2,
+     Genv.store_init_data_list ge m1 b' 0 il = Some m2
+  /\ Mem.loadbytes m2 b' 0 (init_data_list_size il) = Mem.loadbytes m b 0 s.(total_size).
+Proof.
+  intros. unfold init_data_list_of_state in H0; monadInv H0. rename l into LE.
+  set (s1 := pad_to s s.(total_size)) in *.
+  assert (MS1: match_state s1 m b) by (apply pad_to_correct; auto; lia).
+  apply reads_as_zeros_equiv in H2. rewrite Z.sub_0_r in H2.
+  assert (R: rev' (init s1) = rev (init s1)).
+  { unfold rev'. rewrite <- rev_alt. auto. }
+  assert (C: curr s1 = total_size s).
+  { unfold s1, pad_to. destruct zle; simpl; lia. }
+  assert (A: Genv.init_data_list_aligned 0 (rev (init s1))).
+  { exploit match_valid; eauto. generalize (rev (init s1)) 0.
+    induction l as [ | i l]; simpl; intuition. }
+  assert (B: forall id ofs, In (Init_addrof id ofs) (rev (init s1)) ->
+             exists b, Genv.find_symbol ge id = Some b).
+  { intros id ofs. exploit match_valid; eauto. generalize (rev (init s1)) 0.
+    induction l as [ | i l]; simpl; intuition eauto. subst i; assumption. }
+  exploit Genv.store_init_data_list_exists.
+  2: eexact A. 2: eexact B.
+  erewrite match_size by eauto. rewrite C. eauto.
+  intros (m2 & ST). exists m2; split.
+- rewrite R. auto.
+- rewrite R. transitivity (Some (boidl (rev (init s1)))).
+  + eapply Genv.store_init_data_list_loadbytes; eauto.
+    erewrite match_size, C by eauto. auto.
+  + symmetry. rewrite <- C. eapply match_contents; eauto.
+Qed.
+
+(** ** Total size properties *)
+
+Lemma total_size_store_data: forall s pos i s',
+  store_data s pos i = OK s' -> total_size s' = total_size s.
+Proof.
+  unfold store_data; intros. monadInv H. destruct (zle (curr s) pos); monadInv H.
+- auto.
+- destruct x as [[bytes1 bytes2] il2]. inv EQ0. simpl. apply total_size_pad_to.
+Qed.
+
+Lemma total_size_transl_init_bitfield: forall ce s ty sz p w i pos s',
+  transl_init_bitfield ce s ty sz p w i pos = OK s' -> total_size s' = total_size s.
+Proof.
+  unfold transl_init_bitfield; intros. destruct i; monadInv H. destruct x; monadInv EQ0.
+  eapply total_size_store_data. eexact EQ2.
+Qed.
+
+Lemma total_size_transl_init_rec: forall ce s ty i pos s',
+  transl_init_rec ce s ty i pos = OK s' -> total_size s' = total_size s
+with total_size_transl_init_array: forall ce s tyelt il pos s',
+  transl_init_array ce s tyelt il pos = OK s' -> total_size s' = total_size s
+with total_size_transl_init_struct: forall ce s ms il base pos s',
+  transl_init_struct ce s ms il base pos = OK s' -> total_size s' = total_size s.
+Proof.
+- destruct i; simpl; intros.
+  + monadInv H; eauto using total_size_store_data.
+  + destruct ty; monadInv H. eauto.
+  + destruct ty; monadInv H. destruct (co_su x); try discriminate. eauto.
+  + destruct ty; monadInv H. destruct (co_su x); monadInv EQ0. destruct x2.
+    * eauto.
+    * eauto using total_size_transl_init_bitfield.
+- destruct il; simpl; intros.
+  + inv H; auto.
+  + monadInv H. transitivity (total_size x); eauto.
+- destruct il; simpl; intros.
+  + inv H; auto.
+  + revert ms pos H. induction ms; intros.
+    * inv H.
+    * destruct (member_not_initialized a). eapply IHms; eauto.
+      monadInv H. transitivity (total_size x1). eauto.
+      destruct x0; eauto using total_size_transl_init_bitfield.
 Qed.
 
 (** * Soundness of the translation of initializers *)
 
 (** Soundness for single initializers. *)
 
-Theorem transl_init_single_steps:
-  forall ty a data f m v1 ty1 m' v chunk b ofs m'',
+Inductive exec_assign: mem -> block -> Z -> bitfield -> type -> val -> mem -> Prop :=
+  | exec_assign_full: forall m b ofs ty v m' chunk,
+      access_mode ty = By_value chunk ->
+      Mem.store chunk m b ofs v = Some m' ->
+      exec_assign m b ofs Full ty v m'
+  | exec_assign_bits: forall m b ofs sz sg sg1 attr pos width ty n m' c,
+      type_is_volatile ty = false ->
+      0 <= pos -> 0 < width -> pos + width <= bitsize_intsize sz ->
+      sg1 = (if zlt width (bitsize_intsize sz) then Signed else sg) ->
+      Mem.load (chunk_for_carrier sz) m b ofs = Some (Vint c) ->
+      Mem.store (chunk_for_carrier sz) m b ofs
+                (Vint (Int.bitfield_insert (first_bit sz pos width) width c n)) = Some m' ->
+      exec_assign m b ofs (Bits sz sg pos width) (Tint sz sg1 attr) (Vint n) m'.
+
+Lemma transl_init_single_sound:
+  forall ty a data f m v1 ty1 m' v b ofs m'',
   transl_init_single ge ty a = OK data ->
   star step ge (ExprState f a Kstop empty_env m) E0 (ExprState f (Eval v1 ty1) Kstop empty_env m') ->
   sem_cast v1 ty1 ty m' = Some v ->
-  access_mode ty = By_value chunk ->
-  Mem.store chunk m' b ofs v = Some m'' ->
-  Genv.store_init_data ge m b ofs data = Some m''.
+  exec_assign m' b ofs Full ty v m'' ->
+  Genv.store_init_data ge m b ofs data = Some m''
+  /\ match data with Init_space _ => False | _ => True end.
 Proof.
-  intros. monadInv H. monadInv EQ. 
+  intros until m''; intros TR STEPS CAST ASG.
+  monadInv TR. monadInv EQ. 
   exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1.
   exploit sem_cast_match; eauto. intros D.
-  unfold Genv.store_init_data.
-  inv D.
+  inv ASG. rename H into A. unfold Genv.store_init_data. inv D.
 - (* int *)
   remember Archi.ptr64 as ptr64.  destruct ty; try discriminate EQ0.
 + destruct i0; inv EQ0.
-  destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto.
-  destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto.
-  simpl in H2; inv H2. assumption.
-  simpl in H2; inv H2. assumption.
-+ destruct ptr64; inv EQ0. simpl in H2; unfold Mptr in H2; rewrite <- Heqptr64 in H2; inv H2. assumption.
+  destruct s; simpl in A; inv A. rewrite <- Mem.store_signed_unsigned_8; auto. auto.
+  destruct s; simpl in A; inv A. rewrite <- Mem.store_signed_unsigned_16; auto. auto.
+  simpl in A; inv A. auto.
+  simpl in A; inv A. auto.
++ destruct ptr64; inv EQ0. simpl in A; unfold Mptr in A; rewrite <- Heqptr64 in A; inv A. auto.
 - (* Long *)
-  remember Archi.ptr64 as ptr64. destruct ty; inv EQ0.
-+ simpl in H2; inv H2. assumption.
-+ simpl in H2; unfold Mptr in H2; destruct Archi.ptr64; inv H4. 
-  inv H2; assumption.
+  remember Archi.ptr64 as ptr64. destruct ty; monadInv EQ0.
++ simpl in A; inv A. auto.
++ simpl in A; unfold Mptr in A; rewrite <- Heqptr64 in A; inv A. auto.
 - (* float *)
   destruct ty; try discriminate.
-  destruct f1; inv EQ0; simpl in H2; inv H2; assumption.
+  destruct f1; inv EQ0; simpl in A; inv A; auto.
 - (* single *)
   destruct ty; try discriminate.
-  destruct f1; inv EQ0; simpl in H2; inv H2; assumption.
+  destruct f1; inv EQ0; simpl in A; inv A; auto.
 - (* pointer *)
   unfold inj in H.
-  assert (data = Init_addrof b1 ofs1 /\ chunk = Mptr).
+  assert (X: data = Init_addrof b1 ofs1 /\ chunk = Mptr).
   { remember Archi.ptr64 as ptr64.
     destruct ty; inversion EQ0.
-    destruct i; inv H5. unfold Mptr. destruct Archi.ptr64; inv H6; inv H2; auto.
-    subst ptr64. unfold Mptr. destruct Archi.ptr64; inv H5; inv H2; auto.
-    inv H2. auto. }
-  destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H.
-  rewrite Ptrofs.add_zero in H3. auto.
+    - destruct i; monadInv H2. unfold Mptr. rewrite <- Heqptr64. inv A; auto.
+    - monadInv H2. unfold Mptr. rewrite <- Heqptr64. inv A; auto.
+    - inv A; auto.
+  }
+  destruct X; subst. destruct (Genv.find_symbol ge b1); inv H.
+  rewrite Ptrofs.add_zero in H0. auto.
 - (* undef *)
   discriminate.
 Qed.
 
-(** Size properties for initializers. *)
-
-Lemma transl_init_single_size:
-  forall ty a data,
-  transl_init_single ge ty a = OK data ->
-  init_data_size data = sizeof ge ty.
-Proof.
-  intros. monadInv H. monadInv EQ. remember Archi.ptr64 as ptr64. destruct x.
-- monadInv EQ0.
-- destruct ty; try discriminate.
-  destruct i0; inv EQ0; auto.
-  destruct ptr64; inv EQ0. 
-Local Transparent sizeof.
-  unfold sizeof. rewrite <- Heqptr64; auto.
-- destruct ty; inv EQ0; auto. 
-  unfold sizeof. destruct Archi.ptr64; inv H0; auto.
-- destruct ty; try discriminate.
-  destruct f0; inv EQ0; auto.
-- destruct ty; try discriminate.
-  destruct f0; inv EQ0; auto.
-- destruct ty; try discriminate.
-  destruct i0; inv EQ0; auto.
-  destruct Archi.ptr64 eqn:SF; inv H0. simpl. rewrite SF; auto.
-  destruct ptr64; inv EQ0. simpl. rewrite <- Heqptr64; auto.
-  inv EQ0. unfold init_data_size, sizeof. auto.
-Qed.
-
-Notation idlsize := init_data_list_size.
-
-Remark padding_size:
-  forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm.
-Proof.
-  unfold tr_padding; intros. destruct (zlt frm to).
-  simpl. extlia.
-  simpl. lia.
-Qed.
-
-Remark idlsize_app:
-  forall d1 d2, idlsize (d1 ++ d2) = idlsize d1 + idlsize d2.
-Proof.
-  induction d1; simpl; intros.
-  auto.
-  rewrite IHd1. lia.
-Qed.
-
-Remark union_field_size:
-  forall f ty fl, field_type f fl = OK ty -> sizeof ge ty <= sizeof_union ge fl.
-Proof.
-  induction fl as [|[i t]]; simpl; intros.
-- inv H.
-- destruct (ident_eq f i).
-  + inv H. extlia.
-  + specialize (IHfl H). extlia.
-Qed.
-
-Hypothesis ce_consistent: composite_env_consistent ge.
-
-Lemma tr_init_size:
-  forall i ty data,
-  tr_init ty i data ->
-  idlsize data = sizeof ge ty
-with tr_init_array_size:
-  forall ty il sz data,
-  tr_init_array ty il sz data ->
-  idlsize data = sizeof ge ty * sz
-with tr_init_struct_size:
-  forall ty fl il pos data,
-  tr_init_struct ty fl il pos data ->
-  sizeof_struct ge pos fl <= sizeof ge ty ->
-  idlsize data + pos = sizeof ge ty.
-Proof.
-Local Opaque sizeof.
-- destruct 1; simpl.
-+ erewrite transl_init_single_size by eauto. lia.
-+ Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. 
-+ replace (idlsize d) with (idlsize d + 0) by lia.
-  eapply tr_init_struct_size; eauto. simpl.
-  unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H.
-  erewrite co_consistent_sizeof by (eapply ce_consistent; eauto).
-  unfold sizeof_composite. rewrite H0. apply align_le.
-  destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
-+ rewrite idlsize_app, padding_size. 
-  exploit tr_init_size; eauto. intros EQ; rewrite EQ. lia.
-  simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H.
-  apply Z.le_trans with (sizeof_union ge (co_members co)).
-  eapply union_field_size; eauto.
-  erewrite co_consistent_sizeof by (eapply ce_consistent; eauto).
-  unfold sizeof_composite. rewrite H0. apply align_le.
-  destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
-
-- destruct 1; simpl.
-+ lia.
-+ rewrite Z.mul_comm.
-  assert (0 <= sizeof ge ty * sz).
-  { apply Zmult_gt_0_le_0_compat. lia. generalize (sizeof_pos ge ty); lia. }
-  extlia.
-+ rewrite idlsize_app. 
-  erewrite tr_init_size by eauto. 
-  erewrite tr_init_array_size by eauto.
-  ring.
-
-- destruct 1; simpl; intros.
-+ rewrite padding_size by auto. lia.
-+ rewrite ! idlsize_app, padding_size. 
-  erewrite tr_init_size by eauto. 
-  rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). lia.
-  unfold pos1. apply align_le. apply alignof_pos. 
-Qed.
+(* Hypothesis ce_consistent: composite_env_consistent ge. *)
 
 (** A semantics for general initializers *)
 
 Definition dummy_function := mkfunction Tvoid cc_default nil nil Sskip.
 
-Fixpoint fields_of_struct (fl: members) (pos: Z) : list (Z * type) :=
-  match fl with
-  | nil => nil
-  | (id1, ty1) :: fl' =>
-      (align pos (alignof ge ty1), ty1) :: fields_of_struct fl' (align pos (alignof ge ty1) + sizeof ge ty1)
+Fixpoint initialized_fields_of_struct (ms: members) (pos: Z) : res (list (Z * bitfield * type)) :=
+  match ms with
+  | nil =>
+      OK nil
+  | m :: ms' =>
+      let pos' := next_field ge.(genv_cenv) pos m in
+      if member_not_initialized m
+      then initialized_fields_of_struct ms' pos'
+      else
+        do ofs_bf <- layout_field ge.(genv_cenv) pos m;
+        do l <- initialized_fields_of_struct ms' pos';
+        OK ((ofs_bf, type_member m) :: l)
   end.
 
-Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop :=
-  | exec_init_single: forall m b ofs ty a v1 ty1 chunk m' v m'',
+Inductive exec_init: mem -> block -> Z -> bitfield -> type -> initializer -> mem -> Prop :=
+  | exec_init_single_: forall m b ofs bf ty a v1 ty1 m' v m'',
       star step ge (ExprState dummy_function a Kstop empty_env m)
                 E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') ->
       sem_cast v1 ty1 ty m' = Some v ->
-      access_mode ty = By_value chunk ->
-      Mem.store chunk m' b ofs v = Some m'' ->
-      exec_init m b ofs ty (Init_single a) m''
+      exec_assign m' b ofs bf ty v m'' ->
+      exec_init m b ofs bf ty (Init_single a) m''
   | exec_init_array_: forall m b ofs ty sz a il m',
       exec_init_array m b ofs ty sz il m' ->
-      exec_init m b ofs (Tarray ty sz a) (Init_array il) m'
-  | exec_init_struct: forall m b ofs id a il co m',
+      exec_init m b ofs Full (Tarray ty sz a) (Init_array il) m'
+  | exec_init_struct_: forall m b ofs id a il co flds m',
       ge.(genv_cenv)!id = Some co -> co_su co = Struct ->
-      exec_init_list m b ofs (fields_of_struct (co_members co) 0) il m' ->
-      exec_init m b ofs (Tstruct id a) (Init_struct il) m'
-  | exec_init_union: forall m b ofs id a f i ty co m',
+      initialized_fields_of_struct (co_members co) 0 = OK flds ->
+      exec_init_struct m b ofs flds il m' ->
+      exec_init m b ofs Full (Tstruct id a) (Init_struct il) m'
+  | exec_init_union_: forall m b ofs id a f i co ty pos bf m',
       ge.(genv_cenv)!id = Some co -> co_su co = Union ->
       field_type f (co_members co) = OK ty ->
-      exec_init m b ofs ty i m' ->
-      exec_init m b ofs (Tunion id a) (Init_union f i) m'
+      union_field_offset ge f (co_members co) = OK (pos, bf) ->
+      exec_init m b (ofs + pos) bf ty i m' ->
+      exec_init m b ofs Full (Tunion id a) (Init_union f i) m'
 
 with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop :=
   | exec_init_array_nil: forall m b ofs ty sz,
       sz >= 0 ->
       exec_init_array m b ofs ty sz Init_nil m
   | exec_init_array_cons: forall m b ofs ty sz i1 il m' m'',
-      exec_init m b ofs ty i1 m' ->
+      exec_init m b ofs Full ty i1 m' ->
       exec_init_array m' b (ofs + sizeof ge ty) ty (sz - 1) il m'' ->
       exec_init_array m b ofs ty sz (Init_cons i1 il) m''
 
-with exec_init_list: mem -> block -> Z -> list (Z * type) -> initializer_list -> mem -> Prop :=
-  | exec_init_list_nil: forall m b ofs,
-      exec_init_list m b ofs nil Init_nil m
-  | exec_init_list_cons: forall m b ofs pos ty l i1 il m' m'',
-      exec_init m b (ofs + pos) ty i1 m' ->
-      exec_init_list m' b ofs l il m'' ->
-      exec_init_list m b ofs ((pos, ty) :: l) (Init_cons i1 il) m''.
+with exec_init_struct: mem -> block -> Z -> list (Z * bitfield * type) -> initializer_list -> mem -> Prop :=
+  | exec_init_struct_nil: forall m b ofs,
+      exec_init_struct m b ofs nil Init_nil m
+  | exec_init_struct_cons: forall m b ofs pos bf ty l i1 il m' m'',
+      exec_init m b (ofs + pos) bf ty i1 m' ->
+      exec_init_struct m' b ofs l il m'' ->
+      exec_init_struct m b ofs ((pos, bf, ty) :: l) (Init_cons i1 il) m''.
 
 Scheme exec_init_ind3 := Minimality for exec_init Sort Prop
   with exec_init_array_ind3 := Minimality for exec_init_array Sort Prop
-  with exec_init_list_ind3 := Minimality for exec_init_list Sort Prop.
-Combined Scheme exec_init_scheme from exec_init_ind3, exec_init_array_ind3, exec_init_list_ind3.
+  with exec_init_struct_ind3 := Minimality for exec_init_struct Sort Prop.
+Combined Scheme exec_init_scheme from exec_init_ind3, exec_init_array_ind3, exec_init_struct_ind3.
 
 Remark exec_init_array_length:
   forall m b ofs ty sz il m',
@@ -809,87 +1256,95 @@ Proof.
   induction 1; lia.
 Qed.
 
-Lemma store_init_data_list_app:
-  forall data1 m b ofs m' data2 m'',
-  Genv.store_init_data_list ge m b ofs data1 = Some m' ->
-  Genv.store_init_data_list ge m' b (ofs + idlsize data1) data2 = Some m'' ->
-  Genv.store_init_data_list ge m b ofs (data1 ++ data2) = Some m''.
-Proof.
-  induction data1; simpl; intros.
-  inv H. rewrite Z.add_0_r in H0. auto.
-  destruct (Genv.store_init_data ge m b ofs a); try discriminate.
-  rewrite Z.add_assoc in H0. eauto.
-Qed.
-
-Remark store_init_data_list_padding:
-  forall frm to b ofs m,
-  Genv.store_init_data_list ge m b ofs (tr_padding frm to) = Some m.
+Lemma transl_init_rec_sound:
+   (forall m b ofs bf ty i m',
+    exec_init m b ofs bf ty i m' ->
+    forall s s',
+    match_state s m b ->
+    match bf with
+    | Full => transl_init_rec ge s ty i ofs
+    | Bits sz sg p w => transl_init_bitfield ge s ty sz p w i ofs
+    end = OK s' ->
+    match_state s' m' b)
+/\ (forall m b ofs ty sz il m',
+    exec_init_array m b ofs ty sz il m' ->
+    forall s s',
+    match_state s m b ->
+    transl_init_array ge s ty il ofs = OK s' ->
+    match_state s' m' b)
+/\ (forall m b ofs flds il m',
+    exec_init_struct m b ofs flds il m' ->
+    forall s s' ms pos,
+    match_state s m b ->
+    initialized_fields_of_struct ms pos = OK flds ->
+    transl_init_struct ge s ms il ofs pos = OK s' ->
+    match_state s' m' b).
 Proof.
-  intros. unfold tr_padding. destruct (zlt frm to); auto.
-Qed.
-
-Lemma tr_init_sound:
-  (forall m b ofs ty i m', exec_init m b ofs ty i m' ->
-   forall data, tr_init ty i data ->
-   Genv.store_init_data_list ge m b ofs data = Some m')
-/\(forall m b ofs ty sz il m', exec_init_array m b ofs ty sz il m' ->
-   forall data, tr_init_array ty il sz data ->
-   Genv.store_init_data_list ge m b ofs data = Some m')
-/\(forall m b ofs l il m', exec_init_list m b ofs l il m' ->
-   forall ty fl data pos,
-   l = fields_of_struct fl pos ->
-   tr_init_struct ty fl il pos data ->
-   Genv.store_init_data_list ge m b (ofs + pos) data = Some m').
-Proof.
-Local Opaque sizeof.
-  apply exec_init_scheme; simpl; intros.
+  apply exec_init_scheme.
 - (* single *)
-  inv H3. simpl. erewrite transl_init_single_steps by eauto. auto.
+  intros until m''; intros STEP CAST ASG s s' MS TR. destruct bf; monadInv TR.
+  + (* full *)
+    exploit transl_init_single_sound; eauto. intros [P Q].
+    eapply store_data_correct; eauto. 
+  + (* bitfield *)
+    destruct x; monadInv EQ0. monadInv EQ.
+    exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1.
+    exploit sem_cast_match; eauto. intros D.
+    inv ASG. inv D.
+    set (f := first_bit sz pos width) in *.
+    assert (E: Vint c = Vint x) by (eapply load_int_correct; eauto).
+    inv E.
+    eapply store_int_correct; eauto.
 - (* array *)
-  inv H1. replace (Z.max 0 sz) with sz in H7. eauto.
-  assert (sz >= 0) by (eapply exec_init_array_length; eauto). extlia.
+  intros. monadInv H2. eauto.
 - (* struct *)
-  inv H3. unfold lookup_composite in H7. rewrite H in H7. inv H7. 
-  replace ofs with (ofs + 0) by lia. eauto.
+  intros. monadInv H5. unfold lookup_composite in EQ. rewrite H in EQ. inv EQ.
+  rewrite H0 in EQ0. eauto.
 - (* union *)
-  inv H4. unfold lookup_composite in H9. rewrite H in H9. inv H9. rewrite H1 in H12; inv H12. 
-  eapply store_init_data_list_app. eauto.
-  apply store_init_data_list_padding.
-
-- (* array, empty *)
-  inv H0; auto.
-- (* array, nonempty *)
-  inv H3.
-  eapply store_init_data_list_app.
-  eauto.
-  rewrite (tr_init_size _ _ _ H7). eauto.
-
-- (* struct, empty *)
-  inv H0. apply store_init_data_list_padding.
-- (* struct, nonempty *)
-  inv H4. simpl in H3; inv H3. 
-  eapply store_init_data_list_app. apply store_init_data_list_padding.
-  rewrite padding_size.
-  replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by lia.
-  eapply store_init_data_list_app.
+  intros. monadInv H6. unfold lookup_composite in EQ. rewrite H in EQ. inv EQ. rewrite H0 in EQ0.
+  rewrite H1, H2 in EQ0. simpl in EQ0. eauto.
+- (* array nil *)
+  intros. monadInv H1. auto.
+- (* array cons *)
+  intros. monadInv H4. eauto.
+- (* struct nil *)
+  intros. monadInv H1. auto.
+- (* struct cons *)
+  intros. simpl in H5. revert H4 H5. generalize pos0. induction ms as [ | m1 ms]. discriminate.
+  simpl. destruct (member_not_initialized m1).
+  intros; eapply IHms; eauto.
+  clear IHms. intros. monadInv H5. rewrite EQ in H4. monadInv H4. inv EQ0.
   eauto.
-  rewrite (tr_init_size _ _ _ H9).
-  rewrite <- Z.add_assoc. eapply H2. eauto. eauto.
-  apply align_le. apply alignof_pos.
 Qed.
 
 End SOUNDNESS.
 
 Theorem transl_init_sound:
-  forall p m b ty i m' data,
-  exec_init (globalenv p) m b 0 ty i m' ->
+  forall p m b ty i m1 data,
+  let sz := sizeof (prog_comp_env p) ty in
+  Mem.range_perm m b 0 sz Cur Writable ->
+  reads_as_zeros m b 0 sz ->
+  exec_init (globalenv p) m b 0 Full ty i m1 ->
   transl_init (prog_comp_env p) ty i = OK data ->
-  Genv.store_init_data_list (globalenv p) m b 0 data = Some m'.
+  exists m2,
+     Genv.store_init_data_list (globalenv p) m b 0 data = Some m2
+  /\ Mem.loadbytes m2 b 0 (init_data_list_size data) = Mem.loadbytes m1 b 0 sz.
 Proof.
   intros.
   set (ge := globalenv p) in *.
-  change (prog_comp_env p) with (genv_cenv ge) in H0.
-  destruct (tr_init_sound ge) as (A & B & C).
-  eapply build_composite_env_consistent. apply prog_comp_env_eq.
-  eapply A; eauto. apply transl_init_spec; auto.
+  change (prog_comp_env p) with (genv_cenv ge) in *.
+  unfold transl_init in H2; monadInv H2.
+  fold sz in EQ. set (s0 := initial_state sz) in *.
+  assert (match_state ge s0 m b).
+  { constructor; simpl.
+  - generalize (sizeof_pos ge ty). fold sz. lia.
+  - apply Mem.loadbytes_empty. lia.
+  - auto.
+  - assumption.
+  }
+  assert (match_state ge x m1 b).
+  { eapply (proj1 (transl_init_rec_sound ge)); eauto. }
+  assert (total_size x = sz).
+  { change sz with s0.(total_size). eapply total_size_transl_init_rec; eauto. }
+  rewrite <- H4. eapply init_data_list_of_state_correct; eauto; rewrite H4; auto.
 Qed.