From 0e0c64bf93f33044d299bfd5456d9a6b00992a0d Mon Sep 17 00:00:00 2001 From: James Pollard Date: Wed, 1 Jul 2020 20:09:15 +0100 Subject: Improve (?) automation. --- src/common/Coquplib.v | 19 +- src/common/IntegerExtra.v | 33 +- src/translation/HTLgenproof.v | 708 ++++++++++++++++++------------------------ src/translation/HTLgenspec.v | 2 +- src/verilog/Array.v | 69 ++-- 5 files changed, 380 insertions(+), 451 deletions(-) (limited to 'src') diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index ba0a5dc..c9361c2 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -23,12 +23,14 @@ From Coq Require Export List Bool. +Require Import Lia. + From coqup Require Import Show. (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) From compcert.lib Require Export Coqlib. -From compcert Require Integers. +From compcert Require Import Integers. Ltac unfold_rec c := unfold c; fold c. @@ -44,18 +46,21 @@ Ltac solve_by_invert := solve_by_inverts 1. Ltac invert x := inversion x; subst; clear x. +Ltac destruct_match := + match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end. + Ltac clear_obvious := repeat match goal with | [ H : ex _ |- _ ] => invert H - | [ H : ?C _ = ?C _ |- _ ] => invert H + | [ H : Some _ = Some _ |- _ ] => invert H | [ H : _ /\ _ |- _ ] => invert H end. Ltac nicify_goals := repeat match goal with | [ |- _ /\ _ ] => split - | [ |- Some _ = Some _ ] => try reflexivity - | [ _ : ?x |- ?x ] => assumption + | [ |- Some _ = Some _ ] => f_equal + | [ |- S _ = S _ ] => f_equal end. Ltac kill_bools := @@ -124,9 +129,9 @@ Ltac unfold_constants := end end. -Ltac simplify := unfold_constants; simpl in *; - repeat (clear_obvious; nicify_goals; kill_bools); - simpl in *; try discriminate. +Ltac crush := intros; unfold_constants; simpl in *; + repeat (clear_obvious; nicify_goals; kill_bools); + simpl in *; try discriminate; try congruence; try lia; try assumption. Global Opaque Nat.div. Global Opaque Z.mul. diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index 7d3156b..6bac18d 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -27,7 +27,7 @@ Module PtrofsExtra. rewrite Zmod_mod | [ _ : _ |- context[(_ mod Ptrofs.modulus) mod m ] ] => rewrite <- Zmod_div_mod; - try (simplify; lia || assumption) + try (crush; lia || assumption) | [ _ : _ |- context[Ptrofs.modulus mod m] ] => rewrite Zdivide_mod with (a := Ptrofs.modulus); @@ -65,7 +65,7 @@ Module PtrofsExtra. | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] => rewrite <- Zmod_div_mod; try lia; try assumption | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed - end; try (simplify; lia); ptrofs_mod_tac m. + end; try crush; ptrofs_mod_tac m. Qed. Lemma of_int_mod : @@ -96,7 +96,7 @@ Module PtrofsExtra. | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] => rewrite <- Zmod_div_mod; try lia; try assumption | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed - end; try (simplify; lia); ptrofs_mod_tac m. + end; try(crush; lia); ptrofs_mod_tac m. Qed. Lemma add_mod : @@ -115,7 +115,7 @@ Module PtrofsExtra. | [ _ : _ |- context[_ mod Ptrofs.modulus mod m] ] => rewrite <- Zmod_div_mod; try lia; try assumption | [ _ : _ |- context[Ptrofs.unsigned _] ] => rewrite Ptrofs.unsigned_signed - end; try (simplify; lia); ptrofs_mod_tac m. + end; try (crush; lia); ptrofs_mod_tac m. Qed. Lemma mul_divu : @@ -156,7 +156,7 @@ Module PtrofsExtra. eapply Z.le_trans. exact H0. rewrite Z.mul_comm. - apply Z.le_mul_diag_r; simplify; lia. + apply Z.le_mul_diag_r; crush. Qed. Lemma mul_unsigned : @@ -184,6 +184,23 @@ Module PtrofsExtra. Qed. End PtrofsExtra. +Ltac ptrofs := + repeat match goal with + | [ |- context[Ptrofs.add (Ptrofs.zero) _] ] => setoid_rewrite Ptrofs.add_zero_l + | [ H : context[Ptrofs.add (Ptrofs.zero) _] |- _ ] => setoid_rewrite Ptrofs.add_zero_l in H + + | [ |- context[Ptrofs.repr 0] ] => replace (Ptrofs.repr 0) with Ptrofs.zero by reflexivity + | [ H : context[Ptrofs.repr 0] |- _ ] => + replace (Ptrofs.repr 0) with Ptrofs.zero in H by reflexivity + + | [ H: context[Ptrofs.unsigned (Ptrofs.repr (Ptrofs.unsigned _))] |- _ ] => + setoid_rewrite Ptrofs.unsigned_repr in H; [>| apply Ptrofs.unsigned_range_2] + | [ |- context[Ptrofs.unsigned (Ptrofs.repr (Ptrofs.unsigned _))] ] => + rewrite Ptrofs.unsigned_repr; [>| apply Ptrofs.unsigned_range_2] + + | [ |- context[0 <= Ptrofs.unsigned _] ] => apply Ptrofs.unsigned_range_2 + end. + Module IntExtra. Ltac int_mod_match m := @@ -202,7 +219,7 @@ Module IntExtra. rewrite Zmod_mod | [ _ : _ |- context[(_ mod Int.modulus) mod m ] ] => rewrite <- Zmod_div_mod; - try (simplify; lia || assumption) + try (crush; lia || assumption) | [ _ : _ |- context[Int.modulus mod m] ] => rewrite Zdivide_mod with (a := Int.modulus); @@ -242,7 +259,7 @@ Module IntExtra. | [ _ : _ |- context[_ mod Int.modulus mod m] ] => rewrite <- Zmod_div_mod; try lia; try assumption | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed - end; try (simplify; lia); int_mod_tac m. + end; try (crush; lia); int_mod_tac m. Qed. Lemma add_mod : @@ -261,6 +278,6 @@ Module IntExtra. | [ _ : _ |- context[_ mod Int.modulus mod m] ] => rewrite <- Zmod_div_mod; try lia; try assumption | [ _ : _ |- context[Int.unsigned _] ] => rewrite Int.unsigned_signed - end; try (simplify; lia); int_mod_tac m. + end; try (crush; lia); int_mod_tac m. Qed. End IntExtra. 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 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 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 + 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 + 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 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 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. diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index a78256b..0cdecba 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -426,7 +426,7 @@ Proof. destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; destruct (RTL.fn_stacksize f nth_error (list_set i x l) i = Some x. Proof. - induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder. + induction l; intros; destruct i; crush; firstorder. Qed. Hint Resolve list_set_spec1 : array. @@ -37,7 +37,7 @@ Lemma list_set_spec2 {A : Type} : forall l i (x : A) d, i < length l -> nth i (list_set i x l) d = x. Proof. - induction l; intros; destruct i; simplify; try lia; try reflexivity; firstorder. + induction l; intros; destruct i; crush; firstorder. Qed. Hint Resolve list_set_spec2 : array. @@ -46,7 +46,7 @@ Lemma list_set_spec3 {A : Type} : i1 <> i2 -> nth_error (list_set i1 x l) i2 = nth_error l i2. Proof. - induction l; intros; destruct i1; destruct i2; simplify; try lia; try reflexivity; firstorder. + induction l; intros; destruct i1; destruct i2; crush; firstorder. Qed. Hint Resolve list_set_spec3 : array. @@ -56,7 +56,7 @@ Lemma array_set_wf {A : Type} : Proof. induction l; intros; destruct i; auto. - invert H; simplify; auto. + invert H; crush; auto. Qed. Definition array_set {A : Type} (i : nat) (x : A) (a : Array A) := @@ -72,7 +72,7 @@ Proof. intros. rewrite <- a.(arr_wf) in H. - unfold array_set. simplify. + unfold array_set. crush. eauto with array. Qed. Hint Resolve array_set_spec1 : array. @@ -84,7 +84,7 @@ Proof. intros. rewrite <- a.(arr_wf) in H. - unfold array_set. simplify. + unfold array_set. crush. eauto with array. Qed. Hint Resolve array_set_spec2 : array. @@ -93,7 +93,7 @@ Lemma array_set_len {A : Type} : forall a i (x : A), a.(arr_length) = (array_set i x a).(arr_length). Proof. - unfold array_set. simplify. reflexivity. + unfold array_set. crush. Qed. Definition array_get_error {A : Type} (i : nat) (a : Array A) : option A := @@ -104,7 +104,7 @@ Lemma array_get_error_equal {A : Type} : a.(arr_contents) = b.(arr_contents) -> array_get_error i a = array_get_error i b. Proof. - unfold array_get_error. congruence. + unfold array_get_error. crush. Qed. Lemma array_get_error_bound {A : Type} : @@ -142,7 +142,7 @@ Proof. unfold array_get_error. unfold array_set. - simplify. + crush. eauto with array. Qed. @@ -180,18 +180,17 @@ Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A := Lemma list_repeat'_len {A : Type} : forall (a : A) n l, length (list_repeat' l a n) = (n + Datatypes.length l)%nat. Proof. - induction n; intros; simplify; try reflexivity. + induction n; intros; crush; try reflexivity. specialize (IHn (a :: l)). rewrite IHn. - simplify. - lia. + crush. Qed. Lemma list_repeat'_app {A : Type} : forall (a : A) n l, list_repeat' l a n = list_repeat' [] a n ++ l. Proof. - induction n; intros; simplify; try reflexivity. + induction n; intros; crush; try reflexivity. pose proof IHn. specialize (H (a :: l)). @@ -207,7 +206,7 @@ Qed. Lemma list_repeat'_head_tail {A : Type} : forall n (a : A), a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]. Proof. - induction n; intros; simplify; try reflexivity. + induction n; intros; crush; try reflexivity. rewrite list_repeat'_app. replace (a :: list_repeat' [] a n ++ [a]) with (list_repeat' [] a n ++ [a] ++ [a]). @@ -232,17 +231,17 @@ Proof. intros. unfold list_repeat. rewrite list_repeat'_len. - simplify. lia. + crush. Qed. Lemma dec_list_repeat_spec {A : Type} : forall n (a : A) a', (forall x x' : A, {x' = x} + {~ x' = x}) -> In a' (list_repeat a n) -> a' = a. Proof. - induction n; intros; simplify; try contradiction. + induction n; intros; crush. unfold list_repeat in *. - simplify. + crush. rewrite list_repeat'_app in H. pose proof (X a a'). @@ -278,14 +277,19 @@ Lemma list_repeat_lookup {A : Type} : Proof. induction n; intros. - destruct i; simplify; lia. + destruct i; crush. rewrite list_repeat_cons. - destruct i; simplify; firstorder. + destruct i; crush; firstorder. Qed. Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n). +Lemma arr_repeat_length {A : Type} : forall n (a : A), arr_length (arr_repeat a n) = n. +Proof. + unfold list_repeat. crush. apply list_repeat_len. +Qed. + Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C := match x, y with | a :: t, b :: t' => f a b :: list_combine f t t' @@ -295,9 +299,9 @@ Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) Lemma list_combine_length {A B C : Type} (f : A -> B -> C) : forall (x : list A) (y : list B), length (list_combine f x y) = min (length x) (length y). Proof. - induction x; intros; simplify; try reflexivity. + induction x; intros; crush. - destruct y; simplify; auto. + destruct y; crush; auto. Qed. Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C := @@ -310,15 +314,24 @@ Proof. unfold combine. unfold make_array. - simplify. + crush. rewrite <- (arr_wf x) in *. rewrite <- (arr_wf y) in *. - destruct (arr_contents x); simplify. - - reflexivity. - - destruct (arr_contents y); simplify. - f_equal. - rewrite list_combine_length. - destruct (Min.min_dec (length l) (length l0)); congruence. + destruct (arr_contents x); destruct (arr_contents y); crush. + rewrite list_combine_length. + destruct (Min.min_dec (length l) (length l0)); congruence. Qed. + +Ltac array := + try match goal with + | [ |- context[arr_length (combine _ _ _)] ] => + rewrite combine_length + | [ |- context[length (list_repeat _ _)] ] => + rewrite list_repeat_len + | |- context[array_get_error _ (arr_repeat ?x _) = Some ?x] => + unfold array_get_error, arr_repeat + | |- context[nth_error (list_repeat ?x _) _ = Some ?x] => + apply list_repeat_lookup + end. -- cgit From 995ab555d848fcf6188734e6b46677131d4cc173 Mon Sep 17 00:00:00 2001 From: James Pollard Date: Wed, 1 Jul 2020 20:19:04 +0100 Subject: Tidy up (?) automation slightly... --- src/translation/HTLgenproof.v | 37 +++++++++++++++++-------------------- 1 file changed, 17 insertions(+), 20 deletions(-) (limited to 'src') diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index f248e25..6e470d5 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -436,44 +436,41 @@ Section CORRECTNESS. 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_arrs _ _] ] => unfold Verilog.merge_arrs | [ |- context[Verilog.merge_arr] ] => unfold Verilog.merge_arr + | [ |- context[Verilog.merge_regs _ _] ] => unfold Verilog.merge_regs; crush; unfold_merge + | [ |- context[reg_stack_based_pointers] ] => unfold reg_stack_based_pointers; intros + | [ |- context[Verilog.arr_assocmap_set _ _ _ _] ] => unfold Verilog.arr_assocmap_set + + | [ |- context[HTL.empty_stack] ] => unfold HTL.empty_stack + + | [ |- context[_ # ?d <- _ ! ?d] ] => rewrite AssocMap.gss + | [ |- context[_ # ?d <- _ ! ?s] ] => rewrite AssocMap.gso | [ |- 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 + | [ |- context[array_get_error _ (combine Verilog.merge_cell (arr_repeat None _) _)] ] => + rewrite combine_lookup_first + | [ |- state_st_wf _ _ ] => unfold state_st_wf; inversion 1 + | [ |- context[match_states _ _] ] => econstructor; auto + | [ |- match_arrs _ _ _ _ _ ] => econstructor; auto | [ |- 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 + | [ H : ?asa ! ?r = Some _ |- Verilog.arr_assocmap_lookup ?asa ?r _ = Some _ ] => + unfold Verilog.arr_assocmap_lookup; setoid_rewrite H; f_equal | [ |- 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. -- cgit