diff options
| author | Léo Gourdin <leo.gourdin@lilo.org> | 2020-10-11 20:53:47 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@lilo.org> | 2020-10-11 20:53:47 +0200 |
| commit | 98fd357b98b68842561e1e1a2f1bc32e8a6e1e3c (patch) | |
| tree | 4662c3bd348c172f8a2f7ea94d643a216298d30c /aarch64 | |
| parent | 545bd78efd711ebb69cac6e5ff12429362002074 (diff) | |
| download | compcert-kvx-98fd357b98b68842561e1e1a2f1bc32e8a6e1e3c.tar.gz compcert-kvx-98fd357b98b68842561e1e1a2f1bc32e8a6e1e3c.zip | |
Continue the proof of exec_basic_simulation
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Asmgenproof.v | 30 |
1 files changed, 12 insertions, 18 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 1699b5f1..07d1dffb 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1001,21 +1001,6 @@ Proof. + next_stuck_cong. Qed. -Lemma exec_load_propag: forall sz rs2 m2 x a, - (Asm.exec_load tge Mint8unsigned - match sz with - | W => fun v : val => v - | X => Val.longofintu - end a x rs2 m2) = - (match sz with - | W => Asm.exec_load tge Mint8unsigned (fun v : val => v) a x rs2 m2 - | X => Asm.exec_load tge Mint8unsigned Val.longofintu a x rs2 m2 - end). -Proof. - intros. - destruct sz; eauto. -Qed. - Lemma exec_basic_simulation: forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) @@ -1028,9 +1013,18 @@ Lemma exec_basic_simulation: Proof. intros. destruct bi. - 2: { - simpl in*. destruct ld; monadInv TRANSBI; destruct rd as [[r|]|]; try congruence; inversion EQ; subst; exploit load_preserved; eauto. - - intros. simpl in *. rewrite exec_load_propag in H; eauto. + - (* PArith *) + simpl in *. repeat destruct i. monadInv TRANSBI. destruct rd as [[r|]|]; try congruence.inversion EQ; subst. simpl in *. + + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + unfold Asm.nextinstr. rewrite (Pregmap.gso (i := PC) (j := x)); try congruence. + + rewrite <- EQPC. + + all:admit. + - (* PLoad *) + simpl in*. destruct ld; monadInv TRANSBI; destruct rd as [[r|]|]; try congruence; inversion EQ; subst; exploit load_preserved; eauto; + intros; simpl in *; destruct sz; eauto. Admitted. Lemma exec_body_simulation_star': forall |