(* *********************************************************************)
(*                                                                     *)
(*              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 INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** * Correctness of the translation from Clight to C#minor. *)

Require Import Coqlib Errors Maps Integers Floats.
Require Import AST Linking.
Require Import Values Events Memory Globalenvs Smallstep.
Require Import Ctypes Cop Clight Cminor Csharpminor.
Require Import Cshmgen.

(** * Relational specification of the transformation *)

Inductive match_fundef (p: Clight.program) : Clight.fundef -> Csharpminor.fundef -> Prop :=
  | match_fundef_internal: forall f tf,
      transl_function p.(prog_comp_env) f = OK tf ->
      match_fundef p (Ctypes.Internal f) (AST.Internal tf)
  | match_fundef_external: forall ef args res cc,
      ef_sig ef = signature_of_type args res cc ->
      match_fundef p (Ctypes.External ef args res cc) (AST.External ef).

Definition match_varinfo (v: type) (tv: unit) := True.

Definition match_prog (p: Clight.program) (tp: Csharpminor.program) : Prop :=
  match_program_gen match_fundef match_varinfo p p tp.

Lemma transf_program_match:
  forall p tp, transl_program p = OK tp -> match_prog p tp.
Proof.
  unfold transl_program; intros.
  eapply match_transform_partial_program2.
  eexact H.
- intros. destruct f; simpl in H0.
+ monadInv H0. constructor; auto.
+ destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H0.
  constructor; auto.
- intros; red; auto.
Qed.

(** * Properties of operations over types *)

Remark transl_params_types:
  forall params,
  map typ_of_type (map snd params) = typlist_of_typelist (type_of_params params).
Proof.
(* Goal: forall params : list (prod ident type), @eq (list typ) (@map type typ typ_of_type (@map (prod ident type) type (@snd ident type) params)) (typlist_of_typelist (type_of_params params)) *)
  induction params; simpl. auto. destruct a as [id ty]; simpl. f_equal; auto.
Qed.

Lemma transl_fundef_sig1:
  forall ce f tf args res cc,
  match_fundef ce f tf ->
  classify_fun (type_of_fundef f) = fun_case_f args res cc ->
  funsig tf = signature_of_type args res cc.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. inv H.
- monadInv H1. simpl. inversion H0.
(* Goal: @eq signature (signature_of_function f0) (signature_of_type (type_of_params (Clight.fn_params f0)) (fn_return f0) (fn_callconv f0)) *)
  unfold signature_of_function, signature_of_type.
(* Goal: @eq Ptrofs.int (Ptrofs.add i (Ptrofs.of_int (Int.mul (Int.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (Int64.loword i0)))) (Ptrofs.add i (Ptrofs.mul (Ptrofs.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (Ptrofs.of_int64 i0))) *)
  f_equal. apply transl_params_types.
- simpl in H0. unfold funsig. congruence.
Qed.

Lemma transl_fundef_sig2:
  forall ce f tf args res cc,
  match_fundef ce f tf ->
  type_of_fundef f = Tfunction args res cc ->
  funsig tf = signature_of_type args res cc.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. eapply transl_fundef_sig1; eauto.
(* Goal: @eq classify_fun_cases (classify_fun (type_of_fundef f)) (fun_case_f args res cc) *)
  rewrite H0; reflexivity.
Qed.

Lemma transl_sizeof:
  forall (cunit prog: Clight.program) t sz,
  linkorder cunit prog ->
  sizeof cunit.(prog_comp_env) t = OK sz ->
  sz = Ctypes.sizeof prog.(prog_comp_env) t.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. destruct H.
(* Goal: and (@eq Z sz (Ctypes.sizeof (@prog_comp_env Clight.function prog) t)) (@eq Z (alignof_blockcopy (@prog_comp_env Clight.function cunit) t) (alignof_blockcopy (@prog_comp_env Clight.function prog) t)) *)
  unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  symmetry. apply Ctypes.sizeof_stable; auto.
Qed.

Lemma transl_alignof:
  forall (cunit prog: Clight.program) t al,
  linkorder cunit prog ->
  alignof cunit.(prog_comp_env) t = OK al ->
  al = Ctypes.alignof prog.(prog_comp_env) t.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. destruct H.
(* Goal: and (@eq Z sz (Ctypes.sizeof (@prog_comp_env Clight.function prog) t)) (@eq Z (alignof_blockcopy (@prog_comp_env Clight.function cunit) t) (alignof_blockcopy (@prog_comp_env Clight.function prog) t)) *)
  unfold alignof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  symmetry. apply Ctypes.alignof_stable; auto.
Qed.

Lemma transl_alignof_blockcopy:
  forall (cunit prog: Clight.program) t sz,
  linkorder cunit prog ->
  sizeof cunit.(prog_comp_env) t = OK sz ->
  sz = Ctypes.sizeof prog.(prog_comp_env) t /\
  alignof_blockcopy cunit.(prog_comp_env) t = alignof_blockcopy prog.(prog_comp_env) t.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. destruct H.
(* Goal: and (@eq Z sz (Ctypes.sizeof (@prog_comp_env Clight.function prog) t)) (@eq Z (alignof_blockcopy (@prog_comp_env Clight.function cunit) t) (alignof_blockcopy (@prog_comp_env Clight.function prog) t)) *)
  unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  split.
- symmetry. apply Ctypes.sizeof_stable; auto.
- revert C. induction t; simpl; auto;
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (prog_comp_env cunit)!i as [co|] eqn:X; try discriminate; erewrite H1 by eauto; auto.
Qed.

Lemma field_offset_stable:
  forall (cunit prog: Clight.program) id co f,
  linkorder cunit prog ->
  cunit.(prog_comp_env)!id = Some co ->
  prog.(prog_comp_env)!id = Some co /\
  field_offset prog.(prog_comp_env) f (co_members co) = field_offset cunit.(prog_comp_env) f (co_members co).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  assert (C: composite_consistent cunit.(prog_comp_env) co).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  { apply build_composite_env_consistent with cunit.(prog_types) id; auto.
(* Goal: @eq (res composite_env) (build_composite_env (@prog_types Clight.function cunit)) (@OK composite_env (@prog_comp_env Clight.function cunit)) *)
    apply prog_comp_env_eq. }
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  destruct H as [_ A].
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  split. auto. generalize (co_consistent_complete _ _ C).
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  unfold field_offset. generalize 0. induction (co_members co) as [ | [f1 t1] m]; simpl; intros.
- auto.
- InvBooleans.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite ! (alignof_stable _ _ A) by auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite ! (sizeof_stable _ _ A) by auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (ident_eq f f1); eauto.
Qed.

(** * Properties of the translation functions *)

(** Transformation of expressions and statements. *)

Lemma transl_expr_lvalue:
  forall ge e le m a loc ofs ce ta,
  Clight.eval_lvalue ge e le m a loc ofs ->
  transl_expr ce a = OK ta ->
  (exists tb, transl_lvalue ce a = OK tb /\ make_load tb (typeof a) = OK ta).
Proof.
(* Goal: forall (ge : Clight.genv) (e : Clight.env) (le : Clight.temp_env) (m : Mem.mem) (a : Clight.expr) (loc : block) (ofs : Ptrofs.int) (ce : composite_env) (ta : expr) (_ : eval_lvalue ge e le m a loc ofs) (_ : @eq (res expr) (transl_expr ce a) (@OK expr ta)), @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce a) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof a)) (@OK expr ta))) *)
  intros until ta; intros EVAL TR. inv EVAL; simpl in TR.
  (* var local *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exists (Eaddrof id); auto.
  (* var global *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exists (Eaddrof id); auto.
  (* deref *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  monadInv TR. exists x; auto.
  (* field struct *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  monadInv TR. exists x0; split; auto. simpl; rewrite EQ; auto.
  (* field union *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  monadInv TR. exists x0; split; auto. simpl; rewrite EQ; auto.
Qed.

(** Properties of labeled statements *)

Lemma transl_lbl_stmt_1:
  forall ce tyret nbrk ncnt n sl tsl,
  transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl ->
  transl_lbl_stmt ce tyret nbrk ncnt (Clight.select_switch n sl) = OK (select_switch n tsl).
Proof.
(* Goal: forall (ce : composite_env) (tyret : type) (nbrk ncnt : nat) (n : Z) (sl : labeled_statements) (tsl : lbl_stmt) (_ : @eq (res lbl_stmt) (transl_lbl_stmt ce tyret nbrk ncnt sl) (@OK lbl_stmt tsl)), @eq (res lbl_stmt) (transl_lbl_stmt ce tyret nbrk ncnt (Clight.select_switch n sl)) (@OK lbl_stmt (select_switch n tsl)) *)
  intros until n.
  assert (DFL: forall sl tsl,
    transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl ->
    transl_lbl_stmt ce tyret nbrk ncnt (Clight.select_switch_default sl) = OK (select_switch_default tsl)).
(* Goal: @eq Z (Int64.unsigned i) (Int.unsigned (Int64.loword i)) *)
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  {
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
    induction sl; simpl; intros.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    inv H; auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    monadInv H. simpl. destruct o; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto.
  }
  assert (CASE: forall sl tsl,
    transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl ->
    match Clight.select_switch_case n sl with
    | None =>
        select_switch_case n tsl = None
    | Some sl' =>
        exists tsl',
           select_switch_case n tsl = Some tsl'
        /\ transl_lbl_stmt ce tyret nbrk ncnt sl' = OK tsl'
    end).
(* Goal: @eq Z (Int64.unsigned i) (Int.unsigned (Int64.loword i)) *)
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  {
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
    induction sl; simpl; intros.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    inv H; auto.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
    monadInv H; simpl. destruct o. destruct (zeq z n).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    econstructor; split; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    apply IHsl; auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    apply IHsl; auto.
  }
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. specialize (CASE _ _ H). unfold Clight.select_switch, select_switch.
(* Goal: @eq (res lbl_stmt) (transl_lbl_stmt ce tyret nbrk ncnt match Clight.select_switch_case n sl with | Some sl' => sl' | None => Clight.select_switch_default sl end) (@OK lbl_stmt match select_switch_case n tsl with | Some sl' => sl' | None => select_switch_default tsl end) *)
  destruct (Clight.select_switch_case n sl) as [sl'|].
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct CASE as [tsl' [P Q]]. rewrite P, Q. auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite CASE. auto.
Qed.

Lemma transl_lbl_stmt_2:
  forall ce tyret nbrk ncnt sl tsl,
  transl_lbl_stmt ce tyret nbrk ncnt sl = OK tsl ->
  transl_statement ce tyret nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  induction sl; intros.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  monadInv H. auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  monadInv H. simpl. rewrite EQ; simpl. rewrite (IHsl _ EQ1). simpl. auto.
Qed.

(** * Correctness of Csharpminor construction functions *)

Section CONSTRUCTORS.

Variables cunit prog: Clight.program.
Hypothesis LINK: linkorder cunit prog.
Variable ge: genv.

Lemma make_intconst_correct:
  forall n e le m,
  eval_expr ge e le m (make_intconst n) (Vint n).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold make_intconst. econstructor. reflexivity.
Qed.

Lemma make_floatconst_correct:
  forall n e le m,
  eval_expr ge e le m (make_floatconst n) (Vfloat n).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold make_floatconst. econstructor. reflexivity.
Qed.

Lemma make_singleconst_correct:
  forall n e le m,
  eval_expr ge e le m (make_singleconst n) (Vsingle n).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold make_singleconst. econstructor. reflexivity.
Qed.

Lemma make_longconst_correct:
  forall n e le m,
  eval_expr ge e le m (make_longconst n) (Vlong n).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold make_floatconst. econstructor. reflexivity.
Qed.

Lemma make_ptrofsconst_correct:
  forall n e le m,
  eval_expr ge e le m (make_ptrofsconst n) (Vptrofs (Ptrofs.repr n)).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold Vptrofs, make_ptrofsconst. destruct Archi.ptr64 eqn:SF.
- replace (Ptrofs.to_int64 (Ptrofs.repr n)) with (Int64.repr n).
(* Goal: eval_expr ge e le m (make_longconst (Int64.repr n)) (Vlong (Int64.repr n)) *)
(* Goal: @eq Int64.int (Int64.repr n) (Ptrofs.to_int64 (Ptrofs.repr n)) *)
  apply make_longconst_correct.
(* Goal: @eq Int.int (Int.repr n) (Ptrofs.to_int (Ptrofs.repr n)) *)
  symmetry; auto with ptrofs.
- replace (Ptrofs.to_int (Ptrofs.repr n)) with (Int.repr n).
(* Goal: eval_expr ge e le m (make_intconst (Int.repr n)) (Vint (Int.repr n)) *)
(* Goal: @eq Int.int (Int.repr n) (Ptrofs.to_int (Ptrofs.repr n)) *)
  apply make_intconst_correct.
(* Goal: @eq Int.int (Int.repr n) (Ptrofs.to_int (Ptrofs.repr n)) *)
  symmetry; auto with ptrofs.
Qed.

Lemma make_singleoffloat_correct:
  forall a n e le m,
  eval_expr ge e le m a (Vfloat n) ->
  eval_expr ge e le m (make_singleoffloat a) (Vsingle (Float.to_single n)).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. econstructor. eauto. auto.
Qed.

Lemma make_floatofsingle_correct:
  forall a n e le m,
  eval_expr ge e le m a (Vsingle n) ->
  eval_expr ge e le m (make_floatofsingle a) (Vfloat (Float.of_single n)).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. econstructor. eauto. auto.
Qed.

Lemma make_floatofint_correct:
  forall a n sg e le m,
  eval_expr ge e le m a (Vint n) ->
  eval_expr ge e le m (make_floatofint a sg) (Vfloat(cast_int_float sg n)).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold make_floatofint, cast_int_float.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct sg; econstructor; eauto.
Qed.

Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correct
             make_singleconst_correct make_singleoffloat_correct make_floatofsingle_correct
             make_floatofint_correct: cshm.
Hint Constructors eval_expr eval_exprlist: cshm.
Hint Extern 2 (@eq trace _ _) => traceEq: cshm.

Lemma make_cmpu_ne_zero_correct:
  forall e le m a n,
  eval_expr ge e le m a (Vint n) ->
  eval_expr ge e le m (make_cmpu_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros.
  assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero))
                                       (Vint (if Int.eq n Int.zero then Int.zero else Int.one))).
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    unfold Int.cmpu. destruct (Int.eq n Int.zero); auto. }
  assert (CMP: forall ob,
               Val.of_optbool ob = Vint n ->
               n = (if Int.eq n Int.zero then Int.zero else Int.one)).
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  { intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    rewrite Int.eq_false. auto. apply Int.one_not_zero.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    rewrite Int.eq_true. auto. }
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct a; simpl; auto. destruct b; auto.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl in H6. inv H6. eauto.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl in H6. inv H6. eauto.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl in H6. inv H6. eauto.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl in H6. inv H6. eauto.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
(* Goal: @eq Int.int n (if Int.eq n Int.zero then Int.zero else Int.one) *)
  simpl in H6. unfold Val.cmpl in H6.
(* Goal: @eq Z (Z.sub (Z.div (two_power_nat (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Zpos (xO xH))) (Zpos xH)) Int.max_signed *)
  destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
(* Goal: @eq Int.int n (if Int.eq n Int.zero then Int.zero else Int.one) *)
  simpl in H6. unfold Val.cmplu in H6.
(* Goal: @eq Z (Z.sub (Z.div (two_power_nat (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Zpos (xO xH))) (Zpos xH)) Int.max_signed *)
  destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [[]|]; inv H6; reflexivity.
Qed.

Lemma make_cmpu_ne_zero_correct_ptr:
  forall e le m a b i,
  eval_expr ge e le m a (Vptr b i) ->
  Archi.ptr64 = false ->
  Mem.weak_valid_pointer m b (Ptrofs.unsigned i) = true ->
  eval_expr ge e le m (make_cmpu_ne_zero a) Vone.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros.
(* Goal: eval_expr ge e le m (make_cmpu_ne_zero a) Vone *)
  assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) Vone).
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
(* Goal: @eq (option val) (@Some val (Val.of_optbool (if Archi.ptr64 then @None bool else if andb (Int.eq Int.zero Int.zero) (orb (Mem.valid_pointer m b (Ptrofs.unsigned i)) (Mem.valid_pointer m b (Z.sub (Ptrofs.unsigned i) (Zpos xH)))) then Val.cmp_different_blocks Cne else @None bool))) (@Some val Vone) *)
    unfold Mem.weak_valid_pointer in H1. rewrite H0, H1.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    rewrite Int.eq_true; auto. }
(* Goal: eval_expr ge e le m (make_cmpu_ne_zero a) Vone *)
  assert (OF_OPTBOOL: forall ob, Some (Val.of_optbool ob) <> Some (Vptr b i)).
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  { intros. destruct ob as [[]|]; discriminate. }
(* Goal: eval_expr ge e le m (make_cmpu_ne_zero a) Vone *)
  assert (OF_BOOL: forall ob, option_map Val.of_bool ob <> Some (Vptr b i)).
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  { intros. destruct ob as [[]|]; discriminate. }
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct a; simpl; auto. destruct b0; auto.
- inv H; eelim OF_OPTBOOL; eauto.
- inv H; eelim OF_OPTBOOL; eauto.
- inv H; eelim OF_OPTBOOL; eauto.
- inv H; eelim OF_OPTBOOL; eauto.
- inv H; eelim OF_BOOL; eauto.
- inv H; eelim OF_BOOL; eauto.
Qed.

Lemma make_cast_int_correct:
  forall e le m a n sz si,
  eval_expr ge e le m a (Vint n) ->
  eval_expr ge e le m (make_cast_int a sz si) (Vint (cast_int_int sz si n)).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold make_cast_int, cast_int_int.
(* Goal: eval_expr ge e le m match sz with | I8 => match si with | Signed => Eunop Ocast8signed a | Unsigned => Eunop Ocast8unsigned a end | I16 => match si with | Signed => Eunop Ocast16signed a | Unsigned => Eunop Ocast16unsigned a end | I32 => a | IBool => make_cmpu_ne_zero a end (Vint match sz with | I8 => match si with | Signed => Int.sign_ext (Zpos (xO (xO (xO xH)))) n | Unsigned => Int.zero_ext (Zpos (xO (xO (xO xH)))) n end | I16 => match si with | Signed => Int.sign_ext (Zpos (xO (xO (xO (xO xH))))) n | Unsigned => Int.zero_ext (Zpos (xO (xO (xO (xO xH))))) n end | I32 => n | IBool => if Int.eq n Int.zero then Int.zero else Int.one end) *)
  destruct sz.
(* Goal: eval_expr ge e le m match si with | Signed => Eunop Olongofint a | Unsigned => Eunop Olongofintu a end (Vlong match si with | Signed => Int64.repr (Int.signed n) | Unsigned => Int64.repr (Int.unsigned n) end) *)
  destruct si; eauto with cshm.
(* Goal: eval_expr ge e le m match si with | Signed => Eunop Olongofint a | Unsigned => Eunop Olongofintu a end (Vlong match si with | Signed => Int64.repr (Int.signed n) | Unsigned => Int64.repr (Int.unsigned n) end) *)
  destruct si; eauto with cshm.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply make_cmpu_ne_zero_correct; auto.
Qed.

Lemma make_longofint_correct:
  forall e le m a n si,
  eval_expr ge e le m a (Vint n) ->
  eval_expr ge e le m (make_longofint a si) (Vlong (cast_int_long si n)).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold make_longofint, cast_int_long. destruct si; eauto with cshm.
Qed.

Hint Resolve make_cast_int_correct make_longofint_correct: cshm.

Ltac InvEval :=
  match goal with
  | [ H: None = Some _ |- _ ] => discriminate
  | [ H: Some _ = Some _ |- _ ] => inv H; InvEval
  | [ H: match ?x with Some _ => _ | None => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval
  | [ H: match ?x with true => _ | false => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval
  | _ => idtac
  end.

Lemma make_cast_correct:
  forall e le m a b v ty1 ty2 v',
  make_cast ty1 ty2 a = OK b ->
  eval_expr ge e le m a v ->
  sem_cast v ty1 ty2 m = Some v' ->
  eval_expr ge e le m b v'.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold make_cast, sem_cast in *;
(* Goal: eval_expr ge e le m (Eunop Olongofintu a) (Vlong (Int64.repr (Int.unsigned i))) *)
(* Goal: @eq Int64.int (Int64.repr (Int.unsigned i)) (Ptrofs.to_int64 (Ptrofs.of_intu i)) *)
  destruct (classify_cast ty1 ty2); inv H; destruct v; InvEval; eauto with cshm.
- (* single -> int *)
(* Goal: eval_expr ge e le m (make_singleofint a si1) (Vsingle (cast_int_single si1 i)) *)
  unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm.
- (* float -> int *)
(* Goal: eval_expr ge e le m (make_cast_int (make_intofsingle a si2) sz2 si2) (Vint (cast_int_int sz2 si2 i)) *)
  apply make_cast_int_correct.
(* Goal: eval_expr ge e le m (make_intoffloat a si2) (Vint i) *)
  unfold cast_float_int in Heqo. unfold make_intoffloat.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto.
- (* single -> int *)
(* Goal: eval_expr ge e le m (make_cast_int (make_intofsingle a si2) sz2 si2) (Vint (cast_int_int sz2 si2 i)) *)
  apply make_cast_int_correct.
(* Goal: eval_expr ge e le m (make_intofsingle a si2) (Vint i) *)
  unfold cast_single_int in Heqo. unfold make_intofsingle.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto.
- (* long -> float *)
(* Goal: eval_expr ge e le m match si1 with | Signed => Eunop Osingleoflong a | Unsigned => Eunop Osingleoflongu a end (Vsingle match si1 with | Signed => Float32.of_long i | Unsigned => Float32.of_longu i end) *)
  unfold make_floatoflong, cast_long_float. destruct si1; eauto with cshm.
- (* long -> single *)
(* Goal: eval_expr ge e le m match si1 with | Signed => Eunop Osingleoflong a | Unsigned => Eunop Osingleoflongu a end (Vsingle match si1 with | Signed => Float32.of_long i | Unsigned => Float32.of_longu i end) *)
  unfold make_singleoflong, cast_long_single. destruct si1; eauto with cshm.
- (* float -> long *)
(* Goal: eval_expr ge e le m (make_longoffloat a si2) (Vlong i) *)
  unfold cast_float_long in Heqo. unfold make_longoffloat.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto.
- (* single -> long *)
(* Goal: eval_expr ge e le m (make_longofsingle a si2) (Vlong i) *)
  unfold cast_single_long in Heqo. unfold make_longofsingle.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto.
- (* int -> bool *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply make_cmpu_ne_zero_correct; auto.
- (* pointer (32 bits) -> bool *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_cmpu_ne_zero_correct_ptr; eauto.
- (* long -> bool *)
(* Goal: eval_expr ge e le m (Ebinop Oshll a b) (Vlong (Int64.shl i (Int64.repr (Int.unsigned i0)))) *)
  econstructor; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (Int64.eq i Int64.zero); auto.
- (* pointer (64 bits) -> bool *)
(* Goal: eval_expr ge e le m (Ebinop Oshll a b) (Vlong (Int64.shl i (Int64.repr (Int.unsigned i0)))) *)
  econstructor; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in Heqb1.
(* Goal: @eq Z (Z.sub (Z.div (two_power_nat (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Zpos (xO xH))) (Zpos xH)) Int.max_signed *)
  rewrite Heqb0, Heqb1. rewrite Int64.eq_true. reflexivity.
- (* float -> bool *)
(* Goal: eval_expr ge e le m (Ebinop Oshll a b) (Vlong (Int64.shl i (Int64.repr (Int.unsigned i0)))) *)
  econstructor; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (Float.cmp Ceq f Float.zero); auto.
- (* single -> bool *)
(* Goal: eval_expr ge e le m (Ebinop Oshll a b) (Vlong (Int64.shl i (Int64.repr (Int.unsigned i0)))) *)
  econstructor; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  simpl. unfold Val.cmpfs, Val.cmpfs_bool. rewrite Float32.cmp_ne_eq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (Float32.cmp Ceq f Float32.zero); auto.
- (* struct *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (ident_eq id1 id2); inv H1; auto.
- (* union *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (ident_eq id1 id2); inv H1; auto.
Qed.

Lemma make_boolean_correct:
 forall e le m a v ty b,
  eval_expr ge e le m a v ->
  bool_val v ty m = Some b ->
  exists vb,
    eval_expr ge e le m (make_boolean a ty) vb
    /\ Val.bool_of_val vb b.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold make_boolean. unfold bool_val in H0.
  destruct (classify_bool ty); destruct v; InvEval.
- (* int *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; split. apply make_cmpu_ne_zero_correct with (n := i); auto.
  destruct (Int.eq i Int.zero); simpl; constructor.
- (* ptr 32 bits *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exists Vone; split. eapply make_cmpu_ne_zero_correct_ptr; eauto. constructor.
- (* long *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmplu. simpl. eauto.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  destruct (Int64.eq i Int64.zero); simpl; constructor.
- (* ptr 64 bits *)
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  exists Vone; split.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool.
(* Goal: @eq Z (Z.sub (Z.div (two_power_nat (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Zpos (xO xH))) (Zpos xH)) Int.max_signed *)
  unfold Mem.weak_valid_pointer in Heqb0. rewrite Heqb0, Heqb1, Int64.eq_true. reflexivity.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  constructor.
- (* float *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; split. econstructor; eauto with cshm. simpl. eauto.
  unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  destruct (Float.cmp Cne f Float.zero); constructor.
- (* single *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; split. econstructor; eauto with cshm. simpl. eauto.
  unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  destruct (Float32.cmp Cne f Float32.zero); constructor.
Qed.

Lemma make_neg_correct:
  forall a tya c va v e le m,
  sem_neg va tya = Some v ->
  make_neg a tya = OK c ->
  eval_expr ge e le m a va ->
  eval_expr ge e le m c v.
Proof.
  unfold sem_neg, make_neg; intros until m; intros SEM MAKE EV1;
(* Goal: eval_expr ge e le m (Eunop Olongofintu a) (Vlong (Int64.repr (Int.unsigned i))) *)
(* Goal: @eq Int64.int (Int64.repr (Int.unsigned i)) (Ptrofs.to_int64 (Ptrofs.of_intu i)) *)
  destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
Qed.

Lemma make_absfloat_correct:
  forall a tya c va v e le m,
  sem_absfloat va tya = Some v ->
  make_absfloat a tya = OK c ->
  eval_expr ge e le m a va ->
  eval_expr ge e le m c v.
Proof.
  unfold sem_absfloat, make_absfloat; intros until m; intros SEM MAKE EV1;
(* Goal: eval_expr ge e le m (Eunop Olongofintu a) (Vlong (Int64.repr (Int.unsigned i))) *)
(* Goal: @eq Int64.int (Int64.repr (Int.unsigned i)) (Ptrofs.to_int64 (Ptrofs.of_intu i)) *)
  destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
(* Goal: eval_expr ge e le m (make_floatoflong a si1) (Vfloat (cast_long_float si1 i)) *)
  unfold make_floatoflong, cast_long_float. destruct s.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto.
Qed.

Lemma make_notbool_correct:
  forall a tya c va v e le m,
  sem_notbool va tya m = Some v ->
  make_notbool a tya = OK c ->
  eval_expr ge e le m a va ->
  eval_expr ge e le m c v.
Proof.
(* Goal: forall (a : expr) (tya : type) (c : expr) (va v : val) (e : env) (le : temp_env) (m : Mem.mem) (_ : @eq (option val) (sem_notbool va tya m) (@Some val v)) (_ : @eq (res expr) (make_notbool a tya) (@OK expr c)) (_ : eval_expr ge e le m a va), eval_expr ge e le m c v *)
  unfold sem_notbool, bool_val, make_notbool; intros until m; intros SEM MAKE EV1.
(* Goal: eval_expr ge e le m c v *)
  destruct (classify_bool tya); inv MAKE; destruct va; simpl in SEM; InvEval.
- econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (Int.eq i Int.zero); auto.
- destruct Archi.ptr64 eqn:SF; inv SEM.
(* Goal: eval_expr ge e le m (Ebinop (Ocmplu Ceq) a (make_longconst Int64.zero)) v *)
  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int.eq_true. auto.
- econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (Int64.eq i Int64.zero); auto.
- destruct Archi.ptr64 eqn:SF; inv SEM.
(* Goal: eval_expr ge e le m (Ebinop (Ocmplu Ceq) a (make_longconst Int64.zero)) v *)
  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int64.eq_true. auto.
- econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (Float.cmp Ceq f Float.zero); auto.
- econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (Float32.cmp Ceq f Float32.zero); auto.
Qed.

Lemma make_notint_correct:
  forall a tya c va v e le m,
  sem_notint va tya = Some v ->
  make_notint a tya = OK c ->
  eval_expr ge e le m a va ->
  eval_expr ge e le m c v.
Proof.
  unfold sem_notint, make_notint; intros until m; intros SEM MAKE EV1;
(* Goal: eval_expr ge e le m (Eunop Olongofintu a) (Vlong (Int64.repr (Int.unsigned i))) *)
(* Goal: @eq Int64.int (Int64.repr (Int.unsigned i)) (Ptrofs.to_int64 (Ptrofs.of_intu i)) *)
  destruct (classify_notint tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
Qed.

Definition binary_constructor_correct
    (make: expr -> type -> expr -> type -> res expr)
    (sem: val -> type -> val -> type -> mem -> option val): Prop :=
  forall a tya b tyb c va vb v e le m,
  sem va tya vb tyb m = Some v ->
  make a tya b tyb = OK c ->
  eval_expr ge e le m a va ->
  eval_expr ge e le m b vb ->
  eval_expr ge e le m c v.

Definition shift_constructor_correct
    (make: expr -> type -> expr -> type -> res expr)
    (sem: val -> type -> val -> type -> option val): Prop :=
  forall a tya b tyb c va vb v e le m,
  sem va tya vb tyb = Some v ->
  make a tya b tyb = OK c ->
  eval_expr ge e le m a va ->
  eval_expr ge e le m b vb ->
  eval_expr ge e le m c v.

Section MAKE_BIN.

Variable sem_int: signedness -> int -> int -> option val.
Variable sem_long: signedness -> int64 -> int64 -> option val.
Variable sem_float: float -> float -> option val.
Variable sem_single: float32 -> float32 -> option val.
Variables iop iopu fop sop lop lopu: binary_operation.

Hypothesis iop_ok:
  forall x y m, eval_binop iop (Vint x) (Vint y) m = sem_int Signed x y.
Hypothesis iopu_ok:
  forall x y m, eval_binop iopu (Vint x) (Vint y) m = sem_int Unsigned x y.
Hypothesis lop_ok:
  forall x y m, eval_binop lop (Vlong x) (Vlong y) m = sem_long Signed x y.
Hypothesis lopu_ok:
  forall x y m, eval_binop lopu (Vlong x) (Vlong y) m = sem_long Unsigned x y.
Hypothesis fop_ok:
  forall x y m, eval_binop fop (Vfloat x) (Vfloat y) m = sem_float x y.
Hypothesis sop_ok:
  forall x y m, eval_binop sop (Vsingle x) (Vsingle y) m = sem_single x y.

Lemma make_binarith_correct:
  binary_constructor_correct
    (make_binarith iop iopu fop sop lop lopu)
    (sem_binarith sem_int sem_long sem_float sem_single).
Proof.
  red; unfold make_binarith, sem_binarith;
  intros until m; intros SEM MAKE EV1 EV2.
  set (cls := classify_binarith tya tyb) in *.
  set (ty := binarith_type cls) in *.
  monadInv MAKE.
  destruct (sem_cast va tya ty m) as [va'|] eqn:Ca; try discriminate.
  destruct (sem_cast vb tyb ty m) as [vb'|] eqn:Cb; try discriminate.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'.
  destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate.
- destruct s; inv H0; econstructor; eauto with cshm.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite iop_ok; auto. rewrite iopu_ok; auto.
- destruct s; inv H0; econstructor; eauto with cshm.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite lop_ok; auto. rewrite lopu_ok; auto.
- erewrite <- fop_ok in SEM; eauto with cshm.
- erewrite <- sop_ok in SEM; eauto with cshm.
Qed.

Lemma make_binarith_int_correct:
  binary_constructor_correct
    (make_binarith_int iop iopu lop lopu)
    (sem_binarith sem_int sem_long (fun x y => None) (fun x y => None)).
Proof.
  red; unfold make_binarith_int, sem_binarith;
  intros until m; intros SEM MAKE EV1 EV2.
  set (cls := classify_binarith tya tyb) in *.
  set (ty := binarith_type cls) in *.
  monadInv MAKE.
  destruct (sem_cast va tya ty m) as [va'|] eqn:Ca; try discriminate.
  destruct (sem_cast vb tyb ty m) as [vb'|] eqn:Cb; try discriminate.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit make_cast_correct. eexact EQ1. eauto. eauto. intros EV2'.
  destruct cls; inv EQ2; destruct va'; try discriminate; destruct vb'; try discriminate.
- destruct s; inv H0; econstructor; eauto with cshm.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite iop_ok; auto. rewrite iopu_ok; auto.
- destruct s; inv H0; econstructor; eauto with cshm.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite lop_ok; auto. rewrite lopu_ok; auto.
Qed.

End MAKE_BIN.

Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm.

Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)).
Proof.
  assert (A: forall ty si a b c e le m va vb v,
             make_add_ptr_int cunit.(prog_comp_env) ty si a b = OK c ->
             eval_expr ge e le m a va -> eval_expr ge e le m b vb ->
             sem_add_ptr_int (prog_comp_env prog) ty si va vb = Some v ->
             eval_expr ge e le m c v).
(* Goal: @eq Z (Int64.unsigned i) (Int.unsigned (Int64.loword i)) *)
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  { unfold make_add_ptr_int, sem_add_ptr_int; intros until v; intros MAKE EV1 EV2 SEM; monadInv MAKE.
(* Goal: eval_expr ge e le m c v *)
    destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
  - destruct va; InvEval; destruct vb; inv SEM.
  + eauto with cshm.
  + econstructor; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
    simpl. rewrite SF. f_equal. f_equal. f_equal.
(* Goal: @eq Ptrofs.int (Ptrofs.of_int64 (Int64.mul (Int64.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (cast_int_long si i0))) (Ptrofs.mul (Ptrofs.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (ptrofs_of_int si i0)) *)
    assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    { destruct si; simpl; apply Ptrofs.agree64_repr; auto. }
(* Goal: @eq Int64.int (Ptrofs.to_int64 (Ptrofs.of_int64 i)) i *)
    auto with ptrofs.
  - destruct va; InvEval; destruct vb; inv SEM.
  + eauto with cshm.
  + econstructor; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
    simpl. rewrite SF. f_equal. f_equal. f_equal.
(* Goal: @eq Ptrofs.int (Ptrofs.of_int (Int.mul (Int.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) i0)) (Ptrofs.mul (Ptrofs.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (ptrofs_of_int si i0)) *)
    assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs).
(* Goal: @eq Int64.int (Ptrofs.to_int64 (Ptrofs.of_int64 i)) i *)
    auto with ptrofs.
  }
  assert (B: forall ty a b c e le m va vb v,
             make_add_ptr_long cunit.(prog_comp_env) ty a b = OK c ->
             eval_expr ge e le m a va -> eval_expr ge e le m b vb ->
             sem_add_ptr_long (prog_comp_env prog) ty va vb = Some v ->
             eval_expr ge e le m c v).
(* Goal: @eq Z (Int64.unsigned i) (Int.unsigned (Int64.loword i)) *)
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  { unfold make_add_ptr_long, sem_add_ptr_long; intros until v; intros MAKE EV1 EV2 SEM; monadInv MAKE.
(* Goal: eval_expr ge e le m c v *)
    destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
  - destruct va; InvEval; destruct vb; inv SEM.
  + eauto with cshm.
  + econstructor; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
    simpl. rewrite SF. f_equal. f_equal. f_equal. auto with ptrofs.
  - destruct va; InvEval; destruct vb; inv SEM.
  + eauto with cshm.
  + econstructor; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
    simpl. rewrite SF. f_equal. f_equal. f_equal.
(* Goal: @eq Ptrofs.int (Ptrofs.of_int (Int.mul (Int.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (Int64.loword i0))) (Ptrofs.mul (Ptrofs.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (Ptrofs.of_int64 i0)) *)
    assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto).
(* Goal: @eq Int64.int (Ptrofs.to_int64 (Ptrofs.of_int64 i)) i *)
    auto with ptrofs.
  }
  red; unfold make_add, sem_add;
  intros until m; intros SEM MAKE EV1 EV2;
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (classify_add tya tyb); eauto.
- eapply make_binarith_correct; eauto; intros; auto.
Qed.

Lemma make_sub_correct: binary_constructor_correct (make_sub cunit.(prog_comp_env)) (sem_sub prog.(prog_comp_env)).
Proof.
  red; unfold make_sub, sem_sub;
  intros until m; intros SEM MAKE EV1 EV2;
  destruct (classify_sub tya tyb); try (monadInv MAKE).
- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
+ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
(* Goal: eval_expr ge e le m (Ebinop Oshll a b) (Vlong (Int64.shl i (Int64.repr (Int.unsigned i0)))) *)
  econstructor; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
(* Goal: @eq Ptrofs.int (Ptrofs.of_int64 (Int64.mul (Int64.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (cast_int_long si i0))) (Ptrofs.mul (Ptrofs.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (ptrofs_of_int si i0)) *)
  assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  { destruct si; simpl; apply Ptrofs.agree64_repr; auto. }
(* Goal: @eq Int64.int (Ptrofs.to_int64 (Ptrofs.of_int64 i)) i *)
  auto with ptrofs.
+ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
(* Goal: @eq Ptrofs.int (Ptrofs.of_int (Int.mul (Int.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) i0)) (Ptrofs.mul (Ptrofs.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (ptrofs_of_int si i0)) *)
  assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs).
(* Goal: @eq Int64.int (Ptrofs.to_int64 (Ptrofs.of_int64 i)) i *)
  auto with ptrofs.
- rewrite (transl_sizeof _ _ _ _ LINK EQ) in EQ0. clear EQ.
(* Goal: eval_expr ge e le m c v *)
  set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *.
(* Goal: eval_expr ge e le m c v *)
  destruct va; InvEval; destruct vb; InvEval.
(* Goal: eval_expr ge e le m c v *)
  destruct (eq_block b0 b1); try discriminate.
(* Goal: eval_expr ge e le m c v *)
  destruct (zlt 0 sz); try discriminate.
(* Goal: eval_expr ge e le m c v *)
  destruct (zle sz Ptrofs.max_signed); simpl in SEM; inv SEM.
(* Goal: eval_expr ge e le m c (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz))) *)
  assert (E1: Ptrofs.signed (Ptrofs.repr sz) = sz).
(* Goal: @eq Z (Int64.unsigned i) (Int.unsigned (Int64.loword i)) *)
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  { apply Ptrofs.signed_repr. generalize Ptrofs.min_signed_neg; omega. }
(* Goal: eval_expr ge e le m c (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz))) *)
  destruct Archi.ptr64 eqn:SF; inversion EQ0; clear EQ0; subst c.
+ assert (E: Int64.signed (Int64.repr sz) = sz).
(* Goal: @eq Z (Int64.unsigned i) (Int.unsigned (Int64.loword i)) *)
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  { apply Int64.signed_repr.
(* Goal: and (Z.le Int64.min_signed sz) (Z.le sz Int64.max_signed) *)
    replace Int64.max_signed with Ptrofs.max_signed.
(* Goal: and (Z.le Int64.min_signed sz) (Z.le sz Ptrofs.max_signed) *)
(* Goal: @eq Z Ptrofs.max_signed Int64.max_signed *)
    generalize Int64.min_signed_neg; omega.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    unfold Ptrofs.max_signed, Ptrofs.half_modulus; rewrite Ptrofs.modulus_eq64 by auto. reflexivity. }
(* Goal: eval_expr ge e le m (Ebinop Oshll a b) (Vlong (Int64.shl i (Int64.repr (Int.unsigned i0)))) *)
  econstructor; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  rewrite SF, dec_eq_true. simpl.
(* Goal: @eq (option val) (if orb (Int64.eq (Int64.repr sz) Int64.zero) (andb (Int64.eq (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr Int64.min_signed)) (Int64.eq (Int64.repr sz) Int64.mone)) then @None val else @Some val (Vlong (Int64.divs (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
  predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.zero.
(* Goal: @eq (option val) (if orb true (andb (Int64.eq (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr Int64.min_signed)) (Int64.eq (Int64.repr sz) Int64.mone)) then @None val else @Some val (Vlong (Int64.divs (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
(* Goal: @eq (option val) (if orb false (andb (Int64.eq (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr Int64.min_signed)) (Int64.eq (Int64.repr sz) Int64.mone)) then @None val else @Some val (Vlong (Int64.divs (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
  rewrite H in E; rewrite Int64.signed_zero in E; omegaContradiction.
(* Goal: @eq (option val) (if orb false (andb (Int64.eq (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr Int64.min_signed)) (Int64.eq (Int64.repr sz) Int64.mone)) then @None val else @Some val (Vlong (Int64.divs (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
  predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.mone.
(* Goal: @eq (option val) (if orb false (andb (Int64.eq (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr Int64.min_signed)) true) then @None val else @Some val (Vlong (Int64.divs (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
(* Goal: @eq (option val) (if orb false (andb (Int64.eq (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr Int64.min_signed)) false) then @None val else @Some val (Vlong (Int64.divs (Ptrofs.to_int64 (Ptrofs.sub i i0)) (Int64.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
  rewrite H0 in E; rewrite Int64.signed_mone in E; omegaContradiction.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal.
(* Goal: @eq Ptrofs.int (Ptrofs.add i (Ptrofs.of_int (Int.mul (Int.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (Int64.loword i0)))) (Ptrofs.add i (Ptrofs.mul (Ptrofs.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (Ptrofs.of_int64 i0))) *)
  apply f_equal. symmetry. auto with ptrofs.
+ assert (E: Int.signed (Int.repr sz) = sz).
(* Goal: @eq Z (Int64.unsigned i) (Int.unsigned (Int64.loword i)) *)
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  { apply Int.signed_repr.
(* Goal: and (Z.le Int.min_signed sz) (Z.le sz Int.max_signed) *)
    replace Int.max_signed with Ptrofs.max_signed.
(* Goal: and (Z.le Int.min_signed sz) (Z.le sz Ptrofs.max_signed) *)
(* Goal: @eq Z Ptrofs.max_signed Int.max_signed *)
    generalize Int.min_signed_neg; omega.
(* Goal: @eq Z (Z.sub (Z.div (two_power_nat (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Zpos (xO xH))) (Zpos xH)) Int.max_signed *)
    unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity.
  }
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl.
(* Goal: @eq (option val) (if orb (Int.eq (Int.repr sz) Int.zero) (andb (Int.eq (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr Int.min_signed)) (Int.eq (Int.repr sz) Int.mone)) then @None val else @Some val (Vint (Int.divs (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
  predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero.
(* Goal: @eq (option val) (if orb true (andb (Int.eq (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr Int.min_signed)) (Int.eq (Int.repr sz) Int.mone)) then @None val else @Some val (Vint (Int.divs (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
(* Goal: @eq (option val) (if orb false (andb (Int.eq (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr Int.min_signed)) (Int.eq (Int.repr sz) Int.mone)) then @None val else @Some val (Vint (Int.divs (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
  rewrite H in E; rewrite Int.signed_zero in E; omegaContradiction.
(* Goal: @eq (option val) (if orb false (andb (Int.eq (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr Int.min_signed)) (Int.eq (Int.repr sz) Int.mone)) then @None val else @Some val (Vint (Int.divs (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
  predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone.
(* Goal: @eq (option val) (if orb false (andb (Int.eq (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr Int.min_signed)) true) then @None val else @Some val (Vint (Int.divs (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
(* Goal: @eq (option val) (if orb false (andb (Int.eq (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr Int.min_signed)) false) then @None val else @Some val (Vint (Int.divs (Ptrofs.to_int (Ptrofs.sub i i0)) (Int.repr sz)))) (@Some val (Vptrofs (Ptrofs.divs (Ptrofs.sub i i0) (Ptrofs.repr sz)))) *)
  rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal. apply f_equal.
(* Goal: @eq Int64.int i (Ptrofs.to_int64 (Ptrofs.of_int64 i)) *)
  symmetry. auto with ptrofs.
- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
+ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
(* Goal: eval_expr ge e le m (Ebinop Oshll a b) (Vlong (Int64.shl i (Int64.repr (Int.unsigned i0)))) *)
  econstructor; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
(* Goal: @eq Int64.int (Ptrofs.to_int64 (Ptrofs.of_int64 i)) i *)
  auto with ptrofs.
+ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
(* Goal: @eq Ptrofs.int (Ptrofs.of_int (Int.mul (Int.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (Int64.loword i0))) (Ptrofs.mul (Ptrofs.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (Ptrofs.of_int64 i0)) *)
  assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto).
(* Goal: @eq Int64.int (Ptrofs.to_int64 (Ptrofs.of_int64 i)) i *)
  auto with ptrofs.
- eapply make_binarith_correct; eauto; intros; auto.
Qed.

Lemma make_mul_correct: binary_constructor_correct make_mul sem_mul.
Proof.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply make_binarith_correct; intros; auto.
Qed.

Lemma make_div_correct: binary_constructor_correct make_div sem_div.
Proof.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply make_binarith_correct; intros; auto.
Qed.

Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod.
Proof.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply make_binarith_int_correct; intros; auto.
Qed.

Lemma make_and_correct: binary_constructor_correct make_and sem_and.
Proof.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply make_binarith_int_correct; intros; auto.
Qed.

Lemma make_or_correct: binary_constructor_correct make_or sem_or.
Proof.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply make_binarith_int_correct; intros; auto.
Qed.

Lemma make_xor_correct: binary_constructor_correct make_xor sem_xor.
Proof.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply make_binarith_int_correct; intros; auto.
Qed.

Ltac comput val :=
  let x := fresh in set val as x in *; vm_compute in x; subst x.

Remark small_shift_amount_1:
  forall i,
  Int64.ltu i Int64.iwordsize = true ->
  Int.ltu (Int64.loword i) Int64.iwordsize' = true
  /\ Int64.unsigned i = Int.unsigned (Int64.loword i).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. apply Int64.ltu_inv in H. comput (Int64.unsigned Int64.iwordsize).
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  assert (Int64.unsigned i = Int.unsigned (Int64.loword i)).
(* Goal: @eq Z (Int64.unsigned i) (Int.unsigned (Int64.loword i)) *)
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  {
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    unfold Int64.loword. rewrite Int.unsigned_repr; auto.
(* Goal: and (Z.le Z0 (Int64.unsigned i)) (Z.le (Int64.unsigned i) Int.max_unsigned) *)
    comput Int.max_unsigned; omega.
  }
  split; auto. unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto.
Qed.

Remark small_shift_amount_2:
  forall i,
  Int64.ltu i (Int64.repr 32) = true ->
  Int.ltu (Int64.loword i) Int.iwordsize = true.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. apply Int64.ltu_inv in H. comput (Int64.unsigned (Int64.repr 32)).
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  assert (Int64.unsigned i = Int.unsigned (Int64.loword i)).
(* Goal: @eq Z (Int64.unsigned i) (Int.unsigned (Int64.loword i)) *)
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  {
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    unfold Int64.loword. rewrite Int.unsigned_repr; auto.
(* Goal: and (Z.le Z0 (Int64.unsigned i)) (Z.le (Int64.unsigned i) Int.max_unsigned) *)
    comput Int.max_unsigned; omega.
  }
  unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto.
Qed.

Lemma small_shift_amount_3:
  forall i,
  Int.ltu i Int64.iwordsize' = true ->
  Int64.unsigned (Int64.repr (Int.unsigned i)) = Int.unsigned i.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. apply Int.ltu_inv in H. comput (Int.unsigned Int64.iwordsize').
(* Goal: @eq Z (Int64.unsigned (Int64.repr (Int.unsigned i))) (Int.unsigned i) *)
  apply Int64.unsigned_repr. comput Int64.max_unsigned; omega.
Qed.

Lemma make_shl_correct: shift_constructor_correct make_shl sem_shl.
Proof.
  red; unfold make_shl, sem_shl, sem_shift;
  intros until m; intros SEM MAKE EV1 EV2;
  destruct (classify_shift tya tyb); inv MAKE;
  destruct va; try discriminate; destruct vb; try discriminate.
- destruct (Int.ltu i0 Int.iwordsize) eqn:E; inv SEM.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. simpl; rewrite E; auto.
- destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit small_shift_amount_1; eauto. intros [A B].
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  econstructor; eauto with cshm. simpl. rewrite A.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  f_equal; f_equal. unfold Int64.shl', Int64.shl. rewrite B; auto.
- destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto with cshm. simpl. rewrite small_shift_amount_2; auto.
- destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  econstructor; eauto with cshm. simpl. rewrite E.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  unfold Int64.shl', Int64.shl. rewrite small_shift_amount_3; auto.
Qed.

Lemma make_shr_correct: shift_constructor_correct make_shr sem_shr.
Proof.
  red; unfold make_shr, sem_shr, sem_shift;
  intros until m; intros SEM MAKE EV1 EV2;
  destruct (classify_shift tya tyb); inv MAKE;
  destruct va; try discriminate; destruct vb; try discriminate.
- destruct (Int.ltu i0 Int.iwordsize) eqn:E; inv SEM.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct s; inv H0; econstructor; eauto; simpl; rewrite E; auto.
- destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit small_shift_amount_1; eauto. intros [A B].
  destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite A;
(* Goal: @eq Ptrofs.int (Ptrofs.add i (Ptrofs.of_int (Int.mul (Int.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (Int64.loword i0)))) (Ptrofs.add i (Ptrofs.mul (Ptrofs.repr (Ctypes.sizeof (@prog_comp_env Clight.function prog) ty)) (Ptrofs.of_int64 i0))) *)
  f_equal; f_equal.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  unfold Int64.shr', Int64.shr; rewrite B; auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  unfold Int64.shru', Int64.shru; rewrite B; auto.
- destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite small_shift_amount_2; auto.
- destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM.
(* Goal: @eq (option val) (@Some val (if Int.ltu i0 Int64.iwordsize' then Vlong (Int64.shl' i i0) else Vundef)) (@Some val (Vlong (Int64.shl i (Int64.repr (Int.unsigned i0))))) *)
  destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite E.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  unfold Int64.shr', Int64.shr; rewrite small_shift_amount_3; auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto.
Qed.

Lemma make_cmp_ptr_correct:
  forall cmp e le m a va b vb v,
  cmp_ptr m cmp va vb = Some v ->
  eval_expr ge e le m a va ->
  eval_expr ge e le m b vb ->
  eval_expr ge e le m (make_cmp_ptr cmp a b) v.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  unfold cmp_ptr, make_cmp_ptr; intros.
(* Goal: eval_expr ge e le m (Ebinop (if Archi.ptr64 then Ocmplu cmp else Ocmpu cmp) a b) v *)
  destruct Archi.ptr64.
- econstructor; eauto.
- econstructor; eauto. simpl. unfold Val.cmpu.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bo|]; inv H. auto.
Qed.

Remark make_ptrofs_of_int_correct:
  forall e le m a i si,
  eval_expr ge e le m a (Vint i) ->
  eval_expr ge e le m (if Archi.ptr64 then make_longofint a si else a) (Vptrofs (ptrofs_of_int si i)).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold Vptrofs, ptrofs_of_int. destruct Archi.ptr64 eqn:SF.
- unfold make_longofint. destruct si.
+ replace (Ptrofs.to_int64 (Ptrofs.of_ints i)) with (Int64.repr (Int.signed i)).
(* Goal: eval_expr ge e le m (Eunop Olongofintu a) (Vlong (Int64.repr (Int.unsigned i))) *)
(* Goal: @eq Int64.int (Int64.repr (Int.unsigned i)) (Ptrofs.to_int64 (Ptrofs.of_intu i)) *)
  eauto with cshm.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr.
+ replace (Ptrofs.to_int64 (Ptrofs.of_intu i)) with (Int64.repr (Int.unsigned i)).
(* Goal: eval_expr ge e le m (Eunop Olongofintu a) (Vlong (Int64.repr (Int.unsigned i))) *)
(* Goal: @eq Int64.int (Int64.repr (Int.unsigned i)) (Ptrofs.to_int64 (Ptrofs.of_intu i)) *)
  eauto with cshm.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr.
- destruct si.
+ replace (Ptrofs.to_int (Ptrofs.of_ints i)) with i. auto.
(* Goal: @eq Int64.int i (Ptrofs.to_int64 (Ptrofs.of_int64 i)) *)
  symmetry. auto with ptrofs.
+ replace (Ptrofs.to_int (Ptrofs.of_intu i)) with i. auto.
(* Goal: @eq Int64.int i (Ptrofs.to_int64 (Ptrofs.of_int64 i)) *)
  symmetry. auto with ptrofs.
Qed.

Remark make_ptrofs_of_int64_correct:
  forall e le m a i,
  eval_expr ge e le m a (Vlong i) ->
  eval_expr ge e le m (if Archi.ptr64 then a else Eunop Ointoflong a) (Vptrofs (Ptrofs.of_int64 i)).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. unfold Vptrofs. destruct Archi.ptr64 eqn:SF.
- replace (Ptrofs.to_int64 (Ptrofs.of_int64 i)) with i. auto.
(* Goal: @eq Int64.int i (Ptrofs.to_int64 (Ptrofs.of_int64 i)) *)
  symmetry. auto with ptrofs.
- econstructor; eauto. simpl. apply f_equal. apply f_equal.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply Int.eqm_samerepr. rewrite Ptrofs.eqm32 by auto. apply Ptrofs.eqm_unsigned_repr.
Qed.

Lemma make_cmp_correct: forall cmp, binary_constructor_correct (make_cmp cmp) (sem_cmp cmp).
Proof.
  red; unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2;
  destruct (classify_cmp tya tyb).
- inv MAKE. eapply make_cmp_ptr_correct; eauto.
- inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct.
- inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct.
- inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct.
- inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct.
- eapply make_binarith_correct; eauto; intros; auto.
Qed.

Lemma transl_unop_correct:
  forall op a tya c va v e le m,
  transl_unop op a tya = OK c ->
  sem_unary_operation op va tya m = Some v ->
  eval_expr ge e le m a va ->
  eval_expr ge e le m c v.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. destruct op; simpl in *.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_notbool_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_notint_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_neg_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_absfloat_correct; eauto.
Qed.

Lemma transl_binop_correct:
  forall op a tya b tyb c va vb v e le m,
  transl_binop cunit.(prog_comp_env) op a tya b tyb = OK c ->
  sem_binary_operation prog.(prog_comp_env) op va tya vb tyb m = Some v ->
  eval_expr ge e le m a va ->
  eval_expr ge e le m b vb ->
  eval_expr ge e le m c v.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. destruct op; simpl in *.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_add_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_sub_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_mul_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_div_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_mod_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_and_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_or_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_xor_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_shl_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_shr_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_cmp_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_cmp_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_cmp_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_cmp_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_cmp_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_cmp_correct; eauto.
Qed.

Lemma make_load_correct:
  forall addr ty code b ofs v e le m,
  make_load addr ty = OK code ->
  eval_expr ge e le m addr (Vptr b ofs) ->
  deref_loc ty m b ofs v ->
  eval_expr ge e le m code v.
Proof.
(* Goal: forall (addr : expr) (ty : type) (code : expr) (b : block) (ofs : Ptrofs.int) (v : val) (e : env) (le : temp_env) (m : Mem.mem) (_ : @eq (res expr) (make_load addr ty) (@OK expr code)) (_ : eval_expr ge e le m addr (Vptr b ofs)) (_ : deref_loc ty m b ofs v), eval_expr ge e le m code v *)
  unfold make_load; intros until m; intros MKLOAD EVEXP DEREF.
(* Goal: eval_expr ge e le m code v *)
  inv DEREF.
  (* scalar *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite H in MKLOAD. inv MKLOAD. apply eval_Eload with (Vptr b ofs); auto.
  (* by reference *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite H in MKLOAD. inv MKLOAD. auto.
  (* by copy *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite H in MKLOAD. inv MKLOAD. auto.
Qed.

Lemma make_memcpy_correct:
  forall f dst src ty k e le m b ofs v m' s,
  eval_expr ge e le m dst (Vptr b ofs) ->
  eval_expr ge e le m src v ->
  assign_loc prog.(prog_comp_env) ty m b ofs v m' ->
  access_mode ty = By_copy ->
  make_memcpy cunit.(prog_comp_env) dst src ty = OK s ->
  step ge (State f s k e le m) E0 (State f Sskip k e le m').
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. inv H1; try congruence.
  monadInv H3.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit transl_alignof_blockcopy. eexact LINK. eauto. intros [A B]. rewrite A, B.
  change le with (set_optvar None Vundef le) at 2.
(* Goal: eval_expr ge e le m (make_longconst n) (Vlong n) *)
  econstructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor. eauto. econstructor. eauto. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto.
  apply alignof_blockcopy_1248.
  apply sizeof_pos.
  apply sizeof_alignof_blockcopy_compat.
Qed.

Lemma make_store_correct:
  forall addr ty rhs code e le m b ofs v m' f k,
  make_store cunit.(prog_comp_env) addr ty rhs = OK code ->
  eval_expr ge e le m addr (Vptr b ofs) ->
  eval_expr ge e le m rhs v ->
  assign_loc prog.(prog_comp_env) ty m b ofs v m' ->
  step ge (State f code k e le m) E0 (State f Sskip k e le m').
Proof.
(* Goal: forall (addr : expr) (ty : type) (rhs : expr) (code : stmt) (e : env) (le : temp_env) (m : Mem.mem) (b : block) (ofs : Ptrofs.int) (v : val) (m' : Mem.mem) (f : function) (k : cont) (_ : @eq (res stmt) (make_store (@prog_comp_env Clight.function cunit) addr ty rhs) (@OK stmt code)) (_ : eval_expr ge e le m addr (Vptr b ofs)) (_ : eval_expr ge e le m rhs v) (_ : assign_loc (@prog_comp_env Clight.function prog) ty m b ofs v m'), step ge (State f code k e le m) E0 (State f Sskip k e le m') *)
  unfold make_store. intros until k; intros MKSTORE EV1 EV2 ASSIGN.
(* Goal: step ge (State f code k e le m) E0 (State f Sskip k e le m') *)
  inversion ASSIGN; subst.
  (* nonvolatile scalar *)
(* Goal: step ge (State f code k e le m) E0 (State f Sskip k e le m') *)
(* Goal: step ge (State f code k e le m) E0 (State f Sskip k e le m') *)
  rewrite H in MKSTORE; inv MKSTORE.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto.
  (* by copy *)
(* Goal: step ge (State f code k e le m) E0 (State f Sskip k e le m') *)
  rewrite H in MKSTORE.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto.
Qed.

End CONSTRUCTORS.

(** * Basic preservation invariants *)

Section CORRECTNESS.

Variable prog: Clight.program.
Variable tprog: Csharpminor.program.
Hypothesis TRANSL: match_prog prog tprog.

Let ge := globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
  forall s, Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof (Genv.find_symbol_match TRANSL).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_match TRANSL).

Lemma function_ptr_translated:
  forall v f,
  Genv.find_funct_ptr ge v = Some f ->
  exists cu tf, Genv.find_funct_ptr tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
Proof (Genv.find_funct_ptr_match TRANSL).

Lemma functions_translated:
  forall v f,
  Genv.find_funct ge v = Some f ->
  exists cu tf, Genv.find_funct tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
Proof (Genv.find_funct_match TRANSL).

(** * Matching between environments *)

(** In this section, we define a matching relation between
  a Clight local environment and a Csharpminor local environment. *)

Record match_env (e: Clight.env) (te: Csharpminor.env) : Prop :=
(* Goal: @eq Z (Int64.unsigned i) (Int.unsigned (Int64.loword i)) *)
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  mk_match_env {
    me_local:
      forall id b ty,
      e!id = Some (b, ty) -> te!id = Some(b, Ctypes.sizeof ge ty);
    me_local_inv:
      forall id b sz,
      te!id = Some (b, sz) -> exists ty, e!id = Some(b, ty)
  }.

Lemma match_env_globals:
  forall e te id,
  match_env e te ->
  e!id = None ->
  te!id = None.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. destruct (te!id) as [[b sz] | ] eqn:?; auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit me_local_inv; eauto. intros [ty EQ]. congruence.
Qed.

Lemma match_env_same_blocks:
  forall e te,
  match_env e te ->
  blocks_of_env te = Clight.blocks_of_env ge e.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros.
  set (R := fun (x: (block * type)) (y: (block * Z)) =>
         match x, y with
         | (b1, ty), (b2, sz) => b2 = b1 /\ sz = Ctypes.sizeof ge ty
         end).
  assert (list_forall2
            (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
            (PTree.elements e) (PTree.elements te)).
(* Goal: @list_forall2 (prod positive (prod block type)) (prod positive (prod block Z)) (fun (i_x : prod positive (prod block type)) (i_y : prod positive (prod block Z)) => and (@eq positive (@fst positive (prod block type) i_x) (@fst positive (prod block Z) i_y)) (R (@snd positive (prod block type) i_x) (@snd positive (prod block Z) i_y))) (@PTree.elements (prod block type) e) (@PTree.elements (prod block Z) te) *)
(* Goal: @eq (list (prod (prod block Z) Z)) (blocks_of_env te) (Clight.blocks_of_env ge e) *)
  apply PTree.elements_canonical_order.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  intros id [b ty] GET. exists (b, Ctypes.sizeof ge ty); split. eapply me_local; eauto. red; auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  intros id [b sz] GET. exploit me_local_inv; eauto. intros [ty EQ].
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit me_local; eauto. intros EQ1.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exists (b, ty); split. auto. red; split; congruence.

(* Goal: @eq (list (prod (prod block Z) Z)) (blocks_of_env te) (Clight.blocks_of_env ge e) *)
  unfold blocks_of_env, Clight.blocks_of_env.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  generalize H0. induction 1. auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl. f_equal; auto.
(* Goal: @eq (prod (prod block Z) Z) (block_of_binding b1) (Clight.block_of_binding ge a1) *)
  unfold block_of_binding, Clight.block_of_binding.
(* Goal: @eq (prod (prod block Z) Z) (let (_, p) := b1 in let (b, sz) := p in @pair (prod block Z) Z (@pair block Z b Z0) sz) (let (_, p) := a1 in let (b, ty) := p in @pair (prod block Z) Z (@pair block Z b Z0) (Ctypes.sizeof (genv_cenv ge) ty)) *)
  destruct a1 as [id1 [blk1 ty1]]. destruct b1 as [id2 [blk2 sz2]].
(* Goal: forall _ : @eq (option (prod block Z)) (@None (prod block Z)) (@Some (prod block Z) (@pair block Z b sz)), @ex type (fun ty : type => @eq (option (prod block type)) (@PTree.get (prod block type) id (PTree.empty (prod block type))) (@Some (prod block type) (@pair block type b ty))) *)
  simpl in *. destruct H1 as [A [B C]]. congruence.
Qed.

Lemma match_env_free_blocks:
  forall e te m m',
  match_env e te ->
  Mem.free_list m (Clight.blocks_of_env ge e) = Some m' ->
  Mem.free_list m (blocks_of_env te) = Some m'.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. rewrite (match_env_same_blocks _ _ H). auto.
Qed.

Lemma match_env_empty:
  match_env Clight.empty_env Csharpminor.empty_env.
Proof.
(* Goal: match_env Clight.empty_env empty_env *)
  unfold Clight.empty_env, Csharpminor.empty_env.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  constructor.
(* Goal: forall _ : @eq (option (prod block Z)) (@None (prod block Z)) (@Some (prod block Z) (@pair block Z b sz)), @ex type (fun ty : type => @eq (option (prod block type)) (@PTree.get (prod block type) id (PTree.empty (prod block type))) (@Some (prod block type) (@pair block type b ty))) *)
  intros until ty. repeat rewrite PTree.gempty. congruence.
(* Goal: forall _ : @eq (option (prod block Z)) (@None (prod block Z)) (@Some (prod block Z) (@pair block Z b sz)), @ex type (fun ty : type => @eq (option (prod block type)) (@PTree.get (prod block type) id (PTree.empty (prod block type))) (@Some (prod block type) (@pair block type b ty))) *)
  intros until sz. rewrite PTree.gempty. congruence.
Qed.

(** The following lemmas establish the [match_env] invariant at
  the beginning of a function invocation, after allocation of
  local variables and initialization of the parameters. *)

Lemma match_env_alloc_variables:
  forall cunit, linkorder cunit prog ->
  forall e1 m1 vars e2 m2, Clight.alloc_variables ge e1 m1 vars e2 m2 ->
  forall tvars te1,
  mmap (transl_var cunit.(prog_comp_env)) vars = OK tvars ->
  match_env e1 te1 ->
  exists te2,
  Csharpminor.alloc_variables te1 m1 tvars te2 m2
  /\ match_env e2 te2.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  induction 2; simpl; intros.
- inv H0. exists te1; split. constructor. auto.
- monadInv H2. monadInv EQ. simpl in *.
  exploit transl_sizeof. eexact H. eauto. intros SZ; rewrite SZ.
  exploit (IHalloc_variables x0 (PTree.set id (b1, Ctypes.sizeof ge ty) te1)).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  auto.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  constructor.
    (* me_local *)
    intros until ty0. repeat rewrite PTree.gsspec.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
    destruct (peq id0 id); intros. congruence. eapply me_local; eauto.
    (* me_local_inv *)
(* Goal: forall (id : positive) (b : block) (sz : Z) (_ : @eq (option (prod block Z)) (@PTree.get (prod block Z) id (PTree.empty (prod block Z))) (@Some (prod block Z) (@pair block Z b sz))), @ex type (fun ty : type => @eq (option (prod block type)) (@PTree.get (prod block type) id (PTree.empty (prod block type))) (@Some (prod block type) (@pair block type b ty))) *)
    intros until sz. repeat rewrite PTree.gsspec.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
    destruct (peq id0 id); intros. exists ty; congruence. eapply me_local_inv; eauto.
  intros [te2 [ALLOC MENV]].
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exists te2; split. econstructor; eauto. auto.
Qed.

Lemma create_undef_temps_match:
  forall temps,
  create_undef_temps (map fst temps) = Clight.create_undef_temps temps.
Proof.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  induction temps; simpl. auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct a as [id ty]. simpl. decEq. auto.
Qed.

Lemma bind_parameter_temps_match:
  forall vars vals le1 le2,
  Clight.bind_parameter_temps vars vals le1 = Some le2 ->
  bind_parameters (map fst vars) vals le1 = Some le2.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  induction vars; simpl; intros.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct vals; inv H. auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct a as [id ty]. destruct vals; try discriminate. auto.
Qed.

Lemma transl_vars_names:
  forall ce vars tvars,
  mmap (transl_var ce) vars = OK tvars ->
  map fst tvars = var_names vars.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. exploit mmap_inversion; eauto. generalize vars tvars. induction 1; simpl.
- auto.
- monadInv H0. simpl; congruence.
Qed.

(** * Proof of semantic preservation *)

(** ** Semantic preservation for expressions *)

(** The proof of semantic preservation for the translation of expressions
  relies on simulation diagrams of the following form:
<<
         e, le, m, a ------------------- te, le, m, ta
            |                                |
            |                                |
            |                                |
            v                                v
         e, le, m, v ------------------- te, le, m, v
>>
  Left: evaluation of r-value expression [a] in Clight.
  Right: evaluation of its translation [ta] in Csharpminor.
  Top (precondition): matching between environments [e], [te],
    plus well-typedness of expression [a].
  Bottom (postcondition): the result values [v]
    are identical in both evaluations.

  We state these diagrams as the following properties, parameterized
  by the Clight evaluation. *)

Section EXPR.

Variable cunit: Clight.program.
Hypothesis LINK: linkorder cunit prog.
Variable e: Clight.env.
Variable le: temp_env.
Variable m: mem.
Variable te: Csharpminor.env.
Hypothesis MENV: match_env e te.

Lemma transl_expr_lvalue_correct:
  (forall a v,
   Clight.eval_expr ge e le m a v ->
   forall ta (TR: transl_expr cunit.(prog_comp_env) a = OK ta) ,
   Csharpminor.eval_expr tge te le m ta v)
/\(forall a b ofs,
   Clight.eval_lvalue ge e le m a b ofs ->
   forall ta (TR: transl_lvalue cunit.(prog_comp_env) a = OK ta),
   Csharpminor.eval_expr tge te le m ta (Vptr b ofs)).
Proof.
  apply eval_expr_lvalue_ind; intros; try (monadInv TR).
- (* const int *)
(* Goal: eval_expr ge e le m (make_intconst (Int.repr n)) (Vint (Int.repr n)) *)
(* Goal: @eq Int.int (Int.repr n) (Ptrofs.to_int (Ptrofs.repr n)) *)
  apply make_intconst_correct.
- (* const float *)
  apply make_floatconst_correct.
- (* const single *)
  apply make_singleconst_correct.
- (* const long *)
(* Goal: eval_expr ge e le m (make_longconst (Int64.repr n)) (Vlong (Int64.repr n)) *)
(* Goal: @eq Int64.int (Int64.repr n) (Ptrofs.to_int64 (Ptrofs.repr n)) *)
  apply make_longconst_correct.
- (* temp var *)
  constructor; auto.
- (* addrof *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl in TR. auto.
- (* unop *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_unop_correct; eauto.
- (* binop *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_binop_correct; eauto.
- (* cast *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_cast_correct; eauto.
- (* sizeof *)
  rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct.
- (* alignof *)
  rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct.
- (* rvalue out of lvalue *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]].
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_load_correct; eauto.
- (* var local *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit (me_local _ _ MENV); eauto. intros EQ.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor. eapply eval_var_addr_local. eauto.
- (* var global *)
(* Goal: eval_expr ge e le m (make_longconst n) (Vlong n) *)
  econstructor. eapply eval_var_addr_global.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_env_globals; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite symbols_preserved. auto.
- (* deref *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl in TR. eauto.
- (* field struct *)
  unfold make_field_access in EQ0. rewrite H1 in EQ0.
  destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; monadInv EQ0.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B].
  rewrite <- B in EQ1.
  assert (x0 = delta) by (unfold ge in *; simpl in *; congruence).
  subst x0.
(* Goal: eval_expr ge e le m (if Archi.ptr64 then a else Eunop Ointoflong a) (if Archi.ptr64 then Vlong (Ptrofs.to_int64 (Ptrofs.of_int64 i)) else Vint (Ptrofs.to_int (Ptrofs.of_int64 i))) *)
  destruct Archi.ptr64 eqn:SF.
+ eapply eval_Ebinop; eauto using make_longconst_correct.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs.
+ eapply eval_Ebinop; eauto using make_intconst_correct.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs.
- (* field union *)
  unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  auto.
Qed.

Lemma transl_expr_correct:
   forall a v,
   Clight.eval_expr ge e le m a v ->
   forall ta, transl_expr cunit.(prog_comp_env) a = OK ta ->
   Csharpminor.eval_expr tge te le m ta v.
Proof (proj1 transl_expr_lvalue_correct).

Lemma transl_lvalue_correct:
   forall a b ofs,
   Clight.eval_lvalue ge e le m a b ofs ->
   forall ta, transl_lvalue cunit.(prog_comp_env) a = OK ta ->
   Csharpminor.eval_expr tge te le m ta (Vptr b ofs).
Proof (proj2 transl_expr_lvalue_correct).

Lemma transl_arglist_correct:
  forall al tyl vl,
  Clight.eval_exprlist ge e le m al tyl vl ->
  forall tal, transl_arglist cunit.(prog_comp_env) al tyl = OK tal ->
  Csharpminor.eval_exprlist tge te le m tal vl.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  induction 1; intros.
(* Goal: eval_exprlist tge te le m tal (@nil val) *)
(* Goal: eval_exprlist tge te le m tal (@cons val v2 vl) *)
  monadInv H. constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  monadInv H2. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. auto.
Qed.

Lemma typlist_of_arglist_eq:
  forall al tyl vl,
  Clight.eval_exprlist ge e le m al tyl vl ->
  typlist_of_arglist al tyl = typlist_of_typelist tyl.
Proof.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  induction 1; simpl.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  f_equal; auto.
Qed.

End EXPR.

(** ** Semantic preservation for statements *)

(** The simulation diagram for the translation of statements and functions
  is a "plus" diagram of the form
<<
           I
     S1 ------- R1
     |          |
   t |        + | t
     v          v
     S2 ------- R2
           I                         I
>>

The invariant [I] is the [match_states] predicate that we now define.
*)

Inductive match_transl: stmt -> cont -> stmt -> cont -> Prop :=
  | match_transl_0: forall ts tk,
      match_transl ts tk ts tk
  | match_transl_1: forall ts tk,
      match_transl (Sblock ts) tk ts (Kblock tk).

Lemma match_transl_step:
  forall ts tk ts' tk' f te le m,
  match_transl (Sblock ts) tk ts' tk' ->
  star step tge (State f ts' tk' te le m) E0 (State f ts (Kblock tk) te le m).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. inv H.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply star_one. constructor.
(* Goal: @star genv state step tge (State f ts' (Kblock tk) te le m) E0 (State f ts' (Kblock tk) te le m) *)
  apply star_refl.
Qed.

Inductive match_cont: composite_env -> type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> Prop :=
  | match_Kstop: forall ce tyret nbrk ncnt,
      match_cont tyret ce nbrk ncnt Clight.Kstop Kstop
  | match_Kseq: forall ce tyret nbrk ncnt s k ts tk,
      transl_statement ce tyret nbrk ncnt s = OK ts ->
      match_cont ce tyret nbrk ncnt k tk ->
      match_cont ce tyret nbrk ncnt
                 (Clight.Kseq s k)
                 (Kseq ts tk)
  | match_Kloop1: forall ce tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
      transl_statement ce tyret 1%nat 0%nat s1 = OK ts1 ->
      transl_statement ce tyret 0%nat (S ncnt) s2 = OK ts2 ->
      match_cont ce tyret nbrk ncnt k tk ->
      match_cont ce tyret 1%nat 0%nat
                 (Clight.Kloop1 s1 s2 k)
                 (Kblock (Kseq ts2 (Kseq (Sloop (Sseq (Sblock ts1) ts2)) (Kblock tk))))
  | match_Kloop2: forall ce tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
      transl_statement ce tyret 1%nat 0%nat s1 = OK ts1 ->
      transl_statement ce tyret 0%nat (S ncnt) s2 = OK ts2 ->
      match_cont ce tyret nbrk ncnt k tk ->
      match_cont ce tyret 0%nat (S ncnt)
                 (Clight.Kloop2 s1 s2 k)
                 (Kseq (Sloop (Sseq (Sblock ts1) ts2)) (Kblock tk))
  | match_Kswitch: forall ce tyret nbrk ncnt k tk,
      match_cont ce tyret nbrk ncnt k tk ->
      match_cont ce tyret 0%nat (S ncnt)
                 (Clight.Kswitch k)
                 (Kblock tk)
  | match_Kcall: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id tf te le tk cu,
      linkorder cu prog ->
      transl_function cu.(prog_comp_env) f = OK tf ->
      match_env e te ->
      match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk ->
      match_cont ce tyret nbrk ncnt
                 (Clight.Kcall id f e le k)
                 (Kcall id tf te le tk).

Inductive match_states: Clight.state -> Csharpminor.state -> Prop :=
  | match_state:
      forall f nbrk ncnt s k e le m tf ts tk te ts' tk' cu
          (LINK: linkorder cu prog)
          (TRF: transl_function cu.(prog_comp_env) f = OK tf)
          (TR: transl_statement cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt s = OK ts)
          (MTR: match_transl ts tk ts' tk')
          (MENV: match_env e te)
          (MK: match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt k tk),
      match_states (Clight.State f s k e le m)
                   (State tf ts' tk' te le m)
  | match_callstate:
      forall fd args k m tfd tk targs tres cconv cu ce
          (LINK: linkorder cu prog)
          (TR: match_fundef cu fd tfd)
          (MK: match_cont ce Tvoid 0%nat 0%nat k tk)
          (ISCC: Clight.is_call_cont k)
          (TY: type_of_fundef fd = Tfunction targs tres cconv),
      match_states (Clight.Callstate fd args k m)
                   (Callstate tfd args tk m)
  | match_returnstate:
      forall res k m tk ce
          (MK: match_cont ce Tvoid 0%nat 0%nat k tk),
      match_states (Clight.Returnstate res k m)
                   (Returnstate res tk m).

Remark match_states_skip:
  forall f e le te nbrk ncnt k tf tk m cu,
  linkorder cu prog ->
  transl_function cu.(prog_comp_env) f = OK tf ->
  match_env e te ->
  match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt k tk ->
  match_states (Clight.State f Clight.Sskip k e le m) (State tf Sskip tk te le m).
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. econstructor; eauto. simpl; reflexivity. constructor.
Qed.

(** Commutation between label resolution and compilation *)

Section FIND_LABEL.
Variable ce: composite_env.
Variable lbl: label.
Variable tyret: type.

Lemma transl_find_label:
  forall s nbrk ncnt k ts tk
  (TR: transl_statement ce tyret nbrk ncnt s = OK ts)
  (MC: match_cont ce tyret nbrk ncnt k tk),
  match Clight.find_label lbl s k with
  | None => find_label lbl ts tk = None
  | Some (s', k') =>
      exists ts', exists tk', exists nbrk', exists ncnt',
      find_label lbl ts tk = Some (ts', tk')
      /\ transl_statement ce tyret nbrk' ncnt' s' = OK ts'
      /\ match_cont ce tyret nbrk' ncnt' k' tk'
  end

with transl_find_label_ls:
  forall ls nbrk ncnt k tls tk
  (TR: transl_lbl_stmt ce tyret nbrk ncnt ls = OK tls)
  (MC: match_cont ce tyret nbrk ncnt k tk),
  match Clight.find_label_ls lbl ls k with
  | None => find_label_ls lbl tls tk = None
  | Some (s', k') =>
      exists ts', exists tk', exists nbrk', exists ncnt',
      find_label_ls lbl tls tk = Some (ts', tk')
      /\ transl_statement ce tyret nbrk' ncnt' s' = OK ts'
      /\ match_cont ce tyret nbrk' ncnt' k' tk'
  end.

Proof.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
* intro s; case s; intros; try (monadInv TR); simpl.
- (* skip *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  auto.
- (* assign *)
  unfold make_store, make_memcpy in EQ3.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  destruct (access_mode (typeof e)); monadInv EQ3; auto.
- (* set *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  auto.
- (* call *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto.
- (* builtin *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  auto.
- (* seq *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit (transl_find_label s0 nbrk ncnt (Clight.Kseq s1 k)); eauto. constructor; eauto.
  destruct (Clight.find_label lbl s0 (Clight.Kseq s1 k)) as [[s' k'] | ].
  intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]].
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  intro. rewrite H. eapply transl_find_label; eauto.
- (* ifthenelse *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit (transl_find_label s0); eauto.
  destruct (Clight.find_label lbl s0 k) as [[s' k'] | ].
  intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]].
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  intro. rewrite H. eapply transl_find_label; eauto.
- (* loop *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit (transl_find_label s0 1%nat 0%nat (Kloop1 s0 s1 k)); eauto. econstructor; eauto.
  destruct (Clight.find_label lbl s0 (Kloop1 s0 s1 k)) as [[s' k'] | ].
  intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]].
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
  intro. rewrite H.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_find_label; eauto. econstructor; eauto.
- (* break *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  auto.
- (* continue *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  auto.
- (* return *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl in TR. destruct o; monadInv TR. auto. auto.
- (* switch *)
  assert (exists b, ts = Sblock (Sswitch b x x0)).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  { destruct (classify_switch (typeof e)); inv EQ2; econstructor; eauto. }
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  destruct H as [b EQ3]; rewrite EQ3; simpl.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_find_label_ls with (k := Clight.Kswitch k); eauto. econstructor; eauto.
- (* label *)
  destruct (ident_eq lbl l).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exists x; exists tk; exists nbrk; exists ncnt; auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_find_label; eauto.
- (* goto *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  auto.

(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
* intro ls; case ls; intros; monadInv TR; simpl.
- (* nil *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  auto.
- (* cons *)
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit (transl_find_label s nbrk ncnt (Clight.Kseq (seq_of_labeled_statement l) k)); eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. apply transl_lbl_stmt_2; eauto.
  destruct (Clight.find_label lbl s (Clight.Kseq (seq_of_labeled_statement l) k)) as [[s' k'] | ].
  intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]].
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
  intro. rewrite H.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_find_label_ls; eauto.
Qed.

End FIND_LABEL.

(** Properties of call continuations *)

Lemma match_cont_call_cont:
  forall ce' tyret' nbrk' ncnt' ce tyret nbrk ncnt k tk,
  match_cont ce tyret nbrk ncnt k tk ->
  match_cont ce' tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk).
Proof.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  induction 1; simpl; auto.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto.
Qed.

Lemma match_cont_is_call_cont:
  forall ce tyret nbrk ncnt k tk ce' tyret' nbrk' ncnt',
  match_cont ce tyret nbrk ncnt k tk ->
  Clight.is_call_cont k ->
  match_cont ce' tyret' nbrk' ncnt' k tk /\ is_call_cont tk.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. inv H; simpl in H0; try contradiction; simpl.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  split; auto; constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  split; auto; econstructor; eauto.
Qed.

(** The simulation proof *)

Lemma transl_step:
  forall S1 t S2, Clight.step2 ge S1 t S2 ->
  forall T1, match_states S1 T1 ->
  exists T2, plus step tge T1 t T2 /\ match_states S2 T2.
Proof.
  induction 1; intros T1 MST; inv MST.

- (* assign *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR.
  assert (SAME: ts' = ts /\ tk' = tk).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  { inversion MTR. auto.
    subst ts. unfold make_store, make_memcpy in EQ3.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    destruct (access_mode (typeof a1)); monadInv EQ3; auto. }
  destruct SAME; subst ts' tk'.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply plus_one. eapply make_store_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_lvalue_correct; eauto. eapply make_cast_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_expr_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_states_skip; eauto.

- (* set *)
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  monadInv TR. inv MTR. econstructor; split.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply plus_one. econstructor. eapply transl_expr_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_states_skip; eauto.

- (* call *)
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence.
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  intros targs tres cc CF TR. monadInv TR. inv MTR.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK').
  rewrite H in CF. simpl in CF. inv CF.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply plus_one. econstructor; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_expr_correct with (cunit := cu); eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_arglist_correct with (cunit := cu); eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  erewrite typlist_of_arglist_eq by eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_fundef_sig1; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  rewrite H3. auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl. auto.

- (* builtin *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: eval_expr ge e le m (make_longconst n) (Vlong n) *)
  apply plus_one. econstructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply transl_arglist_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply external_call_symbols_preserved with (ge1 := ge). apply senv_preserved. eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_states_skip; eauto.

- (* seq *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply plus_one. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto.

- (* skip seq *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR. inv MK.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
  apply plus_one. apply step_skip_seq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. constructor.

- (* continue seq *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR. inv MK.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply plus_one. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. simpl. reflexivity. constructor.

- (* break seq *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR. inv MK.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply plus_one. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. simpl. reflexivity. constructor.

- (* ifthenelse *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit make_boolean_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit transl_expr_correct; eauto.
  intros [v [A B]].
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply plus_one. apply step_ifthenelse with (v := v) (b := b); auto.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  destruct b; econstructor; eauto; constructor.

- (* loop *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply star_plus_trans. eapply match_transl_step; eauto.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  eapply plus_left. constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  eapply star_left. constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply star_one. constructor.
(* Goal: @eq Z (Z.sub (Z.div (two_power_nat (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Zpos (xO xH))) (Zpos xH)) Int.max_signed *)
  reflexivity. reflexivity. traceEq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. constructor. econstructor; eauto.

- (* skip-or-continue loop *)
  assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  { destruct H; subst x; monadInv TR; inv MTR; auto. }
(* Goal: final_state (Returnstate (Vint r) tk m) r *)
  destruct H0. inv MK.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
  eapply plus_left.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  destruct H0; subst ts'. 2:constructor. constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply star_one. constructor. traceEq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. constructor. econstructor; eauto.

- (* break loop1 *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR. inv MK.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  eapply plus_left. constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  eapply star_left. constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  eapply star_left. constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply star_one. constructor.
(* Goal: @eq Z (Z.sub (Z.div (two_power_nat (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O))))))))))))))))))))))))))))))))) (Zpos (xO xH))) (Zpos xH)) Int.max_signed *)
  reflexivity. reflexivity. traceEq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_states_skip; eauto.

- (* skip loop2 *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR. inv MK.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply plus_one. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl. rewrite H6; simpl. rewrite H8; simpl. eauto.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  constructor.

- (* break loop2 *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR. inv MK.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  eapply plus_left. constructor.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply star_one. constructor.
  traceEq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_states_skip; eauto.

- (* return none *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply plus_one. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_env_free_blocks; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_returnstate with (ce := prog_comp_env cu); eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_cont_call_cont. eauto.

- (* return some *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply plus_one. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_env_free_blocks; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_returnstate with (ce := prog_comp_env cu); eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_cont_call_cont. eauto.

- (* skip call *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit match_cont_is_call_cont; eauto. intros [A B].
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply plus_one. apply step_skip_call. auto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_env_free_blocks; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_returnstate with (ce := prog_comp_env cu); eauto.

- (* switch *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR.
  assert (E: exists b, ts = Sblock (Sswitch b x x0) /\ Switch.switch_argument b v n).
(* Goal: @eq Z (Int64.unsigned i) (Int.unsigned (Int64.loword i)) *)
(* Goal: @eq bool (Int.ltu (Int64.loword i) Int.iwordsize) true *)
  { unfold sem_switch_arg in H0.
    destruct (classify_switch (typeof a)); inv EQ2; econstructor; split; eauto;
    destruct v; inv H0; constructor. }
  destruct E as (b & A & B). subst ts.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit transl_expr_correct; eauto. intro EV.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply star_plus_trans. eapply match_transl_step; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply plus_one. econstructor; eauto. traceEq.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply transl_lbl_stmt_2. apply transl_lbl_stmt_1. eauto.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor. eauto.

- (* skip or break switch *)
  assert ((ts' = Sskip \/ ts' = Sexit nbrk) /\ tk' = tk).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
    destruct H; subst x; monadInv TR; inv MTR; auto.
(* Goal: final_state (Returnstate (Vint r) tk m) r *)
  destruct H0. inv MK.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply plus_one. destruct H0; subst ts'. 2:constructor. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_states_skip; eauto.

- (* continue switch *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR. inv MK.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply plus_one. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. simpl. reflexivity. constructor.

- (* label *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply plus_one. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. constructor.

- (* goto *)
(* Goal: @ex expr (fun tb : expr => and (@eq (res expr) (transl_lvalue ce (Efield a0 i ty)) (@OK expr tb)) (@eq (res expr) (make_load tb (typeof (Efield a0 i ty))) (@OK expr ta))) *)
  monadInv TR. inv MTR.
  generalize TRF. unfold transl_function. intro TRF'. monadInv TRF'.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit (transl_find_label (prog_comp_env cu) lbl). eexact EQ. eapply match_cont_call_cont. eauto.
  rewrite H.
  intros [ts' [tk'' [nbrk' [ncnt' [A [B C]]]]]].
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  apply plus_one. constructor. simpl. eexact A.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. constructor.

- (* internal function *)
(* Goal: final_state R r *)
  inv H. inv TR. monadInv H5.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit match_cont_is_call_cont; eauto. intros [A B].
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit match_env_alloc_variables; eauto.
  apply match_env_empty.
  intros [te1 [C D]].
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
  apply plus_one. eapply step_internal_function.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl. erewrite transl_vars_names by eauto. assumption.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  simpl. assumption.
(* Goal: @eq temp_env (@PTree.set val (@fst ident type (@pair ident type id ty)) Vundef (create_undef_temps (@map (prod ident type) ident (@fst ident type) temps))) (@PTree.set val id Vundef (Clight.create_undef_temps temps)) *)
  simpl. assumption.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl. rewrite create_undef_temps_match. eapply bind_parameter_temps_match; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl. econstructor; eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  constructor.

- (* external function *)
  inv TR.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit match_cont_is_call_cont; eauto. intros [A B].
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  apply plus_one. constructor. eauto.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply match_returnstate with (ce := ce); eauto.

- (* returnstate *)
(* Goal: final_state (Returnstate (Vint r) tk m) r *)
  inv MK.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: final_state (Returnstate (Vint r) Kstop m) r *)
  apply plus_one. constructor.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. simpl; reflexivity. constructor.
Qed.

Lemma transl_initial_states:
  forall S, Clight.initial_state prog S ->
  exists R, initial_state tprog R /\ match_states S R.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. inv H.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  exploit function_ptr_translated; eauto. intros (cu & tf & A & B & C).
  assert (D: Genv.find_symbol tge (AST.prog_main tprog) = Some b).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  { destruct TRANSL as (P & Q & R). rewrite Q. rewrite symbols_preserved. auto. }
  assert (E: funsig tf = signature_of_type Tnil type_int32s cc_default).
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  { eapply transl_fundef_sig2; eauto. }
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  econstructor; split.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  econstructor; eauto. apply (Genv.init_mem_match TRANSL). eauto.
  econstructor; eauto. instantiate (1 := prog_comp_env cu). constructor; auto. exact I.
Qed.

Lemma transl_final_states:
  forall S R r,
  match_states S R -> Clight.final_state S r -> final_state R r.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  intros. inv H0. inv H. inv MK. constructor.
Qed.

Theorem transl_program_correct:
  forward_simulation (Clight.semantics2 prog) (Csharpminor.semantics tprog).
Proof.
  eapply forward_simulation_plus.
  apply senv_preserved.
  eexact transl_initial_states.
  eexact transl_final_states.
  eexact transl_step.
Qed.

End CORRECTNESS.

(** ** Commutation with linking *)

Instance TransfCshmgenLink : TransfLink match_prog.
Proof.
(* Goal: forall (S : Clight.state) (R : state) (r : Int.int) (_ : match_states S R) (_ : Clight.final_state S r), final_state R r *)
  red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2).
  generalize H.
Local Transparent Ctypes.Linker_program.
  simpl; unfold link_program.
  destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate.
  destruct (lift_option (link (prog_types p1) (prog_types p2))) as [[typs EQ]|P]; 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).
  intros E.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  eapply Linking.link_match_program; eauto.
- intros.
Local Transparent Linker_fundef Linking.Linker_fundef.
  inv H3; inv H4; simpl in H2.
+ discriminate.
+ destruct ef; inv H2. econstructor; split. simpl; eauto. left; constructor; auto.
+ destruct ef; inv H2. econstructor; split. simpl; eauto. right; constructor; auto.
+ destruct (external_function_eq ef ef0 && typelist_eq args args0 &&
         type_eq res res0 && calling_convention_eq cc cc0) eqn:E'; inv H2.
(* Goal: and (@eq (option composite) (@PTree.get composite id (@prog_comp_env Clight.function prog)) (@Some composite co)) (@eq (res Z) (field_offset (@prog_comp_env Clight.function prog) f (co_members co)) (field_offset (@prog_comp_env Clight.function cunit) f (co_members co))) *)
  InvBooleans. subst ef0. econstructor; split.
(* Goal: @eq (list typ) (@nil typ) (@nil typ) *)
(* Goal: @eq (list typ) (@cons typ (typ_of_type ty) (typlist_of_arglist bl tyl)) (@cons typ (typ_of_type ty) (typlist_of_typelist tyl)) *)
  simpl; rewrite dec_eq_true; eauto.
(* Goal: forall _ : @eq (option (prod block Z)) (@None (prod block Z)) (@Some (prod block Z) (@pair block Z b sz)), @ex type (fun ty : type => @eq (option (prod block type)) (@PTree.get (prod block type) id (PTree.empty (prod block type))) (@Some (prod block type) (@pair block type b ty))) *)
  left; constructor. congruence.
- intros. exists tt. auto.
- replace (program_of_program p) with pp. auto. inv E; destruct pp; auto.
Qed.
