cleanup

1 files changed, 0 insertions, 42 deletions

diff --git a/aarch64/RTLpathSE_simplify.v b/aarch64/RTLpathSE_simplify.v
deleted file mode 100644
index 1ee7dac5..00000000
--- a/aarch64/RTLpathSE_simplify.v
+++ /dev/null
@@ -1,42 +0,0 @@
-Require Import Coqlib Floats Values Memory.
-Require Import Integers.
-Require Import Op Registers.
-Require Import RTLpathSE_theory.
-Require Import RTLpathSE_simu_specs.
-
-(** Target op simplifications using "fake" values *)
-
-Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
-  None.
-
-Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) :=
-  None.
-
-(* Main proof of simplification *)
-
-Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
-   (H: target_op_simplify op lr hst = Some fsv)
-   (REF: hsilocal_refines ge sp rs0 m0 hst st)
-   (OK0: hsok_local ge sp rs0 m0 hst)
-   (OK1: seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args)
-   (OK2: seval_smem ge sp (si_smem st) rs0 m0 = Some m),
-   seval_sval ge sp (hsval_proj fsv) rs0 m0 = 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.