diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-05 11:10:15 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-05 11:10:49 +0100 |
| commit | 60e11de044fc3fa913e9ce040ee036354eb15659 (patch) | |
| tree | c263b277aac2fef740047c01440e0133b331a039 /mppa_k1c | |
| parent | 9833210392b7bddf740e6b555ce931efb46cf387 (diff) | |
| download | compcert-kvx-60e11de044fc3fa913e9ce040ee036354eb15659.tar.gz compcert-kvx-60e11de044fc3fa913e9ce040ee036354eb15659.zip | |
forward_simu_alt proof Asmblockdeps
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 273ccb68..4912a96f 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1300,11 +1300,16 @@ Proof. - congruence. Qed. -Axiom forward_simu_alt: +Theorem forward_simu_alt: forall rs1 m1 s1' b ge fn, Ge = Genv ge fn -> match_states (State rs1 m1) s1' -> match_outcome (exec_bblock ge fn b rs1 m1) (exec Ge (trans_block b) s1'). +Proof. + intros until fn. intros GENV MS. destruct (exec_bblock _ _ _ _ _) eqn:EXEB. + - eapply forward_simu; eauto. + - eapply forward_simu_stuck; eauto. +Qed. Local Hint Resolve trans_state_match. |