diff options
Diffstat (limited to 'aarch64/Asmblockgenproof.v')
-rw-r--r-- | aarch64/Asmblockgenproof.v | 47 |
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 (* *********************************************************************) |