(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*                 Xavier Leroy, INRIA Paris                           *)
(*                                                                     *)
(*  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.     *)
(*                                                                     *)
(* *********************************************************************)

(** Recognition of combined operations, addressing modes and conditions
  during the [CSE] phase. *)

Require Import FunInd.
Require Import Coqlib.
Require Import Integers Values Memory.
Require Import Op RTL CSEdomain.
Require Import CombineOp.

Section COMBINE.

Variable ge: genv.
Variable sp: val.
Variable m: mem.
Variable get: valnum -> option rhs.
Variable valu: valnum -> val.
Hypothesis get_sound: forall v rhs, get v = Some rhs -> rhs_eval_to valu ge sp m rhs (valu v).

Lemma get_op_sound:
  forall v op vl, get v = Some (Op op vl) -> eval_operation ge sp op (map valu vl) m = Some (valu v).
Proof.
(* Goal: forall (op : operation) (args : list valnum) (op' : operation) (args' : list valnum) (_ : @eq (option (prod operation (list valnum))) (combine_op get op args) (@Some (prod operation (list valnum)) (@pair operation (list valnum) op' args'))), @eq (option val) (@eval_operation fundef unit ge sp op' (@map valnum val valu args') m) (@eval_operation fundef unit ge sp op (@map valnum val valu args) m) *)
  intros. exploit get_sound; eauto. intros REV; inv REV; auto.
Qed.

Ltac UseGetSound :=
  match goal with
  | [ H: get _ = Some _ |- _ ] =>
      let x := fresh "EQ" in (generalize (get_op_sound _ _ _ H); intros x; simpl in x; FuncInv)
  end.

Lemma combine_compimm_ne_0_sound:
  forall x cond args,
  combine_compimm_ne_0 get x = Some(cond, args) ->
  eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.zero) /\
  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.zero).
Proof.
(* Goal: forall (x : valnum) (cond : condition) (args : list valnum) (_ : @eq (option (prod condition (list valnum))) (combine_compimm_ne_1 get x) (@Some (prod condition (list valnum)) (@pair condition (list valnum) cond args))), and (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmp_bool Cne (valu x) (Vint Int.one))) (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.one))) *)
  intros until args. functional induction (combine_compimm_ne_0 get x); intros EQ; inv EQ.
  (* of cmp *)
(* Goal: @eq (option val) (@eval_addressing64 fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing64 fundef unit ge sp (Aindexed n) (@map valnum val valu (@cons valnum x (@nil valnum)))) *)
  UseGetSound. rewrite <- H.
(* Goal: and (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmp_bool Ceq (Val.of_optbool (eval_condition cond (@map valnum val valu args) m)) (Vint Int.one))) (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmpu_bool (Mem.valid_pointer m) Ceq (Val.of_optbool (eval_condition cond (@map valnum val valu args) m)) (Vint Int.one))) *)
  destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
  (* of and *)
(* Goal: @eq (option val) (@eval_addressing64 fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing64 fundef unit ge sp (Aindexed n) (@map valnum val valu (@cons valnum x (@nil valnum)))) *)
  UseGetSound. rewrite <- H.
(* Goal: and (@eq (option bool) (eval_condition (Cmasknotzero n) (@cons val v (@nil val)) m) (Val.cmp_bool Cne (Val.and v (Vint n)) (Vint Int.zero))) (@eq (option bool) (eval_condition (Cmasknotzero n) (@cons val v (@nil val)) m) (Val.cmpu_bool (Mem.valid_pointer m) Cne (Val.and v (Vint n)) (Vint Int.zero))) *)
  destruct v; simpl; auto.
Qed.

Lemma combine_compimm_eq_0_sound:
  forall x cond args,
  combine_compimm_eq_0 get x = Some(cond, args) ->
  eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.zero) /\
  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.zero).
Proof.
(* Goal: forall (x : valnum) (cond : condition) (args : list valnum) (_ : @eq (option (prod condition (list valnum))) (combine_compimm_ne_1 get x) (@Some (prod condition (list valnum)) (@pair condition (list valnum) cond args))), and (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmp_bool Cne (valu x) (Vint Int.one))) (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.one))) *)
  intros until args. functional induction (combine_compimm_eq_0 get x); intros EQ; inv EQ.
  (* of cmp *)
(* Goal: @eq (option val) (@eval_addressing64 fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing64 fundef unit ge sp (Aindexed n) (@map valnum val valu (@cons valnum x (@nil valnum)))) *)
  UseGetSound. rewrite <- H.
(* Goal: and (@eq (option bool) (eval_condition (negate_condition c) (@map valnum val valu args) m) (Val.cmp_bool Cne (Val.of_optbool (eval_condition c (@map valnum val valu args) m)) (Vint Int.one))) (@eq (option bool) (eval_condition (negate_condition c) (@map valnum val valu args) m) (Val.cmpu_bool (Mem.valid_pointer m) Cne (Val.of_optbool (eval_condition c (@map valnum val valu args) m)) (Vint Int.one))) *)
  rewrite eval_negate_condition.
(* Goal: and (@eq (option bool) (@Some bool (negb b)) (Val.cmp_bool Cne (if b then Vtrue else Vfalse) (Vint Int.one))) (@eq (option bool) (@Some bool (negb b)) (Val.cmpu_bool (Mem.valid_pointer m) Cne (if b then Vtrue else Vfalse) (Vint Int.one))) *)
  destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
  (* of and *)
(* Goal: @eq (option val) (@eval_addressing64 fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing64 fundef unit ge sp (Aindexed n) (@map valnum val valu (@cons valnum x (@nil valnum)))) *)
  UseGetSound. rewrite <- H. destruct v; auto.
Qed.

Lemma combine_compimm_eq_1_sound:
  forall x cond args,
  combine_compimm_eq_1 get x = Some(cond, args) ->
  eval_condition cond (map valu args) m = Val.cmp_bool Ceq (valu x) (Vint Int.one) /\
  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Ceq (valu x) (Vint Int.one).
Proof.
(* Goal: forall (x : valnum) (cond : condition) (args : list valnum) (_ : @eq (option (prod condition (list valnum))) (combine_compimm_ne_1 get x) (@Some (prod condition (list valnum)) (@pair condition (list valnum) cond args))), and (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmp_bool Cne (valu x) (Vint Int.one))) (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.one))) *)
  intros until args. functional induction (combine_compimm_eq_1 get x); intros EQ; inv EQ.
  (* of cmp *)
(* Goal: @eq (option val) (@eval_addressing64 fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing64 fundef unit ge sp (Aindexed n) (@map valnum val valu (@cons valnum x (@nil valnum)))) *)
  UseGetSound. rewrite <- H.
(* Goal: and (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmp_bool Ceq (Val.of_optbool (eval_condition cond (@map valnum val valu args) m)) (Vint Int.one))) (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmpu_bool (Mem.valid_pointer m) Ceq (Val.of_optbool (eval_condition cond (@map valnum val valu args) m)) (Vint Int.one))) *)
  destruct (eval_condition cond (map valu args) m); simpl; auto. destruct b; auto.
Qed.

Lemma combine_compimm_ne_1_sound:
  forall x cond args,
  combine_compimm_ne_1 get x = Some(cond, args) ->
  eval_condition cond (map valu args) m = Val.cmp_bool Cne (valu x) (Vint Int.one) /\
  eval_condition cond (map valu args) m = Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.one).
Proof.
(* Goal: forall (x : valnum) (cond : condition) (args : list valnum) (_ : @eq (option (prod condition (list valnum))) (combine_compimm_ne_1 get x) (@Some (prod condition (list valnum)) (@pair condition (list valnum) cond args))), and (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmp_bool Cne (valu x) (Vint Int.one))) (@eq (option bool) (eval_condition cond (@map valnum val valu args) m) (Val.cmpu_bool (Mem.valid_pointer m) Cne (valu x) (Vint Int.one))) *)
  intros until args. functional induction (combine_compimm_ne_1 get x); intros EQ; inv EQ.
  (* of cmp *)
(* Goal: @eq (option val) (@eval_addressing64 fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing64 fundef unit ge sp (Aindexed n) (@map valnum val valu (@cons valnum x (@nil valnum)))) *)
  UseGetSound. rewrite <- H.
(* Goal: and (@eq (option bool) (eval_condition (negate_condition c) (@map valnum val valu args) m) (Val.cmp_bool Cne (Val.of_optbool (eval_condition c (@map valnum val valu args) m)) (Vint Int.one))) (@eq (option bool) (eval_condition (negate_condition c) (@map valnum val valu args) m) (Val.cmpu_bool (Mem.valid_pointer m) Cne (Val.of_optbool (eval_condition c (@map valnum val valu args) m)) (Vint Int.one))) *)
  rewrite eval_negate_condition.
(* Goal: and (@eq (option bool) (@Some bool (negb b)) (Val.cmp_bool Cne (if b then Vtrue else Vfalse) (Vint Int.one))) (@eq (option bool) (@Some bool (negb b)) (Val.cmpu_bool (Mem.valid_pointer m) Cne (if b then Vtrue else Vfalse) (Vint Int.one))) *)
  destruct (eval_condition c (map valu args) m); simpl; auto. destruct b; auto.
Qed.

Theorem combine_cond_sound:
  forall cond args cond' args',
  combine_cond get cond args = Some(cond', args') ->
  eval_condition cond' (map valu args') m = eval_condition cond (map valu args) m.
Proof.
(* Goal: forall (op : operation) (args : list valnum) (op' : operation) (args' : list valnum) (_ : @eq (option (prod operation (list valnum))) (combine_op get op args) (@Some (prod operation (list valnum)) (@pair operation (list valnum) op' args'))), @eq (option val) (@eval_operation fundef unit ge sp op' (@map valnum val valu args') m) (@eval_operation fundef unit ge sp op (@map valnum val valu args) m) *)
  intros. functional inversion H; subst.
  (* compimm ne zero *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Cne Int.zero) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Cne Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.zero) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
  simpl; eapply combine_compimm_ne_0_sound; eauto.
  (* compimm ne one *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Cne Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.zero) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
  simpl; eapply combine_compimm_ne_1_sound; eauto.
  (* compimm eq zero *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.zero) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
  simpl; eapply combine_compimm_eq_0_sound; eauto.
  (* compimm eq one *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
  simpl; eapply combine_compimm_eq_1_sound; eauto.
  (* compuimm ne zero *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Cne Int.zero) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Cne Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.zero) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
  simpl; eapply combine_compimm_ne_0_sound; eauto.
  (* compuimm ne one *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Cne Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.zero) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
  simpl; eapply combine_compimm_ne_1_sound; eauto.
  (* compuimm eq zero *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.zero) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
  simpl; eapply combine_compimm_eq_0_sound; eauto.
  (* compuimm eq one *)
(* Goal: @eq (option bool) (eval_condition cond' (@map valnum val valu args') m) (eval_condition (Ccompuimm Ceq Int.one) (@map valnum val valu (@cons valnum x (@nil valnum))) m) *)
  simpl; eapply combine_compimm_eq_1_sound; eauto.
Qed.

Theorem combine_addr_32_sound:
  forall addr args addr' args',
  combine_addr_32 get addr args = Some(addr', args') ->
  eval_addressing32 ge sp addr' (map valu args') = eval_addressing32 ge sp addr (map valu args).
Proof.
(* Goal: forall (op : operation) (args : list valnum) (op' : operation) (args' : list valnum) (_ : @eq (option (prod operation (list valnum))) (combine_op get op args) (@Some (prod operation (list valnum)) (@pair operation (list valnum) op' args'))), @eq (option val) (@eval_operation fundef unit ge sp op' (@map valnum val valu args') m) (@eval_operation fundef unit ge sp op (@map valnum val valu args) m) *)
  intros. functional inversion H; subst.
  (* indexed - lea *)
(* Goal: @eq (option val) (@eval_addressing64 fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing64 fundef unit ge sp (Aindexed n) (@map valnum val valu (@cons valnum x (@nil valnum)))) *)
  UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7.
(* Goal: @eq (option val) (@eval_addressing32 fundef unit ge sp (offset_addressing_total a n) (@map valnum val valu args')) (@Some val (Val.add (valu x) (Vint (Int.repr n)))) *)
  eapply eval_offset_addressing_total_32; eauto.
Qed.

Theorem combine_addr_64_sound:
  forall addr args addr' args',
  combine_addr_64 get addr args = Some(addr', args') ->
  eval_addressing64 ge sp addr' (map valu args') = eval_addressing64 ge sp addr (map valu args).
Proof.
(* Goal: forall (op : operation) (args : list valnum) (op' : operation) (args' : list valnum) (_ : @eq (option (prod operation (list valnum))) (combine_op get op args) (@Some (prod operation (list valnum)) (@pair operation (list valnum) op' args'))), @eq (option val) (@eval_operation fundef unit ge sp op' (@map valnum val valu args') m) (@eval_operation fundef unit ge sp op (@map valnum val valu args) m) *)
  intros. functional inversion H; subst.
  (* indexed - leal *)
(* Goal: @eq (option val) (@eval_addressing64 fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing64 fundef unit ge sp (Aindexed n) (@map valnum val valu (@cons valnum x (@nil valnum)))) *)
  UseGetSound. simpl. unfold offset_addressing in H7. destruct (addressing_valid (offset_addressing_total a n)); inv H7.
(* Goal: @eq (option val) (@eval_addressing64 fundef unit ge sp (offset_addressing_total a n) (@map valnum val valu args')) (@Some val (Val.addl (valu x) (Vlong (Int64.repr n)))) *)
  eapply eval_offset_addressing_total_64; eauto.
Qed.

Theorem combine_addr_sound:
  forall addr args addr' args',
  combine_addr get addr args = Some(addr', args') ->
  eval_addressing ge sp addr' (map valu args') = eval_addressing ge sp addr (map valu args).
Proof.
(* Goal: forall (addr : addressing) (args : list valnum) (addr' : addressing) (args' : list valnum) (_ : @eq (option (prod addressing (list valnum))) (combine_addr get addr args) (@Some (prod addressing (list valnum)) (@pair addressing (list valnum) addr' args'))), @eq (option val) (@eval_addressing fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing fundef unit ge sp addr (@map valnum val valu args)) *)
  unfold combine_addr, eval_addressing; intros; destruct Archi.ptr64.
(* Goal: @eq (option val) (@eval_addressing64 fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing64 fundef unit ge sp addr (@map valnum val valu args)) *)
(* Goal: @eq (option val) (@eval_addressing32 fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing32 fundef unit ge sp addr (@map valnum val valu args)) *)
  apply combine_addr_64_sound; auto.
(* Goal: @eq (option val) (@eval_addressing32 fundef unit ge sp addr' (@map valnum val valu args')) (@eval_addressing32 fundef unit ge sp addr (@map valnum val valu args)) *)
  apply combine_addr_32_sound; auto.
Qed.

Theorem combine_op_sound:
  forall op args op' args',
  combine_op get op args = Some(op', args') ->
  eval_operation ge sp op' (map valu args') m = eval_operation ge sp op (map valu args) m.
Proof.
(* Goal: forall (op : operation) (args : list valnum) (op' : operation) (args' : list valnum) (_ : @eq (option (prod operation (list valnum))) (combine_op get op args) (@Some (prod operation (list valnum)) (@pair operation (list valnum) op' args'))), @eq (option val) (@eval_operation fundef unit ge sp op' (@map valnum val valu args') m) (@eval_operation fundef unit ge sp op (@map valnum val valu args) m) *)
  intros. functional inversion H; subst.
(* lea-lea *)
(* Goal: @eq (option val) (@eval_operation fundef unit ge sp (Ocmp cond') (@map valnum val valu args') m) (@eval_operation fundef unit ge sp (Ocmp cond) (@map valnum val valu args) m) *)
  simpl. eapply combine_addr_32_sound; eauto.
(* leal-leal *)
(* Goal: @eq (option val) (@eval_operation fundef unit ge sp (Ocmp cond') (@map valnum val valu args') m) (@eval_operation fundef unit ge sp (Ocmp cond) (@map valnum val valu args) m) *)
  simpl. eapply combine_addr_64_sound; eauto.
(* andimm - andimm *)
(* Goal: @eq (option val) (@eval_operation fundef unit ge sp (Ocmp cond') (@map valnum val valu args') m) (@eval_operation fundef unit ge sp (Ocmp cond) (@map valnum val valu args) m) *)
  UseGetSound; simpl. rewrite <- H0. rewrite Val.and_assoc. auto.
(* orimm - orimm *)
(* Goal: @eq (option val) (@eval_operation fundef unit ge sp (Ocmp cond') (@map valnum val valu args') m) (@eval_operation fundef unit ge sp (Ocmp cond) (@map valnum val valu args) m) *)
  UseGetSound; simpl. rewrite <- H0. rewrite Val.or_assoc. auto.
(* xorimm - xorimm *)
(* Goal: @eq (option val) (@eval_operation fundef unit ge sp (Ocmp cond') (@map valnum val valu args') m) (@eval_operation fundef unit ge sp (Ocmp cond) (@map valnum val valu args) m) *)
  UseGetSound; simpl. rewrite <- H0. rewrite Val.xor_assoc. auto.
(* andimm - andimm *)
(* Goal: @eq (option val) (@eval_operation fundef unit ge sp (Ocmp cond') (@map valnum val valu args') m) (@eval_operation fundef unit ge sp (Ocmp cond) (@map valnum val valu args) m) *)
  UseGetSound; simpl. rewrite <- H0. rewrite Val.andl_assoc. auto.
(* orimm - orimm *)
(* Goal: @eq (option val) (@eval_operation fundef unit ge sp (Ocmp cond') (@map valnum val valu args') m) (@eval_operation fundef unit ge sp (Ocmp cond) (@map valnum val valu args) m) *)
  UseGetSound; simpl. rewrite <- H0. rewrite Val.orl_assoc. auto.
(* xorimm - xorimm *)
(* Goal: @eq (option val) (@eval_operation fundef unit ge sp (Ocmp cond') (@map valnum val valu args') m) (@eval_operation fundef unit ge sp (Ocmp cond) (@map valnum val valu args) m) *)
  UseGetSound; simpl. rewrite <- H0. rewrite Val.xorl_assoc. auto.
(* cmp *)
(* Goal: @eq (option val) (@eval_operation fundef unit ge sp (Ocmp cond') (@map valnum val valu args') m) (@eval_operation fundef unit ge sp (Ocmp cond) (@map valnum val valu args) m) *)
  simpl. decEq; decEq. eapply combine_cond_sound; eauto.
Qed.

End COMBINE.
