[Broken version] Intermediate local commit: proof of siexec_snone_por in scheduler proof

2 files changed, 68 insertions, 18 deletions

diff --git a/scheduling/RTLpathLivegenproof.v b/scheduling/RTLpathLivegenproof.v
index 968077a9..861bcfab 100644
--- a/scheduling/RTLpathLivegenproof.v
+++ b/scheduling/RTLpathLivegenproof.v
@@ -600,14 +600,14 @@ Qed.
 Lemma final_inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1:
   list_forall2 eqlive_stackframes stk1 stk2 ->
   eqlive_reg (ext alive) rs1 rs2 -> 
-  eqlive_reg (ext por) rs1 rs2 -> 
+  Regset.Subset por alive ->
   liveness_ok_function f ->
   (fn_code f) ! pc = Some i ->
   path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
   final_inst_checker (fn_path f) alive por i = Some tt -> 
   exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
-Proof. Admitted. (*
-  intros STACKS EQLIVE LIVENESS PC; 
+Proof.
+  intros STACKS EQLIVE SUB LIVENESS PC; 
   destruct 1 as [i' sp pc rs1 m st1|
                  sp pc rs1 m sig ros args res pc' fd|
                  st1 pc rs1 m sig ros args fd m'|
@@ -621,6 +621,7 @@ Proof. Admitted. (*
   + (* Icall *)
     repeat inversion_ASSERT. intros.
     exploit exit_checker_eqlive_ext1; eauto.
+    eapply eqlive_reg_monotonic; eauto.
     intros (path & PATH & EQLIVE2).
     eexists; split.
     - eapply exec_Icall; eauto.
@@ -640,6 +641,7 @@ Proof. Admitted. (*
   + (* Ibuiltin *)
     repeat inversion_ASSERT. intros.
     exploit exit_checker_eqlive_builtin_res; eauto.
+    eapply eqlive_reg_monotonic; eauto.
     intros (path & PATH & EQLIVE2).
     eexists; split.
     - eapply exec_Ibuiltin; eauto.
@@ -649,6 +651,7 @@ Proof. Admitted. (*
   + (* Ijumptable *)
     repeat inversion_ASSERT. intros.
     exploit exit_list_checker_eqlive; eauto.
+    eapply eqlive_reg_monotonic; eauto.
     intros (path & PATH & EQLIVE2).
     eexists; split.
     - eapply exec_Ijumptable; eauto.
@@ -662,8 +665,9 @@ Proof. Admitted. (*
       * erewrite (EQLIVE r); eauto.
         eapply eqlive_states_return; eauto.
       * eapply eqlive_states_return; eauto.
-     Qed.*)
+Qed.
 
+(* TODO useless?
 Lemma subset_contra: forall por alive inputs,
   Regset.Subset por alive ->
   Regset.subset inputs alive = false ->
@@ -736,7 +740,7 @@ Proof.
       intros CONTRA; inv CONTRA.
   - exploit (exit_list_checker_subset_contra por alive f l); eauto;
     intros CONTRA; inv CONTRA.
-Qed.
+Qed.*)
 
 Lemma inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1:
   list_forall2 eqlive_stackframes stk1 stk2 ->
@@ -774,7 +778,6 @@ Proof.
       eapply eqlive_states_intro; eauto.
   + inversion_ASSERT.
     intros; exploit final_inst_checker_eqlive; eauto.
-    eapply final_inst_checker_trans; eauto.
 Qed.
 
 Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2:
diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v
index 026c1425..8d2eff6d 100644
--- a/scheduling/RTLpathSchedulerproof.v
+++ b/scheduling/RTLpathSchedulerproof.v
@@ -288,6 +288,61 @@ Proof.
     erewrite iinst_checker_default_succ; eauto.
 Qed.
 
+Lemma siexec_snone_por_correct rs' is t s alive path0 i sp s0 st0 stk stk' f rs0 m0: forall
+  (SSEM2 : ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone
+          (irs is) (imem is) t s)
+  (SIEXEC : siexec_inst i st0 = Some s0)
+  (ICHK : inst_checker (fn_path f) alive (pre_output_regs path0) i = Some tt),
+  (liveness_ok_function f) ->
+  list_forall2 match_stackframes stk stk' ->
+  eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
+  exists s' : state,
+    ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone rs' (imem is) t s' /\
+    eqlive_states s s'.
+Proof.
+  Local Hint Resolve eqlive_stacks_refl: core.
+  intros ? ? ? LIVE STK EQLIVE.
+  inversion SSEM2; subst; clear SSEM2.
+  eexists; split.
+  * econstructor.
+  * generalize ICHK.
+    unfold inst_checker. destruct i; simpl in *;
+    unfold exit_checker; try discriminate.
+    all:
+      try destruct (list_mem _ _); simpl;
+      try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence; fail).
+    4,5:
+      destruct (Regset.mem _ _); destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
+    1,2,3,4: assert (NPC: n=(si_pc s0)).
+    all: try (inv SIEXEC; simpl; auto; fail).
+    1,2,3,4:
+      try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence);
+      simpl; inversion_SOME p;
+      destruct (Regset.subset (input_regs p) (pre_output_regs path0)) eqn:SUB_PATH; try congruence;
+      intros NPATH _; econstructor; eauto;
+      try (instantiate (1:=p); rewrite <- NPC; auto; fail).
+    1,2,3,4:
+      eapply eqlive_reg_monotonic; eauto; simpl;
+      intros; apply Regset.subset_2 in SUB_PATH;
+      unfold Regset.Subset in SUB_PATH;
+      apply SUB_PATH in H; auto.
+    assert (NPC: n0=(si_pc s0)). { inv SIEXEC; simpl; auto. }
+    inversion_SOME p.
+    2: { destruct (Regset.subset _ _) eqn:?; try congruence. }
+    destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
+    2: { destruct (Regset.subset (pre_output_regs path0) alive) eqn:?; try congruence. }
+    simpl.
+    destruct (Regset.subset (pre_output_regs path0) alive) eqn:SUB_ALIVE'; try congruence.
+    inversion_SOME p'.
+    destruct (Regset.subset (input_regs p') (pre_output_regs path0)) eqn:SUB_PATH; try congruence.
+    intros NPATH NPATH' _. econstructor; eauto.
+    instantiate (1:=p'). rewrite <- NPC; auto.
+    eapply eqlive_reg_monotonic; eauto; simpl.
+    intros. apply Regset.subset_2 in SUB_PATH.
+    unfold Regset.Subset in SUB_PATH.
+    apply SUB_PATH in H; auto.
+Qed.
+
 Lemma pre_output_regs_correct f pc0 path0 stk stk' sp (st:sstate) rs0 m0 t s is rs':
   (liveness_ok_function f) ->
   (fn_path f) ! pc0 = Some path0 ->
@@ -317,18 +372,10 @@ Proof.
   clear DEFSUCC. destruct res as [alive pc1]. simpl in *.
   try_simplify_someHyps.
   destruct (siexec_inst i st0) eqn: SIEXEC; try_simplify_someHyps; intros.
-  { (* Snone *)
-    inversion SSEM2; subst; clear SSEM2.
-    eexists; split.
-    * econstructor.
-    * econstructor; eauto.
-      - admit. (* wf *)
-      - (* TODO: condition sur pre_output_regs a revoir *)
-        eapply eqlive_reg_monotonic; eauto; simpl.
-        admit.
- }
- destruct i; try_simplify_someHyps; try congruence;
- inversion SSEM2; subst; clear SSEM2; simpl in *.
+  (* Snone *)
+  eapply siexec_snone_por_correct; eauto.
+  destruct i; try_simplify_someHyps; try congruence;
+  inversion SSEM2; subst; clear SSEM2; simpl in *.
  + (* Scall *)
     eexists; split.
     * econstructor; eauto.