From c7f3bd8555c1cae001cc93d21398b52b19d58df0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 26 Nov 2020 23:43:37 +0100 Subject: Proof of Pfmovimm fine tuned OK, moving float checks in Asm Also some simplifications in Asmblockdeps --- aarch64/Asmblockdeps.v | 336 ++++++++++++++----------------------------------- 1 file changed, 96 insertions(+), 240 deletions(-) (limited to 'aarch64/Asmblockdeps.v') diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index 7bdc734e..a913313b 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -960,21 +960,9 @@ Proof. simpl; try discriminate; try reflexivity. Qed. -Lemma ppos_discr: forall r r', r <> r' -> ppos r <> ppos r'. +Lemma ppos_discr: forall r r', r <> r' <-> ppos r <> ppos r'. Proof. - destruct r as [dr|cr|]; destruct r' as [dr'|cr'|]; - try destruct dr as [ir|fr]; try destruct dr' as [ir'|fr']; - try destruct ir as [irr|]; try destruct ir' as [irr'|]. - all: try discriminate; try contradiction. - 1: intros; unfold ppos; apply ireg_to_pos_discr; congruence. - 1,2,11,18: intros; unfold ppos; try destruct irr; try destruct irr'; discriminate. - 1,3: intros; unfold ppos; try destruct irr; try destruct fr; try destruct irr'; try destruct fr'; discriminate. - 1,2,7,13: intros; unfold ppos; try destruct fr; try destruct fr'; discriminate. - 1: intros; unfold ppos; apply freg_to_pos_discr; congruence. - 1,4: intros; unfold ppos; try destruct irr; try destruct irr'; try destruct cr; try destruct cr'; discriminate. - 2,4: intros; unfold ppos; try destruct fr; try destruct fr'; try destruct cr; try destruct cr'; discriminate. - 1,2,4,5: intros; unfold ppos; try destruct cr; try destruct cr'; discriminate. - 1: intros; unfold ppos; try destruct cr; try destruct cr'; congruence. + split; unfold not; try intros; try apply ppos_equal in H0; try discriminate; try contradiction. Qed. Lemma ppos_pmem_discr: forall r, pmem <> ppos r. @@ -1236,16 +1224,28 @@ Proof. intros. congruence. Qed. -Lemma ireg_pos_ppos: forall (sr: state) r, +(* Lemma sr_ireg_pos_ppos: forall (sr: state) r, sr (ireg_to_pos r) = sr (# r). Proof. intros. simpl. reflexivity. Qed. -Lemma freg_pos_ppos: forall (sr: state) r, +Lemma sr_freg_pos_ppos: forall (sr: state) r, sr (freg_to_pos r) = sr (# r). Proof. intros. simpl. reflexivity. +Qed. *) + +Lemma ireg_pos_ppos: forall r, + ireg_to_pos r = # r. +Proof. + intros. simpl. reflexivity. +Qed. + +Lemma freg_pos_ppos: forall r, + freg_to_pos r = # r. +Proof. + intros. simpl. reflexivity. Qed. Lemma ireg_not_pc: forall r, @@ -1314,63 +1314,15 @@ Proof. intros; destruct r; discriminate. Qed. -Lemma sr_ireg_update_both: forall sr rsr r1 rr v - (HEQV: forall r : preg, sr (# r) = Val (rsr r)), - (sr <[ ireg_to_pos r1 <- Val (v) ]>) (#rr) = - Val (rsr # r1 <- v rr). -Proof. - intros. unfold assign. - destruct (PregEq.eq r1 rr); subst. - - rewrite Pregmap.gss. simpl. destruct r1; simpl; reflexivity. - - rewrite Pregmap.gso; eauto. - destruct rr; try congruence. - + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; destruct r1; simpl; try congruence. - + destruct c; destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence. - + destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence. -Qed. - -Lemma sr_freg_update_both: forall sr rsr r1 rr v +Lemma sr_update_both: forall sr rsr r1 rr v (HEQV: forall r : preg, sr (# r) = Val (rsr r)), - (sr <[ freg_to_pos r1 <- Val (v) ]>) (#rr) = + (sr <[ (#r1) <- Val (v) ]>) (#rr) = Val (rsr # r1 <- v rr). Proof. intros. unfold assign. - destruct (PregEq.eq r1 rr); subst. - - rewrite Pregmap.gss. simpl. destruct r1; simpl; reflexivity. - - rewrite Pregmap.gso; eauto. - destruct rr; try congruence. - + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; destruct r1; simpl; try congruence. - + destruct c; destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence. - + destruct r1; simpl; try rewrite <- HEQV; unfold ppos; try congruence. -Qed. - -Lemma sr_xsp_update_both: forall sr rsr rr v - (HEQV: forall r : preg, sr (# r) = Val (rsr r)), - (sr <[ #XSP <- Val (v) ]>) (#rr) = - Val (rsr # XSP <- v rr). -Proof. - intros. unfold assign. - destruct (PregEq.eq XSP rr); subst. - - rewrite Pregmap.gss. simpl. reflexivity. - - rewrite Pregmap.gso; eauto. - destruct rr; try congruence. - + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; simpl; try congruence. - + destruct c; simpl; try rewrite <- HEQV; unfold ppos; try congruence. - + simpl; try rewrite <- HEQV; unfold ppos; try congruence. -Qed. - -Lemma sr_pc_update_both: forall sr rsr rr v - (HEQV: forall r : preg, sr (# r) = Val (rsr r)), - (sr <[ #PC <- Val (v) ]>) (#rr) = - Val (rsr # PC <- v rr). -Proof. - intros. unfold assign. - destruct (PregEq.eq PC rr); subst. - - rewrite Pregmap.gss. simpl. reflexivity. - - rewrite Pregmap.gso; eauto. - destruct rr; try congruence. - + destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; simpl; try congruence. - + destruct c; simpl; try rewrite <- HEQV; unfold ppos; try congruence. + destruct (R.eq_dec (#r1) (#rr)); subst. + - apply ppos_equal in e; subst; rewrite Pregmap.gss; reflexivity. + - rewrite Pregmap.gso; eapply ppos_discr in n; auto. Qed. Lemma sr_gss: forall sr pos v, @@ -1402,9 +1354,9 @@ Ltac sr_memstate_rwrt := Ltac replace_ppos := try erewrite !ireg_pos_ppos; - try erewrite !freg_pos_ppos. - -Ltac DI0N0 ir0 := destruct ir0; subst; simpl. + try erewrite !freg_pos_ppos; + try replace (7) with (#XSP) by eauto; + try replace (24) with (#X16) by auto. Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl. @@ -1413,10 +1365,10 @@ Ltac DDRM dr := [destruct irsDDRF | idtac ]. -Ltac DDRF dr := +(* Ltac DDRF dr := destruct dr as [irsDDRF|frDDRF]; [destruct irsDDRF as [irsDDRF|]; [destruct irsDDRF|] - | destruct frDDRF]. + | destruct frDDRF]. *) Ltac DPRF pr := destruct pr as [drDPRF|crDPRF|]; @@ -1429,11 +1381,11 @@ Ltac DPRM pr := [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |] | destruct crDPRF|]. -Ltac DPRI pr := +(* Ltac DPRI pr := destruct pr as [drDPRI|crDPRI|]; [destruct drDPRI as [irDPRI|frDPRI]; [destruct irDPRI as [irrDPRI|]; [destruct irrDPRI|]|] | idtac - | idtac ]. + | idtac ]. *) Ltac discriminate_ppos := try apply ireg_not_pmem; @@ -1479,36 +1431,18 @@ Ltac Simpl_rep sr := ). Ltac Simpl_update := - try eapply sr_ireg_update_both; eauto; - try eapply sr_freg_update_both; eauto; - try eapply sr_xsp_update_both; eauto; - try eapply sr_pc_update_both; eauto. + try eapply sr_update_both; eauto. -Ltac Simpl sr := Simpl_exists sr; try (intros rr; try rewrite sr_update_overwrite; replace_regs_pos sr; DPRM rr); Simpl_update. +Ltac Simpl sr := Simpl_exists sr; try (intros rr(* ; try rewrite sr_update_overwrite; replace_regs_pos sr; DPRM rr *)); Simpl_update. Ltac destruct_res_flag rsr := try (rewrite Pregmap.gso; discriminate_ppos); destruct (rsr _); simpl; try reflexivity. -Ltac discriminate_preg_flags := rewrite !assign_diff; try rewrite !Pregmap.gso; discriminate_ppos; sr_val_rwrt; reflexivity. - -Ltac validate_crbit_flags c := - destruct c; - [ - do 3 (rewrite assign_diff; discriminate_ppos); - do 3 (rewrite Pregmap.gso; try discriminate); - rewrite sr_gss; rewrite Pregmap.gss; reflexivity | - do 2 (rewrite assign_diff; discriminate_ppos); - do 2 (rewrite Pregmap.gso; try discriminate); - rewrite sr_gss; rewrite Pregmap.gss; reflexivity | - do 1 (rewrite assign_diff; discriminate_ppos); - do 1 (rewrite Pregmap.gso; try discriminate); - rewrite sr_gss; rewrite Pregmap.gss; reflexivity | - rewrite sr_gss; rewrite Pregmap.gss; reflexivity - ]. - -Ltac destruct_reg_neq r1 r2 := +(* Ltac discriminate_preg_flags := rewrite !assign_diff; try rewrite !Pregmap.gso; discriminate_ppos; sr_val_rwrt; reflexivity. *) + +(* Ltac destruct_reg_neq r1 r2 := destruct (PregEq.eq r1 r2); subst; [ rewrite sr_gss; rewrite Pregmap.gss; reflexivity | - rewrite assign_diff; try rewrite Pregmap.gso; fold (ppos r1); try apply ppos_discr; auto]. + rewrite assign_diff; try rewrite Pregmap.gso; fold (ppos r1); try apply ppos_discr; auto]. *) Lemma reg_update_overwrite: forall rsr sr r rd v1 v2 (HEQV: forall r : preg, sr (# r) = Val (rsr r)), @@ -1522,22 +1456,34 @@ Proof. unfold not; intros. apply ppos_equal in H. congruence. Qed. -Lemma compare_single_res_aux: forall sr mr rsr rr - (HMEM: sr pmem = Memstate mr) - (HEQV: forall r : preg, sr (# r) = Val (rsr r)), - ((((sr <[ 2 <- Val (_CN (v_compare_single Vundef Vundef)) ]>) <[ 3 <- - Val (_CZ (v_compare_single Vundef Vundef)) ]>) <[ 4 <- - Val (_CC (v_compare_single Vundef Vundef)) ]>) <[ 5 <- - Val (_CV (v_compare_single Vundef Vundef)) ]>) (# rr) = -Val - ((compare_single rsr Vundef Vundef) rr). -Proof. - intros. unfold v_compare_single, compare_single. - (destruct rr; - [ DDRF d; discriminate_preg_flags | - validate_crbit_flags c | - discriminate_preg_flags ]). -Qed. +Ltac replace_regs_cond_force := + try replace (5) with (#CV) in * by auto; + try replace (4) with (#CC) in * by auto; + try replace (3) with (#CZ) in * by auto; + try replace (2) with (#CN) in * by auto. + +Ltac validate_crbit_flags rr v1 v2 := + destruct (R.eq_dec 5 (#rr)) as [eCV|eCV]; subst; + [ destruct v1; destruct v2; simpl; + replace_regs_cond_force; apply ppos_equal in eCV; subst; + rewrite Pregmap.gss; auto | + destruct (R.eq_dec 4 (#rr)) as [eCC|eCC]; subst; + [ destruct v1; destruct v2; simpl; + replace_regs_cond_force; apply ppos_equal in eCC; subst; + rewrite Pregmap.gso, Pregmap.gss; auto; try discriminate | + destruct (R.eq_dec 3 (#rr)) as [eCZ|eCZ]; subst; + [ destruct v1; destruct v2; simpl; + replace_regs_cond_force; apply ppos_equal in eCZ; subst; + rewrite 2Pregmap.gso, Pregmap.gss; auto; try discriminate | + destruct (R.eq_dec 2 (#rr)) as [eCN|eCN]; subst; + [ destruct v1; destruct v2; simpl; + replace_regs_cond_force; apply ppos_equal in eCN; subst; + rewrite 3Pregmap.gso, Pregmap.gss; auto; try discriminate | + destruct v1; destruct v2; simpl; + replace_regs_cond_force; + apply ppos_discr in eCV; apply ppos_discr in eCC; + apply ppos_discr in eCZ; apply ppos_discr in eCN; + rewrite 4Pregmap.gso; auto; try discriminate ]]]]. Lemma compare_single_res: forall sr mr rsr rr v1 v2 (HMEM: sr pmem = Memstate mr) @@ -1549,31 +1495,8 @@ Lemma compare_single_res: forall sr mr rsr rr v1 v2 Val ((compare_single rsr v1 v2) rr). Proof. - intros. - destruct v1; destruct v2; - try eapply compare_single_res_aux; eauto. - unfold v_compare_single, compare_single. - (destruct rr; - [ DDRF d; discriminate_preg_flags | - validate_crbit_flags c | - discriminate_preg_flags ]). -Qed. - -Lemma compare_float_res_aux: forall sr mr rsr rr - (HMEM: sr pmem = Memstate mr) - (HEQV: forall r : preg, sr (# r) = Val (rsr r)), - ((((sr <[ 2 <- Val (_CN (v_compare_float Vundef Vundef)) ]>) <[ 3 <- - Val (_CZ (v_compare_float Vundef Vundef)) ]>) <[ 4 <- - Val (_CC (v_compare_float Vundef Vundef)) ]>) <[ 5 <- - Val (_CV (v_compare_float Vundef Vundef)) ]>) (# rr) = -Val - ((compare_float rsr Vundef Vundef) rr). -Proof. - intros. unfold v_compare_float, compare_float. - (destruct rr; - [ DDRF d; discriminate_preg_flags | - validate_crbit_flags c | - discriminate_preg_flags ]). + intros. unfold v_compare_single, compare_single, assign. + validate_crbit_flags rr v1 v2. Qed. Lemma compare_float_res: forall sr mr rsr rr v1 v2 @@ -1586,31 +1509,8 @@ Lemma compare_float_res: forall sr mr rsr rr v1 v2 Val ((compare_float rsr v1 v2) rr). Proof. - intros. - destruct v1; destruct v2; - try eapply compare_float_res_aux; eauto. - unfold v_compare_float, compare_float. - (destruct rr; - [ DDRF d; discriminate_preg_flags | - validate_crbit_flags c | - discriminate_preg_flags ]). -Qed. - -Lemma compare_long_res_aux: forall sr mr rsr rr - (HMEM: sr pmem = Memstate mr) - (HEQV: forall r : preg, sr (# r) = Val (rsr r)), - ((((sr <[ 2 <- Val (_CN (v_compare_long Vundef Vundef)) ]>) <[ 3 <- - Val (_CZ (v_compare_long Vundef Vundef)) ]>) <[ 4 <- - Val (_CC (v_compare_long Vundef Vundef)) ]>) <[ 5 <- - Val (_CV (v_compare_long Vundef Vundef)) ]>) (# rr) = -Val - ((compare_long rsr Vundef Vundef) rr). -Proof. - intros. unfold v_compare_long, compare_long. - (destruct rr; - [ DDRF d; discriminate_preg_flags | - validate_crbit_flags c | - discriminate_preg_flags ]). + intros. unfold v_compare_float, compare_float, assign. + validate_crbit_flags rr v1 v2. Qed. Lemma compare_long_res: forall sr mr rsr rr v1 v2 @@ -1623,31 +1523,8 @@ Lemma compare_long_res: forall sr mr rsr rr v1 v2 Val ((compare_long rsr v1 v2) rr). Proof. - intros. - destruct v1; destruct v2; - try eapply compare_long_res_aux; eauto; - unfold v_compare_long, compare_long; - (destruct rr; - [ DDRF d; discriminate_preg_flags | - validate_crbit_flags c | - discriminate_preg_flags ]). -Qed. - -Lemma compare_int_res_aux: forall sr mr rsr rr - (HMEM: sr pmem = Memstate mr) - (HEQV: forall r : preg, sr (# r) = Val (rsr r)), - ((((sr <[ 2 <- Val (_CN (v_compare_int Vundef Vundef)) ]>) <[ 3 <- - Val (_CZ (v_compare_int Vundef Vundef)) ]>) <[ 4 <- - Val (_CC (v_compare_int Vundef Vundef)) ]>) <[ 5 <- - Val (_CV (v_compare_int Vundef Vundef)) ]>) (# rr) = -Val - ((compare_int rsr Vundef Vundef) rr). -Proof. - intros. unfold v_compare_int, compare_int. - (destruct rr; - [ DDRF d; discriminate_preg_flags | - validate_crbit_flags c | - discriminate_preg_flags ]). + intros. unfold v_compare_long, compare_long, assign. + validate_crbit_flags rr v1 v2. Qed. Lemma compare_int_res: forall sr mr rsr rr v1 v2 @@ -1660,14 +1537,8 @@ Lemma compare_int_res: forall sr mr rsr rr v1 v2 Val ((compare_int rsr v1 v2) rr). Proof. - intros. - destruct v1; destruct v2; - try eapply compare_int_res_aux; eauto; - unfold v_compare_int, compare_int; - (destruct rr; - [ DDRF d; discriminate_preg_flags | - validate_crbit_flags c | - discriminate_preg_flags ]). + intros. unfold v_compare_int, compare_int, assign. + validate_crbit_flags rr v1 v2. Qed. Section SECT_SEQ. @@ -1686,15 +1557,13 @@ Proof. - (* PArithP *) destruct i. 1,2,3: DIRN1 rd; Simpl sr. - all: admit. (* Special case for Pmovimms/Pmovimmd *) - (* all: DIRN1 rd; Simpl sr; - try (rewrite assign_diff; discriminate_ppos; reflexivity); - try replace 24 with (#X16) by auto; - try replace 7 with (#XSP) by auto; - try (Simpl_update; intros rr; destruct_reg_neq r rr); - try (Simpl_update; intros rr; destruct_reg_neq XSP rr); - try (Simpl_update; intros rr; destruct_reg_neq f0 rr). *) + all: simpl; + try(destruct (negb (is_immediate_float32 _))); + try(destruct (negb (is_immediate_float64 _))); + DIRN1 rd; Simpl sr; + try (rewrite assign_diff; discriminate_ppos; reflexivity); + try (intros rr'; Simpl_update). - (* PArithPP *) DIRN1 rs; DIRN1 rd; Simpl sr. - (* PArithPPP *) @@ -1737,7 +1606,7 @@ Proof. try (eapply compare_int_res; eauto); try (eapply compare_float_res; eauto). - (* Pcset *) - simpl; (*DI0N0 rd.*) unfold eval_testcond, get_testcond_rlocs, cflags_eval; + simpl; unfold eval_testcond, get_testcond_rlocs, cflags_eval; unfold cond_eval_is; unfold flags_testcond_value, list_exp_eval; destruct c; simpl; repeat Simpl_rep sr; Simpl_exists sr; destruct_res_flag rsr; @@ -1745,17 +1614,11 @@ Proof. - (* Pfmovi *) simpl; destruct r1; simpl; destruct fsz; Simpl sr. - (* Pcsel *) - simpl. - unfold eval_testcond, cflags_eval. DIRN1 r1; DIRN1 r2; destruct c; simpl; - repeat Simpl_rep sr; - (eexists; split; [| split]; [reflexivity | DDRM rd; Simpl_exists sr | idtac]). - all: intros rr; destruct (PregEq.eq rr rd); - [ subst; erewrite Pregmap.gss; erewrite sr_gss; reflexivity | - try erewrite Pregmap.gso; try erewrite assign_diff; try rewrite H0; try fold (ppos rd); try eapply ppos_discr; eauto ]. + simpl. destruct c; simpl; + DIRN1 r1; DIRN1 r2; Simpl_rep sr; DDRM rd; Simpl_exists sr; try intros rr; Simpl_update. - (* Pfnmul *) simpl; destruct fsz; Simpl sr. -(* Qed. *) -Admitted. +Qed. Lemma sp_xsp: SP = XSP. @@ -1785,10 +1648,7 @@ Local Ltac preg_eq_discr r rd := destruct a; simpl; try destruct base; Simpl_exists sr; erewrite H; unfold exec_load1, exec_load2, exec_loadU; unfold call_ll_loadv; try destruct (Mem.loadv _ _ _); simpl; auto. - all: eexists; split; [| split]; [ eauto | DDRF rd; eauto | idtac ]; - intros rr; destruct (PregEq.eq rr rd); subst; [ rewrite Pregmap.gss; rewrite sr_gss; reflexivity | - rewrite assign_diff; try rewrite Pregmap.gso; - try rewrite H0; try (fold (ppos rd); eapply ppos_discr); auto]. + all: DDRM rd; Simpl_exists sr; try intros rr; Simpl_update. - (* Store *) unfold exec_store, eval_addressing_rlocs_st, exp_eval; destruct a; simpl; DIRN1 r; try destruct base; Simpl_exists sr; erewrite H; @@ -1865,13 +1725,12 @@ Proof. try (destruct (Val_cmplu_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b); try (destruct (Val.cmp_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b); try (destruct (Val.cmpl_bool _ _ _) eqn:EQCMP; try reflexivity; destruct b); - try (Simpl_exists sr; intros rr; destruct (PregEq.eq rr PC); subst; - [ rewrite sr_gss, Pregmap.gss; reflexivity | rewrite !assign_diff, Pregmap.gso; auto ]); - try (destruct (label_pos _ _ _); try reflexivity; rewrite Pregmap.gss; - destruct Val.offset_ptr; try reflexivity; Simpl_exists sr; - intros rr; destruct (PregEq.eq rr PC); subst; - [ rewrite sr_gss, Pregmap.gss; reflexivity | rewrite !assign_diff, Pregmap.gso; auto ]; - rewrite Pregmap.gso; auto)]. + try (simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr); + destruct (label_pos _ _ _); try reflexivity; rewrite Pregmap.gss; + destruct Val.offset_ptr; try reflexivity; rewrite sr_update_overwrite; + simpl; Simpl sr; (destruct (PregEq.eq rr PC); subst; + [ rewrite sr_gss, Pregmap.gss; reflexivity | + rewrite !assign_diff, !Pregmap.gso; replace_pc; auto; apply ppos_discr; auto]) ]. - (* Ob *) replace_pc. rewrite (H0 PC). simpl. unfold goto_label, control_eval. destruct Ge. @@ -1893,26 +1752,25 @@ Proof. 1,2,3,4,5,6: destruct_res_flag rsr. 7,8,9,10: do 2 (destruct_res_flag rsr). 11,12 : do 3 (destruct_res_flag rsr). - 1,2,3,4,5,6,9,10: destruct (Int.eq _ _); [| Simpl sr ]; + 1,2,3,4,5,6,9,10: destruct (Int.eq _ _); [| simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr ]; destruct (label_pos _ _ _); [| reflexivity]; replace_pc; rewrite !Pregmap.gss; destruct Val.offset_ptr; try (unfold Stuck; reflexivity); Simpl_exists sr; intros rr; apply reg_update_overwrite; eauto. - 1,3: destruct (andb); [| Simpl sr ]; + 1,3: destruct (andb); [| simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr ]; destruct (label_pos _ _ _); [| reflexivity]; replace_pc; rewrite !Pregmap.gss; destruct Val.offset_ptr; try (unfold Stuck; reflexivity); Simpl_exists sr; intros rr; apply reg_update_overwrite; eauto. - 1,2: destruct (orb); [| Simpl sr ]; + 1,2: destruct (orb); [| simpl; rewrite sr_update_overwrite; replace_pc; Simpl sr ]; destruct (label_pos _ _ _); [| reflexivity]; replace_pc; rewrite !Pregmap.gss; destruct Val.offset_ptr; try (unfold Stuck; reflexivity); Simpl_exists sr; intros rr; apply reg_update_overwrite; eauto. - (* Obl *) replace_pc. rewrite (H0 PC). simpl. unfold control_eval. destruct Ge. - rewrite sr_gss. - repeat Simpl_rep sr. Simpl_exists sr. - Simpl sr. - all: repeat (intros; replace_regs_pos sr; try replace (38) with (#X30) by eauto; unfold incrPC; Simpl_update). + rewrite sr_gss. Simpl sr. + replace_pc; try replace (38) with (#X30) by eauto; unfold incrPC. Simpl_update. + repeat (intros; Simpl_update). - (* Obs *) unfold control_eval. destruct Ge. replace_pc. rewrite (H0 PC). simpl; unfold incrPC. replace_pc; Simpl_exists sr; intros rr; apply reg_update_overwrite; eauto. @@ -1958,17 +1816,15 @@ Proof. rewrite assign_diff; auto. intros rr. unfold incrPC. destruct (PregEq.eq rr PC); subst. * rewrite sr_gss, Pregmap.gss. reflexivity. - * rewrite assign_diff, Pregmap.gso; try rewrite H0; try rewrite ppos_discr; auto. - - (*simpl; inv MS. unfold control_eval; destruct Ge. - replace_pc; rewrite H0. congruence.*) + * rewrite assign_diff, Pregmap.gso; try rewrite H0; + auto; try rewrite ppos_discr in n; auto. - simpl. inv MS. eexists; split; [| split]. + unfold control_eval; destruct Ge. replace_pc; rewrite (H0 PC); eauto. + rewrite assign_diff; auto. + intros rr. unfold incrPC. destruct (PregEq.eq rr PC); subst. * rewrite sr_gss, Pregmap.gss. reflexivity. - * rewrite assign_diff, Pregmap.gso; try rewrite H0; try rewrite ppos_discr; auto. + * rewrite assign_diff, Pregmap.gso; try rewrite H0; auto; try rewrite ppos_discr in n; auto. Qed. (* Definition trans_block_aux bdy sz ex := (trans_body bdy) ++ (trans_pcincr sz (trans_exit ex) :: nil). *) -- cgit