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