ugly complete version of liveness proof (I will clean in next commits)

1 files changed, 40 insertions, 34 deletions

diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index 3882639c..a92f24c3 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -277,11 +277,11 @@ Hypothesis all_fundef_liveness_ok: forall b f, Genv.find_funct_ptr ge b = Some f
 
 Local Hint Constructors eqlive_stackframes eqlive_states final_step list_forall2 step: core.
 
-Lemma tr_inputs_eqlive_None f pc ibf rs1 rs2:
+Lemma tr_inputs_eqlive_None f pc tbl ibf rs1 rs2:
   (fn_code f) ! pc = Some ibf ->
   eqlive_reg (ext (input_regs ibf)) rs1 rs2 ->
-  eqlive_reg (ext (input_regs ibf)) (tid f (pc :: nil) None rs1)
-    (tr_inputs f (pc :: nil) None rs2).
+  eqlive_reg (ext (input_regs ibf)) (tid f (pc :: tbl) None rs1)
+    (tr_inputs f (pc :: tbl) None rs2).
 Proof.
   intros PC REGS.
   unfold eqlive_reg. intros r INR.
@@ -439,6 +439,36 @@ Proof.
       simpl; intros; eauto with local.
 Qed.
 
+Lemma tr_inputs_eqlive_list_None tbl: forall f pc n alive ibf rs1 rs2,
+  (*rs1 # arg = Vint n ->*)
+  eqlive_reg (ext alive) rs1 rs2 ->
+  exit_list_checker (fn_code f) alive tbl = true ->
+(*H1 : Regset.mem arg alive = true*)
+  list_nth_z tbl n = Some pc ->
+  (fn_code f) ! pc = Some ibf ->
+  eqlive_reg (ext (input_regs ibf)) rs1 rs2 ->
+  eqlive_reg (ext (input_regs ibf)) (tid f tbl None rs1)
+    (tr_inputs f tbl None rs2).
+Proof.
+  induction tbl as [| pc' tbl IHtbl]; try_simplify_someHyps.
+  autodestruct; try_simplify_someHyps.
+  - intros; eapply tr_inputs_eqlive_None; eauto.
+  - rewrite lazy_and_Some_tt_true in H0.
+    destruct H0 as [EXIT EXIT_REM].
+    intros LIST PC. unfold eqlive_reg.
+    intros r INR.
+    exploit (IHtbl f pc (Z.pred n) alive ibf rs1 rs2); eauto.
+    unfold tid. rewrite !tr_inputs_get.
+    exploit exit_checker_eqlive; eauto.
+    intros (ibf' & PC' & REGS).
+    simpl; rewrite PC'. autodestruct.
+    + intro INRU. apply Regset.mem_2 in INRU.
+      intros EQR. eapply Regset.union_2 in INRU.
+      eapply Regset.mem_1 in INRU. erewrite INRU; auto.
+    + intros. autodestruct.
+      rewrite (H3 r); auto.
+Qed.
+
 Local Hint Resolve tr_inputs_eqlive_None tr_inputs_eqlive_update: core.
 Lemma cfgsem2fsem_finalstep_simu sp f stk1 stk2 s t fin alive rs1 m rs2
   (FSTEP: final_step tid ge stk1 f sp rs1 m fin t s)
@@ -494,37 +524,13 @@ Proof.
       erewrite <- REGS; eauto.
     + repeat (econstructor; simpl; eauto).
 
-(*
-      generalize dependent ibf.
-      generalize dependent n.
-      generalize dependent alive.
-      generalize dependent tbl.
-      induction tbl; simpl; try congruence.
-      intros alive REGS. rewrite lazy_and_Some_tt_true.
-      intros (EXIT & EXIT_REM) INARG n ARG. autodestruct.
-      * try_simplify_someHyps; intros.
-
-  unfold eqlive_reg. intros r INR.
-  unfold tid. rewrite tr_inputs_get.
-  simpl. rewrite PC.
-  exploit Regset.union_3. eapply INR.
-  intros INRU. eapply Regset.mem_1 in INRU.
-  erewrite INRU; eauto.
-
-
-      * try_simplify_someHyps; intros.
-        exploit IHtbl. eapply REGS.
-        eauto. eauto. eauto. eauto.
-        exploit exit_checker_eqlive; eauto.
-    intros (ibf' & PC' & REGS'').
-  unfold eqlive_reg. intros r INR.
-  unfold tid. rewrite tr_inputs_get.
-  simpl. rewrite PC'.
-  exploit Regset.union_3. eapply INR.
-  intros INRU. eapply Regset.mem_1 in INRU.
-  erewrite INRU; eauto.
-   admit.*)
-Admitted.
+      eapply tr_inputs_eqlive_list_None.
+      eapply REGS.
+      eauto.
+      eauto.
+      eauto.
+      eauto.
+Qed.
 
 Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m'
   (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' None)