diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-22 15:44:38 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-22 15:44:38 +0100 |
| commit | af3389dbe670eecfaa8ad1a6a2b3ac1454eedfa8 (patch) | |
| tree | 4f278c7c4aa7e14b45bd72339fb9b31d68ab757f /mppa_k1c/PostpassSchedulingproof.v | |
| parent | ad69926edbee2832242d0b991a654cbda66ff367 (diff) | |
| download | compcert-kvx-af3389dbe670eecfaa8ad1a6a2b3ac1454eedfa8.tar.gz compcert-kvx-af3389dbe670eecfaa8ad1a6a2b3ac1454eedfa8.zip | |
Décomposition de la preuve en une forward_simu_par_stuck et une forward_simu_par
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 1fc5c506..57a84480 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -780,7 +780,10 @@ Lemma checked_bundles_are_parexec_equiv f bundle rs rs' m m' o: verify_par_bblock bundle = OK tt -> parexec_bblock (globalenv (semantics tprog)) f bundle rs m o -> o = Next rs' m'. Proof. -Admitted. + intros. unfold verify_par_bblock in H0. destruct (Asmblockdeps.bblock_para_check _) eqn:BPC; try discriminate. clear H0. + simpl in H. simpl in H1. + eapply Asmblockdeps.bblock_para_check_correct; eauto. +Qed. Lemma seqexec_parexec_equiv b ofs f bundle rs rs' m m' o: (* rs PC = Vptr b ofs -> *) (* needed somewhere ? *) |