1 files changed, 47 insertions, 0 deletions
diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index bcd4495f..0e90cbf5 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -1,3 +1,50 @@
+(** Correctness proof for aarch64/Asmblock generation: main proof. 
+CURRENTLY A STUB !
+*)
+
+Require Import Coqlib Errors.
+Require Import Integers Floats AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock IterList.
+Require Import PseudoAsmblockproof Asmblockgen.
+
+Module MB := Machblock.
+Module AB := Asmblock.
+
+Definition match_prog (p: MB.program) (tp: AB.program) :=
+  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall p tp, transf_program p = OK tp -> match_prog p tp.
+Proof.
+  intros. eapply match_transform_partial_program; eauto.
+Qed.
+
+Parameter next: MB.function -> Z -> Z.
+
+Section PRESERVATION.
+
+Lemma next_progress: forall (f:MB.function) (pos:Z), (pos < (next f pos))%Z.
+Admitted.
+
+Variable prog: Machblock.program.
+Variable tprog: Asmblock.program.
+Hypothesis TRANSF: match_prog prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma functions_bound_max_pos: forall fb f,
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  (max_pos next f) <= Ptrofs.max_unsigned.
+Admitted.
+
+Lemma transf_program_correct:
+  forward_simulation (PseudoAsmblock.semantics next prog) (AB.semantics tprog).
+Admitted.
+
+End PRESERVATION.
+
+
 (* ORIGINAL aarch64/Asmgenproof file that needs to be adapted
 
 (* *********************************************************************)