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/Asmgenproof.v | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index c41d0a0b..f441f20e 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -2241,21 +2241,22 @@ Let tge := Genv.globalenv tprog. Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. -Admitted. -(* TODO unfold match_prog in TRANSF. simpl in TRANSF. inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H. inv H4. inv H. eapply compose_forward_simulations. { exploit Machblockgenproof.transf_program_correct; eauto. } + eapply compose_forward_simulations. + apply PseudoAsmblockproof.transf_program_correct; eauto. - intros; apply Asmblockgenproof.next_progress. - - intros. eapply .functions_bound_max_pos; eauto. - { intros. eapply Asmblock_PRESERVATION.symbol_high_low. eauto. } - + eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto. - { intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. } - apply Asmblock_PRESERVATION.transf_program_correct. eauto. -Qed.*) + - intros. eapply Asmblockgenproof.functions_bound_max_pos; eauto. admit. +(* { intros. eapply Asmblock_PRESERVATION.symbol_high_low; eauto. } *) + + eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto. admit. +(* { intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. } *) + eapply compose_forward_simulations. + - apply PostpassSchedulingproof.transf_program_correct; eauto. + - apply Asmblock_PRESERVATION.transf_program_correct; eauto. +Admitted. End PRESERVATION. -- cgit