-
Notifications
You must be signed in to change notification settings - Fork 7
/
Copy pathmeta.yml
166 lines (136 loc) · 4.89 KB
/
meta.yml
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
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
---
fullname: Bits
shortname: bits
organization: coq-community
community: true
action: true
coqdoc: false
doi: 10.1007/978-3-319-29604-3_2
synopsis: >-
Coq bit vector library
description: |-
A formalization of bitset operations in Coq with a corresponding
axiomatization and extraction to OCaml native integers.
publications:
- pub_url: https://hal.archives-ouvertes.fr/hal-01251943/document
pub_title: "From Sets to Bits in Coq"
pub_doi: 10.1007/978-3-319-29604-3_2
- pub_url: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/coqasm.pdf
pub_title: "Coq: The world's best macro assembler?"
pub_doi: 10.1145/2505879.2505897
authors:
- name: Andrew Kennedy
email: [email protected]
initial: true
- name: Arthur Blot
email: [email protected]
initial: true
- name: Pierre-Évariste Dagand
email: [email protected]
initial: true
maintainers:
- name: Anton Trunov
nickname: anton-trunov
opam-file-maintainer: [email protected]
opam-file-version: dev
license:
fullname: Apache License 2.0
identifier: Apache-2.0
file: LICENSE
supported_coq_versions:
text: 8.16 or later (use releases for other Coq versions)
opam: '{>= "8.16"}'
tested_coq_opam_versions:
- version: '2.0.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.0.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.16'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.2.0-coq-dev'
repo: 'mathcomp/mathcomp'
- version: 'coq-8.19'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
dependencies:
- opam:
name: ocamlbuild
description: OCamlbuild
- opam:
name: coq-mathcomp-algebra
version: '{>= "2.0"}'
description: |-
[MathComp](https://math-comp.github.io) 2.0 or later (`algebra` suffices)
- opam:
name: coq-mathcomp-algebra-tactics
description: |-
[MathComp Algebra Tactics](https://github.com/math-comp/algebra-tactics)
namespace: Bits
keywords:
- name: bit arithmetic
- name: bitset
- name: bit vector
- name: extraction
categories:
- name: Computer Science/Data Types and Data Structures
documentation: |-
## Origins
This library has been extracted from Andrew Kennedy et al. ['x86proved' fork][xprovedkennedy].
This link presently redirects to https://github.com/nbenton/x86proved repository.
The main paper for this project is [Coq: The world’s best macro assembler?][coqasm].
## Using the library
To import the main library, do:
```coq
From Bits Require Import bits.
```
An axiomatic interface supporting efficient extraction to OCaml can be
loaded with:
```coq
From Bits Require Import extraction.axioms8. (* or 16 or 32 *)
```
## Organization
This library, briefly described in the paper [From Sets to Bits in Coq][bitstosets],
helps to model operations on bitsets. It's a formalization of
logical and arithmetic operations on bit vectors. A bit vector is defined as an
SSReflect tuple of bits, i.e. a list of booleans of fixed (word) size.
The key abstractions offered by this library are as follows:
- `BITS n : Type` - vector of `n` bits
- `getBit bs k` - test the `k`-th bit of `bs` bit vector
- `andB xs ys` - bitwise "and"
- `orB xs ys` - bitwise "or"
- `xorB xs ys` - bitwise "xor"
- `invB xs` - bitwise negation
- `shrB xs k` - right shift by `k` bits
- `shlB xs k` - left shift by `k` bits
The library characterizes the interactions between these elementary operations
and provides embeddings to and from the additive group ℤ/(2ⁿ)ℤ.
The overall structure of the code is as follows:
- [src/ssrextra](src/ssrextra): complements to the [Mathcomp][mathcomp] library
- [src/spec](src/spec): specification of bit vectors
- [src/extraction](src/extraction): axiomatic interface to OCaml, for extraction
For a specific formalization developed in a file `A.v`, one will find its
associated properties in the file `A/properties.v`. For example, bit-level
operations are defined in [src/spec/operations.v](src/spec/operations.v),
therefore their properties can be found in
[src/spec/operations/properties.v](src/spec/operations/properties.v).
## Verification axioms
Axioms can be verified for 8-bit and 16-bit (using only extracted code) using
the following command:
```shell
make verify
```
For 8bit, the verification process should finish in few seconds. However
for 16-bit, depending on your computer speed, it could take more than 6
hours.
[bitstosets]: https://hal.archives-ouvertes.fr/hal-01251943/document
[coqasm]: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/12/coqasm.pdf
[xprovedkennedy]: https://x86proved.codeplex.com/SourceControl/network/forks/andrewjkennedy/x86proved/latest#src/bits.v
[mathcomp]: https://github.com/math-comp/math-comp
---