diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-22 08:12:37 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-06-22 08:12:37 +0200 |
commit | 5dec4b189dd7775229199de11e4c81551b7baaf6 (patch) | |
tree | 6ef4f77034cd9003256e34e31e5b91c35a4e1b85 /aarch64/Asmblockgenproof.v | |
parent | 0cde06d359ff8b265b38eef5f62a2e8f4e744059 (diff) | |
download | compcert-kvx-5dec4b189dd7775229199de11e4c81551b7baaf6.tar.gz compcert-kvx-5dec4b189dd7775229199de11e4c81551b7baaf6.zip |
restauring Coq compilation with STUBS
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 (* *********************************************************************) |