[Broken version] Proof of hsistate_simu_spec_correct

scheduling/RTLpathSE_simu_specs.v

@@ -638,15 +638,18 @@ Proof.
   unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
   - destruct SEMI as (SSEML & PCEQ & ALLFU).
     exploit hsilocal_simu_spec_correct; eauto; [apply ctx|]. simpl. intro SSEML2.
-    exists (mk_istate (icontinue is1) (si_pc st2) (irs is1) (imem is1)). constructor.
-    + unfold ssem_internal. simpl. rewrite ICONT. admit.
-      (* constructor; [assumption | constructor; [reflexivity |]].
+    exists (mk_istate (icontinue is1) (si_pc st2) (seval_partial_regset (the_ge2 ctx) (the_sp ctx) 
+              (the_rs0 ctx) (the_m0 ctx) (hsi_local hst2)) (imem is1)). constructor.
+    + unfold ssem_internal. simpl. rewrite ICONT.
+      destruct SSEML2 as [SSEMLP EQLIVE].
+      constructor; [assumption | constructor; [reflexivity |]].
       eapply siexits_simu_all_fallthrough; eauto.
       * eapply hsiexits_simu_siexits; eauto.
       * eapply nested_sok_prop; eauto.
-        eapply ssem_local_sok; eauto. *)
-    + unfold istate_simu. rewrite ICONT. constructor; [simpl; assumption | constructor; [| reflexivity]].
-      constructor.
+        eapply ssem_local_sok; eauto.
+    + unfold istate_simu. rewrite ICONT.
+      destruct SSEML2 as [SSEMLP EQLIVE].
+      constructor; simpl; auto.
   - destruct SEMI as (ext & lx & SSEME & ALLFU).
     assert (SESIMU: siexits_simu dm f outframe (si_exits st1) (si_exits st2) ctx) by (eapply hsiexits_simu_siexits; eauto).
     exploit siexits_simu_all_fallthrough_upto; eauto.
@@ -668,7 +671,7 @@ Proof.
       + unfold istate_simu in *. rewrite ICONT in *. destruct ISIMU as (path & PATHEQ & ISIMULIVE & DMEQ).
         destruct ISIMULIVE as (CONTEQ & REGEQ & MEMEQ).
         exists path. repeat (constructor; auto).
-Admitted.
+Qed.
 
 
 (** ** Specification of the simulation test on [sfval].