Finished Duplicate proof.

2 files changed, 58 insertions, 36 deletions

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index 0f3c2ba9..d1458bd4 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -45,6 +45,17 @@ 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.
 
+Fixpoint verify_is_copy_list revmap ln ln' :=
+  match ln with
+  | n::ln => match ln' with
+             | n'::ln' => do u <- verify_is_copy revmap n n';
+                          verify_is_copy_list revmap ln ln'
+             | nil => Error (msg "verify_is_copy_list: ln' bigger than ln") end
+  | nil => match ln' with
+          | n :: ln' => Error (msg "verify_is_copy_list: ln bigger than ln'")
+          | nil => OK tt end
+  end.
+
 Lemma product_eq {A B: Type} :
   (forall (a b: A), {a=b} + {a<>b}) ->
   (forall (c d: B), {c=d} + {c<>d}) ->
@@ -152,12 +163,18 @@ Definition verify_match_inst revmap inst tinst :=
           else Error (msg "Different cond in Icond")
       | _ => Error (msg "verify_match_inst Icond") end
 
+  | Ijumptable r ln => match tinst with
+      | Ijumptable r' ln' =>
+          do u <- verify_is_copy_list revmap ln ln';
+          if (Pos.eq_dec r r') then OK tt
+          else Error (msg "Different r in Ijumptable")
+      | _ => Error (msg "verify_match_inst Ijumptable") end
+
   | Ireturn or => match tinst with
       | Ireturn or' =>
           if (option_eq Pos.eq_dec or or') then OK tt
           else Error (msg "Different or in Ireturn")
       | _ => Error (msg "verify_match_inst Ireturn") end
-  | _ => Error(msg "not implemented")
   end.
 
 Definition verify_mapping_mn f xf (m: positive*positive) :=
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index ba1fecc1..54dd6196 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -51,26 +51,26 @@ Proof.
     + monadInv H0. destruct x0. eapply IHlb; assumption.
 Qed.
 
-Inductive rtl_one_successor : node -> node -> instruction -> instruction -> Prop :=
-  | inop_one_succ : forall n n', rtl_one_successor n n' (Inop n) (Inop n')
-  | iop_one_succ : forall op lr r n n', rtl_one_successor n n' (Iop op lr r n) (Iop op lr r n')
-  | iload_one_succ : forall m a lr r n n', rtl_one_successor n n' (Iload m a lr r n) (Iload m a lr r n')
-  | istore_one_succ : forall m a lr r n n', rtl_one_successor n n' (Istore m a lr r n) (Istore m a lr r n')
-  | icall_one_succ : forall s ri lr r n n', rtl_one_successor n n' (Icall s ri lr r n) (Icall s ri lr r n')
-  | ibuiltin_one_succ : forall ef lbr br n n', rtl_one_successor n n' (Ibuiltin ef lbr br n) (Ibuiltin ef lbr br n')
-.
-
-Lemma verify_is_copy_correct_one:
-  forall xf n n' i i',
+Lemma verify_is_copy_correct:
+  forall xf n n',
   verify_is_copy (fn_revmap xf) n n' = OK tt ->
-  rtl_one_successor n n' i i' ->
-  match_inst (fun nn => (fn_revmap xf) ! nn) i i'.
+  (fn_revmap xf) ! n' = Some n.
 Proof.
   intros. unfold verify_is_copy in H. destruct (_ ! n') eqn:REVM; [|inversion H].
-  destruct (n ?= p) eqn:NP; try (inversion H; fail). clear H.
+  destruct (n ?= n0) eqn:NP; try (inversion H; fail).
   eapply Pos.compare_eq in NP. subst.
-  inv H0.
-  all: constructor; eauto.
+  reflexivity.
+Qed.
+
+Lemma verify_is_copy_list_correct:
+  forall xf ln ln',
+  verify_is_copy_list (fn_revmap xf) ln ln' = OK tt ->
+  list_forall2 (fun n n' => (fn_revmap xf) ! n' = Some n) ln ln'.
+Proof.
+  induction ln.
+  - intros. destruct ln'; monadInv H. constructor.
+  - intros. destruct ln'; monadInv H. destruct x. apply verify_is_copy_correct in EQ.
+    eapply IHln in EQ0. constructor; assumption.
 Qed.
 
 Lemma verify_match_inst_correct:
@@ -81,39 +81,40 @@ Proof.
   intros. unfold verify_match_inst in H.
   destruct i; try (inversion H; fail).
 (* Inop *)
-  - destruct i'; try (inversion H; fail). monadInv H. eapply verify_is_copy_correct_one. destruct x. eassumption.
+  - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
     constructor; eauto.
 (* Iop *)
   - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
     destruct (eq_operation _ _); try discriminate.
     destruct (list_eq_dec _ _ _); try discriminate.
     destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst.
-    eapply verify_is_copy_correct_one. destruct x. eassumption.
-    constructor.
+    constructor. assumption.
 (* Iload *)
   - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
     destruct (chunk_eq _ _); try discriminate.
     destruct (eq_addressing _ _); try discriminate.
     destruct (list_eq_dec _ _ _); try discriminate.
     destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst.
-    eapply verify_is_copy_correct_one. destruct x. eassumption.
-    constructor.
+    constructor. assumption.
 (* Istore *)
   - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
     destruct (chunk_eq _ _); try discriminate.
     destruct (eq_addressing _ _); try discriminate.
     destruct (list_eq_dec _ _ _); try discriminate.
     destruct (Pos.eq_dec _ _); try discriminate. clear EQ0. subst.
-    eapply verify_is_copy_correct_one. destruct x. eassumption.
-    constructor.
+    constructor. assumption.
 (* Icall *)
   - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
     destruct (signature_eq _ _); try discriminate.
     destruct (product_eq _ _ _ _); try discriminate.
     destruct (list_eq_dec _ _ _); try discriminate.
-    destruct (Pos.eq_dec _ _); try discriminate.
-    eapply verify_is_copy_correct_one. destruct x. eassumption. subst.
-    constructor.
+    destruct (Pos.eq_dec _ _); try discriminate. subst.
+    constructor. assumption.
 (* Itailcall *)
   - destruct i'; try (inversion H; fail).
     destruct (signature_eq _ _); try discriminate.
@@ -122,26 +123,30 @@ Proof.
     constructor.
 (* Ibuiltin *)
   - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_correct in EQ.
     destruct (external_function_eq _ _); try discriminate.
     destruct (list_eq_dec _ _ _); try discriminate.
-    destruct (builtin_res_eq_pos _ _); try discriminate.
-    eapply verify_is_copy_correct_one. destruct x. eassumption. subst.
-    constructor.
+    destruct (builtin_res_eq_pos _ _); try discriminate. subst.
+    constructor. assumption.
 (* Icond *)
   - destruct i'; try (inversion H; fail). monadInv H.
-    unfold verify_is_copy in EQ, EQ1.
-      destruct (_ ! n1) eqn:REVM; [|inversion EQ].
-      destruct (n ?= p) eqn:NP; try (inversion EQ; fail). eapply Pos.compare_eq in NP. subst. inv EQ.
-      destruct (_ ! n2) eqn:REVMM; [|inversion EQ1].
-      destruct (n0 ?= p0) eqn:NP0; try (inversion EQ1; fail). eapply Pos.compare_eq in NP0. subst. inv EQ1.
+    destruct x. eapply verify_is_copy_correct in EQ.
+    destruct x0. eapply verify_is_copy_correct in EQ1.
     destruct (condition_eq _ _); try discriminate.
-    destruct (list_eq_dec _ _ _); try discriminate. subst. constructor; assumption.
+    destruct (list_eq_dec _ _ _); try discriminate. subst.
+    constructor; assumption.
+(* Ijumptable *)
+  - destruct i'; try (inversion H; fail). monadInv H.
+    destruct x. eapply verify_is_copy_list_correct in EQ.
+    destruct (Pos.eq_dec _ _); try discriminate. subst.
+    constructor. assumption.
 (* Ireturn *)
   - destruct i'; try (inversion H; fail).
     destruct (option_eq _ _ _); try discriminate. subst. clear H.
     constructor.
 Qed.
 
+
 Lemma verify_mapping_mn_correct:
   forall mp n n' i f xf tc,
   mp ! n' = Some n ->