diff options
Diffstat (limited to 'src/translation/HTLgenproof.v')
| -rw-r--r-- | src/translation/HTLgenproof.v | 708 |
1 files changed, 301 insertions, 407 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 079cc1e..f248e25 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -183,11 +183,11 @@ Lemma list_combine_none : length l = n -> list_combine Verilog.merge_cell (list_repeat None n) l = l. Proof. - induction n; intros; simplify. + induction n; intros; crush. - symmetry. apply length_zero_iff_nil. auto. - - destruct l; simplify. + - destruct l; crush. rewrite list_repeat_cons. - simplify. f_equal. + crush. f_equal. eauto. Qed. @@ -198,7 +198,7 @@ Lemma combine_none : Proof. intros. unfold combine. - simplify. + crush. rewrite <- (arr_wf a) in H. apply list_combine_none. @@ -211,12 +211,12 @@ Lemma list_combine_lookup_first : nth_error l1 n = Some None -> nth_error (list_combine Verilog.merge_cell l1 l2) n = nth_error l2 n. Proof. - induction l1; intros; simplify. + induction l1; intros; crush. rewrite nth_error_nil in H0. discriminate. - destruct l2 eqn:EQl2. simplify. + destruct l2 eqn:EQl2. crush. simpl in H. invert H. destruct n; simpl in *. invert H0. simpl. reflexivity. @@ -243,9 +243,9 @@ Lemma list_combine_lookup_second : nth_error l1 n = Some (Some x) -> nth_error (list_combine Verilog.merge_cell l1 l2) n = Some (Some x). Proof. - induction l1; intros; simplify; auto. + induction l1; intros; crush; auto. - destruct l2 eqn:EQl2. simplify. + destruct l2 eqn:EQl2. crush. simpl in H. invert H. destruct n; simpl in *. invert H0. simpl. reflexivity. @@ -432,43 +432,54 @@ Section CORRECTNESS. exists asr' asa', HTL.step tge (HTL.State res m st asr asa) Events.E0 (HTL.State res m st asr' asa'). - Ltac big_tac := - repeat (simplify; - match goal with - | [ |- context[Verilog.merge_regs _ _] ] => - unfold Verilog.merge_regs; simplify; unfold_merge - | [ |- context[_ # ?d <- _ ! ?d] ] => apply AssocMap.gss - | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso; try apply st_greater_than_res - | [ |- context[valueToPos (posToValue 32 _)] ] => rewrite assumption_32bit - | [ |- context[match_states _ _] ] => econstructor; eauto - | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr; simplify - | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty; simplify + Opaque combine. - | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] => - unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal - - | [ |- match_assocmaps _ _ _ # _ <- (posToValue 32 _) ] => - apply regs_lessdef_add_greater; [> apply greater_than_max_func | assumption] - - | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1; simplify - - | [ |- match_arrs _ _ _ _ _ ] => econstructor; simplify - | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack; simplify - | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs; simplify - | [ |- context[(AssocMap.combine _ _ _) ! _] ] => - try (rewrite AssocMap.gcombine; [> | reflexivity]) - - | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros - | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] => - rewrite Registers.Regmap.gss - | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] => - destruct (Pos.eq_dec s d) as [EQ|EQ]; - [> rewrite EQ | rewrite Registers.Regmap.gso; auto] - - | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set + Ltac tac0 := + match goal with + | [ |- context[Verilog.merge_regs _ _] ] => + unfold Verilog.merge_regs; crush; unfold_merge + | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss + | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso + | [ |- context[valueToPos (posToValue 32 _)] ] => rewrite assumption_32bit + | [ |- context[match_states _ _] ] => econstructor; auto + | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr + | [ |- context[(AssocMap.empty _) ! _] ] => rewrite AssocMap.gempty + + | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] => + unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal + + | [ |- match_assocmaps _ _ _ # _ <- (posToValue 32 _) ] => + apply regs_lessdef_add_greater; [> apply greater_than_max_func | assumption] + + | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1 + + | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto + | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack + | [ |- context[Verilog.merge_arrs _ _] ] => unfold Verilog.merge_arrs + | [ |- context[(AssocMap.combine _ _ _) ! _] ] => + try (rewrite AssocMap.gcombine; [> | reflexivity]) + + | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros + | [ |- context[Registers.Regmap.get ?d (Registers.Regmap.set ?d _ _)] ] => + rewrite Registers.Regmap.gss + | [ |- context[Registers.Regmap.get ?s (Registers.Regmap.set ?d _ _)] ] => + destruct (Pos.eq_dec s d) as [EQ|EQ]; + [> rewrite EQ | rewrite Registers.Regmap.gso; auto] + + | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set + + | [ |- context[array_get_error _ (combine Verilog.merge_cell + (arr_repeat None _) _)] ] => + rewrite combine_lookup_first + + | [ H : opt_val_value_lessdef _ _ |- _ ] => invert H + + | [ H : context[Z.of_nat (Z.to_nat _)] |- _ ] => rewrite Z2Nat.id in H; [> solve crush |] + | [ H : _ ! _ = Some _ |- _] => setoid_rewrite H + end. - | [ H : _ ! _ = Some _ |- _] => try (setoid_rewrite H; simplify) - end); simplify. + Ltac small_tac := repeat (crush; try array; try ptrofs); crush; auto. + Ltac big_tac := repeat (crush; try array; try ptrofs; try tac0); crush; auto. Lemma transl_inop_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) @@ -490,13 +501,12 @@ Section CORRECTNESS. apply assumption_32bit. (* processing of state *) econstructor. - simplify. + crush. econstructor. econstructor. econstructor. all: invert MARR; big_tac. - Unshelve. constructor. Qed. @@ -612,7 +622,7 @@ Section CORRECTNESS. Ltac inv_arr_access := match goal with | [ _ : translate_arr_access ?chunk ?addr ?args _ _ = OK ?c _ _ |- _] => - destruct c, chunk, addr, args; simplify; tac; simplify + destruct c, chunk, addr, args; crush; tac; crush end. Lemma transl_iload_correct: @@ -633,24 +643,24 @@ Section CORRECTNESS. inv_state. inv_arr_access. + (** Preamble *) - invert MARR. simplify. + invert MARR. crush. unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; simplify. + destruct (Archi.ptr64) eqn:ARCHI; crush. unfold reg_stack_based_pointers in RSBP. pose proof (RSBP r0) as RSBPr0. - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify. + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. - rewrite ARCHI in H1. simplify. + rewrite ARCHI in H1. crush. subst. pose proof MASSOC as MASSOC'. invert MASSOC'. pose proof (H0 r0). assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). + by (eapply RTL.max_reg_function_use; eauto; crush; eauto). apply H6 in HPler0. invert HPler0; try congruence. rewrite EQr0 in H8. @@ -658,7 +668,7 @@ Section CORRECTNESS. clear H0. clear H6. unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; simplify. + unfold check_address_parameter_unsigned in *; crush. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. @@ -666,24 +676,20 @@ Section CORRECTNESS. (** Modular preservation proof *) assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; simplify; try lia. + apply PtrofsExtra.add_mod; crush; try lia. exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) rewrite Integers.Ptrofs.signed_repr; try assumption. admit. (* FIXME: Register bounds. *) apply PtrofsExtra.of_int_mod. - rewrite Integers.Int.signed_repr; simplify; try split; try assumption. } + rewrite Integers.Int.signed_repr; crush. } (** Read bounds proof *) assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto. + { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. unfold stack_bounds in BOUNDS. exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. split; try lia; apply Integers.Ptrofs.unsigned_range_2. - simplify. - replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence. - apply Integers.Ptrofs.unsigned_range_2. } + small_tac. } (** Normalisation proof *) assert (Integers.Ptrofs.repr @@ -692,7 +698,7 @@ Section CORRECTNESS. as NORMALISE. { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. rewrite <- PtrofsExtra.mul_unsigned. - apply PtrofsExtra.mul_divu; simplify; auto; lia. } + apply PtrofsExtra.mul_divu; crush; auto. } (** Normalised bounds proof *) assert (0 <= @@ -704,11 +710,11 @@ Section CORRECTNESS. assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. unfold Integers.Ptrofs.divu at 2 in H0. rewrite H0. clear H0. - rewrite Integers.Ptrofs.unsigned_repr; simplify. + rewrite Integers.Ptrofs.unsigned_repr; crush. apply Zmult_lt_reg_r with (p := 4); try lia. repeat rewrite ZLib.div_mul_undo; try lia. - apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. - apply Z.div_le_upper_bound; lia. } + apply Z.div_pos; small_tac. + apply Z.div_le_upper_bound; small_tac. } inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; clear NORMALISE_BOUND. @@ -718,33 +724,21 @@ Section CORRECTNESS. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. apply assumption_32bit. - econstructor. econstructor. econstructor. simplify. - econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. crush. + econstructor. econstructor. econstructor. crush. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. all: big_tac. + 1: { apply st_greater_than_res. } + 2: { apply st_greater_than_res. } + (** Match assocmaps *) apply regs_lessdef_add_match; big_tac. (** Equality proof *) - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - rewrite ZERO in H7. clear ZERO. - setoid_rewrite Integers.Ptrofs.add_zero_l in H7. - - specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4)))). - - exploit H7. - rewrite Z2Nat.id; eauto. - apply Z.div_pos; lia. - - intros I. - match goal with | [ |- context [valueToNat ?x] ] => assert (Z.to_nat @@ -756,40 +750,35 @@ Section CORRECTNESS. valueToNat x) as EXPR_OK by admit end. - rewrite <- EXPR_OK. - rewrite NORMALISE in I. - rewrite H1 in I. - invert I. assumption. + + specialize (H7 (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4)))). + exploit H7; big_tac. (** RSBP preservation *) unfold arr_stack_based_pointers in ASBP. specialize (ASBP (Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; auto; intros I. - - rewrite NORMALISE in I. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - rewrite ZERO in I. clear ZERO. - simplify. - rewrite Integers.Ptrofs.add_zero_l in I. - rewrite H1 in I. - assumption. + exploit ASBP; big_tac. + rewrite NORMALISE in H0. rewrite H1 in H0. assumption. + (** Preamble *) - invert MARR. simplify. + invert MARR. crush. unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; simplify. + destruct (Archi.ptr64) eqn:ARCHI; crush. unfold reg_stack_based_pointers in RSBP. pose proof (RSBP r0) as RSBPr0. pose proof (RSBP r1) as RSBPr1. destruct (Registers.Regmap.get r0 rs) eqn:EQr0; - destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify. + destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. - rewrite ARCHI in H1. simplify. + rewrite ARCHI in H1. crush. subst. clear RSBPr1. @@ -798,7 +787,7 @@ Section CORRECTNESS. pose proof (H0 r0). pose proof (H0 r1). assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). + by (eapply RTL.max_reg_function_use; eauto; crush; eauto). assert (HPler1 : Ple r1 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). apply H6 in HPler0. @@ -810,7 +799,7 @@ Section CORRECTNESS. clear H0. clear H6. clear H8. unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; simplify. + unfold check_address_parameter_unsigned in *; crush. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) (Integers.Ptrofs.of_int @@ -820,30 +809,26 @@ Section CORRECTNESS. (** Modular preservation proof *) assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; simplify; try lia. + apply PtrofsExtra.add_mod; crush; try lia. exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) rewrite Integers.Ptrofs.signed_repr; try assumption. admit. (* FIXME: Register bounds. *) apply PtrofsExtra.of_int_mod. - apply IntExtra.add_mod; simplify; try lia. + apply IntExtra.add_mod; crush; try lia. exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) - apply IntExtra.mul_mod; simplify; try lia. + apply IntExtra.mul_mod; crush; try lia. exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) admit. (* FIXME: Register bounds. *) - rewrite Integers.Int.signed_repr; simplify; try split; try assumption. - rewrite Integers.Int.signed_repr; simplify; try split; try assumption. } + rewrite Integers.Int.signed_repr; crush. + rewrite Integers.Int.signed_repr; crush. } (** Read bounds proof *) assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto. + { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. unfold stack_bounds in BOUNDS. exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. split; try lia; apply Integers.Ptrofs.unsigned_range_2. - simplify. - replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence. - apply Integers.Ptrofs.unsigned_range_2. } + small_tac. } (** Normalisation proof *) assert (Integers.Ptrofs.repr @@ -852,7 +837,7 @@ Section CORRECTNESS. as NORMALISE. { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. rewrite <- PtrofsExtra.mul_unsigned. - apply PtrofsExtra.mul_divu; simplify; auto; lia. } + apply PtrofsExtra.mul_divu; crush. } (** Normalised bounds proof *) assert (0 <= @@ -864,10 +849,10 @@ Section CORRECTNESS. assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. unfold Integers.Ptrofs.divu at 2 in H0. rewrite H0. clear H0. - rewrite Integers.Ptrofs.unsigned_repr; simplify. + rewrite Integers.Ptrofs.unsigned_repr; crush. apply Zmult_lt_reg_r with (p := 4); try lia. repeat rewrite ZLib.div_mul_undo; try lia. - apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. + apply Z.div_pos; small_tac. apply Z.div_le_upper_bound; lia. } inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; @@ -878,8 +863,8 @@ Section CORRECTNESS. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. apply assumption_32bit. - econstructor. econstructor. econstructor. simplify. - econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. crush. + econstructor. econstructor. econstructor. crush. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. @@ -890,24 +875,13 @@ Section CORRECTNESS. all: big_tac. + 1: { apply st_greater_than_res. } + 2: { apply st_greater_than_res. } + (** Match assocmaps *) apply regs_lessdef_add_match; big_tac. (** Equality proof *) - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - rewrite ZERO in H7. clear ZERO. - setoid_rewrite Integers.Ptrofs.add_zero_l in H7. - - specialize (H7 (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4)))). - - exploit H7. - rewrite Z2Nat.id; eauto. - apply Z.div_pos; lia. - - intros I. match goal with | [ |- context [valueToNat ?x] ] => assert (Z.to_nat @@ -920,32 +894,28 @@ Section CORRECTNESS. as EXPR_OK by admit end. rewrite <- EXPR_OK. - rewrite NORMALISE in I. - rewrite H1 in I. - invert I. assumption. + + specialize (H7 (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4)))). + exploit H7; big_tac. (** RSBP preservation *) unfold arr_stack_based_pointers in ASBP. specialize (ASBP (Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; auto; intros I. - - rewrite NORMALISE in I. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - rewrite ZERO in I. clear ZERO. - simplify. - rewrite Integers.Ptrofs.add_zero_l in I. - rewrite H1 in I. - assumption. + exploit ASBP; big_tac. + rewrite NORMALISE in H0. rewrite H1 in H0. assumption. - + invert MARR. simplify. + + invert MARR. crush. unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; simplify. - rewrite ARCHI in H0. simplify. + destruct (Archi.ptr64) eqn:ARCHI; crush. + rewrite ARCHI in H0. crush. unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; simplify. + unfold check_address_parameter_signed in *; crush. assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. rewrite ZERO in H1. clear ZERO. @@ -958,14 +928,9 @@ Section CORRECTNESS. (** Read bounds proof *) assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as READ_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto. + { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); auto. - simplify. - replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence. - apply Integers.Ptrofs.unsigned_range_2. } + exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET)); big_tac. } (** Normalisation proof *) assert (Integers.Ptrofs.repr @@ -974,7 +939,7 @@ Section CORRECTNESS. as NORMALISE. { replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) at 1 by reflexivity. rewrite <- PtrofsExtra.mul_unsigned. - apply PtrofsExtra.mul_divu; simplify; auto; try lia. } + apply PtrofsExtra.mul_divu; crush. } (** Normalised bounds proof *) assert (0 <= @@ -986,10 +951,10 @@ Section CORRECTNESS. assert (forall x y, Integers.Ptrofs.divu x y = Integers.Ptrofs.divu x y ) by reflexivity. unfold Integers.Ptrofs.divu at 2 in H0. rewrite H0. clear H0. - rewrite Integers.Ptrofs.unsigned_repr; simplify. + rewrite Integers.Ptrofs.unsigned_repr; crush. apply Zmult_lt_reg_r with (p := 4); try lia. repeat rewrite ZLib.div_mul_undo; try lia. - apply Z.div_pos; try lia; apply Integers.Ptrofs.unsigned_range_2. + apply Z.div_pos; small_tac. apply Z.div_le_upper_bound; lia. } inversion NORMALISE_BOUND as [ NORMALISE_BOUND_LOW NORMALISE_BOUND_HIGH ]; @@ -1000,55 +965,43 @@ Section CORRECTNESS. eapply Smallstep.plus_one. eapply HTL.step_module; eauto. apply assumption_32bit. - econstructor. econstructor. econstructor. simplify. - econstructor. econstructor. econstructor. econstructor. simplify. + econstructor. econstructor. econstructor. crush. + econstructor. econstructor. econstructor. econstructor. crush. all: big_tac. + 1: { apply st_greater_than_res. } + 2: { apply st_greater_than_res. } + (** Match assocmaps *) apply regs_lessdef_add_match; big_tac. (** Equality proof *) - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - rewrite ZERO in H7. clear ZERO. - setoid_rewrite Integers.Ptrofs.add_zero_l in H7. + match goal with + | [ |- context [valueToNat ?x] ] => + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat x) + as EXPR_OK by admit + end. + rewrite <- EXPR_OK. specialize (H7 (Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - - exploit H7. - rewrite Z2Nat.id; eauto. - apply Z.div_pos; lia. - - intros I. - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat (ZToValue 32 (Integers.Ptrofs.unsigned OFFSET / 4))) - as EXPR_OK by admit. - rewrite <- EXPR_OK. - rewrite NORMALISE in I. - rewrite H1 in I. - invert I. assumption. + exploit H7; big_tac. (** RSBP preservation *) unfold arr_stack_based_pointers in ASBP. specialize (ASBP (Integers.Ptrofs.unsigned (Integers.Ptrofs.divu OFFSET (Integers.Ptrofs.repr 4)))). - exploit ASBP; auto; intros I. - - rewrite NORMALISE in I. - assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. - rewrite ZERO in I. clear ZERO. - simplify. - rewrite Integers.Ptrofs.add_zero_l in I. - rewrite H1 in I. - assumption. + exploit ASBP; big_tac. + rewrite NORMALISE in H0. rewrite H1 in H0. assumption. Admitted. Hint Resolve transl_iload_correct : htlproof. @@ -1069,24 +1022,24 @@ Section CORRECTNESS. inv_state. inv_arr_access. + (** Preamble *) - invert MARR. simplify. + invert MARR. crush. unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; simplify. + destruct (Archi.ptr64) eqn:ARCHI; crush. unfold reg_stack_based_pointers in RSBP. pose proof (RSBP r0) as RSBPr0. - destruct (Registers.Regmap.get r0 rs) eqn:EQr0; simplify. + destruct (Registers.Regmap.get r0 rs) eqn:EQr0; crush. - rewrite ARCHI in H1. simplify. + rewrite ARCHI in H1. crush. subst. pose proof MASSOC as MASSOC'. invert MASSOC'. pose proof (H0 r0). assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). + by (eapply RTL.max_reg_function_use; eauto; crush; eauto). apply H6 in HPler0. invert HPler0; try congruence. rewrite EQr0 in H8. @@ -1094,7 +1047,7 @@ Section CORRECTNESS. clear H0. clear H6. unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; simplify. + unfold check_address_parameter_signed in *; crush. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. @@ -1102,24 +1055,18 @@ Section CORRECTNESS. (** Modular preservation proof *) assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; simplify; try lia. + apply PtrofsExtra.add_mod; crush; try lia. exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) rewrite Integers.Ptrofs.signed_repr; try assumption. admit. (* FIXME: Register bounds. *) apply PtrofsExtra.of_int_mod. - rewrite Integers.Int.signed_repr; simplify; try split; try assumption. - } + rewrite Integers.Int.signed_repr; crush. } (** Write bounds proof *) assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto. + { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. unfold stack_bounds in BOUNDS. - exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. - split; try lia; apply Integers.Ptrofs.unsigned_range_2. - simplify. - replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence. + exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); big_tac. apply Integers.Ptrofs.unsigned_range_2. } (** Start of proof proper *) @@ -1128,7 +1075,7 @@ Section CORRECTNESS. eapply HTL.step_module; eauto. apply assumption_32bit. econstructor. econstructor. econstructor. - eapply Verilog.stmnt_runp_Vnonblock_arr. simplify. + eapply Verilog.stmnt_runp_Vnonblock_arr. crush. econstructor. eapply Verilog.erun_Vbinop with (EQ := ?[EQ7]). eapply Verilog.erun_Vbinop with (EQ := ?[EQ8]). @@ -1137,11 +1084,11 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - all: simplify. + all: crush. (** State Lookup *) unfold Verilog.merge_regs. - simplify. + crush. unfold_merge. apply AssocMap.gss. @@ -1150,33 +1097,36 @@ Section CORRECTNESS. econstructor; eauto. (** Match assocmaps *) - unfold Verilog.merge_regs. simplify. unfold_merge. + unfold Verilog.merge_regs. crush. unfold_merge. apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. (** States well formed *) - unfold state_st_wf. inversion 1. simplify. + unfold state_st_wf. inversion 1. crush. unfold Verilog.merge_regs. unfold_merge. apply AssocMap.gss. (** Equality proof *) - assert (Z.to_nat - (Integers.Ptrofs.unsigned - (Integers.Ptrofs.divu - OFFSET - (Integers.Ptrofs.repr 4))) - = - valueToNat (vdiv (vplus asr # r0 (ZToValue 32 z) ?EQ8) (ZToValue 32 4) ?EQ7)) - as EXPR_OK by admit. + match goal with + | [ |- context [valueToNat ?x] ] => + assert (Z.to_nat + (Integers.Ptrofs.unsigned + (Integers.Ptrofs.divu + OFFSET + (Integers.Ptrofs.repr 4))) + = + valueToNat x) + as EXPR_OK by admit + end. assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. econstructor. - repeat split; simplify. + repeat split; crush. unfold HTL.empty_stack. - simplify. + crush. unfold Verilog.merge_arrs. rewrite AssocMap.gcombine. @@ -1190,15 +1140,17 @@ Section CORRECTNESS. rewrite combine_length. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. apply list_repeat_len. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. rewrite list_repeat_len. rewrite H4. reflexivity. - intros. + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) + (Integers.Ptrofs.of_int (Integers.Int.repr z))) as OFFSET. + destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). erewrite Mem.load_store_same. @@ -1213,19 +1165,19 @@ Section CORRECTNESS. simpl. assert (Ple src (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); - apply H0 in H14. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H14; eauto. + apply H0 in H13. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H13; eauto. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. rewrite list_repeat_len. auto. assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in H14. - rewrite Z_div_mult in H14; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H14 by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in H14; unfold_constants; try lia. - rewrite H14. rewrite EXPR_OK. + rewrite Z.mul_comm in H13. + rewrite Z_div_mult in H13; try lia. + replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H13 by reflexivity. + rewrite <- PtrofsExtra.divu_unsigned in H13; unfold_constants; try lia. + rewrite H13. rewrite EXPR_OK. rewrite array_get_error_set_bound. reflexivity. unfold arr_length, arr_repeat. simpl. @@ -1242,12 +1194,11 @@ Section CORRECTNESS. right. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. - invert H13. rewrite Z2Nat.id in H19; try lia. apply Zmult_lt_compat_r with (p := 4) in H19; try lia. rewrite ZLib.div_mul_undo in H19; try lia. split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. } rewrite <- EXPR_OK. @@ -1259,26 +1210,26 @@ Section CORRECTNESS. eapply H7; eauto. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. rewrite list_repeat_len. auto. rewrite array_gso. unfold array_get_error. unfold arr_repeat. - simplify. + crush. apply list_repeat_lookup. lia. unfold_constants. intro. - apply Z2Nat.inj_iff in H14; try lia. + apply Z2Nat.inj_iff in H13; try lia. apply Z.div_pos; try lia. - apply Integers.Ptrofs.unsigned_range_2. + apply Integers.Ptrofs.unsigned_range. assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. unfold arr_stack_based_pointers. intros. destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - simplify. + crush. erewrite Mem.load_store_same. 2: { rewrite ZERO. rewrite Integers.Ptrofs.add_zero_l. @@ -1286,10 +1237,11 @@ Section CORRECTNESS. rewrite Integers.Ptrofs.unsigned_repr. exact H1. apply Integers.Ptrofs.unsigned_range_2. } - simplify. + crush. destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. destruct (Archi.ptr64); try discriminate. - pose proof (RSBP src). rewrite EQ_SRC in H0. assumption. + pose proof (RSBP src). rewrite EQ_SRC in H0. + assumption. simpl. erewrite Mem.load_store_other with (m1 := m). @@ -1307,7 +1259,7 @@ Section CORRECTNESS. apply Zmult_lt_compat_r with (p := 4) in H14; try lia. rewrite ZLib.div_mul_undo in H14; try lia. split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. } apply ASBP; assumption. @@ -1319,10 +1271,10 @@ Section CORRECTNESS. 2: { right. right. simpl. rewrite ZERO. rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr; simplify; try lia. - apply ZExtra.mod_0_bounds; simplify; try lia. } - simplify. - exploit (BOUNDS ptr); try lia. intros. simplify. + rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. + apply ZExtra.mod_0_bounds; crush; try lia. } + crush. + exploit (BOUNDS ptr); try lia. intros. crush. exploit (BOUNDS ptr v); try lia. intros. invert H0. match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. @@ -1339,19 +1291,19 @@ Section CORRECTNESS. apply X in H0. invert H0. congruence. + (** Preamble *) - invert MARR. simplify. + invert MARR. crush. unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; simplify. + destruct (Archi.ptr64) eqn:ARCHI; crush. unfold reg_stack_based_pointers in RSBP. pose proof (RSBP r0) as RSBPr0. pose proof (RSBP r1) as RSBPr1. destruct (Registers.Regmap.get r0 rs) eqn:EQr0; - destruct (Registers.Regmap.get r1 rs) eqn:EQr1; simplify. + destruct (Registers.Regmap.get r1 rs) eqn:EQr1; crush. - rewrite ARCHI in H1. simplify. + rewrite ARCHI in H1. crush. subst. clear RSBPr1. @@ -1360,7 +1312,7 @@ Section CORRECTNESS. pose proof (H0 r0). pose proof (H0 r1). assert (HPler0 : Ple r0 (RTL.max_reg_function f)) - by (eapply RTL.max_reg_function_use; eauto; simplify; eauto). + by (eapply RTL.max_reg_function_use; eauto; crush; eauto). assert (HPler1 : Ple r1 (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto). apply H6 in HPler0. @@ -1372,7 +1324,7 @@ Section CORRECTNESS. clear H0. clear H6. clear H8. unfold check_address_parameter_signed in *; - unfold check_address_parameter_unsigned in *; simplify. + unfold check_address_parameter_unsigned in *; crush. remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) (Integers.Ptrofs.of_int @@ -1382,31 +1334,27 @@ Section CORRECTNESS. (** Modular preservation proof *) assert (Integers.Ptrofs.unsigned OFFSET mod 4 = 0) as MOD_PRESERVE. { rewrite HeqOFFSET. - apply PtrofsExtra.add_mod; simplify; try lia. + apply PtrofsExtra.add_mod; crush; try lia. exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) rewrite Integers.Ptrofs.signed_repr; try assumption. admit. (* FIXME: Register bounds. *) apply PtrofsExtra.of_int_mod. - apply IntExtra.add_mod; simplify; try lia. + apply IntExtra.add_mod; crush; try lia. exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) - apply IntExtra.mul_mod; simplify; try lia. + apply IntExtra.mul_mod; crush; try lia. exists 1073741824. reflexivity. (* FIXME: This is sadness inducing. *) admit. (* FIXME: Register bounds. *) - rewrite Integers.Int.signed_repr; simplify; try split; try assumption. - rewrite Integers.Int.signed_repr; simplify; try split; try assumption. + rewrite Integers.Int.signed_repr; crush; try split; try assumption. + rewrite Integers.Int.signed_repr; crush; try split; try assumption. } (** Write bounds proof *) assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto. + { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. unfold stack_bounds in BOUNDS. exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. split; try lia; apply Integers.Ptrofs.unsigned_range_2. - simplify. - replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence. - apply Integers.Ptrofs.unsigned_range_2. } + small_tac. } (** Start of proof proper *) eexists. split. @@ -1414,7 +1362,7 @@ Section CORRECTNESS. eapply HTL.step_module; eauto. apply assumption_32bit. econstructor. econstructor. econstructor. - eapply Verilog.stmnt_runp_Vnonblock_arr. simplify. + eapply Verilog.stmnt_runp_Vnonblock_arr. crush. econstructor. eapply Verilog.erun_Vbinop with (EQ := ?[EQ9]). eapply Verilog.erun_Vbinop with (EQ := ?[EQ10]). @@ -1426,11 +1374,11 @@ Section CORRECTNESS. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. econstructor. - all: simplify. + all: crush. (** State Lookup *) unfold Verilog.merge_regs. - simplify. + crush. unfold_merge. apply AssocMap.gss. @@ -1439,12 +1387,12 @@ Section CORRECTNESS. econstructor; eauto. (** Match assocmaps *) - unfold Verilog.merge_regs. simplify. unfold_merge. + unfold Verilog.merge_regs. crush. unfold_merge. apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. (** States well formed *) - unfold state_st_wf. inversion 1. simplify. + unfold state_st_wf. inversion 1. crush. unfold Verilog.merge_regs. unfold_merge. apply AssocMap.gss. @@ -1465,9 +1413,9 @@ Section CORRECTNESS. inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. econstructor. - repeat split; simplify. + repeat split; crush. unfold HTL.empty_stack. - simplify. + crush. unfold Verilog.merge_arrs. rewrite AssocMap.gcombine. @@ -1481,15 +1429,18 @@ Section CORRECTNESS. rewrite combine_length. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. apply list_repeat_len. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. rewrite list_repeat_len. rewrite H4. reflexivity. - intros. + remember (Integers.Ptrofs.add (Integers.Ptrofs.repr (valueToZ asr # r0)) + (Integers.Ptrofs.of_int + (Integers.Int.add (Integers.Int.mul (valueToInt asr # r1) (Integers.Int.repr z)) + (Integers.Int.repr z0)))) as OFFSET. destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). erewrite Mem.load_store_same. @@ -1504,19 +1455,19 @@ Section CORRECTNESS. simpl. assert (Ple src (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); - apply H0 in H21. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H21; eauto. + apply H0 in H20. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H20; eauto. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. rewrite list_repeat_len. auto. assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in H21. - rewrite Z_div_mult in H21; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H21 by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in H21; unfold_constants; try lia. - rewrite H21. rewrite EXPR_OK. + rewrite Z.mul_comm in H20. + rewrite Z_div_mult in H20; try lia. + replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H20 by reflexivity. + rewrite <- PtrofsExtra.divu_unsigned in H20; unfold_constants; try lia. + rewrite H20. rewrite EXPR_OK. rewrite array_get_error_set_bound. reflexivity. unfold arr_length, arr_repeat. simpl. @@ -1533,12 +1484,11 @@ Section CORRECTNESS. right. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. - invert H20. rewrite Z2Nat.id in H22; try lia. apply Zmult_lt_compat_r with (p := 4) in H22; try lia. rewrite ZLib.div_mul_undo in H22; try lia. split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. } rewrite <- EXPR_OK. @@ -1550,17 +1500,17 @@ Section CORRECTNESS. eapply H7; eauto. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. rewrite list_repeat_len. auto. rewrite array_gso. unfold array_get_error. unfold arr_repeat. - simplify. + crush. apply list_repeat_lookup. lia. unfold_constants. intro. - apply Z2Nat.inj_iff in H21; try lia. + apply Z2Nat.inj_iff in H20; try lia. apply Z.div_pos; try lia. apply Integers.Ptrofs.unsigned_range. @@ -1569,7 +1519,7 @@ Section CORRECTNESS. intros. destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - simplify. + crush. erewrite Mem.load_store_same. 2: { rewrite ZERO. rewrite Integers.Ptrofs.add_zero_l. @@ -1577,7 +1527,7 @@ Section CORRECTNESS. rewrite Integers.Ptrofs.unsigned_repr. exact H1. apply Integers.Ptrofs.unsigned_range_2. } - simplify. + crush. destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. destruct (Archi.ptr64); try discriminate. pose proof (RSBP src). rewrite EQ_SRC in H0. @@ -1599,7 +1549,7 @@ Section CORRECTNESS. apply Zmult_lt_compat_r with (p := 4) in H21; try lia. rewrite ZLib.div_mul_undo in H21; try lia. split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. } apply ASBP; assumption. @@ -1611,10 +1561,10 @@ Section CORRECTNESS. 2: { right. right. simpl. rewrite ZERO. rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr; simplify; try lia. - apply ZExtra.mod_0_bounds; simplify; try lia. } - simplify. - exploit (BOUNDS ptr); try lia. intros. simplify. + rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. + apply ZExtra.mod_0_bounds; crush; try lia. } + crush. + exploit (BOUNDS ptr); try lia. intros. crush. exploit (BOUNDS ptr v); try lia. intros. invert H0. match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. @@ -1630,14 +1580,14 @@ Section CORRECTNESS. (Integers.Ptrofs.repr ptr))) v). apply X in H0. invert H0. congruence. - + invert MARR. simplify. + + invert MARR. crush. unfold Op.eval_addressing in H0. - destruct (Archi.ptr64) eqn:ARCHI; simplify. - rewrite ARCHI in H0. simplify. + destruct (Archi.ptr64) eqn:ARCHI; crush. + rewrite ARCHI in H0. crush. unfold check_address_parameter_unsigned in *; - unfold check_address_parameter_signed in *; simplify. + unfold check_address_parameter_signed in *; crush. assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. rewrite ZERO in H1. clear ZERO. @@ -1650,14 +1600,12 @@ Section CORRECTNESS. (** Write bounds proof *) assert (Integers.Ptrofs.unsigned OFFSET < f.(RTL.fn_stacksize)) as WRITE_BOUND_HIGH. - { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; simplify; auto. + { destruct (Integers.Ptrofs.unsigned OFFSET <? f.(RTL.fn_stacksize)) eqn:EQ; crush; auto. unfold stack_bounds in BOUNDS. exploit (BOUNDS (Integers.Ptrofs.unsigned OFFSET) (Registers.Regmap.get src rs)); auto. - simplify. + crush. replace (Integers.Ptrofs.repr 0) with (Integers.Ptrofs.zero) by reflexivity. - rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr. intros. simplify. congruence. - apply Integers.Ptrofs.unsigned_range_2. } + small_tac. } (** Start of proof proper *) eexists. split. @@ -1665,14 +1613,14 @@ Section CORRECTNESS. eapply HTL.step_module; eauto. apply assumption_32bit. econstructor. econstructor. econstructor. - eapply Verilog.stmnt_runp_Vnonblock_arr. simplify. + eapply Verilog.stmnt_runp_Vnonblock_arr. crush. econstructor. econstructor. econstructor. econstructor. - all: simplify. + all: crush. (** State Lookup *) unfold Verilog.merge_regs. - simplify. + crush. unfold_merge. apply AssocMap.gss. @@ -1681,12 +1629,12 @@ Section CORRECTNESS. econstructor; eauto. (** Match assocmaps *) - unfold Verilog.merge_regs. simplify. unfold_merge. + unfold Verilog.merge_regs. crush. unfold_merge. apply regs_lessdef_add_greater. apply greater_than_max_func. assumption. (** States well formed *) - unfold state_st_wf. inversion 1. simplify. + unfold state_st_wf. inversion 1. crush. unfold Verilog.merge_regs. unfold_merge. apply AssocMap.gss. @@ -1705,9 +1653,9 @@ Section CORRECTNESS. inversion MASSOC; revert HeqOFFSET; subst; clear MASSOC; intros HeqOFFSET. econstructor. - repeat split; simplify. + repeat split; crush. unfold HTL.empty_stack. - simplify. + crush. unfold Verilog.merge_arrs. rewrite AssocMap.gcombine. @@ -1721,15 +1669,15 @@ Section CORRECTNESS. rewrite combine_length. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. apply list_repeat_len. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. rewrite list_repeat_len. rewrite H4. reflexivity. - intros. + remember i0 as OFFSET. destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). erewrite Mem.load_store_same. @@ -1744,19 +1692,19 @@ Section CORRECTNESS. simpl. assert (Ple src (RTL.max_reg_function f)) by (eapply RTL.max_reg_function_use; eauto; simpl; auto); - apply H0 in H10. - destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H10; eauto. + apply H0 in H8. + destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; constructor; invert H8; eauto. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. rewrite list_repeat_len. auto. assert (4 * ptr / 4 = Integers.Ptrofs.unsigned OFFSET / 4) by (f_equal; assumption). - rewrite Z.mul_comm in H10. - rewrite Z_div_mult in H10; try lia. - replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H10 by reflexivity. - rewrite <- PtrofsExtra.divu_unsigned in H10; unfold_constants; try lia. - rewrite H10. rewrite EXPR_OK. + rewrite Z.mul_comm in H8. + rewrite Z_div_mult in H8; try lia. + replace 4 with (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr 4)) in H8 by reflexivity. + rewrite <- PtrofsExtra.divu_unsigned in H8; unfold_constants; try lia. + rewrite H8. rewrite EXPR_OK. rewrite array_get_error_set_bound. reflexivity. unfold arr_length, arr_repeat. simpl. @@ -1773,12 +1721,11 @@ Section CORRECTNESS. right. apply ZExtra.mod_0_bounds; try lia. apply ZLib.Z_mod_mult'. - invert H8. rewrite Z2Nat.id in H12; try lia. apply Zmult_lt_compat_r with (p := 4) in H12; try lia. rewrite ZLib.div_mul_undo in H12; try lia. split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. } rewrite <- EXPR_OK. @@ -1790,17 +1737,17 @@ Section CORRECTNESS. eapply H7; eauto. rewrite <- array_set_len. - unfold arr_repeat. simplify. + unfold arr_repeat. crush. rewrite list_repeat_len. auto. rewrite array_gso. unfold array_get_error. unfold arr_repeat. - simplify. + crush. apply list_repeat_lookup. lia. unfold_constants. intro. - apply Z2Nat.inj_iff in H10; try lia. + apply Z2Nat.inj_iff in H8; try lia. apply Z.div_pos; try lia. apply Integers.Ptrofs.unsigned_range. @@ -1809,7 +1756,7 @@ Section CORRECTNESS. intros. destruct (4 * ptr ==Z Integers.Ptrofs.unsigned OFFSET). - simplify. + crush. erewrite Mem.load_store_same. 2: { rewrite ZERO. rewrite Integers.Ptrofs.add_zero_l. @@ -1817,7 +1764,7 @@ Section CORRECTNESS. rewrite Integers.Ptrofs.unsigned_repr. exact H1. apply Integers.Ptrofs.unsigned_range_2. } - simplify. + crush. destruct (Registers.Regmap.get src rs) eqn:EQ_SRC; try constructor. destruct (Archi.ptr64); try discriminate. pose proof (RSBP src). rewrite EQ_SRC in H0. @@ -1839,7 +1786,7 @@ Section CORRECTNESS. apply Zmult_lt_compat_r with (p := 4) in H10; try lia. rewrite ZLib.div_mul_undo in H10; try lia. split; try lia. - apply Z.le_trans with (m := RTL.fn_stacksize f); simplify; lia. + apply Z.le_trans with (m := RTL.fn_stacksize f); crush; lia. } apply ASBP; assumption. @@ -1851,10 +1798,10 @@ Section CORRECTNESS. 2: { right. right. simpl. rewrite ZERO. rewrite Integers.Ptrofs.add_zero_l. - rewrite Integers.Ptrofs.unsigned_repr; simplify; try lia. - apply ZExtra.mod_0_bounds; simplify; try lia. } - simplify. - exploit (BOUNDS ptr); try lia. intros. simplify. + rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. + apply ZExtra.mod_0_bounds; crush; try lia. } + crush. + exploit (BOUNDS ptr); try lia. intros. crush. exploit (BOUNDS ptr v); try lia. intros. invert H0. match goal with | |- ?x = _ => destruct x eqn:EQ end; try reflexivity. @@ -1906,66 +1853,10 @@ Section CORRECTNESS. apply boolToValue_ValueToBool. constructor. - unfold Verilog.merge_regs. - unfold_merge. - apply AssocMap.gss. - - destruct b. - rewrite assumption_32bit. - simplify. - apply match_state with (sp' := sp'); eauto. - unfold Verilog.merge_regs. - unfold_merge. - apply regs_lessdef_add_greater. apply greater_than_max_func. - assumption. - - unfold state_st_wf. intros. - invert H3. - unfold Verilog.merge_regs. unfold_merge. - apply AssocMap.gss. - - (** Match arrays *) - invert MARR. simplify. - econstructor. - repeat split; simplify. - unfold HTL.empty_stack. - simplify. - unfold Verilog.merge_arrs. - - rewrite AssocMap.gcombine. - 2: { reflexivity. } - rewrite AssocMap.gss. - unfold Verilog.merge_arr. - setoid_rewrite H4. - reflexivity. - - rewrite combine_length. - unfold arr_repeat. simplify. - rewrite list_repeat_len. - reflexivity. - - unfold arr_repeat. simplify. - rewrite list_repeat_len. - congruence. - - intros. - erewrite array_get_error_equal. - eauto. apply combine_none. - assumption. - - rewrite assumption_32bit. - apply match_state with (sp' := sp'); eauto. - unfold Verilog.merge_regs. unfold_merge. - apply regs_lessdef_add_greater. apply greater_than_max_func. - assumption. - - unfold state_st_wf. intros. - invert H1. - unfold Verilog.merge_regs. unfold_merge. - apply AssocMap.gss. + big_tac. - (** Match arrays *) - all: invert MARR. big_tac. + invert MARR. + destruct b; rewrite assumption_32bit; big_tac. Unshelve. constructor. @@ -2018,6 +1909,8 @@ Section CORRECTNESS. constructor. constructor. unfold state_st_wf in WF; big_tac; eauto. + apply st_greater_than_res. + apply st_greater_than_res. apply HTL.step_finish. unfold Verilog.merge_regs. @@ -2043,6 +1936,8 @@ Section CORRECTNESS. constructor. constructor. constructor. unfold state_st_wf in WF; big_tac; eauto. + apply st_greater_than_res. + apply st_greater_than_res. apply HTL.step_finish. unfold Verilog.merge_regs. @@ -2081,7 +1976,7 @@ Section CORRECTNESS. inversion MSTATE; subst. inversion TF; subst. econstructor. split. apply Smallstep.plus_one. - eapply HTL.step_call. simplify. + eapply HTL.step_call. crush. apply match_state with (sp' := stk); eauto. @@ -2093,8 +1988,6 @@ Section CORRECTNESS. constructor. - apply list_repeat_len. - intros. destruct (Mem.load AST.Mint32 m' stk (Integers.Ptrofs.unsigned (Integers.Ptrofs.add Integers.Ptrofs.zero @@ -2103,17 +1996,20 @@ Section CORRECTNESS. pose proof H as ALLOC. eapply LOAD_ALLOC in ALLOC. 2: { exact LOAD. } + ptrofs. rewrite LOAD. rewrite ALLOC. repeat constructor. - constructor. + + ptrofs. rewrite LOAD. + repeat constructor. unfold reg_stack_based_pointers. intros. - unfold RTL.init_regs; simplify. + unfold RTL.init_regs; crush. destruct (RTL.fn_params f); rewrite Registers.Regmap.gi; constructor. unfold arr_stack_based_pointers. intros. - simplify. + crush. destruct (Mem.load AST.Mint32 m' stk (Integers.Ptrofs.unsigned (Integers.Ptrofs.add Integers.Ptrofs.zero @@ -2134,36 +2030,34 @@ Section CORRECTNESS. unfold Mem.alloc in H. invert H. - simplify. + crush. unfold Mem.load. intros. match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. invert v0. unfold Mem.range_perm in H3. - unfold Mem.perm in H3. simplify. + unfold Mem.perm in H3. crush. unfold Mem.perm_order' in H3. - rewrite Integers.Ptrofs.add_zero_l in H3. - rewrite Integers.Ptrofs.unsigned_repr in H3; simplify; try lia. - exploit (H3 ptr). lia. intros. + small_tac. + exploit (H3 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. rewrite Maps.PMap.gss in H8. match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. - simplify. + crush. apply proj_sumbool_true in H10. lia. unfold Mem.alloc in H. invert H. - simplify. + crush. unfold Mem.store. intros. match goal with | |- context[if ?x then _ else _] => destruct x end; try congruence. invert v0. unfold Mem.range_perm in H3. - unfold Mem.perm in H3. simplify. + unfold Mem.perm in H3. crush. unfold Mem.perm_order' in H3. - rewrite Integers.Ptrofs.add_zero_l in H3. - rewrite Integers.Ptrofs.unsigned_repr in H3; simplify; try lia. - exploit (H3 ptr). lia. intros. + small_tac. + exploit (H3 ptr). rewrite Integers.Ptrofs.unsigned_repr; small_tac. intros. rewrite Maps.PMap.gss in H8. match goal with | H8 : context[if ?x then _ else _] |- _ => destruct x eqn:EQ end; try contradiction. - simplify. + crush. apply proj_sumbool_true in H10. lia. Opaque Mem.alloc. Opaque Mem.load. |