diff options
| -rw-r--r-- | default.nix | 10 | ||||
| -rw-r--r-- | shell.nix | 2 | ||||
| -rw-r--r-- | src/common/IntegerExtra.v | 9 | ||||
| -rw-r--r-- | src/common/ZExtra.v | 247 | ||||
| -rw-r--r-- | src/extraction/Extraction.v | 3 | ||||
| -rw-r--r-- | src/hls/Array.v | 6 | ||||
| -rw-r--r-- | src/hls/PrintHTL.ml | 1 | ||||
| -rw-r--r-- | src/hls/Value.v | 3 | ||||
| -rw-r--r-- | src/hls/ValueInt.v | 10 | ||||
| -rw-r--r-- | src/hls/ValueVal.v | 2 |
10 files changed, 261 insertions, 32 deletions
diff --git a/default.nix b/default.nix index 3c8bc92..7abebda 100644 --- a/default.nix +++ b/default.nix @@ -1,8 +1,8 @@ with import <nixpkgs> {}; let - ncoq = coq_8_11; - ncoqPackages = coqPackages_8_11; + ncoq = coq_8_12; + ncoqPackages = coqPackages_8_12; bbv = ncoqPackages.callPackage ( { coq, stdenv, fetchFromGitHub }: stdenv.mkDerivation { @@ -28,9 +28,9 @@ stdenv.mkDerivation { name = "vericert"; src = ./.; - buildInputs = [ ncoq ocamlPackages.menhir dune - ocaml ocamlPackages.findlib bbv - gcc ocamlPackages.utop + buildInputs = [ ncoq dune + ocaml ocamlPackages.findlib ocamlPackages.menhir ocamlPackages.utop + gcc bbv ]; enableParallelBuilding = true; @@ -1,7 +1,7 @@ with import <nixpkgs> {}; mkShell { - buildInputs = (import ./.).buildInputs ++ [ ocamlPackages.ocp-indent verilog yosys + buildInputs = (import ./.).buildInputs ++ [ ocamlPackages.ocp-indent ocamlPackages.merlin ocamlPackages.utop ]; } diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index f44cac2..185f669 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -2,7 +2,6 @@ Require Import BinInt. Require Import Lia. Require Import ZBinary. -From bbv Require Import ZLib. From compcert Require Import Integers Coqlib. Require Import Vericertlib. @@ -500,7 +499,7 @@ Module IntExtra. apply Z.pow_lt_mono_r; lia. pose proof (Zlt_neg_0 p). - pose proof (pow2_nonneg (unsigned y)). rewrite <- Heqz in H0. + pose proof (Z.pow_nonneg 2 (unsigned y)). rewrite <- Heqz in H0. lia. Qed. @@ -521,7 +520,7 @@ Module IntExtra. pose proof (unsigned_range_2 y). lia. rewrite Z.shiftl_1_l. unfold modulus, wordsize, Wordsize_32.wordsize. rewrite two_power_nat_equiv. - split. apply pow2_nonneg. + split. apply Z.pow_nonneg. lia. apply Z.pow_lt_mono_r; lia. - simplify. rewrite Z_mod_modulus_eq in Heqo. @@ -531,7 +530,7 @@ Module IntExtra. pose proof (unsigned_range_2 y). lia. rewrite Z.shiftl_1_l. unfold modulus, wordsize, Wordsize_32.wordsize. rewrite two_power_nat_equiv. - split. apply pow2_nonneg. + split. apply Z.pow_nonneg. lia. apply Z.pow_lt_mono_r; lia. Qed. @@ -584,7 +583,7 @@ Module IntExtra. { apply Z.mod_small. rewrite Z.shiftl_1_l. split. - apply pow2_nonneg. + apply Z.pow_nonneg. lia. replace 4294967296 with (2^32) by auto. apply Z.le_lt_trans with (m := 2 ^ 31); try lia. apply Z.pow_le_mono_r; lia. diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v index 519ee7c..5f9034e 100644 --- a/src/common/ZExtra.v +++ b/src/common/ZExtra.v @@ -1,8 +1,251 @@ -Require Import ZArith. -Require Import Lia. +Require Import Coq.ZArith.BinInt. +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. +Module ZLib. + +Lemma mod2_cases: forall (n: Z), n mod 2 = 0 \/ n mod 2 = 1. +Proof. + intros. pose proof (Z.mod_pos_bound n 2). lia. +Qed. + +Lemma div_mul_undo: forall a b, + b <> 0 -> + a mod b = 0 -> + a / b * b = a. +Proof. + intros. + pose proof Z.div_mul_cancel_l as A. specialize (A a 1 b). + replace (b * 1) with b in A by lia. + rewrite Z.div_1_r in A. + rewrite Z.mul_comm. + rewrite <- Z.divide_div_mul_exact; try assumption. + - apply A; congruence. + - apply Z.mod_divide; assumption. +Qed. + +Lemma mod_0_r: forall (m: Z), + m mod 0 = 0. +Proof. + intros. destruct m; reflexivity. +Qed. + +Lemma sub_mod_0: forall (a b m: Z), + a mod m = 0 -> + b mod m = 0 -> + (a - b) mod m = 0. +Proof. + intros *. intros E1 E2. + rewrite Zminus_mod. + rewrite E1. rewrite E2. + reflexivity. +Qed. + +Lemma add_mod_0: forall a b m : Z, + a mod m = 0 -> + b mod m = 0 -> + (a + b) mod m = 0. +Proof. + intros *. intros E1 E2. + rewrite Zplus_mod. + rewrite E1. rewrite E2. + reflexivity. +Qed. + +Lemma Z_mod_mult': forall a b : Z, + (a * b) mod a = 0. +Proof. + intros. rewrite Z.mul_comm. apply Z_mod_mult. +Qed. + +Lemma mod_add_r: forall a b, + b <> 0 -> + (a + b) mod b = a mod b. +Proof. + intros. rewrite <- Z.add_mod_idemp_r by lia. + rewrite Z.mod_same by lia. + rewrite Z.add_0_r. + reflexivity. +Qed. + +Lemma mod_pow2_same_cases: forall a n, + a mod 2 ^ n = a -> + 2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n. +Proof. + intros. + assert (n < 0 \/ 0 <= n) as C by lia. destruct C as [C | C]. + - left. rewrite (Z.pow_neg_r 2 n C) in *. rewrite mod_0_r in H. auto. + - right. + rewrite <- H. apply Z.mod_pos_bound. + apply Z.pow_pos_nonneg; lia. +Qed. + +Lemma mod_pow2_same_bounds: forall a n, + a mod 2 ^ n = a -> + 0 <= n -> + 0 <= a < 2 ^ n. +Proof. + intros. rewrite <- H. apply Z.mod_pos_bound. + apply Z.pow_pos_nonneg; lia. +Qed. + +Lemma pow2_nonneg: forall n, + 0 <= 2 ^ n. +Proof. + intros. apply Z.pow_nonneg. lia. +Qed. + +Lemma pow2_pos: forall n, + 0 <= n -> + 0 < 2 ^ n. +Proof. + intros. apply Z.pow_pos_nonneg; lia. +Qed. + +Lemma pow2_times2: forall i, + 0 < i -> + 2 ^ i = 2 * 2 ^ (i - 1). +Proof. + intros. + rewrite <- Z.pow_succ_r by lia. + f_equal. + lia. +Qed. + +Lemma pow2_div2: forall i, + 0 <= i -> + 2 ^ (i - 1) = 2 ^ i / 2. +Proof. + intros. + assert (i = 0 \/ 0 < i) as C by lia. destruct C as [C | C]. + - subst. reflexivity. + - rewrite Z.pow_sub_r by lia. + reflexivity. +Qed. + +Lemma div_mul_undo_le: forall a b, + 0 <= a -> + 0 < b -> + a / b * b <= a. +Proof. + intros. + pose proof (Zmod_eq_full a b) as P. + pose proof (Z.mod_bound_pos a b) as Q. + lia. +Qed. + +Lemma testbit_true_nonneg: forall a i, + 0 <= a -> + 0 <= i -> + Z.testbit a i = true -> + 2 ^ i <= a. +Proof. + intros. + apply Z.testbit_true in H1; [|assumption]. + pose proof (pow2_pos i H0). + eapply Z.le_trans; [| apply (div_mul_undo_le a (2 ^ i)); lia]. + replace (2 ^ i) with (1 * 2 ^ i) at 1 by lia. + apply Z.mul_le_mono_nonneg_r; [lia|]. + pose proof (Z.div_pos a (2 ^ i)). + assert (a / 2 ^ i <> 0); [|lia]. + intro E. rewrite E in H1. cbv in H1. discriminate H1. +Qed. + +Lemma range_div_pos: forall a b c d, + 0 < d -> + a <= b <= c -> + a / d <= b / d <= c / d. +Proof. + intuition idtac. + - apply (Z.div_le_mono _ _ _ H H1). + - apply (Z.div_le_mono _ _ _ H H2). +Qed. + +Lemma testbit_true_nonneg': forall a i, + 0 <= i -> + 2 ^ i <= a < 2 ^ (i + 1) -> + Z.testbit a i = true. +Proof. + intros. + apply Z.testbit_true; [assumption|]. + destruct H0 as [A B]. + pose proof (pow2_pos i H) as Q. + apply (Z.div_le_mono _ _ _ Q) in A. + rewrite Z_div_same in A by lia. + pose proof (Z.div_lt_upper_bound a (2 ^ i) 2 Q) as P. + rewrite Z.mul_comm in P. + replace i with (i + 1 - 1) in P by lia. + rewrite <- pow2_times2 in P by lia. + specialize (P B). + replace (i + 1 - 1) with i in P by lia. + replace (a / 2 ^ i) with 1 by lia. + reflexivity. +Qed. + +Lemma testbit_false_nonneg: forall a i, + 0 <= a < 2 ^ i -> + 0 < i -> + Z.testbit a (i - 1) = false -> + a < 2 ^ (i - 1). +Proof. + intros. + assert (2 ^ (i - 1) <= a < 2 ^ i \/ a < 2 ^ (i - 1)) as C by lia. + destruct C as [C | C]; [exfalso|assumption]. + assert (Z.testbit a (i - 1) = true); [|congruence]. + replace i with (i - 1 + 1) in C at 2 by lia. + apply testbit_true_nonneg'; lia. +Qed. + +Lemma signed_bounds_to_sz_pos: forall sz n, + - 2 ^ (sz - 1) <= n < 2 ^ (sz - 1) -> + 0 < sz. +Proof. + intros. + assert (0 < sz \/ sz - 1 < 0) as C by lia. + destruct C as [C | C]; [assumption|exfalso]. + rewrite Z.pow_neg_r in H by assumption. + lia. +Qed. + +Lemma two_digits_encoding_inj_lo: forall base a b c d: Z, + 0 <= b < base -> + 0 <= d < base -> + base * a + b = base * c + d -> + b = d. +Proof. + intros. + pose proof Z.mod_unique as P. + specialize P with (b := base) (q := c) (r := d). + specialize P with (2 := H1). + rewrite P by lia. + rewrite <- Z.add_mod_idemp_l by lia. + rewrite Z.mul_comm. + rewrite Z.mod_mul by lia. + rewrite Z.add_0_l. + rewrite Z.mod_small by lia. + reflexivity. +Qed. + +Lemma two_digits_encoding_inj_hi: forall base a b c d: Z, + 0 <= b < base -> + 0 <= d < base -> + base * a + b = base * c + d -> + a = c. +Proof. + intros. nia. +Qed. + +Lemma Z_to_nat_neg: forall (n: Z), + n < 0 -> + Z.to_nat n = 0%nat. +Proof. + intros. destruct n; (lia||reflexivity). +Qed. + +End ZLib. + Module ZExtra. Lemma mod_0_bounds : diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index c2b3951..e8cfe50 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -18,7 +18,6 @@ From vericert Require Verilog - Value Compiler RTLBlockgen RTLBlock @@ -178,7 +177,7 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction - Verilog.module Value.uvalueToZ vericert.Compiler.transf_hls + Verilog.module vericert.Compiler.transf_hls vericert.Compiler.transf_hls_temp vericert.Compiler.transf_hls_opt RTLBlockgen.transl_program RTLBlock.successors_instr diff --git a/src/hls/Array.v b/src/hls/Array.v index fe0f6b2..5eca269 100644 --- a/src/hls/Array.v +++ b/src/hls/Array.v @@ -29,7 +29,7 @@ Lemma list_set_spec1 {A : Type} : forall l i (x : A), i < length l -> nth_error (list_set i x l) i = Some x. Proof. - induction l; intros; destruct i; crush; firstorder. + induction l; intros; destruct i; crush; firstorder. intuition. 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; crush; firstorder. + induction l; intros; destruct i; crush; firstorder. intuition. Qed. Hint Resolve list_set_spec2 : array. @@ -280,7 +280,7 @@ Proof. destruct i; crush. rewrite list_repeat_cons. - destruct i; crush; firstorder. + destruct i; crush; firstorder. intuition. Qed. Definition arr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n). diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml index 44f8b01..a75d0ee 100644 --- a/src/hls/PrintHTL.ml +++ b/src/hls/PrintHTL.ml @@ -16,7 +16,6 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -open Value open Datatypes open Camlcoq open AST diff --git a/src/hls/Value.v b/src/hls/Value.v index d6a3d8b..0d3ea66 100644 --- a/src/hls/Value.v +++ b/src/hls/Value.v @@ -1,4 +1,4 @@ -(* +(*(* * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> * @@ -549,3 +549,4 @@ Proof. apply Nat2Z.inj_lt in H2. assumption. Qed. +*) diff --git a/src/hls/ValueInt.v b/src/hls/ValueInt.v index f1fd056..e434abc 100644 --- a/src/hls/ValueInt.v +++ b/src/hls/ValueInt.v @@ -17,8 +17,6 @@ *) (* begin hide *) -From bbv Require Import Word. -From bbv Require HexNotation WordScope. From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. From compcert Require Import lib.Integers common.Values. From vericert Require Import Vericertlib. @@ -98,14 +96,6 @@ Definition boolToValue (b : bool) : value := (** ** Arithmetic operations *) -Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1. -intros; subst; assumption. Defined. - -Lemma unify_word_unfold : - forall sz w, - unify_word sz sz w eq_refl = w. -Proof. auto. Qed. - Inductive val_value_lessdef: val -> value -> Prop := | val_value_lessdef_int: forall i v', diff --git a/src/hls/ValueVal.v b/src/hls/ValueVal.v index b882dc6..96e0b1c 100644 --- a/src/hls/ValueVal.v +++ b/src/hls/ValueVal.v @@ -17,8 +17,6 @@ *) (* begin hide *) -From bbv Require Import Word. -From bbv Require HexNotation WordScope. From Coq Require Import ZArith.ZArith FSets.FMapPositive Lia. From compcert Require Export lib.Integers common.Values. From vericert Require Import Vericertlib. |