diff options
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 12 |
1 files 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) |