Try to work on refining the match_states predicate

1 files changed, 22 insertions, 9 deletions

diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index f4e88b9..6e4138b 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -220,6 +220,12 @@ the basic block.
       ~ imm_succ pc pc' ->
       exists b, tc ! pc' = Some b /\ match_block c pc b.(bb_body) b.(bb_exit).
 
+  Definition match_code2' (c: RTL.code) (tc: code) : Prop :=
+    forall i pc pc',
+      c ! pc = Some i ->
+      In pc' (RTL.successors_instr i) ->
+      imm_succ pc pc' ->
+      exists b, tc ! pc' = Some b /\ match_block c pc b.(bb_body) b.(bb_exit).
 
   Variant match_stackframe : RTL.stackframe -> stackframe -> Prop :=
     | match_stackframe_init :
@@ -252,10 +258,8 @@ whole execution (in one big step) of the basic block.
       forall stk stk' f tf sp pc rs m pc0 b rs0 m0
         (TF: transl_function f = OK tf)
         (CODE: match_code' f.(RTL.fn_code) tf.(fn_code))
-        (BLOCK: forall i b',
-            f.(RTL.fn_code) ! pc = Some i ->
-            tf.(fn_code) ! pc0 = Some b' ->
-            match_block f.(RTL.fn_code) pc b b'.(bb_exit))
+        (BLOCK: exists b',
+            tf.(fn_code) ! pc0 = Some b' /\ match_block f.(RTL.fn_code) pc b b'.(bb_exit))
         (STK: Forall2 match_stackframe stk stk')
         (STARSIMU: Smallstep.star RTL.step ge (RTL.State stk f sp pc0 rs0 m0)
                                   E0 (RTL.State stk f sp pc rs m))
@@ -358,7 +362,6 @@ whole execution (in one big step) of the basic block.
       (RTL.fn_code f) ! pc = Some (RTL.Inop pc') ->
       match_states (Some (RBnop :: nil)) (RTL.State s f sp pc rs m)
                    (State stk' tf sp pc1 rs1 (PMap.init false) m1) ->
-      find_block_spec (fn_code tf) pc pc1 ->
       (fn_code tf) ! pc1 = Some x ->
       match_block (RTL.fn_code f) pc1 (bb_body x) (bb_exit x) ->
       RBgoto pc' = bb_exit x ->
@@ -368,7 +371,7 @@ whole execution (in one big step) of the basic block.
         Smallstep.star step tge (State stk' tf sp pc1 rs1 (PMap.init false) m1) E0 s2' /\
           match_states b' (RTL.State s f sp pc' rs m) s2'.
   Proof.
-    intros * H H0 H2 H1 H4 H5 H8 H6.
+    intros * H H0 H1 H4 H5 H8 H6.
     inv H0.
     do 3 econstructor. apply Smallstep.star_one. econstructor.
     eassumption. eapply BB; [econstructor; constructor | eassumption].
@@ -378,6 +381,12 @@ whole execution (in one big step) of the basic block.
   (*   apply Smallstep.star_refl. admit. *)
   (* Admitted. *)
 
+  Definition imm_succ_dec pc pc' : {imm_succ pc pc'} + {~ imm_succ pc pc'}.
+  Proof.
+    unfold imm_succ. pose proof peq.
+    decide equality.
+  Defined.
+
   Lemma transl_Inop_correct:
     forall s f sp pc rs m pc',
       (RTL.fn_code f) ! pc = Some (RTL.Inop pc') ->
@@ -388,9 +397,13 @@ whole execution (in one big step) of the basic block.
     intros s f sp pc rs m pc' H.
     inversion 1; subst; simplify.
     unfold match_code' in *.
-    pose proof (CODE _ _ H) as X. simplify.
-    pose proof (BLOCK _ _ H H1); simplify. inv H3; crush;
-    eauto using transl_Inop_correct_nj, transl_Inop_correct_j.
+    assert (X1: In pc' (RTL.successors_instr (RTL.Inop pc'))) by (crush).
+    destruct (imm_succ_dec pc pc').
+    { admit. }
+    { pose proof (CODE _ _ pc' H X1 n) as X. simplify.
+      inv H3; crush. admit.
+      eapply transl_Inop_correct_j; eauto.
+      eauto using transl_Inop_correct_nj, transl_Inop_correct_j. }
   Qed.
 
   Lemma transl_Iop_correct: