Merge remote-tracking branch 'machblock/mppa_k1c' into mppa-work

Conflicts:
	mppa_k1c/lib/Asmblockgenproof0.v

2 files changed, 52 insertions, 15 deletions

diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index e0780b9d..89d41017 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -15,6 +15,7 @@ Require Import Asmblock.
 Require Import Asmblockgen.
 Require Import Conventions1.
 Require Import Axioms.
+Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *)
 
 Module MB:=Machblock.
 Module AB:=Asmvliw.
@@ -577,21 +578,6 @@ Definition return_address_offset (f: MB.function) (c: MB.code) (ofs: ptrofs) : P
   transl_blocks f c false = OK tc ->
   code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) tc.
 
-(* NB: these two lemma should go into [Coqlib.v] *) 
-Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2).
-Proof.
-  induction l1; simpl; auto with coqlib.
-Qed.
-Hint Resolve is_tail_app: coqlib.
-
-Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3.
-Proof.
-  induction l1; simpl; auto with coqlib.
-  intros l2 l3 H; inversion H; eauto with coqlib.
-Qed.
-Hint Resolve is_tail_app_inv: coqlib.
-
-
 Lemma transl_blocks_tail:
   forall f c1 c2, is_tail c1 c2 ->
   forall tc2 ep2, transl_blocks f c2 ep2 = OK tc2 ->
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.
+