From fbe134640de11d69cef417e2e59e2e2669ccc7ad Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 25 Nov 2020 16:34:02 +0100 Subject: Preservation proof with post pass scheduling in Asmgenproof almost done --- aarch64/PostpassSchedulingproof.v | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'aarch64/PostpassSchedulingproof.v') diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v index c32579a2..48840602 100644 --- a/aarch64/PostpassSchedulingproof.v +++ b/aarch64/PostpassSchedulingproof.v @@ -24,7 +24,7 @@ Require Import Axioms. Local Open Scope error_monad_scope. -Definition match_prog (p tp: Asmblock.program) := +Definition match_prog (p tp: program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. Lemma transf_program_match: @@ -462,21 +462,20 @@ Proof. + eapply exec_step_external; eauto. Qed. -End PRESERVATION_ASMVLIW. +End PRESERVATION_ASMVLIW.*) Section PRESERVATION. +Variable lk: aarch64_linker. Variables prog tprog: program. Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. Theorem transf_program_correct: - forward_simulation (Asmblock.semantics prog) (Asmvliw.semantics tprog). + forward_simulation (Asmblock.semantics lk prog) (Asmblock.semantics lk tprog). Proof. - eapply compose_forward_simulations. eapply transf_program_correct_Asmblock; eauto. - eapply transf_program_correct_Asmvliw; eauto. Qed. -End PRESERVATION.*) +End PRESERVATION. -- cgit