Integrating Asmvliw.v in the proof chain

3 files changed, 29 insertions, 16 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 31bc855d..0d4906b9 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -30,7 +30,7 @@ Require Import Smallstep.
 Require Import Locations.

 Require Stacklayout.

 Require Import Conventions.

-Require Import Asmblock.

+Require Import Asmvliw.

 Require Import Linking.

 Require Import Errors.

 

@@ -416,7 +416,7 @@ Definition program_proj (p: program) : Asmblock.program :=
 

 End RELSEM.

 

-Definition semantics (p: program) := Asmblock.semantics (program_proj p).

+Definition semantics (p: program) := Asmvliw.semantics (program_proj p).

 

 (** Determinacy of the [Asm] semantics. *)

 

@@ -547,7 +547,7 @@ Proof (Genv.senv_match TRANSF).
 

 

 Theorem transf_program_correct:

-  forward_simulation (Asmblock.semantics prog) (semantics tprog).

+  forward_simulation (Asmvliw.semantics prog) (semantics tprog).

 Proof.

   pose proof (match_program_transf prog tprog TRANSF) as TR.

   subst. unfold semantics. rewrite transf_program_proj.

diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 5b58118b..36c68acd 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -31,7 +31,8 @@ Require Import Locations.
 Require Stacklayout.
 Require Import Conventions.
 Require Import Errors.
-Require Import Asmblock.
+Require Export Asmblock.
+Require Import Sorting.Permutation.
 
 Local Open Scope asm.
 
@@ -236,8 +237,6 @@ Definition parexec_wio_bblock_aux (f: function) bdy ext size_b (rs: regset) (m:
 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 m.
 
-Require Import Sorting.Permutation.
-
 Definition parexec_bblock (f: function) (b: bblock) (rs: regset) (m: mem) (o: outcome): Prop :=
    exists bdy1 bdy2, Permutation (bdy1++bdy2) (body b) /\ 
       o=match parexec_wio_bblock_aux f bdy1 (exit b) (Ptrofs.repr (size b)) rs m with
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 7d6d9a7a..6fff3117 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -237,7 +237,7 @@ Proof.
   rewrite <- Zplus_mod. auto.
 Qed.
 
-Section PRESERVATION.
+Section PRESERVATION_ASMBLOCK.
 
 Variables prog tprog: program.
 Hypothesis TRANSL: match_prog prog tprog.
@@ -668,23 +668,37 @@ Proof.
   - apply transf_step_correct.
 Qed.
 
-(* TODO:
+End PRESERVATION_ASMBLOCK.
+
 Require Import Asmvliw.
 
-Theorem transf_program_correct: 
+Section PRESERVATION_ASMVLIW.
+
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Theorem transf_program_correct_Asmvliw: 
   forward_simulation (Asmblock.semantics tprog) (Asmvliw.semantics tprog).
 Proof.
-  eapply forward_simulation_one_one. (* FIXME *)
 Admitted.
 
-Theorem transf_program_correct: 
-  forward_simulation (Asmblock.semantics prog) (Asmvliw.semantics tprog).
-Proof.
-  eapply forward_simulation_compose. (* FIXME *)
-Admitted.
+End PRESERVATION_ASMVLIW.
 
-*)
+Section PRESERVATION.
 
+Variables prog tprog: program.
+Hypothesis TRANSL: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
 
+Theorem transf_program_correct: 
+  forward_simulation (Asmblock.semantics prog) (Asmvliw.semantics tprog).
+Proof.
+  eapply compose_forward_simulations.
+  eapply transf_program_correct_Asmblock; eauto.
+  eapply transf_program_correct_Asmvliw; eauto.
+Qed.
 
 End PRESERVATION.