diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-27 17:36:21 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-27 17:36:21 +0100 |
| commit | c4620aef8a80a9ca088493db5558b84bd3561052 (patch) | |
| tree | d2fc8cdd4166b3311803348edb158c2b0c5f54d8 | |
| parent | 2a353a9380100279769d3a0f65a64b3114e3b11a (diff) | |
| download | compcert-kvx-c4620aef8a80a9ca088493db5558b84bd3561052.tar.gz compcert-kvx-c4620aef8a80a9ca088493db5558b84bd3561052.zip | |
Proof of the entire forward simulation (still stuck to do + permutations)
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index a65be8a8..2bd78449 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1773,9 +1773,16 @@ Theorem forward_simu_par_wio_bblock ge fn rsr mr sr rsw mw sw bdy1 bdy2 ex sz rs parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rsr rsw mr mw = Next rs' m' -> parexec_wio_body ge bdy2 rsr rs' mr m' = Next rs2 m2 -> exists s2', - res_eq (Some s2') (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sw sr) + prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sw sr = Some s2' /\ match_states (State rs2 m2) s2'. -Admitted. +Proof. + intros. exploit forward_simu_par_wio_bblock_aux. 4: eapply H2. all: eauto. + intros (s' & RUNAUX & MS'). + exploit forward_simu_par_body. 4: eapply H3. all: eauto. + intros (s'' & RUNBDY2 & MS''). + eexists. split. + eapply prun_iw_app_some. eassumption. eassumption. eassumption. +Qed. Lemma trans_body_perserves_permutation bdy1 bdy2: Permutation bdy1 bdy2 -> @@ -1841,7 +1848,7 @@ Proof. remember (parexec_wio_bblock_aux _ _ _ _ _ _ _ _ _) as pwb. destruct pwb; try congruence. exploit forward_simu_par_wio_bblock; eauto. intros (s2' & PIW & MS'). - unfold prun; eexists; split; eauto. + unfold prun. unfold res_eq. eexists; split; eauto. Qed. Theorem forward_simu_par_stuck: |