diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-02-22 13:05:51 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-02-22 13:05:51 +0100 |
commit | a86b505f9c392a558315df2d7acd08e914795f38 (patch) | |
tree | d5758f5127d946f3571b56f783ee89d527212ea8 /mppa_k1c/lib | |
parent | 721a9fa45aa53ed00b201c6f2b3a16713205a2cd (diff) | |
download | compcert-kvx-a86b505f9c392a558315df2d7acd08e914795f38.tar.gz compcert-kvx-a86b505f9c392a558315df2d7acd08e914795f38.zip |
squelette de preuve pour Machblockgenproof.v
Diffstat (limited to 'mppa_k1c/lib')
-rw-r--r-- | mppa_k1c/lib/ForwardSimulationBlock.v | 51 |
1 files changed, 51 insertions, 0 deletions
diff --git a/mppa_k1c/lib/ForwardSimulationBlock.v b/mppa_k1c/lib/ForwardSimulationBlock.v index dc8beb29..39dd2234 100644 --- a/mppa_k1c/lib/ForwardSimulationBlock.v +++ b/mppa_k1c/lib/ForwardSimulationBlock.v @@ -271,6 +271,7 @@ However, the Machblock state after a goto remains "equivalent" to the trans_stat *) + Section ForwardSimuBlock_TRANS. Variable L1 L2: semantics. @@ -320,3 +321,53 @@ Proof. Qed. End ForwardSimuBlock_TRANS. + + +(* another version with a relation [trans_state_R] instead of a function [trans_state] *) +Section ForwardSimuBlock_TRANS_R. + +Variable L1 L2: semantics. + +Variable trans_state_R: state L1 -> state L2 -> Prop. + +Definition match_states_R s1 s2: Prop := + exists s2', trans_state_R s1 s2' /\ equiv_on_next_step _ (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 s2'. + +Lemma match_states_trans_state_R s1 s2: trans_state_R s1 s2 -> match_states_R s1 s2. +Proof. + unfold match_states, equiv_on_next_step. firstorder. +Qed. + +Variable dist_end_block: state L1 -> nat. + +Hypothesis simu_mid_block: + forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). + +Hypothesis public_preserved: + forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. + +Hypothesis match_initial_states: + forall s1, initial_state L1 s1 -> exists s2, match_states_R s1 s2 /\ initial_state L2 s2. + +Hypothesis match_final_states: + forall s1 s2 r, final_state L1 s1 r -> trans_state_R s1 s2 -> final_state L2 s2 r. + +Hypothesis final_states_end_block: + forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. + +Hypothesis simu_end_block: + forall s1 t s1' s2, starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> trans_state_R s1 s2 -> exists s2', Step L2 s2 t s2' /\ match_states_R s1' s2'. + +Lemma forward_simulation_block_trans_R: forward_simulation L1 L2. +Proof. + eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states_R); try tauto. + + (* final_states *) intros s1 s2 r H1 (s2' & H2 & H3 & H4). rewrite H4; eauto. + + (* simu_end_block *) + intros s1 t s1' s2 H1 (s2' & H2 & H2a & H2b). exploit simu_end_block; eauto. + intros (x & Hx & (y & H3 & H4 & H5)). repeat (econstructor; eauto). + rewrite H2a; eauto. + inversion_clear H1. eauto. +Qed. + +End ForwardSimuBlock_TRANS_R. + |