Commit 12855fcc authored by MARCHE Claude's avatar MARCHE Claude

mp: in place addition, javascript extraction, all proved

parent e3332a88
......@@ -38,7 +38,7 @@ module N
type limb = Limb.uint32
axiom limb_max_bound: 1 <= Limb.max_uint32
lemma limb_max_bound: 1 <= Limb.max_uint32
constant radix : int = Limb.max_uint32 + 1
......@@ -109,6 +109,11 @@ module N
value_sub_concat x n i m;
value_sub_concat (Map.set x i v) n i m
let rec lemma value_zero (x:map int limb) (n m:int)
requires { MapEq.map_eq_sub x (Map.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 ()
(** {2 conversion from a small integer} *)
......@@ -121,6 +126,40 @@ module N
= { digits = Array31.make (Int31.of_int 1) n }
(** {2 copy, enlarge} *)
let copy (x:t) : t
ensures { value result = value x }
= let limb_zero = Limb.of_int 0 in
let zero = Int31.of_int 0 in
let lx = x.digits.length in
let r = Array31.make lx limb_zero in
Array31.blit x.digits zero r zero lx;
assert { MapEq.map_eq_sub x.digits.elts r.elts 0 (p2i lx) };
{ digits = r }
let enlarge (x:t) (l:int31) : unit
requires { p2i l > p2i x.digits.length }
writes { x }
ensures { x.digits.length = l }
ensures { MapEq.map_eq_sub x.digits.elts (Map.const Limb.zero_unsigned)
(p2i (old x).digits.length) (p2i l) }
ensures { value x = value (old x) }
= 'Init:
let limb_zero = Limb.of_int 0 in
let zero = Int31.of_int 0 in
let lx = x.digits.length in
let r = Array31.make l limb_zero in
assert { MapEq.map_eq_sub r.elts (Map.const limb_zero) (p2i lx) (p2i l) };
Array31.blit x.digits zero r zero lx;
assert { MapEq.map_eq_sub x.digits.elts r.elts 0 (p2i lx) };
assert { value_sub x.digits.elts 0 (p2i lx) = value (at x 'Init) };
assert { MapEq.map_eq_sub r.elts (Map.const limb_zero) (p2i lx) (p2i l) };
assert { value_sub r.elts (p2i lx) (p2i l) = 0 };
assert { value_sub r.elts 0 (p2i l) = value_sub r.elts 0 (p2i lx)
+ value_sub r.elts (p2i lx) (p2i l) * power radix (p2i lx) };
x.digits <- r
(** {2 Comparisons} *)
......@@ -189,9 +228,10 @@ module N
i := Int31.(-) !i one;
if Limb.ne x[!i] limb_zero then
begin
assert { l2i x[p2i !i] >= 1 };
assert { value_sub x.elts (p2i x1) (p2i !i + 1) >=
power radix (p2i !i - p2i x1) * l2i x[p2i !i] >=
power radix (p2i !i - p2i x1) };
power radix (p2i !i - p2i x1) * l2i x[p2i !i] };
assert { power radix (p2i !i - p2i x1) * l2i x[p2i !i] >= power radix (p2i !i - p2i x1) };
assert { value_sub x.elts (p2i x1) (p2i x2) = value_sub x.elts (p2i x1) (p2i !i + 1)
+ power radix (p2i !i + 1 - p2i x1) * value_sub x.elts (p2i !i + 1) (p2i x2)};
assert { value_sub x.elts (p2i x1) (p2i x2) >= power radix (p2i !i - p2i x1) };
......@@ -263,7 +303,7 @@ module N
x[j] = (at x 'Init)[j] }
invariant { p2i x1 <= p2i !i <= p2i x2 }
invariant {
value_array x + power radix (p2i !i) * l2i !c =
value_array x + power radix (p2i !i) * l2i !c =
value_array (at x 'Init) + power radix (p2i x1) * l2i y }
variant { p2i x2 - p2i !i }
let (r,c') = Limb.add_with_carry x[!i] limb_zero !c in
......@@ -320,6 +360,45 @@ module N
exception TooManyDigits
let add_aux_in_place (x:t) (y:array limb) : unit
requires { p2i x.digits.length >= p2i y.length }
(* what is the right clause ? writes { x, x.digits } *)
ensures { value x = value (old x) + value_array y }
raises { TooManyDigits -> true }
= 'Init:
let zero = Int31.of_int 0 in
let one = Int31.of_int 1 in
let limb_zero = Limb.of_int 0 in
let lx = x.digits.length in
let c = add_limbs x.digits y zero lx zero y.length in
assert {
value x + power radix (p2i lx) * l2i c =
value (at x 'Init) + value_array y };
if Limb.eq c limb_zero then () else
begin
(* we enlarge x *)
if Int31.eq lx (of_int 0x3FFFFFFF) then raise TooManyDigits;
'L:
enlarge x (Int31.(+) lx one);
(*
assert { MapEq.map_eq_sub x.digits.elts r.elts 0 (p2i lx) };
*)
assert { l2i x.digits[p2i lx] = 0 };
x.digits[lx] <- c;
assert { value x = value_array (at x.digits 'L) + power radix (p2i lx) * l2i c };
end
let add_in_place (x y:t) : unit
(* writes { x } *)
ensures { value x = value (old x) + value y }
raises { TooManyDigits -> true }
= let lx = x.digits.length in
let ly = y.digits.length in
if Int31.(<) lx ly then enlarge x ly;
add_aux_in_place x y.digits
let add_array (x y:array limb) : array limb
requires { p2i x.length >= p2i y.length }
ensures { value_array result = value_array x + value_array y }
......
......@@ -23,8 +23,6 @@ MAIN=main
GEN=map__Map mp__N
OBJ=$(GEN) parse
parse.cmo: mp__N.cmi
GENML = $(addsuffix .ml, $(GEN))
ML = $(addsuffix .ml, $(OBJ))
CMO = $(addsuffix .cmo, $(OBJ))
......@@ -36,6 +34,9 @@ all: $(MAIN).$(OCAMLBEST)
extract: $(GENML)
parse.cmo: mp__N.cmo
$(MAIN).byte: $(CMO) $(MAIN).cmo
ocamlc $(INCLUDE) $(BIGINTLIB).cma why3extract.cma -g -o $@ $^
......
......@@ -5,11 +5,11 @@
let compute_result text =
try
let a,i = Parse.parse_dec text 0 in
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 text i in
let c = Mp__N.add a b in
Parse.pr Format.str_formatter c;
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"
......
......@@ -13,15 +13,23 @@ let input =
open Mp__N
let input_num =
try let a,i = Parse.parse_dec input 0 in a
try let a,i = Parse.parse_dec_ip input 0 in a
with Parse.SyntaxError -> usage ()
let () =
Format.printf "zero : %a@." Parse.pr (zero ());
Format.printf "one : %a@." Parse.pr (from_limb 1L);
Format.printf "2^{32} : %a@." Parse.pr (from_limb 0x100000000L);
Format.printf "input : %a@." Parse.pr input_num;
let a = add input_num input_num in
Format.printf "times 2: %a@." Parse.pr a;
let a = add a input_num in
Format.printf "times 3: %a@." Parse.pr a
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
......@@ -5,8 +5,20 @@ 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
......@@ -29,6 +41,35 @@ let parse_dec s idx =
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
......@@ -41,13 +82,4 @@ let parse_sep_star s idx =
raise Exit
with Exit -> !i
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 "|%016LX" a.(i);
done;
fprintf fmt "|"
This diff is collapsed.
......@@ -113,6 +113,10 @@ module Unsigned
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 =
......
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