From 958988385d5956577fbad819b6466b36df6a4d1c Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Wed, 22 Jul 2020 18:39:29 +0200 Subject: Complete proof of exec_exit_simulation_star --- aarch64/Asmgenproof.v | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 73921c03..55ff066f 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -529,9 +529,17 @@ Proof. eapply exec_exit_simulation_plus; try rewrite Hex; congruence || eauto. - inv MATCHI. inv EXIT. - assert (X: rs2 = incrPC (Ptrofs.repr (size bb)) rs). { admit. } + assert (X: rs2 = incrPC (Ptrofs.repr (size bb)) rs). { + unfold incrPC. unfold Pregmap.set. + apply functional_extensionality. intros x. + destruct (PregEq.eq x PC) as [X|]. + - rewrite X. rewrite <- AGPC. simpl. + replace (size bb - 0) with (size bb) by omega. reflexivity. + - rewrite AG; try assumption. reflexivity. + } + destruct X. subst; eapply star_refl; eauto. -Admitted. +Qed. Lemma exec_bblock_simulation b ofs f tf bb t rs m rs' m': forall (ATPC: rs PC = Vptr b ofs) -- cgit