(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Type expressions for the Compcert C and Clight languages *)

Require Import Axioms Coqlib Maps Errors.
Require Import AST Linking.
Require Archi.

(** * Syntax of types *)

(** Compcert C types are similar to those of C.  They include numeric types,
  pointers, arrays, function types, and composite types (struct and
  union).  Numeric types (integers and floats) fully specify the
  bit size of the type.  An integer type is a pair of a signed/unsigned
  flag and a bit size: 8, 16, or 32 bits, or the special [IBool] size
  standing for the C99 [_Bool] type.  64-bit integers are treated separately. *)

Inductive signedness : Type :=
  | Signed: signedness
  | Unsigned: signedness.

Inductive intsize : Type :=
  | I8: intsize
  | I16: intsize
  | I32: intsize
  | IBool: intsize.

(** Float types come in two sizes: 32 bits (single precision)
  and 64-bit (double precision). *)

Inductive floatsize : Type :=
  | F32: floatsize
  | F64: floatsize.

(** Every type carries a set of attributes.  Currently, only two
  attributes are modeled: [volatile] and [_Alignas(n)] (from ISO C 2011). *)

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Record attr : Type := mk_attr {
  attr_volatile: bool;
  attr_alignas: option N         (**r log2 of required alignment *)
}.

Definition noattr := {| attr_volatile := false; attr_alignas := None |}.

(** The syntax of type expressions.  Some points to note:
- Array types [Tarray n] carry the size [n] of the array.
  Arrays with unknown sizes are represented by pointer types.
- Function types [Tfunction targs tres] specify the number and types
  of the function arguments (list [targs]), and the type of the
  function result ([tres]).  Variadic functions and old-style unprototyped
  functions are not supported.
*)

Inductive type : Type :=
  | Tvoid: type                                    (**r the [void] type *)
  | Tint: intsize -> signedness -> attr -> type    (**r integer types *)
  | Tlong: signedness -> attr -> type              (**r 64-bit integer types *)
  | Tfloat: floatsize -> attr -> type              (**r floating-point types *)
  | Tpointer: type -> attr -> type                 (**r pointer types ([*ty]) *)
  | Tarray: type -> Z -> attr -> type              (**r array types ([ty[len]]) *)
  | Tfunction: typelist -> type -> calling_convention -> type    (**r function types *)
  | Tstruct: ident -> attr -> type                 (**r struct types *)
  | Tunion: ident -> attr -> type                  (**r union types *)
with typelist : Type :=
  | Tnil: typelist
  | Tcons: type -> typelist -> typelist.

Lemma intsize_eq: forall (s1 s2: intsize), {s1=s2} + {s1<>s2}.
Proof.
(* Goal: sumbool (@eq struct_or_union su su0) (not (@eq struct_or_union su su0)) *)
  decide equality.
Defined.

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2}
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}.
Proof.
(* Goal: sumbool (@eq struct_or_union su su0) (not (@eq struct_or_union su su0)) *)
  assert (forall (x y: signedness), {x=y} + {x<>y}) by decide equality.
(* Goal: sumbool (@eq struct_or_union su su0) (not (@eq struct_or_union su su0)) *)
  assert (forall (x y: floatsize), {x=y} + {x<>y}) by decide equality.
  assert (forall (x y: attr), {x=y} + {x<>y}).
(* Goal: sumbool (@eq struct_or_union su su0) (not (@eq struct_or_union su su0)) *)
  { decide equality. decide equality. apply N.eq_dec. apply bool_dec. }
  generalize ident_eq zeq bool_dec ident_eq intsize_eq; intros.
(* Goal: sumbool (@eq struct_or_union su su0) (not (@eq struct_or_union su su0)) *)
  decide equality.
(* Goal: sumbool (@eq struct_or_union su su0) (not (@eq struct_or_union su su0)) *)
  decide equality.
(* Goal: sumbool (@eq struct_or_union su su0) (not (@eq struct_or_union su su0)) *)
  decide equality.
Defined.

Opaque type_eq typelist_eq.

(** Extract the attributes of a type. *)

Definition attr_of_type (ty: type) :=
  match ty with
  | Tvoid => noattr
  | Tint sz si a => a
  | Tlong si a => a
  | Tfloat sz a => a
  | Tpointer elt a => a
  | Tarray elt sz a => a
  | Tfunction args res cc => noattr
  | Tstruct id a => a
  | Tunion id a => a
  end.

(** Change the top-level attributes of a type *)

Definition change_attributes (f: attr -> attr) (ty: type) : type :=
  match ty with
  | Tvoid => ty
  | Tint sz si a => Tint sz si (f a)
  | Tlong si a => Tlong si (f a)
  | Tfloat sz a => Tfloat sz (f a)
  | Tpointer elt a => Tpointer elt (f a)
  | Tarray elt sz a => Tarray elt sz (f a)
  | Tfunction args res cc => ty
  | Tstruct id a => Tstruct id (f a)
  | Tunion id a => Tunion id (f a)
  end.

(** Erase the top-level attributes of a type *)

Definition remove_attributes (ty: type) : type :=
  change_attributes (fun _ => noattr) ty.

(** Add extra attributes to the top-level attributes of a type *)

Definition attr_union (a1 a2: attr) : attr :=
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  {| attr_volatile := a1.(attr_volatile) || a2.(attr_volatile);
     attr_alignas :=
       match a1.(attr_alignas), a2.(attr_alignas) with
       | None, al => al
       | al, None => al
       | Some n1, Some n2 => Some (N.max n1 n2)
       end
  |}.

Definition merge_attributes (ty: type) (a: attr) : type :=
  change_attributes (attr_union a) ty.

(** Syntax for [struct] and [union] definitions.  [struct] and [union]
  are collectively called "composites".  Each compilation unit
  comes with a list of top-level definitions of composites. *)

Inductive struct_or_union : Type := Struct | Union.

Definition members : Type := list (ident * type).

Inductive composite_definition : Type :=
  Composite (id: ident) (su: struct_or_union) (m: members) (a: attr).

Definition name_composite_def (c: composite_definition) : ident :=
  match c with Composite id su m a => id end.

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Definition composite_def_eq (x y: composite_definition): {x=y} + {x<>y}.
Proof.
(* Goal: sumbool (@eq struct_or_union su su0) (not (@eq struct_or_union su su0)) *)
  decide equality.
(* Goal: sumbool (@eq struct_or_union su su0) (not (@eq struct_or_union su su0)) *)
- decide equality. decide equality. apply N.eq_dec. apply bool_dec.
(* Goal: sumbool (@eq struct_or_union su su0) (not (@eq struct_or_union su su0)) *)
- apply list_eq_dec. decide equality. apply type_eq. apply ident_eq.
(* Goal: sumbool (@eq struct_or_union su su0) (not (@eq struct_or_union su su0)) *)
- decide equality.
- apply ident_eq.
Defined.

Global Opaque composite_def_eq. 

(** For type-checking, compilation and semantics purposes, the composite
  definitions are collected in the following [composite_env] environment.
  The [composite] record contains additional information compared with
  the [composite_definition], such as size and alignment information. *)

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Record composite : Type := {
  co_su: struct_or_union;
  co_members: members;
  co_attr: attr;
  co_sizeof: Z;
  co_alignof: Z;
  co_rank: nat;
  co_sizeof_pos: co_sizeof >= 0;
  co_alignof_two_p: exists n, co_alignof = two_power_nat n;
  co_sizeof_alignof: (co_alignof | co_sizeof)
}.

Definition composite_env : Type := PTree.t composite.

(** * Operations over types *)

(** ** Conversions *)

Definition type_int32s := Tint I32 Signed noattr.
Definition type_bool := Tint IBool Signed noattr.

(** The usual unary conversion.  Promotes small integer types to [signed int32]
  and degrades array types and function types to pointer types.
  Attributes are erased. *)

Definition typeconv (ty: type) : type :=
  match ty with
  | Tint (I8 | I16 | IBool) _ _ => Tint I32 Signed noattr
  | Tarray t sz a       => Tpointer t noattr
  | Tfunction _ _ _     => Tpointer ty noattr
  | _                   => remove_attributes ty
  end.

(** Default conversion for arguments to an unprototyped or variadic function.
  Like [typeconv] but also converts single floats to double floats. *)

Definition default_argument_conversion (ty: type) : type :=
  match ty with
  | Tint (I8 | I16 | IBool) _ _ => Tint I32 Signed noattr
  | Tfloat _ _          => Tfloat F64 noattr
  | Tarray t sz a       => Tpointer t noattr
  | Tfunction _ _ _     => Tpointer ty noattr
  | _                   => remove_attributes ty
  end.

(** ** Complete types *)

(** A type is complete if it fully describes an object.
  All struct and union names appearing in the type must be defined,
  unless they occur under a pointer or function type.  [void] and
  function types are incomplete types. *)

Fixpoint complete_type (env: composite_env) (t: type) : bool :=
  match t with
  | Tvoid => false
  | Tint _ _ _ => true
  | Tlong _ _ => true
  | Tfloat _ _ => true
  | Tpointer _ _ => true
  | Tarray t' _ _ => complete_type env t'
  | Tfunction _ _ _ => false
  | Tstruct id _ | Tunion id _ =>
      match env!id with Some co => true | None => false end
  end.

Definition complete_or_function_type (env: composite_env) (t: type) : bool :=
  match t with
  | Tfunction _ _ _ => true
  | _ => complete_type env t
  end.

(** ** Alignment of a type *)

(** Adjust the natural alignment [al] based on the attributes [a] attached
  to the type.  If an "alignas" attribute is given, use it as alignment
  in preference to [al]. *)

Definition align_attr (a: attr) (al: Z) : Z :=
  match attr_alignas a with
  | Some l => two_p (Z.of_N l)
  | None => al
  end.

(** In the ISO C standard, alignment is defined only for complete
  types.  However, it is convenient that [alignof] is a total
  function.  For incomplete types, it returns 1. *)

Fixpoint alignof (env: composite_env) (t: type) : Z :=
  align_attr (attr_of_type t)
   (match t with
      | Tvoid => 1
      | Tint I8 _ _ => 1
      | Tint I16 _ _ => 2
      | Tint I32 _ _ => 4
      | Tint IBool _ _ => 1
      | Tlong _ _ => Archi.align_int64
      | Tfloat F32 _ => 4
      | Tfloat F64 _ => Archi.align_float64
      | Tpointer _ _ => if Archi.ptr64 then 8 else 4
      | Tarray t' _ _ => alignof env t'
      | Tfunction _ _ _ => 1
      | Tstruct id _ | Tunion id _ =>
          match env!id with Some co => co_alignof co | None => 1 end
    end).

Remark align_attr_two_p:
  forall al a,
  (exists n, al = two_power_nat n) ->
  (exists n, align_attr a al = two_power_nat n).
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. unfold align_attr. destruct (attr_alignas a).
(* Goal: @ex nat (fun n0 : nat => @eq Z (two_p (Z.of_N n)) (two_power_nat n0)) *)
(* Goal: @ex nat (fun n : nat => @eq Z al (two_power_nat n)) *)
  exists (N.to_nat n). rewrite two_power_nat_two_p. rewrite N_nat_Z. auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  auto.
Qed.

Lemma alignof_two_p:
  forall env t, exists n, alignof env t = two_power_nat n.
Proof.
(* Goal: forall (env : composite_env) (t : type), @ex nat (fun n : nat => @eq Z (alignof env t) (two_power_nat n)) *)
  induction t; apply align_attr_two_p; simpl.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exists 0%nat; auto.
(* Goal: @ex nat (fun n : nat => @eq Z match i with | I8 => Zpos xH | I16 => Zpos (xO xH) | I32 => Zpos (xO (xO xH)) | IBool => Zpos xH end (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z Archi.align_int64 (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z match f with | F32 => Zpos (xO (xO xH)) | F64 => Archi.align_float64 end (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z (if Archi.ptr64 then Zpos (xO (xO (xO xH))) else Zpos (xO (xO xH))) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z ((fix alignof (env : composite_env) (t : type) {struct t} : Z := align_attr (attr_of_type t) match t with | Tvoid => Zpos xH | Tint (I8 as i) s a => Zpos xH | Tint (I16 as i) s a => Zpos (xO xH) | Tint (I32 as i) s a => Zpos (xO (xO xH)) | Tint (IBool as i) s a => Zpos xH | Tlong s a => Archi.align_int64 | Tfloat (F32 as f) a => Zpos (xO (xO xH)) | Tfloat (F64 as f) a => Archi.align_float64 | Tpointer t0 a => if Archi.ptr64 then Zpos (xO (xO (xO xH))) else Zpos (xO (xO xH)) | Tarray t' z a => alignof env t' | Tfunction t0 t1 c => Zpos xH | Tstruct id a => match @PTree.get composite id env with | Some co => co_alignof co | None => Zpos xH end | Tunion id a => match @PTree.get composite id env with | Some co => co_alignof co | None => Zpos xH end end) env t) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z (Zpos xH) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end (two_power_nat n)) *)
  destruct i.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    exists 0%nat; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    exists 1%nat; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    exists 2%nat; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    exists 0%nat; auto.
(* Goal: @ex nat (fun n : nat => @eq Z Archi.align_int64 (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z match f with | F32 => Zpos (xO (xO xH)) | F64 => Archi.align_float64 end (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z (if Archi.ptr64 then Zpos (xO (xO (xO xH))) else Zpos (xO (xO xH))) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z ((fix alignof (env : composite_env) (t : type) {struct t} : Z := align_attr (attr_of_type t) match t with | Tvoid => Zpos xH | Tint (I8 as i) s a => Zpos xH | Tint (I16 as i) s a => Zpos (xO xH) | Tint (I32 as i) s a => Zpos (xO (xO xH)) | Tint (IBool as i) s a => Zpos xH | Tlong s a => Archi.align_int64 | Tfloat (F32 as f) a => Zpos (xO (xO xH)) | Tfloat (F64 as f) a => Archi.align_float64 | Tpointer t0 a => if Archi.ptr64 then Zpos (xO (xO (xO xH))) else Zpos (xO (xO xH)) | Tarray t' z a => alignof env t' | Tfunction t0 t1 c => Zpos xH | Tstruct id a => match @PTree.get composite id env with | Some co => co_alignof co | None => Zpos xH end | Tunion id a => match @PTree.get composite id env with | Some co => co_alignof co | None => Zpos xH end end) env t) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z (Zpos xH) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end (two_power_nat n)) *)
    unfold Archi.align_int64. destruct Archi.ptr64; ((exists 2%nat; reflexivity) || (exists 3%nat; reflexivity)).
(* Goal: Z.divide match f with | F32 => Zpos (xO (xO xH)) | F64 => Archi.align_float64 end match f with | F32 => Zpos (xO (xO xH)) | F64 => Zpos (xO (xO (xO xH))) end *)
  destruct f.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    exists 2%nat; auto.
(* Goal: @ex nat (fun n : nat => @eq Z (Zpos (xO (xO xH))) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z (if Archi.ptr64 then Zpos (xO (xO (xO xH))) else Zpos (xO (xO xH))) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z ((fix alignof (env : composite_env) (t : type) {struct t} : Z := align_attr (attr_of_type t) match t with | Tvoid => Zpos xH | Tint (I8 as i) s a => Zpos xH | Tint (I16 as i) s a => Zpos (xO xH) | Tint (I32 as i) s a => Zpos (xO (xO xH)) | Tint (IBool as i) s a => Zpos xH | Tlong s a => Archi.align_int64 | Tfloat (F32 as f) a => Zpos (xO (xO xH)) | Tfloat (F64 as f) a => Archi.align_float64 | Tpointer t0 a => if Archi.ptr64 then Zpos (xO (xO (xO xH))) else Zpos (xO (xO xH)) | Tarray t' z a => alignof env t' | Tfunction t0 t1 c => Zpos xH | Tstruct id a => match @PTree.get composite id env with | Some co => co_alignof co | None => Zpos xH end | Tunion id a => match @PTree.get composite id env with | Some co => co_alignof co | None => Zpos xH end end) env t) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z (Zpos xH) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end (two_power_nat n)) *)
    unfold Archi.align_float64. destruct Archi.ptr64; ((exists 2%nat; reflexivity) || (exists 3%nat; reflexivity)).
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exists (if Archi.ptr64 then 3%nat else 2%nat); destruct Archi.ptr64; auto.
(* Goal: @ex nat (fun n : nat => @eq Z ((fix alignof (env : composite_env) (t : type) {struct t} : Z := align_attr (attr_of_type t) match t with | Tvoid => Zpos xH | Tint (I8 as i) s a => Zpos xH | Tint (I16 as i) s a => Zpos (xO xH) | Tint (I32 as i) s a => Zpos (xO (xO xH)) | Tint (IBool as i) s a => Zpos xH | Tlong s a => Archi.align_int64 | Tfloat (F32 as f) a => Zpos (xO (xO xH)) | Tfloat (F64 as f) a => Archi.align_float64 | Tpointer t0 a => if Archi.ptr64 then Zpos (xO (xO (xO xH))) else Zpos (xO (xO xH)) | Tarray t' z a => alignof env t' | Tfunction t0 t1 c => Zpos xH | Tstruct id a => match @PTree.get composite id env with | Some co => co_alignof co | None => Zpos xH end | Tunion id a => match @PTree.get composite id env with | Some co => co_alignof co | None => Zpos xH end end) env t) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z (Zpos xH) (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end (two_power_nat n)) *)
(* Goal: @ex nat (fun n : nat => @eq Z match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end (two_power_nat n)) *)
  apply IHt.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exists 0%nat; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct (env!i). apply co_alignof_two_p. exists 0%nat; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct (env!i). apply co_alignof_two_p. exists 0%nat; auto.
Qed.

Lemma alignof_pos:
  forall env t, alignof env t > 0.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. destruct (alignof_two_p env t) as [n EQ]. rewrite EQ. apply two_power_nat_pos.
Qed.

(** ** Size of a type *)

(** In the ISO C standard, size is defined only for complete
  types.  However, it is convenient that [sizeof] is a total
  function.  For [void] and function types, we follow GCC and define
  their size to be 1.  For undefined structures and unions, the size is
  arbitrarily taken to be 0.
*)

Fixpoint sizeof (env: composite_env) (t: type) : Z :=
  match t with
  | Tvoid => 1
  | Tint I8 _ _ => 1
  | Tint I16 _ _ => 2
  | Tint I32 _ _ => 4
  | Tint IBool _ _ => 1
  | Tlong _ _ => 8
  | Tfloat F32 _ => 4
  | Tfloat F64 _ => 8
  | Tpointer _ _ => if Archi.ptr64 then 8 else 4
  | Tarray t' n _ => sizeof env t' * Z.max 0 n
  | Tfunction _ _ _ => 1
  | Tstruct id _ | Tunion id _ =>
      match env!id with Some co => co_sizeof co | None => 0 end
  end.

Lemma sizeof_pos:
  forall env t, sizeof env t >= 0.
Proof.
(* Goal: forall (env : composite_env) (t : type), Z.ge (sizeof env t) Z0 *)
  induction t; simpl; try omega.
(* Goal: Z.ge match i with | I8 => Zpos xH | I16 => Zpos (xO xH) | I32 => Zpos (xO (xO xH)) | IBool => Zpos xH end Z0 *)
(* Goal: Z.ge match f with | F32 => Zpos (xO (xO xH)) | F64 => Zpos (xO (xO (xO xH))) end Z0 *)
(* Goal: Z.ge (if Archi.ptr64 then Zpos (xO (xO (xO xH))) else Zpos (xO (xO xH))) Z0 *)
(* Goal: Z.ge (Z.mul (sizeof env t) (Z.max Z0 z)) Z0 *)
(* Goal: Z.ge match @PTree.get composite i env with | Some co => co_sizeof co | None => Z0 end Z0 *)
(* Goal: Z.ge match @PTree.get composite i env with | Some co => co_sizeof co | None => Z0 end Z0 *)
  destruct i; omega.
(* Goal: Z.ge match f with | F32 => Zpos (xO (xO xH)) | F64 => Zpos (xO (xO (xO xH))) end Z0 *)
(* Goal: Z.ge (if Archi.ptr64 then Zpos (xO (xO (xO xH))) else Zpos (xO (xO xH))) Z0 *)
(* Goal: Z.ge (Z.mul (sizeof env t) (Z.max Z0 z)) Z0 *)
(* Goal: Z.ge match @PTree.get composite i env with | Some co => co_sizeof co | None => Z0 end Z0 *)
(* Goal: Z.ge match @PTree.get composite i env with | Some co => co_sizeof co | None => Z0 end Z0 *)
  destruct f; omega.
(* Goal: Z.ge (if Archi.ptr64 then Zpos (xO (xO (xO xH))) else Zpos (xO (xO xH))) Z0 *)
(* Goal: Z.ge (Z.mul (sizeof env t) (Z.max Z0 z)) Z0 *)
(* Goal: Z.ge match @PTree.get composite i env with | Some co => co_sizeof co | None => Z0 end Z0 *)
(* Goal: Z.ge match @PTree.get composite i env with | Some co => co_sizeof co | None => Z0 end Z0 *)
  destruct Archi.ptr64; omega.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega.
(* Goal: Z.divide match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end match @PTree.get composite i env with | Some co => co_sizeof co | None => Z0 end *)
  destruct (env!i). apply co_sizeof_pos. omega.
(* Goal: Z.divide match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end match @PTree.get composite i env with | Some co => co_sizeof co | None => Z0 end *)
  destruct (env!i). apply co_sizeof_pos. omega.
Qed.

(** The size of a type is an integral multiple of its alignment,
  unless the alignment was artificially increased with the [__Alignas]
  attribute. *)

Fixpoint naturally_aligned (t: type) : Prop :=
  attr_alignas (attr_of_type t) = None /\
  match t with
  | Tarray t' _ _ => naturally_aligned t'
  | _ => True
  end.

Lemma sizeof_alignof_compat:
  forall env t, naturally_aligned t -> (alignof env t | sizeof env t).
Proof.
(* Goal: forall (env : composite_env) (t : type) (_ : naturally_aligned t), Z.divide (alignof env t) (sizeof env t) *)
  induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl.
- apply Z.divide_refl.
- destruct i; apply Z.divide_refl.
- exists (8 / Archi.align_int64). unfold Archi.align_int64; destruct Archi.ptr64; reflexivity.
- destruct f. apply Z.divide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity.
- apply Z.divide_refl.
- apply Z.divide_mul_l; auto.
- apply Z.divide_refl.
- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r.
- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r.
Qed.

(** ** Size and alignment for composite definitions *)

(** The alignment for a structure or union is the max of the alignment
  of its members. *)

Fixpoint alignof_composite (env: composite_env) (m: members) : Z :=
  match m with
  | nil => 1
  | (id, t) :: m' => Z.max (alignof env t) (alignof_composite env m')
  end.

(** The size of a structure corresponds to its layout: fields are
  laid out consecutively, and padding is inserted to align
  each field to the alignment for its type. *)

Fixpoint sizeof_struct (env: composite_env) (cur: Z) (m: members) : Z :=
  match m with
  | nil => cur
  | (id, t) :: m' => sizeof_struct env (align cur (alignof env t) + sizeof env t) m'
  end.

(** The size of an union is the max of the sizes of its members. *)

Fixpoint sizeof_union (env: composite_env) (m: members) : Z :=
  match m with
  | nil => 0
  | (id, t) :: m' => Z.max (sizeof env t) (sizeof_union env m')
  end.

Lemma alignof_composite_two_p:
  forall env m, exists n, alignof_composite env m = two_power_nat n.
Proof.
(* Goal: forall (env : composite_env) (m : members), @ex nat (fun n : nat => @eq Z (alignof_composite env m) (two_power_nat n)) *)
  induction m as [|[id t]]; simpl.
- exists 0%nat; auto.
- apply Z.max_case; auto. apply alignof_two_p.
Qed.

Lemma alignof_composite_pos:
  forall env m a, align_attr a (alignof_composite env m) > 0.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros.
  exploit align_attr_two_p. apply (alignof_composite_two_p env m).
  instantiate (1 := a). intros [n EQ].
(* Goal: Z.gt (two_power_nat n) Z0 *)
  rewrite EQ; apply two_power_nat_pos.
Qed.

Lemma sizeof_struct_incr:
  forall env m cur, cur <= sizeof_struct env cur m.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction m as [|[id t]]; simpl; intros.
- omega.
- apply Z.le_trans with (align cur (alignof env t)).
(* Goal: Z.le pos (align pos (alignof env t)) *)
(* Goal: Z.le (align pos (alignof env t)) (Z.add (align pos (alignof env t)) (sizeof env t)) *)
  apply align_le. apply alignof_pos.
(* Goal: Z.le (align cur (alignof env t)) (sizeof_struct env (Z.add (align cur (alignof env t)) (sizeof env t)) m) *)
  apply Z.le_trans with (align cur (alignof env t) + sizeof env t).
(* Goal: forall _ : le (rank_type ce t1) (rank_members ce (co_members co)), lt (rank_type ce t1) (S (rank_members ce (co_members co))) *)
  generalize (sizeof_pos env t); omega.
(* Goal: Z.le (Z.add (align cur (alignof env t)) (sizeof env t)) (sizeof_struct env (Z.add (align cur (alignof env t)) (sizeof env t)) m) *)
  apply IHm.
Qed.

Lemma sizeof_union_pos:
  forall env m, 0 <= sizeof_union env m.
Proof.
(* Goal: le (rank_type ce t) (Init.Nat.max (rank_type ce b) (rank_members ce m)) *)
  induction m as [|[id t]]; simpl; xomega.
Qed.

(** ** Byte offset for a field of a structure *)

(** [field_offset env id fld] returns the byte offset for field [id]
  in a structure whose members are [fld].  Fields are laid out
  consecutively, and padding is inserted to align each field to the
  alignment for its type. *)

Fixpoint field_offset_rec (env: composite_env) (id: ident) (fld: members) (pos: Z)
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
                          {struct fld} : res Z :=
  match fld with
  | nil => Error (MSG "Unknown field " :: CTX id :: nil)
  | (id', t) :: fld' =>
      if ident_eq id id'
      then OK (align pos (alignof env t))
      else field_offset_rec env id fld' (align pos (alignof env t) + sizeof env t)
  end.

Definition field_offset (env: composite_env) (id: ident) (fld: members) : res Z :=
  field_offset_rec env id fld 0.

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Fixpoint field_type (id: ident) (fld: members) {struct fld} : res type :=
  match fld with
  | nil => Error (MSG "Unknown field " :: CTX id :: nil)
  | (id', t) :: fld' => if ident_eq id id' then OK t else field_type id fld'
  end.

(** Some sanity checks about field offsets.  First, field offsets are
  within the range of acceptable offsets. *)

Remark field_offset_rec_in_range:
  forall env id ofs ty fld pos,
  field_offset_rec env id fld pos = OK ofs -> field_type id fld = OK ty ->
  pos <= ofs /\ ofs + sizeof env ty <= sizeof_struct env pos fld.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros until ty. induction fld as [|[i t]]; simpl; intros.
- discriminate.
- destruct (ident_eq id i); intros.
(* Goal: @ex composite (fun co : composite => and (@eq (option composite) (@PTree.get composite id env) (@Some composite co)) (and (@eq members (co_members co) m) (and (@eq attr (co_attr co) a) (@eq struct_or_union (co_su co) su)))) *)
  inv H. inv H0. split.
(* Goal: Z.le pos (align pos (alignof env t)) *)
(* Goal: Z.le (align pos (alignof env t)) (Z.add (align pos (alignof env t)) (sizeof env t)) *)
  apply align_le. apply alignof_pos. apply sizeof_struct_incr.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exploit IHfld; eauto. intros [A B]. split; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  eapply Z.le_trans; eauto. apply Z.le_trans with (align pos (alignof env t)).
(* Goal: forall _ : le (rank_type ce t1) (rank_members ce (co_members co)), lt (rank_type ce t1) (S (rank_members ce (co_members co))) *)
  apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega.
Qed.

Lemma field_offset_in_range:
  forall env fld id ofs ty,
  field_offset env id fld = OK ofs -> field_type id fld = OK ty ->
  0 <= ofs /\ ofs + sizeof env ty <= sizeof_struct env 0 fld.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. eapply field_offset_rec_in_range; eauto.
Qed.

(** Second, two distinct fields do not overlap *)

Lemma field_offset_no_overlap:
  forall env id1 ofs1 ty1 id2 ofs2 ty2 fld,
  field_offset env id1 fld = OK ofs1 -> field_type id1 fld = OK ty1 ->
  field_offset env id2 fld = OK ofs2 -> field_type id2 fld = OK ty2 ->
  id1 <> id2 ->
  ofs1 + sizeof env ty1 <= ofs2 \/ ofs2 + sizeof env ty2 <= ofs1.
Proof.
  intros until fld. unfold field_offset. generalize 0 as pos.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction fld as [|[i t]]; simpl; intros.
- discriminate.
- destruct (ident_eq id1 i); destruct (ident_eq id2 i).
+ congruence.
(* Goal: and (Z.le pos (align pos (alignof env t))) (Z.le (Z.add (align pos (alignof env t)) (sizeof env ty)) (sizeof_struct env (Z.add (align pos (alignof env t)) (sizeof env t)) fld)) *)
(* Goal: and (Z.le pos ofs) (Z.le (Z.add ofs (sizeof env ty)) (sizeof_struct env (Z.add (align pos (alignof env t)) (sizeof env t)) fld)) *)
+ subst i. inv H; inv H0.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exploit field_offset_rec_in_range. eexact H1. eauto. tauto.
+ subst i. inv H1; inv H2.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exploit field_offset_rec_in_range. eexact H. eauto. tauto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
+ eapply IHfld; eauto.
Qed.

(** Third, if a struct is a prefix of another, the offsets of common fields
    are the same. *)

Lemma field_offset_prefix:
  forall env id ofs fld2 fld1,
  field_offset env id fld1 = OK ofs ->
  field_offset env id (fld1 ++ fld2) = OK ofs.
Proof.
(* Goal: forall (_ : @eq (res Z) (field_offset env id fld) (@OK Z ofs)) (_ : @eq (res type) (field_type id fld) (@OK type ty)), Z.divide (alignof env ty) ofs *)
  intros until fld1. unfold field_offset. generalize 0 as pos.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction fld1 as [|[i t]]; simpl; intros.
- discriminate.
- destruct (ident_eq id i); auto.
Qed.

(** Fourth, the position of each field respects its alignment. *)

Lemma field_offset_aligned:
  forall env id fld ofs ty,
  field_offset env id fld = OK ofs -> field_type id fld = OK ty ->
  (alignof env ty | ofs).
Proof.
(* Goal: forall (env : composite_env) (id : ident) (fld : members) (ofs : Z) (ty : type) (_ : @eq (res Z) (field_offset env id fld) (@OK Z ofs)) (_ : @eq (res type) (field_type id fld) (@OK type ty)), Z.divide (alignof env ty) ofs *)
  intros until ty. unfold field_offset. generalize 0 as pos. revert fld.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction fld as [|[i t]]; simpl; intros.
- discriminate.
- destruct (ident_eq id i).
(* Goal: Z.gt (alignof env ty) Z0 *)
+ inv H; inv H0. apply align_divides. apply alignof_pos.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
+ eauto.
Qed.

(** ** Access modes *)

(** The [access_mode] function describes how a l-value of the given
type must be accessed:
- [By_value ch]: access by value, i.e. by loading from the address
  of the l-value using the memory chunk [ch];
- [By_reference]: access by reference, i.e. by just returning
  the address of the l-value (used for arrays and functions);
- [By_copy]: access is by reference, assignment is by copy
  (used for [struct] and [union] types)
- [By_nothing]: no access is possible, e.g. for the [void] type.
*)

Inductive mode: Type :=
  | By_value: memory_chunk -> mode
  | By_reference: mode
  | By_copy: mode
  | By_nothing: mode.

Definition access_mode (ty: type) : mode :=
  match ty with
  | Tint I8 Signed _ => By_value Mint8signed
  | Tint I8 Unsigned _ => By_value Mint8unsigned
  | Tint I16 Signed _ => By_value Mint16signed
  | Tint I16 Unsigned _ => By_value Mint16unsigned
  | Tint I32 _ _ => By_value Mint32
  | Tint IBool _ _ => By_value Mint8unsigned
  | Tlong _ _ => By_value Mint64
  | Tfloat F32 _ => By_value Mfloat32
  | Tfloat F64 _ => By_value Mfloat64
  | Tvoid => By_nothing
  | Tpointer _ _ => By_value Mptr
  | Tarray _ _ _ => By_reference
  | Tfunction _ _ _ => By_reference
  | Tstruct _ _ => By_copy
  | Tunion _ _ => By_copy
end.

(** For the purposes of the semantics and the compiler, a type denotes
  a volatile access if it carries the [volatile] attribute and it is
  accessed by value. *)

Definition type_is_volatile (ty: type) : bool :=
  match access_mode ty with
  | By_value _ => attr_volatile (attr_of_type ty)
  | _          => false
  end.

(** ** Alignment for block copy operations *)

(** A variant of [alignof] for use in block copy operations.
  Block copy operations do not support alignments greater than 8,
  and require the size to be an integral multiple of the alignment. *)

Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z :=
  match t with
  | Tvoid => 1
  | Tint I8 _ _ => 1
  | Tint I16 _ _ => 2
  | Tint I32 _ _ => 4
  | Tint IBool _ _ => 1
  | Tlong _ _ => 8
  | Tfloat F32 _ => 4
  | Tfloat F64 _ => 8
  | Tpointer _ _ => if Archi.ptr64 then 8 else 4
  | Tarray t' _ _ => alignof_blockcopy env t'
  | Tfunction _ _ _ => 1
  | Tstruct id _ | Tunion id _ =>
      match env!id with
      | Some co => Z.min 8 (co_alignof co)
      | None => 1
      end
  end.

Lemma alignof_blockcopy_1248:
  forall env ty, let a := alignof_blockcopy env ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8.
Proof.
  assert (X: forall co, let a := Z.min 8 (co_alignof co) in
             a = 1 \/ a = 2 \/ a = 4 \/ a = 8).
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  {
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
    intros. destruct (co_alignof_two_p co) as [n EQ]. unfold a; rewrite EQ.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    destruct n; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    destruct n; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    destruct n; auto.
(* Goal: or (@eq Z (Z.min (Zpos (xO (xO (xO xH)))) (two_power_nat (S (S (S n))))) (Zpos xH)) (or (@eq Z (Z.min (Zpos (xO (xO (xO xH)))) (two_power_nat (S (S (S n))))) (Zpos (xO xH))) (or (@eq Z (Z.min (Zpos (xO (xO (xO xH)))) (two_power_nat (S (S (S n))))) (Zpos (xO (xO xH)))) (@eq Z (Z.min (Zpos (xO (xO (xO xH)))) (two_power_nat (S (S (S n))))) (Zpos (xO (xO (xO xH))))))) *)
    right; right; right. apply Z.min_l.
(* Goal: Z.le (Zpos (xO (xO (xO xH)))) (two_power_nat (S (S (S n)))) *)
    rewrite two_power_nat_two_p. rewrite ! Nat2Z.inj_succ.
(* Goal: forall _ : le (rank_type ce t1) (rank_members ce (co_members co)), lt (rank_type ce t1) (S (rank_members ce (co_members co))) *)
    change 8 with (two_p 3). apply two_p_monotone. omega.
  }
(* Goal: forall (env : composite_env) (ty : type), let a := alignof_blockcopy env ty in or (@eq Z a (Zpos xH)) (or (@eq Z a (Zpos (xO xH))) (or (@eq Z a (Zpos (xO (xO xH)))) (@eq Z a (Zpos (xO (xO (xO xH))))))) *)
  induction ty; simpl.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct i; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct f; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct Archi.ptr64; auto.
(* Goal: or (@eq Z (alignof_blockcopy env ty) (Zpos xH)) (or (@eq Z (alignof_blockcopy env ty) (Zpos (xO xH))) (or (@eq Z (alignof_blockcopy env ty) (Zpos (xO (xO xH)))) (@eq Z (alignof_blockcopy env ty) (Zpos (xO (xO (xO xH))))))) *)
(* Goal: or (@eq Z (Zpos xH) (Zpos xH)) (or (@eq Z (Zpos xH) (Zpos (xO xH))) (or (@eq Z (Zpos xH) (Zpos (xO (xO xH)))) (@eq Z (Zpos xH) (Zpos (xO (xO (xO xH))))))) *)
(* Goal: or (@eq Z match @PTree.get composite i env with | Some co => Z.min (Zpos (xO (xO (xO xH)))) (co_alignof co) | None => Zpos xH end (Zpos xH)) (or (@eq Z match @PTree.get composite i env with | Some co => Z.min (Zpos (xO (xO (xO xH)))) (co_alignof co) | None => Zpos xH end (Zpos (xO xH))) (or (@eq Z match @PTree.get composite i env with | Some co => Z.min (Zpos (xO (xO (xO xH)))) (co_alignof co) | None => Zpos xH end (Zpos (xO (xO xH)))) (@eq Z match @PTree.get composite i env with | Some co => Z.min (Zpos (xO (xO (xO xH)))) (co_alignof co) | None => Zpos xH end (Zpos (xO (xO (xO xH))))))) *)
(* Goal: or (@eq Z match @PTree.get composite i env with | Some co => Z.min (Zpos (xO (xO (xO xH)))) (co_alignof co) | None => Zpos xH end (Zpos xH)) (or (@eq Z match @PTree.get composite i env with | Some co => Z.min (Zpos (xO (xO (xO xH)))) (co_alignof co) | None => Zpos xH end (Zpos (xO xH))) (or (@eq Z match @PTree.get composite i env with | Some co => Z.min (Zpos (xO (xO (xO xH)))) (co_alignof co) | None => Zpos xH end (Zpos (xO (xO xH)))) (@eq Z match @PTree.get composite i env with | Some co => Z.min (Zpos (xO (xO (xO xH)))) (co_alignof co) | None => Zpos xH end (Zpos (xO (xO (xO xH))))))) *)
  apply IHty.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct (env!i); auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct (env!i); auto.
Qed.

Lemma alignof_blockcopy_pos:
  forall env ty, alignof_blockcopy env ty > 0.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. generalize (alignof_blockcopy_1248 env ty). simpl. intuition omega.
Qed.

Lemma sizeof_alignof_blockcopy_compat:
  forall env ty, (alignof_blockcopy env ty | sizeof env ty).
Proof.
  assert (X: forall co, (Z.min 8 (co_alignof co) | co_sizeof co)).
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  {
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
    intros. apply Z.divide_trans with (co_alignof co). 2: apply co_sizeof_alignof.
(* Goal: Z.gt (alignof env t) Z0 *)
    destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ.
(* Goal: Z.divide (Zpos xH) (Zpos xH) *)
    destruct n. apply Z.divide_refl.
(* Goal: Z.divide (Zpos xH) (Zpos xH) *)
    destruct n. apply Z.divide_refl.
(* Goal: Z.divide (Zpos xH) (Zpos xH) *)
    destruct n. apply Z.divide_refl.
    apply Z.min_case.
    exists (two_p (Z.of_nat n)).
(* Goal: Z.le (Zpos (xO (xO (xO xH)))) (two_p (Z.succ (Z.succ (Z.succ (Z.of_nat n))))) *)
    change 8 with (two_p 3).
    rewrite <- two_p_is_exp by omega.
(* Goal: Z.le (Zpos (xO (xO (xO xH)))) (two_power_nat (S (S (S n)))) *)
    rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. omega.
(* Goal: Z.divide (Zpos xH) (Zpos xH) *)
    apply Z.divide_refl.
  }
(* Goal: forall (env : composite_env) (ty : type), let a := alignof_blockcopy env ty in or (@eq Z a (Zpos xH)) (or (@eq Z a (Zpos (xO xH))) (or (@eq Z a (Zpos (xO (xO xH)))) (@eq Z a (Zpos (xO (xO (xO xH))))))) *)
  induction ty; simpl.
(* Goal: Z.divide (Zpos xH) (Zpos xH) *)
  apply Z.divide_refl.
(* Goal: Z.divide (Zpos xH) (Zpos xH) *)
  apply Z.divide_refl.
(* Goal: Z.divide (Zpos xH) (Zpos xH) *)
  apply Z.divide_refl.
(* Goal: Z.divide (Zpos xH) (Zpos xH) *)
  apply Z.divide_refl.
(* Goal: Z.divide (Zpos xH) (Zpos xH) *)
  apply Z.divide_refl.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  apply Z.divide_mul_l. auto.
(* Goal: Z.divide (Zpos xH) (Zpos xH) *)
  apply Z.divide_refl.
(* Goal: Z.divide match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end match @PTree.get composite i env with | Some co => co_sizeof co | None => Z0 end *)
  destruct (env!i). apply X. apply Z.divide_0_r.
(* Goal: Z.divide match @PTree.get composite i env with | Some co => co_alignof co | None => Zpos xH end match @PTree.get composite i env with | Some co => co_sizeof co | None => Z0 end *)
  destruct (env!i). apply X. apply Z.divide_0_r.
Qed.

(** Type ranks *)

(** The rank of a type is a nonnegative integer that measures the direct nesting
  of arrays, struct and union types.  It does not take into account indirect
  nesting such as a struct type that appears under a pointer or function type.
  Type ranks ensure that type expressions (ignoring pointer and function types)
  have an inductive structure. *)

Fixpoint rank_type (ce: composite_env) (t: type) : nat :=
  match t with
  | Tarray t' _ _ => S (rank_type ce t')
  | Tstruct id _ | Tunion id _ =>
      match ce!id with
      | None => O
      | Some co => S (co_rank co)
      end
  | _ => O
  end.

Fixpoint rank_members (ce: composite_env) (m: members) : nat :=
  match m with
  | nil => 0%nat
  | (id, t) :: m => Init.Nat.max (rank_type ce t) (rank_members ce m)
  end.

(** ** C types and back-end types *)

(** Extracting a type list from a function parameter declaration. *)

Fixpoint type_of_params (params: list (ident * type)) : typelist :=
  match params with
  | nil => Tnil
  | (id, ty) :: rem => Tcons ty (type_of_params rem)
  end.

(** Translating C types to Cminor types and function signatures. *)

Definition typ_of_type (t: type) : AST.typ :=
  match t with
  | Tvoid => AST.Tint
  | Tint _ _ _ => AST.Tint
  | Tlong _ _ => AST.Tlong
  | Tfloat F32 _ => AST.Tsingle
  | Tfloat F64 _ => AST.Tfloat
  | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tptr
  end.

Definition opttyp_of_type (t: type) : option AST.typ :=
  if type_eq t Tvoid then None else Some (typ_of_type t).

Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
  match tl with
  | Tnil => nil
  | Tcons hd tl => typ_of_type hd :: typlist_of_typelist tl
  end.

Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature :=
  mksignature (typlist_of_typelist args) (opttyp_of_type res) cc.

(** * Construction of the composite environment *)

Definition sizeof_composite (env: composite_env) (su: struct_or_union) (m: members) : Z :=
  match su with
  | Struct => sizeof_struct env 0 m
  | Union  => sizeof_union env m
  end.

Lemma sizeof_composite_pos:
  forall env su m, 0 <= sizeof_composite env su m.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. destruct su; simpl.
(* Goal: Z.le Z0 (sizeof_struct env Z0 m) *)
(* Goal: Z.le Z0 (sizeof_union env m) *)
  apply sizeof_struct_incr.
(* Goal: Z.le Z0 (sizeof_union env m) *)
  apply sizeof_union_pos.
Qed.

Fixpoint complete_members (env: composite_env) (m: members) : bool :=
  match m with
  | nil => true
  | (id, t) :: m' => complete_type env t && complete_members env m'
  end.

Lemma complete_member:
  forall env id t m,
  In (id, t) m -> complete_members env m = true -> complete_type env t = true.
Proof.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  induction m as [|[id1 t1] m]; simpl; intuition auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  InvBooleans; inv H1; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  InvBooleans; eauto.
Qed.

(** Convert a composite definition to its internal representation.
  The size and alignment of the composite are determined at this time.
  The alignment takes into account the [__Alignas] attributes
  associated with the definition.  The size is rounded up to a multiple
  of the alignment.

  The conversion fails if a type of a member is not complete.  This rules
  out incorrect recursive definitions such as
<<
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
    struct s { int x; struct s next; }
>>
  Here, when we process the definition of [struct s], the identifier [s]
  is not bound yet in the composite environment, hence field [next]
  has an incomplete type.  However, recursions that go through a pointer type
  are correctly handled:
<<
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
    struct s { int x; struct s * next; }
>>
  Here, [next] has a pointer type, which is always complete, even though
  [s] is not yet bound to a composite.
*)

Program Definition composite_of_def
     (env: composite_env) (id: ident) (su: struct_or_union) (m: members) (a: attr)
     : res composite :=
  match env!id, complete_members env m return _ with
  | Some _, _ =>
      Error (MSG "Multiple definitions of struct or union " :: CTX id :: nil)
  | None, false =>
      Error (MSG "Incomplete struct or union " :: CTX id :: nil)
  | None, true =>
      let al := align_attr a (alignof_composite env m) in
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
      OK {| co_su := su;
            co_members := m;
            co_attr := a;
            co_sizeof := align (sizeof_composite env su m) al;
            co_alignof := al;
            co_rank := rank_members env m;
            co_sizeof_pos := _;
            co_alignof_two_p := _;
            co_sizeof_alignof := _ |}
  end.
Next Obligation.
  apply Z.le_ge. eapply Z.le_trans. eapply sizeof_composite_pos.
  apply align_le; apply alignof_composite_pos.
Defined.
Next Obligation.
(* Goal: @ex nat (fun n : nat => @eq Z (align_attr a (alignof_composite env m)) (two_power_nat n)) *)
  apply align_attr_two_p. apply alignof_composite_two_p.
Defined.
Next Obligation.
(* Goal: Z.divide (align_attr a (alignof_composite env m)) (align (sizeof_composite env su m) (align_attr a (alignof_composite env m))) *)
  apply align_divides. apply alignof_composite_pos.
Defined.

(** The composite environment for a program is obtained by entering
  its composite definitions in sequence.  The definitions are assumed
  to be listed in dependency order: the definition of a composite
  must precede all uses of this composite, unless the use is under
  a pointer or function type. *)

Local Open Scope error_monad_scope.

Fixpoint add_composite_definitions (env: composite_env) (defs: list composite_definition) : res composite_env :=
  match defs with
  | nil => OK env
  | Composite id su m a :: defs =>
      do co <- composite_of_def env id su m a;
      add_composite_definitions (PTree.set id co env) defs
  end.

Definition build_composite_env (defs: list composite_definition) :=
  add_composite_definitions (PTree.empty _) defs.

(** Stability properties for alignments, sizes, and ranks.  If the type is
  complete in a composite environment [env], its size, alignment, and rank
  are unchanged if we add more definitions to [env]. *)

Section STABILITY.

Variables env env': composite_env.
Hypothesis extends: forall id co, env!id = Some co -> env'!id = Some co.

Lemma alignof_stable:
  forall t, complete_type env t = true -> alignof env' t = alignof env t.
Proof.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  induction t; simpl; intros; f_equal; auto.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (env!i) as [co|] eqn:E; try discriminate.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  erewrite extends by eauto. auto.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (env!i) as [co|] eqn:E; try discriminate.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  erewrite extends by eauto. auto.
Qed.

Lemma sizeof_stable:
  forall t, complete_type env t = true -> sizeof env' t = sizeof env t.
Proof.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  induction t; simpl; intros; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  rewrite IHt by auto. auto.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (env!i) as [co|] eqn:E; try discriminate.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  erewrite extends by eauto. auto.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (env!i) as [co|] eqn:E; try discriminate.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  erewrite extends by eauto. auto.
Qed.

Lemma complete_type_stable:
  forall t, complete_type env t = true -> complete_type env' t = true.
Proof.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  induction t; simpl; intros; auto.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (env!i) as [co|] eqn:E; try discriminate.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  erewrite extends by eauto. auto.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (env!i) as [co|] eqn:E; try discriminate.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  erewrite extends by eauto. auto.
Qed.

Lemma rank_type_stable:
  forall t, complete_type env t = true -> rank_type env' t = rank_type env t.
Proof.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  induction t; simpl; intros; auto.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (env!i) as [co|] eqn:E; try discriminate.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  erewrite extends by eauto. auto.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (env!i) as [co|] eqn:E; try discriminate.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  erewrite extends by eauto. auto.
Qed.

Lemma alignof_composite_stable:
  forall m, complete_members env m = true -> alignof_composite env' m = alignof_composite env m.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction m as [|[id t]]; simpl; intros.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  InvBooleans. rewrite alignof_stable by auto. rewrite IHm by auto. auto.
Qed.

Lemma sizeof_struct_stable:
  forall m pos, complete_members env m = true -> sizeof_struct env' pos m = sizeof_struct env pos m.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction m as [|[id t]]; simpl; intros.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  InvBooleans. rewrite alignof_stable by auto. rewrite sizeof_stable by auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  rewrite IHm by auto. auto.
Qed.

Lemma sizeof_union_stable:
  forall m, complete_members env m = true -> sizeof_union env' m = sizeof_union env m.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction m as [|[id t]]; simpl; intros.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  InvBooleans. rewrite sizeof_stable by auto. rewrite IHm by auto. auto.
Qed.

Lemma sizeof_composite_stable:
  forall su m, complete_members env m = true -> sizeof_composite env' su m = sizeof_composite env su m.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. destruct su; simpl.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  apply sizeof_struct_stable; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  apply sizeof_union_stable; auto.
Qed.

Lemma complete_members_stable:
  forall m, complete_members env m = true -> complete_members env' m = true.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction m as [|[id t]]; simpl; intros.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  InvBooleans. rewrite complete_type_stable by auto. rewrite IHm by auto. auto.
Qed.

Lemma rank_members_stable:
  forall m, complete_members env m = true -> rank_members env' m = rank_members env m.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction m as [|[id t]]; simpl; intros.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  InvBooleans. f_equal; auto. apply rank_type_stable; auto.
Qed.

End STABILITY.

Lemma add_composite_definitions_incr:
  forall id co defs env1 env2,
  add_composite_definitions env1 defs = OK env2 ->
  env1!id = Some co -> env2!id = Some co.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction defs; simpl; intros.
- inv H; auto.
- destruct a; monadInv H.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  eapply IHdefs; eauto. rewrite PTree.gso; auto.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  red; intros; subst id0. unfold composite_of_def in EQ. rewrite H0 in EQ; discriminate.
Qed.

(** It follows that the sizes and alignments contained in the composite
  environment produced by [build_composite_env] are consistent with
  the sizes and alignments of the members of the composite types. *)

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Record composite_consistent (env: composite_env) (co: composite) : Prop := {
  co_consistent_complete:
     complete_members env (co_members co) = true;
  co_consistent_alignof:
     co_alignof co = align_attr (co_attr co) (alignof_composite env (co_members co));
  co_consistent_sizeof:
     co_sizeof co = align (sizeof_composite env (co_su co) (co_members co)) (co_alignof co);
  co_consistent_rank:
     co_rank co = rank_members env (co_members co)
}.

Definition composite_env_consistent (env: composite_env) : Prop :=
  forall id co, env!id = Some co -> composite_consistent env co.

Lemma composite_consistent_stable:
  forall (env env': composite_env)
         (EXTENDS: forall id co, env!id = Some co -> env'!id = Some co)
         co,
  composite_consistent env co -> composite_consistent env' co.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. destruct H as [A B C D]. constructor. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  eapply complete_members_stable; eauto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  symmetry; rewrite B. f_equal. apply alignof_composite_stable; auto. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  symmetry; rewrite C. f_equal. apply sizeof_composite_stable; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  symmetry; rewrite D. apply rank_members_stable; auto.
Qed.

Lemma composite_of_def_consistent:
  forall env id su m a co,
  composite_of_def env id su m a = OK co ->
  composite_consistent env co.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  unfold composite_of_def; intros. 
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (env!id); try discriminate. destruct (complete_members env m) eqn:C; inv H.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  constructor; auto.
Qed. 

Theorem build_composite_env_consistent:
  forall defs env, build_composite_env defs = OK env -> composite_env_consistent env.
Proof.
  cut (forall defs env0 env,
       add_composite_definitions env0 defs = OK env ->
       composite_env_consistent env0 ->
       composite_env_consistent env).
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. eapply H; eauto. red; intros. rewrite PTree.gempty in H1; discriminate.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction defs as [|d1 defs]; simpl; intros.
- inv H; auto.
- destruct d1; monadInv H.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  eapply IHdefs; eauto.
(* Goal: composite_env_consistent (@PTree.set composite id x env0) *)
  set (env1 := PTree.set id x env0) in *.
(* Goal: composite_env_consistent env1 *)
  assert (env0!id = None). 
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  { unfold composite_of_def in EQ. destruct (env0!id). discriminate. auto. }
  assert (forall id1 co1, env0!id1 = Some co1 -> env1!id1 = Some co1).
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  { intros. unfold env1. rewrite PTree.gso; auto. congruence. }
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  red; intros. apply composite_consistent_stable with env0; auto.
(* Goal: composite_consistent env0 co *)
  unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id).
+ subst id0. inversion H2; clear H2. subst co.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  eapply composite_of_def_consistent; eauto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
+ eapply H0; eauto. 
Qed.

(** Moreover, every composite definition is reflected in the composite environment. *)

Theorem build_composite_env_charact:
  forall id su m a defs env,
  build_composite_env defs = OK env ->
  In (Composite id su m a) defs ->
  exists co, env!id = Some co /\ co_members co = m /\ co_attr co = a /\ co_su co = su.
Proof.
(* Goal: forall (id : ident) (su : struct_or_union) (m : members) (a : attr) (defs : list composite_definition) (env : composite_env) (_ : @eq (res composite_env) (build_composite_env defs) (@OK composite_env env)) (_ : @In composite_definition (Composite id su m a) defs), @ex composite (fun co : composite => and (@eq (option composite) (@PTree.get composite id env) (@Some composite co)) (and (@eq members (co_members co) m) (and (@eq attr (co_attr co) a) (@eq struct_or_union (co_su co) su)))) *)
  intros until defs. unfold build_composite_env. generalize (PTree.empty composite) as env0.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  revert defs. induction defs as [|d1 defs]; simpl; intros.
- contradiction.
- destruct d1; monadInv H.
(* Goal: @ex composite (fun co : composite => and (@eq (option composite) (@PTree.get composite id env) (@Some composite co)) (and (@eq members (co_members co) m) (and (@eq attr (co_attr co) a) (@eq struct_or_union (co_su co) su)))) *)
  destruct H0; [idtac|eapply IHdefs;eauto]. inv H.
(* Goal: forall _ : or (@eq (option composite) (@PTree.get composite id (@PTree.set composite id0 x env)) (@Some composite co)) (@In composite_definition (Composite id (co_su co) (co_members co) (co_attr co)) l), or (@eq (option composite) (@PTree.get composite id env) (@Some composite co)) (or (@eq composite_definition (Composite id0 su m a) (Composite id (co_su co) (co_members co) (co_attr co))) (@In composite_definition (Composite id (co_su co) (co_members co) (co_attr co)) l)) *)
  unfold composite_of_def in EQ.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (env0!id) eqn:E; try discriminate.
(* Goal: @ex composite (fun co : composite => and (@eq (option composite) (@PTree.get composite id env) (@Some composite co)) (and (@eq members (co_members co) m) (and (@eq attr (co_attr co) a) (@eq struct_or_union (co_su co) su)))) *)
  destruct (complete_members env0 m) eqn:C; simplify_eq EQ. clear EQ; intros EQ.
(* Goal: @ex composite (fun co : composite => and (@eq (option composite) (@PTree.get composite id env) (@Some composite co)) (and (@eq members (co_members co) m) (and (@eq attr (co_attr co) a) (@eq struct_or_union (co_su co) su)))) *)
  exists x.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  split. eapply add_composite_definitions_incr; eauto. apply PTree.gss.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  subst x; auto.
Qed.

Theorem build_composite_env_domain:
  forall env defs id co,
  build_composite_env defs = OK env ->
  env!id = Some co ->
  In (Composite id (co_su co) (co_members co) (co_attr co)) defs.
Proof.
(* Goal: forall (env : composite_env) (defs : list composite_definition) (id : positive) (co : composite) (_ : @eq (res composite_env) (build_composite_env defs) (@OK composite_env env)) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @In composite_definition (Composite id (co_su co) (co_members co) (co_attr co)) defs *)
  intros env0 defs0 id co.
  assert (REC: forall l env env',
    add_composite_definitions env l = OK env' ->
    env'!id = Some co ->
    env!id = Some co \/ In (Composite id (co_su co) (co_members co) (co_attr co)) l).
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  { induction l; simpl; intros. 
  - inv H; auto.
  - destruct a; monadInv H. exploit IHl; eauto.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
    unfold composite_of_def in EQ. destruct (env!id0) eqn:E; try discriminate.
(* Goal: forall (_ : @eq composite (Build_composite su m a (align (sizeof_composite env su m) (align_attr a (alignof_composite env m))) (align_attr a (alignof_composite env m)) (rank_members env m) (composite_of_def_obligation_1 env su m a) (composite_of_def_obligation_2 env m a) (composite_of_def_obligation_3 env su m a)) x) (_ : or (@eq (option composite) (@PTree.get composite id (@PTree.set composite id0 x env)) (@Some composite co)) (@In composite_definition (Composite id (co_su co) (co_members co) (co_attr co)) l)), or (@eq (option composite) (@PTree.get composite id env) (@Some composite co)) (or (@eq composite_definition (Composite id0 su m a) (Composite id (co_su co) (co_members co) (co_attr co))) (@In composite_definition (Composite id (co_su co) (co_members co) (co_attr co)) l)) *)
    destruct (complete_members env m) eqn:C; simplify_eq EQ. clear EQ; intros EQ.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    rewrite PTree.gsspec. intros [A|A]; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    destruct (peq id id0); auto.
    inv A. rewrite <- H0; auto.
  }
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. exploit REC; eauto. rewrite PTree.gempty. intuition congruence.
Qed.

(** As a corollay, in a consistent environment, the rank of a composite type
  is strictly greater than the ranks of its member types. *)

Remark rank_type_members:
  forall ce id t m, In (id, t) m -> (rank_type ce t <= rank_members ce m)%nat.
Proof.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  induction m; simpl; intros; intuition auto.
(* Goal: le (rank_type ce t) (Init.Nat.max (rank_type ce b) (rank_members ce m)) *)
  subst a. xomega.
(* Goal: le (rank_type ce t) (Init.Nat.max (rank_type ce b) (rank_members ce m)) *)
  xomega.
Qed.

Lemma rank_struct_member:
  forall ce id a co id1 t1,
  composite_env_consistent ce ->
  ce!id = Some co ->
  In (id1, t1) (co_members co) ->
  (rank_type ce t1 < rank_type ce (Tstruct id a))%nat.
Proof.
(* Goal: forall _ : let a := alignof_blockcopy env ty in or (@eq Z a (Zpos xH)) (or (@eq Z a (Zpos (xO xH))) (or (@eq Z a (Zpos (xO (xO xH)))) (@eq Z a (Zpos (xO (xO (xO xH))))))), Z.gt (alignof_blockcopy env ty) Z0 *)
  intros; simpl. rewrite H0.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  erewrite co_consistent_rank by eauto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exploit (rank_type_members ce); eauto.
(* Goal: forall _ : le (rank_type ce t1) (rank_members ce (co_members co)), lt (rank_type ce t1) (S (rank_members ce (co_members co))) *)
  omega.
Qed.

Lemma rank_union_member:
  forall ce id a co id1 t1,
  composite_env_consistent ce ->
  ce!id = Some co ->
  In (id1, t1) (co_members co) ->
  (rank_type ce t1 < rank_type ce (Tunion id a))%nat.
Proof.
(* Goal: forall _ : let a := alignof_blockcopy env ty in or (@eq Z a (Zpos xH)) (or (@eq Z a (Zpos (xO xH))) (or (@eq Z a (Zpos (xO (xO xH)))) (@eq Z a (Zpos (xO (xO (xO xH))))))), Z.gt (alignof_blockcopy env ty) Z0 *)
  intros; simpl. rewrite H0.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  erewrite co_consistent_rank by eauto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exploit (rank_type_members ce); eauto.
(* Goal: forall _ : le (rank_type ce t1) (rank_members ce (co_members co)), lt (rank_type ce t1) (S (rank_members ce (co_members co))) *)
  omega.
Qed.

(** * Programs and compilation units *)

(** The definitions in this section are parameterized over a type [F] of 
  internal function definitions, so that they apply both to CompCert C and to Clight. *)

Set Implicit Arguments.

Section PROGRAMS.

Variable F: Type.

(** Functions can either be defined ([Internal]) or declared as
  external functions ([External]). *)

Inductive fundef : Type :=
  | Internal: F -> fundef
  | External: external_function -> typelist -> type -> calling_convention -> fundef.

(** A program, or compilation unit, is composed of:
- a list of definitions of functions and global variables;
- the names of functions and global variables that are public (not static);
- the name of the function that acts as entry point ("main" function).
- a list of definitions for structure and union names
- the corresponding composite environment
- a proof that this environment is consistent with the definitions. *)

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Record program : Type := {
  prog_defs: list (ident * globdef fundef type);
  prog_public: list ident;
  prog_main: ident;
  prog_types: list composite_definition;
  prog_comp_env: composite_env;
  prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env
}.

Definition program_of_program (p: program) : AST.program fundef type :=
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  {| AST.prog_defs := p.(prog_defs);
     AST.prog_public := p.(prog_public);
     AST.prog_main := p.(prog_main) |}.

Coercion program_of_program: program >-> AST.program.

Program Definition make_program (types: list composite_definition)
                                (defs: list (ident * globdef fundef type))
                                (public: list ident)
                                (main: ident) : res program :=
  match build_composite_env types with
  | Error e => Error e
  | OK ce =>
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
      OK {| prog_defs := defs;
            prog_public := public;
            prog_main := main;
            prog_types := types;
            prog_comp_env := ce;
            prog_comp_env_eq := _ |}
  end.

End PROGRAMS.

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Arguments External {F} _ _ _ _.

Unset Implicit Arguments.

(** * Separate compilation and linking *)

(** ** Linking types *)

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Program Instance Linker_types : Linker type := {
  link := fun t1 t2 => if type_eq t1 t2 then Some t1 else None;
  linkorder := fun t1 t2 => t1 = t2
}.
Next Obligation.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct (type_eq x y); inv H. auto.
Defined.

Global Opaque Linker_types.

(** ** Linking composite definitions *)

Definition check_compat_composite (l: list composite_definition) (cd: composite_definition) : bool :=
  List.forallb
    (fun cd' =>
      if ident_eq (name_composite_def cd') (name_composite_def cd) then composite_def_eq cd cd' else true)
    l.

Definition filter_redefs (l1 l2: list composite_definition) :=
  let names1 := map name_composite_def l1 in
  List.filter (fun cd => negb (In_dec ident_eq (name_composite_def cd) names1)) l2.

Definition link_composite_defs (l1 l2: list composite_definition): option (list composite_definition) :=
  if List.forallb (check_compat_composite l2) l1
  then Some (l1 ++ filter_redefs l1 l2)
  else None.

Lemma link_composite_def_inv:
  forall l1 l2 l,
  link_composite_defs l1 l2 = Some l ->
     (forall cd1 cd2, In cd1 l1 -> In cd2 l2 -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1)
  /\ l = l1 ++ filter_redefs l1 l2
  /\ (forall x, In x l <-> In x l1 \/ In x l2).
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  unfold link_composite_defs; intros.
(* Goal: @ex composite (fun co : composite => and (@eq (option composite) (@PTree.get composite id env) (@Some composite co)) (and (@eq members (co_members co) m) (and (@eq attr (co_attr co) a) (@eq struct_or_union (co_su co) su)))) *)
  destruct (forallb (check_compat_composite l2) l1) eqn:C; inv H.
  assert (A: 
    forall cd1 cd2, In cd1 l1 -> In cd2 l2 -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1).
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  { rewrite forallb_forall in C. intros.
(* Goal: @eq composite_definition cd2 cd1 *)
    apply C in H. unfold check_compat_composite in H. rewrite forallb_forall in H. 
    apply H in H0. rewrite H1, dec_eq_true in H0. symmetry; eapply proj_sumbool_true; eauto. }
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  split. auto. split. auto. 
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  unfold filter_redefs; intros. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  rewrite in_app_iff. rewrite filter_In. intuition auto. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct (in_dec ident_eq (name_composite_def x) (map name_composite_def l1)); simpl; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exploit list_in_map_inv; eauto. intros (y & P & Q).
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  assert (x = y) by eauto. subst y. auto.
Qed.

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Program Instance Linker_composite_defs : Linker (list composite_definition) := {
  link := link_composite_defs;
  linkorder := @List.incl composite_definition
}.
Next Obligation.
(* Goal: @incl composite_definition x x *)
  apply incl_refl.
Defined.
Next Obligation.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  red; intros; eauto.
Defined.
Next Obligation.
(* Goal: and (@incl composite_definition x z) (@incl composite_definition y z) *)
  apply link_composite_def_inv in H; destruct H as (A & B & C).
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  split; red; intros; apply C; auto.
Defined.

(** Connections with [build_composite_env]. *)

Lemma add_composite_definitions_append:
  forall l1 l2 env env'',
  add_composite_definitions env (l1 ++ l2) = OK env'' <->
  exists env', add_composite_definitions env l1 = OK env' /\ add_composite_definitions env' l2 = OK env''.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  induction l1; simpl; intros.
- split; intros. exists env; auto. destruct H as (env' & A & B). congruence.
- destruct a; simpl. destruct (composite_of_def env id su m a); simpl.
(* Goal: iff (@eq (res composite_env) (add_composite_definitions (@PTree.set composite id c env) (@app composite_definition l1 l2)) (@OK composite_env env'')) (@ex composite_env (fun env' : composite_env => and (@eq (res composite_env) (add_composite_definitions (@PTree.set composite id c env) l1) (@OK composite_env env')) (@eq (res composite_env) (add_composite_definitions env' l2) (@OK composite_env env'')))) *)
(* Goal: iff (@eq (res composite_env) (@Error composite_env e) (@OK composite_env env'')) (@ex composite_env (fun env' : composite_env => and (@eq (res composite_env) (@Error composite_env e) (@OK composite_env env')) (@eq (res composite_env) (add_composite_definitions env' l2) (@OK composite_env env'')))) *)
  apply IHl1. 
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  split; intros. discriminate. destruct H as (env' & A & B); discriminate.
Qed.

Lemma composite_eq:
  forall su1 m1 a1 sz1 al1 r1 pos1 al2p1 szal1
         su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2,
  su1 = su2 -> m1 = m2 -> a1 = a2 -> sz1 = sz2 -> al1 = al2 -> r1 = r2 ->
  Build_composite su1 m1 a1 sz1 al1 r1 pos1 al2p1 szal1 = Build_composite su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. subst.
(* Goal: @eq composite (Build_composite su2 m2 a2 sz2 al2 r2 pos1 al2p1 szal1) (Build_composite su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2) *)
  assert (pos1 = pos2) by apply proof_irr. 
(* Goal: @eq composite (Build_composite su2 m2 a2 sz2 al2 r2 pos1 al2p1 szal1) (Build_composite su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2) *)
  assert (al2p1 = al2p2) by apply proof_irr.
(* Goal: @eq composite (Build_composite su2 m2 a2 sz2 al2 r2 pos1 al2p1 szal1) (Build_composite su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2) *)
  assert (szal1 = szal2) by apply proof_irr.
(* Goal: and (@linkorder_fundef F (@External F e t t0 c) (@External F e t t0 c)) (@linkorder_fundef F (@External F e0 t1 t2 c0) (@External F e t t0 c)) *)
  subst. reflexivity.
Qed.

Lemma composite_of_def_eq:
  forall env id co,
  composite_consistent env co ->
  env!id = None ->
  composite_of_def env id (co_su co) (co_members co) (co_attr co) = OK co.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. destruct H as [A B C D]. unfold composite_of_def. rewrite H0, A.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct co; simpl in *. f_equal. apply composite_eq; auto. rewrite C, B; auto. 
Qed.

Lemma composite_consistent_unique:
  forall env co1 co2,
  composite_consistent env co1 ->
  composite_consistent env co2 ->
  co_su co1 = co_su co2 ->
  co_members co1 = co_members co2 ->
  co_attr co1 = co_attr co2 ->
  co1 = co2.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. destruct H, H0. destruct co1, co2; simpl in *. apply composite_eq; congruence.
Qed.

Lemma composite_of_def_stable:
  forall (env env': composite_env)
         (EXTENDS: forall id co, env!id = Some co -> env'!id = Some co)
         id su m a co,
  env'!id = None ->
  composite_of_def env id su m a = OK co ->
  composite_of_def env' id su m a = OK co.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. 
(* Goal: @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  unfold composite_of_def in H0. 
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (env!id) eqn:E; try discriminate.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (complete_members env m) eqn:CM; try discriminate.
(* Goal: @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  transitivity (composite_of_def env' id (co_su co) (co_members co) (co_attr co)).
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  inv H0; auto. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  apply composite_of_def_eq; auto. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  apply composite_consistent_stable with env; auto. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  inv H0; constructor; auto.
Qed.

Lemma link_add_composite_definitions:
  forall l0 env0,
  build_composite_env l0 = OK env0 ->
  forall l env1 env1' env2,
  add_composite_definitions env1 l = OK env1' ->
  (forall id co, env1!id = Some co -> env2!id = Some co) ->
  (forall id co, env0!id = Some co -> env2!id = Some co) ->
  (forall id, env2!id = if In_dec ident_eq id (map name_composite_def l0) then env0!id else env1!id) ->
  ((forall cd1 cd2, In cd1 l0 -> In cd2 l -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1)) ->
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  { env2' |
      add_composite_definitions env2 (filter_redefs l0 l) = OK env2'
  /\ (forall id co, env1'!id = Some co -> env2'!id = Some co)
  /\ (forall id co, env0!id = Some co -> env2'!id = Some co) }.
Proof.
  induction l; simpl; intros until env2; intros ACD AGREE1 AGREE0 AGREE2 UNIQUE.
- inv ACD. exists env2; auto.
- destruct a. destruct (composite_of_def env1 id su m a) as [x|e] eqn:EQ; try discriminate.
  simpl in ACD.
  generalize EQ. unfold composite_of_def at 1. 
(* Goal: @eq (res composite_env) (add_composite_definitions env l2) (@OK composite_env env'') *)
  destruct (env1!id) eqn:E1; try congruence.
(* Goal: @eq (res composite_env) (add_composite_definitions env l2) (@OK composite_env env'') *)
  destruct (complete_members env1 m) eqn:CM1; try congruence. 
  intros EQ1.
(* Goal: forall _ : let a := alignof_blockcopy env ty in or (@eq Z a (Zpos xH)) (or (@eq Z a (Zpos (xO xH))) (or (@eq Z a (Zpos (xO (xO xH)))) (@eq Z a (Zpos (xO (xO (xO xH))))))), Z.gt (alignof_blockcopy env ty) Z0 *)
  simpl. destruct (in_dec ident_eq id (map name_composite_def l0)); simpl.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
+ eapply IHl; eauto.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
* intros. rewrite PTree.gsspec in H0. destruct (peq id0 id); auto.
(* Goal: and (Z.le pos (align pos (alignof env t))) (Z.le (Z.add (align pos (alignof env t)) (sizeof env ty)) (sizeof_struct env (Z.add (align pos (alignof env t)) (sizeof env t)) fld)) *)
(* Goal: and (Z.le pos ofs) (Z.le (Z.add ofs (sizeof env ty)) (sizeof_struct env (Z.add (align pos (alignof env t)) (sizeof env t)) fld)) *)
  inv H0.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exploit list_in_map_inv; eauto. intros ([id' su' m' a'] & P & Q).
  assert (X: Composite id su m a = Composite id' su' m' a').
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  { eapply UNIQUE. auto. auto. rewrite <- P; auto. }
  inv X.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exploit build_composite_env_charact; eauto. intros (co' & U & V & W & X). 
  assert (co' = co).
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  { apply composite_consistent_unique with env2.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    apply composite_consistent_stable with env0; auto. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    eapply build_composite_env_consistent; eauto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    apply composite_consistent_stable with env1; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    inversion EQ1; constructor; auto. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    inversion EQ1; auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    inversion EQ1; auto.
    inversion EQ1; auto. }
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  subst co'. apply AGREE0; auto. 
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
* intros. rewrite AGREE2. destruct (in_dec ident_eq id0 (map name_composite_def l0)); auto. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  rewrite PTree.gsspec. destruct (peq id0 id); auto. subst id0. contradiction.
+ assert (E2: env2!id = None).
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  { rewrite AGREE2. rewrite pred_dec_false by auto. auto. }
  assert (E3: composite_of_def env2 id su m a = OK x).
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  { eapply composite_of_def_stable. eexact AGREE1. eauto. eauto. }
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  rewrite E3. simpl. eapply IHl; eauto. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
* intros until co; rewrite ! PTree.gsspec. destruct (peq id0 id); auto.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
* intros until co; rewrite ! PTree.gsspec. intros. destruct (peq id0 id); auto.
(* Goal: @eq (res composite_env) (add_composite_definitions env l2) (@OK composite_env env'') *)
  subst id0. apply AGREE0 in H0. congruence.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
* intros. rewrite ! PTree.gsspec. destruct (peq id0 id); auto. subst id0. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  rewrite pred_dec_false by auto. auto.
Qed.

Theorem link_build_composite_env:
  forall l1 l2 l env1 env2,
  build_composite_env l1 = OK env1 ->
  build_composite_env l2 = OK env2 ->
  link l1 l2 = Some l ->
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  { env |
     build_composite_env l = OK env
  /\ (forall id co, env1!id = Some co -> env!id = Some co)
  /\ (forall id co, env2!id = Some co -> env!id = Some co) }.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. edestruct link_composite_def_inv as (A & B & C); eauto.
  edestruct link_add_composite_definitions as (env & P & Q & R).
  eexact H.
  eexact H0.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  instantiate (1 := env1). intros. rewrite PTree.gempty in H2; discriminate.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  auto.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. destruct (in_dec ident_eq id (map name_composite_def l1)); auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  rewrite PTree.gempty. destruct (env1!id) eqn:E1; auto. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exploit build_composite_env_domain. eexact H. eauto.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. apply (in_map name_composite_def) in H2. elim n; auto. 
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  auto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  exists env; split; auto. subst l. apply add_composite_definitions_append. exists env1; auto. 
Qed.

(** ** Linking function definitions *)

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Definition link_fundef {F: Type} (fd1 fd2: fundef F) :=
  match fd1, fd2 with
  | Internal _, Internal _ => None
  | External ef1 targs1 tres1 cc1, External ef2 targs2 tres2 cc2 =>
      if external_function_eq ef1 ef2
      && typelist_eq targs1 targs2
      && type_eq tres1 tres2
      && calling_convention_eq cc1 cc2
      then Some (External ef1 targs1 tres1 cc1)
      else None
  | Internal f, External ef targs tres cc =>
      match ef with EF_external id sg => Some (Internal f) | _ => None end
  | External ef targs tres cc, Internal f =>
      match ef with EF_external id sg => Some (Internal f) | _ => None end
  end.

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
  | linkorder_fundef_refl: forall fd,
      linkorder_fundef fd fd
  | linkorder_fundef_ext_int: forall f id sg targs tres cc,
      linkorder_fundef (External (EF_external id sg) targs tres cc) (Internal f).

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Program Instance Linker_fundef (F: Type): Linker (fundef F) := {
  link := link_fundef;
  linkorder := linkorder_fundef
}.
Next Obligation.
(* Goal: @linkorder_fundef F x x *)
  constructor.
Defined.
Next Obligation.
(* Goal: @linkorder_fundef F x x *)
  inv H; inv H0; constructor.
Defined.
Next Obligation.
(* Goal: and (@linkorder_fundef F x z) (@linkorder_fundef F y z) *)
  destruct x, y; simpl in H.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
+ discriminate.
(* Goal: @ex composite (fun co : composite => and (@eq (option composite) (@PTree.get composite id env) (@Some composite co)) (and (@eq members (co_members co) m) (and (@eq attr (co_attr co) a) (@eq struct_or_union (co_su co) su)))) *)
+ destruct e; inv H. split; constructor.
(* Goal: @ex composite (fun co : composite => and (@eq (option composite) (@PTree.get composite id env) (@Some composite co)) (and (@eq members (co_members co) m) (and (@eq attr (co_attr co) a) (@eq struct_or_union (co_su co) su)))) *)
+ destruct e; inv H. split; constructor.
(* Goal: @ex composite (fun co : composite => and (@eq (option composite) (@PTree.get composite id env) (@Some composite co)) (and (@eq members (co_members co) m) (and (@eq attr (co_attr co) a) (@eq struct_or_union (co_su co) su)))) *)
+ destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0) eqn:A; inv H.
(* Goal: and (@linkorder_fundef F (@External F e t t0 c) (@External F e t t0 c)) (@linkorder_fundef F (@External F e0 t1 t2 c0) (@External F e t t0 c)) *)
  InvBooleans. subst. split; constructor.
Defined.

Remark link_fundef_either:
  forall (F: Type) (f1 f2 f: fundef F), link f1 f2 = Some f -> f = f1 \/ f = f2.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  simpl; intros. unfold link_fundef in H. destruct f1, f2; try discriminate.
- destruct e; inv H. auto.
- destruct e; inv H. auto.
- destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0); inv H; auto.
Qed.

Global Opaque Linker_fundef.

(** ** Linking programs *)

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Definition lift_option {A: Type} (opt: option A) : { x | opt = Some x } + { opt = None }.
Proof.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct opt. left; exists a; auto. right; auto. 
Defined.

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Definition link_program {F:Type} (p1 p2: program F): option (program F) :=
  match link (program_of_program p1) (program_of_program p2) with
  | None => None
  | Some p =>
      match lift_option (link p1.(prog_types) p2.(prog_types)) with
      | inright _ => None
      | inleft (exist typs EQ) =>
          match link_build_composite_env
                   p1.(prog_types) p2.(prog_types) typs
                   p1.(prog_comp_env) p2.(prog_comp_env)
                   p1.(prog_comp_env_eq) p2.(prog_comp_env_eq) EQ with
          | exist env (conj P Q) =>
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
              Some {| prog_defs := p.(AST.prog_defs);
                      prog_public := p.(AST.prog_public);
                      prog_main := p.(AST.prog_main);
                      prog_types := typs;
                      prog_comp_env := env;
                      prog_comp_env_eq := P |}
          end
      end
  end.

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Definition linkorder_program {F: Type} (p1 p2: program F) : Prop :=
     linkorder (program_of_program p1) (program_of_program p2)
  /\ (forall id co, p1.(prog_comp_env)!id = Some co -> p2.(prog_comp_env)!id = Some co).

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Program Instance Linker_program (F: Type): Linker (program F) := {
  link := link_program;
  linkorder := linkorder_program
}.
Next Obligation.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  split. apply linkorder_refl. auto.
Defined.
Next Obligation.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  destruct H, H0. split. eapply linkorder_trans; eauto.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  intros; auto.
Defined.
Next Obligation.
(* Goal: and (@linkorder_program F x z) (@linkorder_program F y z) *)
  revert H. unfold link_program.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (link (program_of_program x) (program_of_program y)) as [p|] eqn:LP; try discriminate.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (lift_option (link (prog_types x) (prog_types y))) as [[typs EQ]|EQ]; try discriminate.
  destruct (link_build_composite_env (prog_types x) (prog_types y) typs
       (prog_comp_env x) (prog_comp_env y) (prog_comp_env_eq x)
       (prog_comp_env_eq y) EQ) as (env & P & Q & R).
(* Goal: forall _ : @eq (option (program F)) (@Some (program F) (@Build_program F (@AST.prog_defs (fundef F) type p) (@AST.prog_public (fundef F) type p) (@AST.prog_main (fundef F) type p) typs env P)) (@Some (program F) z), and (@linkorder_program F x z) (@linkorder_program F y z) *)
  destruct (link_linkorder _ _ _ LP). 
  intros X; inv X.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  split; split; auto.
Defined.

Global Opaque Linker_program.

(** ** Commutation between linking and program transformations *)

Section LINK_MATCH_PROGRAM.

(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
Context {F G: Type}.
Variable match_fundef: fundef F -> fundef G -> Prop.

Hypothesis link_match_fundef:
  forall f1 tf1 f2 tf2 f,
  link f1 f2 = Some f ->
  match_fundef f1 tf1 -> match_fundef f2 tf2 ->
  exists tf, link tf1 tf2 = Some tf /\ match_fundef f tf.

Let match_program (p: program F) (tp: program G) : Prop :=
    Linking.match_program (fun ctx f tf => match_fundef f tf) eq p tp
 /\ prog_types tp = prog_types p.

Theorem link_match_program:
  forall p1 p2 tp1 tp2 p,
  link p1 p2 = Some p -> match_program p1 tp1 -> match_program p2 tp2 ->
  exists tp, link tp1 tp2 = Some tp /\ match_program p tp.
Proof.
(* Goal: forall (env env' : composite_env) (_ : forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env) (@Some composite co)), @eq (option composite) (@PTree.get composite id env') (@Some composite co)) (id : positive) (su : struct_or_union) (m : members) (a : attr) (co : composite) (_ : @eq (option composite) (@PTree.get composite id env') (@None composite)) (_ : @eq (res composite) (composite_of_def env id su m a) (@OK composite co)), @eq (res composite) (composite_of_def env' id su m a) (@OK composite co) *)
  intros. destruct H0, H1. 
Local Transparent Linker_program.
  simpl in H; unfold link_program in H.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate.
  assert (A: exists tpp,
               link (program_of_program tp1) (program_of_program tp2) = Some tpp
             /\ Linking.match_program (fun ctx f tf => match_fundef f tf) eq pp tpp).
(* Goal: forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1 *)
(* Goal: and (forall (cd1 cd2 : composite_definition) (_ : @In composite_definition cd1 l1) (_ : @In composite_definition cd2 l2) (_ : @eq ident (name_composite_def cd2) (name_composite_def cd1)), @eq composite_definition cd2 cd1) (and (@eq (list composite_definition) (@app composite_definition l1 (filter_redefs l1 l2)) (@app composite_definition l1 (filter_redefs l1 l2))) (forall x : composite_definition, iff (@In composite_definition x (@app composite_definition l1 (filter_redefs l1 l2))) (or (@In composite_definition x l1) (@In composite_definition x l2)))) *)
  { eapply Linking.link_match_program. 
  - intros. exploit link_match_fundef; eauto. intros (tf & A & B). exists tf; auto.
  - intros.
    Local Transparent Linker_types.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
    simpl in *. destruct (type_eq v1 v2); inv H4. exists v; rewrite dec_eq_true; auto.
  - eauto.
  - eauto.
  - eauto.
  - apply (link_linkorder _ _ _ LP).
  - apply (link_linkorder _ _ _ LP). }
  destruct A as (tpp & TLP & MP).
(* Goal: forall _ : @eq (option (program F)) (@link_program F x y) (@Some (program F) z), and (@linkorder_program F x z) (@linkorder_program F y z) *)
  simpl; unfold link_program. rewrite TLP.
(* Goal: and (@linkorder_fundef F (@Internal F f) z) (@linkorder_fundef F (@Internal F f0) z) *)
  destruct (lift_option (link (prog_types p1) (prog_types p2))) as [[typs EQ]|EQ]; try discriminate.
  destruct (link_build_composite_env (prog_types p1) (prog_types p2) typs
           (prog_comp_env p1) (prog_comp_env p2) (prog_comp_env_eq p1)
           (prog_comp_env_eq p2) EQ) as (env & P & Q). 
  rewrite <- H2, <- H3 in EQ.
(* Goal: @eq (res composite_env) (add_composite_definitions env l2) (@OK composite_env env'') *)
  destruct (lift_option (link (prog_types tp1) (prog_types tp2))) as [[ttyps EQ']|EQ']; try congruence.
(* Goal: @eq (res composite_env) (add_composite_definitions env l2) (@OK composite_env env'') *)
  assert (ttyps = typs) by congruence. subst ttyps. 
  destruct (link_build_composite_env (prog_types tp1) (prog_types tp2) typs
         (prog_comp_env tp1) (prog_comp_env tp2) (prog_comp_env_eq tp1)
         (prog_comp_env_eq tp2) EQ') as (tenv & R & S).
(* Goal: @eq (res composite_env) (add_composite_definitions env l2) (@OK composite_env env'') *)
  assert (tenv = env) by congruence. subst tenv.
(* Goal: forall (id : positive) (co : composite) (_ : @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co)), @eq (option composite) (@PTree.get composite id (@prog_comp_env F x)) (@Some composite co) *)
  econstructor; split; eauto. inv H. split; auto.
(* Goal: forall _ : let a := alignof_blockcopy env ty in or (@eq Z a (Zpos xH)) (or (@eq Z a (Zpos (xO xH))) (or (@eq Z a (Zpos (xO (xO xH)))) (@eq Z a (Zpos (xO (xO (xO xH))))))), Z.gt (alignof_blockcopy env ty) Z0 *)
  unfold program_of_program; simpl. destruct pp, tpp; exact MP.
Qed.

End LINK_MATCH_PROGRAM.
