diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-22 18:39:29 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-22 18:39:29 +0200 |
| commit | 958988385d5956577fbad819b6466b36df6a4d1c (patch) | |
| tree | 8b138a40a653055ae3a54de5404e98b620ad6ba1 /aarch64 | |
| parent | be298919b82ca816dc36ad3b70566226fe664a16 (diff) | |
| download | compcert-kvx-958988385d5956577fbad819b6466b36df6a4d1c.tar.gz compcert-kvx-958988385d5956577fbad819b6466b36df6a4d1c.zip | |
Complete proof of exec_exit_simulation_star
Diffstat (limited to 'aarch64')
| -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) |