(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Correctness of instruction selection for operators *)

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Cminor.
Require Import Op.
Require Import CminorSel.
Require Import SelectOp.

Local Open Scope cminorsel_scope.

(** * Useful lemmas and tactics *)

(** The following are trivial lemmas and custom tactics that help
  perform backward (inversion) and forward reasoning over the evaluation
  of operator applications. *)

Ltac EvalOp := eapply eval_Eop; eauto with evalexpr.

Ltac InvEval1 :=
  match goal with
  | [ H: (eval_expr _ _ _ _ _ (Eop _ Enil) _) |- _ ] =>
      inv H; InvEval1
  | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: Enil)) _) |- _ ] =>
      inv H; InvEval1
  | [ H: (eval_expr _ _ _ _ _ (Eop _ (_ ::: _ ::: Enil)) _) |- _ ] =>
      inv H; InvEval1
  | [ H: (eval_exprlist _ _ _ _ _ Enil _) |- _ ] =>
      inv H; InvEval1
  | [ H: (eval_exprlist _ _ _ _ _ (_ ::: _) _) |- _ ] =>
      inv H; InvEval1
  | _ =>
      idtac
  end.

Ltac InvEval2 :=
  match goal with
  | [ H: (eval_operation _ _ _ nil _ = Some _) |- _ ] =>
      simpl in H; FuncInv
  | [ H: (eval_operation _ _ _ (_ :: nil) _ = Some _) |- _ ] =>
      simpl in H; FuncInv
  | [ H: (eval_operation _ _ _ (_ :: _ :: nil) _ = Some _) |- _ ] =>
      simpl in H; FuncInv
  | [ H: (eval_operation _ _ _ (_ :: _ :: _ :: nil) _ = Some _) |- _ ] =>
      simpl in H; FuncInv
  | _ =>
      idtac
  end.

Ltac InvEval := InvEval1; InvEval2; InvEval2; subst.

Ltac TrivialExists :=
  match goal with
  | [ |- exists v, _ /\ Val.lessdef ?a v ] => exists a; split; [EvalOp | auto]
  end.

(** * Correctness of the smart constructors *)

Section CMCONSTR.

Variable ge: genv.
Variable sp: val.
Variable e: env.
Variable m: mem.

(** We now show that the code generated by "smart constructor" functions
  such as [SelectOp.notint] behaves as expected.  Continuing the
  [notint] example, we show that if the expression [e]
  evaluates to some integer value [Vint n], then [SelectOp.notint e]
  evaluates to a value [Vint (Int.not n)] which is indeed the integer
  negation of the value of [e].

  All proofs follow a common pattern:
- Reasoning by case over the result of the classification functions
  (such as [add_match] for integer addition), gathering additional
  information on the shape of the argument expressions in the non-default
  cases.
- Inversion of the evaluations of the arguments, exploiting the additional
  information thus gathered.
- Equational reasoning over the arithmetic operations performed,
  using the lemmas from the [Int] and [Float] modules.
- Construction of an evaluation derivation for the expression returned
(* Goal: eval_exprlist ge sp e m le Enil (@nil val) *)
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  by the smart constructor.
*)

Definition unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop :=
  forall le a x,
  eval_expr ge sp e m le a x ->
  exists v, eval_expr ge sp e m le (cstr a) v /\ Val.lessdef (sem x) v.

Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> val -> val) : Prop :=
  forall le a x b y,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef (sem x y) v.

Lemma eval_Olea_ptr:
  forall a el m,
  eval_operation ge sp (Olea_ptr a) el m = eval_addressing ge sp a el.
Proof.
(* Goal: forall (a : Op.addressing) (el : list val) (m : Mem.mem), @eq (option val) (@eval_operation fundef unit ge sp (Olea_ptr a) el m) (@eval_addressing fundef unit ge sp a el) *)
  unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto.
Qed.

Theorem eval_addrsymbol:
  forall le id ofs,
  exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. unfold addrsymbol. exists (Genv.symbol_address ge id ofs); split; auto.
  destruct (symbol_is_external id).
  predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  subst. EvalOp.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  EvalOp. econstructor. EvalOp. simpl; eauto. econstructor.
  unfold Olea_ptr; destruct Archi.ptr64 eqn:SF; simpl;
  [ rewrite <- Genv.shift_symbol_address_64 by auto | rewrite <- Genv.shift_symbol_address_32 by auto ];
  f_equal; f_equal;
  rewrite Ptrofs.add_zero_l;
  [ apply Ptrofs.of_int64_to_int64 | apply Ptrofs.of_int_to_int ];
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  auto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  EvalOp. (*rewrite eval_Olea_ptr. apply eval_addressing_Aglobal. *)
Qed.

Theorem eval_addrstack:
  forall le ofs,
  exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.offset_ptr sp ofs) v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. unfold addrstack. TrivialExists. (*rewrite eval_Olea_ptr. apply eval_addressing_Ainstack.*)
Qed.

Theorem eval_notint: unary_constructor_sound notint Val.notint.
Proof.
(* Goal: unary_constructor_sound notint Val.notint *)
  unfold notint; red; intros until x. case (notint_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- rewrite Val.not_xor. rewrite Val.xor_assoc. TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Theorem eval_addimm:
  forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)).
Proof.
(* Goal: forall n : Int.int, unary_constructor_sound (addimm n) (fun x : val => Val.add x (Vint n)) *)
  red; unfold addimm; intros until x.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq n Int.zero then a else match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end) v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  predSpec Int.eq Int.eq_spec n Int.zero.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
- subst n. intros. exists x; split; auto.
(* Goal: Val.lessdef (Val.add x (Vint Int.zero)) x *)
  destruct x; simpl; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto.
- case (addimm_match a); intros; InvEval.
+ TrivialExists; simpl. rewrite Int.add_commut. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
+ inv H0. simpl in H6. TrivialExists. simpl.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  erewrite eval_offset_addressing_total_32 by eauto. rewrite Int.repr_signed; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
+ TrivialExists. simpl. rewrite Int.repr_signed; auto.
Qed.

Theorem eval_add: binary_constructor_sound add Val.add.
Proof.
  assert (A: forall x y, Int.repr (x + y) = Int.add (Int.repr x) (Int.repr y)).
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
(* Goal: forall (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), let (mode, args) := addressing chunk a in @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le args vl) (@eq (option val) (@eval_addressing fundef unit ge sp mode vl) (@Some val v))) *)
  { intros; apply Int.eqm_samerepr; auto with ints. }
  assert (B: forall id ofs n, Archi.ptr64 = false ->
             Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.repr n)) =
             Val.add (Genv.symbol_address ge id ofs) (Vint (Int.repr n))).
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int (Int.repr n)) by auto with ptrofs.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
    apply Genv.shift_symbol_address_32; auto. }
(* Goal: binary_constructor_sound mul Val.mul *)
  red; intros until y.
(* Goal: forall (_ : eval_expr ge sp e m le a x) (_ : eval_expr ge sp e m le b y), @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (add a b) v) (Val.lessdef (Val.add x y) v)) *)
  unfold add; case (add_match a b); intros; InvEval.
- rewrite Val.add_commut. apply eval_addimm; auto.
- apply eval_addimm; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite A, Val.add_permut_4. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite A, Val.add_assoc. decEq; decEq. rewrite Val.add_permut. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite A, Val.add_permut_4. rewrite <- Val.add_permut. rewrite <- Val.add_assoc. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite ! Val.add_assoc.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite (Val.add_commut v1). rewrite Val.add_permut. rewrite Val.add_assoc. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite Val.add_assoc. do 2 f_equal. apply Val.add_commut.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite !Val.add_assoc.
(* Goal: @eq (option val) (@Some val (Val.add y (Val.add (Val.mul v1 (Vint (Int.repr sc))) (Vint (Int.repr n))))) (@Some val (Val.add (Val.add (Val.mul v1 (Vint (Int.repr sc))) (Vint (Int.repr n))) y)) *)
  rewrite (Val.add_commut (Vint (Int.repr n1))). rewrite Val.add_permut. do 2 f_equal. apply Val.add_commut.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite Heqb0. rewrite B by auto. rewrite !Val.add_assoc.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite (Val.add_commut (Vint (Int.repr n2))). rewrite Val.add_permut. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite Val.add_permut. rewrite Val.add_assoc.
(* Goal: @eq (option val) (@Some val (Val.add v1 (Val.add y (Vint (Int.repr n))))) (@Some val (Val.add v1 (Val.add (Vint (Int.repr n)) y))) *)
    decEq; decEq. apply Val.add_commut.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite Val.add_assoc; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  unfold Val.add; destruct Archi.ptr64, x, y; auto.
  + rewrite Int.add_zero; auto.
  + rewrite Int.add_zero; auto.
  + rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto.
  + rewrite Ptrofs.add_assoc, Ptrofs.add_zero. auto.
Qed.

Theorem eval_sub: binary_constructor_sound sub Val.sub.
Proof.
(* Goal: binary_constructor_sound mul Val.mul *)
  red; intros until y.
(* Goal: forall (_ : eval_expr ge sp e m le a x) (_ : eval_expr ge sp e m le b y), @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (sub a b) v) (Val.lessdef (Val.sub x y) v)) *)
  unfold sub; case (sub_match a b); intros; InvEval.
- rewrite Val.sub_add_opp. apply eval_addimm; auto.
- rewrite Val.sub_add_l. rewrite Val.sub_add_r.
    rewrite Val.add_assoc. simpl. rewrite Int.add_commut. rewrite <- Int.sub_add_opp.
    replace (Int.repr (n1 - n2)) with (Int.sub (Int.repr n1) (Int.repr n2)).
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
    apply eval_addimm; EvalOp.
(* Goal: @eq Int.int (Int.neg (Int.repr n2)) (Int.repr (Z.opp n2)) *)
    apply Int.eqm_samerepr; auto with ints.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
- rewrite Val.sub_add_l. apply eval_addimm; EvalOp.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
- rewrite Val.sub_add_r. replace (Int.repr (-n2)) with (Int.neg (Int.repr n2)). apply eval_addimm; EvalOp.
(* Goal: @eq Int.int (Int.neg (Int.repr n2)) (Int.repr (Z.opp n2)) *)
    apply Int.eqm_samerepr; auto with ints.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Theorem eval_negint: unary_constructor_sound negint Val.neg.
Proof.
(* Goal: unary_constructor_sound cast16unsigned (Val.zero_ext (Zpos (xO (xO (xO (xO xH)))))) *)
  red; intros until x. unfold negint. case (negint_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Theorem eval_shlimm:
  forall n, unary_constructor_sound (fun a => shlimm a n)
                                    (fun x => Val.shl x (Vint n)).
Proof.
(* Goal: unary_constructor_sound cast16unsigned (Val.zero_ext (Zpos (xO (xO (xO (xO xH)))))) *)
  red; intros until x.  unfold shlimm.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq n Int.zero then a else match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end) v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  predSpec Int.eq Int.eq_spec n Int.zero.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl.
  destruct (shlimm_match a); intros; InvEval.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
- exists (Vint (Int.shl n1 n)); split. EvalOp.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  simpl. rewrite LT. auto.
- destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
+ exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct v1; simpl; auto.
  rewrite Heqb.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct (Int.ltu n Int.iwordsize) eqn:?; simpl; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (addimm (Int.repr (Z.sub n1 n2)) (Eop Osub (Econs t1 (Econs t2 Enil)))) v) (Val.lessdef (Val.add (Val.sub v1 v0) (Vint (Int.add (Int.neg (Int.repr n2)) (Int.repr n1)))) v)) *)
  rewrite Int.add_commut. rewrite Int.shl_shl; auto. rewrite Int.add_commut; auto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
+ TrivialExists. econstructor. EvalOp. simpl; eauto. constructor.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  simpl. auto.
- destruct (shift_is_scale n).
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
+ econstructor; split. EvalOp. simpl. eauto.
  rewrite ! Int.repr_unsigned.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct v1; simpl; auto. rewrite LT.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite Int.shl_mul. rewrite Int.mul_add_distr_l. rewrite (Int.shl_mul (Int.repr n1)). auto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
+ TrivialExists. econstructor. EvalOp. simpl; eauto. constructor. auto.
- destruct (shift_is_scale n).
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
+ econstructor; split. EvalOp. simpl. eauto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct x; simpl; auto. rewrite LT.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite Int.repr_unsigned. rewrite Int.add_zero. rewrite Int.shl_mul. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
+ TrivialExists.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
- intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  auto.
Qed.

Theorem eval_shruimm:
  forall n, unary_constructor_sound (fun a => shruimm a n)
                                    (fun x => Val.shru x (Vint n)).
Proof.
(* Goal: unary_constructor_sound cast16unsigned (Val.zero_ext (Zpos (xO (xO (xO (xO xH)))))) *)
  red; intros until x.  unfold shruimm.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq n Int.zero then a else match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end) v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  predSpec Int.eq Int.eq_spec n Int.zero.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl.
  destruct (shruimm_match a); intros; InvEval.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
- exists (Vint (Int.shru n1 n)); split. EvalOp.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  simpl. rewrite LT; auto.
- destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
+ exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  subst. destruct v1; simpl; auto.
  rewrite Heqb.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (addimm (Int.repr (Z.sub n1 n2)) (Eop Osub (Econs t1 (Econs t2 Enil)))) v) (Val.lessdef (Val.add (Val.sub v1 v0) (Vint (Int.add (Int.neg (Int.repr n2)) (Int.repr n1)))) v)) *)
  rewrite LT. rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
+ TrivialExists. econstructor. EvalOp. simpl; eauto. constructor.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  simpl. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
- intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  auto.
Qed.

Theorem eval_shrimm:
  forall n, unary_constructor_sound (fun a => shrimm a n)
                                    (fun x => Val.shr x (Vint n)).
Proof.
(* Goal: unary_constructor_sound cast16unsigned (Val.zero_ext (Zpos (xO (xO (xO (xO xH)))))) *)
  red; intros until x.  unfold shrimm.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq n Int.zero then a else match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end) v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  predSpec Int.eq Int.eq_spec n Int.zero.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl.
  destruct (shrimm_match a); intros; InvEval.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
- exists (Vint (Int.shr n1 n)); split. EvalOp.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  simpl. rewrite LT; auto.
- destruct (Int.ltu (Int.add n n1) Int.iwordsize) eqn:?.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
+ exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  subst. destruct v1; simpl; auto.
  rewrite Heqb.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct (Int.ltu n1 Int.iwordsize) eqn:?; simpl; auto.
  rewrite LT.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (addimm (Int.repr (Z.sub n1 n2)) (Eop Osub (Econs t1 (Econs t2 Enil)))) v) (Val.lessdef (Val.add (Val.sub v1 v0) (Vint (Int.add (Int.neg (Int.repr n2)) (Int.repr n1)))) v)) *)
  rewrite Int.add_commut. rewrite Int.shr_shr; auto. rewrite Int.add_commut; auto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
+ TrivialExists. econstructor. EvalOp. simpl; eauto. constructor.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  simpl. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
- intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  auto.
Qed.

Lemma eval_mulimm_base:
  forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)).
Proof.
  intros; red; intros; unfold mulimm_base.
  generalize (Int.one_bits_decomp n) (Int.one_bits_range n); intros D R.
  destruct (Int.one_bits n) as [ | i l].
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
  destruct l as [ | j l ].
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  replace (Val.mul x (Vint n)) with (Val.shl x (Vint i)). apply eval_shlimm; auto.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  destruct x; auto; simpl. rewrite D; simpl; rewrite Int.add_zero.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite R by auto with coqlib. rewrite Int.shl_mul. auto.
  destruct l as [ | k l ].
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exploit (eval_shlimm i (x :: le) (Eletvar 0) x). constructor; auto. intros [v1 [A1 B1]].
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exploit (eval_shlimm j (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]].
  exploit eval_add. eexact A1. eexact A2. intros [v3 [A3 B3]].
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exists v3; split. econstructor; eauto.
  rewrite D; simpl; rewrite Int.add_zero.
  replace (Vint (Int.add (Int.shl Int.one i) (Int.shl Int.one j)))
     with (Val.add (Val.shl Vone (Vint i)) (Val.shl Vone (Vint j))).
  rewrite Val.mul_add_distr_r.
  repeat rewrite Val.shl_mul.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  apply Val.lessdef_trans with (Val.add v1 v2); auto. apply Val.add_lessdef; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  simpl. rewrite ! R by auto with coqlib. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
Qed.

Theorem eval_mulimm:
  forall n, unary_constructor_sound (mulimm n) (fun x => Val.mul x (Vint n)).
Proof.
  intros; red; intros until x; unfold mulimm.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq n Int.zero then a else match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end) v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  predSpec Int.eq Int.eq_spec n Int.zero.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. exists (Vint Int.zero); split. EvalOp.
(* Goal: Val.lessdef (Vint (Int.xor i n)) (Vint i) *)
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  destruct x; simpl; auto. subst n. rewrite Int.mul_zero. auto.
  predSpec Int.eq Int.eq_spec n Int.one.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. exists x; split; auto.
(* Goal: Val.lessdef (Vint (Int.xor i n)) (Vint i) *)
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  destruct x; simpl; auto. subst n. rewrite Int.mul_one. auto.
- case (mulimm_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
+ TrivialExists. simpl. rewrite Int.mul_commut; auto.
+ rewrite Val.mul_add_distr_l.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exploit eval_mulimm_base; eauto. instantiate (1 := n). intros [v' [A1 B1]].
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exploit (eval_addimm (Int.mul n (Int.repr n2)) le (mulimm_base n t2) v'). auto. intros [v'' [A2 B2]].
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.add_lessdef; eauto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite Val.mul_commut; auto.
+ apply eval_mulimm_base; auto.
Qed.

Theorem eval_mul: binary_constructor_sound mul Val.mul.
Proof.
(* Goal: binary_constructor_sound mul Val.mul *)
  red; intros until y.
(* Goal: forall (_ : eval_expr ge sp e m le a x) (_ : eval_expr ge sp e m le b y), @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (mul a b) v) (Val.lessdef (Val.mul x y) v)) *)
  unfold mul; case (mul_match a b); intros; InvEval.
- rewrite Val.mul_commut. apply eval_mulimm. auto.
- apply eval_mulimm. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Theorem eval_mulhs: binary_constructor_sound mulhs Val.mulhs.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  unfold mulhs; red; intros; TrivialExists.
Qed.
  
Theorem eval_mulhu: binary_constructor_sound mulhu Val.mulhu.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  unfold mulhu; red; intros; TrivialExists.
Qed.
  
Theorem eval_andimm:
  forall n, unary_constructor_sound (andimm n) (fun x => Val.and x (Vint n)).
Proof.
(* Goal: unary_constructor_sound cast16unsigned (Val.zero_ext (Zpos (xO (xO (xO (xO xH)))))) *)
  intros; red; intros until x. unfold andimm.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq n Int.zero then a else match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end) v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  predSpec Int.eq Int.eq_spec n Int.zero.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. exists (Vint Int.zero); split. EvalOp.
(* Goal: Val.lessdef (Vint (Int.xor i n)) (Vint i) *)
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  destruct x; simpl; auto. subst n. rewrite Int.and_zero. auto.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq n Int.mone then Eop (Ointconst Int.mone) Enil else match orimm_match a with | orimm_case1 n2 => Eop (Ointconst (Int.or n n2)) Enil | orimm_case2 n2 t2 => Eop (Oorimm (Int.or n n2)) (Econs t2 Enil) | orimm_default e2 => Eop (Oorimm n) (Econs e2 Enil) end) v) (Val.lessdef (Val.or x (Vint n)) v)) *)
  predSpec Int.eq Int.eq_spec n Int.mone.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. exists x; split; auto.
(* Goal: Val.lessdef (Vint (Int.xor i n)) (Vint i) *)
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  destruct x; simpl; auto. subst n. rewrite Int.and_mone. auto.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le match andimm_match a with | andimm_case1 n2 => Eop (Ointconst (Int.and n n2)) Enil | andimm_case2 n2 t2 => Eop (Oandimm (Int.and n n2)) (Econs t2 Enil) | andimm_case3 t2 => Eop (Oandimm (Int.and n (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI xH))))))))))) (Econs t2 Enil) | andimm_case4 t2 => Eop (Oandimm (Int.and n (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))))) (Econs t2 Enil) | andimm_default e2 => Eop (Oandimm n) (Econs e2 Enil) end v) (Val.lessdef (Val.and x (Vint n)) v)) *)
  case (andimm_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite Int.and_commut; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite Val.and_assoc. rewrite Int.and_commut. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite Int.and_commut. auto. compute; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite Int.and_commut. auto. compute; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Theorem eval_and: binary_constructor_sound and Val.and.
Proof.
(* Goal: binary_constructor_sound and Val.and *)
  red; intros until y; unfold and; case (and_match a b); intros; InvEval.
- rewrite Val.and_commut. apply eval_andimm; auto.
- apply eval_andimm; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Theorem eval_orimm:
  forall n, unary_constructor_sound (orimm n) (fun x => Val.or x (Vint n)).
Proof.
(* Goal: unary_constructor_sound cast16unsigned (Val.zero_ext (Zpos (xO (xO (xO (xO xH)))))) *)
  intros; red; intros until x. unfold orimm.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq n Int.zero then a else match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end) v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  predSpec Int.eq Int.eq_spec n Int.zero.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. exists x; split. auto.
(* Goal: Val.lessdef (Vint (Int.xor i n)) (Vint i) *)
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  destruct x; simpl; auto. subst n. rewrite Int.or_zero. auto.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq n Int.mone then Eop (Ointconst Int.mone) Enil else match orimm_match a with | orimm_case1 n2 => Eop (Ointconst (Int.or n n2)) Enil | orimm_case2 n2 t2 => Eop (Oorimm (Int.or n n2)) (Econs t2 Enil) | orimm_default e2 => Eop (Oorimm n) (Econs e2 Enil) end) v) (Val.lessdef (Val.or x (Vint n)) v)) *)
  predSpec Int.eq Int.eq_spec n Int.mone.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. exists (Vint Int.mone); split. EvalOp.
(* Goal: Val.lessdef (Vint (Int.xor i n)) (Vint i) *)
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  destruct x; simpl; auto. subst n. rewrite Int.or_mone. auto.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le match orimm_match a with | orimm_case1 n2 => Eop (Ointconst (Int.or n n2)) Enil | orimm_case2 n2 t2 => Eop (Oorimm (Int.or n n2)) (Econs t2 Enil) | orimm_default e2 => Eop (Oorimm n) (Econs e2 Enil) end v) (Val.lessdef (Val.or x (Vint n)) v)) *)
  destruct (orimm_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite Int.or_commut; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
- subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Remark eval_same_expr:
  forall a1 a2 le v1 v2,
  same_expr_pure a1 a2 = true ->
  eval_expr ge sp e m le a1 v1 ->
  eval_expr ge sp e m le a2 v2 ->
  a1 = a2 /\ v1 = v2.
Proof.
(* Goal: forall (a1 a2 : expr) (le : letenv) (v1 v2 : val) (_ : @eq bool (same_expr_pure a1 a2) true) (_ : eval_expr ge sp e m le a1 v1) (_ : eval_expr ge sp e m le a2 v2), Logic.and (@eq expr a1 a2) (@eq val v1 v2) *)
  intros until v2.
(* Goal: forall (_ : @eq bool (same_expr_pure a1 a2) true) (_ : eval_expr ge sp e m le a1 v1) (_ : eval_expr ge sp e m le a2 v2), Logic.and (@eq expr a1 a2) (@eq val v1 v2) *)
  destruct a1; simpl; try (intros; discriminate).
(* Goal: forall (_ : @eq bool match a2 with | Evar v2 => if ident_eq i v2 then true else false | Eop o e => false | Eload m a e => false | Econdition c e e0 => false | Elet e e0 => false | Eletvar n => false | Ebuiltin e e0 => false | Eexternal i s e => false end true) (_ : eval_expr ge sp e m le (Evar i) v1) (_ : eval_expr ge sp e m le a2 v2), Logic.and (@eq expr (Evar i) a2) (@eq val v1 v2) *)
  destruct a2; simpl; try (intros; discriminate).
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  case (ident_eq i i0); intros.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  subst i0. inversion H0. inversion H1. split. auto. congruence.
(* Goal: Logic.and (@eq expr (Evar i) (Evar i0)) (@eq val v1 v2) *)
  discriminate.
Qed.

Remark int_add_sub_eq:
  forall x y z, Int.add x y = z -> Int.sub z x = y.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. subst z. rewrite Int.sub_add_l. rewrite Int.sub_idem. apply Int.add_zero_l.
Qed.

Lemma eval_or: binary_constructor_sound or Val.or.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  red; intros until y; unfold or; case (or_match a b); intros.
  (* intconst *)
- InvEval. rewrite Val.or_commut. apply eval_orimm; auto.
- InvEval. apply eval_orimm; auto.
- (* shlimm - shruimm *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq (Int.add n1 n2) Int.iwordsize then if same_expr_pure t1 t2 then Eop (Ororimm n2) (Econs t1 Enil) else Eop (Oshldimm n1) (Econs t1 (Econs t2 Enil)) else Eop Oor (Econs (Eop (Oshruimm n2) (Econs t2 Enil)) (Econs (Eop (Oshlimm n1) (Econs t1 Enil)) Enil))) v) (Val.lessdef (Val.or x y) v)) *)
  predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if same_expr_pure t1 t2 then Eop (Ororimm n2) (Econs t1 Enil) else Eop (Oshldimm n1) (Econs t1 (Econs t2 Enil))) v) (Val.lessdef (Val.or x y) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Oor (Econs (Eop (Oshruimm n2) (Econs t2 Enil)) (Econs (Eop (Oshlimm n1) (Econs t1 Enil)) Enil))) v) (Val.lessdef (Val.or x y) v)) *)
  destruct (same_expr_pure t1 t2) eqn:?.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  exists (Val.ror v0 (Vint n2)); split. EvalOp.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct v0; simpl; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto.
  simpl. rewrite <- Int.or_ror; auto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  InvEval. econstructor; split; eauto. EvalOp.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  simpl. erewrite int_add_sub_eq; eauto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
- (* shruimm - shlimm *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq (Int.add n1 n2) Int.iwordsize then if same_expr_pure t1 t2 then Eop (Ororimm n2) (Econs t1 Enil) else Eop (Oshldimm n1) (Econs t1 (Econs t2 Enil)) else Eop Oor (Econs (Eop (Oshruimm n2) (Econs t2 Enil)) (Econs (Eop (Oshlimm n1) (Econs t1 Enil)) Enil))) v) (Val.lessdef (Val.or x y) v)) *)
  predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if same_expr_pure t1 t2 then Eop (Ororimm n2) (Econs t1 Enil) else Eop (Oshldimm n1) (Econs t1 (Econs t2 Enil))) v) (Val.lessdef (Val.or x y) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Oor (Econs (Eop (Oshruimm n2) (Econs t2 Enil)) (Econs (Eop (Oshlimm n1) (Econs t1 Enil)) Enil))) v) (Val.lessdef (Val.or x y) v)) *)
  destruct (same_expr_pure t1 t2) eqn:?.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  exists (Val.ror v1 (Vint n2)); split. EvalOp.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct v1; simpl; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto.
  simpl. rewrite Int.or_commut. rewrite <- Int.or_ror; auto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  InvEval. econstructor; split; eauto. EvalOp.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  simpl. erewrite int_add_sub_eq; eauto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite Val.or_commut; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
- (* default *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
Qed.

Theorem eval_xorimm:
  forall n, unary_constructor_sound (xorimm n) (fun x => Val.xor x (Vint n)).
Proof.
(* Goal: unary_constructor_sound cast16unsigned (Val.zero_ext (Zpos (xO (xO (xO (xO xH)))))) *)
  intros; red; intros until x. unfold xorimm.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq n Int.zero then a else match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end) v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  predSpec Int.eq Int.eq_spec n Int.zero.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. exists x; split. auto.
(* Goal: Val.lessdef (Vint (Int.xor i n)) (Vint i) *)
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (shruimm a n2) v) (Val.lessdef (Val.shru x y) v)) *)
  destruct (xorimm_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists. simpl. rewrite Int.xor_commut; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists.
- rewrite Val.not_xor. rewrite Val.xor_assoc.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  rewrite (Val.xor_commut (Vint Int.mone)). TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Theorem eval_xor: binary_constructor_sound xor Val.xor.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (shruimm a n2) v) (Val.lessdef (Val.shru x y) v)) *)
  red; intros until y; unfold xor; case (xor_match a b); intros; InvEval.
- rewrite Val.xor_commut. apply eval_xorimm; auto.
- apply eval_xorimm; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Theorem eval_divs_base:
  forall le a b x y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.divs x y = Some z ->
  exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. unfold divs_base. exists z; split. EvalOp. auto.
Qed.

Theorem eval_divu_base:
  forall le a b x y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.divu x y = Some z ->
  exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. unfold divu_base. exists z; split. EvalOp. auto.
Qed.

Theorem eval_mods_base:
  forall le a b x y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.mods x y = Some z ->
  exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. unfold mods_base. exists z; split. EvalOp. auto.
Qed.

Theorem eval_modu_base:
  forall le a b x y z,
  eval_expr ge sp e m le a x ->
  eval_expr ge sp e m le b y ->
  Val.modu x y = Some z ->
  exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. unfold modu_base. exists z; split. EvalOp. auto.
Qed.

Theorem eval_shrximm:
  forall le a n x z,
  eval_expr ge sp e m le a x ->
  Val.shrx x (Vint n) = Some z ->
  exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. unfold shrximm.
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (if Int.eq n Int.zero then a else match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end) v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  predSpec Int.eq Int.eq_spec n Int.zero.
(* Goal: Val.lessdef (Vint (Int.xor i n)) (Vint i) *)
(* Goal: forall _ : eval_expr ge sp e m le a x, @ex val (fun v : val => Logic.and (eval_expr ge sp e m le match xorimm_match a with | xorimm_case1 n2 => Eop (Ointconst (Int.xor n n2)) Enil | xorimm_case2 n2 t2 => Eop (Oxorimm (Int.xor n n2)) (Econs t2 Enil) | xorimm_case3 t2 => Eop (Oxorimm (Int.not n)) (Econs t2 Enil) | xorimm_default e2 => Eop (Oxorimm n) (Econs e2 Enil) end v) (Val.lessdef (Val.xor x (Vint n)) v)) *)
  subst n. exists x; split; auto.
(* Goal: Logic.and (@eq expr (Evar i) (Evar i0)) (@eq val v1 v2) *)
  destruct x; simpl in H0; try discriminate.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop (Olea (offset_addressing_total addr (Int.signed n))) args) v) (Val.lessdef (Val.add x (Vint n)) v)) *)
  destruct (Int.ltu Int.zero (Int.repr 31)); inv H0.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  replace (Int.shrx i Int.zero) with i. auto.
  unfold Int.shrx, Int.divs. rewrite Int.shl_zero.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  econstructor; split. EvalOp. auto.
Qed.

Theorem eval_shl: binary_constructor_sound shl Val.shl.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  red; intros until y; unfold shl; case (shl_match b); intros.
- InvEval. apply eval_shlimm; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Theorem eval_shr: binary_constructor_sound shr Val.shr.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  red; intros until y; unfold shr; case (shr_match b); intros.
- InvEval. apply eval_shrimm; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Theorem eval_shru: binary_constructor_sound shru Val.shru.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  red; intros until y; unfold shru; case (shru_match b); intros.
- InvEval. apply eval_shruimm; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
- TrivialExists.
Qed.

Theorem eval_negf: unary_constructor_sound negf Val.negf.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  red; intros. TrivialExists.
Qed.

Theorem eval_absf: unary_constructor_sound absf Val.absf.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  red; intros. TrivialExists.
Qed.

Theorem eval_addf: binary_constructor_sound addf Val.addf.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  red; intros; TrivialExists.
Qed.

Theorem eval_subf: binary_constructor_sound subf Val.subf.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  red; intros; TrivialExists.
Qed.

Theorem eval_mulf: binary_constructor_sound mulf Val.mulf.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  red; intros; TrivialExists.
Qed.

Theorem eval_negfs: unary_constructor_sound negfs Val.negfs.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  red; intros. TrivialExists.
Qed.

Theorem eval_absfs: unary_constructor_sound absfs Val.absfs.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  red; intros. TrivialExists.
Qed.

Theorem eval_addfs: binary_constructor_sound addfs Val.addfs.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  red; intros; TrivialExists.
Qed.

Theorem eval_subfs: binary_constructor_sound subfs Val.subfs.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  red; intros; TrivialExists.
Qed.

Theorem eval_mulfs: binary_constructor_sound mulfs Val.mulfs.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  red; intros; TrivialExists.
Qed.

Section COMP_IMM.

Variable default: comparison -> int -> condition.
Variable intsem: comparison -> int -> int -> bool.
Variable sem: comparison -> val -> val -> val.

Hypothesis sem_int: forall c x y, sem c (Vint x) (Vint y) = Val.of_bool (intsem c x y).
Hypothesis sem_undef: forall c v, sem c Vundef v = Vundef.
Hypothesis sem_eq: forall x y, sem Ceq (Vint x) (Vint y) = Val.of_bool (Int.eq x y).
Hypothesis sem_ne: forall x y, sem Cne (Vint x) (Vint y) = Val.of_bool (negb (Int.eq x y)).
Hypothesis sem_default: forall c v n, sem c v (Vint n) = Val.of_optbool (eval_condition (default c n) (v :: nil) m).

Lemma eval_compimm:
  forall le c a n2 x,
  eval_expr ge sp e m le a x ->
  exists v, eval_expr ge sp e m le (compimm default intsem c a n2) v
         /\ Val.lessdef (sem c x (Vint n2)) v.
Proof.
  intros until x.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  unfold compimm; case (compimm_match c a); intros.
- (* constant *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  InvEval. rewrite sem_int. TrivialExists. simpl. destruct (intsem c0 n1 n2); auto.
- (* eq cmp *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (shruimm a n2) v) (Val.lessdef (Val.shru x y) v)) *)
  InvEval. inv H. simpl in H5. inv H5.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  simpl. rewrite eval_negate_condition.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  destruct (eval_condition c0 vl m); simpl.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite sem_undef; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  destruct (Int.eq_dec n2 Int.one). subst n2. TrivialExists.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  simpl. destruct (eval_condition c0 vl m); simpl.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_eq; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite sem_undef; auto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  exists (Vint Int.zero); split. EvalOp.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  destruct (eval_condition c0 vl m); simpl.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  unfold Vtrue, Vfalse. destruct b; rewrite sem_eq; rewrite Int.eq_false; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite sem_undef; auto.
- (* ne cmp *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (shruimm a n2) v) (Val.lessdef (Val.shru x y) v)) *)
  InvEval. inv H. simpl in H5. inv H5.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  destruct (Int.eq_dec n2 Int.zero). subst n2. TrivialExists.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  simpl. destruct (eval_condition c0 vl m); simpl.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite sem_undef; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  destruct (Int.eq_dec n2 Int.one). subst n2. TrivialExists.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  simpl. rewrite eval_negate_condition. destruct (eval_condition c0 vl m); simpl.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  unfold Vtrue, Vfalse. destruct b; simpl; rewrite sem_ne; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite sem_undef; auto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  exists (Vint Int.one); split. EvalOp.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  destruct (eval_condition c0 vl m); simpl.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  unfold Vtrue, Vfalse. destruct b; rewrite sem_ne; rewrite Int.eq_false; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite sem_undef; auto.
- (* eq andimm *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  destruct (Int.eq_dec n2 Int.zero). InvEval; subst.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  econstructor; split. EvalOp. simpl; eauto.
  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_eq.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct (Int.eq (Int.and i n1) Int.zero); auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists. simpl. rewrite sem_default. auto.
- (* ne andimm *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  destruct (Int.eq_dec n2 Int.zero). InvEval; subst.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  econstructor; split. EvalOp. simpl; eauto.
  destruct v1; simpl; try (rewrite sem_undef; auto). rewrite sem_ne.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  destruct (Int.eq (Int.and i n1) Int.zero); auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists. simpl. rewrite sem_default. auto.
- (* default *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists. simpl. rewrite sem_default. auto.
Qed.

Hypothesis sem_swap:
  forall c x y, sem (swap_comparison c) x y = sem c y x.

Lemma eval_compimm_swap:
  forall le c a n2 x,
  eval_expr ge sp e m le a x ->
  exists v, eval_expr ge sp e m le (compimm default intsem (swap_comparison c) a n2) v
         /\ Val.lessdef (sem c (Vint n2) x) v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. rewrite <- sem_swap. eapply eval_compimm; eauto.
Qed.

End COMP_IMM.

Theorem eval_comp:
  forall c, binary_constructor_sound (comp c) (Val.cmp c).
Proof.
(* Goal: binary_constructor_sound mul Val.mul *)
  intros; red; intros until y. unfold comp; case (comp_match a b); intros; InvEval.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  eapply eval_compimm_swap; eauto.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. unfold Val.cmp. rewrite Val.swap_cmp_bool; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  eapply eval_compimm; eauto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
Qed.

Theorem eval_compu:
  forall c, binary_constructor_sound (compu c) (Val.cmpu (Mem.valid_pointer m) c).
Proof.
(* Goal: binary_constructor_sound mul Val.mul *)
  intros; red; intros until y. unfold compu; case (compu_match a b); intros; InvEval.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  eapply eval_compimm_swap; eauto.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. unfold Val.cmpu. rewrite Val.swap_cmpu_bool; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  eapply eval_compimm; eauto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
Qed.

Theorem eval_compf:
  forall c, binary_constructor_sound (compf c) (Val.cmpf c).
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros; red; intros. unfold compf. TrivialExists.
Qed.

Theorem eval_compfs:
  forall c, binary_constructor_sound (compfs c) (Val.cmpfs c).
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros; red; intros. unfold compfs. TrivialExists.
Qed.

Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
Proof.
(* Goal: unary_constructor_sound cast16unsigned (Val.zero_ext (Zpos (xO (xO (xO (xO xH)))))) *)
  red; intros until x. unfold cast8signed. case (cast8signed_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
Qed.

Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8).
Proof.
(* Goal: unary_constructor_sound cast16unsigned (Val.zero_ext (Zpos (xO (xO (xO (xO xH)))))) *)
  red; intros until x. unfold cast8unsigned. destruct (cast8unsigned_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite Int.and_commut. apply eval_andimm; auto. compute; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
Qed.

Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16).
Proof.
(* Goal: unary_constructor_sound cast16unsigned (Val.zero_ext (Zpos (xO (xO (xO (xO xH)))))) *)
  red; intros until x. unfold cast16signed. case (cast16signed_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
Qed.

Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16).
Proof.
(* Goal: unary_constructor_sound cast16unsigned (Val.zero_ext (Zpos (xO (xO (xO (xO xH)))))) *)
  red; intros until x. unfold cast16unsigned. destruct (cast16unsigned_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (andimm (Int.and (Int.repr (Zpos (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI (xI xH))))))))))))))))) n) t) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) (Val.and v1 (Vint n))) v)) *)
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Ocast16unsigned (Econs e0 Enil)) v) (Val.lessdef (Val.zero_ext (Zpos (xO (xO (xO (xO xH))))) x) v)) *)
  subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite Int.and_commut. apply eval_andimm; auto. compute; auto.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
Qed.

Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  red; intros. unfold singleoffloat. TrivialExists.
Qed.

Theorem eval_floatofsingle: unary_constructor_sound floatofsingle Val.floatofsingle.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  red; intros. unfold floatofsingle. TrivialExists.
Qed.

Theorem eval_intoffloat:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.intoffloat x = Some y ->
  exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  intros; unfold intoffloat. TrivialExists.
Qed.

Theorem eval_floatofint:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.floatofint x = Some y ->
  exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (shruimm a n2) v) (Val.lessdef (Val.shru x y) v)) *)
  intros until y; unfold floatofint. case (floatofint_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
Qed.

Theorem eval_intuoffloat:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.intuoffloat x = Some y ->
  exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. destruct x; simpl in H0; try discriminate.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop (Olea (offset_addressing_total addr (Int.signed n))) args) v) (Val.lessdef (Val.add x (Vint n)) v)) *)
  destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exists (Vint n); split; auto. unfold intuoffloat.
  set (im := Int.repr Int.half_modulus).
  set (fm := Float.of_intu im).
  assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)).
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
    constructor. auto.
  assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar O) (Vfloat fm)).
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
    constructor. auto.
  econstructor. eauto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  econstructor. instantiate (1 := Vfloat fm). EvalOp.
  eapply eval_Econdition with (va := Float.cmp Clt f fm).
  eauto with evalexpr.
  destruct (Float.cmp Clt f fm) eqn:?.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exploit Float.to_intu_to_int_1; eauto. intro EQ.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  EvalOp. simpl. rewrite EQ; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exploit Float.to_intu_to_int_2; eauto.
  change Float.ox8000_0000 with im. fold fm. intro EQ.
  set (t2 := subf (Eletvar (S O)) (Eletvar O)).
  set (t3 := intoffloat t2).
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exploit (eval_subf (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f) (Eletvar O)); eauto.
  fold t2. intros [v2 [A2 B2]]. simpl in B2. inv B2.
  exploit (eval_addimm Float.ox8000_0000 (Vfloat fm :: Vfloat f :: le) t3).
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
    unfold t3. unfold intoffloat. EvalOp. simpl. rewrite EQ. simpl. eauto.
  intros [v4 [A4 B4]]. simpl in B4. inv B4.
  rewrite Int.sub_add_opp in A4. rewrite Int.add_assoc in A4.
  rewrite (Int.add_commut (Int.neg im)) in A4.
  rewrite Int.add_neg_zero in A4.
  rewrite Int.add_zero in A4.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  auto.
Qed.

Theorem eval_floatofintu:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.floatofintu x = Some y ->
  exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros until y; unfold floatofintu. case (floatofintu_match a); intros.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  InvEval. TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop (Olea (offset_addressing_total addr (Int.signed n))) args) v) (Val.lessdef (Val.add x (Vint n)) v)) *)
  destruct x; simpl in H0; try discriminate. inv H0.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exists (Vfloat (Float.of_intu i)); split; auto.
  econstructor. eauto.
  set (fm := Float.of_intu Float.ox8000_0000).
  assert (eval_expr ge sp e m (Vint i :: le) (Eletvar O) (Vint i)).
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
    constructor. auto.
  eapply eval_Econdition with (va := Int.ltu i Float.ox8000_0000).
  eauto with evalexpr.
  destruct (Int.ltu i Float.ox8000_0000) eqn:?.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite Float.of_intu_of_int_1; auto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  unfold floatofint. EvalOp.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exploit (eval_addimm (Int.neg Float.ox8000_0000) (Vint i :: le) (Eletvar 0)); eauto.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  simpl. intros [v [A B]]. inv B.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  unfold addf. EvalOp.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  constructor. unfold floatofint. EvalOp. simpl; eauto.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  constructor. EvalOp. simpl; eauto. constructor. simpl; eauto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  fold fm. rewrite Float.of_intu_of_int_2; auto.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite Int.sub_add_opp. auto.
Qed.

Theorem eval_intofsingle:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.intofsingle x = Some y ->
  exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  intros; unfold intofsingle. TrivialExists.
Qed.

Theorem eval_singleofint:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.singleofint x = Some y ->
  exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (shruimm a n2) v) (Val.lessdef (Val.shru x y) v)) *)
  intros until y; unfold singleofint. case (singleofint_match a); intros; InvEval.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  TrivialExists.
Qed.

Theorem eval_intuofsingle:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.intuofsingle x = Some y ->
  exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros. destruct x; simpl in H0; try discriminate.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop (Olea (offset_addressing_total addr (Int.signed n))) args) v) (Val.lessdef (Val.add x (Vint n)) v)) *)
  destruct (Float32.to_intu f) as [n|] eqn:?; simpl in H0; inv H0.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (intuofsingle a) v) (Val.lessdef (Vint n) v)) *)
  unfold intuofsingle. apply eval_intuoffloat with (Vfloat (Float.of_single f)).
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  unfold floatofsingle. EvalOp.
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  simpl. change (Float.of_single f) with (Float32.to_double f).
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  erewrite Float32.to_intu_double; eauto. auto.
Qed.

Theorem eval_singleofintu:
  forall le a x y,
  eval_expr ge sp e m le a x ->
  Val.singleofintu x = Some y ->
  exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v.
Proof.
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  intros until y; unfold singleofintu. case (singleofintu_match a); intros.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop Osingleofint (Econs e0 Enil)) v) (Val.lessdef y v)) *)
  InvEval. TrivialExists.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (Eop (Olea (offset_addressing_total addr (Int.signed n))) args) v) (Val.lessdef (Val.add x (Vint n)) v)) *)
  destruct x; simpl in H0; try discriminate. inv H0.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exploit eval_floatofintu. eauto. simpl. reflexivity.
  intros (v & A & B).
(* Goal: Logic.and (@eq expr (Evar i) (Evar i)) (@eq val v1 v2) *)
(* Goal: Logic.and (@eq expr (Evar i) (Evar i0)) (@eq val v1 v2) *)
  exists (Val.singleoffloat v); split.
(* Goal: eval_expr ge sp e m le (Eop Ofloatofsingle (Econs a Enil)) (Vfloat (Float.of_single f)) *)
(* Goal: @eq (option val) (Val.intuoffloat (Vfloat (Float.of_single f))) (@Some val (Vint n)) *)
  unfold singleoffloat; EvalOp.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  inv B; simpl. rewrite Float32.of_intu_double. auto.
Qed.

Theorem eval_addressing:
  forall le chunk a v b ofs,
  eval_expr ge sp e m le a v ->
  v = Vptr b ofs ->
  match addressing chunk a with (mode, args) =>
    exists vl,
    eval_exprlist ge sp e m le args vl /\
    eval_addressing ge sp mode vl = Some v
  end.
Proof.
(* Goal: forall (le : letenv) (chunk : memory_chunk) (a : expr) (v : val) (b : block) (ofs : Ptrofs.int) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), let (mode, args) := addressing chunk a in @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le args vl) (@eq (option val) (@eval_addressing fundef unit ge sp mode vl) (@Some val v))) *)
  intros until ofs.
  assert (A: v = Vptr b ofs -> eval_addressing ge sp (Aindexed 0) (v :: nil) = Some v).
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  { intros. subst v. unfold eval_addressing.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
    destruct Archi.ptr64 eqn:SF; simpl; rewrite SF; rewrite Ptrofs.add_zero; auto. }
  assert (D: forall a,
             eval_expr ge sp e m le a v ->
             v = Vptr b ofs ->
             exists vl, eval_exprlist ge sp e m le (a ::: Enil) vl
                     /\ eval_addressing ge sp (Aindexed 0) vl = Some v).
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  { intros. exists (v :: nil); split. constructor; auto. constructor. auto. }
(* Goal: forall (a : expr) (_ : eval_expr ge sp e m le a v) (_ : @eq val v (Vptr b ofs)), @ex (list val) (fun vl : list val => Logic.and (eval_exprlist ge sp e m le (Econs a Enil) vl) (@eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) vl) (@Some val v))) *)
  unfold addressing; case (addressing_match a); intros.
- destruct (negb Archi.ptr64 && addressing_valid addr) eqn:E.
+ inv H. InvBooleans. apply negb_true_iff in H. unfold eval_addressing; rewrite H.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exists vl; auto.
+ apply D; auto.
- destruct (Archi.ptr64 && addressing_valid addr) eqn:E.
+ inv H. InvBooleans. unfold eval_addressing; rewrite H.
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  exists vl; auto.
+ apply D; auto.
- apply D; auto.
Qed.

Theorem eval_builtin_arg_addr:
  forall addr al vl v,
  eval_exprlist ge sp e m nil al vl ->
  Op.eval_addressing ge sp addr vl = Some v ->
  CminorSel.eval_builtin_arg ge sp e m (builtin_arg_addr addr al) v.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (shruimm a n2) v) (Val.lessdef (Val.shru x y) v)) *)
  intros until v. unfold builtin_arg_addr; case (builtin_arg_addr_match addr al); intros; InvEval.
- set (v2 := if Archi.ptr64 then Vlong (Int64.repr n) else Vint (Int.repr n)).
  assert (EQ: v = if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2).
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  { unfold Op.eval_addressing in H0; unfold v2; destruct Archi.ptr64; simpl in H0; inv H0; auto. }
(* Goal: @eq (option val) (@eval_addressing fundef unit ge sp (Aindexed Z0) (@cons val v (@nil val))) (@Some val v) *)
  rewrite EQ. constructor. constructor; auto. unfold v2; destruct Archi.ptr64; constructor.
- rewrite eval_addressing_Aglobal in H0. inv H0. constructor.
- rewrite eval_addressing_Ainstack in H0. inv H0. constructor.
- constructor. econstructor. eauto. rewrite eval_Olea_ptr. auto. 
Qed. 

Theorem eval_builtin_arg:
  forall a v,
  eval_expr ge sp e m nil a v ->
  CminorSel.eval_builtin_arg ge sp e m (builtin_arg a) v.
Proof.
(* Goal: @ex val (fun v : val => Logic.and (eval_expr ge sp e m le (shruimm a n2) v) (Val.lessdef (Val.shru x y) v)) *)
  intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval.
- constructor.
- constructor.
- destruct Archi.ptr64 eqn:SF. 
+ constructor; auto.
+ inv H. eapply eval_builtin_arg_addr. eauto. unfold Op.eval_addressing; rewrite SF; assumption.
- destruct Archi.ptr64 eqn:SF. 
+ inv H. eapply eval_builtin_arg_addr. eauto. unfold Op.eval_addressing; rewrite SF; assumption.
+ constructor; auto.
- simpl in H5. inv H5. constructor.
- constructor; auto.
- inv H. InvEval. rewrite eval_addressing_Aglobal in H6. inv H6. constructor; auto.
- inv H. InvEval. rewrite eval_addressing_Ainstack in H6. inv H6. constructor; auto.
- constructor; auto.
Qed.

End CMCONSTR.
