Separate target_op_simplify for riscV

1 files changed, 19 insertions, 0 deletions

diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
new file mode 100644
index 00000000..4fadcfdc
--- /dev/null
+++ b/riscV/RTLpathSE_simplify.v
@@ -0,0 +1,19 @@
+Require Import Op Registers.
+Require Import RTLpathSE_theory.
+Require Import RTLpathSE_simu_specs.
+
+Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
+  None.  (* default implementation *)
+
+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. congruence.
+Qed.
+Global Opaque target_op_simplify.
+