Trying to finish the bisimu reduce proof for builtin (last case admitted)

1 files changed, 76 insertions, 29 deletions

diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v
index 1bccb5dd..d778ddca 100644
--- a/aarch64/Asmblockdeps.v
+++ b/aarch64/Asmblockdeps.v
@@ -43,12 +43,15 @@ Open Scope impure.
 
 (** auxiliary treatments of builtins *)
 
-Definition has_builtin(bb: bblock): bool :=
- match exit bb with
+Definition is_builtin(ex: option control): bool :=
+ match ex with
  | Some (Pbuiltin _ _ _) => true
  | _ => false
  end.
 
+Definition has_builtin(bb: bblock): bool :=
+ is_builtin (exit bb).
+
 Remark builtin_arg_eq_dreg: forall (a b: builtin_arg dreg), {a=b} + {a<>b}.
 Proof.
   intros.
@@ -74,16 +77,19 @@ Definition assert_same_builtin (bb1 bb2: bblock): ?? unit :=
         else FAILWITH "Different ef in Pbuiltin"
      | _ =>  FAILWITH "Expected a builtin: found something else" (* XXX: on peut raffiner le message d'erreur si nécessaire *)
      end
-  | _ => RET tt (* ok *)
+  | _ => match exit bb2 with
+         | Some (Pbuiltin ef2 lbar2 brr2) => FAILWITH "Expected a something else: found a builtin"
+         | _ => RET tt (* ok *)
+         end
   end.
 
 Lemma assert_same_builtin_correct (bb1 bb2: bblock):
   WHEN assert_same_builtin bb1 bb2 ~> _ THEN
-    has_builtin bb1 = true -> exit bb1 = exit bb2.
+    has_builtin bb1 = true \/ has_builtin bb2 = true -> exit bb1 = exit bb2.
 Proof.
   unfold assert_same_builtin, has_builtin.
-  destruct (exit bb1) as [[]|]; simpl; try (wlp_simplify; congruence).
-  destruct (exit bb2) as [[]|]; wlp_simplify.
+  destruct (exit bb1) as [[]|]; simpl;
+  destruct (exit bb2) as [[]|]; wlp_simplify; try congruence.
 Qed.
 Global Opaque assert_same_builtin.
 Local Hint Resolve assert_same_builtin_correct: wlp.
@@ -1057,7 +1063,7 @@ Definition trans_control (ctl: control) : inst :=
                     (#PC, Op (Control (Obtbl tbl)) (PReg(#r) @ PReg(#PC) @ Enil));
                     (#X16, Op (Constant Vundef) Enil);
                     (#X17, Op (Constant Vundef) Enil)]
-  | Pbuiltin ef args res => [(# PC, Op (Control OError) Enil)]
+  | Pbuiltin ef args res => []
   end.
 
 Definition trans_exit (ex: option control) : L.inst :=
@@ -1937,14 +1943,23 @@ Qed.
 
 Theorem bisimu_exit ex sz rsr mr sr:
   match_states (State rsr mr) sr ->
+  (*is_builtin ex = false ->*)
   match_outcome (estep Ge.(_genv) Ge.(_fn) ex (Ptrofs.repr sz) rsr mr) (inst_run Ge (trans_pcincr sz (trans_exit ex)) sr sr).
 Proof.
   intros MS; unfold estep.
   destruct ex.
   - destruct c.
     + exploit (bisimu_control i sz rsr mr sr); eauto.
-    + simpl; inv MS. unfold control_eval; destruct Ge.
-      replace_pc; rewrite H0. reflexivity.
+    + simpl. inv MS. eexists; split; [| split].
+      unfold control_eval; destruct Ge.
+      replace_pc; rewrite (H0 PC); eauto.
+      rewrite assign_diff; auto.
+      intros rr. unfold incrPC. destruct (PregEq.eq rr PC); subst.
+      * rewrite sr_gss, Pregmap.gss. reflexivity.
+      * rewrite assign_diff, Pregmap.gso; try rewrite H0; try rewrite ppos_discr; auto.
+
+ (*simpl; inv MS. unfold control_eval; destruct Ge.
+      replace_pc; rewrite H0. congruence.*)
   - simpl. inv MS. eexists; split; [| split].
     + unfold control_eval; destruct Ge.
       replace_pc; rewrite (H0 PC); eauto.
@@ -2220,12 +2235,59 @@ Qed.
 Lemma bblock_simu_reduce:
   forall p1 p2,
   L.bblock_simu Ge (trans_block p1) (trans_block p2) ->
-  (has_builtin p1 = true -> exit p1 = exit p2) ->
+  (has_builtin p1 = true \/ has_builtin p2 = true -> exit p1 = exit p2) ->
   Asmblockprops.bblock_simu Ge.(_lk) Ge.(_genv) Ge.(_fn) p1 p2.
 Proof.
   unfold bblock_simu. intros p1 p2 H0 BLT rs m EBB.
   unfold exec_bblock.
-  generalize (H0 (trans_state (State rs m))); clear H0.
+  generalize (bblock_simu_reduce_aux p1 p2 H0).
+  unfold bblock_simu_aux. clear H0.
+  unfold exec_bblock, bbstep. intros H0 m' t0 (rs1 & m1 & H1 & H2).
+  assert ((has_builtin p1 = false /\ has_builtin p2 = false) \/ (has_builtin p1 = true \/ has_builtin p2 = true)). { repeat destruct (has_builtin _); simpl; intuition. }
+  destruct H as [[X1 X2]|H].
+  - (* Not a builtin *)
+    exploit (H0); eauto; erewrite H1; simpl; (*gen*)
+    unfold estep; unfold has_builtin in *.
+    { destruct (exit p1) as [[]|] eqn: EQEX1; try discriminate; simpl in *.
+    inversion H2; subst. rewrite H3; discriminate. }
+    destruct (exit p1) as [[]|] eqn: EQEX1; try discriminate; simpl in *.
+    { inversion H2; subst. rewrite H3.
+    destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.
+    intros H4. eexists; eexists; split; try reflexivity.
+    destruct (exit p2) as [[]|] eqn:EQEX2; simpl in *; try discriminate; try econstructor; eauto.
+    inversion H4. econstructor. }
+    { inversion H2; subst.
+      destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.
+intros H4. eexists; eexists; split; try reflexivity.
+    destruct (exit p2) as [[]|] eqn:EQEX2; simpl in *; try discriminate; try econstructor; eauto.
+    inversion H4. rewrite H3. econstructor. }
+  - (* Builtin *)
+    exploit (BLT); eauto.
+    intros EXIT.
+    unfold has_builtin in H.
+    assert (is_builtin (exit p1) = true). { rewrite <- EXIT in H; intuition. }
+    clear H.
+    generalize (H0 rs m); eauto; erewrite H1; simpl;
+    unfold estep. destruct (exit p1) as [[]|] eqn:EQEX1; try discriminate.
+    rewrite <- EXIT.
+    intros CONTRA.
+    exploit (CONTRA); try discriminate.
+    destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.
+    intros H4. eexists; eexists; split; try reflexivity.
+    inversion H2; subst. inversion H4; subst.
+    econstructor; eauto.
+    + unfold incrPC in H5.
+      replace (rs2 SP) with (rs1 SP).
+      replace (fun r : dreg => rs2 r) with (fun r : dreg => rs1 r); auto.
+      * apply functional_extensionality.
+        intros r; destruct (PregEq.eq r PC); try discriminate.
+        replace (rs1 r) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) r) by auto.
+        rewrite H5; rewrite Pregmap.gso; auto.
+      * replace (rs1 SP) with (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size p1))) SP) by auto.
+        rewrite H5; rewrite Pregmap.gso; auto; try discriminate.
+    + admit.
+    
+(*  generalize (H0 (trans_state (State rs m))); clear H0.
   intros H0 m' t0 (rs1 & m1 & H1 & H2).
   exploit (bisimu Ge rs m (trans_state (State rs m)) p1); eauto.
   exploit (bisimu Ge rs m (trans_state (State rs m)) p2); eauto.
@@ -2248,25 +2310,10 @@ Proof.
     - replace (_m0) with (_m); auto. congruence.
     - apply functional_extensionality. intros r.
       generalize (H1 r). intros Hr. congruence.
-  * discriminate.
-
+  * discriminate.*)
 
-  (*generalize (bblock_simu_reduce_aux p1 p2 H0).*)
-  (*unfold bblock_simu_aux. clear H0.*)
-  (*unfold exec_bblock, bbstep. intros H0 m' t0 (rs1 & m1 & H1 & H2).*)
-  (*generalize (H0 rs m); clear H0. rewrite H1. simpl. unfold estep.*)
-  (*inversion H2.*)
-  (*- intros H6. exploit (H6); try discriminate; clear H6.*)
-    (*destruct (exec_body _ _ (body p2) _ _) as [[rs2 m2]|]; try discriminate.*)
-    (*intros H6. eexists; eexists; split; try reflexivity.*)
-    (*destruct (exit p2) eqn:EQOC.*)
-    (*destruct (c).*)
-    (*+  econstructor; eauto.*)
-    (*+*)
-  (*generalize (H0 (trans_state (State rs m))); clear H0.*)
-  (*intro H0.*)
-
-  (*exploit (*)
+Admitted.
+  
 (*Qed.*)
 
 (** Used for debug traces *)