cleaner separation between Asmgenproof and Machblockgenproof

2 files changed, 29 insertions, 8 deletions

diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index b0e7619d..85978cc9 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -42,17 +42,15 @@ Qed.
 
 (** Return Address Offset *)
 
-Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop :=
-  Asmblockgenproof.return_address_offset (Machblockgen.transf_function f) (Machblockgen.trans_code c) ofs.
+Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop :=
+  Mach_return_address_offset Asmblockgenproof.return_address_offset.
 
 Lemma return_address_exists:
   forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
   exists ra, return_address_offset f c ra.
 Proof.
-  intros.
-  exploit Mach_Machblock_tail; eauto.
-  destruct 1.
-  eapply Asmblockgenproof.return_address_exists; eauto.
+  intros; unfold return_address_offset; eapply Mach_return_address_exists; eauto.
+  intros; eapply Asmblockgenproof.return_address_exists; eauto.
 Qed.
 
 
@@ -72,7 +70,6 @@ Proof.
   eapply compose_forward_simulations. 
   exploit Machblockgenproof.transf_program_correct; eauto.
   unfold Machblockgenproof.inv_trans_rao. 
-  intros X; apply X.
   eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
   apply Asm.transf_program_correct. eauto.
 Qed.
diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v
index 11c3db6d..e729a907 100644
--- a/mppa_k1c/Machblockgenproof.v
+++ b/mppa_k1c/Machblockgenproof.v
@@ -651,7 +651,9 @@ Qed.
 
 End PRESERVATION.
 
-(** Auxiliary lemmas used in [Asmgenproof.return_address_exists] *)
+
+
+(** Auxiliary lemmas used to prove existence of a Mach return adress from a Machblock return address. *)
 
 Lemma is_trans_code_monotonic i c b l:
    is_trans_code c (b::l) ->
@@ -709,3 +711,25 @@ Proof.
       simpl; eapply ex_intro.
       eapply is_tail_trans; eauto with coqlib.
 Qed.
+
+Section Mach_Return_Address.
+
+Variable return_address_offset: function -> code -> ptrofs -> Prop.
+
+Hypothesis ra_exists: forall (b: bblock) (f: function) (c : list bblock),
+       is_tail (b :: c) (fn_code f) -> exists ra : ptrofs, return_address_offset f c ra.
+
+Definition Mach_return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop :=
+ return_address_offset (transf_function f) (trans_code c) ofs.
+
+Lemma Mach_return_address_exists:
+  forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) ->
+  exists ra, Mach_return_address_offset f c ra.
+Proof.
+  intros.
+  exploit Mach_Machblock_tail; eauto.
+  destruct 1.
+  eapply ra_exists; eauto.
+Qed.
+
+End Mach_Return_Address.
\ No newline at end of file