Commit 700b3079 authored by MARCHE Claude's avatar MARCHE Claude

mp: prepare for multiplication

parent bb11ac5a
......@@ -46,13 +46,22 @@ module mach.int.UInt32
syntax val (>=) "(>=)"
syntax val (>) "(>)"
(* direct realization of add_with_carry.
Remind that parameters x y and c are assumed to denote unsigned integers
(* direct realization of add_with_carry, mul_with_carry, fused_mul_add.
Remember 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))"
syntax val mul_with_carry "(fun x y ->
let r = Int64.mul x y in
(Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))"
syntax val fused_mul_add "(fun x y c ->
let r = Int64.add (Int64.mul x y) c in
(Int64.logand r 0xFFFFFFFFL,Int64.shift_right_logical r 32))"
end
module mach.int.Int63
......
......@@ -20,7 +20,9 @@ module N
these are represented by an array of "limbs". A limb is expected to
be a machine word, abstractly it can be any unsigned integer type
*)
(* does not allow extraction...
(*i FIXME: does not allow extraction...
type limb
clone mach.int.Unsigned as Limb
......@@ -32,7 +34,7 @@ module N
*)
(* temporary: stick to uint32 *)
(*i temporary: stick to uint32 *)
use mach.int.UInt32 as Limb
......@@ -44,7 +46,6 @@ module N
(**)
function l2i (x:limb) : int = Limb.to_int x
function p2i (i:int31) : int = Int31.to_int i
......@@ -362,7 +363,7 @@ module N
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 } *)
writes { x.digits, x.digits.elts }
ensures { value x = value (old x) + value_array y }
raises { TooManyDigits -> true }
= 'Init:
......@@ -380,16 +381,13 @@ module N
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 } *)
writes { x.digits, x.digits.elts }
ensures { value x = value (old x) + value y }
raises { TooManyDigits -> true }
= let lx = x.digits.length in
......@@ -436,7 +434,7 @@ end
(* does not work as expected
(*i does not work as expected
module N64
use import mach.int.Int64
......
......@@ -122,6 +122,16 @@ module Unsigned
to_int r + (max+1) * to_int d =
to_int x + to_int y + to_int c }
val mul_with_carry (x y:t) : (t,t)
returns { (r,d) ->
to_int r + (max+1) * to_int d =
to_int x * to_int y + to_int c }
val fused_mul_add (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
......
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