Cshmgenproof.v

(* *********************************************************************)
(*                                                                     *)
(*              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 Ctyping 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.
  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.
  intros. inv H.
- monadInv H1. simpl. inversion H0.
  unfold signature_of_function, signature_of_type.
  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.
  intros. eapply transl_fundef_sig1; eauto.
  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.
  intros. destruct H.
  unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
  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.
  intros. destruct H.
  unfold alignof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
  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.
  intros. destruct H.
  unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
  split.
- symmetry. apply Ctypes.sizeof_stable; auto.
- revert C. induction t; simpl; auto;
  destruct (prog_comp_env cunit)!i as [co|] eqn:X; try discriminate; erewrite H1 by eauto; auto.
Qed.

Lemma union_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 /\
  union_field_offset prog.(prog_comp_env) f (co_members co) = union_field_offset cunit.(prog_comp_env) f (co_members co).
Proof.
  intros.
  assert (C: composite_consistent cunit.(prog_comp_env) co).
  { apply build_composite_env_consistent with cunit.(prog_types) id; auto.
    apply prog_comp_env_eq. }
  destruct H as [_ A].
  split. auto. apply Ctypes.union_field_offset_stable; eauto using co_consistent_complete.
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.
  intros.
  assert (C: composite_consistent cunit.(prog_comp_env) co).
  { apply build_composite_env_consistent with cunit.(prog_types) id; auto.
    apply prog_comp_env_eq. }
  destruct H as [_ A].
  split. auto. apply Ctypes.field_offset_stable; eauto using co_consistent_complete.
Qed.

(** * Properties of the translation functions *)

(** 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.
  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)).
  {
    induction sl; simpl; intros.
    inv H; auto.
    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).
  {
    induction sl; simpl; intros.
    inv H; auto.
    monadInv H; simpl. destruct o. destruct (zeq z n).
    econstructor; split; eauto. simpl; rewrite EQ; simpl; rewrite EQ1; auto.
    apply IHsl; auto.
    apply IHsl; auto.
  }
  intros. specialize (CASE _ _ H). unfold Clight.select_switch, select_switch.
  destruct (Clight.select_switch_case n sl) as [sl'|].
  destruct CASE as [tsl' [P Q]]. rewrite P, Q. auto.
  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.
  induction sl; intros.
  monadInv H. auto.
  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.
  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.
  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.
  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.
  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.
  intros. unfold Vptrofs, make_ptrofsconst. destruct Archi.ptr64 eqn:SF.
- replace (Ptrofs.to_int64 (Ptrofs.repr n)) with (Int64.repr n).
  apply make_longconst_correct.
  symmetry; auto with ptrofs.
- replace (Ptrofs.to_int (Ptrofs.repr n)) with (Int.repr n).
  apply make_intconst_correct.
  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.
  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.
  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.
  intros. unfold make_floatofint, cast_int_float.
  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.
  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))).
  { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
    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)).
  { intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2.
    rewrite Int.eq_false. auto. apply Int.one_not_zero.
    rewrite Int.eq_true. auto. }
  destruct a; simpl; auto. destruct b; auto.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
  simpl in H6. inv H6. eauto.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
  simpl in H6. inv H6. eauto.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
  simpl in H6. inv H6. eauto.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
  simpl in H6. inv H6. eauto.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
  simpl in H6. unfold Val.cmpl in H6.
  destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity.
- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
  simpl in H6. unfold Val.cmplu in H6.
  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.
  intros.
  assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) Vone).
  { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
    unfold Mem.weak_valid_pointer in H1. rewrite H0, H1.
    rewrite Int.eq_true; auto. }
  assert (OF_OPTBOOL: forall ob, Some (Val.of_optbool ob) <> Some (Vptr b i)).
  { intros. destruct ob as [[]|]; discriminate. }
  assert (OF_BOOL: forall ob, option_map Val.of_bool ob <> Some (Vptr b i)).
  { intros. destruct ob as [[]|]; discriminate. }
  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.
  intros. unfold make_cast_int, cast_int_int.
  destruct sz.
  destruct si; eauto with cshm.
  destruct si; eauto with cshm.
  auto.
  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.
  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.
  intros. unfold make_cast, sem_cast in *;
  destruct (classify_cast ty1 ty2); inv H; destruct v; InvEval; eauto with cshm.
- (* single -> int *)
  unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm.
- (* float -> int *)
  apply make_cast_int_correct.
  unfold cast_float_int in Heqo. unfold make_intoffloat.
  destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto.
- (* single -> int *)
  apply make_cast_int_correct.
  unfold cast_single_int in Heqo. unfold make_intofsingle.
  destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto.
- (* long -> float *)
  unfold make_floatoflong, cast_long_float. destruct si1; eauto with cshm.
- (* long -> single *)
  unfold make_singleoflong, cast_long_single. destruct si1; eauto with cshm.
- (* float -> long *)
  unfold cast_float_long in Heqo. unfold make_longoffloat.
  destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto.
- (* single -> long *)
  unfold cast_single_long in Heqo. unfold make_longofsingle.
  destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto.
- (* int -> bool *)
  apply make_cmpu_ne_zero_correct; auto.
- (* pointer (32 bits) -> bool *)
  eapply make_cmpu_ne_zero_correct_ptr; eauto.
- (* long -> bool *)
  econstructor; eauto with cshm.
  simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu.
  destruct (Int64.eq i Int64.zero); auto.
- (* pointer (64 bits) -> bool *)
  econstructor; eauto with cshm.
  simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in Heqb1.
  rewrite Heqb0, Heqb1. rewrite Int64.eq_true. reflexivity.
- (* float -> bool *)
  econstructor; eauto with cshm.
  simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq.
  destruct (Float.cmp Ceq f Float.zero); auto.
- (* single -> bool *)
  econstructor; eauto with cshm.
  simpl. unfold Val.cmpfs, Val.cmpfs_bool. rewrite Float32.cmp_ne_eq.
  destruct (Float32.cmp Ceq f Float32.zero); auto.
- (* struct *)
  destruct (ident_eq id1 id2); inv H1; auto.
- (* union *)
  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.
  intros. unfold make_boolean. unfold bool_val in H0.
  destruct (classify_bool ty); destruct v; InvEval.
- (* int *)
  econstructor; split. apply make_cmpu_ne_zero_correct with (n := i); auto.
  destruct (Int.eq i Int.zero); simpl; constructor.
- (* ptr 32 bits *)
  exists Vone; split. eapply make_cmpu_ne_zero_correct_ptr; eauto. constructor.
- (* long *)
  econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmplu. simpl. eauto.
  destruct (Int64.eq i Int64.zero); simpl; constructor.
- (* ptr 64 bits *)
  exists Vone; split.
  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool.
  unfold Mem.weak_valid_pointer in Heqb0. rewrite Heqb0, Heqb1, Int64.eq_true. reflexivity.
  constructor.
- (* float *)
  econstructor; split. econstructor; eauto with cshm. simpl. eauto.
  unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq.
  destruct (Float.cmp Cne f Float.zero); constructor.
- (* single *)
  econstructor; split. econstructor; eauto with cshm. simpl. eauto.
  unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq.
  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;
  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;
  destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
  unfold make_floatoflong, cast_long_float. destruct s.
  econstructor. econstructor; simpl; eauto. simpl; eauto. simpl; eauto.
  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.
  unfold sem_notbool, bool_val, make_notbool; intros until m; intros SEM MAKE EV1.
  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.
  destruct (Int.eq i Int.zero); auto.
- destruct Archi.ptr64 eqn:SF; inv SEM.
  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0.
  econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
  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.
  destruct (Int64.eq i Int64.zero); auto.
- destruct Archi.ptr64 eqn:SF; inv SEM.
  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0.
  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool.
  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.
  destruct (Float.cmp Ceq f Float.zero); auto.
- econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool.
  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;
  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.
  exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'.
  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.
  rewrite iop_ok; auto. rewrite iopu_ok; auto.
- destruct s; inv H0; econstructor; eauto with cshm.
  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.
  exploit make_cast_correct. eexact EQ. eauto. eauto. intros EV1'.
  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.
  rewrite iop_ok; auto. rewrite iopu_ok; auto.
- destruct s; inv H0; econstructor; eauto with cshm.
  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).
  { unfold make_add_ptr_int, sem_add_ptr_int; intros until v; intros MAKE EV1 EV2 SEM; monadInv MAKE.
    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.
    simpl. rewrite SF. f_equal. f_equal. f_equal.
    assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)).
    { destruct si; simpl; apply Ptrofs.agree64_repr; auto. }
    auto with ptrofs.
  - destruct va; InvEval; destruct vb; inv SEM.
  + eauto with cshm.
  + econstructor; eauto with cshm.
    simpl. rewrite SF. f_equal. f_equal. f_equal.
    assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs).
    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).
  { unfold make_add_ptr_long, sem_add_ptr_long; intros until v; intros MAKE EV1 EV2 SEM; monadInv MAKE.
    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.
    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.
    simpl. rewrite SF. f_equal. f_equal. f_equal.
    assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto).
    auto with ptrofs.
  }
  red; unfold make_add, sem_add;
  intros until m; intros SEM MAKE EV1 EV2;
  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.
  econstructor; eauto with cshm.
  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
  assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)).
  { destruct si; simpl; apply Ptrofs.agree64_repr; auto. }
  auto with ptrofs.
+ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
  econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
  assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs).
  auto with ptrofs.
- rewrite (transl_sizeof _ _ _ _ LINK EQ) in EQ0. clear EQ.
  set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *.
  destruct va; InvEval; destruct vb; InvEval.
  destruct (eq_block b0 b1); try discriminate.
  destruct (zlt 0 sz); try discriminate.
  destruct (zle sz Ptrofs.max_signed); simpl in SEM; inv SEM.
  assert (E1: Ptrofs.signed (Ptrofs.repr sz) = sz).
  { apply Ptrofs.signed_repr. generalize Ptrofs.min_signed_neg; lia. }
  destruct Archi.ptr64 eqn:SF; inversion EQ0; clear EQ0; subst c.
+ assert (E: Int64.signed (Int64.repr sz) = sz).
  { apply Int64.signed_repr.
    replace Int64.max_signed with Ptrofs.max_signed.
    generalize Int64.min_signed_neg; lia.
    unfold Ptrofs.max_signed, Ptrofs.half_modulus; rewrite Ptrofs.modulus_eq64 by auto. reflexivity. }
  econstructor; eauto with cshm.
  rewrite SF, dec_eq_true. simpl.
  predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.zero.
  rewrite H in E; rewrite Int64.signed_zero in E; extlia.
  predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.mone.
  rewrite H0 in E; rewrite Int64.signed_mone in E; extlia.
  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal.
  apply f_equal. symmetry. auto with ptrofs.
+ assert (E: Int.signed (Int.repr sz) = sz).
  { apply Int.signed_repr.
    replace Int.max_signed with Ptrofs.max_signed.
    generalize Int.min_signed_neg; lia.
    unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity.
  }
  econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl.
  predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero.
  rewrite H in E; rewrite Int.signed_zero in E; extlia.
  predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone.
  rewrite H0 in E; rewrite Int.signed_mone in E; extlia.
  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. apply f_equal. apply f_equal.
  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.
  econstructor; eauto with cshm.
  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
  auto with ptrofs.
+ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
  econstructor; eauto with cshm. simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal.
  assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto).
  auto with ptrofs.
- eapply make_binarith_correct; eauto; intros; auto.
Qed.

Lemma make_mul_correct: binary_constructor_correct make_mul sem_mul.
Proof.
  apply make_binarith_correct; intros; auto.
Qed.

Lemma make_div_correct: binary_constructor_correct make_div sem_div.
Proof.
  apply make_binarith_correct; intros; auto.
Qed.

Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod.
Proof.
  apply make_binarith_int_correct; intros; auto.
Qed.

Lemma make_and_correct: binary_constructor_correct make_and sem_and.
Proof.
  apply make_binarith_int_correct; intros; auto.
Qed.

Lemma make_or_correct: binary_constructor_correct make_or sem_or.
Proof.
  apply make_binarith_int_correct; intros; auto.
Qed.

Lemma make_xor_correct: binary_constructor_correct make_xor sem_xor.
Proof.
  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.
  intros. apply Int64.ltu_inv in H. comput (Int64.unsigned Int64.iwordsize).
  assert (Int64.unsigned i = Int.unsigned (Int64.loword i)).
  {
    unfold Int64.loword. rewrite Int.unsigned_repr; auto.
    comput Int.max_unsigned; lia.
  }
  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.
  intros. apply Int64.ltu_inv in H. comput (Int64.unsigned (Int64.repr 32)).
  assert (Int64.unsigned i = Int.unsigned (Int64.loword i)).
  {
    unfold Int64.loword. rewrite Int.unsigned_repr; auto.
    comput Int.max_unsigned; lia.
  }
  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.
  intros. apply Int.ltu_inv in H. comput (Int.unsigned Int64.iwordsize').
  apply Int64.unsigned_repr. comput Int64.max_unsigned; lia.
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.
  econstructor; eauto. simpl; rewrite E; auto.
- destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM.
  exploit small_shift_amount_1; eauto. intros [A B].
  econstructor; eauto with cshm. simpl. rewrite A.
  f_equal; f_equal. unfold Int64.shl', Int64.shl. rewrite B; auto.
- destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM.
  econstructor; eauto with cshm. simpl. rewrite small_shift_amount_2; auto.
- destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM.
  econstructor; eauto with cshm. simpl. rewrite E.
  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.
  destruct s; inv H0; econstructor; eauto; simpl; rewrite E; auto.
- destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM.
  exploit small_shift_amount_1; eauto. intros [A B].
  destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite A;
  f_equal; f_equal.
  unfold Int64.shr', Int64.shr; rewrite B; auto.
  unfold Int64.shru', Int64.shru; rewrite B; auto.
- destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM.
  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.
  destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite E.
  unfold Int64.shr', Int64.shr; rewrite small_shift_amount_3; auto.
  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.
  unfold cmp_ptr, make_cmp_ptr; intros.
  destruct Archi.ptr64.
- econstructor; eauto.
- econstructor; eauto. simpl. unfold Val.cmpu.
  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.
  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)).
  eauto with cshm.
  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)).
  eauto with cshm.
  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.
  symmetry. auto with ptrofs.
+ replace (Ptrofs.to_int (Ptrofs.of_intu i)) with i. auto.
  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.
  intros. unfold Vptrofs. destruct Archi.ptr64 eqn:SF.
- replace (Ptrofs.to_int64 (Ptrofs.of_int64 i)) with i. auto.
  symmetry. auto with ptrofs.
- econstructor; eauto. simpl. apply f_equal. apply f_equal.
  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.
  intros. destruct op; simpl in *.
  eapply make_notbool_correct; eauto.
  eapply make_notint_correct; eauto.
  eapply make_neg_correct; eauto.
  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.
  intros. destruct op; simpl in *.
  eapply make_add_correct; eauto.
  eapply make_sub_correct; eauto.
  eapply make_mul_correct; eauto.
  eapply make_div_correct; eauto.
  eapply make_mod_correct; eauto.
  eapply make_and_correct; eauto.
  eapply make_or_correct; eauto.
  eapply make_xor_correct; eauto.
  eapply make_shl_correct; eauto.
  eapply make_shr_correct; eauto.
  eapply make_cmp_correct; eauto.
  eapply make_cmp_correct; eauto.
  eapply make_cmp_correct; eauto.
  eapply make_cmp_correct; eauto.
  eapply make_cmp_correct; eauto.
  eapply make_cmp_correct; eauto.
Qed.

Remark int_ltu_true:
  forall x, 0 <= x < Int.zwordsize -> Int.ltu (Int.repr x) Int.iwordsize = true.
Proof.
  intros. unfold Int.ltu. rewrite Int.unsigned_repr_wordsize, Int.unsigned_repr, zlt_true by (generalize Int.wordsize_max_unsigned; lia).
  auto.
Qed.

Remark first_bit_range: forall sz pos width,
  0 <= pos -> 0 < width -> pos + width <= bitsize_carrier sz ->
     0 <= first_bit sz pos width < Int.zwordsize
  /\ 0 <= Int.zwordsize - first_bit sz pos width - width < Int.zwordsize.
Proof.
  intros.
  assert (bitsize_carrier sz <= Int.zwordsize) by (destruct sz; compute; congruence).
  unfold first_bit; destruct Archi.big_endian; lia.
Qed.

Lemma make_load_correct:
  forall addr ty bf code b ofs v e le m,
  make_load addr ty bf = OK code ->
  eval_expr ge e le m addr (Vptr b ofs) ->
  deref_loc ty m b ofs bf v ->
  eval_expr ge e le m code v.
Proof.
  unfold make_load; intros until m; intros MKLOAD EVEXP DEREF.
  inv DEREF.
- (* scalar *)
  rewrite H in MKLOAD. inv MKLOAD. apply eval_Eload with (Vptr b ofs); auto.
- (* by reference *)
  rewrite H in MKLOAD. inv MKLOAD. auto.
- (* by copy *)
  rewrite H in MKLOAD. inv MKLOAD. auto.
- (* by bitfield *)
  inv H.
  unfold make_extract_bitfield in MKLOAD. unfold bitfield_extract.
  exploit (first_bit_range sz pos width); eauto. lia. intros [A1 A2].
  set (amount1 := Int.repr (Int.zwordsize - first_bit sz pos width - width)) in MKLOAD.
  set (amount2 := Int.repr (Int.zwordsize - width)) in MKLOAD.
  destruct (zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz)); inv MKLOAD.
  set (e1 := Eload (chunk_for_carrier sz) addr).
  assert (E1: eval_expr ge e le m e1 (Vint c)) by (econstructor; eauto).
  set (e2 := Ebinop Oshl e1 (make_intconst amount1)).
  assert (E2: eval_expr ge e le m e2 (Vint (Int.shl c amount1))).
  { econstructor; eauto using make_intconst_correct. cbn.
    unfold amount1 at 1; rewrite int_ltu_true by lia. auto. } 
  econstructor; eauto using make_intconst_correct.
  destruct (Ctypes.intsize_eq sz IBool || Ctypes.signedness_eq sg Unsigned); cbn.
  + unfold amount2 at 1; rewrite int_ltu_true by lia. 
    rewrite Int.unsigned_bitfield_extract_by_shifts by lia. auto.
  + unfold amount2 at 1; rewrite int_ltu_true by lia. 
    rewrite Int.signed_bitfield_extract_by_shifts by lia. auto.
Qed.

Lemma make_store_bitfield_correct: 
  forall f sz sg pos width 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 (Bits sz sg pos width) v m' ->
  make_store_bitfield sz sg pos width dst src = OK s ->
  step ge (State f s k e le m) E0 (State f Sskip k e le m').
Proof.
  intros until s; intros DST SRC ASG MK.
  inv ASG. inv H5. unfold make_store_bitfield in MK.
  destruct (zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz)); inv MK.
  econstructor; eauto.
  exploit (first_bit_range sz pos width); eauto. lia. intros [A1 A2].
  rewrite Int.bitfield_insert_alternative by lia.
  set (amount := first_bit sz pos width).
  set (mask := Int.shl (Int.repr (two_p width - 1)) (Int.repr amount)).
  repeat econstructor; eauto. cbn. rewrite int_ltu_true by lia. 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 Full 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.
  intros. inv H1; try congruence.
  monadInv H3.
  exploit transl_alignof_blockcopy. eexact LINK. eauto. intros [A B]. rewrite A, B.
  change le with (set_optvar None Vundef le) at 2.
  econstructor.
  econstructor. eauto. econstructor. eauto. constructor.
  econstructor; eauto.
  apply alignof_blockcopy_1248.
  apply sizeof_pos.
  apply sizeof_alignof_blockcopy_compat.
Qed.

Lemma make_store_correct:
  forall addr ty bf rhs code e le m b ofs v m' f k,
  make_store cunit.(prog_comp_env) addr ty bf 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 bf v m' ->
  step ge (State f code k e le m) E0 (State f Sskip k e le m').
Proof.
  unfold make_store. intros until k; intros MKSTORE EV1 EV2 ASSIGN.
  inversion ASSIGN; subst.
- (* nonvolatile scalar *)
  rewrite H in MKSTORE; inv MKSTORE.
  econstructor; eauto.
- (* by copy *)
  rewrite H in MKSTORE.
  eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto.
- (* bitfield *)
  eapply make_store_bitfield_correct; eauto.
Qed.

Lemma make_normalization_correct:
  forall e le m a v t,
  eval_expr ge e le m a v ->
  wt_val v t ->
  eval_expr ge e le m (make_normalization t a) v.
Proof.
  intros. destruct t; simpl; auto. inv H0.
- destruct i; simpl in H3.
  + destruct s; econstructor; eauto; simpl; congruence.
  + destruct s; econstructor; eauto; simpl; congruence.
  + auto.
  + econstructor; eauto; simpl; congruence.
- auto.
- destruct i.
  + destruct s; econstructor; eauto. 
  + destruct s; econstructor; eauto.
  + auto.
  + econstructor; 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 :=
  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.
  intros. destruct (te!id) as [[b sz] | ] eqn:?; auto.
  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.
  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)).
  apply PTree.elements_canonical_order.
  intros id [b ty] GET. exists (b, Ctypes.sizeof ge ty); split. eapply me_local; eauto. red; auto.
  intros id [b sz] GET. exploit me_local_inv; eauto. intros [ty EQ].
  exploit me_local; eauto. intros EQ1.
  exists (b, ty); split. auto. red; split; congruence.

  unfold blocks_of_env, Clight.blocks_of_env.
  generalize H0. induction 1. auto.
  simpl. f_equal; auto.
  unfold block_of_binding, Clight.block_of_binding.
  destruct a1 as [id1 [blk1 ty1]]. destruct b1 as [id2 [blk2 sz2]].
  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.
  intros. rewrite (match_env_same_blocks _ _ H). auto.
Qed.

Lemma match_env_empty:
  match_env Clight.empty_env Csharpminor.empty_env.
Proof.
  unfold Clight.empty_env, Csharpminor.empty_env.
  constructor.
  intros until ty. repeat rewrite PTree.gempty. congruence.
  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.
  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)).
  auto.
  constructor.
    (* me_local *)
    intros until ty0. repeat rewrite PTree.gsspec.
    destruct (peq id0 id); intros. congruence. eapply me_local; eauto.
    (* me_local_inv *)
    intros until sz. repeat rewrite PTree.gsspec.
    destruct (peq id0 id); intros. exists ty; congruence. eapply me_local_inv; eauto.
  intros [te2 [ALLOC MENV]].
  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.
  induction temps; simpl. auto.
  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.
  induction vars; simpl; intros.
  destruct vals; inv H. auto.
  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.
  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:
  forall a loc ofs bf ta,
  Clight.eval_lvalue ge e le m a loc ofs bf ->
  transl_expr cunit.(prog_comp_env) a = OK ta ->
  exists tb, transl_lvalue cunit.(prog_comp_env) a = OK (tb, bf)
          /\ make_load tb (typeof a) bf = OK ta.
Proof.
  intros until ta; intros EVAL TR. inv EVAL; simpl in TR.
- (* var local *)
  exists (Eaddrof id); auto.
- (* var global *)
  exists (Eaddrof id); auto.
- (* deref *)
  monadInv TR. cbn; rewrite EQ. exists x; auto.
- (* field struct *)
  monadInv TR.
  assert (x1 = bf).
  { rewrite H0 in EQ1. unfold make_field_access in EQ1.
    destruct ((prog_comp_env cunit)!id) as [co'|] eqn:E; try discriminate.
    monadInv EQ1.
    exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B].
    simpl in H1, H2. congruence. }
  subst x1.
  exists x0; split; auto. simpl; rewrite EQ; auto.
- (* field union *)
  monadInv TR.
  assert (x1 = bf).
  { rewrite H0 in EQ1. unfold make_field_access in EQ1.
    destruct ((prog_comp_env cunit)!id) as [co'|] eqn:E; try discriminate.
    monadInv EQ1.
    exploit union_field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B].
    simpl in H1, H2. congruence. }
  subst x1.
  exists x0; split; auto. simpl; rewrite EQ; auto.
Qed.

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 bf,
   Clight.eval_lvalue ge e le m a b ofs bf ->
   forall ta bf' (TR: transl_lvalue cunit.(prog_comp_env) a = OK (ta, bf')),
   bf = bf' /\ Csharpminor.eval_expr tge te le m ta (Vptr b ofs)).
Proof.
  apply eval_expr_lvalue_ind; intros; try (monadInv TR).
- (* const int *)
  apply make_intconst_correct.
- (* const float *)
  apply make_floatconst_correct.
- (* const single *)
  apply make_singleconst_correct.
- (* const long *)
  apply make_longconst_correct.
- (* temp var *)
  constructor; auto.
- (* addrof *)
  destruct x0; inv EQ0. apply H0 in EQ. destruct EQ. auto.
- (* unop *)
  eapply transl_unop_correct; eauto.
- (* binop *)
  eapply transl_binop_correct; eauto.
- (* cast *)
  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 *)
  exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]].
  apply H0 in TRLVAL; destruct TRLVAL. 
  eapply make_load_correct; eauto.
- (* var local *)
  exploit (me_local _ _ MENV); eauto. intros EQ.
  split; auto. econstructor. eapply eval_var_addr_local. eauto.
- (* var global *)
  split; auto. econstructor. eapply eval_var_addr_global.
  eapply match_env_globals; eauto.
  rewrite symbols_preserved. auto.
- (* deref *)
  eauto.
- (* field struct *)
  unfold make_field_access in EQ0. rewrite H1 in EQ0.
  destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; try discriminate; monadInv EQ0.
  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).
  assert (bf' = bf) by (unfold ge in *; simpl in *; congruence).
  subst x0 bf'. split; auto.
  destruct Archi.ptr64 eqn:SF.
+ eapply eval_Ebinop; eauto using make_longconst_correct.
  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs.
+ eapply eval_Ebinop; eauto using make_intconst_correct.
  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.
  destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; try discriminate; monadInv EQ0.
  exploit union_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).
  assert (bf' = bf) by (unfold ge in *; simpl in *; congruence).
  subst x0 bf'. split; auto.
  destruct Archi.ptr64 eqn:SF.
+ eapply eval_Ebinop; eauto using make_longconst_correct.
  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs.
+ eapply eval_Ebinop; eauto using make_intconst_correct.
  simpl. rewrite SF. apply f_equal. apply f_equal. apply f_equal. auto with ptrofs.
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 bf,
   Clight.eval_lvalue ge e le m a b ofs bf ->
   forall ta bf', transl_lvalue cunit.(prog_comp_env) a = OK (ta, bf') ->
   bf = bf' /\ 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.
  induction 1; intros.
  monadInv H. constructor.
  monadInv H2. constructor.
  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.
  induction 1; simpl.
  auto.
  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.
  intros. inv H.
  apply star_one. constructor.
  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)
  | match_Kcall_normalize: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id a 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 ->
      (forall v e le m, wt_val v tyret -> le!id = Some v -> eval_expr tge e le m a v) ->
      match_cont ce tyret nbrk ncnt
                 (Clight.Kcall (Some id) f e le k)
                 (Kcall (Some id) tf te le (Kseq (Sset id a) 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 tres 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 tres k m tk ce
          (MK: match_cont ce tres 0%nat 0%nat k tk)
          (WT: wt_val res tres),
      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.
  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.
* intro s; case s; intros; try (monadInv TR); simpl.
- (* skip *)
  auto.
- (* assign *)
  unfold make_store, make_memcpy in EQ3.
  destruct x0.
  destruct (access_mode (typeof e)); monadInv EQ3; auto.
  unfold make_store_bitfield in EQ3.
  destruct (zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz));
  monadInv EQ3; auto.
- (* set *)
  auto.
- (* call *)
  simpl in TR. destruct (classify_fun (typeof e)); monadInv TR.
  unfold make_funcall.
  destruct o; auto; destruct Conventions1.return_value_needs_normalization; auto.
- (* tailcall *)
  simpl in TR. destruct (classify_fun (typeof e)); monadInv TR.
  auto.
- (* builtin *)
  auto.
- (* seq *)
  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]]]]]].
  rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
  intro. rewrite H. eapply transl_find_label; eauto.
- (* ifthenelse *)
  exploit (transl_find_label s0); eauto.
  destruct (Clight.find_label lbl s0 k) as [[s' k'] | ].
  intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]].
  rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
  intro. rewrite H. eapply transl_find_label; eauto.
- (* loop *)
  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]]]]]].
  rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
  intro. rewrite H.
  eapply transl_find_label; eauto. econstructor; eauto.
- (* break *)
  auto.
- (* continue *)
  auto.
- (* return *)
  simpl in TR. destruct o; monadInv TR. auto. auto.
- (* switch *)
  assert (exists b, ts = Sblock (Sswitch b x x0)).
  { destruct (classify_switch (typeof e)); inv EQ2; econstructor; eauto. }
  destruct H as [b EQ3]; rewrite EQ3; simpl.
  eapply transl_find_label_ls with (k := Clight.Kswitch k); eauto. econstructor; eauto.
- (* label *)
  destruct (ident_eq lbl l).
  exists x; exists tk; exists nbrk; exists ncnt; auto.
  eapply transl_find_label; eauto.
- (* goto *)
  auto.

* intro ls; case ls; intros; monadInv TR; simpl.
- (* nil *)
  auto.
- (* cons *)
  exploit (transl_find_label s nbrk ncnt (Clight.Kseq (seq_of_labeled_statement l) k)); eauto.
  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]]]]]].
  rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
  intro. rewrite H.
  eapply transl_find_label_ls; eauto.
Qed.

End FIND_LABEL.

(** Properties of call continuations *)

Lemma match_cont_call_cont:
  forall ce' 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.
  induction 1; simpl; auto.
- apply match_Kstop.
- eapply match_Kcall; eauto.
- eapply match_Kcall_normalize; eauto.
Qed.

Lemma match_cont_is_call_cont:
  forall ce tyret nbrk ncnt k tk ce' 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.
  intros. inv H; simpl in H0; try contradiction; simpl.
  split; auto; apply match_Kstop.
  split; auto; eapply match_Kcall; eauto.
  split; auto; eapply match_Kcall_normalize; eauto.
Qed.

Lemma call_cont_is_call_cont:
  forall k, Clight.is_call_cont (Clight.call_cont k).
Proof.
  induction k; simpl; auto.
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 *)
  monadInv TR.
  assert (SAME: ts' = ts /\ tk' = tk).
  { inversion MTR. auto.
    subst ts. unfold make_store, make_memcpy in EQ3.
    destruct x0.
    destruct (access_mode (typeof a1)); monadInv EQ3; auto.
    unfold make_store_bitfield in EQ3.
    destruct (zle 0 pos && zlt 0 width && zle (pos + width) (bitsize_carrier sz));
    monadInv EQ3; auto.
  }
  destruct SAME; subst ts' tk'.
  exploit transl_lvalue_correct; eauto. intros [A B]; subst x0.
  econstructor; split.
  apply plus_one. eapply make_store_correct; eauto.
  eapply make_cast_correct; eauto.
  eapply transl_expr_correct; eauto.
  eapply match_states_skip; eauto.

- (* set *)
  monadInv TR. inv MTR. econstructor; split.
  apply plus_one. econstructor. eapply transl_expr_correct; eauto.
  eapply match_states_skip; eauto.

- (* call *)
  revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence.
  intros targs tres cc CF TR. monadInv TR.
  exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK').
  rewrite H in CF. simpl in CF. inv CF.
  set (sg := {| sig_args := typlist_of_arglist al targs;
                sig_res := rettype_of_type tres;
                sig_cc := cc |}) in *.
  assert (SIG: funsig tfd = sg).
  { unfold sg; erewrite typlist_of_arglist_eq by eauto.
    eapply transl_fundef_sig1; eauto. rewrite H3; auto. }
  assert (EITHER: tk' = tk /\ ts' = Scall optid sg x x0
               \/ exists id, optid = Some id /\
                  tk' = tk /\ ts' = Sseq (Scall optid sg x x0)
                                         (Sset id (make_normalization tres (Evar id)))).
  { unfold make_funcall in MTR.
    destruct optid. destruct Conventions1.return_value_needs_normalization.
    inv MTR. right; exists i; auto.
    inv MTR; auto.
    inv MTR; auto. }
  destruct EITHER as [(EK & ES) | (id & EI & EK & ES)]; rewrite EK, ES.
  + (* without normalization of return value *)
    econstructor; split.
    apply plus_one. eapply step_call; eauto.
    eapply transl_expr_correct with (cunit := cu); eauto.
    eapply transl_arglist_correct with (cunit := cu); eauto.
    econstructor; eauto.
    eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto.
    exact I.
  + (* with normalization of return value *)
    subst optid.
    econstructor; split.
    eapply plus_two. apply step_seq. eapply step_call; eauto. 
    eapply transl_expr_correct with (cunit := cu); eauto.
    eapply transl_arglist_correct with (cunit := cu); eauto.
    traceEq.
    econstructor; eauto.
    eapply match_Kcall_normalize  with (ce := prog_comp_env cu') (cu := cu); eauto.
    intros. eapply make_normalization_correct; eauto. constructor; eauto.
    exact I.

- (* tailcall *)
  revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence.
  intros targs tres cc CF TR. monadInv TR. inv MTR.
  exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK').
  rewrite H in CF. simpl in CF. inv CF.
  set (sg := {| sig_args := typlist_of_arglist al targs;
                sig_res := rettype_of_type (fn_return f);
                sig_cc := cc |}) in *.
  assert (SIG: funsig tfd = sg).
  { unfold sg; erewrite typlist_of_arglist_eq by eauto.
    eapply transl_fundef_sig1; eauto. rewrite H3; auto. }
  econstructor; split.
  apply plus_one. eapply step_tailcall; eauto.
  eapply transl_expr_correct with (cunit := cu); eauto.
  eapply transl_arglist_correct with (cunit := cu); eauto.
  eapply match_env_free_blocks; eauto.
  eapply match_callstate with (ce := prog_comp_env cu); eauto.
  eapply match_cont_call_cont. eauto.
  apply call_cont_is_call_cont.

- (* builtin *)
  monadInv TR. inv MTR.
  econstructor; split.
  apply plus_one. econstructor.
  eapply transl_arglist_correct; eauto.
  eapply external_call_symbols_preserved with (ge1 := ge). apply senv_preserved. eauto.
  eapply match_states_skip; eauto.

- (* seq *)
  monadInv TR. inv MTR.
  econstructor; split.
  apply plus_one. constructor.
  econstructor; eauto. constructor.
  econstructor; eauto.

- (* skip seq *)
  monadInv TR. inv MTR. inv MK.
  econstructor; split.
  apply plus_one. apply step_skip_seq.
  econstructor; eauto. constructor.

- (* continue seq *)
  monadInv TR. inv MTR. inv MK.
  econstructor; split.
  apply plus_one. constructor.
  econstructor; eauto. simpl. reflexivity. constructor.

- (* break seq *)
  monadInv TR. inv MTR. inv MK.
  econstructor; split.
  apply plus_one. constructor.
  econstructor; eauto. simpl. reflexivity. constructor.

- (* ifthenelse *)
  monadInv TR. inv MTR.
  exploit make_boolean_correct; eauto.
  exploit transl_expr_correct; eauto.
  intros [v [A B]].
  econstructor; split.
  apply plus_one. apply step_ifthenelse with (v := v) (b := b); auto.
  destruct b; econstructor; eauto; constructor.

- (* loop *)
  monadInv TR.
  econstructor; split.
  eapply star_plus_trans. eapply match_transl_step; eauto.
  eapply plus_left. constructor.
  eapply star_left. constructor.
  apply star_one. constructor.
  reflexivity. reflexivity. traceEq.
  econstructor; eauto. constructor. econstructor; eauto.

- (* skip-or-continue loop *)
  assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk).
  { destruct H; subst x; monadInv TR; inv MTR; auto. }
  destruct H0. inv MK.
  econstructor; split.
  eapply plus_left.
  destruct H0; subst ts'. 2:constructor. constructor.
  apply star_one. constructor. traceEq.
  econstructor; eauto. constructor. econstructor; eauto.

- (* break loop1 *)
  monadInv TR. inv MTR. inv MK.
  econstructor; split.
  eapply plus_left. constructor.
  eapply star_left. constructor.
  eapply star_left. constructor.
  apply star_one. constructor.
  reflexivity. reflexivity. traceEq.
  eapply match_states_skip; eauto.

- (* skip loop2 *)
  monadInv TR. inv MTR. inv MK.
  econstructor; split.
  apply plus_one. constructor.
  econstructor; eauto.
  simpl. rewrite H6; simpl. rewrite H8; simpl. eauto.
  constructor.

- (* break loop2 *)
  monadInv TR. inv MTR. inv MK.
  econstructor; split.
  eapply plus_left. constructor.
  apply star_one. constructor.
  traceEq.
  eapply match_states_skip; eauto.

- (* return none *)
  monadInv TR. inv MTR.
  econstructor; split.
  apply plus_one. constructor.
  eapply match_env_free_blocks; eauto.
  eapply match_returnstate with (ce := prog_comp_env cu); eauto.
  eapply match_cont_call_cont. eauto.
  constructor.

- (* return some *)
  monadInv TR. inv MTR.
  econstructor; split.
  apply plus_one. constructor.
  eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto.
  eapply match_env_free_blocks; eauto.
  eapply match_returnstate with (ce := prog_comp_env cu); eauto.
  eapply match_cont_call_cont. eauto.
  apply wt_val_casted. eapply cast_val_is_casted; eauto.

- (* skip call *)
  monadInv TR. inv MTR.
  exploit match_cont_is_call_cont; eauto. intros [A B].
  econstructor; split.
  apply plus_one. apply step_skip_call. auto.
  eapply match_env_free_blocks; eauto.
  eapply match_returnstate with (ce := prog_comp_env cu); eauto.
  constructor.

- (* switch *)
  monadInv TR.
  assert (E: exists b, ts = Sblock (Sswitch b x x0) /\ Switch.switch_argument b v n).
  { 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.
  exploit transl_expr_correct; eauto. intro EV.
  econstructor; split.
  eapply star_plus_trans. eapply match_transl_step; eauto.
  apply plus_one. econstructor; eauto. traceEq.
  econstructor; eauto.
  apply transl_lbl_stmt_2. apply transl_lbl_stmt_1. eauto.
  constructor.
  econstructor. eauto.

- (* skip or break switch *)
  assert ((ts' = Sskip \/ ts' = Sexit nbrk) /\ tk' = tk).
    destruct H; subst x; monadInv TR; inv MTR; auto.
  destruct H0. inv MK.
  econstructor; split.
  apply plus_one. destruct H0; subst ts'. 2:constructor. constructor.
  eapply match_states_skip; eauto.

- (* continue switch *)
  monadInv TR. inv MTR. inv MK.
  econstructor; split.
  apply plus_one. constructor.
  econstructor; eauto. simpl. reflexivity. constructor.

- (* label *)
  monadInv TR. inv MTR.
  econstructor; split.
  apply plus_one. constructor.
  econstructor; eauto. constructor.

- (* goto *)
  monadInv TR. inv MTR.
  generalize TRF. unfold transl_function. intro TRF'. monadInv TRF'.
  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]]]]]].
  econstructor; split.
  apply plus_one. constructor. simpl. eexact A.
  econstructor; eauto. constructor.

- (* internal function *)
  inv H. inv TR. monadInv H5.
  exploit match_cont_is_call_cont; eauto. intros [A B].
  exploit match_env_alloc_variables; eauto.
  apply match_env_empty.
  intros [te1 [C D]].
  econstructor; split.
  apply plus_one. eapply step_internal_function.
  simpl. erewrite transl_vars_names by eauto. assumption.
  simpl. assumption.
  simpl. assumption.
  simpl; eauto.
  simpl. rewrite create_undef_temps_match. eapply bind_parameter_temps_match; eauto.
  simpl. econstructor; eauto.
  unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto.
  constructor.
  replace (fn_return f) with tres. eassumption.
  simpl in TY. unfold type_of_function in TY. congruence. 

- (* external function *)
  inv TR.
  exploit match_cont_is_call_cont; eauto. intros [A B].
  econstructor; split.
  apply plus_one. constructor.
  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
  eapply match_returnstate with (ce := ce); eauto.
  apply has_rettype_wt_val. 
  replace (rettype_of_type tres0) with (sig_res (ef_sig ef)).
  eapply external_call_well_typed_gen; eauto.
  rewrite H5. simpl. simpl in TY. congruence.

- (* returnstate *)
  inv MK.
  + (* without normalization *)
    econstructor; split.
    apply plus_one. constructor.
    econstructor; eauto. simpl; reflexivity. constructor.
  + (* with normalization *)
    econstructor; split.
    eapply plus_three. econstructor. econstructor. constructor.
    simpl. apply H13. eauto. apply PTree.gss.
    traceEq.
    simpl. rewrite PTree.set2. 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.
  intros. inv H.
  exploit function_ptr_translated; eauto. intros (cu & tf & A & B & C).
  assert (D: Genv.find_symbol tge (AST.prog_main tprog) = Some b).
  { destruct TRANSL as (P & Q & R). rewrite Q. rewrite symbols_preserved. auto. }
  assert (E: funsig tf = signature_of_type Tnil type_int32s cc_default).
  { eapply transl_fundef_sig2; eauto. }
  econstructor; split.
  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.
  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 *)

Global Instance TransfCshmgenLink : TransfLink match_prog.
Proof.
  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.
  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.
  InvBooleans. subst ef0. econstructor; split.
  simpl; rewrite dec_eq_true; eauto.
  left; constructor. congruence.
- intros. exists tt. auto.
- replace (program_of_program p) with pp. auto. inv E; destruct pp; auto.
Qed.