From 6f05c86e614797b76d92bc3dbbd4c0ece683168e Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Thu, 3 Oct 2019 16:31:03 +0200
Subject: Proof for Iop

---
 backend/Duplicate.v      | 14 +++++++++++++-
 backend/Duplicateproof.v |  7 +++++++
 2 files changed, 20 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index ce6c436f..a96d0826 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -2,7 +2,7 @@
   structures *)
 
 Require Import AST RTL Maps Globalenvs.
-Require Import Coqlib Errors.
+Require Import Coqlib Errors Op.
 
 Local Open Scope error_monad_scope.
 Local Open Scope positive_scope.
@@ -45,9 +45,21 @@ Definition verify_is_copy revmap n n' :=
   | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end
   end.
 
+
 Definition verify_match_inst revmap inst tinst :=
   match inst with
   | Inop n => match tinst with Inop n' => do u <- verify_is_copy revmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end
+  | Iop op lr r n => match tinst with
+      Iop op' lr' r' n' =>
+          do u <- verify_is_copy revmap n n';
+          if (eq_operation op op') then
+            if (list_eq_dec Pos.eq_dec lr lr') then
+              if (Pos.eq_dec r r') then
+                OK tt
+              else Error (msg "Different r in Iop")
+            else Error (msg "Different lr in Iop")
+          else Error(msg "Different operations in Iop")
+      | _ => Error(msg "verify_match_inst Inop") end
   | _ => Error(msg "not implemented")
   end.
 
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index f3218f5f..d8ca9cd1 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -83,6 +83,13 @@ Proof.
 (* Inop *)
   - destruct i'; try (inversion H; fail). monadInv H. eapply verify_is_copy_correct_one. destruct x. eassumption.
     constructor; eauto.
+(* Iop *)
+  - destruct i'; try (inversion H; fail). monadInv H.
+    destruct (eq_operation _ _) eqn:EQO; try discriminate.
+    destruct (list_eq_dec _ _ _) eqn:LEQ; try discriminate.
+    destruct (Pos.eq_dec _ _) eqn:POS; try discriminate. clear EQ0. subst.
+    eapply verify_is_copy_correct_one. destruct x. eassumption.
+    constructor.
 Qed.
 
 Lemma verify_mapping_mn_correct:
-- 
cgit