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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
Require Export Bool Sumbool.
Require Vector.
Export Vector.VectorNotations.
Require Import Minus.
Local Open Scope nat_scope.
(**
We build bit vectors in the spirit of List.v.
The size of the vector is a parameter which is too important
to be accessible only via function "length".
The first idea is to build a record with both the list and the length.
Unfortunately, this a posteriori verification leads to
numerous lemmas for handling lengths.
The second idea is to use a dependent type in which the length
is a building parameter. This leads to structural induction that
are slightly more complex and in some cases we will use a proof-term
as definition, since the type inference mechanism for pattern-matching
is sometimes weaker that the one implemented for elimination tactiques.
*)
Section BOOLEAN_VECTORS.
(**
A bit vector is a vector over booleans.
Notice that the LEAST significant bit comes first (little-endian representation).
We extract the least significant bit (head) and the rest of the vector (tail).
We compute bitwise operation on vector: negation, and, or, xor.
We compute size-preserving shifts: to the left (towards most significant bits,
we hence use Vshiftout) and to the right (towards least significant bits,
we use Vshiftin) by inserting a 'carry' bit (logical shift) or by repeating
the most significant bit (arithmetical shift).
NOTA BENE: all shift operations expect predecessor of size as parameter
(they only work on non-empty vectors).
*)
Definition Bvector := Vector.t bool.
Definition Bnil := @Vector.nil bool.
Definition Bcons := @Vector.cons bool.
Definition Bvect_true := Vector.const true.
Definition Bvect_false := Vector.const false.
Definition Blow := @Vector.hd bool.
Definition Bhigh := @Vector.tl bool.
Definition Bsign := @Vector.last bool.
Definition Bneg := @Vector.map _ _ negb.
Definition BVand := @Vector.map2 _ _ _ andb.
Definition BVor := @Vector.map2 _ _ _ orb.
Definition BVxor := @Vector.map2 _ _ _ xorb.
Definition BVeq m n := @Vector.eqb bool eqb m n.
Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
Bcons carry n (Vector.shiftout bv).
Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) :=
Bhigh (S n) (Vector.shiftin carry bv).
Definition BshiftRa (n:nat) (bv:Bvector (S n)) :=
Bhigh (S n) (Vector.shiftrepeat bv).
Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
match p with
| O => bv
| S p' => BshiftL n (BshiftL_iter n bv p') false
end.
Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
match p with
| O => bv
| S p' => BshiftRl n (BshiftRl_iter n bv p') false
end.
Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
match p with
| O => bv
| S p' => BshiftRa n (BshiftRa_iter n bv p')
end.
End BOOLEAN_VECTORS.
Module BvectorNotations.
Declare Scope Bvector_scope.
Delimit Scope Bvector_scope with Bvector.
Notation "^~ x" := (Bneg _ x) (at level 35, right associativity) : Bvector_scope.
Infix "^&" := (BVand _) (at level 40, left associativity) : Bvector_scope.
Infix "^⊕" := (BVxor _) (at level 45, left associativity) : Bvector_scope.
Infix "^|" := (BVor _) (at level 50, left associativity) : Bvector_scope.
Infix "=?" := (BVeq _ _) (at level 70, no associativity) : Bvector_scope.
Open Scope Bvector_scope.
End BvectorNotations.
|
