diff --git a/examples/multiprecision/add.mlw b/examples/multiprecision/add.mlw index afd9114939c59ad8bad13d9545abae7ee743c6f2..c8a80dd5214d16eda71f99a0d37eae8f64f83418 100644 --- a/examples/multiprecision/add.mlw +++ b/examples/multiprecision/add.mlw @@ -48,20 +48,7 @@ module Add value_tail r !i; value_tail x !i; assert { value r (!i+1) + (power radix (!i+1)) * !c - = value x (!i+1) + y - (* by - value r !i + (power radix !i) * !c - = value r k + (power radix k) * res - + (power radix !i) * !c - = value r k + (power radix k) * res - + (power radix k) * radix * !c - = value r k + (power radix k) * (res + radix * !c) - = value r k + - (power radix k) * (!lx + (!c at StartLoop)) - = value r k + (power radix k) * (!c at StartLoop) - + (power radix k) * !lx - = value x k + y + (power radix k) * !lx - = value x !i + y*) }; + = value x (!i+1) + y }; i := Int32.(+) !i (Int32.of_int 1); done; if Int32.(=) !i sz then !c @@ -127,27 +114,7 @@ module Add value_tail x !i; value_tail y !i; assert { value r (!i+1) + (power radix (!i+1)) * !c = - value x (!i+1) + value y (!i+1) - (*by - value r !i + (power radix !i) * !c - = value r k + (power radix k) * res - + (power radix !i) * !c - = value r k + (power radix k) * res - + (power radix k) * radix * !c - = value r k + (power radix k) * (res + radix * !c) - = value r k + - (power radix k) * (!lx + !ly + (!c at StartLoop)) - = value r k + (power radix k) * (!c at StartLoop) - + (power radix k) * (!lx + !ly) - = value x k + value y k - + (power radix k) * (!lx + !ly) - = value x k + (power radix k) * !lx - + value y k + (power radix k) * !ly - = value x !i - + value y k + (power radix k) * !ly - = value x !i - + (value y k + (power radix k) * !ly) - = value x !i + value y !i*) }; + value x (!i+1) + value y (!i+1) }; i := Int32.(+) !i (Int32.of_int 1); done; !c @@ -192,27 +159,7 @@ module Add value_tail x !i; value_tail y !i; assert { value r (!i+1) + (power radix (!i+1)) * !c = - value x (!i+1) + value y (!i+1) - (*by - value r !i + (power radix !i) * !c - = value r k + (power radix k) * res - + (power radix !i) * !c - = value r k + (power radix k) * res - + (power radix k) * radix * !c - = value r k + (power radix k) * (res + radix * !c) - = value r k + - (power radix k) * (!lx + !ly + (!c at StartLoop)) - = value r k + (power radix k) * (!c at StartLoop) - + (power radix k) * (!lx + !ly) - = value x k + value y k - + (power radix k) * (!lx + !ly) - = value x k + (power radix k) * !lx - + value y k + (power radix k) * !ly - = value x !i - + value y k + (power radix k) * !ly - = value x !i - + (value y k + (power radix k) * !ly) - = value x !i + value y !i*) }; + value x (!i+1) + value y (!i+1) }; i := Int32.(+) !i (Int32.of_int 1); done; try @@ -235,22 +182,7 @@ module Add value_tail r !i; value_tail x !i; assert { value r (!i+1) + (power radix (!i+1)) * !c = - value x (!i+1) + value y sy - (*by - value r !i + (power radix !i) * !c - = value r k + (power radix k) * res - + (power radix !i) * !c - = value r k + (power radix k) * res - + (power radix k) * radix * !c - = value r k + (power radix k) * (res + radix * !c) - = value r k + - (power radix k) * (!lx + 0 + (!c at StartLoop2)) - = value r k + (power radix k) * (!c at StartLoop2) - + (power radix k) * !lx - = value x k + value y sy - + (power radix k) * !lx - = value x !i - + value y sy*) }; + value x (!i+1) + value y sy }; i := Int32.(+) !i (Int32.of_int 1); done; assert { !i = sx } @@ -272,17 +204,7 @@ module Add value_tail x !i; assert { value r !i = value x !i + value y sy }; (* true with this, should not be needed *) assert { value r (!i+1) + power radix (!i+1) * !c - = value x (!i+1) + value y sy - (* - by - value r !i + power radix !i * !c - = value r !i - = value r k + power radix k * !lx - so value x !i - = value x k + power radix k * !lx - so value r k - = value r k + power radix k * !c - = value x k + value y sy*) }; + = value x (!i+1) + value y sy }; i := Int32.(+) !i (Int32.of_int 1); done; !c @@ -332,28 +254,7 @@ module Add value_tail ox !i; value_tail y !i; assert { value x (!i+1) + (power radix (!i+1)) * !c = - value ox (!i+1) + value y (!i+1) - (*by value ox k + (power radix k) * !lx - = value ox !i - so value x !i + (power radix !i) * !c - = value x k + (power radix k) * res - + (power radix !i) * !c - = value x k + (power radix k) * res - + (power radix k) * radix * !c - = value x k + (power radix k) * (res + radix * !c) - = value x k + - (power radix k) * (!lx + !ly + (!c at StartLoop)) - = value x k + (power radix k) * (!c at StartLoop) - + (power radix k) * (!lx + !ly) - = value ox k + value y k - + (power radix k) * (!lx + !ly) - = (value ox k + (power radix k) * !lx) - + (value y k + (power radix k) * !ly) - = value ox !i - + (value y k + (power radix k) * !ly) - = value ox !i - + (value y k + (power radix k) * !ly) - = value ox !i + value y !i*) }; + value ox (!i+1) + value y (!i+1) }; i := Int32.(+) !i (Int32.of_int 1); done; try @@ -383,24 +284,7 @@ module Add value_tail ox !i; value_tail x !i; assert { value x (!i+1) + (power radix (!i+1)) * !c = - value ox (!i+1) + value y sy - (*by value ox k + (power radix k) * !lx - = value ox !i - so - value x !i + (power radix !i) * !c - = value x k + (power radix k) * res - + (power radix !i) * !c - = value x k + (power radix k) * res - + (power radix k) * radix * !c - = value x k + (power radix k) * (res + radix * !c) - = value x k + - (power radix k) * (!lx + 0 + (!c at StartLoop2)) - = value x k + (power radix k) * (!c at StartLoop2) - + (power radix k) * !lx - = value ox k + value y sy - + (power radix k) * !lx - = value ox !i - + value y sy*) }; + value ox (!i+1) + value y sy }; i := Int32.(+) !i (Int32.of_int 1); done; assert { !i = sx }; diff --git a/examples/multiprecision/div.mlw b/examples/multiprecision/div.mlw index 377ec0b3f042bacd0e75e6c3e5bbc480d4d5bfb0..e175faff5b658f228b67fc8ae6a5f9c68226e02e 100644 --- a/examples/multiprecision/div.mlw +++ b/examples/multiprecision/div.mlw @@ -455,57 +455,8 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb (q.offset + sz) }; (*nonlinear*) assert { mult * value_sub (pelts x) (x.offset + !i) (x.offset + sz) - = value_sub (pelts q) (q.offset + !i) (q.offset + sz) - * ry - + !r - (* by - (pelts q)[q.offset + k] = qu - so - (pelts x)[x.offset + k] = !lx - so - l + radix * h = !lx * mult - so - mult * value_sub (pelts x) (x.offset + !i + 1) - (x.offset + sz) - = mult * value_sub (pelts x) (x.offset + k) (x.offset + sz) - = mult * ((pelts x)[x.offset + k] - + radix * value_sub (pelts x) (x.offset + k + 1) - (x.offset + sz)) - = mult * !lx - + mult * radix * value_sub (pelts x) (x.offset + k + 1) - (x.offset + sz) - = l + radix * h - + mult * radix * value_sub (pelts x) (x.offset + k + 1) - (x.offset + sz) - = l + radix * h - + radix * (value_sub (pelts q) (q.offset + k + 1) - (q.offset + sz) - * ry - + (!r at StartLoop)) - = l + radix * h + radix * (!r at StartLoop) - + radix * (value_sub (pelts q) (q.offset + k + 1) - (q.offset + sz) - * ry) - = l + radix * (h + (!r at StartLoop)) - + radix * (value_sub (pelts q) (q.offset + k + 1) - (q.offset + sz) - * ry) - = qu * ry + !r - + radix * value_sub (pelts q) (q.offset + k + 1) - (q.offset + sz) - * ry - = (pelts q)[q.offset + k] * ry + !r - + radix * value_sub (pelts q) (q.offset + k + 1) - (q.offset + sz) - * ry - = ry * ((pelts q)[q.offset + k] - + radix * value_sub (pelts q) (q.offset + k + 1) - (q.offset + sz)) - + !r - = ry * value_sub (pelts q) (q.offset + !i + 1) - (q.offset + sz) - + !r *) - }; + = value_sub (pelts q) (q.offset + !i) (q.offset + sz) * ry + + !r }; i := Int32.(-) !i one; done; let ghost res = lsr !r (Limb.of_int32 clz) in @@ -624,8 +575,6 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb r1 := sub_mod um p; label CQuot in let ghost a = div (l2i um - l2i dh * l2i sh) radix in - (*assert { um - dh * sh = a * radix + !r1 - by !r1 = mod (um - dh * sh) radix };*) let tl, th = mul_double sh dl in let il, b = sub_with_borrow ul tl zero in let (ih, ghost b') = sub_with_borrow !r1 th b in @@ -1100,15 +1049,6 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb < radix * radix * radix } ensures { reciprocal_3by2 v dh dl } = () - (*let ghost d = dl + radix * dh in - let ghost w = Limb.of_int (div (radix*radix*radix -1) d - radix) in - assert { reciprocal_3by2 w dh dl }; - let ghost e = v - w in - assert { radix * radix * radix - d - <= (radix + w) * d - < radix * radix * radix }; - assert { e = 0 }*) - let reciprocal_word_3by2 (dh dl:limb) : limb requires { dh >= div radix 2 } @@ -1813,12 +1753,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb ((!qp).offset + sx - sy - !i) = value_sub (pelts q at QUp) (!qp.offset + 1) ((!qp).offset + sx - sy - !i) - = value (!qp at StartLoop) (sx - sy - k) - (* by offset !qp at StartLoop = (!qp).offset + 1 - so offset (!qp at StartLoop) + sx - sy - k - = (!qp).offset + sx - sy - !i - so map_eq_sub_shift (pelts q) (pelts !qp at StartLoop) - ((!qp).offset + 1) ((!qp).offset + 1) (sx + sy - k) *) }; + = value (!qp at StartLoop) (sx - sy - k) }; value_sub_head (pelts q) (!qp).offset ((!qp).offset + p2i sx - p2i sy - p2i !i); value_sub_tail (pelts x) x.offset (x.offset + p2i sy + p2i !i - 1); @@ -2290,51 +2225,6 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb assert { !ql * vy = !ql * vly + power radix (sy - 2) * (!ql * (dl + radix * dh)) }; (*nonlinear*) - (*assert { value (xd at SubProd) sy - + power radix sy * (!x1 at StartLoop) - - !ql * vy - = value xd (sy - 2) - - power radix (sy - 2) * cy - + power radix (sy - 2) * (rl + radix * rh) - by - value (xd at SubProd) sy - + power radix sy * (!x1 at StartLoop) - - !ql * vy - = vlx + power radix (sy - 2) - * (xp0 + radix * xp1) - + power radix sy * (!x1 at StartLoop) - - !ql * vy - = vlx + power radix (sy - 2) - * (xp0 + radix * xp1) - + power radix sy * (!x1 at StartLoop) - - !ql * (vly + power radix (sy - 2) - * (dl + radix * dh)) - = vlx - + power radix (sy - 2) - * (xp0 + radix * xp1 - + radix * radix * !x1 at StartLoop) - - !ql * (vly + power radix (sy - 2) - * (dl + radix * dh)) - = vlx - + power radix (sy - 2) - * (xp0 + radix * xp1 - + radix * radix * !x1 at StartLoop) - - !ql * vly - - power radix (sy - 2) - * !ql * (dl + radix * dh) - = vlx - !ql * vly - + power radix (sy - 2) - * (xp0 + radix * xp1 - + radix * radix * !x1 at StartLoop - - !ql * (dl + radix * dh)) - = vlx - !ql * vly - + power radix (sy - 2) * - (rl + radix * rh) - = value xd (sy - 2) - - power radix (sy - 2) * cy - + power radix (sy - 2) * - (rl + radix * rh) - } *) end; begin ensures { value xd (sy - 2) - power radix (sy - 2) * cy @@ -2372,72 +2262,6 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb = !x0 - radix * cy1) else cy1 = 0 /\ rl - cy = l2i !x0)) } (* nonlinear *) - (* refl example *) - (* assert { value xd (sy - 2) - - power radix (sy - 2) * cy - + power radix (sy - 2) * - (rl + radix * rh) - = value xd (sy - 1) - + power radix (sy - 1) * !x1 - - power radix sy * cy2 - by - (rl + radix * rh - cy - = !x0 + radix * !x1 - radix * radix * cy2 - by - (!x0 - radix * cy1 = rl - cy - by - !x0 = mod (rl - cy) radix - so - radix < rl - cy < radix - so (if rl < cy - then cy1 = 1 - /\ (- radix < rl - cy < 0 - so - div (rl - cy) radix = - 1 - so rl - cy - = radix * div (rl - cy) radix - + mod (rl - cy) radix - = !x0 - radix - = !x0 - radix * cy1) - else cy1 = 0 /\ rl - cy = l2i !x0) - ) - so !x1 - radix * cy2 = rh - cy1 - so radix * !x1 - radix * radix * cy2 - = radix * rh - radix * cy1 - so radix * rh - = radix * cy1 - + radix * !x1 - radix * radix * cy2 - so rl + radix * rh - cy - = rl - cy + radix * rh - = !x0 - radix * cy1 + radix * rh - = !x0 - radix * cy1 - + radix * cy1 - + radix * !x1 - radix * radix * cy2 - = !x0 + radix * !x1 - radix * radix * cy2 - ) - so - ( - power radix (sy - 2) * cy - + power radix (sy - 2) * (rl + radix * rh) - = power radix (sy - 2) - * (rl + radix * rh - cy) - = power radix (sy - 2) - * (!x0 + radix * !x1 - radix * radix * cy2) - = power radix (sy - 2) * !x0 - + power radix (sy - 1) * !x1 - - power radix sy * cy2 - by power radix (sy - 2) * radix = power radix (sy - 1) - so power radix (sy - 2) * radix * radix = power radix sy - ) - so value xd (sy - 2) - - power radix (sy - 2) * cy - + power radix (sy - 2) * (rl + radix * rh) - = value xd (sy - 2) - + power radix (sy - 2) * !x0 - + power radix (sy - 1) * !x1 - - power radix sy * cy2 - = value xd (sy - 1) - + power radix (sy - 1) * !x1 - - power radix sy * cy2 - }*) end; end; if [@ex:unlikely] (not (Limb.(=) cy2 limb_zero)) @@ -3064,201 +2888,7 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb + qh * power radix (sx - sy - !i)) * vy * power radix !i + value x (sy + !i - 1) - + power radix (sy + !i - 1) * !x1 - (*by - value !qp (sx - sy - !i) - = !ql + radix * - value_sub (pelts q) ((!qp).offset + 1) - ((!qp).offset + sx - sy - !i) - so (value_sub (pelts q) ((!qp).offset + 1) - ((!qp).offset + sx - sy - !i) - = value (!qp at StartLoop) - (sx - sy - k) - by - (!qp at StartLoop).offset = (!qp).offset + 1 - so ((!qp).offset + sx - sy - !i) - - ((!qp).offset + 1) - = sx - sy - k - ) - so value !qp (sx - sy - !i) - = !ql + radix * value (!qp at StartLoop) - (sx - sy - k) - so (value x s - = value x !i - + power radix !i - * value xd (sy - 1) - by - xd.offset = x.offset + !i - so x.offset + s = xd.offset + sy - 1 - so pelts x = pelts xd - so x.offset + s - xd.offset = sy - 1 - so value_sub (pelts x) xd.offset (x.offset + s) - = value xd (sy - 1) - so value x s - = value_sub (pelts x) x.offset xd.offset - + power radix !i * value_sub (pelts x) xd.offset (x.offset + s) - = value x !i - + power radix !i * value xd (sy - 1) - ) - so (power radix s - = power radix !i * power radix (sy - 1) - by - let n = !i in - let m = sy - 1 in - let x = radix in - power x s = power x (n + m) - so (power x (n + m) = power x n * power x m - by 0 <= n - so 0 <= m - so forall x:int, n:int, m:int. - 0 <= n -> 0 <= m -> power x (n + m) = (power x n * power x m))) - so (value x s + power radix s * !x1 - = value x !i - + power radix !i * - (value (xd at SubProd) sy - + power radix sy * (!x1 at StartLoop) - - !ql * vy) - by - cy2 = 0 - so value xd (sy - 1) - + power radix (sy - 1) * !x1 - = value (xd at SubProd) sy - + power radix sy * (!x1 at StartLoop) - - !ql * vy - so value x s + power radix s * !x1 - = value x !i - + power radix !i - * value xd (sy - 1) - + power radix (!i + sy - 1) * !x1 - = value x !i - + power radix !i - * value xd (sy - 1) - + power radix !i - * power radix (sy - 1) * !x1 - = value x !i - + power radix !i * - (value xd (sy - 1) - + power radix (sy - 1) * !x1) - = value x !i - + power radix !i * - (value (xd at SubProd) sy - + power radix sy * (!x1 at StartLoop) - - !ql * vy) - ) - so (value (x at StartLoop) (sy + k - 1) - = value (x at SubProd) !i - + power radix !i - * value (xd at SubProd) sy - by - value (x at StartLoop) (sy + k - 1) - = value_sub (pelts x at SubProd) (x at SubProd).offset - ((x at SubProd).offset + sy + k - 1) - = value_sub (pelts x at SubProd) (x at SubProd).offset xd.offset - + power radix (xd.offset - (x at SubProd).offset) - * value_sub (pelts x at SubProd) xd.offset - ((x at SubProd).offset + sy + k - 1) - so (x at SubProd).offset = x.offset - so xd.offset = x.offset + !i - so value_sub (pelts x at SubProd) (x at SubProd).offset xd.offset - = value (x at SubProd) !i - so power radix (xd.offset - x.offset) = power radix !i - so x.offset + sy + k - 1 - xd.offset = p2i sy - so value_sub (pelts x at SubProd) xd.offset - (x.offset + sy + k - 1) - = value (xd at SubProd) sy - ) - so (value x !i - = value (x at SubProd) !i - ) - so power radix !i * power radix sy = power radix (!i + sy) - so value x s + power radix s * !x1 - - value (x at StartLoop) (sy + k - 1) - = value x !i - + power radix !i * - (value (xd at SubProd) sy - + power radix sy * (!x1 at StartLoop) - - !ql * vy) - - (value (x at SubProd) !i - + power radix !i - * value (xd at SubProd) sy) - = value x !i - + power radix !i * - (value (xd at SubProd) sy - + power radix sy * (!x1 at StartLoop) - - !ql * vy) - - (value x !i - + power radix !i - * value (xd at SubProd) sy) - = power radix !i - * (power radix sy * (!x1 at StartLoop) - - !ql * vy) - = power radix !i * power radix sy * (!x1 at StartLoop) - - power radix !i * !ql * vy - = power radix (!i + sy) * (!x1 at StartLoop) - - power radix !i * !ql * vy - = power radix (sy + k - 1) * (!x1 at StartLoop) - - power radix !i * !ql * vy - so value x s + power radix s * !x1 - = value (x at StartLoop) (sy + k - 1) - + power radix (sy + k - 1) * (!x1 at StartLoop) - - power radix !i * !ql * vy - so power radix (sx - sy - !i) - = radix * power radix (sx - sy - k) - so radix * power radix !i = power radix k - so (value !qp (sx - sy - !i) - + qh * power radix (sx - sy - !i)) - * vy * power radix !i - + value x (sy + !i - 1) - + power radix (sy + !i - 1) * !x1 - = (!ql + radix * value (!qp at StartLoop) - (sx - sy - k) - + qh * power radix (sx - sy - !i)) - * vy * power radix !i - + value x (sy + !i - 1) - + power radix (sy + !i - 1) * !x1 - = (!ql + radix * value (!qp at StartLoop) - (sx - sy - k) - + qh * radix * power radix (sx - sy - k)) - * vy * power radix !i - + value x (sy + !i - 1) - + power radix (sy + !i - 1) * !x1 - = !ql * vy * power radix !i - + (value (!qp at StartLoop) - (sx - sy - k) - + qh * power radix (sx - sy - k)) - * vy * radix * power radix !i - + value x (sy + !i - 1) - + power radix (sy + !i - 1) * !x1 - = !ql * vy * power radix !i - + (value (!qp at StartLoop) - (sx - sy - k) - + qh * power radix (sx - sy - k)) - * vy * power radix k - + value x (sy + !i - 1) - + power radix (sy + !i - 1) * !x1 - = !ql * vy * power radix !i - + (value (!qp at StartLoop) - (sx - sy - k) - + qh * power radix (sx - sy - k)) - * vy * power radix k - + value x s - + power radix s * !x1 - = !ql * vy * power radix !i - + (value (!qp at StartLoop) - (sx - sy - k) - + qh * power radix (sx - sy - k)) - * vy * power radix k - + value (x at StartLoop) (sy + k - 1) - + power radix (sy + k - 1) * (!x1 at StartLoop) - - power radix !i * !ql * vy - = (value (!qp at StartLoop) - (sx - sy - k) - + qh * power radix (sx - sy - k)) - * vy * power radix k - + value (x at StartLoop) (sy + k - 1) - + power radix (sy + k - 1) * (!x1 at StartLoop) - = value (old x) sx *) - }; + + power radix (sy + !i - 1) * !x1 }; value_sub_tail (pelts y) y.offset (y.offset + p2i sy - 1); value_sub_tail (pelts y) y.offset (y.offset + p2i sy - 2); let ghost vly = value y (p2i sy - 2) in @@ -3719,9 +3349,6 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb /\ (pelts x)[x.offset + 1] = !rh}; !qh - -(* val sub_limb_in_place (x:t) (y:limb) (sz:int32) : limb*) - (** `div_qr q r x y sx sy` divides `(x, sx)` by `(y, sy)`, writes the quotient in `(q, (sx-sy))` and the remainder in `(r, sy)`. Corresponds to `mpn_tdiv_qr`. *) @@ -4356,57 +3983,6 @@ let divmod_1 (q x:t) (y:limb) (sz:int32) : limb () end end - (* else begin - let dn = Int32.(+) !qn one in - let dqn = Int32.(+) !qn !qn in - let ign = Int32.(-) sy dn in - let ix = C.incr nx (Int32.(-) sx dqn) in - let iy = C.incr y ign in - let clz = clz_ext (C.get_ofs y (Int32.(-) sy one)) in - (*let ghost p = power 2 (p2i clz) in*) - (if Int32.(=) clz zero - then begin - copy nx x sx; - C.set_ofs nx sx limb_zero; - ( - if (Int32.(=) dn two) - then - let _d1 = divmod_2 q ix iy (Int32.(+) dqn one) in () - else - let _s1 = div_sb_qr q ix iy (Int32.(+) dqn one) dn in () - ) - end - else begin - let _ = lshift ny y sy (Limb.of_int32 clz) in - let h = lshift nx x sx (Limb.of_int32 clz) in - C.set_ofs nx sx h; - begin - if (Int32.(=) dn two) - then - let _d2 = divmod_2 q ix (incr ny ign) (Int32.(+) dqn one) in () - else - let _s2 = div_sb_qr q ix (incr ny ign) (Int32.(+) dqn one) dn in () - end - end); - (* we have an estimated q, adjust by at most 1 *) - let dl = ref limb_zero in - let st = Int32.(-) sy one in - let snx = Int32.(+) sx one in - let tp = C.malloc (UInt32.of_int32 st) in - mul tp q ny !qn ign; - let b = sub_in_place nx tp snx st in - (if Limb.(>) b limb_zero - then (* quotient too large *) - let _s = sub_limb_in_place q (Limb.of_int 1) (!qn) in - let _a = add_in_place nx ny snx sy in - () - else ()); - if Int32.(=) clz zero - then begin copy r nx sy end - else let _r = rshift r nx sy (Limb.of_int32 clz) in (); - C.free tp; - () - end*) let tdiv_qr (q r x y:t) (sx sy:int32) : unit requires { 1 <= sy <= sx <= (Int32.max_int32 - 1) } diff --git a/examples/multiprecision/logical.mlw b/examples/multiprecision/logical.mlw index 14e90b661259d0326d79d4ac0b6d61699a171372..fe224f74e830cf72f99f832bb3e4b00a6629b37c 100644 --- a/examples/multiprecision/logical.mlw +++ b/examples/multiprecision/logical.mlw @@ -314,52 +314,7 @@ module Logical (*nonlinear part*) assert { retval + radix * (value r (!i+1) + (power radix (!i+1)) * !low) - = value x (!i+2) * c - (* by - (pelts r)[r.offset + k] - = (pelts r)[(!rp.offset at StartLoop)] - = (!low at StartLoop) + l - so - !high = (pelts x)[(!xp).offset] - so - retval + radix * (value r !i - + (power radix !i) * !low) - = retval + radix * (value r k - + power radix k * (pelts r)[r.offset+k] - + power radix !i * !low) - = retval + radix * (value r k - + power radix k * ((!low at StartLoop) + l) - + power radix !i * !low) - = retval + radix * (value r k - + power radix k * (!low at StartLoop) - + power radix k * l - + power radix !i * !low) - = retval + radix * (value r k - + power radix k * (!low at StartLoop)) - + radix * (power radix k * l - + power radix !i * !low) - = value x (k+1) * power 2 (tnc) - + radix * (power radix k * l - + power radix !i * !low) - = value x !i * power 2 (tnc) - + radix * (power radix k * l - + power radix !i * !low) - = value x !i * power 2 (tnc) - + radix * (power radix k * l - + power radix k * radix * !low) - = value x !i * power 2 (tnc) - + radix * (power radix k * (l + radix * !low)) - = value x !i * power 2 (tnc) - + radix * (power radix k * !high * power 2 (tnc)) - = value x !i * power 2 (tnc) - + power radix !i * !high * power 2 (tnc) - = (value x !i + power radix !i * !high) - * power 2 (tnc) - = (value x !i - + power radix !i * (pelts x)[x.offset + !i]) - * power 2 (tnc) - = value x (1 + !i) * power 2 (tnc) *) - }; + = value x (!i+2) * c }; i := Int32.(+) !i one; rp.contents <- C.incr !rp one; done; diff --git a/examples/multiprecision/mul.mlw b/examples/multiprecision/mul.mlw index d770b2110568babb98d7492b24158dc4fb85d0f9..536f190b406aa9ce890169191ad8a86661c3f28b 100644 --- a/examples/multiprecision/mul.mlw +++ b/examples/multiprecision/mul.mlw @@ -65,28 +65,7 @@ module Mul = value x !i * y + power radix !i * (!lx * y) }; (*nonlinear, needed for reflection*) assert { value r (!i+1) + (power radix (!i+1)) * !c = - value x (!i+1) * y - (* by - value r !i + !c * (power radix !i) - = value r k + res * (power radix k) - + (power radix !i) * !c - = value r k + (power radix k) * res - + (power radix k) * radix * !c - = value r k + (power radix k) * (res + radix * !c) - = value r k + (power radix k) * - (res + radix * (rh + carry)) - = value r k + (power radix k) * - (res + radix * carry + radix * rh) - = value r k + (power radix k) * - ((!c at StartLoop) + rl + radix*rh) - = value r k + (power radix k) * - ((!c at StartLoop) + !lx * y) - = value r k + (power radix k) * (!c at StartLoop) - + (power radix k) * !lx * y - = value x k * y + (power radix k) * !lx * y - = (value x k + (power radix k) * !lx) * y - = value x !i * y *) - }; + value x (!i+1) * y }; i := Int32.(+) !i (Int32.of_int 1); done; !c @@ -164,52 +143,7 @@ module Mul (* nonlinear part *) assert { value r (!i+1) + (power radix (!i+1)) * !c = value (old r) (!i+1) - + value x (!i+1) * y - (* by - (value r !i + (power radix !i) * !c - = value (r at StartLoop) !i + - (power radix k) * (res - !lr) - + (power radix !i) * !c - = value (r at StartLoop) !i + - (power radix k) * (res - !lr) - + (power radix !i) * (rh + carry) - = value (r at StartLoop) !i + - (power radix k) * (res - !lr) - + (power radix k) * radix * (rh + carry) - = value (r at StartLoop) !i + - (power radix k) * (res - !lr - + radix * (rh + carry)) - = value (r at StartLoop) !i + - (power radix k) * (res + radix * carry - - !lr + radix * rh) - = value (r at StartLoop) !i + - (power radix k) * (rl + !lr + (!c at StartLoop) - - !lr + radix * rh) - = value (r at StartLoop) !i + - (power radix k) * (rl + radix * rh + (!c at StartLoop)) - = value (r at StartLoop) !i + - (power radix k) * (!lx * y + (!c at StartLoop)) - = value (r at StartLoop) k - + (power radix k) * !lr - + (power radix k) * (!lx * y + (!c at StartLoop)) - = value (r at StartLoop) k - + (power radix k) * (!c at StartLoop) - + (power radix k) * (!lx * y + !lr) - = value (old r) k - + value x k * y - + (power radix k) * (!lx * y + !lr) - = value (old r) k - + (power radix k) * !lr - + (value x k + (power radix k)* (!lx)) * y - = value (old r) !i - + (value x k + (power radix k)* (!lx)) * y - = value (old r) !i - + value x !i * y - by - value (old r) !i = value (old r) k - + (power radix k) * (!lr) - ) *) - }; + + value x (!i+1) * y }; i := Int32.(+) !i (Int32.of_int 1); done; !c @@ -370,108 +304,7 @@ module Mul assert { value r (!i + sz + 1) + (power radix (!i + sz + 1)) * !c = value (old r) (!i + sz + 1) - + value x sz - * value y (!i + 1) - (*by - power radix (k + sz) = power radix k * power radix sz - so - power radix (!i + sz) = power radix k * power radix sz * radix - so - value (r at StartLoop) k - + (power radix k) * value_sub (pelts r at StartLoop) - (r.offset + k) (r.offset + k + sz) - = value (r at StartLoop) (k + sz) - so (value (old r) (!i+sz) - = value (old r) (k+sz) - + power radix (k+sz) * !lr - by !lr = (pelts (old r))[r.offset + k + sz]) - so - value !rp sz + (power radix sz) * c' = - value (!rp at StartLoop) sz - + value x sz * !ly - so - value r (!i + sz) - + (power radix (!i + sz)) * !c - = value r (k + sz) - + (power radix (k + sz)) * res - + (power radix (!i + sz)) * !c - = value r k - + (power radix k) * value !rp sz - + (power radix (k + sz)) * res - + (power radix (!i + sz)) * !c - = value r k - + (power radix k) * value !rp sz - + (power radix k) * (power radix sz) * res - + (power radix (!i + sz)) * !c - = value r k - + (power radix k) * value !rp sz - + (power radix k) * (power radix sz) * res - + (power radix k) * (power radix sz) * radix * !c - = value r k - + (power radix k) * value !rp sz - + (power radix k) * (power radix sz) - * (res + radix * !c) - = value r k - + (power radix k) * value !rp sz - + (power radix k) * (power radix sz) - * (c' + (!c at StartLoop) + !lr) - = value r k + (power radix k) - * (value !rp sz - + power radix sz * (c'+ (!c at StartLoop) + !lr)) - = value r k + (power radix k) - * (value !rp sz - + power radix sz * c' - + power radix sz * ((!c at StartLoop) + !lr)) - = value r k + (power radix k) - * (value (!rp at StartLoop) sz - + value x sz * !ly - + (power radix sz) * ((!c at StartLoop) + !lr)) - = value r k - + power radix k * (value (!rp at StartLoop) sz) - + power radix k * (value x sz * !ly - + (power radix sz) * ((!c at StartLoop) + !lr)) - = value (r at StartLoop) k - + power radix k * (value (!rp at StartLoop) sz) - + power radix k * (value x sz * !ly - + (power radix sz) * ((!c at StartLoop) + !lr)) - = value (r at StartLoop) k - + power radix k * (value_sub (pelts r at StartLoop) (r.offset+k) - (r.offset+k+ sz)) - + power radix k * (value x sz * !ly - + (power radix sz) * ((!c at StartLoop) + !lr)) - = value (r at StartLoop) (k + sz) - + power radix k * (value x sz * !ly - + (power radix sz) * ((!c at StartLoop) + !lr)) - = value (r at StartLoop) (k + sz) - + power radix k * value x sz * !ly - + power radix k * power radix sz * ((!c at StartLoop) + !lr) - = value (r at StartLoop) (k + sz) - + power radix k * power radix sz * ((!c at StartLoop) + !lr) - + power radix k * value x sz * !ly - = value (r at StartLoop) (k + sz) - + power radix (k + sz) * ((!c at StartLoop) + !lr) - + power radix k * value x sz * !ly - = value (r at StartLoop) (k + sz) - + power radix (k + sz) * ((!c at StartLoop)) - + power radix (k + sz) * !lr - + power radix k * value x sz * !ly - = value (old r) (k+sz) - + value x sz * value y k - + power radix (k + sz) * !lr - + power radix k * value x sz * !ly - = value (old r) (k+sz) - + power radix (k + sz) * !lr - + value x sz * value y k - + power radix k * value x sz * !ly - = value (old r) (k+sz) - + power radix (k + sz) * !lr - + value x sz * (value y k + power radix k * !ly) - = value (old r) (k+sz) - + power radix (k + sz) * !lr - + value x sz * value y !i - = value (old r) (!i +sz) - + value x sz * value y !i *) - }; + + value x sz * value y (!i + 1) }; i := Int32.(+) !i one; rp.contents <- C.incr !rp one; assert { forall j. (!rp).offset + sz <= j -> @@ -549,51 +382,7 @@ module Mul = value x sx * value y !i + power radix !i * (value x sx * !ly) }; (*nonlinear*) - assert { value r (!i + sx + 1) = value x sx * value y (!i+1) - (*by (value !rp sx + power radix sx * res - = value (!rp at StartLoop) sx + value x sx * !ly - by value !rp sx = value (!rp at BeforeCarry) sx) - so power radix (k + sx) = power radix k * power radix sx - so - value (r at StartLoop) k - + (power radix k) * value_sub (pelts r at StartLoop) - (r.offset + k) (r.offset + k + sx) - = value (r at StartLoop) (k + sx) - so - value r (!i + sx) - = value r (k + sx) - + (power radix (k + sx)) * res - = value r k - + (power radix k) * value !rp sx - + (power radix (k + sx)) * res - = value r k - + (power radix k) * value !rp sx - + (power radix k) * (power radix sx) * res - = value r k - + (power radix k) * value !rp sx - + (power radix k) * (power radix sx) * res - = value r k - + (power radix k) * (value !rp sx + (power radix sx) * res) - = value r k + (power radix k) - * (value (!rp at StartLoop) sx - + value x sx * !ly) - = value r k - + power radix k * (value (!rp at StartLoop) sx) - + power radix k * (value x sx * !ly) - = value (r at StartLoop) k - + power radix k * (value (!rp at StartLoop) sx) - + power radix k * (value x sx * !ly) - = value (r at StartLoop) k - + power radix k * (value_sub (pelts r at StartLoop) (r.offset+k) - (r.offset+k+ sx)) - + power radix k * (value x sx * !ly) - = value (r at StartLoop) (k + sx) - + power radix k * (value x sx * !ly) - = value x sx * value y k - + power radix k * value x sx * !ly - = value x sx * - (value y k + power radix k * !ly) - = value x sx * value y !i *) }; + assert { value r (!i + sx + 1) = value x sx * value y (!i+1) }; i := Int32.(+) !i one; rp.contents <- C.incr !rp one; done; diff --git a/examples/multiprecision/sub.mlw b/examples/multiprecision/sub.mlw index 4b87de6b7ad0198b48ae789da5df99760ce95649..996eea0ee1087d69ffb5e29e6d4d20bca1f9c6be 100644 --- a/examples/multiprecision/sub.mlw +++ b/examples/multiprecision/sub.mlw @@ -48,21 +48,7 @@ module Sub value_tail r !i; value_tail x !i; assert { value r (!i+1) - power radix (!i+1) * !b - = value x (!i+1) - y - (*by - value r !i - power radix !i * !b - = value r k + power radix k * res - - power radix !i * !b - = value r k + power radix k * res - - power radix k * radix * !b - = value r k + power radix k * (res - radix * !b) - = value r k + - (power radix k) * (!lx - (!b at StartLoop)) - = value r k - power radix k * (!b at StartLoop) - + power radix k * !lx - = value x k - y + power radix k * !lx - = value x !i - y*) - }; + = value x (!i+1) - y }; i := Int32.(+) !i (Int32.of_int 1); done; if Int32.(=) !i sz then !b @@ -126,29 +112,7 @@ module Sub value_tail x !i; value_tail y !i; assert { value r (!i+1) - (power radix (!i+1)) * !b - = value x (!i+1) - value y (!i+1) - (*by - value r !i - power radix !i * !b - = value r k + power radix k * res - - power radix !i * !b - = value r k + power radix k * res - - power radix k * radix * !b - = value r k - + power radix k * (res - radix * !b) - = value r k - + power radix k * (!lx - !ly - (!b at StartLoop)) - = value r k - power radix k * (!b at StartLoop) - + power radix k * (!lx - !ly) - = value x k - value y k - + power radix k * (!lx - !ly) - = value x k - value y k - + power radix k * !lx - power radix k * !ly - = value x k + power radix k * !lx - - (value y k + power radix k * !ly) - = value x !i - - (value y k + power radix k * !ly) - = value x !i - value y !i*) - }; + = value x (!i+1) - value y (!i+1) }; i := Int32.(+) !i (Int32.of_int 1); done; !b @@ -194,26 +158,7 @@ module Sub value_tail x !i; value_tail y !i; assert { value r (!i+1) - power radix (!i+1) * !b = - value x (!i+1) - value y (!i+1) - (*by - value r !i - power radix !i * !b - = value r k + power radix k * res - - power radix !i * !b - = value r k + power radix k * res - - (power radix k) * radix * !b - = value r k - + power radix k * (res - radix * !b) - = value r k - + power radix k * (!lx - !ly - (!b at StartLoop)) - = value r k - (power radix k) * (!b at StartLoop) - + power radix k * (!lx - !ly) - = value x k - value y k - + power radix k * (!lx - !ly) - = value x k + power radix k * !lx - - value y k - power radix k * !ly - = value x !i - - (value y k + power radix k * !ly) - = value x !i - value y !i*) }; + value x (!i+1) - value y (!i+1) }; i := Int32.(+) !i one; done; try @@ -236,22 +181,7 @@ module Sub value_tail r !i; value_tail x !i; assert { value r (!i+1) - power radix (!i+1) * !b = - value x (!i+1) - value y sy - (*by - value r !i - power radix !i * !b - = value r k + power radix k * res - - (power radix !i) * !b - = value r k + power radix k * res - - (power radix k) * radix * !b - = value r k + power radix k * (res - radix * !b) - = value r k - + power radix k * (!lx - 0 - (!b at StartLoop2)) - = value r k - (power radix k) * (!b at StartLoop2) - + (power radix k) * !lx - = value x k - value y sy - + (power radix k) * !lx - = value x !i - - value y sy*) }; + value x (!i+1) - value y sy }; i := Int32.(+) !i one; done; assert { !i = sx } @@ -273,17 +203,7 @@ module Sub value_tail x !i; assert { value r !i = value x !i - value y sy }; assert { value r (!i+1) - power radix (!i+1) * !b - = value x (!i+1) - value y sy - (*by - value r !i + power radix !i * !b - = value r !i - = value r k + power radix k * !lx - so value x !i - = value x k + power radix k * !lx - so value r k - = value r k + power radix k * !b - = value x k - value y sy*) - }; + = value x (!i+1) - value y sy }; i := Int32.(+) !i (Int32.of_int 1); done; !b @@ -334,25 +254,7 @@ module Sub value_tail x !i; value_tail y !i; assert { value x (!i+1) - power radix (!i+1) * !b = - value ox (!i+1) - value y (!i+1) - (*by value x !i - power radix !i * !b - = value x k + power radix k * res - - power radix !i * !b - = value x k + power radix k * res - - (power radix k) * radix * !b - = value x k - + power radix k * (res - radix * !b) - = value x k - + power radix k * (!lx - !ly - (!b at StartLoop)) - = value x k - (power radix k) * (!b at StartLoop) - + power radix k * (!lx - !ly) - = value ox k - value y k - + power radix k * (!lx - !ly) - = value ox k + power radix k * !lx - - value y k - power radix k * !ly - = value ox !i - - (value y k + power radix k * !ly) - = value ox !i - value y !i*) }; + value ox (!i+1) - value y (!i+1) }; i := Int32.(+) !i one; done; try @@ -382,22 +284,7 @@ module Sub value_tail ox !i; value_tail x !i; assert { value x (!i+1) - power radix (!i+1) * !b = - value ox (!i+1) - value y sy - (*by - value x !i - power radix !i * !b - = value x k + power radix k * res - - (power radix !i) * !b - = value x k + power radix k * res - - (power radix k) * radix * !b - = value x k + power radix k * (res - radix * !b) - = value x k - + power radix k * (!lx - 0 - (!b at StartLoop2)) - = value x k - (power radix k) * (!b at StartLoop2) - + (power radix k) * !lx - = value ox k - value y sy - + (power radix k) * !lx - = value ox !i - - value y sy*) }; + value ox (!i+1) - value y sy }; i := Int32.(+) !i one; done; assert { !i = sx };