bblock_equiv_reduce Asmblockdeps.v

1 files changed, 42 insertions, 4 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 80383c2f..bb800b99 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -10,6 +10,7 @@ Require Import Floats.
 Require Import ZArith.
 Require Import Coqlib.
 Require Import ImpDep.
+Require Import Axioms.
 
 Open Scope impure.
 
@@ -648,6 +649,12 @@ Definition match_states (s: Asmblock.state) (s': state) :=
      s' pmem = Memstate m
   /\ forall r, s' (#r) = Val (rs r).
 
+Definition match_outcome (o:outcome) (s: option state) :=
+  match o with
+  | Next rs m => exists s', s=Some s' /\ match_states (State rs m) s'
+  | Stuck => s=None
+  end.
+ 
 Notation "a <[ b <- c ]>" := (assign a b c) (at level 102, right associativity).
 
 Definition trans_state (s: Asmblock.state) : state :=
@@ -673,12 +680,13 @@ Qed.
 Lemma not_eq_add:
   forall k n n', n <> n' -> k + n <> k + n'.
 Proof.
-Admitted. (* FIXME - help Sylvain ? *)
+  intros k n n' H1 H2. apply H1; clear H1. eapply Pos.add_reg_l; eauto.
+Qed.
 
 Lemma not_eq_ireg_to_pos:
   forall n r r', r' <> r -> n + ireg_to_pos r <> n + ireg_to_pos r'.
 Proof.
-  intros. destruct r; destruct r'; try contradiction; apply not_eq_add; discriminate. (* FIXME - quite long to prove *)
+  intros. destruct r; destruct r'; try contradiction; apply not_eq_add; discriminate.
 Qed.
 
 Lemma not_eq_ireg_ppos: 
@@ -1268,12 +1276,42 @@ Proof.
   - congruence.
 Qed.
 
+Axiom 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').
 
-Axiom bblock_equiv_reduce: 
+Local Hint Resolve trans_state_match.
+
+Lemma bblock_equiv_reduce: 
   forall p1 p2 ge fn,
   Ge = Genv ge fn ->
   L.bblock_equiv Ge (trans_block p1) (trans_block p2) ->
-  Asmblockgenproof0.bblock_equiv ge fn p1 p2. (* FIXME *)
+  Asmblockgenproof0.bblock_equiv ge fn p1 p2.
+Proof.
+  unfold bblock_equiv, res_eq; intros p1 p2 ge fn H1 H2; constructor.
+  intros rs m.
+  generalize (H2 (trans_state (State rs m))); clear H2.
+  intro H2. 
+  exploit (forward_simu_alt rs m (trans_state (State rs m)) p1 ge fn); eauto.
+  exploit (forward_simu_alt rs m (trans_state (State rs m)) p2 ge fn); eauto.
+  remember (exec_bblock ge fn p1 rs m) as exp1.
+  destruct exp1.
+  + (* Next *) 
+    intros H3 (s2' & exp2 & MS'). unfold exec in exp2, H3. rewrite exp2 in H2.
+    destruct H2 as (m2' & H2 & H4). rewrite H2 in H3.
+    destruct (exec_bblock ge fn p2 rs m); simpl in H3.
+    * destruct H3 as (s' & H3 & H5 & H6). inv H3. inv MS'.
+      cutrewrite (rs0=rs1).
+      - cutrewrite (m0=m1); auto. congruence.
+      - apply functional_extensionality. intros r.
+        generalize (H0 r). intros Hr. congruence.
+    * discriminate.
+  + intros MO MO2. remember (trans_state (State rs m)) as s1. inversion MO2. clear MO2. unfold exec in *.
+    rewrite H0 in H2. clear H0. destruct (exec_bblock ge fn p2 rs m); auto. rewrite H2 in MO. unfold match_outcome in MO.
+    destruct MO as (? & ? & ?). discriminate.
+Qed.
 
 Definition string_of_name (x: P.R.t): ?? pstring := RET (Str ("resname")).
 (*   match x with