Require Import VST.floyd.base2.
Require Import VST.floyd.client_lemmas.
Require Import VST.floyd.fieldlist.
Require Import VST.floyd.type_induction.
Require Import VST.floyd.nested_pred_lemmas.
Require Import VST.floyd.align_compatible_dec.
Open Scope Z.

(************************************************

Definition of nested_field_type2, nested_field_offset2

The principle of this part is only exposing nft2 and nfo2 to users
and hide the implimentation of nf_rec

************************************************)

Inductive gfield : Type :=
  | ArraySubsc : forall i: Z, gfield
  | StructField : forall i: ident, gfield
  | UnionField : forall i: ident, gfield.

Delimit Scope gfield_scope with gfield.
Bind Scope gfield_scope with list gfield.
Notation "x 'DOT' y " := (@cons gfield (StructField y) x%gfield) (at level 40, left associativity): gfield_scope.
Notation "x 'UDOT' y " := (@cons gfield (UnionField y) x%gfield) (at level 40, left associativity): gfield_scope.
Notation "x 'SUB' y " := (@cons gfield (ArraySubsc y) x%gfield) (at level 40, left associativity): gfield_scope.
Notation "'DOT' y " := (@cons gfield (StructField y) nil) (at level 40): gfield_scope.
Notation "'UDOT' y " := (@cons gfield (UnionField y) nil) (at level 40): gfield_scope.
Notation "'SUB' y " := (@cons gfield (ArraySubsc y) nil) (at level 40): gfield_scope.

(*
Notation "Y @s X" := (cons (StructField X) Y) (at level 70).
Notation "Y @u X" := (cons (UnionField X) Y) (at level 70).
Notation "Y [ X ]" := (cons (ArraySubsc X) Y) (at level 70).
*)
(*
Notation "@@s X" := (cons (StructField X) nil) (at level 60).
Notation "@@u X" := (cons (UnionField X) nil) (at level 60).
Notation "[( X )]" := (cons (ArraySubsc X) nil) (at level 60).
*)

Section COMPOSITE_ENV.

Context {cs: compspecs}.
Definition gfield_type t gf :=
  match t, gf with
  | Tarray t0 _ _, ArraySubsc _ => t0
  | Tstruct id _, StructField i
  | Tunion id _, UnionField i => field_type i (co_members (get_co id))
  | _, _ => Tvoid
  end.

Definition gfield_offset t gf :=
  match t, gf with
  | Tarray t0 _ _, ArraySubsc i => sizeof t0 * i
  | Tstruct id _, StructField i => field_offset cenv_cs i (co_members (get_co id))
  | Tunion id _, UnionField i => 0
  | _, _ => 0
  end.

Definition no_alignas_attr (a: attr): attr := mk_attr (attr_volatile a) None.

Lemma no_alignas_attr_spec: forall a d,
  align_attr (no_alignas_attr a) d = d.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (align_attr (no_alignas_attr a) d) d *)
  destruct a; simpl.
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
  reflexivity.
Qed.

Definition gfield_array_type t lo hi :=
  match t with
  | Tarray t0 _ a => Tarray t0 (hi - lo) (no_alignas_attr a)
  | _ => Tarray Tvoid (hi - lo) (no_alignas_attr (attr_of_type t))
  end.

Fixpoint nested_field_rec (t: type) (gfs: list gfield) : option (prod Z type) :=
  match gfs with
  | nil => Some (0, t)
  | hd :: tl =>
    match nested_field_rec t tl with
    | Some (pos, t') =>
      match t', hd with
      | Tarray t'' n _, ArraySubsc i => Some(pos + sizeof t'' * i, t'')
      | Tstruct id _, StructField i =>
        let m := co_members (get_co id) in
        if compute_in_members i m then
          Some (pos + field_offset cenv_cs i m, field_type i m)
        else
          None
      | Tunion id _, UnionField i =>
        let m := co_members (get_co id) in
        if compute_in_members i m then
          Some (pos, field_type i m)
        else
          None
      | _, _ => None
      end
    | None => None
    end
  end%Z.

(*
Fixpoint nested_field_rec (t: type) (gfs: list gfield) : option (prod Z type) :=
  match gfs with
  | nil => Some (0, t)
  | hd :: tl =>
    match nested_field_rec t tl with
    | Some (pos, t') =>
      match t', hd with
      | Tarray t'' n _, ArraySubsc i => Some(pos + sizeof t'' * i, t'')
      | Tstruct id _, StructField i =>
        if compute_in_members i (co_members (get_co id)) then
          Some (pos + field_offset cenv_cs i (co_members (get_co id)), field_type i (co_members (get_co id)))
        else
          None
      | Tunion id _, UnionField i =>
        if compute_in_members i (co_members (get_co id)) then
          Some (pos, field_type i (co_members (get_co id)))
        else
          None
      | _, _ => None
      end
    | None => None
    end
  end.
*)

Definition nested_field_offset (t: type) (gfs: list gfield) : Z :=
  match nested_field_rec t gfs with
  | Some (pos, _) => pos
  | _ => 0
  end.

Definition nested_field_type (t: type) (gfs: list gfield) : type :=
  match nested_field_rec t gfs with
  | Some (_, t0) => t0
  | _ => Tvoid
  end.

Definition nested_field_array_type t gfs lo hi :=
  Tarray (nested_field_type t (ArraySubsc 0 :: gfs)) (hi - lo) (no_alignas_attr (attr_of_type (nested_field_type t gfs))).

Definition legal_field t gf :=
  match t, gf with
  | Tarray _ n _, ArraySubsc i => 0 <= i < n
  | Tstruct id _, StructField i => in_members i (co_members (get_co id))
  | Tunion id _, UnionField i => in_members i (co_members (get_co id))
  | _, _ => False
  end.

Definition legal_field0 t gf :=
  match t, gf with
  | Tarray _ n _, ArraySubsc i => 0 <= i <= n
  | Tstruct id _, StructField i => in_members i (co_members (get_co id))
  | Tunion id _, UnionField i => in_members i (co_members (get_co id))
  | _, _ => False
  end.

Fixpoint legal_nested_field (t: type) (gfs: list gfield) : Prop :=
  match gfs with
  | nil => True
  | gf :: gfs0 => legal_nested_field t gfs0 /\ legal_field (nested_field_type t gfs0) gf
  end.

Definition legal_nested_field0 t gfs :=
  match gfs with
  | nil => True
  | gf :: gfs0 => legal_nested_field t gfs0 /\ legal_field0 (nested_field_type t gfs0) gf
  end.

Fixpoint compute_legal_nested_field (t: type) (gfs: list gfield) : list Prop :=
  match gfs with
  | nil => nil
  | gf :: gfs0 =>
    match (nested_field_type t gfs0), gf with
    | Tarray _ n _, ArraySubsc i =>
       (0 <= i < n) :: compute_legal_nested_field t gfs0
    | Tstruct id _, StructField i =>
       if compute_in_members i (co_members (get_co id)) then compute_legal_nested_field t gfs0 else False :: nil
    | Tunion id _, UnionField i =>
       if compute_in_members i (co_members (get_co id)) then compute_legal_nested_field t gfs0 else False :: nil
    | _, _ => False :: nil
    end
  end.

Lemma nested_field_type_ind: forall t gfs,
  nested_field_type t gfs =
  match gfs with
  | nil => t
  | gf :: gfs0 => gfield_type (nested_field_type t gfs0) gf
  end.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t gfs) match gfs with | nil => Z0 | cons gf gfs0 => Z.add (nested_field_offset t gfs0) (gfield_offset (nested_field_type t gfs0) gf) end *)
  destruct gfs as [| gf gfs]; [reflexivity |].
(* Goal: @eq type (nested_field_type t (@cons gfield gf gfs)) (gfield_type (nested_field_type t gfs) gf) *)
  unfold nested_field_type.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  simpl.
(* Goal: @eq Z match match nested_field_rec t gfs with | Some (pair pos (Tvoid as t') as p) => @None (prod Z type) | Some (pair pos (Tint i s a as t') as p) => @None (prod Z type) | Some (pair pos (Tlong s a as t') as p) => @None (prod Z type) | Some (pair pos (Tfloat f a as t') as p) => @None (prod Z type) | Some (pair pos (Tpointer t a as t') as p) => @None (prod Z type) | Some (pair pos (Tarray t'' n a as t') as p) => match gf with | ArraySubsc i => @Some (prod Z type) (@pair Z type (Z.add pos (Z.mul (@sizeof (@cenv_cs cs) t'') i)) t'') | StructField i => @None (prod Z type) | UnionField i => @None (prod Z type) end | Some (pair pos (Tfunction t t0 c as t') as p) => @None (prod Z type) | Some (pair pos (Tstruct id a as t') as p) => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type (Z.add pos match Ctypes.field_offset (@cenv_cs cs) i (co_members (@get_co cs id)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) | UnionField i => @None (prod Z type) end | Some (pair pos (Tunion id a as t') as p) => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => @None (prod Z type) | UnionField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type pos match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) end | None => @None (prod Z type) end with | Some (pair pos t as p) => pos | None => Z0 end (Z.add match nested_field_rec t gfs with | Some (pair pos t as p) => pos | None => Z0 end (gfield_offset match nested_field_rec t gfs with | Some (pair z t0 as p) => t0 | None => Tvoid end gf)) *)
  destruct (nested_field_rec t gfs) as [[ofs0 t0] |] eqn:NFR; [| reflexivity].
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
  destruct t0 as [| | | | | | | id ? | id ?]; destruct gf; try reflexivity.
  + destruct_in_members i (co_members (get_co id)).
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    - reflexivity.
    - unfold gfield_type.
(* Goal: @eq bool (@nested_pred cs atom_pred (field_type i (co_members (@get_co cs id)))) true *)
      rewrite not_in_members_field_type; auto.
  + destruct_in_members i (co_members (get_co id)).
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    - reflexivity.
    - unfold gfield_type.
(* Goal: @eq bool (@nested_pred cs atom_pred (field_type i (co_members (@get_co cs id)))) true *)
      rewrite not_in_members_field_type; auto.
Defined.

Lemma nested_field_offset_ind: forall t gfs,
  legal_nested_field0 t gfs ->
  nested_field_offset t gfs =
  match gfs with
  | nil => 0
  | gf :: gfs0 => nested_field_offset t gfs0 + gfield_offset (nested_field_type t gfs0) gf
  end.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t gfs) match gfs with | nil => Z0 | cons gf gfs0 => Z.add (nested_field_offset t gfs0) (gfield_offset (nested_field_type t gfs0) gf) end *)
  destruct gfs as [| gf gfs]; [reflexivity |].
(* Goal: P *)
  destruct H.
(* Goal: @eq Z (nested_field_offset t (@cons gfield gf gfs)) (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf)) *)
  unfold nested_field_type, nested_field_offset in *.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  simpl.
(* Goal: @eq Z match match nested_field_rec t gfs with | Some (pair pos (Tvoid as t') as p) => @None (prod Z type) | Some (pair pos (Tint i s a as t') as p) => @None (prod Z type) | Some (pair pos (Tlong s a as t') as p) => @None (prod Z type) | Some (pair pos (Tfloat f a as t') as p) => @None (prod Z type) | Some (pair pos (Tpointer t a as t') as p) => @None (prod Z type) | Some (pair pos (Tarray t'' n a as t') as p) => match gf with | ArraySubsc i => @Some (prod Z type) (@pair Z type (Z.add pos (Z.mul (@sizeof (@cenv_cs cs) t'') i)) t'') | StructField i => @None (prod Z type) | UnionField i => @None (prod Z type) end | Some (pair pos (Tfunction t t0 c as t') as p) => @None (prod Z type) | Some (pair pos (Tstruct id a as t') as p) => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type (Z.add pos match Ctypes.field_offset (@cenv_cs cs) i (co_members (@get_co cs id)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) | UnionField i => @None (prod Z type) end | Some (pair pos (Tunion id a as t') as p) => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => @None (prod Z type) | UnionField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type pos match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) end | None => @None (prod Z type) end with | Some (pair pos t as p) => pos | None => Z0 end (Z.add match nested_field_rec t gfs with | Some (pair pos t as p) => pos | None => Z0 end (gfield_offset match nested_field_rec t gfs with | Some (pair z t0 as p) => t0 | None => Tvoid end gf)) *)
  destruct (nested_field_rec t gfs) as [[ofs0 t0] |] eqn:NFR; [| reflexivity].
(* Goal: @eq Z match match t0 with | Tvoid => @None (prod Z type) | Tint i s a => @None (prod Z type) | Tlong s a => @None (prod Z type) | Tfloat f a => @None (prod Z type) | Tpointer t a => @None (prod Z type) | Tarray t'' n a => match gf with | ArraySubsc i => @Some (prod Z type) (@pair Z type (Z.add ofs0 (Z.mul (@sizeof (@cenv_cs cs) t'') i)) t'') | StructField i => @None (prod Z type) | UnionField i => @None (prod Z type) end | Tfunction t t0 c => @None (prod Z type) | Tstruct id a => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type (Z.add ofs0 match Ctypes.field_offset (@cenv_cs cs) i (co_members (@get_co cs id)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) | UnionField i => @None (prod Z type) end | Tunion id a => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => @None (prod Z type) | UnionField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type ofs0 match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) end end with | Some (pair pos t as p) => pos | None => Z0 end (Z.add ofs0 (gfield_offset t0 gf)) *)
  destruct t0 as [| | | | | | | id ? | id ?]; destruct gf; try inversion H0; auto.
  + destruct_in_members i (co_members (get_co id)); [| tauto].
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    reflexivity.
  + destruct_in_members i (co_members (get_co id)); [| tauto].
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
    simpl. omega.
Qed.

Lemma nested_field_offset_ind': forall t gfs,
  legal_nested_field t gfs ->
  nested_field_offset t gfs =
  match gfs with
  | nil => 0
  | gf :: gfs0 => nested_field_offset t gfs0 + gfield_offset (nested_field_type t gfs0) gf
  end.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t gfs) match gfs with | nil => Z0 | cons gf gfs0 => Z.add (nested_field_offset t gfs0) (gfield_offset (nested_field_type t gfs0) gf) end *)
  destruct gfs as [| gf gfs]; [reflexivity |].
(* Goal: P *)
  destruct H.
(* Goal: @eq Z (nested_field_offset t (@cons gfield gf gfs)) (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf)) *)
  unfold nested_field_type, nested_field_offset in *.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  simpl.
(* Goal: @eq Z match match nested_field_rec t gfs with | Some (pair pos (Tvoid as t') as p) => @None (prod Z type) | Some (pair pos (Tint i s a as t') as p) => @None (prod Z type) | Some (pair pos (Tlong s a as t') as p) => @None (prod Z type) | Some (pair pos (Tfloat f a as t') as p) => @None (prod Z type) | Some (pair pos (Tpointer t a as t') as p) => @None (prod Z type) | Some (pair pos (Tarray t'' n a as t') as p) => match gf with | ArraySubsc i => @Some (prod Z type) (@pair Z type (Z.add pos (Z.mul (@sizeof (@cenv_cs cs) t'') i)) t'') | StructField i => @None (prod Z type) | UnionField i => @None (prod Z type) end | Some (pair pos (Tfunction t t0 c as t') as p) => @None (prod Z type) | Some (pair pos (Tstruct id a as t') as p) => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type (Z.add pos match Ctypes.field_offset (@cenv_cs cs) i (co_members (@get_co cs id)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) | UnionField i => @None (prod Z type) end | Some (pair pos (Tunion id a as t') as p) => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => @None (prod Z type) | UnionField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type pos match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) end | None => @None (prod Z type) end with | Some (pair pos t as p) => pos | None => Z0 end (Z.add match nested_field_rec t gfs with | Some (pair pos t as p) => pos | None => Z0 end (gfield_offset match nested_field_rec t gfs with | Some (pair z t0 as p) => t0 | None => Tvoid end gf)) *)
  destruct (nested_field_rec t gfs) as [[ofs0 t0] |] eqn:NFR; [| reflexivity].
(* Goal: @eq Z match match t0 with | Tvoid => @None (prod Z type) | Tint i s a => @None (prod Z type) | Tlong s a => @None (prod Z type) | Tfloat f a => @None (prod Z type) | Tpointer t a => @None (prod Z type) | Tarray t'' n a => match gf with | ArraySubsc i => @Some (prod Z type) (@pair Z type (Z.add ofs0 (Z.mul (@sizeof (@cenv_cs cs) t'') i)) t'') | StructField i => @None (prod Z type) | UnionField i => @None (prod Z type) end | Tfunction t t0 c => @None (prod Z type) | Tstruct id a => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type (Z.add ofs0 match Ctypes.field_offset (@cenv_cs cs) i (co_members (@get_co cs id)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) | UnionField i => @None (prod Z type) end | Tunion id a => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => @None (prod Z type) | UnionField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type ofs0 match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) end end with | Some (pair pos t as p) => pos | None => Z0 end (Z.add ofs0 (gfield_offset t0 gf)) *)
  destruct t0 as [| | | | | | | id ? | id ?]; destruct gf; try inversion H0; auto.
  + destruct_in_members i (co_members (get_co id)); [| tauto].
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    reflexivity.
  + destruct_in_members i (co_members (get_co id)); [| tauto].
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
    simpl. omega.
Qed.

Lemma offset_val_nested_field_offset_ind: forall t gfs p,
  legal_nested_field0 t gfs ->
  offset_val (nested_field_offset t gfs) p =
  match gfs with
  | nil => force_ptr p
  | gf :: gfs0 => offset_val (gfield_offset (nested_field_type t gfs0) gf)
                    (offset_val (nested_field_offset t gfs0) p)
  end.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs)) p) *)
  rewrite nested_field_offset_ind by auto.
(* Goal: sumbool (legal_nested_field0 t gfs) (not (legal_nested_field0 t gfs)) *)
  destruct gfs as [| gf gfs].
  + fold Int.zero. rewrite offset_val_force_ptr; auto.
  + rewrite offset_offset_val.
(* Goal: @eq bool (compute_in_members i al) true *)
    auto.
Qed.

Lemma nested_field_array_type_ind: forall t gfs lo hi,
  nested_field_array_type t gfs lo hi =
  gfield_array_type (nested_field_type t gfs) lo hi.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq type (nested_field_array_type t gfs lo hi) (gfield_array_type (nested_field_type t gfs) lo hi) *)
  unfold nested_field_array_type.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t (@cons gfield gf gfs)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield gf gfs))) Ptrofs.modulus) *)
  rewrite nested_field_type_ind.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct (nested_field_type t gfs); simpl; auto.
Qed.

Lemma nested_field0_offset_ind: forall t gfs,
  legal_nested_field0 t gfs ->
  nested_field_offset t gfs =
  match gfs with
  | nil => 0
  | gf :: gfs0 => nested_field_offset t gfs0 + gfield_offset (nested_field_type t gfs0) gf
  end.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t gfs) match gfs with | nil => Z0 | cons gf gfs0 => Z.add (nested_field_offset t gfs0) (gfield_offset (nested_field_type t gfs0) gf) end *)
  destruct gfs as [| gf gfs]; [reflexivity |].
(* Goal: P *)
  destruct H.
(* Goal: @eq Z (nested_field_offset t (@cons gfield gf gfs)) (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf)) *)
  unfold nested_field_type, nested_field_offset in *.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  simpl.
(* Goal: @eq Z match match nested_field_rec t gfs with | Some (pair pos (Tvoid as t') as p) => @None (prod Z type) | Some (pair pos (Tint i s a as t') as p) => @None (prod Z type) | Some (pair pos (Tlong s a as t') as p) => @None (prod Z type) | Some (pair pos (Tfloat f a as t') as p) => @None (prod Z type) | Some (pair pos (Tpointer t a as t') as p) => @None (prod Z type) | Some (pair pos (Tarray t'' n a as t') as p) => match gf with | ArraySubsc i => @Some (prod Z type) (@pair Z type (Z.add pos (Z.mul (@sizeof (@cenv_cs cs) t'') i)) t'') | StructField i => @None (prod Z type) | UnionField i => @None (prod Z type) end | Some (pair pos (Tfunction t t0 c as t') as p) => @None (prod Z type) | Some (pair pos (Tstruct id a as t') as p) => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type (Z.add pos match Ctypes.field_offset (@cenv_cs cs) i (co_members (@get_co cs id)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) | UnionField i => @None (prod Z type) end | Some (pair pos (Tunion id a as t') as p) => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => @None (prod Z type) | UnionField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type pos match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) end | None => @None (prod Z type) end with | Some (pair pos t as p) => pos | None => Z0 end (Z.add match nested_field_rec t gfs with | Some (pair pos t as p) => pos | None => Z0 end (gfield_offset match nested_field_rec t gfs with | Some (pair z t0 as p) => t0 | None => Tvoid end gf)) *)
  destruct (nested_field_rec t gfs) as [[ofs0 t0] |] eqn:NFR; [| reflexivity].
(* Goal: @eq Z match match t0 with | Tvoid => @None (prod Z type) | Tint i s a => @None (prod Z type) | Tlong s a => @None (prod Z type) | Tfloat f a => @None (prod Z type) | Tpointer t a => @None (prod Z type) | Tarray t'' n a => match gf with | ArraySubsc i => @Some (prod Z type) (@pair Z type (Z.add ofs0 (Z.mul (@sizeof (@cenv_cs cs) t'') i)) t'') | StructField i => @None (prod Z type) | UnionField i => @None (prod Z type) end | Tfunction t t0 c => @None (prod Z type) | Tstruct id a => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type (Z.add ofs0 match Ctypes.field_offset (@cenv_cs cs) i (co_members (@get_co cs id)) with | Errors.OK ofs => ofs | Errors.Error e => Z0 end) match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) | UnionField i => @None (prod Z type) end | Tunion id a => match gf with | ArraySubsc i => @None (prod Z type) | StructField i => @None (prod Z type) | UnionField i => if compute_in_members i (co_members (@get_co cs id)) then @Some (prod Z type) (@pair Z type ofs0 match Ctypes.field_type i (co_members (@get_co cs id)) with | Errors.OK t => t | Errors.Error e => Tvoid end) else @None (prod Z type) end end with | Some (pair pos t as p) => pos | None => Z0 end (Z.add ofs0 (gfield_offset t0 gf)) *)
  destruct t0 as [| | | | | | | id ? | id ?]; destruct gf; try inversion H0; auto.
  + destruct_in_members i (co_members (get_co id)); [| tauto].
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    reflexivity.
  + destruct_in_members i (co_members (get_co id)); [| tauto].
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
    simpl. omega.
Qed.

Ltac valid_nested_field_rec f a T :=
  let H := fresh "H" in
  let t := fresh "t" in
  let ofs := fresh "ofs" in
  simpl in T; destruct (nested_field_rec f a) as [[ofs t]|] eqn:H; [|inversion T].

Ltac auto_destruct_above_line :=
repeat (
  let H1 := fresh "H" in
  let H2 := fresh "H" in
  let x := fresh "x" in
  match goal with
  | H: _ /\ _ |- _ => destruct H as [H1 H2]
  | H: prod _ _ |- _ => destruct H as [H1 H2]
  | H: @ex _ _ |- _ => destruct H as [x H1]
  | H: sigT _ |- _ => destruct H as [x H1]
  end).
(*
Lemma legal_nested_field_nested_field_rec_None_conflict: forall t gfs P,
  legal_nested_field t gfs ->
  nested_field_rec t gfs = None ->
  P.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  unfold legal_nested_field in H.
  rewrite H0 in H.
(* Goal: field_compatible (nested_field_type t_root gfsA) (@nil gfield) (field_address t_root gfsA a) *)
  simpl in H.
(* Goal: @eq bool (compute_in_members i al) true *)
  tauto.
Qed.

Lemma nested_field_rec_cons_eq_Some_lemma: forall t gf gfs ofs0 t0,
  nested_field_rec t (gf :: gfs) = Some (ofs0, t0)
  <->
  match gf, nested_field_rec t gfs with
  | ArraySubsc i0, Some (ofs, Tarray t1 n a) =>
      ofs0 = ofs + sizeof t0 * i0 /\ t0 = t1
  | StructField i, Some (ofs, Tstruct id a) =>
      in_members i (co_members (get_co id)) /\ co_su (get_co id) = Struct /\ t0 = field_type2 i (co_members (get_co id)) /\ ofs0 = ofs + field_offset2 cenv_cs i (co_members (get_co id))
  | UnionField i, Some (ofs, Tunion id a) =>
      in_members i (co_members (get_co id)) /\ co_su (get_co id) = Union /\ t0 = field_type2 i (co_members (get_co id)) /\ ofs0 = ofs
  | _, _ => False
  end.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  simpl (nested_field_rec t (gf :: gfs)).
  unfold nested_field_type2.
  destruct (nested_field_rec t gfs) as [[? tt]| ]; [destruct tt |]; destruct gf;
  (split; intro H; auto_destruct_above_line);
  try solve[inversion H | inversion H0 | inversion H1 | inversion H2].
  + inversion H; subst.
(* Goal: @eq bool (compute_in_members i al) true *)
    auto.
  + subst. auto.
  + unfold destruct (cenv_cs ! i); [| inversion H].
    destruct (co_su c); [| inversion H].
    destruct_in_members i0 (co_members c); [| inversion H].
    inversion H.
(* Goal: @eq bool (compute_in_members i al) true *)
    auto.
  + destruct (cenv_cs ! i); [| inversion H].
    auto_destruct_above_line.
    apply compute_in_members_true_iff in H0.
    rewrite H, H0.
(* Goal: @eq bool (compute_in_members i al) true *)
    subst; auto.
  + destruct (cenv_cs ! i); [| inversion H].
    destruct (co_su c); [inversion H |].
    destruct_in_members i0 (co_members c); [| inversion H].
    inversion H.
(* Goal: @eq bool (compute_in_members i al) true *)
    auto.
  + destruct (cenv_cs ! i); [| inversion H].
    auto_destruct_above_line.
    apply compute_in_members_true_iff in H0.
    rewrite H, H0.
(* Goal: @eq bool (compute_in_members i al) true *)
    subst; auto.
Qed.

Ltac solve_legal_nested_field_cons H :=
  let HH := fresh "HH" in
  let Heq := fresh "Heq" in
  let HeqNFT := fresh "Heq" in
  let H1 := fresh "H" in
  let H2 := fresh "H" in
  let H3 := fresh "H" in
  let id := fresh "id" in
  let co := fresh "co" in
  let CO := fresh "CO" in
  match type of H with
  | (legal_nested_field ?T (?A :: ?GFS)) =>
    destruct (legal_nested_field_cons_lemma T A GFS) as [HH _];
    specialize (HH H);
    destruct A eqn:Heq;
    destruct (nested_field_type2 T GFS) as [ | | | | | | | id ? | id ? ] eqn:HeqNFT;
    try solve [destruct HH as [_ HH]; inversion HH]
  end;
  [try solve [inversion Heq]; destruct HH as [H1 H2]
  |try solve [inversion Heq]; destruct HH as [H1 H2];
   destruct (cenv_cs ! id) as [co |] eqn:CO; [| inversion H2];
   destruct H2 as [H2 H3]
  |try solve [inversion Heq]; destruct HH as [H1 H2];
   destruct (cenv_cs ! id) as [co |] eqn:CO; [| inversion H2];
   destruct H2 as [H2 H3]].

Ltac solve_nested_field_rec_cons_eq_Some H :=
  let HH := fresh "HH" in
  let HeqA := fresh "Heq" in
  let HeqNFT := fresh "Heq" in
  let H1 := fresh "H" in
  let H2 := fresh "H" in
  let H3 := fresh "H" in
  let H4 := fresh "H" in
  let ofs := fresh "ofs" in
  let id := fresh "id" in
  let co := fresh "co" in
  let CO := fresh "CO" in
  match type of H with
  | (nested_field_rec ?T (?A :: ?GFS) = Some (?OFS, ?T0)) =>
    destruct (nested_field_rec_cons_eq_Some_lemma T A GFS OFS T0) as [HH _];
    specialize (HH H);
    destruct A eqn:HeqA;
    destruct (nested_field_rec T GFS) as [[ofs [ | | | | | | | id ? | id ? ]]|] eqn:HeqNFT;
    try solve [inversion HH]
  end;
  [try solve [inversion HeqA]; destruct HH as [H1 H2]
  |try solve [inversion HeqA]; destruct (cenv_cs ! id) as [co |] eqn:CO; [| inversion HH];
   destruct HH as [H1 [H2 [H3 H4]]]
  |try solve [inversion HeqA]; destruct (cenv_cs ! id) as [co |] eqn:CO; [| inversion HH];
   destruct HH as [H1 [H2 [H3 H4]]]].

Ltac solve_legal_nested_field :=
  first [
   solve [apply legal_nested_field_nil_lemma]
  | apply legal_nested_field_cons_lemma; simpl;
    split; [solve_legal_nested_field | auto]].

Global Opaque legal_nested_field.
*)

Definition legal_nested_field_dec: forall t gfs,
  {legal_nested_field t gfs} + {~ legal_nested_field t gfs}.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: sumbool (legal_nested_field t gfs) (not (legal_nested_field t gfs)) *)
  induction gfs.
  + left. exact I.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  + simpl.
(* Goal: sumbool (and (legal_nested_field t gfs) (legal_field (nested_field_type t gfs) a)) (not (and (legal_nested_field t gfs) (legal_field (nested_field_type t gfs) a))) *)
    apply sumbool_dec_and; [auto |].
    destruct a, (nested_field_type t gfs) as [| | | | | | | id ? | id ?]; try solve [right; tauto];
    unfold legal_field.
    - apply sumbool_dec_and; [apply Z_le_dec | apply Z_lt_dec].
    - destruct_in_members i (co_members (get_co id)); auto.
    - destruct_in_members i (co_members (get_co id)); auto.
Qed.

Definition legal_nested_field0_dec: forall t gfs,
  {legal_nested_field0 t gfs} + {~ legal_nested_field0 t gfs}.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: sumbool (legal_nested_field0 t gfs) (not (legal_nested_field0 t gfs)) *)
  destruct gfs as [| gf gfs].
  + left. exact I.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  + simpl.
(* Goal: sumbool (and (legal_nested_field t gfs) (legal_field0 (nested_field_type t gfs) gf)) (not (and (legal_nested_field t gfs) (legal_field0 (nested_field_type t gfs) gf))) *)
    apply sumbool_dec_and; [apply legal_nested_field_dec |].
    destruct gf, (nested_field_type t gfs) as [| | | | | | | id ? | id ?]; try solve [right; tauto];
    unfold legal_field0.
    - apply sumbool_dec_and; [apply Z_le_dec | apply Z_le_dec].
    - destruct_in_members i (co_members (get_co id)); auto.
    - destruct_in_members i (co_members (get_co id)); auto.
Qed.

Definition field_compatible t gfs p :=
  isptr p /\
  complete_legal_cosu_type t = true /\
  size_compatible t p /\
  align_compatible t p /\
  legal_nested_field t gfs.

Definition field_compatible0 t gfs p :=
  isptr p /\
  complete_legal_cosu_type t = true /\
  size_compatible t p /\
  align_compatible t p /\
  legal_nested_field0 t gfs.

Lemma field_compatible_dec: forall t gfs p,
  {field_compatible t gfs p} + {~ field_compatible t gfs p}.
Proof.
(* Goal: iff (@field_compatible cs_from t gfs p) (@field_compatible cs_to t gfs p) *)
  unfold field_compatible.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: sumbool (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field0 t gfs))))) (not (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field0 t gfs)))))) *)
  repeat apply sumbool_dec_and.
  + destruct p; simpl; try (left; tauto); try (right; tauto).
  + destruct complete_legal_cosu_type; [left | right]; congruence.
  + destruct p; simpl; try solve [left; auto].
    destruct (zlt (Ptrofs.unsigned i + sizeof t) Ptrofs.modulus); [left | right]; omega.
  + apply align_compatible_dec.
  + apply legal_nested_field_dec.
Qed.

Lemma field_compatible0_dec: forall t gfs p,
  {field_compatible0 t gfs p} + {~ field_compatible0 t gfs p}.
Proof.
(* Goal: forall (t : type) (gfs : list gfield) (p : val), sumbool (field_compatible0 t gfs p) (not (field_compatible0 t gfs p)) *)
  unfold field_compatible0.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: sumbool (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field0 t gfs))))) (not (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field0 t gfs)))))) *)
  repeat apply sumbool_dec_and.
  + destruct p; simpl; try (left; tauto); try (right; tauto).
  + destruct complete_legal_cosu_type; [left | right]; congruence.
  + destruct p; simpl; try solve [left; auto].
    destruct (zlt (Ptrofs.unsigned i + sizeof t) Ptrofs.modulus); [left | right]; omega.
  + apply align_compatible_dec.
  + apply legal_nested_field0_dec.
Qed.

Lemma field_compatible_cons: forall t gf gfs p,
  field_compatible t (gf :: gfs) p <->
  match nested_field_type t gfs, gf with
  | Tstruct id _, StructField i => in_members i (co_members (get_co id)) /\ field_compatible t gfs p
  | Tunion id _, UnionField i => in_members i (co_members (get_co id)) /\ field_compatible t gfs p
  | Tarray _ n _, ArraySubsc i => 0 <= i < n /\ field_compatible t gfs p
  | _, _ => False
  end.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: iff (@field_compatible cs_from t gfs p) (@field_compatible cs_to t gfs p) *)
  unfold field_compatible.
(* Goal: iff (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field t (@cons gfield gf gfs)))))) match nested_field_type t gfs with | Tvoid => False | Tint i s a => False | Tlong s a => False | Tfloat f a => False | Tpointer t a => False | Tarray t0 n a => match gf with | ArraySubsc i => and (and (Z.le Z0 i) (Z.lt i n)) (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field t gfs))))) | StructField i => False | UnionField i => False end | Tfunction t t0 c => False | Tstruct id a => match gf with | ArraySubsc i => False | StructField i => and (in_members i (co_members (@get_co cs id))) (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field t gfs))))) | UnionField i => False end | Tunion id a => match gf with | ArraySubsc i => False | StructField i => False | UnionField i => and (in_members i (co_members (@get_co cs id))) (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field t gfs))))) end end *)
  simpl (legal_nested_field t (gf :: gfs)).
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct (nested_field_type t gfs), gf; simpl; tauto.
Qed.

Lemma field_compatible0_cons: forall t gf gfs p,
  field_compatible0 t (gf :: gfs) p <->
  match nested_field_type t gfs, gf with
  | Tstruct id _, StructField i => in_members i (co_members (get_co id)) /\ field_compatible t gfs p
  | Tunion id _, UnionField i => in_members i (co_members (get_co id)) /\ field_compatible t gfs p
  | Tarray _ n _, ArraySubsc i => 0 <= i <= n /\ field_compatible t gfs p
  | _, _ => False
  end.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: iff (field_compatible0 t (@cons gfield gf gfs) p) match nested_field_type t gfs with | Tvoid => False | Tint i s a => False | Tlong s a => False | Tfloat f a => False | Tpointer t a => False | Tarray t0 n a => match gf with | ArraySubsc i => and (and (Z.le Z0 i) (Z.le i n)) (field_compatible t gfs p) | StructField i => False | UnionField i => False end | Tfunction t t0 c => False | Tstruct id a => match gf with | ArraySubsc i => False | StructField i => and (in_members i (co_members (@get_co cs id))) (field_compatible t gfs p) | UnionField i => False end | Tunion id a => match gf with | ArraySubsc i => False | StructField i => False | UnionField i => and (in_members i (co_members (@get_co cs id))) (field_compatible t gfs p) end end *)
  unfold field_compatible, field_compatible0.
(* Goal: iff (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field0 t (@cons gfield gf gfs)))))) match nested_field_type t gfs with | Tvoid => False | Tint i s a => False | Tlong s a => False | Tfloat f a => False | Tpointer t a => False | Tarray t0 n a => match gf with | ArraySubsc i => and (and (Z.le Z0 i) (Z.le i n)) (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field t gfs))))) | StructField i => False | UnionField i => False end | Tfunction t t0 c => False | Tstruct id a => match gf with | ArraySubsc i => False | StructField i => and (in_members i (co_members (@get_co cs id))) (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field t gfs))))) | UnionField i => False end | Tunion id a => match gf with | ArraySubsc i => False | StructField i => False | UnionField i => and (in_members i (co_members (@get_co cs id))) (and (isptr p) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t) true) (and (@size_compatible cs t p) (and (@align_compatible cs t p) (legal_nested_field t gfs))))) end end *)
  simpl (legal_nested_field0 t (gf :: gfs)).
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct (nested_field_type t gfs), gf; simpl; tauto.
Qed.

(* The following two lemmas is covered by the previous two. Delete them some time. *)
Lemma field_compatible_cons_Tarray:
  forall i t t0 n a gfs p,
  nested_field_type t gfs = Tarray t0 n a ->
  field_compatible t gfs p ->
  (0 <= i < n)%Z ->
  field_compatible t (ArraySubsc i :: gfs) p.
Proof.
(* Goal: forall (i : Z) (t t0 : type) (n : Z) (a : attr) (gfs : list gfield) (p : val) (_ : @eq type (nested_field_type t gfs) (Tarray t0 n a)) (_ : field_compatible t gfs p) (_ : and (Z.le Z0 i) (Z.lt i n)), field_compatible t (@cons gfield (ArraySubsc i) gfs) p *)
unfold field_compatible; intros; intuition.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
simpl.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned i) (@sizeof (@cenv_cs cs) t)) Ptrofs.modulus *)
rewrite H.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
simpl.
(* Goal: @eq bool (compute_in_members i al) true *)
auto.
Qed.

Lemma field_compatible0_cons_Tarray:
  forall k t n a gfs p t',
  nested_field_type t gfs = Tarray t' n a ->
  field_compatible t gfs p ->
  (0 <= k <= n)%Z ->
  field_compatible0 t (ArraySubsc k :: gfs) p.
Proof.
(* Goal: forall (k : Z) (t : type) (n : Z) (a : attr) (gfs : list gfield) (p : val) (t' : type) (_ : @eq type (nested_field_type t gfs) (Tarray t' n a)) (_ : field_compatible t gfs p) (_ : and (Z.le Z0 k) (Z.le k n)), field_compatible0 t (@cons gfield (ArraySubsc k) gfs) p *)
unfold field_compatible, field_compatible0; intros; intuition.
(* Goal: legal_nested_field0 t (@cons gfield (ArraySubsc k) gfs) *)
unfold legal_nested_field0.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned i) (@sizeof (@cenv_cs cs) t)) Ptrofs.modulus *)
rewrite H.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
simpl.
(* Goal: @eq bool (compute_in_members i al) true *)
auto.
Qed.

Definition field_address t gfs p :=
  if (field_compatible_dec t gfs p)
  then offset_val (nested_field_offset t gfs) p
  else Vundef.

Definition field_address0 t gfs p :=
  if (field_compatible0_dec t gfs p)
  then offset_val (nested_field_offset t gfs) p
  else Vundef.

Lemma field_address_isptr:
  forall t path c, field_compatible t path c -> isptr (field_address t path c).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  unfold field_address. rewrite if_true by auto.
(* Goal: isptr (offset_val (nested_field_offset t path) c) *)
  destruct H as [? _].
(* Goal: isptr (offset_val (nested_field_offset t path) c) *)
  normalize.
Qed.

Lemma field_address0_isptr:
  forall t path c, field_compatible0 t path c -> isptr (field_address0 t path c).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  unfold field_address0. rewrite if_true by auto.
(* Goal: isptr (offset_val (nested_field_offset t path) c) *)
  destruct H as [? _].
(* Goal: isptr (offset_val (nested_field_offset t path) c) *)
  normalize.
Qed.

Lemma field_address_clarify:
 forall t path c,
   is_pointer_or_null (field_address t path c) ->
   field_address t path c = offset_val (nested_field_offset t path) c.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros. unfold field_address in *.
(* Goal: @eq val (if field_compatible0_dec t path c then offset_val (nested_field_offset t path) c else Vundef) (offset_val (nested_field_offset t path) c) *)
  if_tac; try contradiction.
(* Goal: @eq bool (compute_in_members i al) true *)
  auto.
Qed.

Lemma field_address0_clarify:
 forall t path c,
   is_pointer_or_null (field_address0 t path c) ->
   field_address0 t path c = offset_val (nested_field_offset t path) c.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
 intros. unfold field_address0 in *.
(* Goal: @eq val (if field_compatible0_dec t path c then offset_val (nested_field_offset t path) c else Vundef) (offset_val (nested_field_offset t path) c) *)
  if_tac; try contradiction.
(* Goal: @eq bool (compute_in_members i al) true *)
  auto.
Qed.

Lemma field_compatible_field_compatible0:
  forall (t : type) (gfs : list gfield) (p : val),
  field_compatible t gfs p -> field_compatible0 t gfs p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: field_compatible0 t gfs p *)
  destruct gfs as [| gf gfs]; [auto |].
(* Goal: field_compatible0 t (@cons gfield gf gfs) p *)
  rewrite field_compatible0_cons.
(* Goal: match nested_field_type t gfs with | Tvoid => False | Tint i s a => False | Tlong s a => False | Tfloat f a => False | Tpointer t a => False | Tarray t0 n a => match gf with | ArraySubsc i => and (and (Z.le Z0 i) (Z.le i n)) (field_compatible t gfs p) | StructField i => False | UnionField i => False end | Tfunction t t0 c => False | Tstruct id a => match gf with | ArraySubsc i => False | StructField i => and (in_members i (co_members (@get_co cs id))) (field_compatible t gfs p) | UnionField i => False end | Tunion id a => match gf with | ArraySubsc i => False | StructField i => False | UnionField i => and (in_members i (co_members (@get_co cs id))) (field_compatible t gfs p) end end *)
  rewrite field_compatible_cons in H.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct (nested_field_type t gfs), gf; try tauto.
(* Goal: and (and (Z.le Z0 i) (Z.le i z)) (field_compatible t gfs p) *)
  split; [| tauto].
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  omega.
Qed.

Lemma field_compatible_field_compatible0':
  forall (t : type) (i : Z) (gfs : list gfield) (p : val),
  field_compatible t (ArraySubsc i :: gfs) p <->
  field_compatible0 t (ArraySubsc i :: gfs) p /\
  field_compatible0 t (ArraySubsc (i + 1) :: gfs) p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: iff (field_compatible t (@cons gfield (ArraySubsc i) gfs) p) (and (field_compatible0 t (@cons gfield (ArraySubsc i) gfs) p) (field_compatible0 t (@cons gfield (ArraySubsc (Z.add i (Zpos xH))) gfs) p)) *)
  rewrite !field_compatible0_cons.
(* Goal: iff (field_compatible t (@cons gfield (ArraySubsc i) gfs) p) (and match nested_field_type t gfs with | Tvoid => False | Tint i s a => False | Tlong s a => False | Tfloat f a => False | Tpointer t a => False | Tarray t0 n a => and (and (Z.le Z0 i) (Z.le i n)) (field_compatible t gfs p) | Tfunction t t0 c => False | Tstruct id a => False | Tunion id a => False end match nested_field_type t gfs with | Tvoid => False | Tint i s a => False | Tlong s a => False | Tfloat f a => False | Tpointer t a => False | Tarray t0 n a => and (and (Z.le Z0 (Z.add i (Zpos xH))) (Z.le (Z.add i (Zpos xH)) n)) (field_compatible t gfs p) | Tfunction t t0 c => False | Tstruct id a => False | Tunion id a => False end) *)
  rewrite field_compatible_cons.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct (nested_field_type t gfs); try tauto.
  assert (0 <= i < z <-> 0 <= i <= z /\ 0 <= i + 1 <= z) by omega.
(* Goal: @eq bool (compute_in_members i al) true *)
  tauto.
Qed.

Lemma field_compatible0_range:
 forall i lo hi t gfs p,
   lo <= i <= hi ->
   field_compatible0 t (ArraySubsc lo :: gfs) p ->
   field_compatible0 t (ArraySubsc hi :: gfs) p ->
   field_compatible0 t (ArraySubsc i :: gfs) p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: field_compatible0 t (@cons gfield (ArraySubsc i) gfs) p *)
  destruct H0 as [? [? [? [? [? ?]]]]].
(* Goal: field_compatible0 t (@cons gfield (ArraySubsc i) gfs) p *)
  destruct H1 as [? [? [? [? [? ?]]]]].
(* Goal: @eq bool (compute_in_members i al) true *)
  repeat split; auto.
  hnf in H6, H11|-*.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct (nested_field_type t gfs); auto.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  omega.
Qed.

Lemma field_compatible_range:
 forall i lo hi t gfs p,
   lo <= i < hi ->
   field_compatible0 t (ArraySubsc lo :: gfs) p ->
   field_compatible0 t (ArraySubsc hi :: gfs) p ->
   field_compatible t (ArraySubsc i :: gfs) p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: field_compatible t (@cons gfield (ArraySubsc i) gfs) p *)
  rewrite field_compatible_field_compatible0'.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  split; apply (field_compatible0_range _ lo hi); eauto; omega.
Qed.

Lemma is_pointer_or_null_field_compatible:
  forall t path c,
     is_pointer_or_null (field_address t path c) ->
      field_compatible t path c.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
 intros.
(* Goal: field_compatible t path c *)
 unfold field_address in H.
(* Goal: @eq bool (compute_in_members i al) true *)
 if_tac in H; auto. inv H.
Qed.

Lemma nested_field_type_ArraySubsc: forall t i gfs,
  nested_field_type t (ArraySubsc i :: gfs) = nested_field_type t (ArraySubsc 0 :: gfs).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq type (nested_field_type t (@cons gfield (ArraySubsc i) gfs)) (nested_field_type t (@cons gfield (ArraySubsc Z0) gfs)) *)
  rewrite !nested_field_type_ind with (gfs := _ :: gfs).
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct (nested_field_type t gfs); try tauto.
Qed.
(* TODO: not useful any longer *)
(*
Lemma gfield_type_complete_type: forall t gf,
  legal_field t gf ->
  complete_type cenv_cs t = true ->
  complete_type cenv_cs (gfield_type t gf) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  destruct t as [| | | | | | | id ? | id ?], gf; try inversion H; simpl in H0 |- *.
  + auto.
  + eapply complete_member.
    - apply in_members_field_type; auto.
    - apply co_consistent_complete.
      apply get_co_consistent.
  + eapply complete_member.
    - apply in_members_field_type; auto.
    - apply co_consistent_complete.
      apply get_co_consistent.
Qed.

Lemma gfield_array_type_complete_type: forall t lo hi,
  legal_field0 t (ArraySubsc lo) ->
  complete_type cenv_cs t = true ->
  complete_type cenv_cs (gfield_array_type t lo hi) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  destruct t as [| | | | | | | id ? | id ?]; try inversion H; simpl in H0 |- *.
(* Goal: @eq bool (compute_in_members i al) true *)
  auto.
Qed.

Lemma nested_field_type_complete_type: forall t gfs,
  legal_nested_field t gfs ->
  complete_type cenv_cs t = true ->
  complete_type cenv_cs (nested_field_type t gfs) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t (@cons gfield gf gfs)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield gf gfs))) Ptrofs.modulus) *)
  induction gfs as [| gf gfs]; rewrite nested_field_type_ind.
  + exact H0.
  + destruct H.
(* Goal: @eq bool (compute_in_members i al) true *)
    apply gfield_type_complete_type; auto.
Qed.

Lemma nested_field_array_type_complete_type: forall t gfs lo hi,
  legal_nested_field0 t (ArraySubsc lo :: gfs) ->
  complete_type cenv_cs t = true ->
  complete_type cenv_cs (nested_field_array_type t gfs lo hi) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo))) p) *)
  rewrite nested_field_array_type_ind.
  apply gfield_array_type_complete_type.
  + simpl in H; tauto.
  + apply nested_field_type_complete_type; auto.
(* Goal: @eq bool (compute_in_members i al) true *)
    simpl in H; tauto.
Qed.
*)
Lemma gfield_type_nested_pred: forall {atom_pred: type -> bool}, atom_pred Tvoid = true -> forall (t: type) (gf: gfield),
  nested_pred atom_pred t = true -> nested_pred atom_pred (gfield_type t gf) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  destruct t as [| | | | | | | id ? | id ?], gf; auto;
   unfold gfield_type in *; rewrite nested_pred_eq in H0.
  + rewrite andb_true_iff in H0.
(* Goal: @eq bool (compute_in_members i al) true *)
    tauto.
  + rewrite andb_true_iff in H0.
(* Goal: @eq bool (@nested_pred cs atom_pred (field_type i (co_members (@get_co cs id)))) true *)
    destruct_in_members i (co_members (get_co id)).
    - eapply nested_fields_pred_nested_pred; auto; tauto.
    - rewrite not_in_members_field_type; auto.
  + rewrite andb_true_iff in H0.
(* Goal: @eq bool (@nested_pred cs atom_pred (field_type i (co_members (@get_co cs id)))) true *)
    destruct_in_members i (co_members (get_co id)).
    - eapply nested_fields_pred_nested_pred; auto; tauto.
    - rewrite not_in_members_field_type; auto.
Qed.

Lemma gfield_array_type_nested_pred: forall {atom_pred: type -> bool},
  (forall t n m a,
    0 <= m ->
    atom_pred (Tarray t n a) = true ->
    atom_pred (Tarray t m (no_alignas_attr a)) = true) ->
  forall (t: type) lo hi,
  lo <= hi ->
  legal_field0 t (ArraySubsc lo) ->
  nested_pred atom_pred t = true -> nested_pred atom_pred (gfield_array_type t lo hi) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct t as [| | | | | | | id ? | id ?]; auto.
  simpl in H2 |- *; rewrite nested_pred_eq in H2 |- *.
  rewrite andb_true_iff in H2 |- *.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct H2; split; auto.
(* Goal: @eq bool (compute_in_members i al) true *)
  eapply H; eauto.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  omega.
Qed.

Lemma gfield_type_complete_legal_cosu_type: forall (t: type) (gf: gfield),
  legal_field t gf ->
  complete_legal_cosu_type t = true -> complete_legal_cosu_type (gfield_type t gf) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  destruct t as [| | | | | | | id ? | id ?], gf; auto;
  unfold gfield_type in *; simpl in H, H0; unfold get_co in *.
  + destruct (cenv_cs ! id) eqn:?H; [| inv H0].
(* Goal: @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (field_type i (co_members c))) true *)
    pose proof cenv_legal_su _ _ H1.
(* Goal: @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (field_type i (co_members c))) true *)
    unfold in_members in H.
(* Goal: @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (field_type i (co_members c))) true *)
    induction (co_members c) as [| [i0 t0] ?].
    - inv H.
    - simpl in H2; rewrite andb_true_iff in H2; destruct H2.
      simpl in H |- *.
(* Goal: @eq bool (compute_in_members i al) true *)
      if_tac; auto.
(* Goal: @eq bool (compute_in_members i al) true *)
      apply IHm; auto.
(* Goal: @In ident i (@map (prod ident type) ident (@fst ident type) m) *)
      destruct H; auto; congruence.
  + destruct (cenv_cs ! id) eqn:?H; [| inv H0].
(* Goal: @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (field_type i (co_members c))) true *)
    pose proof cenv_legal_su _ _ H1.
(* Goal: @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (field_type i (co_members c))) true *)
    unfold in_members in H.
(* Goal: @eq bool (@complete_legal_cosu_type (@cenv_cs cs) (field_type i (co_members c))) true *)
    induction (co_members c) as [| [i0 t0] ?].
    - inv H.
    - simpl in H2; rewrite andb_true_iff in H2; destruct H2.
      simpl in H |- *.
(* Goal: @eq bool (compute_in_members i al) true *)
      if_tac; auto.
(* Goal: @eq bool (compute_in_members i al) true *)
      apply IHm; auto.
(* Goal: @In ident i (@map (prod ident type) ident (@fst ident type) m) *)
      destruct H; auto; congruence.
Qed.

Lemma gfield_array_type_complete_legal_cosu_type: forall (t: type) lo hi,
  legal_field0 t (ArraySubsc lo) ->
  complete_legal_cosu_type t = true ->
  complete_legal_cosu_type (gfield_array_type t lo hi) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct t as [| | | | | | | id ? | id ?]; auto.
Qed.

Lemma nested_field_type_complete_legal_cosu_type: forall (t: type) (gfs: list gfield), complete_legal_cosu_type t = true -> legal_nested_field t gfs -> complete_legal_cosu_type (nested_field_type t gfs) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t (@cons gfield gf gfs)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield gf gfs))) Ptrofs.modulus) *)
  induction gfs; rewrite nested_field_type_ind.
  + auto.
  + destruct H0.
(* Goal: @eq bool (compute_in_members i al) true *)
    apply gfield_type_complete_legal_cosu_type; auto.
Qed.

Lemma nested_field_array_type_complete_legal_cosu_type: forall (t: type) (gfs: list gfield) lo hi, complete_legal_cosu_type t = true -> legal_nested_field0 t (ArraySubsc lo :: gfs) -> complete_legal_cosu_type (nested_field_array_type t gfs lo hi) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo))) p) *)
  rewrite nested_field_array_type_ind.
(* Goal: and (legal_nested_field t (@app gfield gfs1 gfs0)) (legal_field0 (nested_field_type (nested_field_type t gfs0) gfs1) g) *)
  simpl in H0; destruct H0.
(* Goal: @eq bool (compute_in_members i al) true *)
  apply gfield_array_type_complete_legal_cosu_type; auto.
(* Goal: @eq bool (compute_in_members i al) true *)
  apply nested_field_type_complete_legal_cosu_type; auto.
Qed.

Lemma nested_field_type_nest_pred: forall {atom_pred: type -> bool}, atom_pred Tvoid = true -> forall (t: type) (gfs: list gfield),
  nested_pred atom_pred t = true -> nested_pred atom_pred (nested_field_type t gfs) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t (@cons gfield gf gfs)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield gf gfs))) Ptrofs.modulus) *)
  induction gfs; rewrite nested_field_type_ind.
  + auto.
  + apply gfield_type_nested_pred; auto.
Qed.

Lemma nested_field_array_type_nest_pred: forall {atom_pred: type -> bool},
  atom_pred Tvoid = true ->
  (forall t n m a,
     0 <= m ->
     atom_pred (Tarray t n a) = true ->
     atom_pred (Tarray t m (no_alignas_attr a)) = true) ->
  forall (t: type) gfs lo hi,
  lo <= hi ->
  legal_nested_field0 t (ArraySubsc lo :: gfs) ->
  nested_pred atom_pred t = true ->
  nested_pred atom_pred (nested_field_array_type t gfs lo hi) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo))) p) *)
  rewrite nested_field_array_type_ind.
(* Goal: align_compatible_rec (@cenv_cs cs) (field_type i (co_members (@get_co cs i0))) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (UnionField i) gfs))) Ptrofs.modulus) *)
  simpl in H2.
(* Goal: @eq bool (@nested_pred cs atom_pred (gfield_array_type (nested_field_type t gfs) lo hi)) true *)
  apply gfield_array_type_nested_pred; [auto | auto | tauto |].
(* Goal: @eq bool (compute_in_members i al) true *)
  apply nested_field_type_nest_pred; auto.
Qed.
(*
Lemma alignof_gfield_type_divide_alignof: forall t gf,
  legal_alignas_type t = true ->
  (alignof (gfield_type t gf) | alignof t).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  destruct t as [| | | | | | | id ? | id ?], gf; try solve [simpl; apply Z.divide_1_l].
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  + simpl.
    apply legal_alignas_type_spec in H.
(* Goal: legal_nested_field t (@app gfield (@nil gfield) gfs0) *)
    exact H.
  + eapply Z.divide_trans; [| apply legal_alignas_type_Tstruct; auto].
(* Goal: @eq type (@gfield_type cs_from (Tunion i0 a) (UnionField i)) (@gfield_type cs_to (Tunion i0 a) (UnionField i)) *)
    unfold gfield_type.
(* Goal: @eq bool (@nested_pred cs atom_pred (field_type i (co_members (@get_co cs id)))) true *)
    destruct_in_members i (co_members (get_co id)).
    - apply alignof_field_type_divide_alignof; auto.
    - rewrite not_in_members_field_type by auto.
      apply Z.divide_1_l.
  + eapply Z.divide_trans; [| apply legal_alignas_type_Tunion; auto].
(* Goal: @eq type (@gfield_type cs_from (Tunion i0 a) (UnionField i)) (@gfield_type cs_to (Tunion i0 a) (UnionField i)) *)
    unfold gfield_type.
(* Goal: @eq bool (@nested_pred cs atom_pred (field_type i (co_members (@get_co cs id)))) true *)
    destruct_in_members i (co_members (get_co id)).
    - apply alignof_field_type_divide_alignof; auto.
    - rewrite not_in_members_field_type by auto.
      apply Z.divide_1_l.
Qed.

Lemma alignof_gfield_array_type_eq: forall t lo hi i,
  legal_alignas_type t = true ->
  legal_field0 t (ArraySubsc lo) ->
  alignof (gfield_array_type t lo hi) = alignof (gfield_type t (ArraySubsc i)).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  destruct t as [| | | | | | | id ? | id ?]; try solve [inversion H0].
  apply legal_alignas_type_spec in H.
Transparent alignof.
  simpl (alignof (gfield_array_type (Tarray t z a) lo hi)).
Opaque alignof.
  unfold plain_alignof in H.
  rewrite no_alignas_attr_spec.
(* Goal: @eq bool (compute_in_members i al) true *)
  auto.
Qed.

Lemma alignof_nested_field_type_divide_alignof: forall t gfs,
  legal_alignas_type t = true ->
  legal_nested_field t gfs ->
  (alignof (nested_field_type t gfs) | alignof t).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t (@cons gfield gf gfs)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield gf gfs))) Ptrofs.modulus) *)
  induction gfs; rewrite nested_field_type_ind.
  + apply Z.divide_refl.
  + specialize (IHgfs (proj1 H0)).
    eapply Z.divide_trans; [| eauto].
    apply alignof_gfield_type_divide_alignof.
(* Goal: @eq bool (compute_in_members i al) true *)
    unfold legal_alignas_type; apply nested_field_type_nest_pred; auto.
Qed.

Lemma alignof_nested_field_type_divide_alignof': forall t gfs,
  legal_alignas_type t = true ->
  legal_nested_field0 t gfs ->
  (alignof (nested_field_type t gfs) | alignof t).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t (@cons gfield gf gfs)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield gf gfs))) Ptrofs.modulus) *)
  destruct gfs; rewrite nested_field_type_ind.
  + apply Z.divide_refl.
  + simpl in H0.
    pose proof alignof_nested_field_type_divide_alignof t gfs H (proj1 H0).
    eapply Z.divide_trans; [| eauto].
    apply alignof_gfield_type_divide_alignof.
(* Goal: @eq bool (compute_in_members i al) true *)
    unfold legal_alignas_type; apply nested_field_type_nest_pred; auto.
Qed.

Lemma alignof_nested_field_array_type_eq: forall t gfs lo hi i,
  legal_alignas_type t = true ->
  legal_nested_field0 t (ArraySubsc lo :: gfs) ->
  alignof (nested_field_array_type t gfs lo hi) = alignof (nested_field_type t (ArraySubsc i :: gfs)).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t (@cons gfield gf gfs)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield gf gfs))) Ptrofs.modulus) *)
  rewrite nested_field_type_ind.
(* Goal: @align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo))) p) *)
  rewrite nested_field_array_type_ind.
(* Goal: @align_compatible cs (gfield_array_type (Tarray t0 z a) lo hi) (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (Tarray t0 z a) (ArraySubsc lo))) p) *)
  simpl in H0.
  apply alignof_gfield_array_type_eq.
  + apply nested_field_type_nest_pred; auto.
  + tauto.
Qed.

Lemma alignof_nested_field_array_type_divide_alignof: forall t gfs lo hi,
  legal_alignas_type t = true ->
  legal_nested_field0 t (ArraySubsc lo :: gfs) ->
  (alignof (nested_field_array_type t gfs lo hi) | alignof t).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  rewrite alignof_nested_field_array_type_eq with (i := lo) by auto.
(* Goal: @eq bool (compute_in_members i al) true *)
  apply alignof_nested_field_type_divide_alignof'; auto.
Qed.

Lemma gfield_offset_type_divide: forall gf t, legal_alignas_type t = true ->
  (alignof (gfield_type t gf) | gfield_offset t gf).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  pose proof H.
  destruct t as [| | | | | | | id ? | id ?], gf; try solve [simpl; apply Z.divide_0_r];
  unfold legal_alignas_type in H;
  rewrite nested_pred_eq in H;
  rewrite andb_true_iff in H;
(* Goal: P *)
  destruct H.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  + simpl.
    apply Z.divide_mul_l.
(* Goal: @eq bool (compute_in_members i al) true *)
    apply legal_alignas_type_Tarray in H0; auto.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  + simpl.
    apply field_offset_aligned.
Qed.
*)
Lemma legal_nested_field0_field:
  forall t gfs, legal_nested_field t gfs -> legal_nested_field0 t gfs.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
intros.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
revert t H; induction gfs; intros.
(* Goal: legal_nested_field0 t (@nil gfield) *)
(* Goal: legal_nested_field0 t (@cons gfield a gfs) *)
apply I.
(* Goal: @eq bool (compute_in_members i al) true *)
destruct H; split; auto.
clear - H0.
(* Goal: @eq bool (compute_in_members i al) true *)
destruct (nested_field_type t gfs); simpl in *; auto.
(* Goal: @eq bool (compute_in_members i al) true *)
destruct a; auto.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
omega.
Qed.

Hint Resolve legal_nested_field0_field.
(*
Lemma nested_field_offset_type_divide: forall gfs t,
  legal_alignas_type t = true ->
  legal_nested_field t gfs ->
  (alignof (nested_field_type t gfs) | nested_field_offset t gfs).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  induction gfs; rewrite nested_field_type_ind, nested_field_offset_ind by auto.
  + apply Z.divide_0_r.
  + simpl in H0; spec IHgfs; [tauto |].
    assert (legal_alignas_type (nested_field_type t gfs) = true) by
      (unfold legal_alignas_type; apply nested_field_type_nest_pred; auto).
    apply Z.divide_add_r.
    - eapply Z.divide_trans; [| eauto].
(* Goal: @eq bool (compute_in_members i al) true *)
      apply alignof_gfield_type_divide_alignof; auto.
    - apply gfield_offset_type_divide; auto.
Qed.

Lemma nested_field_offset_type_divide0: forall gfs t,
  legal_alignas_type t = true ->
  legal_nested_field0 t gfs ->
  (alignof (nested_field_type t gfs) | nested_field_offset t gfs).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct gfs; rewrite nested_field_type_ind, nested_field_offset_ind by auto.
  + apply Z.divide_0_r.
  + simpl in H0.
    pose proof nested_field_offset_type_divide gfs t H (proj1 H0).
    assert (legal_alignas_type (nested_field_type t gfs) = true) by
      (unfold legal_alignas_type; apply nested_field_type_nest_pred; auto).
    apply Z.divide_add_r.
    - eapply Z.divide_trans; [| eauto].
(* Goal: @eq bool (compute_in_members i al) true *)
      apply alignof_gfield_type_divide_alignof; auto.
    - apply gfield_offset_type_divide; auto.
Qed.
*)
Lemma gfield_offset_in_range: forall t gf,
  legal_field t gf ->
  complete_legal_cosu_type t = true ->
  0 <= gfield_offset t gf /\ gfield_offset t gf + sizeof (gfield_type t gf) <= sizeof t.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: and (Z.le Z0 (gfield_offset t gf)) (Z.le (gfield_offset t gf) (@sizeof (@cenv_cs cs) t)) *)
  destruct t as [| | | | | | | id ? | id ?], gf; try solve [inversion H]; simpl in H.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  + simpl. rewrite Z.max_r by omega.
    pose_size_mult cenv_cs t (0 :: i :: i + 1 :: z :: nil).
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
  + unfold gfield_type, gfield_offset.
(* Goal: and (Z.le Z0 (field_offset (@cenv_cs cs) i (co_members (@get_co cs id)))) (Z.le (field_offset (@cenv_cs cs) i (co_members (@get_co cs id))) (@sizeof (@cenv_cs cs) (Tstruct id a))) *)
    pose_sizeof_co (Tstruct id a).
(* Goal: and (Z.le Z0 (field_offset (@cenv_cs cs) i (co_members (@get_co cs id)))) (Z.le (field_offset (@cenv_cs cs) i (co_members (@get_co cs id))) (@sizeof (@cenv_cs cs) (Tstruct id a))) *)
    pose proof field_offset_in_range _ _ H.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
  + unfold gfield_type, gfield_offset.
(* Goal: and (Z.le Z0 Z0) (Z.le Z0 (@sizeof (@cenv_cs cs) (Tunion id a))) *)
    pose_sizeof_co (Tunion id a).
(* Goal: and (Z.le Z0 Z0) (Z.le Z0 (@sizeof (@cenv_cs cs) (Tunion id a))) *)
    pose proof sizeof_union_in_members _ _ H.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
Qed.

Lemma gfield_array_offset_in_range: forall t lo hi,
  legal_field0 t (ArraySubsc lo) ->
  legal_field0 t (ArraySubsc hi) ->
  complete_legal_cosu_type t = true ->
  0 <= gfield_offset t (ArraySubsc lo) /\
  gfield_offset t (ArraySubsc lo) + sizeof (gfield_array_type t lo hi) <= sizeof t.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: and (Z.le Z0 (gfield_offset t (ArraySubsc lo))) (Z.le (Z.add (gfield_offset t (ArraySubsc lo)) (@sizeof (@cenv_cs cs) (gfield_array_type t lo hi))) (@sizeof (@cenv_cs cs) t)) *)
  destruct t as [| | | | | | | id ? | id ?]; try solve [inversion H]; simpl in H.
(* Goal: align_compatible_rec (@cenv_cs cs) (gfield_type (Tarray t0 z a) (ArraySubsc i)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (ArraySubsc i) gfs))) Ptrofs.modulus) *)
  simpl in *.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  rewrite (Z.max_r 0 z) by omega.
  assert (0 <= Z.max 0 (hi - lo) <= hi) by (apply arith_aux05; omega).
  assert (0 <= lo + Z.max 0 (hi - lo) <= z) by (apply arith_aux06; omega).
  pose_size_mult cenv_cs t (0 :: Z.max 0 (hi - lo) :: hi :: nil).
  pose_size_mult cenv_cs t (0 :: lo :: lo + Z.max 0 (hi - lo) :: z :: nil).
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  omega.
Qed.

Lemma gfield0_offset_in_range: forall t gf,
  legal_field0 t gf ->
  complete_legal_cosu_type t = true ->
  0 <= gfield_offset t gf /\ gfield_offset t gf <= sizeof t.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: and (Z.le Z0 (gfield_offset t gf)) (Z.le (gfield_offset t gf) (@sizeof (@cenv_cs cs) t)) *)
  destruct t as [| | | | | | | id ? | id ?], gf; try solve [inversion H]; simpl in H.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  + simpl.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    rewrite Z.max_r by omega.
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t) i)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t) i) (Z.mul (@sizeof (@cenv_cs cs) t) z)) *)
    pose_size_mult cenv_cs t (0 :: i :: z :: nil).
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
  + unfold gfield_type, gfield_offset.
(* Goal: and (Z.le Z0 (field_offset (@cenv_cs cs) i (co_members (@get_co cs id)))) (Z.le (field_offset (@cenv_cs cs) i (co_members (@get_co cs id))) (@sizeof (@cenv_cs cs) (Tstruct id a))) *)
    pose_sizeof_co (Tstruct id a).
(* Goal: and (Z.le Z0 (field_offset (@cenv_cs cs) i (co_members (@get_co cs id)))) (Z.le (field_offset (@cenv_cs cs) i (co_members (@get_co cs id))) (@sizeof (@cenv_cs cs) (Tstruct id a))) *)
    pose proof field_offset_in_range _ _ H.
(* Goal: and (Z.le Z0 Z0) (Z.le Z0 (@sizeof (@cenv_cs cs) (Tunion id a))) *)
    pose proof sizeof_pos (field_type i (co_members (get_co id))).
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
  + unfold gfield_type, gfield_offset.
(* Goal: and (Z.le Z0 Z0) (Z.le Z0 (@sizeof (@cenv_cs cs) (Tunion id a))) *)
    pose_sizeof_co (Tunion id a).
(* Goal: and (Z.le Z0 Z0) (Z.le Z0 (@sizeof (@cenv_cs cs) (Tunion id a))) *)
    pose proof sizeof_union_in_members _ _ H.
(* Goal: and (Z.le Z0 Z0) (Z.le Z0 (@sizeof (@cenv_cs cs) (Tunion id a))) *)
    pose proof sizeof_pos (field_type i (co_members (get_co id))).
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
Qed.

Lemma nested_field_offset_in_range: forall t gfs,
  legal_nested_field t gfs ->
  complete_legal_cosu_type t = true ->
  0 <= nested_field_offset t gfs /\
  (nested_field_offset t gfs) + sizeof (nested_field_type t gfs) <= sizeof t.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  induction gfs as [| gf gfs]; rewrite nested_field_type_ind, nested_field_offset_ind by auto.
  + omega.
  + specialize (IHgfs (proj1 H)).
(* Goal: and (Z.le Z0 (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf))) (Z.le (Z.add (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf)) (@sizeof (@cenv_cs cs) (gfield_type (nested_field_type t gfs) gf))) (@sizeof (@cenv_cs cs) t)) *)
    pose proof gfield_offset_in_range (nested_field_type t gfs) gf (proj2 H).
(* Goal: P *)
    destruct H.
(* Goal: and (Z.le Z0 (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf))) (Z.le (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf)) (@sizeof (@cenv_cs cs) t)) *)
    spec H1; [apply nested_field_type_complete_legal_cosu_type; auto |].
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
Qed.

Lemma nested_field_array_offset_in_range: forall t gfs lo hi,
  legal_nested_field0 t (ArraySubsc lo :: gfs) ->
  legal_nested_field0 t (ArraySubsc hi :: gfs) ->
  complete_legal_cosu_type t = true ->
  0 <= nested_field_offset t (ArraySubsc lo :: gfs) /\
  nested_field_offset t (ArraySubsc lo :: gfs) + sizeof (nested_field_array_type t gfs lo hi) <= sizeof t.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo))) p) *)
  rewrite nested_field_array_type_ind.
(* Goal: @eq bool (compute_in_members i al) true *)
  rewrite nested_field0_offset_ind by auto.
(* Goal: and (Z.le Z0 (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo)))) (Z.le (Z.add (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo))) (@sizeof (@cenv_cs cs) (gfield_array_type (nested_field_type t gfs) lo hi))) (@sizeof (@cenv_cs cs) t)) *)
  pose proof gfield_array_offset_in_range (nested_field_type t gfs) lo hi (proj2 H) (proj2 H0).
(* Goal: and (legal_nested_field t (@app gfield gfs1 gfs0)) (legal_field0 (nested_field_type (nested_field_type t gfs0) gfs1) g) *)
  destruct H0.
(* Goal: and (Z.le Z0 (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo)))) (Z.le (Z.add (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo))) (@sizeof (@cenv_cs cs) (gfield_array_type (nested_field_type t gfs) lo hi))) (@sizeof (@cenv_cs cs) t)) *)
  spec H2; [apply nested_field_type_complete_legal_cosu_type; auto |].
(* Goal: Z.lt (Z.add (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs))) Ptrofs.modulus) (Z.mul (@sizeof (@cenv_cs cs) (nested_field_type t (@cons gfield (ArraySubsc Z0) gfs))) (Z.max Z0 (Z.sub hi lo)))) Ptrofs.modulus *)
  pose proof nested_field_offset_in_range t gfs (proj1 H) H1.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  omega.
Qed.

Lemma nested_field0_offset_in_range: forall (t : type) (gfs : list gfield),
  legal_nested_field0 t gfs ->
  complete_legal_cosu_type t = true ->
  0 <= nested_field_offset t gfs <= sizeof t.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct gfs as [| gf gfs]; rewrite nested_field0_offset_ind by auto.
  + pose proof sizeof_pos t; omega.
  + pose proof gfield0_offset_in_range (nested_field_type t gfs) gf (proj2 H).
(* Goal: P *)
    destruct H.
(* Goal: and (Z.le Z0 (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf))) (Z.le (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf)) (@sizeof (@cenv_cs cs) t)) *)
    spec H1; [apply nested_field_type_complete_legal_cosu_type; auto |].
(* Goal: and (Z.le Z0 (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf))) (Z.le (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf)) (@sizeof (@cenv_cs cs) t)) *)
    pose proof nested_field_offset_in_range t gfs.
(* Goal: and (Z.le Z0 (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf))) (Z.le (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf)) (@sizeof (@cenv_cs cs) t)) *)
    spec H3; [auto |].
(* Goal: and (Z.le Z0 (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf))) (Z.le (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf)) (@sizeof (@cenv_cs cs) t)) *)
    spec H3; [auto |].
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
Qed.

(************************************************

nested_field app

************************************************)

Lemma nested_field_type_nested_field_type: forall t gfs0 gfs1,
  nested_field_type (nested_field_type t gfs0) gfs1 = nested_field_type t (gfs1 ++ gfs0).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t (@app gfield gfs1 gfs0)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) gfs1)) *)
  induction gfs1.
  + rewrite nested_field_type_ind.
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    reflexivity.
  + rewrite nested_field_type_ind.
(* Goal: @eq Z (nested_field_offset t (@app gfield (@nil gfield) gfs0)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) (@nil gfield))) *)
    simpl app.
    rewrite nested_field_type_ind with (t := t) (gfs := a :: gfs1 ++ gfs0).
(* Goal: @eq type (gfield_type (nested_field_type (nested_field_type t gfs0) gfs1) a) (gfield_type (nested_field_type t (@app gfield gfs1 gfs0)) a) *)
    rewrite IHgfs1.
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    reflexivity.
Defined.

Lemma legal_nested_field_shrink: forall t gfs0 gfs1,
  legal_nested_field t (gfs1 ++ gfs0) -> legal_nested_field t gfs0.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t (@app gfield gfs1 gfs0)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) gfs1)) *)
  induction gfs1.
  + simpl in *; auto.
  + simpl app in H.
(* Goal: field_compatible (nested_field_type t_root gfsA) (@nil gfield) (field_address t_root gfsA a) *)
    simpl in H.
(* Goal: @eq bool (compute_in_members i al) true *)
    tauto.
Qed.

Lemma legal_nested_field0_shrink: forall t gfs0 gfs1,
  legal_nested_field0 t (gfs1 ++ gfs0) -> legal_nested_field0 t gfs0.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t (@app gfield gfs1 gfs0)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) gfs1)) *)
  destruct gfs1.
  + simpl in *; auto.
  + simpl app in H.
(* Goal: P *)
    destruct H.
(* Goal: @eq bool (compute_in_members i al) true *)
    apply legal_nested_field_shrink in H; auto.
Qed.

Lemma legal_nested_field0_shrink1: forall t gfs0 gfs1,
  gfs1 <> nil ->
  legal_nested_field0 t (gfs1 ++ gfs0) -> legal_nested_field t gfs0.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t (@app gfield gfs1 gfs0)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) gfs1)) *)
  destruct gfs1.
  + congruence.
  + simpl app in H0.
(* Goal: and (legal_nested_field t (@app gfield gfs1 gfs0)) (legal_field0 (nested_field_type (nested_field_type t gfs0) gfs1) g) *)
    destruct H0.
(* Goal: @eq bool (compute_in_members i al) true *)
    apply legal_nested_field_shrink in H0; auto.
Qed.

Lemma legal_nested_field_app: forall t gfs0 gfs1,
  legal_nested_field t (gfs1 ++ gfs0) -> legal_nested_field (nested_field_type t gfs0) gfs1.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t (@app gfield gfs1 gfs0)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) gfs1)) *)
  induction gfs1.
  + exact I.
  + simpl in H.
(* Goal: @eq Z (nested_field_offset t (@cons gfield a (@app gfield gfs1 gfs0))) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) (@cons gfield a gfs1))) *)
    specialize (IHgfs1 (proj1 H)).
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
    simpl.
(* Goal: @eq Z (Z.add (nested_field_offset t (@app gfield gfs1 gfs0)) (gfield_offset (nested_field_type t (@app gfield gfs1 gfs0)) g)) (Z.add (nested_field_offset t gfs0) (Z.add (nested_field_offset (nested_field_type t gfs0) gfs1) (gfield_offset (nested_field_type (nested_field_type t gfs0) gfs1) g))) *)
    rewrite nested_field_type_nested_field_type.
(* Goal: @eq bool (compute_in_members i al) true *)
    tauto.
Qed.

Lemma legal_nested_field0_app: forall t gfs0 gfs1,
  legal_nested_field0 t (gfs1 ++ gfs0) -> legal_nested_field0 (nested_field_type t gfs0) gfs1.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t (@app gfield gfs1 gfs0)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) gfs1)) *)
  destruct gfs1.
  + exact I.
  + simpl in H.
(* Goal: legal_nested_field0 (nested_field_type t gfs0) (@cons gfield g gfs1) *)
    pose proof legal_nested_field_app t gfs0 gfs1.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
    simpl.
(* Goal: @eq Z (Z.add (nested_field_offset t (@app gfield gfs1 gfs0)) (gfield_offset (nested_field_type t (@app gfield gfs1 gfs0)) g)) (Z.add (nested_field_offset t gfs0) (Z.add (nested_field_offset (nested_field_type t gfs0) gfs1) (gfield_offset (nested_field_type (nested_field_type t gfs0) gfs1) g))) *)
    rewrite nested_field_type_nested_field_type.
(* Goal: @eq bool (compute_in_members i al) true *)
    tauto.
Qed.

Lemma legal_nested_field_app_inv: forall t gfs0 gfs1,
  legal_nested_field t gfs0 ->
  legal_nested_field (nested_field_type t gfs0) gfs1 ->
  legal_nested_field t (gfs1 ++ gfs0).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t (@app gfield gfs1 gfs0)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) gfs1)) *)
  induction gfs1.
  + exact H.
  + simpl in *.
    rewrite <- nested_field_type_nested_field_type.
(* Goal: @eq bool (compute_in_members i al) true *)
    tauto.
Qed.

Lemma legal_nested_field0_app_inv: forall t gfs0 gfs1,
  legal_nested_field t gfs0 ->
  legal_nested_field0 (nested_field_type t gfs0) gfs1 ->
  legal_nested_field0 t (gfs1 ++ gfs0).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t (@app gfield gfs1 gfs0)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) gfs1)) *)
  destruct gfs1.
  + apply legal_nested_field0_field.
(* Goal: legal_nested_field t (@app gfield (@nil gfield) gfs0) *)
    exact H.
  + simpl in *.
    rewrite <- nested_field_type_nested_field_type.
(* Goal: and (legal_nested_field t (@app gfield gfs1 gfs0)) (legal_field0 (nested_field_type (nested_field_type t gfs0) gfs1) g) *)
    destruct H0.
(* Goal: @eq bool (compute_in_members i al) true *)
    split; auto.
(* Goal: @eq bool (compute_in_members i al) true *)
    apply legal_nested_field_app_inv; auto.
Qed.

Lemma nested_field_offset_app: forall t gfs0 gfs1,
  legal_nested_field t (gfs1 ++ gfs0) ->
  nested_field_offset t (gfs1 ++ gfs0) = nested_field_offset t gfs0 +
    nested_field_offset (nested_field_type t gfs0) gfs1.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t (@app gfield gfs1 gfs0)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) gfs1)) *)
  induction gfs1.
  + simpl app.
(* Goal: legal_nested_field0 (nested_field_type t gfs0) (@nil gfield) *)
    rewrite nested_field_offset_ind with (gfs := nil) by exact I.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
  + simpl app in *.
(* Goal: @eq Z (nested_field_offset t (@cons gfield a (@app gfield gfs1 gfs0))) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) (@cons gfield a gfs1))) *)
    specialize (IHgfs1 (proj1 H)).
    rewrite nested_field_offset_ind with (gfs := a :: gfs1 ++ gfs0) by auto.
(* Goal: @eq Z (Z.add (nested_field_offset t (@app gfield gfs1 gfs0)) (gfield_offset (nested_field_type t (@app gfield gfs1 gfs0)) a)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) (@cons gfield a gfs1))) *)
    rewrite nested_field_offset_ind with (gfs := a :: gfs1) by (apply legal_nested_field0_field; apply legal_nested_field_app; auto).
(* Goal: @eq Z (Z.add (nested_field_offset t (@app gfield gfs1 gfs0)) (gfield_offset (nested_field_type t (@app gfield gfs1 gfs0)) g)) (Z.add (nested_field_offset t gfs0) (Z.add (nested_field_offset (nested_field_type t gfs0) gfs1) (gfield_offset (nested_field_type (nested_field_type t gfs0) gfs1) g))) *)
    rewrite nested_field_type_nested_field_type.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
Qed.

Lemma nested_field_offset0_app: forall t gfs0 gfs1,
  legal_nested_field0 t (gfs1 ++ gfs0) ->
  nested_field_offset t (gfs1 ++ gfs0) = nested_field_offset t gfs0 +
    nested_field_offset (nested_field_type t gfs0) gfs1.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq Z (nested_field_offset t (@app gfield gfs1 gfs0)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) gfs1)) *)
  destruct gfs1.
  + simpl app.
(* Goal: legal_nested_field0 (nested_field_type t gfs0) (@nil gfield) *)
    rewrite nested_field_offset_ind with (gfs := nil) by exact I.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
  + simpl app in *.
    rewrite nested_field_offset_ind with (gfs := g :: gfs1 ++ gfs0) by auto.
(* Goal: @eq Z (Z.add (nested_field_offset t (@app gfield gfs1 gfs0)) (gfield_offset (nested_field_type t (@app gfield gfs1 gfs0)) g)) (Z.add (nested_field_offset t gfs0) (nested_field_offset (nested_field_type t gfs0) (@cons gfield g gfs1))) *)
    rewrite nested_field_offset_ind with (gfs := g :: gfs1) by (apply legal_nested_field0_app; auto).
(* Goal: P *)
    destruct H.
(* Goal: @eq Z (Z.add (nested_field_offset t (@app gfield gfs1 gfs0)) (gfield_offset (nested_field_type t (@app gfield gfs1 gfs0)) g)) (Z.add (nested_field_offset t gfs0) (Z.add (nested_field_offset (nested_field_type t gfs0) gfs1) (gfield_offset (nested_field_type (nested_field_type t gfs0) gfs1) g))) *)
    pose proof (nested_field_offset_app t gfs0 gfs1 H).
(* Goal: @eq Z (Z.add (nested_field_offset t (@app gfield gfs1 gfs0)) (gfield_offset (nested_field_type t (@app gfield gfs1 gfs0)) g)) (Z.add (nested_field_offset t gfs0) (Z.add (nested_field_offset (nested_field_type t gfs0) gfs1) (gfield_offset (nested_field_type (nested_field_type t gfs0) gfs1) g))) *)
    rewrite nested_field_type_nested_field_type.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
    omega.
Qed.
(*
Lemma size_1_compatible: forall t, sizeof t = 1 -> forall p, size_compatible t p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct p; simpl; auto.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned i) (@sizeof (@cenv_cs cs) t)) Ptrofs.modulus *)
  rewrite H.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned i) Z0) Ptrofs.modulus *)
  destruct (Ptrofs.unsigned_range i).
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  omega.
Qed.
*)
Lemma size_0_compatible: forall t, sizeof t = 0 -> forall p, size_compatible t p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct p; simpl; auto.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned i) (@sizeof (@cenv_cs cs) t)) Ptrofs.modulus *)
  rewrite H.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned i) Z0) Ptrofs.modulus *)
  destruct (Ptrofs.unsigned_range i).
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  omega.
Qed.
(*
Lemma align_1_compatible: forall t, alignof t = 1 -> forall p, align_compatible t p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct p; simpl; auto.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned i) (@sizeof (@cenv_cs cs) t)) Ptrofs.modulus *)
  rewrite H.
  apply Z.divide_1_l.
Qed.
*)

Lemma size_compatible_nested_field: forall t gfs p,
  legal_nested_field t gfs ->
  complete_legal_cosu_type t = true ->
  size_compatible t p ->
  size_compatible (nested_field_type t gfs) (offset_val (nested_field_offset t gfs) p).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct p; simpl; try tauto.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr (nested_field_offset t gfs)))) (@sizeof (@cenv_cs cs) (nested_field_type t gfs))) Ptrofs.modulus *)
  unfold size_compatible in H1.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs))))) (Z.mul (@sizeof (@cenv_cs cs) (nested_field_type t (@cons gfield (ArraySubsc Z0) gfs))) (Z.max Z0 (Z.sub hi lo)))) Ptrofs.modulus *)
  solve_mod_modulus.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t gfs) (Z.modulo (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) Ptrofs.modulus) *)
  inv_int i.
(* Goal: Z.lt (Z.add (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (@sizeof (@cenv_cs cs) (nested_field_type t gfs))) Ptrofs.modulus *)
  pose proof nested_field_offset_in_range t gfs H H0.
  pose proof Zmod_le (ofs + nested_field_offset t gfs) (Ptrofs.modulus).
(* Goal: Z.lt (Z.add (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (@sizeof (@cenv_cs cs) (nested_field_type t gfs))) Ptrofs.modulus *)
  spec H4; [pose proof Ptrofs.modulus_pos; omega |].
(* Goal: Z.lt (Z.add (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (@sizeof (@cenv_cs cs) (nested_field_type t gfs))) Ptrofs.modulus *)
  spec H4; [omega |].
(* Goal: Z.lt (Z.add (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (@sizeof (@cenv_cs cs) (nested_field_type t gfs))) Ptrofs.modulus *)
  pose proof nested_field_offset_in_range t gfs H H0.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  omega.
Qed.

Lemma size_compatible_nested_field_array: forall t gfs lo hi p,
  legal_nested_field0 t (ArraySubsc lo :: gfs) ->
  legal_nested_field0 t (ArraySubsc hi :: gfs) ->
  complete_legal_cosu_type t = true ->
  size_compatible t p ->
  size_compatible (nested_field_array_type t gfs lo hi)
   (offset_val (nested_field_offset t (ArraySubsc lo :: gfs)) p).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct p; simpl; try tauto.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs))))) (Z.mul (@sizeof (@cenv_cs cs) (nested_field_type t (@cons gfield (ArraySubsc Z0) gfs))) (Z.max Z0 (Z.sub hi lo)))) Ptrofs.modulus *)
  unfold size_compatible in H2.
(* Goal: Z.lt (Z.add (Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs))))) (Z.mul (@sizeof (@cenv_cs cs) (nested_field_type t (@cons gfield (ArraySubsc Z0) gfs))) (Z.max Z0 (Z.sub hi lo)))) Ptrofs.modulus *)
  solve_mod_modulus.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t gfs) (Z.modulo (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) Ptrofs.modulus) *)
  inv_int i.
(* Goal: Z.lt (Z.add (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs))) Ptrofs.modulus) (Z.mul (@sizeof (@cenv_cs cs) (nested_field_type t (@cons gfield (ArraySubsc Z0) gfs))) (Z.max Z0 (Z.sub hi lo)))) Ptrofs.modulus *)
  pose proof nested_field_array_offset_in_range t gfs lo hi H H0 H1.
  pose proof Zmod_le (ofs + nested_field_offset t (ArraySubsc lo :: gfs)) (Ptrofs.modulus).
(* Goal: Z.lt (Z.add (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs))) Ptrofs.modulus) (Z.mul (@sizeof (@cenv_cs cs) (nested_field_type t (@cons gfield (ArraySubsc Z0) gfs))) (Z.max Z0 (Z.sub hi lo)))) Ptrofs.modulus *)
  spec H5; [pose proof Ptrofs.modulus_pos; omega |].
(* Goal: Z.lt (Z.add (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs))) Ptrofs.modulus) (Z.mul (@sizeof (@cenv_cs cs) (nested_field_type t (@cons gfield (ArraySubsc Z0) gfs))) (Z.max Z0 (Z.sub hi lo)))) Ptrofs.modulus *)
  spec H5; [omega |].
(* Goal: Z.lt (Z.add (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs))) Ptrofs.modulus) (Z.mul (@sizeof (@cenv_cs cs) (nested_field_type t (@cons gfield (ArraySubsc Z0) gfs))) (Z.max Z0 (Z.sub hi lo)))) Ptrofs.modulus *)
  pose proof nested_field_offset_in_range t gfs (proj1 H) H1.
(* Goal: Z.lt (Z.add (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs))) Ptrofs.modulus) (Z.mul (@sizeof (@cenv_cs cs) (nested_field_type t (@cons gfield (ArraySubsc Z0) gfs))) (Z.max Z0 (Z.sub hi lo)))) Ptrofs.modulus *)
  simpl in H3.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  omega.
Qed.

Lemma align_compatible_nested_field: forall t gfs p,
  legal_nested_field t gfs ->
  size_compatible t p ->
  align_compatible t p ->
  complete_legal_cosu_type t = true ->
  align_compatible (nested_field_type t gfs) (offset_val (nested_field_offset t gfs) p).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros. rename H2 into Hcomplete.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct p; simpl in *; try tauto.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  unfold Ptrofs.unsigned; simpl.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  unfold Ptrofs.unsigned at 2; simpl.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t gfs) (Ptrofs.Z_mod_modulus (Z.add (Ptrofs.unsigned i) (Ptrofs.Z_mod_modulus (nested_field_offset t gfs)))) *)
  repeat rewrite Ptrofs.Z_mod_modulus_eq.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t gfs) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (nested_field_offset t gfs) Ptrofs.modulus)) Ptrofs.modulus) *)
  rewrite Zplus_mod_idemp_r.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t gfs) (Z.modulo (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) Ptrofs.modulus) *)
  inv_int i.
(* Goal: align_compatible_rec (@cenv_cs cs) (nested_field_type t gfs) (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) *)
  induction gfs as [| gf gfs].
  + rewrite nested_field_type_ind.
(* Goal: @align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs)) p) *)
    rewrite nested_field_offset_ind by auto.
(* Goal: @eq Z (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (Z.modulo (Z.add ofs (Z.add (nested_field_offset t gfs) Z0)) Ptrofs.modulus) *)
    rewrite Z.add_0_r.
(* Goal: @eq bool (compute_in_members i al) true *)
    rewrite Zmod_small by auto.
(* Goal: @eq bool (compute_in_members i al) true *)
    auto.
  + rewrite nested_field_type_ind.
(* Goal: P *)
     destruct H.
(* Goal: align_compatible_rec (@cenv_cs cs) (gfield_type (nested_field_type t gfs) gf) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield gf gfs))) Ptrofs.modulus) *)
     specialize (IHgfs H).
(* Goal: @eq Z (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add (Ptrofs.unsigned i) (Ptrofs.unsigned (Ptrofs.repr (nested_field_offset t gfs)))))) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
     destruct (nested_field_offset_in_range t gfs H Hcomplete).
(* Goal: align_compatible_rec (@cenv_cs cs) (gfield_type (nested_field_type t gfs) gf) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield gf gfs))) Ptrofs.modulus) *)
     destruct gf.
    *
(* Goal: align_compatible_rec (@cenv_cs cs) (gfield_type (nested_field_type t gfs) (UnionField i)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (UnionField i) gfs))) Ptrofs.modulus) *)
      destruct (nested_field_type t gfs) eqn:?H; try contradiction H2.
(* Goal: align_compatible_rec (@cenv_cs cs) (gfield_type (Tarray t0 z a) (ArraySubsc i)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (ArraySubsc i) gfs))) Ptrofs.modulus) *)
      simpl in *.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
      rewrite Z.max_r in H5 by omega.
(* Goal: align_compatible_rec (@cenv_cs cs) t0 (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (ArraySubsc i) gfs))) Ptrofs.modulus) *)
      rewrite nested_field_offset_ind by (split;auto; hnf; rewrite H6; omega).
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
      rewrite H6. simpl.
(* Goal: @eq bool (compute_in_members i al) true *)
     apply align_compatible_rec_Tarray_inv with (i:=i) in IHgfs; auto.
     match goal with H: align_compatible_rec _ t0 ?A |- align_compatible_rec _ t0 ?B => replace B with A; auto end.
(* Goal: @eq Z (Z.add (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) (Z.modulo (Z.add ofs (Z.add (nested_field_offset t gfs) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) Ptrofs.modulus) *)
     pose proof (sizeof_pos t).  pose proof (sizeof_pos t0).
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo))) Ptrofs.modulus) *)
     rewrite Z.add_assoc.
(* Goal: @eq Z (Z.add (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) (Z.modulo (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
     assert (Ptrofs.modulus <> 0) by computable.
     rewrite (Z.add_mod (_ + _)) by auto.
     assert (0 <= sizeof t0 * i <= sizeof t0 * z). {
           rewrite <- (Z.mul_0_r (sizeof t0)).
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
           split; apply Zmult_le_compat_l; omega.
     }
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
     rewrite (Z.mod_small (sizeof t0 * i))  by omega.
(* Goal: @eq Z (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) (Z.modulo (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
     symmetry. apply Z.mod_small.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
     rewrite Z.mod_small; omega.
   *
(* Goal: align_compatible_rec (@cenv_cs cs) (gfield_type (nested_field_type t gfs) (UnionField i)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (UnionField i) gfs))) Ptrofs.modulus) *)
      assert (H12:= nested_field_type_complete_legal_cosu_type _ _ Hcomplete H).
(* Goal: align_compatible_rec (@cenv_cs cs) (gfield_type (nested_field_type t gfs) (UnionField i)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (UnionField i) gfs))) Ptrofs.modulus) *)
      destruct (nested_field_type t gfs) eqn:?H; try contradiction H2.
(* Goal: @eq type (@gfield_type cs_from (Tunion i0 a) (UnionField i)) (@gfield_type cs_to (Tunion i0 a) (UnionField i)) *)
      unfold gfield_type.
(* Goal: align_compatible_rec (@cenv_cs cs) (field_type i (co_members (@get_co cs i0))) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (StructField i) gfs))) Ptrofs.modulus) *)
      destruct (gfield_offset_in_range (Tstruct i0 a) (StructField i) H2 H12) as [H13 H14].
(* Goal: align_compatible_rec (@cenv_cs cs) (field_type i (co_members (@get_co cs i0))) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (UnionField i) gfs))) Ptrofs.modulus) *)
      simpl in H2.
(* Goal: align_compatible_rec (@cenv_cs cs) (field_type i (co_members (@get_co cs i0))) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (StructField i) gfs))) Ptrofs.modulus) *)
      eapply align_compatible_rec_Tstruct_inv' in IHgfs; try eassumption.
      match goal with H: align_compatible_rec _ _ ?A |- align_compatible_rec _ _ ?B => replace B with A; auto end.
(* Goal: @eq Z (Z.add (@nested_field_offset cs_to t gfs) (@gfield_offset cs_from (@nested_field_type cs_from t gfs) a)) (Z.add (@nested_field_offset cs_to t gfs) (@gfield_offset cs_to (@nested_field_type cs_to t gfs) a)) *)
      clear IHgfs.
(* Goal: @eq Z (Z.add (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (StructField i) gfs))) Ptrofs.modulus) *)
      rewrite (nested_field_offset_ind _ (_ DOT _)) by (split; auto; rewrite H6; simpl; auto).
(* Goal: @eq Z (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (Z.modulo (Z.add ofs (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (UnionField i)))) Ptrofs.modulus) *)
      rewrite H6. unfold gfield_offset.
(* Goal: @eq Z (Z.add (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) (Z.modulo (Z.add ofs (Z.add (nested_field_offset t gfs) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) Ptrofs.modulus) *)
     pose proof (sizeof_pos t). pose proof (sizeof_pos (Tstruct i0 a)).
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo))) Ptrofs.modulus) *)
     rewrite Z.add_assoc.
(* Goal: @eq Z (Z.add (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) (Z.modulo (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
     assert (Ptrofs.modulus <> 0) by computable.
     rewrite (Z.add_mod (_ + _)) by auto.
     rewrite (Z.mod_small (ofs + _)) by omega.
(* Goal: @eq Z (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) (Z.modulo (Z.add (Z.add ofs (nested_field_offset t gfs)) (Z.modulo (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))) Ptrofs.modulus)) Ptrofs.modulus) *)
     pose (sizeof_pos (field_type i (co_members (get_co i0)))).
(* Goal: @eq Z (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) (Z.modulo (Z.add (Z.add ofs (nested_field_offset t gfs)) (Z.modulo (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))) Ptrofs.modulus)) Ptrofs.modulus) *)
     unfold gfield_offset in H13, H14. unfold gfield_type in H14.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
     rewrite (Z.mod_small (field_offset _ _ _)) by omega.
(* Goal: @eq Z (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) (Z.modulo (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
     symmetry. apply Z.mod_small.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
     omega.
   *
(* Goal: align_compatible_rec (@cenv_cs cs) (gfield_type (nested_field_type t gfs) (UnionField i)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (UnionField i) gfs))) Ptrofs.modulus) *)
      assert (H12:= nested_field_type_complete_legal_cosu_type _ _ Hcomplete H).
(* Goal: align_compatible_rec (@cenv_cs cs) (gfield_type (nested_field_type t gfs) (UnionField i)) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (UnionField i) gfs))) Ptrofs.modulus) *)
      destruct (nested_field_type t gfs) eqn:?H; try contradiction H2.
(* Goal: @eq type (@gfield_type cs_from (Tunion i0 a) (UnionField i)) (@gfield_type cs_to (Tunion i0 a) (UnionField i)) *)
      unfold gfield_type.
(* Goal: align_compatible_rec (@cenv_cs cs) (field_type i (co_members (@get_co cs i0))) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (UnionField i) gfs))) Ptrofs.modulus) *)
      destruct (gfield_offset_in_range (Tunion i0 a) (UnionField i) H2 H12) as [H13 H14].
(* Goal: align_compatible_rec (@cenv_cs cs) (field_type i (co_members (@get_co cs i0))) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (UnionField i) gfs))) Ptrofs.modulus) *)
      simpl in H2.
(* Goal: align_compatible_rec (@cenv_cs cs) (field_type i (co_members (@get_co cs i0))) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (UnionField i) gfs))) Ptrofs.modulus) *)
      eapply align_compatible_rec_Tunion_inv' in IHgfs; try eassumption.
      match goal with H: align_compatible_rec _ _ ?A |- align_compatible_rec _ _ ?B => replace B with A; auto end.
(* Goal: @eq Z (Z.add (@nested_field_offset cs_to t gfs) (@gfield_offset cs_from (@nested_field_type cs_from t gfs) a)) (Z.add (@nested_field_offset cs_to t gfs) (@gfield_offset cs_to (@nested_field_type cs_to t gfs) a)) *)
      clear IHgfs.
(* Goal: @eq Z (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (Z.modulo (Z.add ofs (nested_field_offset t (@cons gfield (UnionField i) gfs))) Ptrofs.modulus) *)
      rewrite (nested_field_offset_ind _ (_ UDOT _)) by (split; auto; rewrite H6; simpl; auto).
(* Goal: @eq Z (Z.modulo (Z.add ofs (nested_field_offset t gfs)) Ptrofs.modulus) (Z.modulo (Z.add ofs (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (UnionField i)))) Ptrofs.modulus) *)
      rewrite H6. unfold gfield_offset.
(* Goal: @eq bool (compute_in_members i al) true *)
      rewrite Z.add_0_r. auto.
Qed.

Lemma align_compatible_nested_field_array: forall t gfs lo hi p,
  legal_nested_field0 t (ArraySubsc lo :: gfs) ->
  legal_nested_field0 t (ArraySubsc hi :: gfs) ->
  size_compatible t p ->
  align_compatible t p ->
  complete_legal_cosu_type t = true ->
  align_compatible (nested_field_array_type t gfs lo hi)
   (offset_val (nested_field_offset t (ArraySubsc lo :: gfs)) p).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros. rename H3 into Hcomplete.
(* Goal: @align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs)) p) *)
  rewrite nested_field_offset_ind by auto.
(* Goal: P *)
  destruct H.
(* Goal: @align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo))) p) *)
  destruct H0 as [_ ?].
(* Goal: @align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo))) p) *)
  assert (H9:= align_compatible_nested_field t gfs p H H1 H2 Hcomplete).
(* Goal: @align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo))) p) *)
  rewrite nested_field_array_type_ind.
(* Goal: @align_compatible cs (gfield_array_type (nested_field_type t gfs) lo hi) (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) (ArraySubsc lo))) p) *)
  destruct (nested_field_type t gfs) eqn:?H; inv H3. simpl in H0.
(* Goal: @align_compatible cs (gfield_array_type (Tarray t0 z a) lo hi) (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (Tarray t0 z a) (ArraySubsc lo))) p) *)
  simpl gfield_array_type.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct p; simpl in *; try tauto.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  unfold Ptrofs.unsigned; simpl.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  unfold Ptrofs.unsigned at 2; simpl.
(* Goal: align_compatible_rec (@cenv_cs cs) (Tarray t0 (Z.sub hi lo) (no_alignas_attr a)) (Ptrofs.Z_mod_modulus (Z.add (Ptrofs.unsigned i) (Ptrofs.Z_mod_modulus (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo))))) *)
  apply align_compatible_rec_Tarray.
(* Goal: forall (i0 : Z) (_ : and (Z.le Z0 i0) (Z.lt i0 (Z.sub hi lo))), align_compatible_rec (@cenv_cs cs) t0 (Z.add (Ptrofs.Z_mod_modulus (Z.add (Ptrofs.unsigned i) (Ptrofs.Z_mod_modulus (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo))))) (Z.mul (@sizeof (@cenv_cs cs) t0) i0)) *)
  intros j ?.
  apply align_compatible_rec_Tarray_inv with (i:= (lo+j)) in H9; [ |omega].
  match goal with H: align_compatible_rec _ _ ?A |- align_compatible_rec _ _ ?B => replace B with A; auto end.
(* Goal: @eq Z (Z.add (Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr (nested_field_offset t gfs)))) (Z.mul (@sizeof (@cenv_cs cs) t0) (Z.add lo j))) (Z.add (Ptrofs.Z_mod_modulus (Z.add (Ptrofs.unsigned i) (Ptrofs.Z_mod_modulus (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo))))) (Z.mul (@sizeof (@cenv_cs cs) t0) j)) *)
  rewrite !Ptrofs.Z_mod_modulus_eq.
(* Goal: @eq Z (Z.add (Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr (nested_field_offset t gfs)))) (Z.mul (@sizeof (@cenv_cs cs) t0) (Z.add lo j))) (Z.add (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) (Z.mul (@sizeof (@cenv_cs cs) t0) j)) *)
  rewrite Z.mul_add_distr_l.
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo))) Ptrofs.modulus) *)
  rewrite Z.add_assoc.
(* Goal: @eq Z (Z.mul (@sizeof (@cenv_cs cs_from) T) i) (Z.mul (@sizeof (@cenv_cs cs_to) T) i) *)
  f_equal.
(* Goal: @eq Z (Z.add (Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr (nested_field_offset t gfs)))) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
  unfold Ptrofs.add.
(* Goal: @eq Z (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add (Ptrofs.unsigned i) (Ptrofs.unsigned (Ptrofs.repr (nested_field_offset t gfs)))))) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
  destruct (nested_field_offset_in_range t gfs H Hcomplete).
(* Goal: @eq Z (Z.add (Ptrofs.unsigned (Ptrofs.repr (Z.add (Ptrofs.unsigned i) (Ptrofs.unsigned (Ptrofs.repr (nested_field_offset t gfs)))))) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
  pose proof (sizeof_pos (nested_field_type t gfs)).
  assert (Ptrofs.max_unsigned = Ptrofs.modulus-1) by computable. (* TODO: This should not be necessary, rep_omega should know it *)
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  rewrite (Ptrofs.unsigned_repr (nested_field_offset _ _)) by rep_omega.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  rewrite Ptrofs.unsigned_repr by rep_omega.
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
  pose proof (sizeof_pos t0).
     assert (0 <= sizeof t0 * lo <= sizeof t0 * z). {
           rewrite <- (Z.mul_0_r (sizeof t0)).
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
           split; apply Zmult_le_compat_l; omega.
     }
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  rewrite H4 in *. simpl in H8. rewrite Z.max_r in H8 by omega.
  rewrite (Z.mod_small (_ + _ * _)) by rep_omega.
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo))) Ptrofs.modulus) *)
  rewrite Z.add_assoc.
(* Goal: @eq Z (Z.modulo (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) *)
  symmetry; apply Z.mod_small.
(* Goal: and (Z.le Z0 (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0))))) (Z.lt (Z.add (Z.add ofs (nested_field_offset t gfs)) (field_offset (@cenv_cs cs) i (co_members (@get_co cs i0)))) Ptrofs.modulus) *)
  rep_omega.
Qed.

Lemma field_compatible_nested_field: forall t gfs p,
  field_compatible t gfs p ->
  field_compatible (nested_field_type t gfs) nil (offset_val (nested_field_offset t gfs) p).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  unfold field_compatible in *.
(* Goal: and (isptr (offset_val (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs)) p)) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) (nested_field_array_type t gfs lo hi)) true) (and (@size_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs)) p)) (and (@align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs)) p)) (legal_nested_field (nested_field_array_type t gfs lo hi) (@nil gfield))))) *)
  repeat split.
  + rewrite isptr_offset_val; tauto.
  + apply nested_field_type_complete_legal_cosu_type; auto; tauto.
  + apply size_compatible_nested_field; tauto.
  + apply align_compatible_nested_field; tauto.
Qed.

Lemma field_compatible0_nested_field_array: forall t gfs lo hi p,
  field_compatible0 t (ArraySubsc lo :: gfs) p ->
  field_compatible0 t (ArraySubsc hi :: gfs) p ->
  lo <= hi ->
  field_compatible (nested_field_array_type t gfs lo hi) nil (offset_val (nested_field_offset t (ArraySubsc lo :: gfs)) p).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  unfold field_compatible, field_compatible0 in *.
(* Goal: and (isptr (offset_val (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs)) p)) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) (nested_field_array_type t gfs lo hi)) true) (and (@size_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs)) p)) (and (@align_compatible cs (nested_field_array_type t gfs lo hi) (offset_val (nested_field_offset t (@cons gfield (ArraySubsc lo) gfs)) p)) (legal_nested_field (nested_field_array_type t gfs lo hi) (@nil gfield))))) *)
  repeat split.
  + rewrite isptr_offset_val; tauto.
  + apply nested_field_array_type_complete_legal_cosu_type; try tauto.
  + apply size_compatible_nested_field_array; tauto.
  + apply align_compatible_nested_field_array; tauto.
Qed.

Lemma field_compatible_isptr :
  forall t path p, field_compatible t path p -> isptr p.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
Proof. intros. destruct H; auto. Qed.

Lemma field_compatible0_isptr :
  forall t path p, field_compatible0 t path p -> isptr p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
intros. destruct H; auto.
Qed.
(*
Lemma field_compatible_complete_type:
  forall t path p, field_compatible t path p -> complete_type cenv_cs t = true.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
Proof. intros. destruct H; tauto. Qed.

Lemma field_compatible0_complete_type:
  forall t path p, field_compatible0 t path p -> complete_type cenv_cs t = true.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
Proof. intros. destruct H; tauto. Qed.
*)
Lemma field_compatible_legal_nested_field:
  forall (t : type) (path : list gfield) (p : val),
  field_compatible t path p -> legal_nested_field t path.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct H; tauto.
Qed.

Lemma field_compatible_legal_nested_field0:
  forall (t : type) (path : list gfield) (p : val),
  field_compatible t path p -> legal_nested_field0 t path.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: legal_nested_field0 t path *)
  apply legal_nested_field0_field.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct H; tauto.
Qed.

Lemma field_compatible0_legal_nested_field0:
  forall (t : type) (path : list gfield) (p : val),
  field_compatible0 t path p -> legal_nested_field0 t path.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct H; tauto.
Qed.

Lemma field_compatible_field_address: forall t gfs p, field_compatible t gfs p -> field_address t gfs p = offset_val (nested_field_offset t gfs) p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq val (field_address t gfs p) (offset_val (nested_field_offset t gfs) p) *)
  unfold field_address.
(* Goal: @eq bool (compute_in_members i al) true *)
  rewrite if_true by auto.
(* Goal: @eq bool (compute_in_members i al) true *)
  auto.
Qed.

Lemma field_compatible0_field_address0: forall t gfs p, field_compatible0 t gfs p -> field_address0 t gfs p = offset_val (nested_field_offset t gfs) p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq val (field_address0 t gfs p) (offset_val (nested_field_offset t gfs) p) *)
  unfold field_address0.
(* Goal: @eq bool (compute_in_members i al) true *)
  rewrite if_true by auto.
(* Goal: @eq bool (compute_in_members i al) true *)
  auto.
Qed.

Lemma field_compatible_shrink: forall t_root gfsB gfsA a,
  field_compatible t_root (gfsB ++ gfsA) a ->
  field_compatible t_root gfsA a.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros. unfold field_compatible in *. rename H into A. repeat destruct A as [? A].
  repeat split; try assumption. eapply legal_nested_field_shrink. eassumption.
Qed.

Lemma field_compatible0_shrink: forall t_root gfsB gfsA a,
  field_compatible0 t_root (gfsB ++ gfsA) a ->
  field_compatible0 t_root gfsA a.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros. unfold field_compatible0 in *. rename H into A. repeat destruct A as [? A].
  repeat split; try assumption. eapply legal_nested_field0_shrink. eassumption.
Qed.

Lemma field_compatible0_shrink1: forall t_root gfsB gfsA a,
  gfsB <> nil ->
  field_compatible0 t_root (gfsB ++ gfsA) a ->
  field_compatible t_root gfsA a.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros. unfold field_compatible0, field_compatible in *. rename H0 into A. repeat destruct A as [? A].
  repeat split; try assumption. eapply legal_nested_field0_shrink1. eassumption. eassumption.
Qed.

Lemma field_compatible_app: forall gfsB t_root gfsA a,
  field_compatible t_root (gfsB ++ gfsA) a ->
  field_compatible (nested_field_type t_root gfsA) gfsB (field_address t_root gfsA a).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intro gfsB. induction gfsB; intros.
  - simpl in H. rewrite field_compatible_field_address by assumption.
(* Goal: field_compatible (nested_field_type t_root gfsA) (@nil gfield) (offset_val (nested_field_offset t_root gfsA) a) *)
    apply field_compatible_nested_field. assumption.
  - rewrite <- app_comm_cons in H.
(* Goal: field_compatible (nested_field_type t_root gfsA) (@cons gfield a gfsB) (field_address t_root gfsA a0) *)
    apply field_compatible_cons in H.
    destruct (nested_field_type t_root (gfsB ++ gfsA)) eqn: E;
    try solve [exfalso; assumption];
    destruct a; try solve [exfalso; assumption];
    rewrite <- nested_field_type_nested_field_type in E;
    apply field_compatible_cons;
(* Goal: @eq bool (compute_in_members i al) true *)
    rewrite E; destruct H; auto.
Qed.

Lemma field_compatible0_app1: forall gfsB t_root gfsA a
  (NEQ: gfsB <> nil),
  field_compatible0 t_root (gfsB ++ gfsA) a ->
  field_compatible0 (nested_field_type t_root gfsA) gfsB (field_address t_root gfsA a).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: field_compatible0 (nested_field_type t_root gfsA) gfsB (field_address t_root gfsA a) *)
  destruct gfsB; [congruence | clear NEQ].
(* Goal: field_compatible0 (nested_field_type t_root gfsA) (@cons gfield g gfsB) (field_address t_root gfsA a) *)
  pose proof field_compatible_app gfsB t_root gfsA a.
  rewrite <- app_comm_cons in H.
(* Goal: field_compatible0 (nested_field_type t_root gfsA) (@cons gfield g gfsB) (field_address t_root gfsA a) *)
  apply field_compatible0_cons in H.
  destruct (nested_field_type t_root (gfsB ++ gfsA)) eqn: E;
  try solve [exfalso; assumption];
  destruct g; try solve [exfalso; assumption];
  rewrite <- nested_field_type_nested_field_type in E;
  apply field_compatible0_cons;
(* Goal: @eq bool (compute_in_members i al) true *)
  rewrite E; destruct H; auto.
Qed.

Lemma field_compatible_app_inv': forall gfsB t_root gfsA a,
  field_compatible t_root gfsA a ->
  legal_nested_field (nested_field_type t_root gfsA) gfsB ->
  field_compatible t_root (gfsB ++ gfsA) a.
Proof.
(* Goal: iff (@field_compatible cs_from t gfs p) (@field_compatible cs_to t gfs p) *)
  unfold field_compatible.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: and (isptr a) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t_root) true) (and (@size_compatible cs t_root a) (and (@align_compatible cs t_root a) (legal_nested_field t_root (@app gfield gfsB gfsA))))) *)
  pose proof legal_nested_field_app_inv t_root gfsA gfsB.
(* Goal: @eq bool (compute_in_members i al) true *)
  tauto.
Qed.

Lemma field_compatible0_app_inv': forall gfsB t_root gfsA a,
  field_compatible t_root gfsA a ->
  legal_nested_field0 (nested_field_type t_root gfsA) gfsB ->
  field_compatible0 t_root (gfsB ++ gfsA) a.
Proof.
(* Goal: forall (gfsB : list gfield) (t_root : type) (gfsA : list gfield) (a : val) (_ : field_compatible t_root gfsA a) (_ : legal_nested_field0 (nested_field_type t_root gfsA) gfsB), field_compatible0 t_root (@app gfield gfsB gfsA) a *)
  unfold field_compatible0, field_compatible.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: and (isptr a) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs) t_root) true) (and (@size_compatible cs t_root a) (and (@align_compatible cs t_root a) (legal_nested_field0 t_root (@app gfield gfsB gfsA))))) *)
  pose proof legal_nested_field0_app_inv t_root gfsA gfsB.
(* Goal: @eq bool (compute_in_members i al) true *)
  tauto.
Qed.

Lemma field_compatible_app_inv: forall gfsB t_root gfsA a,
  field_compatible t_root gfsA a ->
  field_compatible (nested_field_type t_root gfsA) gfsB (field_address t_root gfsA a) ->
  field_compatible t_root (gfsB ++ gfsA) a.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  apply field_compatible_app_inv'; auto.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct H0; tauto.
Qed.

Lemma field_compatible0_app_inv: forall gfsB t_root gfsA a,
  field_compatible t_root gfsA a ->
  field_compatible0 (nested_field_type t_root gfsA) gfsB (field_address t_root gfsA a) ->
  field_compatible0 t_root (gfsB ++ gfsA) a.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  apply field_compatible0_app_inv'; auto.
(* Goal: @eq bool (compute_in_members i al) true *)
  destruct H0; tauto.
Qed.

Lemma field_address_app: forall t_root gfsA gfsB a,
  field_address t_root (gfsB ++ gfsA) a =
  field_address (nested_field_type t_root gfsA) gfsB (field_address t_root gfsA a).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  assert (
    ~ field_compatible t_root gfsA a /\ ~ field_compatible t_root (gfsB ++ gfsA) a \/
    ~ field_compatible (nested_field_type t_root gfsA) gfsB (field_address t_root gfsA a) /\ ~ field_compatible t_root (gfsB ++ gfsA) a \/
    field_compatible t_root (gfsB ++ gfsA) a).
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
  {
    pose proof field_compatible_app_inv gfsB t_root gfsA a.
(* Goal: @eq bool (compute_in_members i al) true *)
    tauto.
  }
  destruct H as [[? ?] | [[? ?] | ?]].
  + unfold field_address.
(* Goal: @eq bool (compute_in_members i al) true *)
    rewrite if_false by auto.
    destruct (field_compatible_dec t_root gfsA a); [tauto |].
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    if_tac; reflexivity.
  + unfold field_address.
(* Goal: @eq bool (compute_in_members i al) true *)
    rewrite if_false by auto.
(* Goal: @eq bool (compute_in_members i al) true *)
    rewrite if_false by auto.
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    reflexivity.
  + rewrite field_compatible_field_address.
    rewrite field_compatible_field_address.
    rewrite nested_field_offset_app.
    rewrite field_compatible_field_address.
(* Goal: @eq val (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf)) p) (offset_val (gfield_offset (nested_field_type t gfs) gf) (offset_val (nested_field_offset t gfs) p)) *)
    rewrite offset_offset_val.
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    reflexivity.
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
    { eapply field_compatible_shrink. eassumption. }
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
    { eapply field_compatible_legal_nested_field. eassumption. }
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
    { eapply field_compatible_app. assumption. }
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
    { assumption. }
Qed.

Lemma field_address0_app: forall t_root gfsA gfsB a
  (NEQ: gfsB <> nil),
  field_address0 t_root (gfsB ++ gfsA) a =
  field_address0 (nested_field_type t_root gfsA) gfsB (field_address t_root gfsA a).
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
  assert (
    ~ field_compatible t_root gfsA a /\ ~ field_compatible0 t_root (gfsB ++ gfsA) a \/
    ~ field_compatible0 (nested_field_type t_root gfsA) gfsB (field_address t_root gfsA a) /\ ~ field_compatible0 t_root (gfsB ++ gfsA) a \/
    field_compatible0 t_root (gfsB ++ gfsA) a).
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
  {
    pose proof field_compatible0_app_inv gfsB t_root gfsA a.
(* Goal: @eq bool (compute_in_members i al) true *)
    tauto.
  }
  destruct H as [[? ?] | [[? ?] | ?]].
  + unfold field_address0, field_address.
(* Goal: @eq bool (compute_in_members i al) true *)
    rewrite if_false by auto.
    destruct (field_compatible_dec t_root gfsA a); [tauto |].
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    if_tac; reflexivity.
  + unfold field_address0, field_address.
(* Goal: @eq bool (compute_in_members i al) true *)
    rewrite if_false by auto.
(* Goal: @eq bool (compute_in_members i al) true *)
    rewrite if_false by auto.
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    reflexivity.
  + rewrite field_compatible0_field_address0.
    rewrite field_compatible0_field_address0.
    rewrite nested_field_offset0_app.
    rewrite field_compatible_field_address.
(* Goal: @eq val (offset_val (Z.add (nested_field_offset t gfs) (gfield_offset (nested_field_type t gfs) gf)) p) (offset_val (gfield_offset (nested_field_type t gfs) gf) (offset_val (nested_field_offset t gfs) p)) *)
    rewrite offset_offset_val.
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    reflexivity.
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
    { eapply field_compatible0_shrink1; eassumption. }
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
    { eapply field_compatible0_legal_nested_field0. eassumption. }
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
    { eapply field_compatible0_app1; assumption. }
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
    { assumption. }
Qed.

End COMPOSITE_ENV.
(*
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
Arguments nested_field_offset2 {cs} t gfs /.
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
Arguments nested_field_type2 {cs} t gfs /.
*)

(* Hint Resolve field_address_isptr. *)
Hint Resolve is_pointer_or_null_field_compatible.
(* Hint Extern 1 (complete_type _ _ = true) => (eapply field_compatible_complete_type; eassumption). *)
Hint Extern 1 (isptr _) => (eapply field_compatible_isptr; eassumption).
Hint Extern 1 (isptr _) => (eapply field_compatible0_isptr; eassumption).
Hint Extern 1 (legal_nested_field _ _) => (eapply field_compatible_legal_nested_field; eassumption).
Hint Extern 1 (legal_nested_field0 _ _) => (eapply field_compatible_legal_nested_field0; eassumption).
Hint Extern 1 (legal_nested_field0 _ _) => (eapply field_compatible0_legal_nested_field0; eassumption).

(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
Lemma nested_field_type_preserves_change_composite: forall {cs_from cs_to} {CCE: change_composite_env cs_from cs_to} (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  forall gfs, cs_preserve_type cs_from cs_to (coeq cs_from cs_to) (@nested_field_type cs_to t gfs) = true.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  induction gfs; auto.
(* Goal: @eq type (@gfield_type cs_from (@nested_field_type cs_from t gfs) a) (@nested_field_type cs_to t (@cons gfield a gfs)) *)
  rewrite (@nested_field_type_ind cs_to).
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  revert IHgfs; generalize (@nested_field_type cs_to t gfs) as T; clear; intros.
(* Goal: @eq Z (@gfield_offset cs_from T a) (@gfield_offset cs_to T a) *)
  destruct a.
  + destruct T; auto.
  + destruct T; auto.
(* Goal: @eq type (@gfield_type cs_from (Tunion i0 a) (UnionField i)) (@gfield_type cs_to (Tunion i0 a) (UnionField i)) *)
    unfold gfield_type.
(* Goal: @eq bool (compute_in_members i al) true *)
    apply members_spec_change_composite''; auto.
  + destruct T; auto.
(* Goal: @eq type (@gfield_type cs_from (Tunion i0 a) (UnionField i)) (@gfield_type cs_to (Tunion i0 a) (UnionField i)) *)
    unfold gfield_type.
(* Goal: @eq bool (compute_in_members i al) true *)
    apply members_spec_change_composite''; auto.
Qed.

(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
Lemma nested_field_type_change_composite: forall {cs_from cs_to} {CCE: change_composite_env cs_from cs_to} (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  forall gfs, @nested_field_type cs_from t gfs = @nested_field_type cs_to t gfs.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  induction gfs; auto.
(* Goal: @eq type (@nested_field_type cs_from t (@cons gfield a gfs)) (@nested_field_type cs_to t (@cons gfield a gfs)) *)
  rewrite (@nested_field_type_ind cs_from).
(* Goal: @eq type (@gfield_type cs_from (@nested_field_type cs_from t gfs) a) (@nested_field_type cs_to t (@cons gfield a gfs)) *)
  rewrite (@nested_field_type_ind cs_to).
(* Goal: @eq type (@gfield_type cs_from (@nested_field_type cs_from t gfs) a) (@gfield_type cs_to (@nested_field_type cs_to t gfs) a) *)
  rewrite IHgfs.
(* Goal: @eq Z (Z.add (@nested_field_offset cs_to t gfs) (@gfield_offset cs_from (@nested_field_type cs_from t gfs) a)) (Z.add (@nested_field_offset cs_to t gfs) (@gfield_offset cs_to (@nested_field_type cs_to t gfs) a)) *)
  clear IHgfs.
(* Goal: @eq Z (@gfield_offset cs_from (@nested_field_type cs_to t gfs) a) (@gfield_offset cs_to (@nested_field_type cs_to t gfs) a) *)
  generalize (nested_field_type_preserves_change_composite _ H gfs).
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  generalize (@nested_field_type cs_to t gfs) as T; clear; intros.
(* Goal: @eq Z (@gfield_offset cs_from T a) (@gfield_offset cs_to T a) *)
    destruct a.
    - destruct T; auto.
    - destruct T; auto.
(* Goal: @eq type (@gfield_type cs_from (Tunion i0 a) (UnionField i)) (@gfield_type cs_to (Tunion i0 a) (UnionField i)) *)
      unfold gfield_type.
(* Goal: @eq bool (compute_in_members i al) true *)
      rewrite co_members_get_co_change_composite; auto.
    - destruct T; auto.
(* Goal: @eq type (@gfield_type cs_from (Tunion i0 a) (UnionField i)) (@gfield_type cs_to (Tunion i0 a) (UnionField i)) *)
      unfold gfield_type.
(* Goal: @eq bool (compute_in_members i al) true *)
      rewrite co_members_get_co_change_composite; auto.
Qed.

(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
Lemma legal_nested_field_change_composite: forall {cs_from cs_to} {CCE: change_composite_env cs_from cs_to} (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  forall gfs, @legal_nested_field cs_from t gfs <-> @legal_nested_field cs_to t gfs.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  revert t H; induction gfs; intros.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  + simpl.
(* Goal: @eq bool (compute_in_members i al) true *)
    tauto.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
  + simpl.
(* Goal: iff (and (@legal_nested_field cs_from t gfs) (@legal_field cs_from (@nested_field_type cs_from t gfs) a)) (and (@legal_nested_field cs_to t gfs) (@legal_field cs_to (@nested_field_type cs_to t gfs) a)) *)
    apply Morphisms_Prop.and_iff_morphism; [apply IHgfs; auto |].
(* Goal: @eq bool (compute_in_members i al) true *)
    rewrite nested_field_type_change_composite by auto.
(* Goal: @eq Z (@gfield_offset cs_from (@nested_field_type cs_to t gfs) a) (@gfield_offset cs_to (@nested_field_type cs_to t gfs) a) *)
    generalize (nested_field_type_preserves_change_composite _ H gfs).
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
    generalize (@nested_field_type cs_to t gfs) as T; clear; intros.
(* Goal: @eq Z (@gfield_offset cs_from T a) (@gfield_offset cs_to T a) *)
    destruct a.
    - destruct T; try tauto.
    - destruct T; try tauto.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
      simpl.
(* Goal: @eq bool (compute_in_members i al) true *)
      rewrite co_members_get_co_change_composite by auto.
(* Goal: @eq bool (compute_in_members i al) true *)
      tauto.
    - destruct T; try tauto.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
      simpl.
(* Goal: @eq bool (compute_in_members i al) true *)
      rewrite co_members_get_co_change_composite by auto.
(* Goal: @eq bool (compute_in_members i al) true *)
      tauto.
Qed.

(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
Lemma field_compatible_change_composite: forall {cs_from cs_to} {CCE: change_composite_env cs_from cs_to} (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  forall gfs p, @field_compatible cs_from t gfs p <-> @field_compatible cs_to t gfs p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: iff (@field_compatible cs_from t gfs p) (@field_compatible cs_to t gfs p) *)
  unfold field_compatible.
(* Goal: iff (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs_to) t) true) (and (@size_compatible cs_from t p) (and (@align_compatible cs_from t p) (@legal_nested_field cs_from t gfs)))) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs_to) t) true) (and (@size_compatible cs_to t p) (and (@align_compatible cs_to t p) (@legal_nested_field cs_to t gfs)))) *)
  apply and_iff_compat_l.
(* Goal: @eq bool (compute_in_members i al) true *)
  rewrite complete_legal_cosu_type_change_composite by auto.
(* Goal: iff (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs_to) t) true) (and (@size_compatible cs_from t p) (and (@align_compatible cs_from t p) (@legal_nested_field cs_from t gfs)))) (and (@eq bool (@complete_legal_cosu_type (@cenv_cs cs_to) t) true) (and (@size_compatible cs_to t p) (and (@align_compatible cs_to t p) (@legal_nested_field cs_to t gfs)))) *)
  apply and_iff_compat_l.
(* Goal: iff (and (@size_compatible cs_from t p) (and (@align_compatible cs_from t p) (@legal_nested_field cs_from t gfs))) (and (@size_compatible cs_to t p) (and (@align_compatible cs_to t p) (@legal_nested_field cs_to t gfs))) *)
  apply Morphisms_Prop.and_iff_morphism; [| apply Morphisms_Prop.and_iff_morphism].
  + unfold size_compatible.
(* Goal: @eq bool (compute_in_members i al) true *)
    rewrite sizeof_change_composite by auto.
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    reflexivity.
  + unfold align_compatible.
(* Goal: iff match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end match p with | Vundef => True | Vint i => True | Vlong i => True | Vfloat f => True | Vsingle f => True | Vptr b i_ofs => Z.lt (Z.add (Ptrofs.unsigned i_ofs) (@sizeof (@cenv_cs cs_to) t)) Ptrofs.modulus end *)
    destruct p; try reflexivity.
(* Goal: @eq bool (compute_in_members i al) true *)
    apply align_compatible_rec_change_composite; auto.
  + apply legal_nested_field_change_composite; auto.
Qed.

(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
Lemma nested_field_offset_change_composite: forall {cs_from cs_to} {CCE: change_composite_env cs_from cs_to} (t: type),
  cs_preserve_type cs_from cs_to (coeq _ _) t = true ->
  forall gfs,
    @legal_nested_field cs_from t gfs ->
    @legal_nested_field cs_to t gfs ->
    @nested_field_offset cs_from t gfs = @nested_field_offset cs_to t gfs.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @eq bool (compute_in_members i al) true *)
  induction gfs; auto.
(* Goal: @eq Z (@nested_field_offset cs_from t (@cons gfield a gfs)) (@nested_field_offset cs_to t (@cons gfield a gfs)) *)
  rewrite (@nested_field_offset_ind cs_from) by (apply legal_nested_field0_field; auto).
(* Goal: @eq Z (Z.add (@nested_field_offset cs_from t gfs) (@gfield_offset cs_from (@nested_field_type cs_from t gfs) a)) (@nested_field_offset cs_to t (@cons gfield a gfs)) *)
  rewrite (@nested_field_offset_ind cs_to) by (apply legal_nested_field0_field; auto).
(* Goal: @eq Z (Z.add (@nested_field_offset cs_from t gfs) (@gfield_offset cs_from (@nested_field_type cs_from t gfs) a)) (Z.add (@nested_field_offset cs_to t gfs) (@gfield_offset cs_to (@nested_field_type cs_to t gfs) a)) *)
  rewrite IHgfs by (simpl in H0, H1; tauto).
(* Goal: @eq Z (Z.add (@nested_field_offset cs_to t gfs) (@gfield_offset cs_from (@nested_field_type cs_from t gfs) a)) (Z.add (@nested_field_offset cs_to t gfs) (@gfield_offset cs_to (@nested_field_type cs_to t gfs) a)) *)
  clear IHgfs.
(* Goal: @eq Z (Z.mul (@sizeof (@cenv_cs cs_from) T) i) (Z.mul (@sizeof (@cenv_cs cs_to) T) i) *)
  f_equal.
(* Goal: @eq Z (@gfield_offset cs_from (@nested_field_type cs_from t gfs) a) (@gfield_offset cs_to (@nested_field_type cs_to t gfs) a) *)
  destruct H1 as [_ ?].
(* Goal: @eq bool (compute_in_members i al) true *)
  rewrite nested_field_type_change_composite by auto.
(* Goal: @eq Z (@gfield_offset cs_from (@nested_field_type cs_to t gfs) a) (@gfield_offset cs_to (@nested_field_type cs_to t gfs) a) *)
  generalize (nested_field_type_preserves_change_composite _ H gfs).
(* Goal: forall _ : @eq bool (cs_preserve_type cs_from cs_to (@coeq cs_from cs_to CCE) (@nested_field_type cs_to t gfs)) true, @eq Z (@gfield_offset cs_from (@nested_field_type cs_to t gfs) a) (@gfield_offset cs_to (@nested_field_type cs_to t gfs) a) *)
  revert H1.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  generalize (@nested_field_type cs_to t gfs) as T; clear; intros.
(* Goal: @eq Z (@gfield_offset cs_from T a) (@gfield_offset cs_to T a) *)
  destruct a.
  + destruct T; auto; inv H1.
(* Goal: @eq Z (@gfield_offset cs_from (Tarray T z a) (ArraySubsc i)) (@gfield_offset cs_to (Tarray T z a) (ArraySubsc i)) *)
    simpl.
(* Goal: @eq Z (Z.mul (@sizeof (@cenv_cs cs_from) T) i) (Z.mul (@sizeof (@cenv_cs cs_to) T) i) *)
    f_equal.
(* Goal: @eq bool (compute_in_members i al) true *)
    apply sizeof_change_composite; auto.
  + destruct T; try inv H1.
(* Goal: @eq Z (@gfield_offset cs_from (Tstruct i0 a) (StructField i)) (@gfield_offset cs_to (Tstruct i0 a) (StructField i)) *)
    unfold gfield_offset.
(* Goal: @eq bool (compute_in_members i al) true *)
    rewrite co_members_get_co_change_composite by auto.
(* Goal: @eq bool (compute_in_members i al) true *)
    apply field_offset_change_composite; auto.
  + destruct T; try inv H1.
(* Goal: @eq bool (compute_in_members i al) true *)
    auto.
Qed.

Lemma lvar_size_compatible:
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
  forall  {cs: compspecs} id t v rho,
  locald_denote (lvar id t v) rho ->
  sizeof t < Ptrofs.modulus ->
  size_compatible t v.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
intros. hnf in H.
(* Goal: @size_compatible cs t v *)
destruct (Map.get (ve_of rho) id) as [[? ?] | ]; try contradiction.
(* Goal: @size_compatible cs t v *)
destruct H; subst.
(* Goal: @size_compatible cs t0 (Vptr b Ptrofs.zero) *)
red.
(* Goal: @eq bool (compute_in_members i al) true *)
rewrite Ptrofs.unsigned_zero. rewrite Z.add_0_l; auto.
Qed.

Lemma lvar_field_compatible:
(* Goal: and (Z.le Z0 (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.le (Z.mul (@sizeof (@cenv_cs cs) t0) lo) (Z.mul (@sizeof (@cenv_cs cs) t0) z)) *)
(* Goal: @eq Z (Z.add (Z.add (Ptrofs.unsigned i) (nested_field_offset t gfs)) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) (Z.modulo (Z.add (Ptrofs.unsigned i) (Z.modulo (Z.add (nested_field_offset t gfs) (Z.mul (@sizeof (@cenv_cs cs) t0) lo)) Ptrofs.modulus)) Ptrofs.modulus) *)
  forall {cs: compspecs} id t v rho,
    locald_denote (lvar id t v) rho ->
    complete_legal_cosu_type t = true ->
    is_aligned cenv_cs ha_env_cs la_env_cs t 0 = true ->
    sizeof t < Ptrofs.modulus ->
    field_compatible t nil v.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
  intros.
(* Goal: @field_compatible cs t (@nil gfield) v *)
  pose proof (lvar_size_compatible _ _ _ _ H).
(* Goal: @field_compatible cs t (@nil gfield) v *)
  hnf in H.
(* Goal: @field_compatible cs t (@nil gfield) v *)
  destruct (Map.get (ve_of rho) id); try contradiction.
(* Goal: P *)
  destruct p. destruct H. subst v t0.
(* Goal: @eq bool (compute_in_members i al) true *)
  repeat split; auto.
(* Goal: @align_compatible cs t (Vptr b Ptrofs.zero) *)
  hnf.
(* Goal: @eq bool (compute_in_members i al) true *)
  apply la_env_cs_sound; auto.
Qed.

Lemma compute_in_members_e:
 forall i al, compute_in_members i al = true -> in_members i al.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
intros.
(* Goal: @eq bool (compute_in_members i al) true *)
apply compute_in_members_true_iff. auto.
Qed.

Hint Extern 2 (field_compatible _ (StructField _ :: _) _) =>
  (apply field_compatible_cons; split; [ apply compute_in_members_e; reflexivity | ])
      : field_compatible.

Lemma field_compatible_nullval: forall CS t f P,
  @field_compatible CS t f nullval -> P.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
intros.
(* Goal: P *)
destruct H.
(* Goal: P *)
contradiction H.
Qed.

Lemma field_compatible_nullval1:
 forall (CS: compspecs) t fld p,
  @field_compatible CS t fld p -> p <> nullval.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
 intros. intro; subst p. apply (field_compatible_nullval _ _ _ _ H).
Qed.

Lemma field_compatible_nullval2:
 forall (CS: compspecs) t fld p,
  @field_compatible CS t fld p -> nullval <> p.
Proof.
(* Goal: forall (CS : compspecs) (t : type) (fld : list gfield) (p : val) (_ : @field_compatible CS t fld p), not (@eq val nullval p) *)
 intros. intro; subst p. apply (field_compatible_nullval _ _ _ _ H).
Qed.

