[Broken version] Intermediate local commit: pre_output_regs_correct proved

scheduling/RTLpathSchedulerproof.v

@@ -381,12 +381,16 @@ Proof.
     * econstructor; eauto.
     * econstructor; eauto.
       econstructor; eauto.
+      (* wf *)
+      generalize ICHK.
+      unfold inst_checker; simpl in *.
+      destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
+      destruct (list_mem _ _); try congruence.
+      destruct (reg_sum_mem _ _); try congruence.
+      intros EXIT.
+      exploit exit_checker_eqlive_ext1; eauto.
+      intros. destruct H as [p [PATH EQLIVE']].
       econstructor; eauto.
-      - admit. (* wf *)
-      - intros; eapply eqlive_reg_update.
-        (* TODO: condition sur pre_output_regs a revoir *)
-        eapply eqlive_reg_monotonic; eauto; simpl.
-        admit.
  + (* Stailcall *)
     eexists; split.
     * econstructor; eauto.
@@ -394,25 +398,32 @@ Proof.
  + (* Sbuiltin *)
     eexists; split.
     * econstructor; eauto.
-    * econstructor; eauto.
-      - admit. (* wf *)
-      - (* TODO: condition sur pre_output_regs a voir *)
-        (* NB: cas du [regmap_setres] à traiter *)
-        admit.
+    * (* wf *)
+      generalize ICHK.
+      unfold inst_checker; simpl in *.
+      destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
+      destruct (list_mem _ _); try congruence.
+      intros EXIT.
+      exploit exit_checker_eqlive_builtin_res; eauto.
+      intros. destruct H as [p [PATH EQLIVE']].
+      econstructor; eauto.
  + (* Sjumptable *)
     eexists; split.
     * econstructor; eauto.
-    * econstructor; eauto.
-      - admit. (* wf *)
-      - (* TODO: condition sur pre_output_regs a revoir *)
-        eapply eqlive_reg_monotonic; eauto; simpl.
-        admit.
+    * (* wf *)
+      generalize ICHK.
+      unfold inst_checker; simpl in *.
+      destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
+      destruct (Regset.mem _ _); try congruence.
+      destruct (exit_list_checker _ _ _) eqn:EQL; try congruence.
+      exploit exit_list_checker_eqlive; eauto.
+      intros. destruct H as [p [PATH EQLIVE']].
+      econstructor; eauto.
  + (* Sreturn *)
     eexists; split.
     * econstructor; eauto.
     * econstructor; eauto.
-Admitted.
-
+Qed.
 
 (* The main theorem on simulation of symbolic states ! *)
 Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s: