Commit cc8215e3 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Remove large comments in multiprecision

parent f04adefa
......@@ -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 };
......
This diff is collapsed.
......@@ -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;
......
This diff is collapsed.
......@@ -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 };
......
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