Require Import Coqlib Floats Values Memory.
Require Import Integers.
Require Import Op Registers.
Require Import BTL_SEtheory.
Require Import BTL_SEsimuref.

(** Target op simplifications using "fake" values *)

Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): option sval :=
  None.

Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) :=
  None.

(* Main proof of simplification *)

(*
Lemma target_op_simplify_correct ge sp ctx op lr hrs fsv st args m: forall
   (H: target_op_simplify op lr hrs = Some fsv)
   (REF: ris_refines ctx hrs st)
   (OK0: ris_ok ctx hrs)
   (OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args)
   (OK2: eval_smem ctx (si_smem st) = Some m),
   eval_sval ctx fsv = eval_operation ge sp op args m.
Proof.
  unfold target_op_simplify; simpl.
  intros H (LREF & SREF & SREG & SMEM) ? ? ?.
  congruence.
Qed.

Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
  (TARGET: target_cbranch_expanse hst c l = Some (c', l'))
  (LREF : hsilocal_refines ge sp rs0 m0 hst st)
  (OK: hsok_local ge sp rs0 m0 hst),
  seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 =
  seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
Proof.
  unfold target_cbranch_expanse, seval_condition; simpl.
  intros H (LREF & SREF & SREG & SMEM) ?.
  congruence.
Qed.
Global Opaque target_op_simplify.
   Global Opaque target_cbranch_expanse.*)