diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-20 17:12:49 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-20 17:12:49 +0200 |
| commit | 3405bc5f341ef398bbf681f956da26074d1dde1a (patch) | |
| tree | a8de03e1fef502cd506d119d12945b1e462a7119 /aarch64/Asmgenproof.v | |
| parent | 0c6e2d98365d78283058f3c1497bc0b382771491 (diff) | |
| download | compcert-kvx-3405bc5f341ef398bbf681f956da26074d1dde1a.tar.gz compcert-kvx-3405bc5f341ef398bbf681f956da26074d1dde1a.zip | |
update comments
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 31 |
1 files changed, 14 insertions, 17 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 833c6f03..b2671972 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1426,7 +1426,6 @@ Proof. exploit header_body_tail_bound; eauto. intros BDYTAIL. exploit exec_basic_simulation; eauto. intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT). - (* Code from the star' lemma bellow. We need this to exploit exec_step_internal. *) exploit exec_basic_dont_move_PC; eauto. intros AGPC. inversion MI_NEXT as [A B C D E M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT PC_OFS_NEXT RS RS']. subst A. subst B. subst C. subst D. subst E. @@ -1458,7 +1457,6 @@ Proof. intros STEP_NEXT. destruct li as [|a' li]; simpl in *. - (* case of a single instruction in li: this our base case in the induction *) - (* XXX New code --> no need to use the star' lemma this way. *) inversion BODY; subst. eexists; split. + apply plus_one. eauto. @@ -1468,21 +1466,20 @@ Proof. apply f_equal. rewrite bblock_size_aux, list_length_z_cons; simpl. omega. - - (* TODO: apply the induction hypothesis IHli *) - exploit (IHli b ofs f bb rs1 m_next' (State rs_next' m_next')); congruence || eauto. - + exploit is_tail_app_def; eauto. - intros (l3 & EQ); rewrite EQ. - exploit (is_tail_app_right _ (l3 ++ a::nil)). - rewrite <- app_assoc; simpl; eauto. - + constructor; auto. - rewrite ATPC_NEXT. - apply f_equal. - apply f_equal. - rewrite! list_length_z_cons; simpl. - omega. - + intros (s2' & LAST_STEPS & LAST_MATCHS). - eexists. split; eauto. - eapply plus_left'; eauto. + - exploit (IHli b ofs f bb rs1 m_next' (State rs_next' m_next')); congruence || eauto. + + exploit is_tail_app_def; eauto. + intros (l3 & EQ); rewrite EQ. + exploit (is_tail_app_right _ (l3 ++ a::nil)). + rewrite <- app_assoc; simpl; eauto. + + constructor; auto. + rewrite ATPC_NEXT. + apply f_equal. + apply f_equal. + rewrite! list_length_z_cons; simpl. + omega. + + intros (s2' & LAST_STEPS & LAST_MATCHS). + eexists. split; eauto. + eapply plus_left'; eauto. Qed. Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall |