From ddc17a17408541efa8b23afa3e6ccad1e6ce0b6e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 1 Sep 2021 16:57:12 +0200 Subject: cleanup --- aarch64/RTLpathSE_simplify.v | 42 ------------------------------------------ 1 file changed, 42 deletions(-) delete mode 100644 aarch64/RTLpathSE_simplify.v (limited to 'aarch64') 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. -- cgit