Require Import VST.msl.msl_standard.
Require Import VST.veric.Clight_base.
Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.Clight_lemmas.
Require Import VST.veric.mpred.
Require Import VST.veric.tycontext.
Require Import VST.veric.expr2.
Require Import VST.veric.Clight_Cop2.
Require Import VST.veric.juicy_mem.
Require Import VST.veric.binop_lemmas2.

Lemma denote_tc_nonzero_e:
 forall i m, app_pred (denote_tc_nonzero (Vint i)) m -> i <> Int.zero.
Proof.
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
simpl; auto .
Qed.

Lemma denote_tc_nodivover_e:
 forall i j m, app_pred (denote_tc_nodivover (Vint i) (Vint j)) m ->
   ~ (i =Int.repr Int.min_signed /\ j = Int.mone).
Proof.
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
simpl; auto.
Qed.

Lemma denote_tc_nonzero_e64:
 forall i m, app_pred (denote_tc_nonzero (Vlong i)) m -> i <> Int64.zero.
Proof.
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
simpl; auto.
Qed.

Lemma denote_tc_nodivover_e64_ll:
 forall i j m, app_pred (denote_tc_nodivover (Vlong i) (Vlong j)) m ->
   ~ (i =Int64.repr Int64.min_signed /\ j = Int64.mone).
Proof.
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
simpl; auto.
Qed.

Lemma denote_tc_nodivover_e64_il:
  (* This is a rather vacuous lemma, since the premise is simply True *)
 forall s i j m, app_pred (denote_tc_nodivover (Vint i) (Vlong j)) m ->
   ~ (cast_int_long s i = Int64.repr Int64.min_signed /\ j = Int64.mone).
Proof.
(* Goal: forall (s : signedness) (i : Int64.int) (j : Int.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vint j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int (cast_int_long s j) Int64.mone)) *)
simpl; intros.
(* Goal: not (and (@eq Int64.int (cast_int_long s i) (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
intros [? ?].
(* Goal: False *)
subst.
(* Goal: @eq Int.int j Int.mone *)
destruct s; simpl in *.
*
(* Goal: @eq Int.int j Int.mone *)
pose proof (@f_equal _ _ Int64.signed _ _ H0).
(* Goal: False *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite Int64.signed_repr in H1.
(* Goal: False *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite Int64.signed_repr in H1.
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
pose proof (Int.signed_range i).
(* Goal: False *)
(* Goal: and (Z.le Z0 (Z.add Int64.modulus Int64.min_signed)) (Z.le (Z.add Int64.modulus Int64.min_signed) Int64.max_unsigned) *)
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
rewrite H1 in H2.
(* Goal: False *)
(* Goal: and (Z.le Z0 (Z.add Int64.modulus Int64.min_signed)) (Z.le (Z.add Int64.modulus Int64.min_signed) Int64.max_unsigned) *)
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
destruct H2.
(* Goal: False *)
(* Goal: and (Z.le Z0 (Z.add Int64.modulus Int64.min_signed)) (Z.le (Z.add Int64.modulus Int64.min_signed) Int64.max_unsigned) *)
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
compute in H2. apply H2; auto.
(* Goal: and (Z.le Z0 (Z.add Int64.modulus Int64.min_signed)) (Z.le (Z.add Int64.modulus Int64.min_signed) Int64.max_unsigned) *)
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
compute; split; congruence.
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
pose proof (Int.signed_range i).
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
clear - H2. forget (Int.signed i) as a.
(* Goal: False *)
(* Goal: and (Z.le Z0 (Z.add Int64.modulus Int64.min_signed)) (Z.le (Z.add Int64.modulus Int64.min_signed) Int64.max_unsigned) *)
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
destruct H2.
(* Goal: and (Z.le Int64.min_signed (Int.signed j)) (Z.le (Int.signed j) Int64.max_signed) *)
split; eapply Z.le_trans; try eassumption.
(* Goal: Z.le Int.modulus (Z.sub Int64.modulus (Zpos xH)) *)
compute; congruence.
(* Goal: Z.le Int.modulus (Z.sub Int64.modulus (Zpos xH)) *)
compute; congruence.
*
(* Goal: False *)
pose proof (@f_equal _ _ Int64.unsigned _ _ H0).
(* Goal: False *)
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
rewrite Int64.unsigned_repr in H1.
replace (Int64.repr Int64.min_signed) 
  with (Int64.repr (Int64.modulus + Int64.min_signed)) in H1.
(* Goal: False *)
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
rewrite Int64.unsigned_repr in H1.
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
pose proof (Int.unsigned_range i).
(* Goal: False *)
(* Goal: and (Z.le Z0 (Z.add Int64.modulus Int64.min_signed)) (Z.le (Z.add Int64.modulus Int64.min_signed) Int64.max_unsigned) *)
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
rewrite H1 in H2.
(* Goal: False *)
(* Goal: and (Z.le Z0 (Z.add Int64.modulus Int64.min_signed)) (Z.le (Z.add Int64.modulus Int64.min_signed) Int64.max_unsigned) *)
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
destruct H2.
(* Goal: False *)
(* Goal: and (Z.le Z0 (Z.add Int64.modulus Int64.min_signed)) (Z.le (Z.add Int64.modulus Int64.min_signed) Int64.max_unsigned) *)
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
compute in H2. apply H2; auto.
(* Goal: and (Z.le Z0 (Z.add Int64.modulus Int64.min_signed)) (Z.le (Z.add Int64.modulus Int64.min_signed) Int64.max_unsigned) *)
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
compute; split; congruence.
(* Goal: @eq Int64.int (Int64.repr (Z.add Int64.modulus Int64.min_signed)) (Int64.repr Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
apply Int64.eqm_samerepr.
(* Goal: Int64.eqm (Z.add Int64.modulus Int64.min_signed) Int64.min_signed *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
rewrite <- Z.add_0_l.
(* Goal: Int64.eqm (Z.add Int64.modulus Int64.min_signed) (Z.add Z0 Int64.min_signed) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
apply Int64.eqm_add.
(* Goal: Int64.eqm Int64.modulus Z0 *)
(* Goal: Int64.eqm Int64.min_signed Int64.min_signed *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
unfold Int64.eqm.
(* Goal: Int64.eqmod Int64.modulus Int64.modulus Z0 *)
(* Goal: Int64.eqm Int64.min_signed Int64.min_signed *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
exists 1. reflexivity.
(* Goal: Int64.eqm Int64.min_signed Int64.min_signed *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
apply Int64.eqm_refl.
(* Goal: and (Z.le (Z.opp (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH)))) Z0) (Z.le Z0 (Z.sub (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH))) (Zpos xH))) *)
clear.
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
pose proof (Int.unsigned_range i).
(* Goal: and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int.int j Int.mone) *)
destruct H; split; auto.
(* Goal: Z.le (Int.unsigned i) Int64.max_unsigned *)
assert (Int.modulus < Int64.max_unsigned).
(* Goal: Z.lt Int.modulus Int64.max_unsigned *)
(* Goal: Z.le (Int.unsigned i) Int64.max_unsigned *)
compute; auto.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))) Z0) (Z.le Z0 (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))) *)
omega.
Qed.

Lemma denote_tc_nodivover_e64_li:
 forall s i j m, app_pred (denote_tc_nodivover (Vlong i) (Vint j)) m ->
   ~ (i = Int64.repr Int64.min_signed /\ cast_int_long s j = Int64.mone).
Proof.
(* Goal: forall (s : signedness) (i : Int64.int) (j : Int.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vint j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int (cast_int_long s j) Int64.mone)) *)
simpl; intros.
(* Goal: not (@eq Int64.int (Int64.repr (Int.signed i)) Int64.zero) *)
contradict H.
(* Goal: and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int.int j Int.mone) *)
destruct H; split; auto.
(* Goal: @eq Int.int j Int.mone *)
clear - H0.
(* Goal: @eq Int.int j Int.mone *)
destruct s; simpl in *.
*
(* Goal: @eq Int.int j Int.mone *)
unfold Int64.mone in H0.
(* Goal: @eq Int.int j Int.mone *)
pose proof (@f_equal _ _ Int64.signed _ _ H0).
(* Goal: @eq Int.int j Int.mone *)
clear H0.
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite Int64.signed_repr in H.
(* Goal: @eq Int.int j Int.mone *)
(* Goal: and (Z.le Int64.min_signed (Int.signed j)) (Z.le (Int.signed j) Int64.max_signed) *)
change (Int.signed j = -1) in H.
(* Goal: @eq Int.int j Int.mone *)
(* Goal: and (Z.le Int64.min_signed (Int.signed j)) (Z.le (Int.signed j) Int64.max_signed) *)
rewrite <- (Int.repr_signed j).
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
rewrite H. reflexivity.
(* Goal: and (Z.le Int64.min_signed (Int.signed j)) (Z.le (Int.signed j) Int64.max_signed) *)
clear H.
(* Goal: and (Z.le Int64.min_signed (Int.signed j)) (Z.le (Int.signed j) Int64.max_signed) *)
pose proof (Int.signed_range j).
(* Goal: and (Z.le Int64.min_signed (Int.signed j)) (Z.le (Int.signed j) Int64.max_signed) *)
destruct H.
(* Goal: and (Z.le Int64.min_signed (Int.signed j)) (Z.le (Int.signed j) Int64.max_signed) *)
split; eapply Z.le_trans; try eassumption.
(* Goal: Z.lt Int.modulus Int64.max_signed *)
(* Goal: Z.le (Int.unsigned j) Int64.max_signed *)
compute. congruence. compute. congruence.
*
(* Goal: @eq Int.int j Int.mone *)
unfold Int64.mone in H0.
(* Goal: @eq Int.int j Int.mone *)
pose proof (@f_equal _ _ Int64.signed _ _ H0).
(* Goal: @eq Int.int j Int.mone *)
clear H0.
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite Int64.signed_repr in H.
(* Goal: @eq Int.int j Int.mone *)
(* Goal: and (Z.le Int64.min_signed (Int.unsigned j)) (Z.le (Int.unsigned j) Int64.max_signed) *)
change (Int.unsigned j = -1) in H.
(* Goal: and (Z.le Int64.min_signed (Int.unsigned j)) (Z.le (Int.unsigned j) Int64.max_signed) *)
pose proof (Int.unsigned_range j).
(* Goal: @eq Int.int j Int.mone *)
(* Goal: and (Z.le Int64.min_signed (Int.unsigned j)) (Z.le (Int.unsigned j) Int64.max_signed) *)
rewrite H in H0.
(* Goal: forall _ : @eq Datatypes.comparison Lt Gt, False *)
(* Goal: Z.le (Int.unsigned j) Int64.max_signed *)
destruct H0. compute in H0. congruence.
(* Goal: and (Z.le Int64.min_signed (Int.unsigned j)) (Z.le (Int.unsigned j) Int64.max_signed) *)
pose proof (Int.unsigned_range j).
(* Goal: and (Z.le Int64.min_signed (Int.unsigned j)) (Z.le (Int.unsigned j) Int64.max_signed) *)
destruct H0.
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
split.
(* Goal: Z.le Int64.min_signed (Int.unsigned j) *)
(* Goal: Z.le (Int.unsigned j) Int64.max_signed *)
eapply Z.le_trans; try eassumption.
(* Goal: Z.lt Int.modulus Int64.max_signed *)
(* Goal: Z.le (Int.unsigned j) Int64.max_signed *)
compute. congruence.
(* Goal: Z.le (Int.unsigned j) Int64.max_signed *)
assert (Int.modulus < Int64.max_signed).
(* Goal: Z.lt Int.modulus Int64.max_signed *)
(* Goal: Z.le (Int.unsigned j) Int64.max_signed *)
compute. auto.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))) Z0) (Z.le Z0 (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))) *)
omega.
Qed.

Lemma Int64_eq_repr_signed32_nonzero:
  forall i, i <> Int.zero ->
             Int64.repr (Int.signed i) <> Int64.zero.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
intros.
(* Goal: not (@eq Int64.int (Int64.repr (Int.signed i)) Int64.zero) *)
contradict H.
(* Goal: not (@eq Int64.int (Int64.repr (Int.unsigned i)) Int64.zero) *)
rename H into H0.
(* Goal: @eq Int.int i Int.zero *)
unfold Int64.zero in H0.
(* Goal: @eq Int.int i Int.zero *)
assert (Int64.signed (Int64.repr (Int.signed i)) = Int64.signed (Int64.repr 0)) by (f_equal; auto).
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite Int64.signed_repr in H.
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite Int64.signed_repr in H.
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Int64.min_signed Z0) (Z.le Z0 Int64.max_signed) *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite <- (Int.repr_signed i).
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
rewrite H. reflexivity.
(* Goal: and (Z.le Int64.min_signed Z0) (Z.le Z0 Int64.max_signed) *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
pose proof (Int64.signed_range Int64.zero).
(* Goal: and (Z.le Int64.min_signed Z0) (Z.le Z0 Int64.max_signed) *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite Int64.signed_zero in H1.
(* Goal: @eq Int64.int i Int64.zero *)
auto.
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
pose proof (Int.signed_range i).
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
clear - H1.
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
destruct H1.
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
split.
(* Goal: @eq Int64.int i Int64.zero *)
apply Z.le_trans with Int.min_signed; auto.
(* Goal: Z.le Int.modulus (Z.sub Int64.modulus (Zpos xH)) *)
compute; congruence.
(* Goal: @eq Int64.int i Int64.zero *)
apply Z.le_trans with Int.max_signed; auto.
(* Goal: Z.le Int.modulus (Z.sub Int64.modulus (Zpos xH)) *)
compute; congruence.
Qed.

(*
Lemma Int64_eq_repr_signed32_nonzero:
  forall i, Int.eq i Int.zero = false ->
             Int64.eq (Int64.repr (Int.signed i)) Int64.zero = false.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
intros.
(* Goal: and (Z.le Int64.min_signed (Int.signed j)) (Z.le (Int.signed j) Int64.max_signed) *)
pose proof (Int.eq_spec i Int.zero). rewrite H in H0. clear H.
(* Goal: @eq Int64.int i Int64.zero *)
rewrite Int64.eq_false; auto.
(* Goal: not (@eq Int64.int (Int64.repr (Int.unsigned i)) Int64.zero) *)
contradict H0.
(* Goal: @eq Int.int i Int.zero *)
unfold Int64.zero in H0.
(* Goal: @eq Int.int i Int.zero *)
assert (Int64.signed (Int64.repr (Int.signed i)) = Int64.signed (Int64.repr 0)) by (f_equal; auto).
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite Int64.signed_repr in H.
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite Int64.signed_repr in H.
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Int64.min_signed Z0) (Z.le Z0 Int64.max_signed) *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite <- (Int.repr_signed i).
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
rewrite H. reflexivity.
(* Goal: and (Z.le Int64.min_signed Z0) (Z.le Z0 Int64.max_signed) *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
pose proof (Int64.signed_range Int64.zero).
(* Goal: and (Z.le Int64.min_signed Z0) (Z.le Z0 Int64.max_signed) *)
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
rewrite Int64.signed_zero in H1.
(* Goal: @eq Int64.int i Int64.zero *)
auto.
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
pose proof (Int.signed_range i).
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
clear - H1.
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
destruct H1.
(* Goal: and (Z.le Int64.min_signed (Int.signed i)) (Z.le (Int.signed i) Int64.max_signed) *)
split.
(* Goal: @eq Int64.int i Int64.zero *)
apply Z.le_trans with Int.min_signed; auto.
(* Goal: Z.le Int.modulus (Z.sub Int64.modulus (Zpos xH)) *)
compute; congruence.
(* Goal: @eq Int64.int i Int64.zero *)
apply Z.le_trans with Int.max_signed; auto.
(* Goal: Z.le Int.modulus (Z.sub Int64.modulus (Zpos xH)) *)
compute; congruence.
Qed.
*)

Lemma Int64_eq_repr_unsigned32_nonzero:
  forall i, i <> Int.zero ->
             Int64.repr (Int.unsigned i) <> Int64.zero.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
intros.
(* Goal: not (@eq Int64.int (Int64.repr (Int.unsigned i)) Int64.zero) *)
rename H into H0.
(* Goal: not (@eq Int64.int (Int64.repr (Int.unsigned i)) Int64.zero) *)
contradict H0.
(* Goal: @eq Int.int i Int.zero *)
unfold Int64.zero in H0.
(* Goal: @eq Int.int i Int.zero *)
assert (Int64.unsigned (Int64.repr (Int.unsigned i)) = Int64.unsigned (Int64.repr 0)) by (f_equal; auto).
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
rewrite Int64.unsigned_repr in H.
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
rewrite Int64.unsigned_repr in H.
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Z0 Z0) (Z.le Z0 Int64.max_unsigned) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
rewrite <- (Int.repr_unsigned i).
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
rewrite H. reflexivity.
(* Goal: Z.le Int.modulus (Z.sub Int64.modulus (Zpos xH)) *)
split; compute; congruence.
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
pose proof (Int.unsigned_range i).
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
clear - H1.
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
destruct H1.
(* Goal: @eq Int64.int i Int64.zero *)
split; auto.
(* Goal: Z.le (Int.unsigned i) Int64.max_unsigned *)
unfold Int64.max_unsigned.
(* Goal: Z.le (Int.unsigned i) (Z.sub Int64.modulus (Zpos xH)) *)
apply Z.le_trans with Int.modulus.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))) Z0) (Z.le Z0 (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))) *)
omega.
(* Goal: Z.le Int.modulus (Z.sub Int64.modulus (Zpos xH)) *)
compute; congruence.
Qed.

(*

Lemma Int64_eq_repr_unsigned32_nonzero:
  forall i, Int.eq i Int.zero = false ->
             Int64.eq (Int64.repr (Int.unsigned i)) Int64.zero = false.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
intros.
(* Goal: and (Z.le Int64.min_signed (Int.signed j)) (Z.le (Int.signed j) Int64.max_signed) *)
pose proof (Int.eq_spec i Int.zero). rewrite H in H0. clear H.
(* Goal: @eq Int64.int i Int64.zero *)
rewrite Int64.eq_false; auto.
(* Goal: not (@eq Int64.int (Int64.repr (Int.unsigned i)) Int64.zero) *)
contradict H0.
(* Goal: @eq Int.int i Int.zero *)
unfold Int64.zero in H0.
(* Goal: @eq Int.int i Int.zero *)
assert (Int64.unsigned (Int64.repr (Int.unsigned i)) = Int64.unsigned (Int64.repr 0)) by (f_equal; auto).
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
rewrite Int64.unsigned_repr in H.
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
rewrite Int64.unsigned_repr in H.
(* Goal: @eq Int.int i Int.zero *)
(* Goal: and (Z.le Z0 Z0) (Z.le Z0 Int64.max_unsigned) *)
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
rewrite <- (Int.repr_unsigned i).
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
rewrite H. reflexivity.
(* Goal: Z.le Int.modulus (Z.sub Int64.modulus (Zpos xH)) *)
split; compute; congruence.
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
pose proof (Int.unsigned_range i).
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
clear - H1.
(* Goal: and (Z.le Z0 (Int.unsigned i)) (Z.le (Int.unsigned i) Int64.max_unsigned) *)
destruct H1.
(* Goal: @eq Int64.int i Int64.zero *)
split; auto.
(* Goal: Z.le (Int.unsigned i) Int64.max_unsigned *)
unfold Int64.max_unsigned.
(* Goal: Z.le (Int.unsigned i) (Z.sub Int64.modulus (Zpos xH)) *)
apply Z.le_trans with Int.modulus.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))) Z0) (Z.le Z0 (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))) *)
omega.
(* Goal: Z.le Int.modulus (Z.sub Int64.modulus (Zpos xH)) *)
compute; congruence.
Qed.
*)

Lemma Int64_eq_repr_int_nonzero:
  forall s i, i <> Int.zero ->
    cast_int_long s i <> Int64.zero.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: not (@eq Int64.int (cast_int_long s i) Int64.zero) *)
  destruct s.
(* Goal: @eq Int64.int i Int64.zero *)
  + apply Int64_eq_repr_signed32_nonzero; auto.
(* Goal: @eq Int64.int i Int64.zero *)
  + apply Int64_eq_repr_unsigned32_nonzero; auto.
Qed.

(*
Lemma Int64_eq_repr_int_nonzero:
  forall s i, Int.eq i Int.zero = false ->
    Int64.eq (cast_int_long s i) Int64.zero = false.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: not (@eq Int64.int (cast_int_long s i) Int64.zero) *)
  destruct s.
(* Goal: @eq Int64.int i Int64.zero *)
  + apply Int64_eq_repr_signed32_nonzero; auto.
(* Goal: @eq Int64.int i Int64.zero *)
  + apply Int64_eq_repr_unsigned32_nonzero; auto.
Qed.
*)

Lemma denote_tc_igt_e:
  forall m i j, app_pred (denote_tc_igt j (Vint i)) m ->
        Int.unsigned i < Int.unsigned j.
Proof. auto. Qed.

Lemma denote_tc_lgt_e:
  forall m i j, app_pred (denote_tc_lgt j (Vlong i)) m ->
        Int64.unsigned i < Int64.unsigned j.
Proof. auto. Qed.

Lemma denote_tc_iszero_long_e:
 forall m i,
  app_pred (denote_tc_iszero (Vlong i)) m -> i = Int64.zero.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
intros.
(* Goal: @eq Int64.int i Int64.zero *)
hnf in H.
(* Goal: @eq Int64.int i Int64.zero *)
pose proof (Int64.eq_spec i Int64.zero).
(* Goal: @eq Int64.int i Int64.zero *)
destruct (Int64.eq i Int64.zero); try contradiction.
(* Goal: @eq Int64.int i Int64.zero *)
auto.
Qed.

Lemma int_type_tc_val_Vtrue:
  forall t, is_int_type t = true -> tc_val t Vtrue.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
intros.
    destruct t as [| [| | |] [|] | | | | | | |]; 
(* Goal: @eq Int64.int i Int64.zero *)
 try discriminate; hnf; auto.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))) (Int.signed Int.one)) (Z.le (Int.signed Int.one) (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))) *)
change (Int.signed Int.one) with 1.
(* Goal: and (Z.le Byte.min_signed Z0) (Z.le Z0 Byte.max_signed) *)
(* Goal: and (Z.le (Z.opp (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH)))) Z0) (Z.le Z0 (Z.sub (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH))) (Zpos xH))) *)
change Byte.min_signed with (-128).
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO xH)))))))) Z0) (Z.le Z0 Byte.max_signed) *)
(* Goal: and (Z.le (Z.opp (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH)))) Z0) (Z.le Z0 (Z.sub (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH))) (Zpos xH))) *)
change Byte.max_signed with 127.
(* Goal: and (Z.le (Z.opp (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH)))) Z0) (Z.le Z0 (Z.sub (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH))) (Zpos xH))) *)
clear. omega.
(* Goal: and (Z.le (Z.opp (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH)))) Z0) (Z.le Z0 (Z.sub (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH))) (Zpos xH))) *)
clear.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
simpl. 
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))) (Int.signed Int.one)) (Z.le (Int.signed Int.one) (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))) *)
change (Int.signed Int.one) with 1.
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))) Z0) (Z.le Z0 (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))) *)
omega.
Qed.

Lemma int_type_tc_val_Vfalse:
  forall t, is_int_type t = true -> tc_val t Vfalse.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
intros.
    destruct t as [| [| | |] [|] | | | | | | |]; 
 try discriminate; hnf; auto;
change (Int.signed Int.zero) with 0.
(* Goal: and (Z.le Byte.min_signed Z0) (Z.le Z0 Byte.max_signed) *)
(* Goal: and (Z.le (Z.opp (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH)))) Z0) (Z.le Z0 (Z.sub (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH))) (Zpos xH))) *)
change Byte.min_signed with (-128).
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO xH)))))))) Z0) (Z.le Z0 Byte.max_signed) *)
(* Goal: and (Z.le (Z.opp (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH)))) Z0) (Z.le Z0 (Z.sub (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH))) (Zpos xH))) *)
change Byte.max_signed with 127.
(* Goal: and (Z.le (Z.opp (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH)))) Z0) (Z.le Z0 (Z.sub (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH))) (Zpos xH))) *)
clear. omega.
(* Goal: and (Z.le (Z.opp (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH)))) Z0) (Z.le Z0 (Z.sub (two_p (Z.sub (Zpos (xO (xO (xO (xO xH))))) (Zpos xH))) (Zpos xH))) *)
clear. simpl. omega.
Qed.


Lemma int_type_tc_val_of_bool:
  forall t b, is_int_type t = true -> tc_val t (Val.of_bool b).
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
intros.
    destruct t as [| [| | |] [|] | | | | | | |]; 
 try discriminate; hnf; auto; clear H;
 destruct b; simpl; auto;
change (Int.signed Int.one) with 1;
change (Int.signed Int.zero) with 0;
change (Int.unsigned Int.one) with 1;
change (Int.unsigned Int.zero) with 0;
change Byte.min_signed with (-128);
change Byte.max_signed with 127;
change Byte.max_unsigned with 255;
(* Goal: and (Z.le (Zneg (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))) Z0) (Z.le Z0 (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH)))))))))))))))) *)
try omega.
Qed.

Lemma Ptrofs_to_of64_lemma:
 Archi.ptr64 = false -> 
 forall i, Ptrofs.to_int (Ptrofs.of_int64 i) = Int.repr (Int64.unsigned i).
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
intros.
(* Goal: @eq Int.int (Ptrofs.to_int (Ptrofs.of_int64 i)) (Int.repr (Int64.unsigned i)) *)
unfold Ptrofs.of_int64, Ptrofs.to_int.
(* Goal: @eq Int.int (Int.repr (Ptrofs.unsigned (Ptrofs.repr (Int64.unsigned i)))) (Int.repr (Int64.unsigned i)) *)
pose proof (Ptrofs.agree32_repr H (Int64.unsigned i)).
(* Goal: @eq Int.int (Int.repr (Ptrofs.unsigned (Ptrofs.repr (Int64.unsigned i)))) (Int.repr (Int64.unsigned i)) *)
red in H0.
(* Goal: @eq Int.int (Int.repr (Ptrofs.unsigned (Ptrofs.repr (Int64.unsigned i)))) (Int.repr (Int64.unsigned i)) *)
rewrite H0.
(* Goal: @eq Int.int (Int.repr (Int.unsigned (Int.repr (Int64.unsigned i)))) (Int.repr (Int64.unsigned i)) *)
apply Int.repr_unsigned.
Qed.


Lemma Int64repr_Intsigned_zero:
  forall i, Int64.repr (Int.signed i) = Int64.zero -> i=Int.zero.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
intros.
(* Goal: @eq Int.int i Int.zero *)
pose proof (Int.eq_spec i Int.zero).
(* Goal: @eq Int64.int i Int64.zero *)
destruct (Int.eq i Int.zero) eqn:?; auto.
(* Goal: @eq Int.int i Int.zero *)
apply Int64_eq_repr_signed32_nonzero in H0.
(* Goal: @eq Int.int i Int.zero *)
contradiction.
Qed.

Lemma Int64repr_Intunsigned_zero:
  forall i, Int64.repr (Int.unsigned i) = Int64.zero -> i=Int.zero.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
intros.
(* Goal: @eq Int.int i Int.zero *)
pose proof (Int.eq_spec i Int.zero).
(* Goal: @eq Int64.int i Int64.zero *)
destruct (Int.eq i Int.zero) eqn:?; auto.
(* Goal: @eq Int.int i Int.zero *)
apply Int64_eq_repr_unsigned32_nonzero in H0.
(* Goal: @eq Int.int i Int.zero *)
contradiction.
Qed.

Lemma eq_block_true: forall b1 b2 i1 i2 A (a b: A),
    is_true (sameblock (Vptr b1 i1) (Vptr b2 i2)) ->
    (if eq_block b1 b2 then a else b) = a.
Proof.
(* Goal: forall (b1 b2 : block) (i1 i2 : Ptrofs.int) (A : Type) (a b : A) (_ : is_true (sameblock (Vptr b1 i1) (Vptr b2 i2))), @eq A (if eq_block b1 b2 then a else b) a *)
  unfold sameblock, eq_block.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: @eq A (if peq b1 b2 then a else b) a *)
  apply is_true_e in H.
(* Goal: @eq Int64.int i Int64.zero *)
  destruct (peq b1 b2); auto.
(* Goal: @eq positive a b *)
  inv H.
Qed.

Lemma sizeof_range_true {CS: composite_env}: forall t A (a b: A) (max: Z),
    negb (Z.eqb (sizeof t) 0) = true ->
    Z.leb (sizeof t) max = true ->
    (if zlt 0 (sizeof t) && zle (sizeof t) max then a else b) = a.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (zlt Z0 (@sizeof CS t))) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (zle (@sizeof CS t) max)) then a else b) a *)
  rewrite negb_true_iff in H.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (zlt Z0 (@sizeof CS t))) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (zle (@sizeof CS t) max)) then a else b) a *)
  rewrite Z.eqb_neq in H.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (zlt Z0 (@sizeof CS t))) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (zle (@sizeof CS t) max)) then a else b) a *)
  pose proof sizeof_pos t.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (zlt Z0 (@sizeof CS t))) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (zle (@sizeof CS t) max)) then a else b) a *)
  rewrite <- Zle_is_le_bool in H0.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (zlt Z0 (@sizeof CS t))) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (zle (@sizeof CS t) max)) then a else b) a *)
  destruct (zlt 0 (sizeof t)); [| omega].
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (zle (@sizeof CS t) max)) then a else b) a *)
  destruct (zle (sizeof t) max); [| omega]. 
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
  reflexivity.
Qed.

Inductive tc_val_PM: type -> val -> Prop :=
| tc_val_PM_Tint: forall sz sg a v, is_int sz sg v -> tc_val_PM (Tint sz sg a) v
| tc_val_PM_Tlong: forall s a v, is_long v -> tc_val_PM (Tlong s a) v
| tc_val_PM_Tfloat_single: forall a v, is_single v -> tc_val_PM (Tfloat F32 a) v
| tc_val_PM_Tfloat_double: forall a v, is_float v -> tc_val_PM (Tfloat F64 a) v
| tc_val_PM_Tpointer: forall t a v, 
          (if eqb_type (Tpointer t a) int_or_ptr_type
           then is_pointer_or_integer
           else is_pointer_or_null) v -> 
          tc_val_PM (Tpointer t a) v
| tc_val_PM_Tarray: forall t n a v, is_pointer_or_null v -> tc_val_PM (Tarray t n a) v
| tc_val_PM_Tfunction: forall ts t a v, is_pointer_or_null v -> tc_val_PM (Tfunction ts t a) v
| tc_val_PM_Tstruct: forall i a v, isptr v -> tc_val_PM (Tstruct i a) v
| tc_val_PM_Tunion: forall i a v, isptr v -> tc_val_PM (Tunion i a) v.

Lemma tc_val_tc_val_PM: forall t v, tc_val t v <-> tc_val_PM t v.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  split; intros.
(* Goal: @eq Int64.int i Int64.zero *)
  + destruct t as [| | | [ | ] ? | | | | |]; try (inv H); constructor; auto.
(* Goal: @eq Int64.int i Int64.zero *)
  + inversion H; subst; auto.
Qed.

Inductive tc_val_PM': type -> val -> Prop :=
| tc_val_PM'_Tint: forall t0 sz sg a v, t0 = Tint sz sg a -> is_int sz sg v -> tc_val_PM' t0 v
| tc_val_PM'_Tlong: forall t0 s a v, stupid_typeconv t0 = Tlong s a -> is_long v -> tc_val_PM' t0 v
| tc_val_PM'_Tfloat_single: forall t0 a v, stupid_typeconv t0 = Tfloat F32 a -> is_single v -> tc_val_PM' t0 v
| tc_val_PM'_Tfloat_double: forall t0 a v, stupid_typeconv t0 = Tfloat F64 a -> is_float v -> tc_val_PM' t0 v
| tc_val_PM'_Tpointer: forall t0 t a v, 
  stupid_typeconv t0 = Tpointer t a -> 
  (if eqb_type t0 int_or_ptr_type
           then is_pointer_or_integer
           else is_pointer_or_null) v -> 
  tc_val_PM' t0 v
| tc_val_PM'_Tstruct: forall t0 i a v, stupid_typeconv t0 = Tstruct i a -> isptr v -> tc_val_PM' t0 v
| tc_val_PM'_Tunion: forall t0 i a v, stupid_typeconv t0 = Tunion i a -> isptr v -> tc_val_PM' t0 v.

Lemma tc_val_tc_val_PM': forall t v, tc_val t v <-> tc_val_PM' t v.
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  split; intros.
  + destruct t as [| | | [ | ] ? | | | | |]; try (inv H).
(* Goal: @eq Int64.int i Int64.zero *)
    - destruct s; eapply tc_val_PM'_Tint; eauto.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
    - eapply tc_val_PM'_Tlong; eauto; reflexivity.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
    - eapply tc_val_PM'_Tfloat_single; eauto; reflexivity.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
    - eapply tc_val_PM'_Tfloat_double; eauto; reflexivity.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
    - eapply tc_val_PM'_Tpointer; eauto; reflexivity.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
    - eapply tc_val_PM'_Tpointer; eauto; reflexivity.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
    - eapply tc_val_PM'_Tpointer; eauto; reflexivity.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
    - eapply tc_val_PM'_Tstruct; eauto; reflexivity.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
    - eapply tc_val_PM'_Tunion; eauto; reflexivity.
  + inversion H; subst; auto;
    destruct t as [| | | [ | ] ? | | | | |]; try (inv H0);
(* Goal: @eq Int64.int i Int64.zero *)
    auto.
(* Goal: tc_val (Tint i s a0) v *)
(* Goal: tc_val (Tint i0 s a0) v *)
(* Goal: tc_val (Tint i0 s a0) v *)
    destruct i; inv H3.
(* Goal: tc_val (Tint i s a0) v *)
(* Goal: tc_val (Tint i0 s a0) v *)
(* Goal: tc_val (Tint i0 s a0) v *)
    destruct i; inv H3.
(* Goal: tc_val (Tint i s a0) v *)
(* Goal: tc_val (Tint i0 s a0) v *)
(* Goal: tc_val (Tint i0 s a0) v *)
    destruct i; inv H3.
(* Goal: tc_val (Tint i s a0) v *)
(* Goal: tc_val (Tint i0 s a0) v *)
(* Goal: tc_val (Tint i0 s a0) v *)
    destruct i; inv H3.
(* Goal: tc_val (Tint i0 s a0) v *)
    destruct i0; inv H3.
(* Goal: tc_val (Tint i0 s a0) v *)
    destruct i0; inv H3.
Qed.

Ltac solve_tc_val H :=
(* Goal: @eq positive a b *)
  rewrite tc_val_tc_val_PM in H; inv H.

Ltac solve_tc_val' H :=
(* Goal: @eq positive a b *)
  rewrite tc_val_tc_val_PM' in H; inv H.

Lemma tc_val_sem_binarith': forall {CS: compspecs} sem_int sem_long sem_float sem_single t1 t2 t v1 v2 deferr reterr rho m
  (TV2: tc_val t2 v2)
  (TV1: tc_val t1 v1),
  (denote_tc_assert (binarithType' t1 t2 t deferr reterr) rho) m ->
  tc_val t
    (force_val
      (Clight_Cop2.sem_binarith
        (fun s n1 n2 => Some (Vint (sem_int s n1 n2)))
        (fun s n1 n2 => Some (Vlong (sem_long s n1 n2)))
        (fun n1 n2 => Some (Vfloat (sem_float n1 n2)))
        (fun n1 n2 => Some (Vsingle (sem_single n1 n2)))
        t1 t2 v1 v2)).
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: tc_val t (force_val (sem_binarith (fun (s : signedness) (n1 n2 : Int.int) => @Some val (Vint (sem_int s n1 n2))) (fun (s : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (sem_long s n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (sem_float n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (sem_single n1 n2))) t1 t2 v1 v2)) *)
  unfold binarithType' in H.
(* Goal: tc_val t match sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Vint (match sg with | Signed => Int.mods | Unsigned => Int.modu end n1 n2))) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (match sg with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (fun _ _ : float => @None val) (fun _ _ : float32 => @None val) (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho) with | Some v' => v' | None => Vundef end *)
  unfold Clight_Cop2.sem_binarith.
(* Goal: tc_val t match match classify_binarith (typeof e1) (typeof e2) with | bin_case_i sg => both_int (fun n1 n2 : Int.int => @Some val (Vint (match sg with | Signed => Int.mods | Unsigned => Int.modu end n1 n2))) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_case_l sg => both_long (fun n1 n2 : Int64.int => @Some val (Vlong (match sg with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_case_f => both_float (fun _ _ : float => @None val) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_case_s => both_single (fun _ _ : float32 => @None val) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_default => fun _ _ : val => @None val end (@eval_expr CS e1 rho) (@eval_expr CS e2 rho) with | Some v' => v' | None => Vundef end *)
  rewrite classify_binarith_eq.
  destruct (classify_binarith' t1 t2) eqn:?H;
  try solve [inv H]; apply tc_bool_e in H;
  destruct t1 as [|  [| | |] [|] | | [ | ] ? | | | | |]; try discriminate H0;
  destruct t2 as [|  [| | |] [|] | | [ | ] ? | | | | |]; try inv H0;
  try contradiction;
  destruct v1; try solve [inv TV1];
  destruct v2; try solve [inv TV2];
  destruct t as [| [| | |] [|] ? | | [|] | | | | |]; inv H; simpl; auto; apply I.
Qed.

Lemma tc_val_sem_cmp_binarith': forall sem_int sem_long sem_float sem_single t1 t2 t v1 v2
  (TV2: tc_val t2 v2)
  (TV1: tc_val t1 v1),
  is_numeric_type t1 = true ->
  is_numeric_type t2 = true ->
  is_int_type t = true ->
  tc_val t
    (force_val
      (Clight_Cop2.sem_binarith
        (fun s n1 n2 => Some (Val.of_bool (sem_int s n1 n2)))
        (fun s n1 n2 => Some (Val.of_bool (sem_long s n1 n2)))
        (fun n1 n2 => Some (Val.of_bool (sem_float n1 n2)))
        (fun n1 n2 => Some (Val.of_bool (sem_single n1 n2)))
        t1 t2 v1 v2)).
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
  destruct t; inv H1.
(* Goal: tc_val t match sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Vint (match sg with | Signed => Int.mods | Unsigned => Int.modu end n1 n2))) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (match sg with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (fun _ _ : float => @None val) (fun _ _ : float32 => @None val) (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho) with | Some v' => v' | None => Vundef end *)
  unfold Clight_Cop2.sem_binarith.
(* Goal: tc_val t match match classify_binarith (typeof e1) (typeof e2) with | bin_case_i sg => both_int (fun n1 n2 : Int.int => @Some val (Vint (match sg with | Signed => Int.mods | Unsigned => Int.modu end n1 n2))) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_case_l sg => both_long (fun n1 n2 : Int64.int => @Some val (Vlong (match sg with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_case_f => both_float (fun _ _ : float => @None val) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_case_s => both_single (fun _ _ : float32 => @None val) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_default => fun _ _ : val => @None val end (@eval_expr CS e1 rho) (@eval_expr CS e2 rho) with | Some v' => v' | None => Vundef end *)
  rewrite classify_binarith_eq.
  destruct (classify_binarith' t1 t2) eqn:?H.
1,2,3,4:
  destruct t1 as [|  [| | |] [|] | | [ | ] ? | | | | |]; try discriminate H0;
  destruct t2 as [|  [| | |] [|] | | [ | ] ? | | | | |]; try inv H0;
  try contradiction;
  destruct v1; try solve [inv TV1];
  destruct v2; try solve [inv TV2];
  inv H1;
  simpl;
(* Goal: @eq Int64.int i Int64.zero *)
  apply tc_val_of_bool; auto.
  destruct t1 as [|  [| | |] [|] | | [ | ] ? | | | | |]; inv H;
  destruct t2 as [|  [| | |] [|] | | [ | ] ? | | | | |]; inv H0;
  inv H1.
Qed.

Lemma negb_true: forall a, negb a = true -> a = false.
Proof.  intros; destruct a; auto; inv H. Qed.

Lemma typecheck_Oadd_sound:
forall {CS: compspecs} (rho : environ) m (e1 e2 : expr) (t : type)
   (IBR: denote_tc_assert (isBinOpResultType Oadd e1 e2 t) rho m)
   (TV2: tc_val (typeof e2) (eval_expr e2 rho))
   (TV1: tc_val (typeof e1) (eval_expr e1 rho)),
   tc_val t
     (eval_binop Oadd (typeof e1) (typeof e2)
       (eval_expr e1 rho) (eval_expr e2 rho)).
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: tc_val t (@eval_binop CS Omod (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  rewrite den_isBinOpR in IBR. 
  unfold tc_int_or_ptr_type, eval_binop, sem_binary_operation', isBinOpResultType, Clight_Cop2.sem_add in IBR |- *.
(* Goal: tc_val t (force_val2 match classify_add (typeof e1) (typeof e2) with | add_case_pi ty si => @sem_add_ptr_int CS ty si | add_case_pl ty => @sem_add_ptr_long CS ty | add_case_ip si ty => @sem_add_int_ptr CS ty si | add_case_lp ty => @sem_add_long_ptr CS ty | add_default => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.add n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.add n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.add n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.add n1 n2))) (typeof e1) (typeof e2) end (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  rewrite classify_add_eq.
  destruct (classify_add' (typeof e1) (typeof e2)) eqn:?H;
  unfold force_val2, force_val;
  rewrite tc_val_tc_val_PM in TV1,TV2|-*;
  unfold classify_add' in H; simpl in IBR;
    repeat match goal with
    | H: _ /\ _ |- _ => destruct H
    | H: app_pred (denote_tc_assert (tc_bool _ _) _) _ |- _ => 
                      apply tc_bool_e in H
    | H: negb (eqb_type ?A ?B) = true |- _ =>
             let J := fresh "J" in
              destruct (eqb_type A B) eqn:J; [inv H | clear H]              
    end;
  try solve [
    unfold is_pointer_type in H1;
    destruct (typeof e1) as [| [| | |] ? ? | | [|] | | | | |]; inv TV1;
    destruct (typeof e2) as [| [| | |] ? ? | | [|] | | | | |]; inv TV2;
    simpl in H; inv H;
    try rewrite J in *; clear J;
    destruct (eval_expr e1 rho), (eval_expr e2 rho);
     simpl in *; try contradiction;
    destruct t; try solve [inv H1];
    try solve [constructor; try rewrite (negb_true _ H1); apply I]
  ].
(* Goal: tc_val t (force_val2 (fun v1 v2 : val => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.mul n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.mul n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.mul n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.mul n1 n2))) (typeof e1) (typeof e2) v1 v2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  rewrite denote_tc_assert_andp in IBR. destruct IBR.
  rewrite <- tc_val_tc_val_PM in TV1,TV2|-*.
(* Goal: @eq Int64.int i Int64.zero *)
  eapply tc_val_sem_binarith'; eauto.
Qed.

Lemma peq_eq_block:
   forall a b A (c d: A), is_true (peq a b) ->
       (if eq_block a b then c else d) = c.
 Proof.
(* Goal: @eq Int64.int i Int64.zero *)
  intros. rewrite if_true; auto.
(* Goal: @eq Int64.int i Int64.zero *)
   destruct (peq a b); auto. inv H.
 Qed.

Lemma typecheck_Osub_sound:
forall {CS: compspecs} (rho : environ) m (e1 e2 : expr) (t : type)
   (IBR: denote_tc_assert (isBinOpResultType Osub e1 e2 t) rho m)
   (TV2: tc_val (typeof e2) (eval_expr e2 rho))
   (TV1: tc_val (typeof e1) (eval_expr e1 rho)),
   tc_val t
     (eval_binop Osub (typeof e1) (typeof e2)
       (eval_expr e1 rho) (eval_expr e2 rho)).
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: tc_val t (@eval_binop CS Omod (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  rewrite den_isBinOpR in IBR.
  unfold tc_int_or_ptr_type, eval_binop, sem_binary_operation', isBinOpResultType, Clight_Cop2.sem_sub in IBR |- *.
(* Goal: tc_val t (force_val2 match classify_sub (typeof e1) (typeof e2) with | sub_case_pi ty si => @sem_sub_pi CS ty si | sub_case_pp ty => @sem_sub_pp CS ty | sub_case_pl ty => @sem_sub_pl CS ty | sub_default => sem_sub_default (typeof e1) (typeof e2) end (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  rewrite classify_sub_eq.
  destruct (classify_sub' (typeof e1) (typeof e2)) eqn:?H;
  unfold force_val2, force_val;
  rewrite tc_val_tc_val_PM in TV1,TV2|-*;
  unfold classify_sub' in H; simpl in IBR;
    repeat match goal with
    | H: _ /\ _ |- _ => destruct H
    | H: app_pred (denote_tc_assert (tc_bool _ _) _) _ |- _ => 
                      apply tc_bool_e in H
    | H: negb (eqb_type ?A ?B) = true |- _ =>
             let J := fresh "J" in
              destruct (eqb_type A B) eqn:J; [inv H | clear H]              
    end;
  try solve [
    unfold is_pointer_type in H1;
    destruct (typeof e1); inv TV1; destruct (typeof e2) as [| [| | |] [|] | | | | | | |]; inv TV2;
    simpl in H; inv H;
    try rewrite J in *; clear J;
    destruct (eval_expr e1 rho), (eval_expr e2 rho);
     simpl in *; try contradiction;
    destruct t; try solve [inv H1];
    try solve [constructor; try rewrite (negb_true _ H1); apply I]
  ].
 +
    destruct (typeof e1); inv TV1; destruct (typeof e2); inv TV2;
    simpl in H; inv H;
    rewrite ?J, ?J0 in *; clear J J0;
    destruct (eval_expr e1 rho), (eval_expr e2 rho);
     simpl in *; try contradiction;
    destruct t as [| [| | |] [|] | | | | | | |]; inv H4;
    simpl; constructor;
    try (rewrite peq_eq_block by auto; 
           rewrite sizeof_range_true by auto);
    try discriminate;
    try apply I.
 +
  rewrite <- tc_val_tc_val_PM in TV1,TV2|-*.
(* Goal: tc_val t (force_val2 (fun v1 v2 : val => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.mul n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.mul n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.mul n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.mul n1 n2))) (typeof e1) (typeof e2) v1 v2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  rewrite denote_tc_assert_andp in IBR. destruct IBR.
(* Goal: @eq Int64.int i Int64.zero *)
  eapply tc_val_sem_binarith'; eauto.
Qed.

Lemma typecheck_Omul_sound:
forall {CS: compspecs} (rho : environ) m (e1 e2 : expr) (t : type)
   (IBR: denote_tc_assert (isBinOpResultType Omul e1 e2 t) rho m)
   (TV2: tc_val (typeof e2) (eval_expr e2 rho))
   (TV1: tc_val (typeof e1) (eval_expr e1 rho)),
   tc_val t
     (eval_binop Omul (typeof e1) (typeof e2)
       (eval_expr e1 rho) (eval_expr e2 rho)).
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: tc_val t (@eval_binop CS Omod (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  rewrite den_isBinOpR in IBR. 
  unfold eval_binop, sem_binary_operation', isBinOpResultType, Clight_Cop2.sem_mul in IBR |- *.
(* Goal: tc_val t (force_val2 (fun v1 v2 : val => sem_binarith (fun (_ : signedness) (n1 n2 : Int.int) => @Some val (Vint (Int.mul n1 n2))) (fun (_ : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (Int64.mul n1 n2))) (fun n1 n2 : float => @Some val (Vfloat (Float.mul n1 n2))) (fun n1 n2 : float32 => @Some val (Vsingle (Float32.mul n1 n2))) (typeof e1) (typeof e2) v1 v2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  rewrite denote_tc_assert_andp in IBR. destruct IBR.
(* Goal: tc_val t (force_val2 (fun v1 v2 : val => sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Vint (match sg with | Signed => Int.mods | Unsigned => Int.modu end n1 n2))) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (match sg with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (fun _ _ : float => @None val) (fun _ _ : float32 => @None val) (typeof e1) (typeof e2) v1 v2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  unfold force_val2, force_val.
(* Goal: @eq Int64.int i Int64.zero *)
  eapply tc_val_sem_binarith'; eauto.
Qed.

Lemma typecheck_Odiv_sound:
forall {CS: compspecs} (rho : environ) m (e1 e2 : expr) (t : type)
   (IBR: denote_tc_assert (isBinOpResultType Odiv e1 e2 t) rho m)
   (TV2: tc_val (typeof e2) (eval_expr e2 rho))
   (TV1: tc_val (typeof e1) (eval_expr e1 rho)),
   tc_val t
     (eval_binop Odiv (typeof e1) (typeof e2)
       (eval_expr e1 rho) (eval_expr e2 rho)).
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: tc_val t (@eval_binop CS Omod (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  rewrite den_isBinOpR in IBR.
  unfold eval_binop, sem_binary_operation', isBinOpResultType, Clight_Cop2.sem_mul in IBR |- *.
(* Goal: tc_val t (force_val2 (fun v1 v2 : val => sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Vint (match sg with | Signed => Int.mods | Unsigned => Int.modu end n1 n2))) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (match sg with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (fun _ _ : float => @None val) (fun _ _ : float32 => @None val) (typeof e1) (typeof e2) v1 v2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  unfold force_val2, force_val.
(* Goal: @eq Int64.int i Int64.zero *)
  eapply (tc_val_sem_binarith' _ _ _ _ _ _ _ _ _ _ _ rho m); eauto.
  unfold binarithType'.
(* Goal: @eq Int64.int i Int64.zero *)
  destruct (classify_binarith' (typeof e1) (typeof e2)); eauto.
(* Goal: @eq Int64.int i Int64.zero *)
  + destruct s; destruct IBR; eauto.
(* Goal: @eq Int64.int i Int64.zero *)
  + destruct s; destruct IBR; eauto.
Qed.

Lemma typecheck_Omod_sound:
forall {CS: compspecs} (rho : environ) m (e1 e2 : expr) (t : type)
   (IBR: denote_tc_assert (isBinOpResultType Omod e1 e2 t) rho m)
   (TV2: tc_val (typeof e2) (eval_expr e2 rho))
   (TV1: tc_val (typeof e1) (eval_expr e1 rho)),
   tc_val t
     (eval_binop Omod (typeof e1) (typeof e2)
       (eval_expr e1 rho) (eval_expr e2 rho)).
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
(* Goal: tc_val t (@eval_binop CS Omod (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  rewrite den_isBinOpR in IBR.
  unfold eval_binop, sem_binary_operation', isBinOpResultType, Clight_Cop2.sem_mod in IBR |- *.
(* Goal: tc_val t (force_val2 (fun v1 v2 : val => sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Vint (match sg with | Signed => Int.mods | Unsigned => Int.modu end n1 n2))) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (match sg with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (fun _ _ : float => @None val) (fun _ _ : float32 => @None val) (typeof e1) (typeof e2) v1 v2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  unfold force_val2, force_val.
(* Goal: tc_val t match sem_binarith (fun (sg : signedness) (n1 n2 : Int.int) => @Some val (Vint (match sg with | Signed => Int.mods | Unsigned => Int.modu end n1 n2))) (fun (sg : signedness) (n1 n2 : Int64.int) => @Some val (Vlong (match sg with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (fun _ _ : float => @None val) (fun _ _ : float32 => @None val) (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho) with | Some v' => v' | None => Vundef end *)
  unfold Clight_Cop2.sem_binarith.
(* Goal: tc_val t match match classify_binarith (typeof e1) (typeof e2) with | bin_case_i sg => both_int (fun n1 n2 : Int.int => @Some val (Vint (match sg with | Signed => Int.mods | Unsigned => Int.modu end n1 n2))) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_case_l sg => both_long (fun n1 n2 : Int64.int => @Some val (Vlong (match sg with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_case_f => both_float (fun _ _ : float => @None val) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_case_s => both_single (fun _ _ : float32 => @None val) (sem_cast (typeof e1) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith (typeof e1) (typeof e2)))) | bin_default => fun _ _ : val => @None val end (@eval_expr CS e1 rho) (@eval_expr CS e2 rho) with | Some v' => v' | None => Vundef end *)
  rewrite classify_binarith_eq.
(* Goal: tc_val t match match classify_binarith' (typeof e1) (typeof e2) with | bin_case_i sg => both_int (fun n1 n2 : Int.int => @Some val (Vint (match sg with | Signed => Int.mods | Unsigned => Int.modu end n1 n2))) (sem_cast (typeof e1) (binarith_type (classify_binarith' (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith' (typeof e1) (typeof e2)))) | bin_case_l sg => both_long (fun n1 n2 : Int64.int => @Some val (Vlong (match sg with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (sem_cast (typeof e1) (binarith_type (classify_binarith' (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith' (typeof e1) (typeof e2)))) | bin_case_f => both_float (fun _ _ : float => @None val) (sem_cast (typeof e1) (binarith_type (classify_binarith' (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith' (typeof e1) (typeof e2)))) | bin_case_s => both_single (fun _ _ : float32 => @None val) (sem_cast (typeof e1) (binarith_type (classify_binarith' (typeof e1) (typeof e2)))) (sem_cast (typeof e2) (binarith_type (classify_binarith' (typeof e1) (typeof e2)))) | bin_default => fun _ _ : val => @None val end (@eval_expr CS e1 rho) (@eval_expr CS e2 rho) with | Some v' => v' | None => Vundef end *)
  destruct (classify_binarith' (typeof e1) (typeof e2)) eqn:?H.
  + solve_tc_val TV1;
    solve_tc_val TV2;
    rewrite <- H2, <- H0 in H;
    try solve [inv H];
    try solve [destruct sz,sg; inv H].
(* Goal: tc_val t match both_long (fun n1 n2 : Int64.int => @Some val (Vlong (match s with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (sem_cast (Tlong s0 a) (binarith_type (bin_case_l s))) (sem_cast (Tlong s1 a0) (binarith_type (bin_case_l s))) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho) with | Some v' => v' | None => Vundef end *)
    destruct s; destruct IBR as [?IBR ?IBR].
    - destruct IBR as [?IBR ?IBR].
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
      apply tc_bool_e in IBR0.
      simpl in IBR, IBR1 |- *; unfold_lift in IBR; unfold_lift in IBR1.
      destruct (eval_expr e1 rho), (eval_expr e2 rho);
      try solve [inv H1 | inv H3 | inv IBR].
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
      unfold both_int; simpl.
(* Goal: tc_val t match match sem_cast (Tint sz sg a) (Tint I32 Unsigned noattr) (Vint i) with | Some (Vundef as v) => @None val | Some (Vint v1' as v) => match sem_cast (Tint sz0 sg0 a0) (Tint I32 Unsigned noattr) (Vint i0) with | Some (Vundef as v0) => @None val | Some (Vint v2' as v0) => @Some val (Vint (Int.modu v1' v2')) | Some (Vlong i as v0) => @None val | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vlong i as v) => @None val | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
      apply denote_tc_nonzero_e in IBR; try rewrite IBR.
(* Goal: tc_val t match match sem_cast (Tint sz sg a) (Tint I32 Signed noattr) (Vint i) with | Some (Vundef as v) => @None val | Some (Vint v1' as v) => match sem_cast (Tint sz0 sg0 a0) (Tint I32 Signed noattr) (Vint i0) with | Some (Vundef as v0) => @None val | Some (Vint v2' as v0) => @Some val (Vint (Int.mods v1' v2')) | Some (Vlong i as v0) => @None val | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vlong i as v) => @None val | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
      apply denote_tc_nodivover_e in IBR1; try rewrite IBR1.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
      simpl.
      destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0];
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
      simpl; auto.
(* Goal: is_int I32 s match match sem_cast (Tint sz sg a) (Tint I32 Unsigned noattr) (Vint i) with | Some (Vundef as v) => @None val | Some (Vint v1' as v) => match sem_cast (Tint sz0 sg0 a0) (Tint I32 Unsigned noattr) (Vint i0) with | Some (Vundef as v0) => @None val | Some (Vint v2' as v0) => @Some val (Vint (Int.modu v1' v2')) | Some (Vlong i as v0) => @None val | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vlong i as v) => @None val | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
      unfold Clight_Cop2.sem_cast, Clight_Cop2.classify_cast.
      unfold  sem_cast_pointer.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
      destruct Archi.ptr64; reflexivity.
    - apply tc_bool_e in IBR0.
      simpl in IBR |- *; unfold_lift in IBR.
      destruct (eval_expr e1 rho), (eval_expr e2 rho);
      try solve [inv H1 | inv H3 | inv IBR].
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
      unfold both_int; simpl.
(* Goal: tc_val t match match sem_cast (Tint sz sg a) (Tint I32 Unsigned noattr) (Vint i) with | Some (Vundef as v) => @None val | Some (Vint v1' as v) => match sem_cast (Tint sz0 sg0 a0) (Tint I32 Unsigned noattr) (Vint i0) with | Some (Vundef as v0) => @None val | Some (Vint v2' as v0) => @Some val (Vint (Int.modu v1' v2')) | Some (Vlong i as v0) => @None val | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vlong i as v) => @None val | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
      apply denote_tc_nonzero_e in IBR; try rewrite IBR.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
      simpl.
      destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0];
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
      simpl; auto.
(* Goal: is_int I32 s match match sem_cast (Tint sz sg a) (Tint I32 Unsigned noattr) (Vint i) with | Some (Vundef as v) => @None val | Some (Vint v1' as v) => match sem_cast (Tint sz0 sg0 a0) (Tint I32 Unsigned noattr) (Vint i0) with | Some (Vundef as v0) => @None val | Some (Vint v2' as v0) => @Some val (Vint (Int.modu v1' v2')) | Some (Vlong i as v0) => @None val | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vlong i as v) => @None val | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
      unfold Clight_Cop2.sem_cast, Clight_Cop2.classify_cast.
      unfold  sem_cast_pointer.
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
      destruct Archi.ptr64; reflexivity.
  + solve_tc_val TV1;
    solve_tc_val TV2;
    rewrite <- H2, <- H0 in H;
    try solve [inv H];
    try solve [destruct sz,sg; try destruct sz0,sg0; inv H].
    - (* int long *)
(* Goal: tc_val t match both_long (fun n1 n2 : Int64.int => @Some val (Vlong (match s with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (sem_cast (Tlong s0 a) (binarith_type (bin_case_l s))) (sem_cast (Tlong s1 a0) (binarith_type (bin_case_l s))) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho) with | Some v' => v' | None => Vundef end *)
      destruct s; destruct IBR as [?IBR ?IBR].
      * destruct IBR as [?IBR ?IBR].
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
        apply tc_bool_e in IBR0.
        simpl in IBR, IBR1 |- *; unfold_lift in IBR; unfold_lift in IBR1.
        destruct (eval_expr e1 rho), (eval_expr e2 rho);
          try solve [inv H1 | inv H3].
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        unfold both_long; simpl.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Unsigned noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Unsigned noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.modu v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        apply denote_tc_nonzero_e64 in IBR; try rewrite IBR.
(* Goal: tc_val t match match sem_cast (Tlong s0 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v2' as v) => @Some val (Vlong (Int64.mods (cast_int_long sg i) v2')) | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        apply (denote_tc_nodivover_e64_il sg) in IBR1; try rewrite IBR1.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        simpl.
        destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0];
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
        simpl; auto.
      * apply tc_bool_e in IBR0.
        simpl in IBR |- *; unfold_lift in IBR.
        destruct (eval_expr e1 rho), (eval_expr e2 rho);
        try solve [inv H1 | inv H3 | inv IBR].
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        unfold both_long; simpl.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Unsigned noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Unsigned noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.modu v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        apply denote_tc_nonzero_e64 in IBR; try rewrite IBR.
        destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0];
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
        simpl; auto.
    - (* long int *)
(* Goal: tc_val t match both_long (fun n1 n2 : Int64.int => @Some val (Vlong (match s with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (sem_cast (Tlong s0 a) (binarith_type (bin_case_l s))) (sem_cast (Tlong s1 a0) (binarith_type (bin_case_l s))) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho) with | Some v' => v' | None => Vundef end *)
      destruct s; destruct IBR as [?IBR ?IBR].
      * destruct IBR as [?IBR ?IBR].
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
        apply tc_bool_e in IBR0.
        simpl in IBR, IBR1 |- *; unfold_lift in IBR; unfold_lift in IBR1.
        destruct (eval_expr e1 rho), (eval_expr e2 rho);
          try solve [inv H1 | inv H3].
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        unfold both_long; simpl.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Unsigned noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => @Some val (Vlong (Int64.modu v1' (cast_int_long sg i0))) | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        apply denote_tc_nonzero_e, (Int64_eq_repr_int_nonzero sg) in IBR; try rewrite IBR.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => @Some val (Vlong (Int64.mods v1' (cast_int_long sg i0))) | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        apply (denote_tc_nodivover_e64_li sg) in IBR1; try rewrite IBR1.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        simpl.
        destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0];
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
        simpl; auto.
      * apply tc_bool_e in IBR0.
        simpl in IBR |- *; unfold_lift in IBR.
        destruct (eval_expr e1 rho), (eval_expr e2 rho);
        try solve [inv H1 | inv H3 | inv IBR].
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        unfold both_long; simpl.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Unsigned noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => @Some val (Vlong (Int64.modu v1' (cast_int_long sg i0))) | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        apply denote_tc_nonzero_e, (Int64_eq_repr_int_nonzero sg) in IBR; try rewrite IBR.
        destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0];
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
        simpl; auto.
    - (* long long *)
(* Goal: tc_val t match both_long (fun n1 n2 : Int64.int => @Some val (Vlong (match s with | Signed => Int64.mods | Unsigned => Int64.modu end n1 n2))) (sem_cast (Tlong s0 a) (binarith_type (bin_case_l s))) (sem_cast (Tlong s1 a0) (binarith_type (bin_case_l s))) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho) with | Some v' => v' | None => Vundef end *)
      destruct s; destruct IBR as [?IBR ?IBR].
      * destruct IBR as [?IBR ?IBR].
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
        apply tc_bool_e in IBR0.
        simpl in IBR, IBR1 |- *; unfold_lift in IBR; unfold_lift in IBR1.
        destruct (eval_expr e1 rho), (eval_expr e2 rho);
          try solve [inv H1 | inv H3].
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        unfold both_long; simpl.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Unsigned noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Unsigned noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.modu v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        apply denote_tc_nonzero_e64 in IBR; try rewrite IBR.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        apply denote_tc_nodivover_e64_ll in IBR1; try rewrite IBR1.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        simpl.
        destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0];
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
        simpl; auto.
      * apply tc_bool_e in IBR0.
        simpl in IBR |- *; unfold_lift in IBR.
        destruct (eval_expr e1 rho), (eval_expr e2 rho);
        try solve [inv H1 | inv H3 | inv IBR].
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        unfold both_long; simpl.
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Unsigned noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Unsigned noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.modu v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
        apply denote_tc_nonzero_e64 in IBR; try rewrite IBR.
        destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0];
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
        simpl; auto.
  + inv IBR.
  + inv IBR.
  + inv IBR.
Qed.

Lemma typecheck_Oshift_sound:
 forall op {CS: compspecs} (rho : environ) m (e1 e2 : expr) (t : type)
   (IBR: denote_tc_assert (isBinOpResultType op e1 e2 t) rho m)
   (TV2: tc_val (typeof e2) (eval_expr e2 rho))
   (TV1: tc_val (typeof e1) (eval_expr e1 rho))
   (OP: op = Oshl \/ op = Oshr),
   tc_val t
     (eval_binop op (typeof e1) (typeof e2) (eval_expr e1 rho) (eval_expr e2 rho)).
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
  replace
    ((denote_tc_assert (isBinOpResultType op e1 e2 t) rho) m)
  with
    ((denote_tc_assert
           match classify_shift' (typeof e1) (typeof e2) with
           | shift_case_ii _ =>
               tc_andp' (tc_ilt' e2 Int.iwordsize)
                 (tc_bool (is_int32_type t) (op_result_type (Ebinop op e1 e2 t)))
           | shift_case_il _ =>
               tc_andp' (tc_llt' e2 (Int64.repr 32))
                 (tc_bool (is_int32_type t) (op_result_type (Ebinop op e1 e2 t)))
           | shift_case_li _ =>
               tc_andp' (tc_ilt' e2 Int64.iwordsize')
                 (tc_bool (is_long_type t) (op_result_type (Ebinop op e1 e2 t)))
           | shift_case_ll _ =>
               tc_andp' (tc_llt' e2 Int64.iwordsize)
                 (tc_bool (is_long_type t) (op_result_type (Ebinop op e1 e2 t)))
           | _ => tc_FF (arg_type (Ebinop op e1 e2 t))
           end rho) m)
  in IBR
  by (rewrite den_isBinOpR; destruct OP; subst; auto).
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  destruct (classify_shift' (typeof e1) (typeof e2)) eqn:?H; try solve [inv IBR].
  + (* shift_ii *)
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    destruct IBR as [?IBR ?IBR].
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    apply tc_bool_e in IBR0.
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    simpl in IBR; unfold_lift in IBR.
    solve_tc_val TV1;
    solve_tc_val TV2;
    rewrite <- H0, <- H2 in H;
    try solve [inv H];
    try solve [destruct sz,sg; try destruct sz0,sg0; inv H].
    destruct (eval_expr e1 rho), (eval_expr e2 rho);
      try solve [inv H1 | inv H3].
    destruct OP; subst; auto;
    simpl;
    unfold force_val, Clight_Cop2.sem_shift;
    rewrite classify_shift_eq, H;
(* Goal: tc_val t match match sem_cast (Tlong s0 a) (Tlong Signed noattr) (Vlong i) with | Some (Vundef as v) => @None val | Some (Vint i as v) => @None val | Some (Vlong v1' as v) => match sem_cast (Tlong s1 a0) (Tlong Signed noattr) (Vlong i0) with | Some (Vundef as v0) => @None val | Some (Vint i as v0) => @None val | Some (Vlong v2' as v0) => @Some val (Vlong (Int64.mods v1' v2')) | Some (Vfloat f as v0) => @None val | Some (Vsingle f as v0) => @None val | Some (Vptr b i as v0) => @None val | None => @None val end | Some (Vfloat f as v) => @None val | Some (Vsingle f as v) => @None val | Some (Vptr b i as v) => @None val | None => @None val end with | Some v' => v' | None => Vundef end *)
    simpl.
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
    - destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0]; simpl; auto.
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
    - destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0]; simpl; auto.
  + (* shift_ll *)
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    destruct IBR as [?IBR ?IBR].
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    apply tc_bool_e in IBR0.
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    simpl in IBR; unfold_lift in IBR.
    solve_tc_val TV1;
    solve_tc_val TV2;
    rewrite <- H0, <- H2 in H;
    try solve [inv H];
    try solve [destruct sz,sg; try destruct sz0,sg0; inv H].
    destruct (eval_expr e1 rho), (eval_expr e2 rho);
      try solve [inv H1 | inv H3].
    destruct OP; subst; auto;
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
    simpl; destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0]; simpl; auto.
  + (* shift_il *)
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    destruct IBR as [?IBR ?IBR].
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    apply tc_bool_e in IBR0.
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    simpl in IBR; unfold_lift in IBR.
    solve_tc_val TV1;
    solve_tc_val TV2;
    rewrite <- H0, <- H2 in H;
    try solve [inv H];
    try solve [destruct sz,sg; try destruct sz0,sg0; inv H].
    destruct (eval_expr e1 rho), (eval_expr e2 rho);
      try solve [inv H1 | inv H3].
    destruct OP; subst; auto;
    simpl;
    unfold force_val, Clight_Cop2.sem_shift;
    rewrite classify_shift_eq, H;
    simpl;
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
    destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0]; simpl; auto.
  + (* shift_li *)
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    destruct IBR as [?IBR ?IBR].
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    apply tc_bool_e in IBR0.
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    simpl in IBR; unfold_lift in IBR.
    solve_tc_val TV1;
    solve_tc_val TV2;
    rewrite <- H0, <- H2 in H;
    try solve [inv H];
    try solve [destruct sz,sg; try destruct sz0,sg0; inv H].
    destruct (eval_expr e1 rho), (eval_expr e2 rho);
      try solve [inv H1 | inv H3].
    destruct OP; subst; auto;
    simpl;
    unfold force_val, Clight_Cop2.sem_shift;
    rewrite classify_shift_eq, H;
    simpl;
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
    destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR0]; simpl; auto.
Qed.

Lemma typecheck_Obin_sound:
 forall op {CS: compspecs} (rho : environ) m (e1 e2 : expr) (t : type)
   (IBR: denote_tc_assert (isBinOpResultType op e1 e2 t) rho m)
   (TV2: tc_val (typeof e2) (eval_expr e2 rho))
   (TV1: tc_val (typeof e1) (eval_expr e1 rho))
   (OP: op = Oand \/ op = Oor \/ op = Oxor),
   tc_val t
     (eval_binop op (typeof e1) (typeof e2) (eval_expr e1 rho) (eval_expr e2 rho)).
Proof.
(* Goal: forall (op : binary_operation) (CS : compspecs) (rho : environ) (m : rmap) (e1 e2 : expr) (t : type) (_ : @app_pred rmap ag_rmap (@denote_tc_assert CS (@isBinOpResultType CS op e1 e2 t) rho) m) (_ : tc_val (typeof e2) (@eval_expr CS e2 rho)) (_ : tc_val (typeof e1) (@eval_expr CS e1 rho)) (_ : or (@eq binary_operation op Oand) (or (@eq binary_operation op Oor) (@eq binary_operation op Oxor))), tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  intros.
  replace
    ((denote_tc_assert (isBinOpResultType op e1 e2 t) rho) m)
  with
    ((denote_tc_assert
           match classify_binarith' (typeof e1) (typeof e2) with
           | bin_case_i _ => tc_bool (is_int32_type t) (op_result_type (Ebinop op e1 e2 t))
           | bin_case_l _ => tc_bool (is_long_type t) (op_result_type (Ebinop op e1 e2 t))
           | _ => tc_FF (arg_type (Ebinop op e1 e2 t))
           end rho) m)
  in IBR
  by (rewrite den_isBinOpR; destruct OP as [| [ | ]]; subst; auto).
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
  destruct (classify_binarith' (typeof e1) (typeof e2)) eqn:?H; try solve [inv IBR].
  + (* bin_case_i *)
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    apply tc_bool_e in IBR.
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    simpl in IBR; unfold_lift in IBR.
    solve_tc_val TV1;
    solve_tc_val TV2;
    rewrite <- H0, <- H2 in H;
    try solve [inv H];
    try solve [destruct sz,sg; try destruct sz0,sg0; inv H].
    destruct (eval_expr e1 rho), (eval_expr e2 rho);
      try solve [inv H1 | inv H3].
(* Goal: tc_val t (@eval_binop CS op (Tint sz sg a) (Tint sz0 sg0 a0) (Vint i) (Vint i0)) *)
   clear e1 e2 H0 H2.
    destruct OP as [| [|]]; subst; auto;
    simpl;
    unfold force_val, Clight_Cop2.sem_and, Clight_Cop2.sem_or, Clight_Cop2.sem_xor, Clight_Cop2.sem_binarith;
    rewrite classify_binarith_eq, H;
    simpl;
    destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR]; simpl; auto;
    unfold both_int, Clight_Cop2.sem_cast, Clight_Cop2.classify_cast, sem_cast_pointer;
(* Goal: @eq A (if andb (@proj_sumbool (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) (@left (Z.lt Z0 (@sizeof CS t)) (Z.ge Z0 (@sizeof CS t)) l)) (@proj_sumbool (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) (@left (Z.le (@sizeof CS t) max) (Z.gt (@sizeof CS t) max) l0)) then a else b) a *)
   destruct Archi.ptr64; reflexivity.
  + (* bin_case_l *)
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    apply tc_bool_e in IBR.
(* Goal: tc_val t (@eval_binop CS op (typeof e1) (typeof e2) (@eval_expr CS e1 rho) (@eval_expr CS e2 rho)) *)
    simpl in IBR; unfold_lift in IBR.
    solve_tc_val TV1;
    solve_tc_val TV2;
    rewrite <- H0, <- H2 in H;
    try solve [inv H];
    try solve [destruct sz,sg; try destruct sz0,sg0; inv H].
    - destruct (eval_expr e1 rho), (eval_expr e2 rho);
        try solve [inv H1 | inv H3].
      destruct OP as [| [|]]; subst; auto;
      simpl;
      unfold force_val, Clight_Cop2.sem_and, Clight_Cop2.sem_or, Clight_Cop2.sem_xor, Clight_Cop2.sem_binarith;
      rewrite classify_binarith_eq, H;
      simpl;
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
      destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR]; simpl; auto.
    - destruct (eval_expr e1 rho), (eval_expr e2 rho);
        try solve [inv H1 | inv H3].
      destruct OP as [| [|]]; subst; auto;
      simpl;
      unfold force_val, Clight_Cop2.sem_and, Clight_Cop2.sem_or, Clight_Cop2.sem_xor, Clight_Cop2.sem_binarith;
      rewrite classify_binarith_eq, H;
      simpl;
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
      destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR]; simpl; auto.
    - destruct (eval_expr e1 rho), (eval_expr e2 rho);
        try solve [inv H1 | inv H3].
      destruct OP as [| [|]]; subst; auto;
      simpl;
      unfold force_val, Clight_Cop2.sem_and, Clight_Cop2.sem_or, Clight_Cop2.sem_xor, Clight_Cop2.sem_binarith;
      rewrite classify_binarith_eq, H;
      simpl;
(* Goal: forall (i j : Int64.int) (m : rmap) (_ : @app_pred rmap ag_rmap (denote_tc_nodivover (Vlong i) (Vlong j)) m), not (and (@eq Int64.int i (Int64.repr Int64.min_signed)) (@eq Int64.int j Int64.mone)) *)
      destruct t as [| [| | |] ? ? | | | | | | |]; try solve [inv IBR]; simpl; auto.
Qed.

