diff options
author | James Pollard <james@pollard.dev> | 2020-06-17 23:08:32 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-06-17 23:08:32 +0100 |
commit | 00c579e603478d452959dde0ec61672d7b5d27a4 (patch) | |
tree | 182b9c995c5ab396a400991e427377aa3822bf2b /src | |
parent | 58f0022a8b5f9ab42e1a8515a77820a9d086ba76 (diff) | |
download | vericert-kvx-00c579e603478d452959dde0ec61672d7b5d27a4.tar.gz vericert-kvx-00c579e603478d452959dde0ec61672d7b5d27a4.zip |
Some (very) useful lemmas about arrays.
Diffstat (limited to 'src')
-rw-r--r-- | src/common/Coquplib.v | 2 | ||||
-rw-r--r-- | src/translation/HTLgenproof.v | 36 | ||||
-rw-r--r-- | src/verilog/Array.v | 108 |
3 files changed, 139 insertions, 7 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index 675ad23..efa1323 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -52,6 +52,8 @@ Ltac clear_obvious := Ltac simplify := simpl in *; clear_obvious; simpl in *; try discriminate. +Global Opaque Nat.div. + (* Definition const (A B : Type) (a : A) (b : B) : A := a. Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *) diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 773497b..1356f08 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -43,15 +43,16 @@ Definition state_st_wf (m : HTL.module) (s : HTL.state) := Hint Unfold state_st_wf : htlproof. Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : mem) : - AssocMap.t (list value) -> Prop := + Verilog.assocmap_arr -> Prop := | match_arr : forall asa stack, - m.(HTL.mod_stk_len) = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> - asa ! (m.(HTL.mod_stk)) = Some stack -> + asa ! (m.(HTL.mod_stk)) = Some stack /\ + stack.(arr_length) = Z.to_nat (f.(RTL.fn_stacksize) / 4) /\ (forall ptr, 0 <= ptr < Z.of_nat m.(HTL.mod_stk_len) -> opt_val_value_lessdef (Mem.loadv AST.Mint32 mem (Values.Val.offset_ptr sp (Integers.Ptrofs.repr ptr))) - (nth (Z.to_nat ptr / 4) stack (ZToValue 32 0))) -> + (Option.default (NToValue 32 0) + (Option.join (array_get_error (Z.to_nat ptr / 4) stack)))) -> match_arrs m f sp mem asa. Inductive match_stacks (mem : mem) : list RTL.stackframe -> list HTL.stackframe -> Prop := @@ -130,6 +131,33 @@ Proof. Qed. Hint Resolve regs_lessdef_add_match : htlproof. +Lemma list_combine_none : + forall n l, + length l = n -> + list_combine Verilog.merge_cell (list_repeat None n) l = l. +Proof. + induction n; intros; simplify. + - symmetry. apply length_zero_iff_nil. auto. + - destruct l; simplify. + rewrite list_repeat_cons. + simplify. f_equal. + eauto. +Qed. + +Lemma combine_none : + forall n a, + a.(arr_length) = n -> + arr_contents (combine Verilog.merge_cell (arr_repeat None n) a) = arr_contents a. +Proof. + intros. + unfold combine. + simplify. + + rewrite <- (arr_wf a) in H. + apply list_combine_none. + assumption. +Qed. + (* Need to eventually move posToValue 32 to posToValueAuto, as that has this proof. *) Lemma assumption_32bit : forall v, diff --git a/src/verilog/Array.v b/src/verilog/Array.v index 16f5406..0b6e2a9 100644 --- a/src/verilog/Array.v +++ b/src/verilog/Array.v @@ -122,14 +122,15 @@ Proof. info_eauto with array. Qed. +(** Tail recursive version of standard library function. *) Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A := match n with | O => acc | S n => list_repeat' (a::acc) a n end. -Lemma list_repeat'_len : forall {A : Type} (a : A) n l, - Datatypes.length (list_repeat' l a n) = (n + Datatypes.length l)%nat. +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. @@ -139,9 +140,46 @@ Proof. lia. 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. + + pose proof IHn. + specialize (H (a :: l)). + rewrite H. clear H. + specialize (IHn (a :: nil)). + rewrite IHn. clear IHn. + remember (list_repeat' [] a n) as l0. + + rewrite <- app_assoc. + f_equal. +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. + rewrite list_repeat'_app. + + replace (a :: list_repeat' [] a n ++ [a]) with (list_repeat' [] a n ++ [a] ++ [a]). + 2: { rewrite app_comm_cons. rewrite IHn; auto. + rewrite app_assoc. reflexivity. } + rewrite app_assoc. reflexivity. +Qed. + +Lemma list_repeat'_cons {A : Type} : forall (a : A) n, + list_repeat' [a] a n = a :: list_repeat' [] a n. +Proof. + intros. + + rewrite list_repeat'_head_tail; auto. + apply list_repeat'_app. +Qed. + Definition list_repeat {A : Type} : A -> nat -> list A := list_repeat' nil. -Lemma list_repeat_len {A : Type} : forall n (a : A), Datatypes.length (list_repeat a n) = n. +Lemma list_repeat_len {A : Type} : forall n (a : A), length (list_repeat a n) = n. Proof. intros. unfold list_repeat. @@ -149,6 +187,42 @@ Proof. simplify. lia. 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. + + unfold list_repeat in *. + simplify. + + rewrite list_repeat'_app in H. + pose proof (X a a'). + destruct H0; auto. + + (* This is actually a degenerate case, not an unprovable goal. *) + pose proof (in_app_or (list_repeat' [] a n) ([a])). + apply H0 in H. invert H. + + - eapply IHn in X; eassumption. + - invert H1; contradiction. +Qed. + +Lemma list_repeat_head_tail {A : Type} : forall n (a : A), + a :: list_repeat a n = list_repeat a n ++ [a]. +Proof. + unfold list_repeat. apply list_repeat'_head_tail. +Qed. + +Lemma list_repeat_cons {A : Type} : forall n (a : A), + list_repeat a (S n) = a :: list_repeat a n. +Proof. + intros. + + unfold list_repeat. + apply list_repeat'_cons. +Qed. + Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n). Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C := @@ -157,5 +231,33 @@ Fixpoint list_combine {A B C : Type} (f : A -> B -> C) (x : list A) (y : list B) | _, _ => nil end. +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. + + destruct y; simplify; auto. +Qed. + Definition combine {A B C : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C := make_array (list_combine f x.(arr_contents) y.(arr_contents)). + +Lemma combine_length {A B C: Type} : forall x y (f : A -> B -> C), + x.(arr_length) = y.(arr_length) -> arr_length (combine f x y) = x.(arr_length). +Proof. + intros. + + unfold combine. + unfold make_array. + simplify. + + 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. +Qed. |