Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
46fab9d2
Commit
46fab9d2
authored
May 24, 2018
by
Jean-Christophe Filliâtre
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
bitvectors: removed more Coq proofs
parent
46afb5a9
Changes
14
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
14 changed files
with
2382 additions
and
4612 deletions
+2382
-4612
examples/bitvectors/bitvector/bitvector_BitVector_nth_from_int2c_plus_pow2_1.v
...itvector/bitvector_BitVector_nth_from_int2c_plus_pow2_1.v
+0
-369
examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_zero2_1.v
...vectors/bitvector/bitvector_BitVector_to_nat_of_zero2_1.v
+0
-304
examples/bitvectors/bitvector/why3session.xml
examples/bitvectors/bitvector/why3session.xml
+18
-8
examples/bitvectors/bitvector/why3shapes.gz
examples/bitvectors/bitvector/why3shapes.gz
+0
-0
examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_exp_const_1.v
...ors/double_of_int/double_of_int_DoubleOfInt_exp_const_1.v
+432
-292
examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v
...t/double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v
+457
-339
examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v
...t/double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v
+450
-335
examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_lemma1_neg_1.v
...rs/double_of_int/double_of_int_DoubleOfInt_lemma1_neg_1.v
+0
-717
examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_lemma1_pos_1.v
...rs/double_of_int/double_of_int_DoubleOfInt_lemma1_pos_1.v
+0
-742
examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_lemma2_1.v
...ectors/double_of_int/double_of_int_DoubleOfInt_lemma2_1.v
+483
-355
examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v
...of_int/double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v
+0
-776
examples/bitvectors/double_of_int/double_of_int_DoubleOfInt_var_value0_1.v
...rs/double_of_int/double_of_int_DoubleOfInt_var_value0_1.v
+502
-368
examples/bitvectors/double_of_int/why3session.xml
examples/bitvectors/double_of_int/why3session.xml
+40
-7
examples/bitvectors/double_of_int/why3shapes.gz
examples/bitvectors/double_of_int/why3shapes.gz
+0
-0
No files found.
examples/bitvectors/bitvector/bitvector_BitVector_nth_from_int2c_plus_pow2_1.v
deleted
100644 → 0
View file @
46afb5a9
(
*
This
file
is
generated
by
Why3
'
s
Coq
8.4
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
bool
.
Bool
.
Require
int
.
Int
.
Require
int
.
Abs
.
Require
int
.
EuclideanDivision
.
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
pow2pos
:
forall
(
i
:
Z
),
(
0
%
Z
<=
i
)
%
Z
->
(
0
%
Z
<
(
pow2
i
))
%
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
).
Axiom
Div_double
:
forall
(
x
:
Z
)
(
y
:
Z
),
(((
0
%
Z
<
y
)
%
Z
/
\
(
y
<=
x
)
%
Z
)
/
\
(
x
<
(
2
%
Z
*
y
)
%
Z
)
%
Z
)
->
((
int
.
EuclideanDivision
.
div
x
y
)
=
1
%
Z
).
Axiom
Div_pow
:
forall
(
x
:
Z
)
(
i
:
Z
),
(
0
%
Z
<
i
)
%
Z
->
((((
pow2
(
i
-
1
%
Z
)
%
Z
)
<=
x
)
%
Z
/
\
(
x
<
(
pow2
i
))
%
Z
)
->
((
int
.
EuclideanDivision
.
div
x
(
pow2
(
i
-
1
%
Z
)
%
Z
))
=
1
%
Z
)).
Axiom
Div_double_neg
:
forall
(
x
:
Z
)
(
y
:
Z
),
(((((
-
2
%
Z
)
%
Z
*
y
)
%
Z
<=
x
)
%
Z
/
\
(
x
<
(
-
y
)
%
Z
)
%
Z
)
/
\
((
-
y
)
%
Z
<
0
%
Z
)
%
Z
)
->
((
int
.
EuclideanDivision
.
div
x
y
)
=
(
-
2
%
Z
)
%
Z
).
Axiom
Div_pow2
:
forall
(
x
:
Z
)
(
i
:
Z
),
(
0
%
Z
<
i
)
%
Z
->
((((
-
(
pow2
i
))
%
Z
<=
x
)
%
Z
/
\
(
x
<
(
-
(
pow2
(
i
-
1
%
Z
)
%
Z
))
%
Z
)
%
Z
)
->
((
int
.
EuclideanDivision
.
div
x
(
pow2
(
i
-
1
%
Z
)
%
Z
))
=
(
-
2
%
Z
)
%
Z
)).
Axiom
Mod_pow2_gen
:
forall
(
x
:
Z
)
(
i
:
Z
)
(
k
:
Z
),
(
0
%
Z
<=
x
)
%
Z
->
(((
0
%
Z
<=
k
)
%
Z
/
\
(
k
<
i
)
%
Z
)
->
((
int
.
EuclideanDivision
.
mod1
(
int
.
EuclideanDivision
.
div
(
x
+
(
pow2
i
))
%
Z
(
pow2
k
))
2
%
Z
)
=
(
int
.
EuclideanDivision
.
mod1
(
int
.
EuclideanDivision
.
div
x
(
pow2
k
))
2
%
Z
))).
Parameter
size
:
Z
.
Axiom
size_positive
:
(
1
%
Z
<
size
)
%
Z
.
Axiom
bv
:
Type
.
Parameter
bv_WhyType
:
WhyType
bv
.
Existing
Instance
bv_WhyType
.
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
).
(
*
Why3
assumption
*
)
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
/
\
(
s
<
size
)
%
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
/
\
(
s
<
size
)
%
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
)
/
\
(
j
<
size
)
%
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
)
/
\
(
j
<
size
)
%
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
),
(((
j
<
size
)
%
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
),
((
j
<
size
)
%
Z
/
\
(
0
%
Z
<=
i
)
%
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
),
(((
j
<
size
)
%
Z
/
\
(
i
<=
j
)
%
Z
)
/
\
(
0
%
Z
<=
i
)
%
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
),
((
j
<
size
)
%
Z
/
\
(
0
%
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
))).
Parameter
from_int
:
Z
->
bv
.
Axiom
nth_from_int_high_even
:
forall
(
n
:
Z
)
(
i
:
Z
),
(((
i
<
size
)
%
Z
/
\
(
0
%
Z
<=
i
)
%
Z
)
/
\
((
int
.
EuclideanDivision
.
mod1
(
int
.
EuclideanDivision
.
div
n
(
pow2
i
))
2
%
Z
)
=
0
%
Z
))
->
((
nth
(
from_int
n
)
i
)
=
false
).
Axiom
nth_from_int_high_odd
:
forall
(
n
:
Z
)
(
i
:
Z
),
(((
i
<
size
)
%
Z
/
\
(
0
%
Z
<=
i
)
%
Z
)
/
\
~
((
int
.
EuclideanDivision
.
mod1
(
int
.
EuclideanDivision
.
div
n
(
pow2
i
))
2
%
Z
)
=
0
%
Z
))
->
((
nth
(
from_int
n
)
i
)
=
true
).
Axiom
nth_from_int_low_even
:
forall
(
n
:
Z
),
((
int
.
EuclideanDivision
.
mod1
n
2
%
Z
)
=
0
%
Z
)
->
((
nth
(
from_int
n
)
0
%
Z
)
=
false
).
Axiom
nth_from_int_low_odd
:
forall
(
n
:
Z
),
(
~
((
int
.
EuclideanDivision
.
mod1
n
2
%
Z
)
=
0
%
Z
))
->
((
nth
(
from_int
n
)
0
%
Z
)
=
true
).
Axiom
nth_from_int_0
:
forall
(
i
:
Z
),
((
i
<
size
)
%
Z
/
\
(
0
%
Z
<=
i
)
%
Z
)
->
((
nth
(
from_int
0
%
Z
)
i
)
=
false
).
Parameter
from_int2c
:
Z
->
bv
.
Axiom
nth_sign_positive
:
forall
(
n
:
Z
),
(
0
%
Z
<=
n
)
%
Z
->
((
nth
(
from_int2c
n
)
(
size
-
1
%
Z
)
%
Z
)
=
false
).
Axiom
nth_sign_negative
:
forall
(
n
:
Z
),
(
n
<
0
%
Z
)
%
Z
->
((
nth
(
from_int2c
n
)
(
size
-
1
%
Z
)
%
Z
)
=
true
).
Axiom
nth_from_int2c_high_even
:
forall
(
n
:
Z
)
(
i
:
Z
),
(((
i
<
(
size
-
1
%
Z
)
%
Z
)
%
Z
/
\
(
0
%
Z
<=
i
)
%
Z
)
/
\
((
int
.
EuclideanDivision
.
mod1
(
int
.
EuclideanDivision
.
div
n
(
pow2
i
))
2
%
Z
)
=
0
%
Z
))
->
((
nth
(
from_int2c
n
)
i
)
=
false
).
Axiom
nth_from_int2c_high_odd
:
forall
(
n
:
Z
)
(
i
:
Z
),
(((
i
<
(
size
-
1
%
Z
)
%
Z
)
%
Z
/
\
(
0
%
Z
<=
i
)
%
Z
)
/
\
~
((
int
.
EuclideanDivision
.
mod1
(
int
.
EuclideanDivision
.
div
n
(
pow2
i
))
2
%
Z
)
=
0
%
Z
))
->
((
nth
(
from_int2c
n
)
i
)
=
true
).
Axiom
nth_from_int2c_low_even
:
forall
(
n
:
Z
),
((
int
.
EuclideanDivision
.
mod1
n
2
%
Z
)
=
0
%
Z
)
->
((
nth
(
from_int2c
n
)
0
%
Z
)
=
false
).
Axiom
nth_from_int2c_low_odd
:
forall
(
n
:
Z
),
(
~
((
int
.
EuclideanDivision
.
mod1
n
2
%
Z
)
=
0
%
Z
))
->
((
nth
(
from_int2c
n
)
0
%
Z
)
=
true
).
Axiom
nth_from_int2c_0
:
forall
(
i
:
Z
),
((
i
<
size
)
%
Z
/
\
(
0
%
Z
<=
i
)
%
Z
)
->
((
nth
(
from_int2c
0
%
Z
)
i
)
=
false
).
Open
Scope
Z_scope
.
Require
Import
Why3
.
Ltac
ae
:=
why3
"alt-ergo"
timelimit
3.
(
*
Why3
goal
*
)
Theorem
nth_from_int2c_plus_pow2
:
forall
(
x
:
Z
)
(
k
:
Z
)
(
i
:
Z
),
(((
0
%
Z
<=
k
)
%
Z
/
\
(
k
<
i
)
%
Z
)
/
\
(
k
<
(
size
-
1
%
Z
)
%
Z
)
%
Z
)
->
((
nth
(
from_int2c
(
x
+
(
pow2
i
))
%
Z
)
k
)
=
(
nth
(
from_int2c
x
)
k
)).
(
*
intros
x
k
i
((
h1
,
h2
),
h3
).
*
)
intros
x
k
i
(
h1
&
h2
).
assert
(
h
:
int
.
EuclideanDivision
.
mod1
(
int
.
EuclideanDivision
.
div
x
(
pow2
k
))
2
=
0
\
/
int
.
EuclideanDivision
.
mod1
(
int
.
EuclideanDivision
.
div
x
(
pow2
k
))
2
<>
0
)
by
omega
.
destruct
h
.
rewrite
nth_from_int2c_high_even
;
intuition
.
rewrite
nth_from_int2c_high_even
;
intuition
.
rewrite
Mod_pow2_gen
;
auto
.
rewrite
nth_from_int2c_high_odd
.
rewrite
nth_from_int2c_high_odd
;
intuition
.
split
;
auto
with
zarith
.
rewrite
Mod_pow2_gen
;
auto
.
Qed
.
examples/bitvectors/bitvector/bitvector_BitVector_to_nat_of_zero2_1.v
deleted
100644 → 0
View file @
46afb5a9
(
*
This
file
is
generated
by
Why3
'
s
Coq
8.4
driver
*
)
(
*
Beware
!
Only
edit
allowed
sections
below
*
)
Require
Import
BuiltIn
.
Require
BuiltIn
.
Require
bool
.
Bool
.
Require
int
.
Int
.
Require
int
.
Abs
.
Require
int
.
EuclideanDivision
.
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
pow2pos
:
forall
(
i
:
Z
),
(
0
%
Z
<=
i
)
%
Z
->
(
0
%
Z
<
(
pow2
i
))
%
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
).
Axiom
Div_mult_inst
:
forall
(
x
:
Z
)
(
z
:
Z
),
(
0
%
Z
<
x
)
%
Z
->
((
int
.
EuclideanDivision
.
div
((
x
*
1
%
Z
)
%
Z
+
z
)
%
Z
x
)
=
(
1
%
Z
+
(
int
.
EuclideanDivision
.
div
z
x
))
%
Z
).
Axiom
Div_double
:
forall
(
x
:
Z
)
(
y
:
Z
),
((
0
%
Z
<
y
)
%
Z
/
\
((
y
<=
x
)
%
Z
/
\
(
x
<
(
2
%
Z
*
y
)
%
Z
)
%
Z
))
->
((
int
.
EuclideanDivision
.
div
x
y
)
=
1
%
Z
).
Axiom
Div_pow
:
forall
(
x
:
Z
)
(
i
:
Z
),
(
0
%
Z
<
i
)
%
Z
->
((((
pow2
(
i
