Commit bb11ac5a authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'claude'

parents f7b45e7c 12855fcc
......@@ -226,6 +226,8 @@ pvsbin/
/examples/vstte12_combinators/*__*.ml
/examples/in_progress/bigInt/jsmain.js
/examples/in_progress/bigInt/*__*.ml
/examples/in_progress/mp/jsmain.js
/examples/in_progress/mp/*__*.ml
# modules
......
......@@ -45,6 +45,14 @@ module mach.int.UInt32
syntax val (<) "(<)"
syntax val (>=) "(>=)"
syntax val (>) "(>)"
(* direct realization of add_with_carry.
Remind that parameters x y and c are assumed to denote unsigned integers
less than 2^{32} *)
syntax val add_with_carry "(fun x y c ->
let r = Int64.add x (Int64.add y c) in
(Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))"
end
module mach.int.Int63
......
(** A library for arbitrary-precision integer arithmetic *)
(** {1 A library for arbitrary-precision integer arithmetic} *)
module N
......@@ -11,10 +11,18 @@ module N
use import int.Int
use import int.Power
(** {2 data type for unbound integers and invariants} *)
constant base : int = 10000
(** a power of ten whose square fits on 31 bits *)
type t = { mutable digits: array int31 }
(** an unbounded integer is stored in an array of 31 bits integers,
with all values between 0 included and [base] excluded
index 0 is the lsb. the msb is never 0.
*)
predicate ok_array (a:array int31) =
(to_int a.length >= 1 -> to_int a[to_int a.length - 1] <> 0) /\
forall i:int. 0 <= i < to_int a.length ->
......@@ -22,6 +30,9 @@ module N
predicate ok (x:t) = ok_array x.digits
(** {2 value stored in an array} *)
(* [value_sub x n m] denotes the integer represented by
the digits x[n..m-1] with lsb at index n *)
function value_sub (x:map int int31) (n:int) (m:int) (l:int): int
......@@ -79,6 +90,46 @@ module N
function value (x:t) : int = value_array x.digits
(** {2 general lemmas} *)
(* moved to stdlib
lemma power_monotonic:
forall x y z. 0 <= x <= y -> power z x <= power z y
*)
lemma power_non_neg:
forall x y. x >= 0 /\ y >= 0 -> power x y >= 0
lemma value_zero:
forall x:array int31.
let l = to_int x.length in
l = 0 -> value_array x = 0
lemma value_sub_upper_bound:
forall x:map int int31, n l:int. 0 <= n <= l ->
(forall i:int. 0 <= i < n -> 0 <= to_int (Map.get x i) < base) ->
value_sub x 0 n l < power base n
lemma value_sub_lower_bound:
forall x:map int int31, n l:int. 0 <= n <= l ->
(forall i:int. 0 <= i < n -> 0 <= to_int (Map.get x i) < base) ->
0 <= value_sub x 0 n l
lemma value_sub_lower_bound_tight:
forall x:map int int31, n l:int. 0 < n <= l ->
(forall i:int. 0 <= i < n-1 -> 0 <= to_int (Map.get x i) < base) ->
0 < to_int (Map.get x (n-1)) < base ->
power base (n-1) <= value_sub x 0 n l
lemma value_bounds_array:
forall x:array int31. ok_array x ->
let l = to_int x.length in
l > 0 -> power base (l-1) <= value_array x < power base l
(** {2 conversion from a small integer} *)
let from_small_int (n:int31) : t
requires { 0 <= to_int n < base }
ensures { ok result }
......@@ -92,6 +143,98 @@ module N
in
{ digits = a }
(** {2 Comparisons} *)
exception Break
(* Comparisons *)
let compare_array (x y:array int31) : int31
requires { ok_array x /\ ok_array y }
ensures { -1 <= to_int result <= 1 }
ensures { to_int result = -1 -> value_array x < value_array y }
ensures { to_int result = 0 -> value_array x = value_array y }
ensures { to_int result = 1 -> value_array x > value_array y }
= let zero = of_int 0 in
let one = of_int 1 in
let minus_one = of_int (-1) in
let l1 = x.length in
let l2 = y.length in
if Int31.(<) l1 l2 then minus_one else
if Int31.(>) l1 l2 then one else
let i = ref l1 in
let res = ref zero in
let ghost acc = ref 0 in
try
while Int31.(>) !i zero do
invariant { to_int !res = 0 }
(* needed to be sure it is zero at normal exit ! *)
invariant { 0 <= to_int !i <= to_int l1 }
invariant {
value_sub x.elts 0 (to_int !i) (to_int l1) = value_array x - !acc
}
invariant {
value_sub y.elts 0 (to_int !i) (to_int l1) = value_array y - !acc
}
variant { to_int !i }
assert { value_array x - !acc =
value_sub x.elts 0 (to_int !i - 1) (to_int l1) +
power base (to_int !i - 1) * (to_int x[to_int !i - 1])
};
assert { value_array y - !acc =
value_sub y.elts 0 (to_int !i - 1) (to_int l1) +
power base (to_int !i - 1) * (to_int y[to_int !i - 1])
};
i := Int31.(-) !i one;
if Int31.(<) x[!i] y[!i] then
begin
assert { value_sub y.elts 0 (to_int !i) (to_int l1) >= 0 };
assert { value_sub x.elts 0 (to_int !i) (to_int l1) <
power base (to_int !i)
};
assert { value_array y - !acc >=
power base (to_int !i) * (to_int y[to_int !i])
};
assert { to_int y[to_int !i] >= to_int x[to_int !i] + 1 };
assert { power base (to_int !i) * (to_int y[to_int !i]) >=
power base (to_int !i) * (to_int x[to_int !i] + 1) };
assert { power base (to_int !i) * (to_int y[to_int !i]) >=
power base (to_int !i) * (to_int x[to_int !i])
+ power base (to_int !i) };
res := minus_one;
raise Break;
end;
if Int31.(>) x[!i] y[!i] then
begin
assert { value_sub x.elts 0 (to_int !i) (to_int l1) >= 0 };
assert { value_sub y.elts 0 (to_int !i) (to_int l1) <
power base (to_int !i)
};
assert { value_array x - !acc >=
power base (to_int !i) * (to_int x[to_int !i])
};
assert { to_int x[to_int !i] >= to_int y[to_int !i] + 1 };
assert { power base (to_int !i) * (to_int x[to_int !i]) >=
power base (to_int !i) * (to_int y[to_int !i] + 1) };
assert { power base (to_int !i) * (to_int x[to_int !i]) >=
power base (to_int !i) * (to_int y[to_int !i])
+ power base (to_int !i) };
res := one;
raise Break
end;
acc := !acc + power base (to_int !i) * to_int x[!i];
done;
raise Break
with Break -> !res
end
let eq (x y:t) : bool
requires { ok x /\ ok y }
ensures { if result then value x = value y else value x <> value y }
= Int31.eq (compare_array x.digits y.digits) (of_int 0)
(** {2 arithmetic operations} *)
exception TooManyDigits
let add_array (x y:array int31) : array int31
......@@ -176,7 +319,7 @@ module N
assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
value_sub (at arr 'L).elts 0 (to_int !i) (to_int h + 1) };
assert { value_array arr = value_array x + value_array y };
abstract
abstract
ensures { -1 <= to_int !non_null_idx <= to_int !i }
ensures { to_int !non_null_idx >= 0 -> to_int arr[to_int !non_null_idx] <> 0 }
ensures {
......@@ -194,9 +337,9 @@ module N
MapEq.map_eq_sub arr.elts arr'.elts 0 (to_int len) };
assert { value_sub arr.elts 0 (to_int len) (to_int len) =
value_sub arr'.elts 0 (to_int len) (to_int len) } ;
assert { to_int arr'.length >= 1 ->
assert { to_int arr'.length >= 1 ->
to_int arr'[to_int arr'.length - 1] <> 0 };
assert { forall j. 0 <= j < to_int arr'.length ->
assert { forall j. 0 <= j < to_int arr'.length ->
0 <= to_int arr'[j] < base };
arr'
......@@ -214,7 +357,26 @@ module N
in
{ digits = res }
(* Multiplication: school book algorithm *)
(*
let rec mul_array (x y:array int31) : array int31
requires { ok_array x /\ ok_array y }
ensures { ok_array result }
ensures { value_array result = value_array x * value_array y }
raises { TooManyDigits -> true }
= let zero = of_int 0 in
let one = of_int 1 in
let two = of_int 2 in
let base31 = of_int 10000 in
assert { to_int base31 = base };
let l1 = x.digits.length in
let l2 = y.digits.length in
TODO
*)
(* Multiplication: Karatsuba algorithm
let rec mul_array (x y:array int31) : array int31
requires { ok_array x /\ ok_array y }
ensures { ok_array result }
......@@ -233,8 +395,12 @@ module N
let h = Int31.(/) n base31 in
let l = Int31.(-) n (Int31.(*) h base31) in
if Int31.eq h zero then
let arr = Array31.make one l in
{ digits = arr }
if Int31.eq l zero then
let arr = Array31.make zero zero in
{ digits = arr }
else
let arr = Array31.make one l in
{ digits = arr }
else
let arr = Array31.make two l in
arr.(1) <- h;
......@@ -260,6 +426,8 @@ module N
let z2 = mul_array high1 high2 in
(*
return (z2*10^(2*m2))+((z1-z2-z0)*10^(m2))+(z0)
-> we need subtraction !
*)
let mul (x y:t) : t
......
This diff is collapsed.
This diff is collapsed.
BENCH ?= no
ifeq ($(BENCH),yes)
WHY3=../../bin/why3
WHY3SHARE=../../share
else
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
WHY3SHARE=$(shell $(WHY3) --print-datadir)
endif
include $(WHY3SHARE)/Makefile.config
ifeq ($(BENCH),yes)
INCLUDE += -I ../../lib/why3
endif
MAIN=main
GEN=map__Map mp__N
OBJ=$(GEN) parse
GENML = $(addsuffix .ml, $(GEN))
ML = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
CMX = $(addsuffix .cmx, $(OBJ))
OCAMLOPT=ocamlopt -noassert -inline 1000
all: $(MAIN).$(OCAMLBEST)
extract: $(GENML)
parse.cmo: mp__N.cmo
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -g -o $@ $^
$(MAIN).opt: $(CMX) $(MAIN).cmx
$(OCAMLOPT) $(INCLUDE) $(BIGINTLIB).cmxa why3extract.cmxa -o $@ $^
$(MAIN).cmx: $(CMX)
$(GENML): ../mp.mlw
$(WHY3) -E ocaml32 $< -o .
%.cmx: %.ml
$(OCAMLOPT) $(INCLUDE) -annot -c $<
%.cmo: %.ml
ocamlc -g $(INCLUDE) -annot -c $<
%.cmi: %.mli
ocamlc -g $(INCLUDE) -annot -c $<
clean::
rm -f $(GENML) *.cm[xio] *.o *.annot $(MAIN).opt $(MAIN).byte
rm -f why3__*.ml* mp__*.ml* int__*.ml*
# javascript
JSMAIN=jsmain
JSOCAMLC=ocamlfind ocamlc -package js_of_ocaml -package js_of_ocaml.syntax \
-syntax camlp4o
$(JSMAIN).js: $(JSMAIN).byte
js_of_ocaml -pretty -noinline $(JSMAIN).byte
$(JSMAIN).byte: $(CMO) jsmain.ml
$(JSOCAMLC) $(INCLUDE) -o $@ -linkpkg $^
%.cmo: %.ml
$(JSOCAMLC) $(INCLUDE) -g -annot -c $<
%.cmi: %.mli
$(JSOCAMLC) $(INCLUDE) -g -annot -c $<
<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN"
"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>Javascript test for bigInt</title>
</head>
<body id="test">
<h1>Javascript test for bigInt</h1>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<script type="text/javascript" src="jsmain.js"></script>
</body>
</html>
(* computation part *)
let compute_result text =
try
let a,i = Parse.parse_dec_ip text 0 in
let i = Parse.parse_sep_star text i in
let b,i = Parse.parse_dec_ip text i in
Mp__N.add_in_place a b;
Parse.pr Format.str_formatter a;
Format.flush_str_formatter ()
with Parse.SyntaxError -> "syntax error"
(* HTML rendering *)
module Html = Dom_html
let node x = (x : #Dom.node Js.t :> Dom.node Js.t)
let (<|) e l = List.iter (fun c -> Dom.appendChild e c) l; node e
let html_of_string (d : Html.document Js.t) (s:string) =
d##createElement (Js.string "p") <|
[node (d##createTextNode (Js.string s))]
let replace_child p n =
Js.Opt.iter (p##firstChild) (fun c -> Dom.removeChild p c);
Dom.appendChild p n
let onload (_event : #Html.event Js.t) : bool Js.t =
let d = Html.document in
let body =
Js.Opt.get (d##getElementById(Js.string "test"))
(fun () -> assert false) in
let textbox = Html.createTextarea d in
textbox##rows <- 20; textbox##cols <- 100;
let preview = Html.createDiv d in
preview##style##border <- Js.string "1px black";
preview##style##padding <- Js.string "5px";
Dom.appendChild body textbox;
Dom.appendChild body (Html.createBr d);
Dom.appendChild body preview;
let rec dyn_preview old_text n =
let text = Js.to_string (textbox##value) in
let n =
if text <> old_text then
begin
begin try
let rendered =
html_of_string d (compute_result text)
in
replace_child preview rendered
with _ -> ()
end;
20
end
else
max 0 (n - 1)
in
Lwt.bind
(Lwt_js.sleep (if n = 0 then 0.5 else 0.1))
(fun () -> dyn_preview text n)
in
let (_ : 'a Lwt.t) = dyn_preview "" 0 in Js._false
let (_ : unit) = Html.window##onload <- Html.handler onload
open Why3extract
open Format
let usage () =
eprintf "Usage: %s <decimal number>@." Sys.argv.(0);
exit 2
let input =
if Array.length Sys.argv <> 2 then usage ();
Sys.argv.(1)
open Mp__N
let input_num =
try let a,i = Parse.parse_dec_ip input 0 in a
with Parse.SyntaxError -> usage ()
let () =
let z = zero () in
Format.printf "zero : %a@." Parse.pr z;
let a = from_limb 1L in
Format.printf "one : %a@." Parse.pr a;
let a = from_limb 0xFFFFFFFFL in
Format.printf "2^{32}-1 : %a@." Parse.pr a;
add_in_place z a;
Format.printf "0 + 2^{32}-1 : %a@." Parse.pr z;
add_in_place a (from_limb 1L);
Format.printf "2^{32}-1+1 : %a@." Parse.pr a;
let a = copy input_num in
Format.printf "input : %a@." Parse.pr a;
add_in_place a input_num;
Format.printf "times 2 : %a@." Parse.pr a;
add_in_place a input_num ;
Format.printf "times 3 : %a@." Parse.pr a
open Mp__N
let n__add = Mp__N.add
let n__zero = Mp__N.zero
let n__from_limb = Mp__N.from_limb
open Format
let pr fmt a =
let a = a.digits in
let l = Array.length a in
for i=l-1 downto 0 do
fprintf fmt "|%08LX" a.(i);
done;
fprintf fmt "|"
exception SyntaxError
(*
let times10 a =
let a2 = n__add a a in
let a4 = n__add a2 a2 in
let a5 = n__add a4 a in
n__add a5 a5
let parse_dec s idx =
let a = ref (n__zero ()) in
let i = ref idx in
try
while !i < String.length s do
match String.get s !i with
| '0'..'9' as c ->
let d = Int64.of_int (Char.code c - Char.code '0') in
a := n__add (times10 !a) (n__from_limb d);
i := succ !i
| _ ->
raise Exit
done;
raise Exit
with Exit ->
if !i = idx then raise SyntaxError else !a,!i
*)
let times10_ip a =
let b = copy a in
add_in_place a a; (* times 2 *)
add_in_place a a; (* times 4 *)
add_in_place a b; (* times 5 *)
add_in_place a a (* times 10 *)
let parse_dec_ip s idx =
let a = n__zero () in
let i = ref idx in
try
while !i < String.length s do
match String.get s !i with
| '0'..'9' as c ->
let d = Int64.of_int (Char.code c - Char.code '0') in
eprintf "parse_dec_ip: a = %a@." pr a;
times10_ip a;
eprintf "parse_dec_ip: 10a = %a, d=%Ld@." pr a d;
add_in_place a (n__from_limb d);
eprintf "parse_dec_ip: a = %a@." pr a;
i := succ !i
| _ ->
raise Exit
done;
raise Exit
with Exit ->
if !i = idx then raise SyntaxError else a,!i
let parse_sep_star s idx =
let i = ref idx in
try
while !i < String.length s do
match String.get s !i with
| ' ' | '\t' | '\n' | '\r' -> i := succ !i
| _ -> raise Exit
done;
raise Exit
with Exit -> !i
This diff is collapsed.
......@@ -79,3 +79,19 @@ rewrite 3!power_is_exponentiation ; auto with zarith.
apply Power_mult2 ; auto with zarith.
Qed.
(* Why3 goal *)
Lemma Power_non_neg : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z <= y)%Z) ->
(0%Z <= (power x y))%Z.
intros x y (h1,h2).
now apply Z.pow_nonneg.
Qed.
Open Scope Z_scope.
(* Why3 goal *)
Lemma Power_monotonic : forall (x:Z) (n:Z) (m:Z), ((0%Z < x)%Z /\
((0%Z <= n)%Z /\ (n <= m)%Z)) -> ((power x n) <= (power x m))%Z.
intros.
apply Z.pow_le_mono_r; auto with zarith.
Qed.
......@@ -24,11 +24,11 @@ module Array32
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
val ([]) (a: array ~'a) (i: int32) : 'a
requires { 0 <= to_int i < to_int a.length }
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
val ([]<-) (a: array ~'a) (i: int32) (v: 'a) : unit writes {a}
requires { 0 <= to_int i < to_int a.length }
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = M.set (old a.elts) (to_int i) v }
val length (a: array ~'a) : int32 ensures { result = a.length }
......@@ -54,7 +54,7 @@ module Array32
{ length = n; elts = M.const v }
val make (n: int32) (v: ~'a) : array 'a
requires { to_int n >= 0 }
requires { "expl:array creation size" to_int n >= 0 }
ensures { result = make n v }
val append (a1: array ~'a) (a2: array 'a) : array 'a
......@@ -141,11 +141,11 @@ module Array31
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
val ([]) (a: array ~'a) (i: int31) : 'a
requires { 0 <= to_int i < to_int a.length }
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
val ([]<-) (a: array ~'a) (i: int31) (v: 'a) : unit writes {a}
requires { 0 <= to_int i < to_int a.length }
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = M.set (old a.elts) (to_int i) v }
val length (a: array ~'a) : int31 ensures { result = a.length }
......@@ -171,7 +171,7 @@ module Array31
{ length = n; elts = M.const v }
val make (n: int31) (v: ~'a) : array 'a
requires { to_int n >= 0 }
requires { "expl:array creation size" to_int n >= 0 }
ensures { result = make n v }
val append (a1: array ~'a) (a2: array 'a) : array 'a
......@@ -258,11 +258,11 @@ module Array63
function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v
val ([]) (a: array ~'a) (i: int63) : 'a
requires { 0 <= to_int i < to_int a.length }
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { result = a[to_int i] }
val ([]<-) (a: array ~'a) (i: int63) (v: 'a) : unit writes {a}
requires { 0 <= to_int i < to_int a.length }
requires { "expl:index in array bounds" 0 <= to_int i < to_int a.length }
ensures { a.elts = M.set (old a.elts) (to_int i) v }
val length (a: array ~'a) : int63 ensures { result = a.length }
......@@ -288,7 +288,7 @@ module Array63
{ length = n; elts = M.const v }
val make (n: int63) (v: ~'a) : array 'a
requires { to_int n >= 0 }
requires { "expl:array creation size" to_int n >= 0 }
ensures { result = make n v }
val append (a1: array ~'a) (a2: array 'a) : array 'a
......
......@@ -104,6 +104,26 @@ module Bounded_int
end
module Unsigned
use import int.Int
constant min_unsigned : int = 0
clone export Bounded_int with
constant min = min_unsigned
constant zero_unsigned : t
axiom zero_unsigned_is_zero : to_int zero_unsigned = 0
val add_with_carry (x y:t) (c:t) : (t,t)
returns { (r,d) ->
to_int r + (max+1) * to_int d =
to_int x + to_int y + to_int c }
end
module Int31
use import int.Int
......@@ -140,12 +160,10 @@ module UInt32
type uint32
constant min_uint32 : int = 0x00000000
constant max_uint32 : int = 0xffffffff
clone export Bounded_int with
clone export Unsigned with
type t = uint32,
constant min = min_uint32,
constant max = max_uint32
end
......@@ -188,12 +206,10 @@ module UInt64
type uint64
constant min_uint64 : int = 0x0000000000000000
constant max_uint64 : int = 0xffffffffffffffff
clone export Bounded_int with
clone export Unsigned with
type t = uint64,
constant min = min_uint64,
constant max = max_uint64
end
......@@ -235,6 +235,12 @@ theory Power
goal CommutativeMonoid.Unit_def_l, goal CommutativeMonoid.Unit_def_r,
goal CommutativeMonoid.Comm.Comm
lemma Power_non_neg:
forall x y. x >= 0 /\ y >= 0 -> power x y >= 0
lemma Power_monotonic:
forall x n m:int. 0 < x /\ 0 <= n <= m -> power x n <= power x m
end
(** {2 Number of elements satisfying a given predicate}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment