blob: 15134f50cb77cf89afe3a4dafa1b4d41ca08491a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
|
(* Copyright (C) 2022 Yann Herklotz
*
* 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.ZArith.
Require Import Coq.micromega.Lia.
Require Import Coq.micromega.Psatz.
Require Import Coq.Bool.Bool.
Require Import biteq.Lib.
#[local] Open Scope Z_scope.
Record bv := Zbv { size: N; val: Z; }.
Definition bvZ (b: bv) := (val b) mod (2 ^ (Z.of_N (size b))).
Definition bvadd (sz: N) (a b: bv) := Zbv sz (bvZ a + bvZ b).
Definition bvmult (sz: N) (a b: bv) := Zbv sz (bvZ a * bvZ b).
Lemma pow_2_div : forall p q, 0 <= p <= q -> (2 ^ p | 2 ^ q).
Proof.
intros.
exploit Z.le_exists_sub.
assert (p <= q) by lia. apply H0.
intros. inversion H0. inversion H1. rewrite H2.
rewrite Z.pow_add_r; try lia.
apply Z.divide_mul_r. apply Z.divide_refl.
Qed.
Lemma mod_mod_pow_2 :
forall a p q,
0 <= p <= q -> (a mod 2 ^ q) mod (2 ^ p) = a mod (2 ^ p).
Proof.
intros. rewrite <- Znumtheory.Zmod_div_mod; try lia. now apply pow_2_div.
Qed.
Lemma bounded_add_assoc :
forall (p q r s v u: N) (a b c: Z),
(v <= q)%N -> (v <= u)%N ->
bvZ (bvadd v (bvadd u (Zbv p a) (Zbv r b)) (Zbv s c))
= bvZ (bvadd v (Zbv p a) (bvadd q (Zbv r b) (Zbv s c))).
Proof.
intros.
unfold bvadd, bvZ; simpl in *.
rewrite Zplus_mod by eauto. rewrite mod_mod_pow_2 by lia. symmetry.
rewrite Zplus_mod by eauto.
replace (((b mod 2 ^ Z.of_N r + c mod 2 ^ Z.of_N s) mod 2 ^ Z.of_N q) mod 2 ^ Z.of_N v)
with ((b mod 2 ^ Z.of_N r + c mod 2 ^ Z.of_N s) mod 2 ^ Z.of_N v)
by (symmetry; apply mod_mod_pow_2; lia).
rewrite <- Zplus_mod. symmetry.
rewrite <- Zplus_mod. now rewrite Z.add_assoc.
Qed.
|
