From 5dec4b189dd7775229199de11e4c81551b7baaf6 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 22 Jun 2020 08:12:37 +0200 Subject: restauring Coq compilation with STUBS --- aarch64/Asmblockgenproof.v | 47 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) (limited to 'aarch64/Asmblockgenproof.v') 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 (* *********************************************************************) -- cgit