From 3405bc5f341ef398bbf681f956da26074d1dde1a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Oct 2020 17:12:49 +0200 Subject: update comments --- aarch64/Asmgenproof.v | 31 ++++++++++++++----------------- 1 file changed, 14 insertions(+), 17 deletions(-) (limited to 'aarch64/Asmgenproof.v') 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 -- cgit