1 files changed, 41 insertions, 0 deletions
diff --git a/aarch64/BTL_SEsimplify.v b/aarch64/BTL_SEsimplify.v
new file mode 100644
index 00000000..3e930439
--- /dev/null
+++ b/aarch64/BTL_SEsimplify.v
@@ -0,0 +1,41 @@
+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 ctx op lr hrs fsv st args: 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),
+   eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) op args (cm0 ctx).
+Proof.
+  unfold target_op_simplify; simpl.
+  intros H ? ? ?.
+  congruence.
+Qed.
+
+Lemma target_cbranch_expanse_correct hrs c l ctx st c' l': forall
+  (TARGET: target_cbranch_expanse hrs c l = Some (c', l'))
+  (REF: ris_refines ctx hrs st)
+  (OK: ris_ok ctx hrs),
+  eval_scondition ctx c' l' =
+  eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)).
+Proof.
+  unfold target_cbranch_expanse; simpl.
+  intros H ? ?.
+  congruence.
+Qed.
+Global Opaque target_op_simplify.
+Global Opaque target_cbranch_expanse.