Machblock: adaptation to the generalized ForwardSimulationBlock

1 files changed, 103 insertions, 8 deletions

diff --git a/driver/ForwardSimulationBlock.v b/driver/ForwardSimulationBlock.v
index 8c1fcb08..a9569e08 100644
--- a/driver/ForwardSimulationBlock.v
+++ b/driver/ForwardSimulationBlock.v
@@ -1,6 +1,7 @@
 (***
 
-Variante de Forward Simulation pour les blocks.
+Auxiliary lemmas on starN and forward_simulation 
+in order to prove the forward simulation of Mach -> Machblock. 
 
 ***)
 
@@ -15,16 +16,36 @@ Require Import Smallstep.
 Local Open Scope nat_scope.
 
 
-Section ForwardSimuBlock.
+(** Auxiliary lemma on starN *)
+Section starN_lemma.
 
-Variable L1 L2: semantics.
+Variable L: semantics.
 
-Local Hint Resolve starN_refl starN_step.
+Local Hint Resolve starN_refl starN_step Eapp_assoc.
+
+Lemma starN_split n s t s':
+  starN (step L) (globalenv L) n s t s' ->
+  forall m k, n=m+k ->
+  exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2.
+Proof.
+  induction 1; simpl.
+  + intros m k H; assert (X: m=0); try omega.
+    assert (X0: k=0); try omega.
+    subst; repeat (eapply ex_intro); intuition eauto.
+  + intros m; destruct m as [| m']; simpl.
+    - intros k H2; subst; repeat (eapply ex_intro); intuition eauto.
+    - intros k H2. inversion H2.
+      exploit (IHstarN m' k); eauto. intro.
+      destruct H3 as (t5 & t6 & s0 & H5 & H6 & H7).
+      repeat (eapply ex_intro).
+      instantiate (1 := t6); instantiate (1 := t1 ** t5); instantiate (1 := s0).
+      intuition eauto. subst. auto.
+Qed.
 
 Lemma starN_last_step n s t1 s': 
-  starN (step L1) (globalenv L1) n s t1 s' ->
+  starN (step L) (globalenv L) n s t1 s' ->
   forall (t t2:trace) s'',
-     Step L1 s' t2 s'' -> t = t1 ** t2 -> starN (step L1) (globalenv L1) (S n) s t s''.
+     Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''.
 Proof.
   induction 1; simpl. 
   + intros t t1 s0; autorewrite with trace_rewrite.
@@ -34,6 +55,17 @@ Proof.
     intros; subst; autorewrite with trace_rewrite; auto.
 Qed.
 
+End starN_lemma.
+
+
+
+(** General scheme from a "match_states" relation *)
+
+Section ForwardSimuBlock_REL.
+
+Variable L1 L2: semantics.
+
+
 (** Hypothèses de la preuve *)
 
 Variable dist_end_block: state L1 -> nat.
@@ -61,6 +93,8 @@ Hypothesis simu_end_block:
 
 (** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *)
 
+Local Hint Resolve starN_refl starN_step.
+
 Definition star_in_block (head current: state L1): Prop :=
   dist_end_block head >= dist_end_block current 
   /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. 
@@ -216,7 +250,7 @@ Proof.
       * unfold head; rewrite H2; simpl. intuition eauto. 
 Qed.
 
-Lemma forward_simulation_block: forward_simulation L1 L2.
+Lemma forward_simulation_block_rel: forward_simulation L1 L2.
 Proof.
   eapply compose_forward_simulations.
   eapply forward_memo_simulation_1.
@@ -224,4 +258,65 @@ Proof.
 Qed.
 
 
-End ForwardSimuBlock.
\ No newline at end of file
+End ForwardSimuBlock_REL.
+
+
+
+(* An instance of the previous scheme, when there is a translation from L1 states to L2 states 
+
+Here, we do not require that the sequence of S2 states does exactly match the sequence of L1 states by trans_state.
+This is because the exact matching is broken in Machblock on "goto" instruction (due to the find_label).
+
+However, the Machblock state after a goto remains "equivalent" to the trans_state of the Mach state in the sense of "equiv_on_next_step" below...
+
+*)
+
+Section ForwardSimuBlock_TRANS.
+
+Variable L1 L2: semantics.
+
+Variable trans_state: state L1 -> state L2.
+
+Definition equiv_on_next_step (P Q: Prop) s2_a s2_b: Prop := 
+  (P -> (forall t s', Step L2 s2_a t s' <-> Step L2 s2_b t s')) /\ (Q -> (forall r, (final_state L2 s2_a r) <-> (final_state L2 s2_b r))).
+
+Definition match_states s1 s2: Prop :=
+  equiv_on_next_step (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 (trans_state s1).
+
+Lemma match_states_trans_state s1: match_states s1 (trans_state s1).
+Proof.
+  unfold match_states, equiv_on_next_step. intuition.
+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 s1 s2 /\ initial_state L2 s2.
+
+Hypothesis match_final_states:
+  forall s1 r, final_state L1 s1 r -> final_state L2 (trans_state s1) 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', starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> exists s2', Step L2 (trans_state s1) t s2' /\ match_states s1' s2'.
+
+Lemma forward_simulation_block_trans: forward_simulation L1 L2.
+Proof.
+  eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states); try tauto.
+  + (* final_states *) intros s1 s2 r H1 [H2 H3]. rewrite H3; eauto.
+  + (* simu_end_block *)
+    intros s1 t s1' s2 H1 [H2a H2b]. exploit simu_end_block; eauto.
+    intros (s2' & H3 & H4); econstructor 1; intuition eauto.
+    rewrite H2a; auto.
+    inversion_clear H1. eauto.
+Qed.
+
+End ForwardSimuBlock_TRANS.
\ No newline at end of file