From 222c9047d61961db9c6b19fed5ca49829223fd33 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 27 Feb 2020 05:45:13 +0100
Subject: CSE2 now uses is_trivial_op

---
 backend/CSE2proof.v | 23 +++++++++++++++++++++--
 1 file changed, 21 insertions(+), 2 deletions(-)

(limited to 'backend/CSE2proof.v')

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 0b92f5e5..eb4268f0 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -1401,6 +1401,24 @@ Proof.
 Qed.
 Hint Resolve wellformed_mem_mpc : wellformed.
 
+Lemma match_same_option :
+  forall { A B : Type},
+  forall x : option A,
+  forall y : B,
+    (match x with Some _ => y | None => y end) = y.
+Proof.
+  destruct x; trivial.
+Qed.
+
+Lemma match_same_bool :
+  forall { B : Type},
+  forall x : bool,
+  forall y : B,
+    (if x then y else y) = y.
+Proof.
+  destruct x; trivial.
+Qed.
+
 Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 ->
   forall S1', match_states S1 S1' ->
@@ -1428,8 +1446,9 @@ Proof.
   reflexivity.
 - (* op *)
   unfold transf_instr in *.
-  destruct find_op_in_fmap eqn:FIND_OP.
+  destruct (if is_trivial_op op then None else find_op_in_fmap (forward_map f)  pc op (subst_args (forward_map f) pc args)) eqn:FIND_OP.
   {
+    destruct is_trivial_op. discriminate.
     unfold find_op_in_fmap, fmap_sem', fmap_sem in *.
     destruct (forward_map f) as [map |] eqn:MAP.
     2: discriminate.
@@ -1846,4 +1865,4 @@ Proof.
   exact step_simulation.
 Qed.
 
-End PRESERVATION.
\ No newline at end of file
+End PRESERVATION.
-- 
cgit