diff options
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/IntegerExtra.v | 328 | ||||
| -rw-r--r-- | src/common/Maps.v | 31 | ||||
| -rw-r--r-- | src/common/Monad.v | 19 | ||||
| -rw-r--r-- | src/common/Statemonad.v | 18 | ||||
| -rw-r--r-- | src/common/Vericertlib.v | 35 | ||||
| -rw-r--r-- | src/common/ZExtra.v | 266 |
6 files changed, 666 insertions, 31 deletions
diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v index c9b5dbd..2b6cded 100644 --- a/src/common/IntegerExtra.v +++ b/src/common/IntegerExtra.v @@ -1,11 +1,30 @@ -Require Import BinInt. -Require Import Lia. -Require Import ZBinary. - -From bbv Require Import ZLib. -From compcert Require Import Integers Coqlib. - -Require Import Vericertlib. +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020-2021 Yann Herklotz <yann@yannherklotz.com> + * 2020 James Pollard <j@mes.dev> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +Require Import Coq.ZArith.BinInt. +Require Import Coq.micromega.Lia. +Require Import Coq.Numbers.Integer.Binary.ZBinary. + +Require Import compcert.lib.Coqlib. +Require Import compcert.lib.Integers. + +Require Import vericert.common.Vericertlib. Local Open Scope Z_scope. @@ -319,7 +338,7 @@ Module IntExtra. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru. change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize. - apply zlt_true. omega. omega. + apply zlt_true. lia. lia. Qed. Lemma bits_byte3: @@ -329,7 +348,7 @@ Module IntExtra. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize). - apply zlt_true. omega. omega. + apply zlt_true. lia. lia. Qed. Lemma bits_byte4: @@ -339,7 +358,7 @@ Module IntExtra. assert (zwordsize = 4 * Byte.zwordsize) by reflexivity. fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru. change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize). - apply zlt_true. omega. omega. + apply zlt_true. lia. lia. Qed. Lemma bits_ofwords: @@ -362,4 +381,291 @@ Module IntExtra. rewrite testbit_repr; auto. Abort. + Lemma div_divs_equiv : + forall x y, + signed x >= 0 -> + signed y >= 0 -> + divs x y = divu x y. + Proof. + unfold divs, divu. + intros. + rewrite !signed_eq_unsigned; + try rewrite Zquot.Zquot_Zdiv_pos; try reflexivity; + lazymatch goal with + | |- unsigned _ <= max_signed => + solve [rewrite <- signed_positive; assumption] + | |- 0 <= unsigned _ => solve [apply unsigned_range_2] + end. + Qed. + + Lemma neg_signed' : + forall x : int, + unsigned x <> 2147483648 -> + signed (neg x) = - signed x. + Proof. + intros x Hhalf. + Transparent repr. + unfold signed. + simpl. + rewrite Z_mod_modulus_eq. + replace modulus with 4294967296; auto. + replace half_modulus with 2147483648; auto. + repeat match goal with | |- context[if ?x then _ else _] => destruct x end. + - destruct (Z.eq_dec (unsigned x) 0). + + rewrite e. auto. + + pose proof (Z.mod_opp_l_nz (unsigned x) 4294967296). + assert (4294967296 <> 0) by lia. + apply H in H0. + rewrite H0 in l. + pose proof (Z.mod_small (unsigned x) 4294967296). + assert (0 <= unsigned x < 4294967296). + pose proof (unsigned_range_2 x). lia. + apply H1 in H2. rewrite H2 in l. lia. + rewrite Z.mod_small. assumption. + pose proof (unsigned_range_2 x). lia. + - destruct (Z.eq_dec (unsigned x) 0). + + lia. + + rewrite Z.mod_opp_l_nz; try lia. + rewrite Z.opp_sub_distr. + rewrite Z.mod_small. lia. + pose proof (unsigned_range_2 x). + simplify; lia. + rewrite Z.mod_small. assumption. + pose proof (unsigned_range_2 x). + simplify; lia. + - destruct (Z.eq_dec (unsigned x) 0). + + rewrite e in *. rewrite Z.opp_0 in *. rewrite Zmod_0_l in g. lia. + + rewrite Z.mod_opp_l_nz; try lia. + rewrite Z.mod_small. lia. + pose proof (unsigned_range_2 x). lia. + rewrite Z.mod_small. assumption. + pose proof (unsigned_range_2 x). lia. + - destruct (Z.eq_dec (unsigned x) 0). + + lia. + + rewrite Z.mod_opp_l_nz in g; try lia. + rewrite Z.mod_small in g. + assert (unsigned x < 2147483648) by lia. lia. + pose proof (unsigned_range_2 x). + replace max_unsigned with 4294967295 in * by auto. lia. + rewrite Z.mod_small. assumption. + pose proof (unsigned_range_2 x). + replace max_unsigned with 4294967295 in * by auto. lia. + Qed. + + Lemma neg_divs_distr_l : + forall x y, + unsigned x <> 2147483648 -> + neg (divs x y) = divs (neg x) y. + Proof. + intros x y Hhalf. unfold divs, neg. + set (x' := signed x). set (y' := signed y). + apply eqm_samerepr. + apply eqm_trans with (- (Z.quot x' y')). + auto with ints. + replace (- (Z.quot x' y')) with (Z.quot (- x') y') + by (rewrite Zquot.Zquot_opp_l; auto). + unfold x'. + rewrite <- neg_signed'. + auto with ints. + assumption. + Qed. + + Lemma neg_signed : + forall x : int, + unsigned x <> 2147483648 -> + signed x < 0 -> + signed (neg x) >= 0. + Proof. + intros. + rewrite neg_signed'. lia. + assumption. + Qed. + + Lemma shl_signed_positive : + forall y, + unsigned y <= 30 -> + signed (shl one y) >= 0. + Proof. + intros. + unfold signed, shl. + destruct (zlt (unsigned (repr (Z.shiftl (unsigned one) (unsigned y)))) half_modulus). + - rewrite unsigned_repr. + + rewrite Z.shiftl_1_l. + apply Z.le_ge. apply Z.pow_nonneg. lia. + + rewrite Z.shiftl_1_l. split. + apply Z.pow_nonneg. lia. + simplify. + replace (4294967295) with (2 ^ 32 - 1); try lia. + transitivity (2 ^ 31); try lia. + apply Z.pow_le_mono_r; lia. + - simplify. rewrite Z.shiftl_1_l in g. + unfold half_modulus, modulus, wordsize, + Wordsize_32.wordsize in *. unfold two_power_nat in *. simplify. + unfold Z_mod_modulus in *. + destruct (2 ^ unsigned y) eqn:?. + apply Z.ge_le in g. exfalso. + replace (4294967296 / 2) with (2147483648) in g; auto. + rewrite Z.shiftl_1_l. rewrite Heqz. + unfold wordsize in *. unfold Wordsize_32.wordsize in *. + rewrite Zbits.P_mod_two_p_eq in *. + replace (4294967296 / 2) with (2147483648) in g; auto. + rewrite <- Heqz in g. + rewrite Z.mod_small in g. + replace (2147483648) with (2 ^ 31) in g. + pose proof (Z.pow_le_mono_r 2 (unsigned y) 30). + apply Z.ge_le in g. + assert (0 < 2) by lia. apply H0 in H1. lia. assumption. lia. + split. lia. rewrite two_power_nat_equiv. + apply Z.pow_lt_mono_r; lia. + + pose proof (Zlt_neg_0 p). + pose proof (Z.pow_nonneg 2 (unsigned y)). rewrite <- Heqz in H0. + lia. + Qed. + + Lemma is_power2_shl : + forall y, + unsigned y <= 30 -> + is_power2 (shl one y) = Some y. + Proof. + intros. + unfold is_power2, shl. + destruct (Zbits.Z_is_power2 (unsigned (repr (Z.shiftl (unsigned one) (unsigned y))))) eqn:?. + - simplify. + rewrite Z_mod_modulus_eq in Heqo. + rewrite Z.mod_small in Heqo. rewrite Z.shiftl_1_l in Heqo. + rewrite <- two_p_correct in Heqo. + rewrite Zbits.Z_is_power2_complete in Heqo. inv Heqo. + rewrite repr_unsigned. auto. + 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 Z.pow_nonneg. lia. + apply Z.pow_lt_mono_r; lia. + - simplify. + rewrite Z_mod_modulus_eq in Heqo. + rewrite Z.mod_small in Heqo. rewrite Z.shiftl_1_l in Heqo. + rewrite <- two_p_correct in Heqo. + rewrite Zbits.Z_is_power2_complete in Heqo. discriminate. + 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 Z.pow_nonneg. lia. + apply Z.pow_lt_mono_r; lia. + Qed. + + Definition shrx_alt (x y : int) : int := + if zlt (signed x) 0 + then neg (shru (neg x) y) + else shru x y. + + Lemma shrx_shrx_alt_equiv_ne : + forall x y, + unsigned x <> 2147483648 -> + unsigned y <= 30 -> + shrx x y = shrx_alt x y. + Proof. + intros x y Hhalf H. + unfold shrx, shrx_alt, lt. + destruct (Z_ge_lt_dec (signed x) 0); + [rewrite zlt_false | rewrite zlt_true]; + + repeat lazymatch goal with + | |- is_power2 _ = Some _ => apply is_power2_shl + | |- signed (shl one _) >= 0 => apply shl_signed_positive + | |- signed (neg _) >= 0 => apply neg_signed + | |- divs _ _ = divu _ _ => apply div_divs_equiv + | |- divs ?x (shl one ?y) = neg (shru (neg ?x) ?y) => + rewrite <- neg_involutive at 1; rewrite neg_divs_distr_l; + try assumption; f_equal + | |- divs ?x (shl one ?y) = shru ?x ?y => + let H := fresh "H" in + pose proof (divu_pow2 x (shl one y) y) as H; + rewrite <- H + end; try assumption. + Qed. + + Lemma shrx_shrx_alt_equiv_eq : + forall x y, + unsigned x = 2147483648 -> + unsigned y <= 30 -> + shrx x y = shrx_alt x y. + Proof. + intros. + repeat unfold shrx, shrx_alt, signed, divs, neg. + replace half_modulus with 2147483648 by auto. + replace modulus with 4294967296 by auto. + simplify. + rewrite !Z_mod_modulus_eq. + rewrite !H. + simplify. + assert (Hshl: Z.shiftl 1 (unsigned y) mod 4294967296 = Z.shiftl 1 (unsigned y)). + { apply Z.mod_small. + rewrite Z.shiftl_1_l. + split. + 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. + } + rewrite !Hshl. + f_equal. + assert ((Z.shiftl 1 (unsigned y)) < 2147483648). + rewrite Z.shiftl_1_l. + replace 2147483648 with (2^31) by auto. + apply Z.le_lt_trans with (m := 2 ^ 30); try lia. + apply Z.pow_le_mono_r; lia. + destruct (zlt (Z.shiftl 1 (unsigned y)) 2147483648); try lia. + replace (-2147483648 mod 4294967296) with 2147483648 by auto. + assert (Hmodeq : Z.shiftr 2147483648 (unsigned y) mod 4294967296 + = Z.shiftr 2147483648 (unsigned y)). + { apply Z.mod_small. split. + apply Z.shiftr_nonneg. lia. + rewrite Z.shiftr_div_pow2. + replace 4294967296 with (Z.succ 4294967295); auto. + apply Zle_lt_succ. + replace 4294967295 with (4294967295 * (2 ^ unsigned y) / (2 ^ unsigned y)). + 2: { + apply Z.div_mul. + pose proof (Z.pow_pos_nonneg 2 (unsigned y)). + apply not_eq_sym. + apply Z.le_neq. apply H2; try lia. + apply unsigned_range_2. + } + + apply Z.div_le_mono. + apply Z.pow_pos_nonneg. lia. + apply unsigned_range_2. + transitivity 4294967295; try lia. + apply Z.le_mul_diag_r; try lia. + replace 1 with (Z.succ 0) by auto. + apply Z.le_succ_l. + apply Z.pow_pos_nonneg; try lia. + apply unsigned_range_2. apply unsigned_range_2. + } + rewrite !Hmodeq. + replace (-2147483648) with (Z.opp 2147483648) by auto. + rewrite Zquot.Zquot_opp_l. + f_equal. + rewrite Zquot.Zquot_Zdiv_pos. + rewrite Z.shiftr_div_pow2. + rewrite Z.shiftl_1_l. auto. + apply unsigned_range_2. + lia. + rewrite Z.shiftl_1_l. + apply Z.lt_le_incl. + apply Z.pow_pos_nonneg; try lia. + apply unsigned_range_2. + Qed. + + Theorem shrx_shrx_alt_equiv : + forall x y, + unsigned y <= 30 -> + shrx x y = shrx_alt x y. + Proof. + intros. + destruct (Z.eq_dec (unsigned x) 2147483648); + [ apply shrx_shrx_alt_equiv_eq | apply shrx_shrx_alt_equiv_ne]; auto. + Qed. + End IntExtra. diff --git a/src/common/Maps.v b/src/common/Maps.v index 7a45259..2db5114 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -1,11 +1,32 @@ -From vericert Require Import Vericertlib. - -From compcert Require Export Maps. -From compcert Require Import Errors. -Import PTree. +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * 2020 James Pollard <j@mes.dev> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) Set Implicit Arguments. +Require Export compcert.lib.Maps. + +Require Import compcert.common.Errors. + +Require Import vericert.common.Vericertlib. + +Import PTree. + Local Open Scope error_monad_scope. (** Instance of traverse for [PTree] and [Errors]. This should maybe be generalised diff --git a/src/common/Monad.v b/src/common/Monad.v index c42f4a3..68233b1 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -1,3 +1,22 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * 2021 Michalis Pardalos <mpardalos@gmail.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + From Coq Require Import BinNums Lists.List. From compcert Require Import Maps. diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v index 2eada2f..16dcbbf 100644 --- a/src/common/Statemonad.v +++ b/src/common/Statemonad.v @@ -1,3 +1,21 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + From compcert Require Errors. From vericert Require Import Monad. From Coq Require Import Lists.List. diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index 8b56c7d..a0d2af1 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -1,6 +1,7 @@ (* * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * Copyright (C) 2019-2021 Yann Herklotz <yann@yannherklotz.com> + * 2020 James Pollard <j@mes.dev> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -16,21 +17,23 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From Coq Require Export - String - ZArith - Znumtheory - List - Bool. +Set Implicit Arguments. -Require Import Lia. +Require Export Coq.Bool.Bool. +Require Export Coq.Lists.List. +Require Export Coq.Strings.String. +Require Export Coq.ZArith.ZArith. +Require Export Coq.ZArith.Znumtheory. +Require Import Coq.micromega.Lia. -From vericert Require Import Show. +Require Export compcert.lib.Coqlib. +Require Import compcert.lib.Integers. + +Require Export vericert.common.VericertTactics. +Require Import vericert.common.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 Import Integers. Local Open Scope Z_scope. @@ -70,7 +73,12 @@ 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. + match goal with + | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:? + | [ H: context[match ?x with | _ => _ end] |- _ ] => destruct x eqn:? + end. + +Ltac auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try congruence. Ltac nicify_hypotheses := repeat match goal with @@ -180,7 +188,8 @@ Ltac liapp := | _ => idtac end. -Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption. +Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; + try assumption; try (solve [auto]). Global Opaque Nat.div. Global Opaque Z.mul. diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v index 519ee7c..62ca54d 100644 --- a/src/common/ZExtra.v +++ b/src/common/ZExtra.v @@ -1,8 +1,270 @@ -Require Import ZArith. -Require Import Lia. +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * 2020 James Pollard <j@mes.dev> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +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 : |