1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
(* ========================================================================= *)
(* The Bernstein-Yang "divstep" iteration for gcd, modular inverse etc. *)
(* https://gcd.cr.yp.to/safegcd-20190413.pdf *)
(* ========================================================================= *)
needs "Library/iter.ml";;
needs "Library/integer.ml";;
needs "Library/floor.ml";;
(* ------------------------------------------------------------------------- *)
(* Explicit divstep function *)
(* ------------------------------------------------------------------------- *)
loadt "Divstep/divstep.ml";;
(* ------------------------------------------------------------------------- *)
(* Integer-scaled version. *)
(* ------------------------------------------------------------------------- *)
loadt "Divstep/idivstep.ml";;
(* ------------------------------------------------------------------------- *)
(* Convex hull reasoning to prove the bounds. *)
(* ------------------------------------------------------------------------- *)
loadt "Divstep/hull_light.ml";;
(* ------------------------------------------------------------------------- *)
(* Connecting the two things. *)
(* ------------------------------------------------------------------------- *)
loadt "Divstep/divstep_bounds.ml";;
|
