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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
(*
** A verfied implementation of the integer sqare root function
** that is non-tail-recursive and of logarithmic time complexity
**
** Author: Hongwei Xi
** Authoremail: hwxi AT cs DOT bu DOT edu
** Time: November, 2009
*)
(* ****** ****** *)
//
// The code is ported to ATS2 by Hongwei Xi on Friday, July 20, 2012
//
(* ****** ****** *)
staload _ = "prelude/DATS/integer.dats"
(* ****** ****** *)
propdef
ISQRT (x: int, n: int) =
[x0,x1:nat | x0 <= x; x < x1] (MUL (n, n, x0), MUL (n+1, n+1, x1))
// end of [SQRT]
extern
prfun ISQRT_4_lemma {x:nat} {n2:nat}
(pf: ISQRT (x/4, n2)): [n:int | 2*n2 <= n; n <= 2*n2+1] ISQRT (x, n)
// end of [ISQRT_4_lemma]
primplmnt
ISQRT_4_lemma // nonrec
{x} {n2} ([x0:int,x1:int] pf) = let
prval pf0 = pf.0 // MUL (n2, n2, x0) // x0 <= x/4
prval pf1 = pf.1 // MUL (n2+1, n2+1, x1) // x/4 < x1
prval pf1_alt = mul_expand_linear {1,1} {1,1} (pf0)
prval () = mul_isfun (pf1, pf1_alt)
stadef n_1 = n2 + n2
stadef n_2 = n_1 + 1 and n_3 = n_1 + 2
prval pf0_1 = mul_expand_linear {2,0} {2,0} (pf0)
stadef x_2 = 4 * x0 + 4 * n2 + 1
prval pf0_2 = mul_expand_linear {1,1} {1,1} (pf0_1)
prval pf0_3 = mul_expand_linear {1,2} {1,2} (pf0_1)
in
sif (x < x_2) then #[n_1 | (pf0_1, pf0_2)] else #[n_2 | (pf0_2, pf0_3)]
end // end of [ISORT_4_lemma]
(* ****** ****** *)
extern // 10 points
fun isqrt {x:nat}
(x: int x):<> [n:nat] (ISQRT (x, n) | int n)
// end of [isqrt]
implement isqrt (x) = let
//
fun aux {x:nat}.<x>. // non-tail-recursive
(x: int x):<> [n:nat] (ISQRT (x, n) | int n) =
if x > 0 then let
val x4 = x \ndiv 4
val [n2:int] (pf4 | n2) = aux (x4)
prval [n:int] pf = ISQRT_4_lemma {x} {n2} (pf4)
val n_1 = n2 + n2
val n_2 = n_1 + 1
val (pf_mul | x1) = g1int_mul2 (n_2, n_2)
in
if x < x1 then let
prval () = (
sif (n==2*n2) then () else let
prval () = mul_isfun (pf_mul, pf.0) in (*nothing*)
end // end of [sif]
) : [n==2*n2] void
in
(pf | n_1)
end else let
prval () = (
sif (n==2*n2+1) then () else let
prval () = mul_isfun (pf_mul, pf.1) in (*nothing*)
end // end of [sif]
) : [n==2*n2+1] void
in
(pf | n_2)
end // end of [if]
end else let
prval pf0_mul = mul_make {0,0} ()
prval pf1_mul = mul_make {1,1} ()
in
((pf0_mul, pf1_mul) | 0)
end // end of [if]
in
aux (x)
end // end of [isqrt]
(* ****** ****** *)
implement
main0 ((*void*)) =
{
val () = assertloc ( (isqrt(1023)).1 = 31 )
val () = assertloc ( (isqrt(1024)).1 = 32 )
val () = assertloc ( (isqrt(1025)).1 = 32 )
} // end of [main0]
(* ****** ****** *)
(* end of [isqrt.dats] *)
|
