diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-09-03 11:51:14 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-09-03 11:51:14 +0200 |
| commit | 0fef148ea767281afc3fb8248bee0420f431f9aa (patch) | |
| tree | c05cd29f03be05436a9ec982f372ac0f808c0535 /kvx | |
| parent | 536c51538de614e0fc6bf9476898615673f9463e (diff) | |
| download | compcert-kvx-0fef148ea767281afc3fb8248bee0420f431f9aa.tar.gz compcert-kvx-0fef148ea767281afc3fb8248bee0420f431f9aa.zip | |
More proofs
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/lib/RTLpathSE_impl.v | 40 |
1 files changed, 32 insertions, 8 deletions
diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v index e7efa3ec..e173aa6c 100644 --- a/kvx/lib/RTLpathSE_impl.v +++ b/kvx/lib/RTLpathSE_impl.v @@ -1235,9 +1235,12 @@ Lemma hsiexec_inst_correct_stat i hst hst' st: exists st', siexec_inst i st = Some st' /\ (hsistate_refines_stat hst st -> hsistate_refines_stat hst' st'). Proof. - destruct i; simpl; intros STEPI; inversion_clear STEPI; discriminate || eexists; split; eauto. - (* TODO *) -Admitted. + destruct i; simpl; intros STEPI; inversion_clear STEPI; discriminate || eexists; split; eauto. + intros HREF. constructor; [simpl; reflexivity|]. simpl. + destruct HREF as (PCEQ & EXREF). + constructor; [|assumption]. clear EXREF. + constructor. +Qed. Lemma refines_okargs ge sp rs0 m0 hst st l: hsistate_refines_dyn ge sp rs0 m0 hst st -> @@ -1312,22 +1315,43 @@ Fixpoint hsiexec_path (path:nat) (f: function) (hst: hsistate): option hsistate hsiexec_path p f hst1 end. -Lemma hsiexec_path_correct_stat ps f hst hst' st: +Lemma hsiexec_path_correct_stat f ps: forall hst hst', hsiexec_path ps f hst = Some hst' -> - hsistate_refines_stat hst st -> + forall st, hsistate_refines_stat hst st -> exists st', siexec_path ps f st = Some st' /\ hsistate_refines_stat hst' st'. Proof. -Admitted. + induction ps. + - simpl. intros. inv H. repeat (econstructor; eauto). + - simpl. intros hst hst' EPATH st HREF. + destruct HREF as (PCREF & EXREF). rewrite <- PCREF. + destruct ((fn_code f) ! (hsi_pc hst)); [|discriminate]. + destruct (hsiexec_inst i hst) eqn:HSI; [|discriminate]. + eapply (hsiexec_inst_correct_stat _ _ _ st) in HSI. destruct HSI as (st' & SI' & HREF'). + lapply HREF'; [|constructor; assumption]. clear HREF'. intro HREF'. + eapply IHps in EPATH; eauto. destruct EPATH as (st'' & SIPATH & HREF''). + exists st''. constructor; [|assumption]. + rewrite SI'. assumption. +Qed. -Lemma hsiexec_path_correct_dyn ge sp rs0 m0 ps f hst hst' st st': +Lemma hsiexec_path_correct_dyn ge sp rs0 m0 f: forall ps hst hst', hsiexec_path ps f hst = Some hst' -> + forall st st', siexec_path ps f st = Some st' -> hsistate_refines_stat hst st -> hsistate_refines_stat hst' st' -> hsistate_refines_dyn ge sp rs0 m0 hst st -> hsistate_refines_dyn ge sp rs0 m0 hst' st'. Proof. -Admitted. + induction ps; [simpl; intros; congruence|]. + intros hst hst' HPATH st st' SPATH HSTAT HSTAT' HDYN. + simpl in *. destruct HSTAT as (PCREF & EXREF). rewrite <- PCREF in SPATH. + destruct ((fn_code f) ! (hsi_pc hst)); [|discriminate]. + destruct (hsiexec_inst i hst) eqn:HSI; [|discriminate]. + exploit hsiexec_inst_correct_stat; eauto. intros (s & SI & HREF). + lapply HREF; [|constructor; eassumption]. clear HREF. intro HREF. + rewrite SI in SPATH. + eapply hsiexec_inst_correct_dyn in HSI; eauto. +Qed. Definition hsexec_final (i: instruction) (prev: hsistate_local): sfval := |