diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-15 11:49:29 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-15 11:49:29 +0100 |
| commit | fa161ba8b966ee652c7bfd4809334127d1d46089 (patch) | |
| tree | 4510142aff8671dbd96a1879e62b5252886a7a91 /scheduling | |
| parent | 7209e1ba8c6ae100922601b88a9faba5a7ce752f (diff) | |
| download | compcert-kvx-fa161ba8b966ee652c7bfd4809334127d1d46089.tar.gz compcert-kvx-fa161ba8b966ee652c7bfd4809334127d1d46089.zip | |
[Broken version] Proof of hsistate_simu_spec_correct
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/RTLpathSE_simu_specs.v | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/scheduling/RTLpathSE_simu_specs.v b/scheduling/RTLpathSE_simu_specs.v index 03329651..589cf25f 100644 --- a/scheduling/RTLpathSE_simu_specs.v +++ b/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]. |