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
120
Issues
120
List
Boards
Labels
Service Desk
Milestones
Merge Requests
17
Merge Requests
17
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
e55e1d35
Commit
e55e1d35
authored
Jun 05, 2018
by
Raphael Rieu-Helft
1
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Add schoolbook GMP functions to examples and bench
parent
bb165cfe
Changes
34
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
34 changed files
with
29540 additions
and
1 deletion
+29540
-1
bench/bench
bench/bench
+2
-1
examples/multiprecision/add.mlw
examples/multiprecision/add.mlw
+548
-0
examples/multiprecision/add/why3session.xml
examples/multiprecision/add/why3session.xml
+1307
-0
examples/multiprecision/add/why3shapes.gz
examples/multiprecision/add/why3shapes.gz
+0
-0
examples/multiprecision/compare.mlw
examples/multiprecision/compare.mlw
+87
-0
examples/multiprecision/compare/why3session.xml
examples/multiprecision/compare/why3session.xml
+147
-0
examples/multiprecision/compare/why3shapes.gz
examples/multiprecision/compare/why3shapes.gz
+0
-0
examples/multiprecision/div.mlw
examples/multiprecision/div.mlw
+4433
-0
examples/multiprecision/div/why3session.xml
examples/multiprecision/div/why3session.xml
+10635
-0
examples/multiprecision/div/why3shapes.gz
examples/multiprecision/div/why3shapes.gz
+0
-0
examples/multiprecision/lemmas.mlw
examples/multiprecision/lemmas.mlw
+207
-0
examples/multiprecision/lemmas/why3session.xml
examples/multiprecision/lemmas/why3session.xml
+272
-0
examples/multiprecision/lemmas/why3shapes.gz
examples/multiprecision/lemmas/why3shapes.gz
+0
-0
examples/multiprecision/lineardecision.mlw
examples/multiprecision/lineardecision.mlw
+2105
-0
examples/multiprecision/lineardecision/why3session.xml
examples/multiprecision/lineardecision/why3session.xml
+4352
-0
examples/multiprecision/lineardecision/why3shapes.gz
examples/multiprecision/lineardecision/why3shapes.gz
+0
-0
examples/multiprecision/logical.mlw
examples/multiprecision/logical.mlw
+389
-0
examples/multiprecision/logical/why3session.xml
examples/multiprecision/logical/why3session.xml
+899
-0
examples/multiprecision/logical/why3shapes.gz
examples/multiprecision/logical/why3shapes.gz
+0
-0
examples/multiprecision/mul.mlw
examples/multiprecision/mul.mlw
+601
-0
examples/multiprecision/mul/why3session.xml
examples/multiprecision/mul/why3session.xml
+1471
-0
examples/multiprecision/mul/why3shapes.gz
examples/multiprecision/mul/why3shapes.gz
+0
-0
examples/multiprecision/sub.mlw
examples/multiprecision/sub.mlw
+546
-0
examples/multiprecision/sub/why3session.xml
examples/multiprecision/sub/why3session.xml
+1261
-0
examples/multiprecision/sub/why3shapes.gz
examples/multiprecision/sub/why3shapes.gz
+0
-0
examples/multiprecision/types.mlw
examples/multiprecision/types.mlw
+14
-0
examples/multiprecision/types/why3session.xml
examples/multiprecision/types/why3session.xml
+7
-0
examples/multiprecision/types/why3shapes.gz
examples/multiprecision/types/why3shapes.gz
+0
-0
examples/multiprecision/util.mlw
examples/multiprecision/util.mlw
+65
-0
examples/multiprecision/util/why3session.xml
examples/multiprecision/util/why3session.xml
+172
-0
examples/multiprecision/util/why3shapes.gz
examples/multiprecision/util/why3shapes.gz
+0
-0
examples/multiprecision/wmpn.mlw
examples/multiprecision/wmpn.mlw
+13
-0
examples/multiprecision/wmpn/why3session.xml
examples/multiprecision/wmpn/why3session.xml
+7
-0
examples/multiprecision/wmpn/why3shapes.gz
examples/multiprecision/wmpn/why3shapes.gz
+0
-0
No files found.
bench/bench
View file @
e55e1d35
...
...
@@ -269,8 +269,8 @@ goods examples/avl "-L examples/avl"
goods examples/verifythis_2016_matrix_multiplication
"-L examples/verifythis_2016_matrix_multiplication"
goods examples/double_wp
"-L examples/double_wp"
goods examples/ring_decision
"-L examples/ring_decision"
goods examples/multiprecision
"-L examples/multiprecision"
goods examples/in_progress
goods examples/in_progress/multiprecision
"-L examples/in_progress/multiprecision"
echo
""
echo
"=== Checking replay (no prover) ==="
...
...
@@ -290,6 +290,7 @@ replay examples/avl "-L examples/avl --merging-only"
#replay examples/to_port/verifythis_2016_matrix_multiplication "-L examples/to_port/verifythis_2016_matrix_multiplication --merging-only"
replay examples/double_wp
"-L examples/double_wp --merging-only"
replay examples/ring_decision
"-L examples/ring_decision --merging-only"
replay examples/multiprecision
"-L examples/multiprecision --merging-only"
#replay examples/in_progress --merging-only
#replay examples/in_progress/multiprecision "-L examples/in_progress/multiprecision --merging-only"
echo
""
...
...
examples/multiprecision/add.mlw
0 → 100644
View file @
e55e1d35
This diff is collapsed.
Click to expand it.
examples/multiprecision/add/why3session.xml
0 → 100644
View file @
e55e1d35
This diff is collapsed.
Click to expand it.
examples/multiprecision/add/why3shapes.gz
0 → 100644
View file @
e55e1d35
File added
examples/multiprecision/compare.mlw
0 → 100644
View file @
e55e1d35
module Compare
use import int.Int
use import mach.int.Int32
use import mach.int.UInt64GMP as Limb
use import int.Power
use import ref.Ref
use import mach.c.C
use import map.Map
use import types.Types
use import lemmas.Lemmas
function compare_int (x y:int) : int =
if x < y then -1 else if x=y then 0 else 1
(** [compare_same_size] compares [x[0..sz-1]] and [y[0..sz-1]] as unsigned integers. It corresponds to [GMPN_CMP]. *)
let compare_same_size (x y:t) (sz:int32) : int32
requires { valid x sz }
requires { valid y sz }
ensures { result = compare_int (value x sz) (value y sz) }
=
let i = ref sz in
try
while Int32.(>=) !i (Int32.of_int 1) do
variant { p2i !i }
invariant { 0 <= !i <= sz }
invariant { forall j. !i <= j < sz ->
(pelts x)[x.offset+j] = (pelts y)[y.offset+j] }
assert { forall j. 0 <= j < sz - !i ->
let k = !i+j in
!i <= k < sz ->
(pelts x)[x.offset+k] = (pelts y)[y.offset+k] /\
(pelts x)[!i+x.offset+j] = (pelts y)[!i+y.offset+j] };
value_sub_frame_shift (pelts x) (pelts y) (p2i !i+x.offset)
(p2i !i+y.offset) ((p2i sz) - (p2i !i));
let ghost k = p2i !i in
i := Int32.(-) !i (Int32.of_int 1);
assert { 0 <= !i < sz };
let lx = get_ofs x !i in
let ly = get_ofs y !i in
if (not (Limb.(=) lx ly))
then begin
value_sub_concat (pelts x) x.offset (x.offset+k) (x.offset+p2i sz);
value_sub_concat (pelts y) y.offset (y.offset+k) (y.offset+p2i sz);
assert { compare_int (value x sz)
(value y sz)
= compare_int (value x k) (value y k) };
value_sub_tail (pelts x) x.offset (x.offset+k-1);
value_sub_tail (pelts y) y.offset (y.offset+k-1);
if Limb.(>) lx ly
then begin
value_sub_upper_bound (pelts y) y.offset (y.offset+k-1);
value_sub_lower_bound (pelts x) x.offset (x.offset+k-1);
assert { value x k - value y k =
(l2i lx - ly) * (power radix (k-1))
- ((value y (k-1)) - (value x (k-1)))
};
assert { (lx - ly) * (power radix (k-1))
>= power radix (k-1)
> ((value y (k-1)) - (value x (k-1)))
};
raise Return32 (Int32.of_int 1)
end
else begin
assert { ly > lx };
value_sub_upper_bound (pelts x) x.offset (x.offset+k-1);
value_sub_lower_bound (pelts y) y.offset (y.offset+k-1);
assert { value y k - value x k =
(ly - lx) * (power radix (k-1))
- ((value x (k-1)) - (value y (k-1)))
};
assert { (ly - lx) * (power radix (k-1))
>= power radix (k-1)
> ((value x (k-1)) - (value y (k-1)))
};
raise Return32 (Int32.(-_) (Int32.of_int 1))
end
end
else ()
done;
value_sub_frame_shift (pelts x) (pelts y) x.offset y.offset (p2i sz);
Int32.of_int 0
with Return32 r -> r
end
end
\ No newline at end of file
examples/multiprecision/compare/why3session.xml
0 → 100644
View file @
e55e1d35
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"1"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"Z3"
version=
"4.5.0"
timelimit=
"1"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"4"
name=
"Z3"
version=
"4.4.1"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"5"
name=
"Alt-Ergo"
version=
"2.0.0"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<file
name=
"../compare.mlw"
proved=
"true"
>
<theory
name=
"Compare"
proved=
"true"
>
<goal
name=
"VC compare_same_size"
expl=
"VC for compare_same_size"
proved=
"true"
>
<transf
name=
"split_goal_right"
proved=
"true"
>
<goal
name=
"VC compare_same_size.0"
expl=
"loop invariant init"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
steps=
"9"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.1"
expl=
"loop invariant init"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"10"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.2"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.09"
steps=
"21"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.3"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.05"
steps=
"39"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.4"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
steps=
"46"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.5"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
steps=
"24"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.6"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
steps=
"26"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.7"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"16"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.8"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"28"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.9"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.05"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.06"
steps=
"28"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.10"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.05"
steps=
"20"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.11"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.06"
steps=
"21"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.12"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
steps=
"51"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.13"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.05"
steps=
"23"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.14"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.07"
steps=
"24"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.15"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.10"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.16"
expl=
"assertion"
proved=
"true"
>
<transf
name=
"inline_all"
proved=
"true"
>
<goal
name=
"VC compare_same_size.16.0"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"5"
timelimit=
"1"
><result
status=
"valid"
time=
"0.04"
steps=
"19"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC compare_same_size.17"
expl=
"assertion"
proved=
"true"
>
<transf
name=
"split_goal_right"
proved=
"true"
>
<goal
name=
"VC compare_same_size.17.0"
expl=
"VC for compare_same_size"
proved=
"true"
>
<proof
prover=
"1"
memlimit=
"2000"
><result
status=
"valid"
time=
"0.17"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.17.1"
expl=
"VC for compare_same_size"
proved=
"true"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC compare_same_size.18"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.19"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.20"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.05"
steps=
"26"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.21"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.06"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.22"
expl=
"assertion"
proved=
"true"
>
<transf
name=
"inline_all"
proved=
"true"
>
<goal
name=
"VC compare_same_size.22.0"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"5"
timelimit=
"1"
><result
status=
"valid"
time=
"0.05"
steps=
"20"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC compare_same_size.23"
expl=
"assertion"
proved=
"true"
>
<transf
name=
"split_goal_right"
proved=
"true"
>
<goal
name=
"VC compare_same_size.23.0"
expl=
"VC for compare_same_size"
proved=
"true"
>
<proof
prover=
"1"
memlimit=
"2000"
><result
status=
"valid"
time=
"0.27"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.23.1"
expl=
"VC for compare_same_size"
proved=
"true"
>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC compare_same_size.24"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.04"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.23"
steps=
"43"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.25"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.04"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.26"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.27"
expl=
"loop variant decrease"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.03"
/></proof>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"20"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.28"
expl=
"loop invariant preservation"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
steps=
"20"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.29"
expl=
"loop invariant preservation"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"44"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.30"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"43"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.31"
expl=
"integer overflow"
proved=
"true"
>
<proof
prover=
"4"
><result
status=
"valid"
time=
"0.03"
/></proof>
</goal>
<goal
name=
"VC compare_same_size.32"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.10"
steps=
"37"
/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
examples/multiprecision/compare/why3shapes.gz
0 → 100644
View file @
e55e1d35
File added
examples/multiprecision/div.mlw
0 → 100644
View file @
e55e1d35
This diff is collapsed.
Click to expand it.
examples/multiprecision/div/why3session.xml
0 → 100644
View file @
e55e1d35
This diff is collapsed.
Click to expand it.
examples/multiprecision/div/why3shapes.gz
0 → 100644
View file @
e55e1d35
File added
examples/multiprecision/lemmas.mlw
0 → 100644
View file @
e55e1d35
module Lemmas
use import array.Array
use import map.Map
use map.MapEq
use map.Const
use import int.Int
(** {3 complements to map standard library} *)
predicate map_eq_sub_shift (x y:map int 'a) (xi yi sz:int) =
forall i. 0 <= i < sz -> x[xi+i] = y[yi+i]
let lemma map_eq_shift (x y:map int 'a) (xi yi sz k:int)
requires { map_eq_sub_shift x y xi yi sz }
requires { 0 <= k < sz }
ensures { x[xi+k] = y[yi+k] }
= ()
let rec lemma map_eq_shift_zero (x y: map int 'a) (n m: int)
requires { map_eq_sub_shift x y n n (m-n) }
variant { m - n }
ensures { MapEq.map_eq_sub x y n m }
=
if n < m then
begin
assert { forall i. 0 <= i < m-n -> x[n+i] = y[n+i] };
assert { forall i. n <= i < m ->
let j = i - n in 0 <= j < m-n ->
x[n+j] = y[n+j] -> x[i] = y[i]};
map_eq_shift_zero x y (n+1) m;
end
else ()
use import mach.int.Int32
use import ref.Ref
use import mach.int.UInt64GMP as Limb
use import int.Int
use import int.Power
use import mach.c.C
use import types.Types
meta compute_max_steps 0x100000
(** {3 Long integers as arrays of libs} *)
lemma limb_max_bound: 1 <= max_uint64
function l2i (x:limb) : int = Limb.to_int x
function p2i (i:int32) : int = int32'int i
let lemma prod_compat_strict_r (a b c:int)
requires { 0 <= a < b }
requires { 0 < c }
ensures { c * a < c * b }
= ()
let lemma prod_compat_r (a b c:int)
requires { 0 <= a <= b }
requires { 0 <= c }
ensures { c * a <= c * b }
= ()
(** {3 Integer value of a natural number} *)
(** [value_sub x n m] denotes the integer represented by
the digits x[n..m-1] with lsb at index n *)
let rec ghost function value_sub (x:map int limb) (n:int) (m:int) : int
variant {m - n}
=
if n < m then
l2i x[n] + radix * value_sub x (n+1) m
else 0
let rec lemma value_sub_frame (x y:map int limb) (n m:int)
requires { MapEq.map_eq_sub x y n m }
variant { m - n }
ensures { value_sub x n m = value_sub y n m }
=
if n < m then value_sub_frame x y (n+1) m else ()
let rec lemma value_sub_frame_shift (x y:map int limb) (xi yi sz:int)
requires { map_eq_sub_shift x y xi yi sz }
variant { sz }
ensures { value_sub x xi (xi+sz) = value_sub y yi (yi+sz) }
=
if sz>0
then begin
map_eq_shift x y xi yi sz 0;
assert { forall i. 0 <= i < sz-1 ->
let j = 1+i in x[xi+j] = y[yi+j] };
value_sub_frame_shift x y (xi+1) (yi+1) (sz-1)
end
else assert { 1+2 = 3 }
let rec lemma value_sub_tail (x:map int limb) (n m:int)
requires { n <= m }
variant { m - n }
ensures {
value_sub x n (m+1) =
value_sub x n m + (Map.get x m) * power radix (m-n) }
= [@vc:sp] if n < m then value_sub_tail x (n+1) m else ()(*assert { 1+2=3 }*)
let rec lemma value_sub_concat (x:map int limb) (n m l:int)
requires { n <= m <= l}
variant { m - n }
ensures {
value_sub x n l =
value_sub x n m + value_sub x m l * power radix (m-n) }
=
if n < m then
begin
assert {n<m};
value_sub_concat x (n+1) m l
end
else ()
let lemma value_sub_head (x:map int limb) (n m:int)
requires { n < m }
ensures { value_sub x n m = x[n] + radix * value_sub x (n+1) m }
= value_sub_concat x n (n+1) m
let lemma value_sub_update (x:map int limb) (i n m:int) (v:limb)
requires { n <= i < m }
ensures {
value_sub (Map.set x i v) n m =
value_sub x n m + power radix (i - n) * (v -(Map.get x i))
}
= assert { MapEq.map_eq_sub x (Map.set x i v) n i };
assert { MapEq.map_eq_sub x (Map.set x i v) (i+1) m };
value_sub_concat x n i m;
value_sub_concat (Map.set x i v) n i m;
value_sub_head x i m;
value_sub_head (Map.set x i v) i m
let rec lemma value_zero (x:map int limb) (n m:int)
requires { MapEq.map_eq_sub x (Const.const Limb.zero_unsigned) n m }
variant { m - n }
ensures { value_sub x n m = 0 }
= if n < m then value_zero x (n+1) m else ()
let lemma value_sub_update_no_change (x: map int limb) (i n m: int) (v:limb)
requires { n <= m }
requires { i < n \/ m <= i }
ensures { value_sub x n m = value_sub (Map.set x i v) n m }
= value_sub_frame x (Map.set x i v) n m
let lemma value_sub_shift_no_change (x:map int limb) (ofs i sz:int) (v:limb)
requires { i < 0 \/ sz <= i }
requires { 0 <= sz }
ensures { value_sub x ofs (ofs + sz) =
value_sub (Map.set x (ofs+i) v) ofs (ofs+sz) }
= value_sub_frame_shift x (Map.set x (ofs+i) v) ofs ofs sz
(** {3 Comparisons} *)
let rec lemma value_sub_lower_bound (x:map int limb) (x1 x2:int)
variant { x2 - x1 }
ensures { 0 <= value_sub x x1 x2 }
= if x2 <= x1 then () else
begin
value_sub_head x x1 x2;
value_sub_lower_bound x (x1+1) x2
end
let rec lemma value_sub_upper_bound (x:map int limb) (x1 x2:int)
requires { x1 <= x2 }
variant { x2 - x1 }
ensures { value_sub x x1 x2 < power radix (x2 - x1) }
= if x1 = x2 then () else
begin
value_sub_tail x x1 (x2-1);
assert { value_sub x x1 x2
<= value_sub x x1 (x2-1) + power radix (x2-x1-1) * (radix - 1) };
value_sub_upper_bound x x1 (x2-1)
end
let lemma value_sub_lower_bound_tight (x:map int limb) (x1 x2:int)
requires { x1 < x2 }
ensures { power radix (x2-x1-1) * l2i (Map.get x (x2-1)) <= value_sub x x1 x2 }
= assert { value_sub x x1 x2 = value_sub x x1 (x2-1)
+ power radix (x2-x1-1) * l2i (Map.get x (x2-1)) }
let lemma value_sub_upper_bound_tight (x:map int limb) (x1 x2:int)
requires { x1 < x2 }
ensures { value_sub x x1 x2 < power radix (x2-x1-1) * (l2i (Map.get x (x2-1)) + 1) }
= value_sub_upper_bound x x1 (x2-1)
function value (x:t) (sz:int) : int =
value_sub (pelts x) x.offset (x.offset + sz)
let lemma value_tail (x:t) (sz:int32)
requires { 0 <= sz }
ensures { value x (sz+1) = value x sz + (pelts x)[x.offset + sz] * power radix sz }
= value_sub_tail (pelts x) x.offset (x.offset + p2i sz)
meta remove_prop axiom value_tail
let lemma value_concat (x:t) (n m:int32)
requires { 0 <= n <= m }
ensures { value x m
= value x n + power radix n
* value_sub (pelts x) (x.offset + n) (x.offset + m) }
= value_sub_concat (pelts x) x.offset (x.offset + p2i n) (x.offset + p2i m)
end
\ No newline at end of file
examples/multiprecision/lemmas/why3session.xml
0 → 100644
View file @
e55e1d35
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session
shape_version=
"4"
>
<prover
id=
"0"
name=
"Eprover"
version=
"1.9.1-001"
timelimit=
"5"
steplimit=
"0"
memlimit=
"2000"
/>
<prover
id=
"1"
name=
"CVC3"
version=
"2.4.1"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"2"
name=
"CVC4"
version=
"1.4"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"3"
name=
"Z3"
version=
"4.5.0"
timelimit=
"1"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"4"
name=
"Z3"
version=
"4.4.1"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<prover
id=
"5"
name=
"Alt-Ergo"
version=
"2.0.0"
timelimit=
"5"
steplimit=
"0"
memlimit=
"1000"
/>
<file
name=
"../lemmas.mlw"
proved=
"true"
>
<theory
name=
"Lemmas"
proved=
"true"
>
<goal
name=
"VC map_eq_shift"
expl=
"VC for map_eq_shift"
proved=
"true"
>
<transf
name=
"split_goal_right"
proved=
"true"
>
<goal
name=
"VC map_eq_shift.0"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"5"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC map_eq_shift_zero"
expl=
"VC for map_eq_shift_zero"
proved=
"true"
>
<transf
name=
"split_goal_right"
proved=
"true"
>
<goal
name=
"VC map_eq_shift_zero.0"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
steps=
"6"
/></proof>
</goal>
<goal
name=
"VC map_eq_shift_zero.1"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"8"
/></proof>
</goal>
<goal
name=
"VC map_eq_shift_zero.2"
expl=
"variant decrease"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
steps=
"3"
/></proof>
</goal>
<goal
name=
"VC map_eq_shift_zero.3"
expl=
"precondition"
proved=
"true"
>
<transf
name=
"introduce_premises"
proved=
"true"
>
<goal
name=
"VC map_eq_shift_zero.3.0"
expl=
"precondition"
proved=
"true"
>
<transf
name=
"inline_goal"
proved=
"true"
>
<goal
name=
"VC map_eq_shift_zero.3.0.0"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"5"
timelimit=
"1"
><result
status=
"valid"
time=
"0.00"
steps=
"10"
/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal
name=
"VC map_eq_shift_zero.4"
expl=
"postcondition"
proved=
"true"
>
<transf
name=
"inline_all"
proved=
"true"
>
<goal
name=
"VC map_eq_shift_zero.4.0"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"5"
memlimit=
"2000"
><result
status=
"valid"
time=
"0.00"
steps=
"10"
/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal
name=
"limb_max_bound"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.02"
steps=
"5"
/></proof>
</goal>
<goal
name=
"VC prod_compat_strict_r"
expl=
"VC for prod_compat_strict_r"
proved=
"true"
>
<proof
prover=
"1"
><result
status=
"valid"
time=
"0.05"
/></proof>
</goal>
<goal
name=
"VC prod_compat_r"
expl=
"VC for prod_compat_r"
proved=
"true"
>
<proof
prover=
"5"
memlimit=
"2000"
><result
status=
"valid"
time=
"0.02"
steps=
"10"
/></proof>
</goal>
<goal
name=
"VC value_sub"
expl=
"VC for value_sub"
proved=
"true"
>
<transf
name=
"split_goal_right"
proved=
"true"
>
<goal
name=
"VC value_sub.0"
expl=
"variant decrease"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"7"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC value_sub_frame"
expl=
"VC for value_sub_frame"
proved=
"true"
>
<transf
name=
"split_goal_right"
proved=
"true"
>
<goal
name=
"VC value_sub_frame.0"
expl=
"variant decrease"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"8"
/></proof>
</goal>
<goal
name=
"VC value_sub_frame.1"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
steps=
"23"
/></proof>
</goal>
<goal
name=
"VC value_sub_frame.2"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.07"
steps=
"34"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC value_sub_frame_shift"
expl=
"VC for value_sub_frame_shift"
proved=
"true"
>
<transf
name=
"split_goal_right"
proved=
"true"
>
<goal
name=
"VC value_sub_frame_shift.0"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.02"
steps=
"8"
/></proof>
</goal>
<goal
name=
"VC value_sub_frame_shift.1"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
steps=
"8"
/></proof>
</goal>
<goal
name=
"VC value_sub_frame_shift.2"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"12"
/></proof>
</goal>
<goal
name=
"VC value_sub_frame_shift.3"
expl=
"variant decrease"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.02"
steps=
"9"
/></proof>
</goal>
<goal
name=
"VC value_sub_frame_shift.4"
expl=
"precondition"
proved=
"true"
>
<transf
name=
"introduce_premises"
proved=
"true"
>
<goal
name=
"VC value_sub_frame_shift.4.0"
expl=
"precondition"
proved=
"true"
>
<transf
name=
"inline_goal"
proved=
"true"
>
<goal
name=
"VC value_sub_frame_shift.4.0.0"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"0"
><result
status=
"valid"
time=
"0.17"
/></proof>
<proof
prover=
"3"
><result
status=
"valid"
time=
"0.02"
/></proof>
<proof
prover=
"4"
memlimit=
"2000"
><result
status=
"valid"
time=
"0.02"
/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal
name=
"VC value_sub_frame_shift.5"
expl=
"assertion"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"8"
/></proof>
</goal>
<goal
name=
"VC value_sub_frame_shift.6"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.02"
steps=
"12"
/></proof>
</goal>
</transf>
</goal>
<goal
name=
"VC value_sub_tail"
expl=
"VC for value_sub_tail"
proved=
"true"
>
<transf
name=
"split_goal_right"
proved=
"true"
>
<goal
name=
"VC value_sub_tail.0"
expl=
"variant decrease"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.03"
steps=
"8"
/></proof>
</goal>
<goal
name=
"VC value_sub_tail.1"
expl=
"precondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.04"
steps=
"8"
/></proof>
</goal>
<goal
name=
"VC value_sub_tail.2"
expl=
"postcondition"
proved=
"true"
>
<proof
prover=
"5"
><result
status=
"valid"
time=
"0.07"
steps=
"34"
/></proof>