maj forward_simu_par_wio_bblock_aux en forward_simu_par_wio

  avec une legere simplification (comme dans le papier)

2 files changed, 19 insertions, 21 deletions

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index b11a77ff..a8f81be6 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1081,14 +1081,13 @@ Qed.
 
 Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil).
 
-Theorem forward_simu_par_wio_bblock_aux ge fn rsr mr sr rsw mw sw bdy ex sz:
+Theorem forward_simu_par_wio ge fn rsr mr sr bdy ex sz:
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
-  match_states (State rsw mw) sw ->
-  match_outcome (parexec_wio_bblock_aux ge fn bdy ex (Ptrofs.repr sz) rsr rsw mr mw) (prun_iw Ge (trans_block_aux bdy sz ex) sw sr).
+  match_outcome (parexec_wio ge fn bdy ex (Ptrofs.repr sz) rsr mr) (prun_iw Ge (trans_block_aux bdy sz ex) sr sr).
 Proof.
-  intros GENV MSR MSW. unfold parexec_wio_bblock_aux, trans_block_aux.
-  exploit (forward_simu_par_body bdy ge fn rsr mr sr rsw mw sw); eauto.
+  intros GENV MSR. unfold parexec_wio, trans_block_aux.
+  exploit (forward_simu_par_body bdy ge fn rsr mr sr rsr mr sr); eauto.
   destruct (parexec_wio_body _ _ _ _ _ _); simpl.
   - intros (s' & X1 & X2).
     erewrite prun_iw_app_Some; eauto.
@@ -1098,20 +1097,19 @@ Proof.
   - intros X; erewrite prun_iw_app_None; eauto.
 Qed.
 
-Theorem forward_simu_par_wio_bblock ge fn rsr rsw mr sr sw mw bdy1 bdy2 ex sz:
+Theorem forward_simu_par_wio_bblock ge fn rsr mr sr bdy1 bdy2 ex sz:
   Ge = Genv ge fn ->
   match_states (State rsr mr) sr ->
-  match_states (State rsw mw) sw ->
   match_outcome 
-   match parexec_wio_bblock_aux ge fn bdy1 ex (Ptrofs.repr sz) rsr rsw mr mw with
+   match parexec_wio ge fn bdy1 ex (Ptrofs.repr sz) rsr mr with
    | Next rs' m' => parexec_wio_body ge bdy2 rsr rs' mr m'
    | Stuck => Stuck
    end
-   (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sw sr).
+   (prun_iw Ge ((trans_block_aux bdy1 sz ex)++(trans_body bdy2)) sr sr).
 Proof.
   intros.
-  exploit (forward_simu_par_wio_bblock_aux ge fn rsr mr sr rsw mw sw bdy1 ex sz); eauto.
-  destruct (parexec_wio_bblock_aux _ _ _ _ _ _); simpl.
+  exploit (forward_simu_par_wio ge fn rsr mr sr bdy1 ex sz); eauto.
+  destruct (parexec_wio _ _ _ _ _ _); simpl.
   - intros (s' & X1 & X2).
     erewrite prun_iw_app_Some; eauto.
     eapply forward_simu_par_body; eauto.
@@ -1157,7 +1155,7 @@ Proof.
   inversion PAREXEC as (bdy1 & bdy2 & PERM & WIO).
   exploit trans_block_perserves_permutation; eauto.
   intros Perm.
-  exploit (forward_simu_par_wio_bblock ge fn rs1 rs1 m1 s1' s1' m1 bdy1 bdy2 (exit b) (size b)); eauto.
+  exploit (forward_simu_par_wio_bblock ge fn rs1 m1 s1' bdy1 bdy2 (exit b) (size b)); eauto.
   rewrite <- WIO. clear WIO.
   intros H; eexists; split. 2: eapply H.
   unfold prun; eexists; split; eauto. 
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index bb6b7132..c5b7db45 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -148,7 +148,7 @@ Definition gpreg_o_expand (x : gpreg_o) : gpreg * gpreg * gpreg * gpreg :=
   | R56R57R58R59 => (GPR56, GPR57, GPR58, GPR59)
   | R60R61R62R63 => (GPR60, GPR61, GPR62, GPR63)
   end.
-    
+
 Lemma gpreg_o_eq : forall (x y : gpreg_o), {x=y} + {x<>y}.
 Proof. decide equality. Defined.
 
@@ -1553,16 +1553,16 @@ Definition incrPC size_b (rs: regset) :=
 Definition parexec_exit (f: function) ext size_b (rsr rsw: regset) (mw: mem) 
   := parexec_control f ext (incrPC size_b rsr) rsw mw.
 
-Definition parexec_wio_bblock_aux f bdy ext size_b (rsr rsw: regset) (mr mw: mem): outcome :=
-  match parexec_wio_body bdy rsr rsw mr mw with
-  | Next rsw mw => parexec_exit f ext size_b rsr rsw mw
+Definition parexec_wio f bdy ext size_b (rs: regset) (m: mem): outcome :=
+  match parexec_wio_body bdy rs rs m m with
+  | Next rsw mw => parexec_exit f ext size_b rs rsw mw
   | Stuck => Stuck
   end.
 
 (** non-deterministic (out-of-order writes) parallel execution of bundles *)
 Definition parexec_bblock (f: function) (bundle: bblock) (rs: regset) (m: mem) (o: outcome): Prop :=
    exists bdy1 bdy2, Permutation (bdy1++bdy2) (body bundle) /\ 
-      o=match parexec_wio_bblock_aux f bdy1 (exit bundle) (Ptrofs.repr (size bundle)) rs rs m m with
+      o=match parexec_wio f bdy1 (exit bundle) (Ptrofs.repr (size bundle)) rs m with
       | Next rsw mw => parexec_wio_body bdy2 rs rsw m mw
       | Stuck => Stuck
       end.
@@ -1689,7 +1689,7 @@ Inductive step: state -> trace -> state -> Prop :=
 
 (** parallel in-order writes execution of bundles *)
 Definition parexec_wio_bblock (f: function) (b: bblock) (rs: regset) (m: mem): outcome :=
-  parexec_wio_bblock_aux f (body b) (exit b) (Ptrofs.repr (size b)) rs rs m m.
+  parexec_wio f (body b) (exit b) (Ptrofs.repr (size b)) rs m.
 
 
 Lemma parexec_bblock_write_in_order f b rs m:
@@ -1699,7 +1699,7 @@ Proof.
    constructor 1.
    - rewrite app_nil_r; auto.
    - unfold parexec_wio_bblock.
-     destruct (parexec_wio_bblock_aux f _ _ _ _ _); simpl; auto.
+     destruct (parexec_wio f _ _ _); simpl; auto.
 Qed.
 
 
@@ -1777,9 +1777,9 @@ Ltac Det_WIO X :=
 - (* determ *) intros s t1 s1 t2 s2 H H0. inv H; Det_WIO X1;
   inv H0; Det_WIO X2; Equalities.
   + split. constructor. auto. 
-  + unfold parexec_wio_bblock, parexec_wio_bblock_aux in X1. destruct (parexec_wio_body _ _ _ _ _ _); try discriminate.
+  + unfold parexec_wio_bblock, parexec_wio in X1. destruct (parexec_wio_body _ _ _ _ _ _); try discriminate.
     rewrite H8 in X1. discriminate.
-  + unfold parexec_wio_bblock, parexec_wio_bblock_aux in X2. destruct (parexec_wio_body _ _ _ _ _ _); try discriminate.
+  + unfold parexec_wio_bblock, parexec_wio in X2. destruct (parexec_wio_body _ _ _ _ _ _); try discriminate.
     rewrite H4 in X2. discriminate.
   + assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
     exploit external_call_determ. eexact H6. eexact H13. intros [A B].