finish verify_block and proof

1 files changed, 123 insertions, 21 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 82a54061..7bc091ef 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -512,20 +512,91 @@ Proof.
   - intros. destruct ln'; monadInv H. constructor; eauto.
 Qed.
 
+(* TODO Copied from duplicate, should we import ? *)
+Lemma product_eq {A B: Type} :
+  (forall (a b: A), {a=b} + {a<>b}) ->
+  (forall (c d: B), {c=d} + {c<>d}) ->
+  forall (x y: A+B), {x=y} + {x<>y}.
+Proof.
+  intros H H'. intros. decide equality.
+Qed.
+
+(* TODO Copied from duplicate, should we import ? *)
+(** FIXME Ideally i would like to put this in AST.v but i get an "illegal application"
+ * error when doing so *)
+Remark builtin_arg_eq_pos: forall (a b: builtin_arg positive), {a=b} + {a<>b}.
+Proof.
+  intros.
+  apply (builtin_arg_eq Pos.eq_dec).
+Defined.
+Global Opaque builtin_arg_eq_pos.
+
+(* TODO Copied from duplicate, should we import ? *)
+Remark builtin_res_eq_pos: forall (a b: builtin_res positive), {a=b} + {a<>b}.
+Proof. intros. apply (builtin_res_eq Pos.eq_dec). Qed.
+Global Opaque builtin_res_eq_pos.
+
 (* TODO: deuxième étape (après BTLtoRTLproof.plus_simulation) *)
 Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) :=
   match ib with
   | BF fi =>
       match fi with
-      | Bgoto pc =>
-          match dupmap!pc with
-          | Some _ => OK None
-          | None => Error (msg "verify_block: incorrect dupmap Bgoto")
+      | Bgoto pc1 =>
+          do u <- verify_is_copy dupmap pc1 pc;
+          if negb isfst then
+            OK None
+          else Error (msg "verify_block: isfst is true Bgoto")
+      | Breturn or =>
+          match cfg!pc with
+          | Some (Ireturn or') =>
+              if option_eq Pos.eq_dec or or' then OK None
+              else Error (msg "verify_block: different opt reg in Breturn")
+          | _ => Error (msg "verify_block: incorrect cfg Breturn")
           end
-      | _ =>
+      | Bcall s ri lr r pc1 =>
           match cfg!pc with
-          | Some i => Error (msg "TODO") (* TODO *)
-          | None => Error (msg "verify_block: incorrect cfg BF")
+          | Some (Icall s' ri' lr' r' pc2) =>
+              do u <- verify_is_copy dupmap pc1 pc2;
+              if (signature_eq s s') then
+                if (product_eq Pos.eq_dec ident_eq ri ri') then
+                  if (list_eq_dec Pos.eq_dec lr lr') then
+                    if (Pos.eq_dec r r') then OK None
+                    else Error (msg "verify_block: different r r' in Bcall")
+                  else Error (msg "verify_block: different lr in Bcall")
+                else Error (msg "verify_block: different ri in Bcall")
+              else Error (msg "verify_block: different signatures in Bcall")
+          | _ => Error (msg "verify_block: incorrect cfg Bcall")
+          end
+      | Btailcall s ri lr =>
+          match cfg!pc with
+          | Some (Itailcall s' ri' lr') =>
+              if (signature_eq s s') then
+                if (product_eq Pos.eq_dec ident_eq ri ri') then
+                  if (list_eq_dec Pos.eq_dec lr lr') then OK None
+                  else Error (msg "verify_block: different lr in Btailcall")
+                else Error (msg "verify_block: different ri in Btailcall")
+              else Error (msg "verify_block: different signatures in Btailcall")
+          | _ => Error (msg "verify_block: incorrect cfg Btailcall")
+          end
+      | Bbuiltin ef la br pc1 =>
+          match cfg!pc with
+          | Some (Ibuiltin ef' la' br' pc2) =>
+              do u <- verify_is_copy dupmap pc1 pc2;
+              if (external_function_eq ef ef') then
+                if (list_eq_dec builtin_arg_eq_pos la la') then
+                  if (builtin_res_eq_pos br br') then OK None
+                  else Error (msg "verify_block: different brr in Bbuiltin")
+                else Error (msg "verify_block: different lbar in Bbuiltin")
+              else Error (msg "verify_block: different ef in Bbuiltin")
+          | _ => Error (msg "verify_block: incorrect cfg Bbuiltin")
+          end
+      | Bjumptable r ln =>
+          match cfg!pc with
+          | Some (Ijumptable r' ln') =>
+              do u <- verify_is_copy_list dupmap ln ln';
+              if (Pos.eq_dec r r') then OK None
+              else Error (msg "verify_block: different r in Bjumptable")
+          | _ => Error (msg "verify_block: incorrect cfg Bjumptable")
           end
       end
   | Bnop =>
@@ -602,12 +673,51 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
   end.
 
 (* This property expresses that "relation" [match_iblock] is a partial function (see also [iblock_istep_run_equiv] above) *)
-Lemma verify_block_correct: forall dupmap cfg isfst pc ib fin,
+Lemma verify_block_correct dupmap cfg ib: forall pc isfst fin,
    verify_block dupmap cfg isfst pc ib = (OK fin) -> match_iblock dupmap cfg isfst pc ib fin.
 Proof.
   induction ib; intros;
   try (unfold verify_block in H; destruct (cfg!pc) eqn:EQCFG; [ idtac | discriminate; fail ]).
-  - admit.
+  - (* BF *)
+    destruct fi; unfold verify_block in H.
+    + (* Bgoto *)
+      monadInv H.
+      destruct (isfst); simpl in EQ0; inv EQ0.
+      eapply verify_is_copy_correct in EQ.
+      constructor; assumption.
+    + (* Breturn *)
+      destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate.
+      destruct (option_eq _ _ _); try discriminate. inv H.
+      eapply mib_BF; eauto. constructor.
+    + (* Bcall *)
+      destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate.
+      monadInv H.
+      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. subst.
+      inv EQ0. eapply mib_BF; eauto. constructor; assumption.
+    + (* Btailcall *)
+      destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate.
+      destruct (signature_eq _ _); try discriminate.
+      destruct (product_eq _ _ _ _); try discriminate.
+      destruct (list_eq_dec _ _ _); try discriminate. subst.
+      inv H. eapply mib_BF; eauto. constructor.
+    + (* Bbuiltin *)
+      destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate.
+      monadInv H.
+      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. subst.
+      inv EQ0. eapply mib_BF; eauto. constructor; assumption.
+    + (* Bjumptable *)
+      destruct (cfg!pc) eqn:EQCFG; try destruct i; try discriminate.
+      monadInv H.
+      eapply verify_is_copy_list_correct in EQ.
+      destruct (Pos.eq_dec _ _); try discriminate. subst.
+      inv EQ0. eapply mib_BF; eauto. constructor; assumption.
   - (* Bnop *)
     destruct i; inv H.
     constructor; assumption.
@@ -636,10 +746,8 @@ Proof.
     monadInv H.
     destruct x; try discriminate.
     eapply mib_seq_Some.
-    eapply IHib1; eauto. admit.
-    (*eapply IHib2; eauto.*)
-    (*destruct (cfg!pc) eqn:ECFG; try discriminate.*)
-    (*destruct i; try discriminate.*)
+    eapply IHib1; eauto.
+    eapply IHib2; eauto.
   - (* Bcond *)
     destruct i; try discriminate.
     destruct (list_eq_dec _ _ _); try discriminate.
@@ -648,14 +756,8 @@ Proof.
     fold (verify_block dupmap cfg false n0 ib2) in H.
     monadInv H.
     destruct x, x0; try destruct (Pos.eq_dec _ _); try discriminate.
-    + inv EQ2. eapply mib_cond; eauto.
-      admit.
-      admit.
-      admit.
-    + admit.
-    + admit.
-    + admit.
-Admitted.
+    all: inv EQ2; eapply mib_cond; eauto; econstructor.
+Qed.
 Local Hint Resolve verify_block_correct: core.
 
 Fixpoint verify_blocks dupmap (cfg: code) (cfg':RTL.code) l: res unit :=