diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-11-26 15:39:53 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-11-26 15:39:53 +0100 |
| commit | df48280ac8a59754070dd1ad7db43f05fa0f9bcd (patch) | |
| tree | 6ac76fa39361df590087d0664d85e885fa295f5d /aarch64/Asmgenproof.v | |
| parent | 3f691c8c892c897791d2e9cef104f209f587abee (diff) | |
| download | compcert-kvx-df48280ac8a59754070dd1ad7db43f05fa0f9bcd.tar.gz compcert-kvx-df48280ac8a59754070dd1ad7db43f05fa0f9bcd.zip | |
finish Asmgenproof.transf_program_correct
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index f441f20e..bbca6968 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -2249,14 +2249,24 @@ Proof. eapply compose_forward_simulations. + apply PseudoAsmblockproof.transf_program_correct; eauto. - intros; apply Asmblockgenproof.next_progress. - - 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. } *) + - intros. eapply Asmblockgenproof.functions_bound_max_pos; eauto. + { intros. + unfold Genv.symbol_address. + erewrite <- PostpassSchedulingproof.symbols_preserved; eauto. + erewrite Asmblock_PRESERVATION.symbol_high_low; eauto. + reflexivity. + } + + eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto. + { intros. + unfold Genv.symbol_address. + erewrite <- PostpassSchedulingproof.symbols_preserved; eauto. + erewrite Asmblock_PRESERVATION.symbol_high_low; eauto. + reflexivity. + } eapply compose_forward_simulations. - apply PostpassSchedulingproof.transf_program_correct; eauto. - apply Asmblock_PRESERVATION.transf_program_correct; eauto. -Admitted. +Qed. End PRESERVATION. |