Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
125
Issues
125
List
Boards
Labels
Service Desk
Milestones
Merge Requests
15
Merge Requests
15
Operations
Operations
Incidents
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
c8d03c30
Commit
c8d03c30
authored
Nov 16, 2011
by
Tuyen Nguyen
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
bitvector1/add *.v
parent
e9a542f8
Changes
25
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
25 changed files
with
11198 additions
and
480 deletions
+11198
-480
tests/bitvector1.why
tests/bitvector1.why
+1
-1
tests/bitvector1/bitvector1_BitVector_lsr_to_nat_sub_1.v
tests/bitvector1/bitvector1_BitVector_lsr_to_nat_sub_1.v
+211
-0
tests/bitvector1/bitvector1_BitVector_lsr_to_nat_sub_2.v
tests/bitvector1/bitvector1_BitVector_lsr_to_nat_sub_2.v
+287
-0
tests/bitvector1/bitvector1_BitVector_nth_from_int_0_1.v
tests/bitvector1/bitvector1_BitVector_nth_from_int_0_1.v
+332
-0
tests/bitvector1/bitvector1_BitVector_nth_from_int_0_2.v
tests/bitvector1/bitvector1_BitVector_nth_from_int_0_2.v
+343
-0
tests/bitvector1/bitvector1_BitVector_pow2i_1.v
tests/bitvector1/bitvector1_BitVector_pow2i_1.v
+329
-0
tests/bitvector1/bitvector1_BitVector_to_nat_of_one_1.v
tests/bitvector1/bitvector1_BitVector_to_nat_of_one_1.v
+279
-0
tests/bitvector1/bitvector1_BitVector_to_nat_of_one_2.v
tests/bitvector1/bitvector1_BitVector_to_nat_of_one_2.v
+309
-0
tests/bitvector1/bitvector1_BitVector_to_nat_of_zero2_1.v
tests/bitvector1/bitvector1_BitVector_to_nat_of_zero2_1.v
+271
-0
tests/bitvector1/bitvector1_BitVector_to_nat_sub_low_true_1.v
...s/bitvector1/bitvector1_BitVector_to_nat_sub_low_true_1.v
+191
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_const_value0_2.v
tests/bitvector1/bitvector1_TestDoubleOfInt_const_value0_2.v
+568
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_const_value0_3.v
tests/bitvector1/bitvector1_TestDoubleOfInt_const_value0_3.v
+579
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_const_value_2.v
tests/bitvector1/bitvector1_TestDoubleOfInt_const_value_2.v
+573
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_const_value_3.v
tests/bitvector1/bitvector1_TestDoubleOfInt_const_value_3.v
+573
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_exp_var_1.v
tests/bitvector1/bitvector1_TestDoubleOfInt_exp_var_1.v
+597
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value0_1.v
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value0_1.v
+614
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value0_2.v
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value0_2.v
+624
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_1.v
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_1.v
+627
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_2.v
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_2.v
+617
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_3.v
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_3.v
+628
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_4.v
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_4.v
+622
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_5.v
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_5.v
+622
-0
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_6.v
tests/bitvector1/bitvector1_TestDoubleOfInt_var_value_6.v
+628
-0
tests/bitvector1/bitvector1_TestNegAsXOR_to_nat_sub_jqt_1.v
tests/bitvector1/bitvector1_TestNegAsXOR_to_nat_sub_jqt_1.v
+316
-0
tests/bitvector1/why3session.xml
tests/bitvector1/why3session.xml
+457
-479
No files found.
tests/bitvector1.why
View file @
c8d03c30
...
...
@@ -299,7 +299,7 @@ theory BitVector
to_nat_sub b j i = 0
lemma to_nat_of_one:
forall b:bv, i j:int.
forall b:bv, i j:int.
i >= j >=0 ->
(forall k:int. j >= k >= i -> nth b k = True) ->
to_nat_sub b j i = pow2 (j-i+1) - 1
...
...
tests/bitvector1/bitvector1_BitVector_lsr_to_nat_sub_1.v
0 → 100644
View file @
c8d03c30
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
ZArith
.
Require
Import
Rbase
.
Parameter
pow_of2
:
Z
->
Z
.
Axiom
pow_of2_value
:
((
pow_of2
0
%
Z
)
=
1
%
Z
)
/
\
(((
pow_of2
1
%
Z
)
=
2
%
Z
)
/
\
(((
pow_of2
2
%
Z
)
=
4
%
Z
)
/
\
(((
pow_of2
3
%
Z
)
=
8
%
Z
)
/
\
(((
pow_of2
4
%
Z
)
=
16
%
Z
)
/
\
(((
pow_of2
5
%
Z
)
=
32
%
Z
)
/
\
(((
pow_of2
6
%
Z
)
=
64
%
Z
)
/
\
(((
pow_of2
7
%
Z
)
=
128
%
Z
)
/
\
(((
pow_of2
8
%
Z
)
=
256
%
Z
)
/
\
(((
pow_of2
9
%
Z
)
=
512
%
Z
)
/
\
(((
pow_of2
10
%
Z
)
=
1024
%
Z
)
/
\
(((
pow_of2
11
%
Z
)
=
2048
%
Z
)
/
\
(((
pow_of2
12
%
Z
)
=
4096
%
Z
)
/
\
(((
pow_of2
13
%
Z
)
=
8192
%
Z
)
/
\
(((
pow_of2
14
%
Z
)
=
16384
%
Z
)
/
\
(((
pow_of2
15
%
Z
)
=
32768
%
Z
)
/
\
(((
pow_of2
16
%
Z
)
=
65536
%
Z
)
/
\
(((
pow_of2
17
%
Z
)
=
131072
%
Z
)
/
\
(((
pow_of2
18
%
Z
)
=
262144
%
Z
)
/
\
(((
pow_of2
19
%
Z
)
=
524288
%
Z
)
/
\
(((
pow_of2
20
%
Z
)
=
1048576
%
Z
)
/
\
(((
pow_of2
21
%
Z
)
=
2097152
%
Z
)
/
\
(((
pow_of2
22
%
Z
)
=
4194304
%
Z
)
/
\
(((
pow_of2
23
%
Z
)
=
8388608
%
Z
)
/
\
(((
pow_of2
24
%
Z
)
=
16777216
%
Z
)
/
\
(((
pow_of2
25
%
Z
)
=
33554432
%
Z
)
/
\
(((
pow_of2
26
%
Z
)
=
67108864
%
Z
)
/
\
(((
pow_of2
27
%
Z
)
=
134217728
%
Z
)
/
\
(((
pow_of2
28
%
Z
)
=
268435456
%
Z
)
/
\
(((
pow_of2
29
%
Z
)
=
536870912
%
Z
)
/
\
(((
pow_of2
30
%
Z
)
=
1073741824
%
Z
)
/
\
(((
pow_of2
31
%
Z
)
=
2147483648
%
Z
)
/
\
(((
pow_of2
32
%
Z
)
=
4294967296
%
Z
)
/
\
(((
pow_of2
33
%
Z
)
=
8589934592
%
Z
)
/
\
(((
pow_of2
34
%
Z
)
=
17179869184
%
Z
)
/
\
(((
pow_of2
35
%
Z
)
=
34359738368
%
Z
)
/
\
(((
pow_of2
36
%
Z
)
=
68719476736
%
Z
)
/
\
(((
pow_of2
37
%
Z
)
=
137438953472
%
Z
)
/
\
(((
pow_of2
38
%
Z
)
=
274877906944
%
Z
)
/
\
(((
pow_of2
39
%
Z
)
=
549755813888
%
Z
)
/
\
(((
pow_of2
40
%
Z
)
=
1099511627776
%
Z
)
/
\
(((
pow_of2
41
%
Z
)
=
2199023255552
%
Z
)
/
\
(((
pow_of2
42
%
Z
)
=
4398046511104
%
Z
)
/
\
(((
pow_of2
43
%
Z
)
=
8796093022208
%
Z
)
/
\
(((
pow_of2
44
%
Z
)
=
17592186044416
%
Z
)
/
\
(((
pow_of2
45
%
Z
)
=
35184372088832
%
Z
)
/
\
(((
pow_of2
46
%
Z
)
=
70368744177664
%
Z
)
/
\
(((
pow_of2
47
%
Z
)
=
140737488355328
%
Z
)
/
\
(((
pow_of2
48
%
Z
)
=
281474976710656
%
Z
)
/
\
(((
pow_of2
49
%
Z
)
=
562949953421312
%
Z
)
/
\
(((
pow_of2
50
%
Z
)
=
1125899906842624
%
Z
)
/
\
(((
pow_of2
51
%
Z
)
=
2251799813685248
%
Z
)
/
\
(((
pow_of2
52
%
Z
)
=
4503599627370496
%
Z
)
/
\
(((
pow_of2
53
%
Z
)
=
9007199254740992
%
Z
)
/
\
(((
pow_of2
54
%
Z
)
=
18014398509481984
%
Z
)
/
\
(((
pow_of2
55
%
Z
)
=
36028797018963968
%
Z
)
/
\
(((
pow_of2
56
%
Z
)
=
72057594037927936
%
Z
)
/
\
(((
pow_of2
57
%
Z
)
=
144115188075855872
%
Z
)
/
\
(((
pow_of2
58
%
Z
)
=
288230376151711744
%
Z
)
/
\
(((
pow_of2
59
%
Z
)
=
576460752303423488
%
Z
)
/
\
(((
pow_of2
60
%
Z
)
=
1152921504606846976
%
Z
)
/
\
(((
pow_of2
61
%
Z
)
=
2305843009213693952
%
Z
)
/
\
(((
pow_of2
62
%
Z
)
=
4611686018427387904
%
Z
)
/
\
((
pow_of2
63
%
Z
)
=
9223372036854775808
%
Z
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
Parameter
size
:
Z
.
Parameter
bv
:
Type
.
Parameter
nth
:
bv
->
Z
->
bool
.
Parameter
bvzero
:
bv
.
Axiom
Nth_zero
:
forall
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
bvzero
n
)
=
false
).
Parameter
bvone
:
bv
.
Axiom
Nth_one
:
forall
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
bvone
n
)
=
true
).
Definition
eq
(
v1
:
bv
)
(
v2
:
bv
)
:
Prop
:=
forall
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
v1
n
)
=
(
nth
v2
n
)).
Axiom
extensionality
:
forall
(
v1
:
bv
)
(
v2
:
bv
),
(
eq
v1
v2
)
->
(
v1
=
v2
).
Parameter
bw_and
:
bv
->
bv
->
bv
.
Axiom
Nth_bw_and
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
(
bw_and
v1
v2
)
n
)
=
(
andb
(
nth
v1
n
)
(
nth
v2
n
))).
Parameter
bw_or
:
bv
->
bv
->
bv
.
Axiom
Nth_bw_or
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
(
bw_or
v1
v2
)
n
)
=
(
orb
(
nth
v1
n
)
(
nth
v2
n
))).
Parameter
bw_xor
:
bv
->
bv
->
bv
.
Axiom
Nth_bw_xor
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
xorb
(
nth
v1
n
)
(
nth
v2
n
))).
Axiom
Nth_bw_xor_v1true
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
/
\
((
nth
v1
n
)
=
true
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
negb
(
nth
v2
n
))).
Axiom
Nth_bw_xor_v1false
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
/
\
((
nth
v1
n
)
=
false
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
nth
v2
n
)).
Axiom
Nth_bw_xor_v2true
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
/
\
((
nth
v2
n
)
=
true
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
negb
(
nth
v1
n
))).
Axiom
Nth_bw_xor_v2false
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
/
\
((
nth
v2
n
)
=
false
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
nth
v1
n
)).
Parameter
bw_not
:
bv
->
bv
.
Axiom
Nth_bw_not
:
forall
(
v
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
(
bw_not
v
)
n
)
=
(
negb
(
nth
v
n
))).
Parameter
lsr
:
bv
->
Z
->
bv
.
Axiom
lsr_nth_low
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
(((
n
+
s
)
%
Z
<
size
)
%
Z
->
((
nth
(
lsr
b
s
)
n
)
=
(
nth
b
(
n
+
s
)
%
Z
)))).
Axiom
lsr_nth_high
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
((
size
<=
(
n
+
s
)
%
Z
)
%
Z
->
((
nth
(
lsr
b
s
)
n
)
=
false
))).
Parameter
asr
:
bv
->
Z
->
bv
.
Axiom
asr_nth_low
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
(((
n
+
s
)
%
Z
<
size
)
%
Z
->
((
nth
(
asr
b
s
)
n
)
=
(
nth
b
(
n
+
s
)
%
Z
)))).
Axiom
asr_nth_high
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
((
size
<=
(
n
+
s
)
%
Z
)
%
Z
->
((
nth
(
asr
b
s
)
n
)
=
(
nth
b
(
size
-
1
%
Z
)
%
Z
)))).
Parameter
lsl
:
bv
->
Z
->
bv
.
Axiom
lsl_nth_high
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
((
0
%
Z
<=
(
n
-
s
)
%
Z
)
%
Z
->
((
nth
(
lsl
b
s
)
n
)
=
(
nth
b
(
n
-
s
)
%
Z
)))).
Axiom
lsl_nth_low
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
(((
n
-
s
)
%
Z
<
0
%
Z
)
%
Z
->
((
nth
(
lsl
b
s
)
n
)
=
false
))).
Parameter
to_nat_aux
:
bv
->
Z
->
Z
.
Axiom
to_nat_aux_zero
:
forall
(
b
:
bv
)
(
i
:
Z
),
((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<
size
)
%
Z
)
->
(((
nth
b
i
)
=
false
)
->
((
to_nat_aux
b
i
)
=
(
2
%
Z
*
(
to_nat_aux
b
(
i
+
1
%
Z
)
%
Z
))
%
Z
)).
Axiom
to_nat_aux_one
:
forall
(
b
:
bv
)
(
i
:
Z
),
((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<
size
)
%
Z
)
->
(((
nth
b
i
)
=
true
)
->
((
to_nat_aux
b
i
)
=
(
1
%
Z
+
(
2
%
Z
*
(
to_nat_aux
b
(
i
+
1
%
Z
)
%
Z
))
%
Z
)
%
Z
)).
Axiom
to_nat_aux_high
:
forall
(
b
:
bv
)
(
i
:
Z
),
(
size
<=
i
)
%
Z
->
((
to_nat_aux
b
i
)
=
0
%
Z
).
Parameter
to_nat_sub
:
bv
->
Z
->
Z
->
Z
.
Axiom
to_nat_sub_zero
:
forall
(
b
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<=
j
)
%
Z
)
->
(((
nth
b
j
)
=
false
)
->
((
to_nat_sub
b
j
i
)
=
(
to_nat_sub
b
(
j
-
1
%
Z
)
%
Z
i
))).
Axiom
to_nat_sub_one
:
forall
(
b
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<=
j
)
%
Z
)
->
(((
nth
b
j
)
=
true
)
->
((
to_nat_sub
b
j
i
)
=
((
pow_of2
(
j
-
i
)
%
Z
)
+
(
to_nat_sub
b
(
j
-
1
%
Z
)
%
Z
i
))
%
Z
)).
Axiom
to_nat_sub_high
:
forall
(
b
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
(
j
<
i
)
%
Z
->
((
to_nat_sub
b
j
i
)
=
0
%
Z
).
Axiom
to_nat_sub_low_true
:
forall
(
b
:
bv
)
(
j
:
Z
),
((
nth
b
j
)
=
true
)
->
((
to_nat_sub
b
j
j
)
=
1
%
Z
).
Axiom
to_nat_sub_low_false
:
forall
(
b
:
bv
)
(
j
:
Z
),
((
nth
b
j
)
=
false
)
->
((
to_nat_sub
b
j
j
)
=
0
%
Z
).
Axiom
to_nat_of_zero
:
forall
(
b
:
bv
)
(
i
:
Z
)
(
j
:
Z
),
(
forall
(
k
:
Z
),
((
k
<=
j
)
%
Z
/
\
(
i
<=
k
)
%
Z
)
->
((
nth
b
k
)
=
false
))
->
((
to_nat_sub
b
j
i
)
=
0
%
Z
).
Axiom
to_nat_of_one
:
forall
(
b
:
bv
)
(
i
:
Z
)
(
j
:
Z
),
(
forall
(
k
:
Z
),
((
k
<=
j
)
%
Z
/
\
(
i
<=
k
)
%
Z
)
->
((
nth
b
k
)
=
true
))
->
((
to_nat_sub
b
j
i
)
=
((
pow_of2
((
j
-
i
)
%
Z
+
1
%
Z
)
%
Z
)
-
1
%
Z
)
%
Z
).
Axiom
to_nat_sub_footprint
:
forall
(
b1
:
bv
)
(
b2
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
(
forall
(
k
:
Z
),
((
i
<=
k
)
%
Z
/
\
(
k
<=
j
)
%
Z
)
->
((
nth
b1
k
)
=
(
nth
b2
k
)))
->
((
to_nat_sub
b1
j
i
)
=
(
to_nat_sub
b2
j
i
)).
(
*
YOU
MAY
EDIT
THE
CONTEXT
BELOW
*
)
(
*
DO
NOT
EDIT
BELOW
*
)
Theorem
lsr_to_nat_sub
:
forall
(
b
:
bv
)
(
s
:
Z
),
(
0
%
Z
<=
s
)
%
Z
->
((
to_nat_sub
(
lsr
b
s
)
(
size
-
1
%
Z
)
%
Z
0
%
Z
)
=
(
to_nat_sub
b
((
size
-
1
%
Z
)
%
Z
-
s
)
%
Z
0
%
Z
)).
(
*
YOU
MAY
EDIT
THE
PROOF
BELOW
*
)
intros
.
split
.
Qed
.
(
*
DO
NOT
EDIT
BELOW
*
)
tests/bitvector1/bitvector1_BitVector_lsr_to_nat_sub_2.v
0 → 100644
View file @
c8d03c30
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
ZArith
.
Require
Import
Rbase
.
Parameter
pow2
:
Z
->
Z
.
Axiom
Power_0
:
((
pow2
0
%
Z
)
=
1
%
Z
).
Axiom
Power_s
:
forall
(
n
:
Z
),
(
0
%
Z
<=
n
)
%
Z
->
((
pow2
(
n
+
1
%
Z
)
%
Z
)
=
(
2
%
Z
*
(
pow2
n
))
%
Z
).
Axiom
Power_1
:
((
pow2
1
%
Z
)
=
2
%
Z
).
Axiom
Power_sum
:
forall
(
n
:
Z
)
(
m
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
0
%
Z
<=
m
)
%
Z
)
->
((
pow2
(
n
+
m
)
%
Z
)
=
((
pow2
n
)
*
(
pow2
m
))
%
Z
).
Axiom
pow2_0
:
((
pow2
0
%
Z
)
=
1
%
Z
).
Axiom
pow2_1
:
((
pow2
1
%
Z
)
=
2
%
Z
).
Axiom
pow2_2
:
((
pow2
2
%
Z
)
=
4
%
Z
).
Axiom
pow2_3
:
((
pow2
3
%
Z
)
=
8
%
Z
).
Axiom
pow2_4
:
((
pow2
4
%
Z
)
=
16
%
Z
).
Axiom
pow2_5
:
((
pow2
5
%
Z
)
=
32
%
Z
).
Axiom
pow2_6
:
((
pow2
6
%
Z
)
=
64
%
Z
).
Axiom
pow2_7
:
((
pow2
7
%
Z
)
=
128
%
Z
).
Axiom
pow2_8
:
((
pow2
8
%
Z
)
=
256
%
Z
).
Axiom
pow2_9
:
((
pow2
9
%
Z
)
=
512
%
Z
).
Axiom
pow2_10
:
((
pow2
10
%
Z
)
=
1024
%
Z
).
Axiom
pow2_11
:
((
pow2
11
%
Z
)
=
2048
%
Z
).
Axiom
pow2_12
:
((
pow2
12
%
Z
)
=
4096
%
Z
).
Axiom
pow2_13
:
((
pow2
13
%
Z
)
=
8192
%
Z
).
Axiom
pow2_14
:
((
pow2
14
%
Z
)
=
16384
%
Z
).
Axiom
pow2_15
:
((
pow2
15
%
Z
)
=
32768
%
Z
).
Axiom
pow2_16
:
((
pow2
16
%
Z
)
=
65536
%
Z
).
Axiom
pow2_17
:
((
pow2
17
%
Z
)
=
131072
%
Z
).
Axiom
pow2_18
:
((
pow2
18
%
Z
)
=
262144
%
Z
).
Axiom
pow2_19
:
((
pow2
19
%
Z
)
=
524288
%
Z
).
Axiom
pow2_20
:
((
pow2
20
%
Z
)
=
1048576
%
Z
).
Axiom
pow2_21
:
((
pow2
21
%
Z
)
=
2097152
%
Z
).
Axiom
pow2_22
:
((
pow2
22
%
Z
)
=
4194304
%
Z
).
Axiom
pow2_23
:
((
pow2
23
%
Z
)
=
8388608
%
Z
).
Axiom
pow2_24
:
((
pow2
24
%
Z
)
=
16777216
%
Z
).
Axiom
pow2_25
:
((
pow2
25
%
Z
)
=
33554432
%
Z
).
Axiom
pow2_26
:
((
pow2
26
%
Z
)
=
67108864
%
Z
).
Axiom
pow2_27
:
((
pow2
27
%
Z
)
=
134217728
%
Z
).
Axiom
pow2_28
:
((
pow2
28
%
Z
)
=
268435456
%
Z
).
Axiom
pow2_29
:
((
pow2
29
%
Z
)
=
536870912
%
Z
).
Axiom
pow2_30
:
((
pow2
30
%
Z
)
=
1073741824
%
Z
).
Axiom
pow2_31
:
((
pow2
31
%
Z
)
=
2147483648
%
Z
).
Axiom
pow2_32
:
((
pow2
32
%
Z
)
=
4294967296
%
Z
).
Axiom
pow2_33
:
((
pow2
33
%
Z
)
=
8589934592
%
Z
).
Axiom
pow2_34
:
((
pow2
34
%
Z
)
=
17179869184
%
Z
).
Axiom
pow2_35
:
((
pow2
35
%
Z
)
=
34359738368
%
Z
).
Axiom
pow2_36
:
((
pow2
36
%
Z
)
=
68719476736
%
Z
).
Axiom
pow2_37
:
((
pow2
37
%
Z
)
=
137438953472
%
Z
).
Axiom
pow2_38
:
((
pow2
38
%
Z
)
=
274877906944
%
Z
).
Axiom
pow2_39
:
((
pow2
39
%
Z
)
=
549755813888
%
Z
).
Axiom
pow2_40
:
((
pow2
40
%
Z
)
=
1099511627776
%
Z
).
Axiom
pow2_41
:
((
pow2
41
%
Z
)
=
2199023255552
%
Z
).
Axiom
pow2_42
:
((
pow2
42
%
Z
)
=
4398046511104
%
Z
).
Axiom
pow2_43
:
((
pow2
43
%
Z
)
=
8796093022208
%
Z
).
Axiom
pow2_44
:
((
pow2
44
%
Z
)
=
17592186044416
%
Z
).
Axiom
pow2_45
:
((
pow2
45
%
Z
)
=
35184372088832
%
Z
).
Axiom
pow2_46
:
((
pow2
46
%
Z
)
=
70368744177664
%
Z
).
Axiom
pow2_47
:
((
pow2
47
%
Z
)
=
140737488355328
%
Z
).
Axiom
pow2_48
:
((
pow2
48
%
Z
)
=
281474976710656
%
Z
).
Axiom
pow2_49
:
((
pow2
49
%
Z
)
=
562949953421312
%
Z
).
Axiom
pow2_50
:
((
pow2
50
%
Z
)
=
1125899906842624
%
Z
).
Axiom
pow2_51
:
((
pow2
51
%
Z
)
=
2251799813685248
%
Z
).
Axiom
pow2_52
:
((
pow2
52
%
Z
)
=
4503599627370496
%
Z
).
Axiom
pow2_53
:
((
pow2
53
%
Z
)
=
9007199254740992
%
Z
).
Axiom
pow2_54
:
((
pow2
54
%
Z
)
=
18014398509481984
%
Z
).
Axiom
pow2_55
:
((
pow2
55
%
Z
)
=
36028797018963968
%
Z
).
Axiom
pow2_56
:
((
pow2
56
%
Z
)
=
72057594037927936
%
Z
).
Axiom
pow2_57
:
((
pow2
57
%
Z
)
=
144115188075855872
%
Z
).
Axiom
pow2_58
:
((
pow2
58
%
Z
)
=
288230376151711744
%
Z
).
Axiom
pow2_59
:
((
pow2
59
%
Z
)
=
576460752303423488
%
Z
).
Axiom
pow2_60
:
((
pow2
60
%
Z
)
=
1152921504606846976
%
Z
).
Axiom
pow2_61
:
((
pow2
61
%
Z
)
=
2305843009213693952
%
Z
).
Axiom
pow2_62
:
((
pow2
62
%
Z
)
=
4611686018427387904
%
Z
).
Axiom
pow2_63
:
((
pow2
63
%
Z
)
=
9223372036854775808
%
Z
).
Parameter
size
:
Z
.
Parameter
bv
:
Type
.
Parameter
nth
:
bv
->
Z
->
bool
.
Parameter
bvzero
:
bv
.
Axiom
Nth_zero
:
forall
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
bvzero
n
)
=
false
).
Parameter
bvone
:
bv
.
Axiom
Nth_one
:
forall
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
bvone
n
)
=
true
).
Definition
eq
(
v1
:
bv
)
(
v2
:
bv
)
:
Prop
:=
forall
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
v1
n
)
=
(
nth
v2
n
)).
Axiom
extensionality
:
forall
(
v1
:
bv
)
(
v2
:
bv
),
(
eq
v1
v2
)
->
(
v1
=
v2
).
Parameter
bw_and
:
bv
->
bv
->
bv
.
Axiom
Nth_bw_and
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
(
bw_and
v1
v2
)
n
)
=
(
andb
(
nth
v1
n
)
(
nth
v2
n
))).
Parameter
bw_or
:
bv
->
bv
->
bv
.
Axiom
Nth_bw_or
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
(
bw_or
v1
v2
)
n
)
=
(
orb
(
nth
v1
n
)
(
nth
v2
n
))).
Parameter
bw_xor
:
bv
->
bv
->
bv
.
Axiom
Nth_bw_xor
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
xorb
(
nth
v1
n
)
(
nth
v2
n
))).
Axiom
Nth_bw_xor_v1true
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
/
\
((
nth
v1
n
)
=
true
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
negb
(
nth
v2
n
))).
Axiom
Nth_bw_xor_v1false
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
/
\
((
nth
v1
n
)
=
false
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
nth
v2
n
)).
Axiom
Nth_bw_xor_v2true
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
/
\
((
nth
v2
n
)
=
true
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
negb
(
nth
v1
n
))).
Axiom
Nth_bw_xor_v2false
:
forall
(
v1
:
bv
)
(
v2
:
bv
)
(
n
:
Z
),
(((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
/
\
((
nth
v2
n
)
=
false
))
->
((
nth
(
bw_xor
v1
v2
)
n
)
=
(
nth
v1
n
)).
Parameter
bw_not
:
bv
->
bv
.
Axiom
Nth_bw_not
:
forall
(
v
:
bv
)
(
n
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
nth
(
bw_not
v
)
n
)
=
(
negb
(
nth
v
n
))).
Parameter
lsr
:
bv
->
Z
->
bv
.
Axiom
lsr_nth_low
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
(((
n
+
s
)
%
Z
<
size
)
%
Z
->
((
nth
(
lsr
b
s
)
n
)
=
(
nth
b
(
n
+
s
)
%
Z
)))).
Axiom
lsr_nth_high
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
((
size
<=
(
n
+
s
)
%
Z
)
%
Z
->
((
nth
(
lsr
b
s
)
n
)
=
false
))).
Parameter
asr
:
bv
->
Z
->
bv
.
Axiom
asr_nth_low
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
(((
n
+
s
)
%
Z
<
size
)
%
Z
->
((
nth
(
asr
b
s
)
n
)
=
(
nth
b
(
n
+
s
)
%
Z
)))).
Axiom
asr_nth_high
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
((
size
<=
(
n
+
s
)
%
Z
)
%
Z
->
((
nth
(
asr
b
s
)
n
)
=
(
nth
b
(
size
-
1
%
Z
)
%
Z
)))).
Parameter
lsl
:
bv
->
Z
->
bv
.
Axiom
lsl_nth_high
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
((
0
%
Z
<=
(
n
-
s
)
%
Z
)
%
Z
->
((
nth
(
lsl
b
s
)
n
)
=
(
nth
b
(
n
-
s
)
%
Z
)))).
Axiom
lsl_nth_low
:
forall
(
b
:
bv
)
(
n
:
Z
)
(
s
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
n
<
size
)
%
Z
)
->
((
0
%
Z
<=
s
)
%
Z
->
(((
n
-
s
)
%
Z
<
0
%
Z
)
%
Z
->
((
nth
(
lsl
b
s
)
n
)
=
false
))).
Parameter
to_nat_sub
:
bv
->
Z
->
Z
->
Z
.
Axiom
to_nat_sub_zero
:
forall
(
b
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<=
j
)
%
Z
)
->
(((
nth
b
j
)
=
false
)
->
((
to_nat_sub
b
j
i
)
=
(
to_nat_sub
b
(
j
-
1
%
Z
)
%
Z
i
))).
Axiom
to_nat_sub_one
:
forall
(
b
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
((
0
%
Z
<=
i
)
%
Z
/
\
(
i
<=
j
)
%
Z
)
->
(((
nth
b
j
)
=
true
)
->
((
to_nat_sub
b
j
i
)
=
((
pow2
(
j
-
i
)
%
Z
)
+
(
to_nat_sub
b
(
j
-
1
%
Z
)
%
Z
i
))
%
Z
)).
Axiom
to_nat_sub_high
:
forall
(
b
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
(
j
<
i
)
%
Z
->
((
to_nat_sub
b
j
i
)
=
0
%
Z
).
Axiom
to_nat_of_zero2
:
forall
(
b
:
bv
)
(
i
:
Z
)
(
j
:
Z
),
((
i
<=
j
)
%
Z
/
\
(
0
%
Z
<=
i
)
%
Z
)
->
((
forall
(
k
:
Z
),
((
k
<=
j
)
%
Z
/
\
(
i
<
k
)
%
Z
)
->
((
nth
b
k
)
=
false
))
->
((
to_nat_sub
b
j
0
%
Z
)
=
(
to_nat_sub
b
i
0
%
Z
))).
Axiom
to_nat_of_zero
:
forall
(
b
:
bv
)
(
i
:
Z
)
(
j
:
Z
),
(
i
<=
j
)
%
Z
->
((
forall
(
k
:
Z
),
((
k
<=
j
)
%
Z
/
\
(
i
<=
k
)
%
Z
)
->
((
nth
b
k
)
=
false
))
->
((
to_nat_sub
b
j
i
)
=
0
%
Z
)).
Axiom
to_nat_of_one
:
forall
(
b
:
bv
)
(
i
:
Z
)
(
j
:
Z
),
(
forall
(
k
:
Z
),
((
k
<=
j
)
%
Z
/
\
(
i
<=
k
)
%
Z
)
->
((
nth
b
k
)
=
true
))
->
((
to_nat_sub
b
j
i
)
=
((
pow2
((
j
-
i
)
%
Z
+
1
%
Z
)
%
Z
)
-
1
%
Z
)
%
Z
).
Axiom
to_nat_sub_footprint
:
forall
(
b1
:
bv
)
(
b2
:
bv
)
(
j
:
Z
)
(
i
:
Z
),
(
forall
(
k
:
Z
),
((
i
<=
k
)
%
Z
/
\
(
k
<=
j
)
%
Z
)
->
((
nth
b1
k
)
=
(
nth
b2
k
)))
->
((
to_nat_sub
b1
j
i
)
=
(
to_nat_sub
b2
j
i
)).
(
*
YOU
MAY
EDIT
THE
CONTEXT
BELOW
*
)
(
*
DO
NOT
EDIT
BELOW
*
)
Theorem
lsr_to_nat_sub
:
forall
(
b
:
bv
)
(
s
:
Z
),
(
0
%
Z
<=
s
)
%
Z
->
((
to_nat_sub
(
lsr
b
s
)
(
size
-
1
%
Z
)
%
Z
0
%
Z
)
=
(
to_nat_sub
b
((
size
-
1
%
Z
)
%
Z
-
s
)
%
Z
0
%
Z
)).
(
*
YOU
MAY
EDIT
THE
PROOF
BELOW
*
)
intuition
.
Qed
.
(
*
DO
NOT
EDIT
BELOW
*
)
tests/bitvector1/bitvector1_BitVector_nth_from_int_0_1.v
0 → 100644
View file @
c8d03c30
(
*
This
file
is
generated
by
Why3
'
s
Coq
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
ZArith
.
Require
Import
Rbase
.
Parameter
pow2
:
Z
->
Z
.
Axiom
Power_0
:
((
pow2
0
%
Z
)
=
1
%
Z
).
Axiom
Power_s
:
forall
(
n
:
Z
),
(
0
%
Z
<=
n
)
%
Z
->
((
pow2
(
n
+
1
%
Z
)
%
Z
)
=
(
2
%
Z
*
(
pow2
n
))
%
Z
).
Axiom
Power_1
:
((
pow2
1
%
Z
)
=
2
%
Z
).
Axiom
Power_sum
:
forall
(
n
:
Z
)
(
m
:
Z
),
((
0
%
Z
<=
n
)
%
Z
/
\
(
0
%
Z
<=
m
)
%
Z
)
->
((
pow2
(
n
+
m
)
%
Z
)
=
((
pow2
n
)
*
(
pow2
m
))
%
Z
).
Axiom
pow2_0
:
((
pow2
0
%
Z
)
=
1
%
Z
).
Axiom
pow2_1
:
((
pow2
1
%
Z
)
=
2
%
Z
).
Axiom
pow2_2
:
((
pow2
2
%
Z
)
=
4
%
Z
).
Axiom
pow2_3
:
((
pow2
3
%
Z
)
=
8
%
Z
).
Axiom
pow2_4
:
((
pow2
4
%
Z
)
=
16
%
Z
).
Axiom
pow2_5
:
((
pow2
5
%
Z
)
=
32
%
Z
).
Axiom
pow2_6
:
((
pow2
6
%
Z
)
=
64
%
Z
).
Axiom
pow2_7
:
((
pow2
7
%
Z
)
=
128
%
Z
).
Axiom
pow2_8
:
((
pow2
8
%
Z
)
=
256
%
Z
).
Axiom
pow2_9
:
((
pow2
9
%
Z
)
=
512
%
Z
).
Axiom
pow2_10
:
((
pow2
10
%
Z
)
=
1024
%
Z
).
Axiom
pow2_11
:
((
pow2
11
%
Z
)
=
2048
%
Z
).
Axiom
pow2_12
:
((
pow2
12
%
Z
)
=
4096
%
Z
).