1(*---------------------------------------------------------------------------*)
2(* Elliptic curve algorithms brought over from                               *)
3(*                                                                           *)
4(*    HOLDIR/examples/elliptic/spec/elliptic_exampleScript.sml               *)
5(*                                                                           *)
6(*---------------------------------------------------------------------------*)
7
8use "prelim";
9
10val field_neg_def = 
11 Define
12   `field_neg (x:word32) = if x = 0w then (0w:word32) else 751w - x`;
13
14val field_add_def =
15 Define
16  `field_add (x:word32,y:word32) =
17     let z = x + y 
18      in 
19       if z < 751w then z else z - 751w`;
20
21val field_sub_def =
22 Define
23  `field_sub (x,y) = field_add(x,field_neg y)`;
24
25val field_mult_aux_def = 
26 Define 
27   `field_mult_aux (x:word32,y:word32,acc:word32) =
28      if y = 0w then acc 
29      else let 
30        x' = field_add (x,x) in let 
31        y' = y >>> 1         in let 
32        acc' = (if y && 1w = 0w then acc else field_add (acc,x))
33        in
34          field_mult_aux (x',y',acc')`;
35
36val field_mult_def = 
37 Define
38   `field_mult (x,y) = field_mult_aux (x,y,0w)`;
39
40val field_exp_aux_def = 
41 Define
42   `field_exp_aux (x:word32,n:word32,acc:word32) =
43      if n = 0w then acc
44      else
45       let x' = field_mult (x,x) in
46       let n' = n >>> 1 in
47       let acc' = (if n && 1w = 0w then acc else field_mult (acc,x))
48        in
49          field_exp_aux (x',n',acc')`;
50
51val field_exp_def = 
52 Define
53   `field_exp (x,n) = field_exp_aux (x,n,1w)`;
54
55val field_inv_def =
56 Define 
57   `field_inv x = field_exp (x,749w)`;
58
59val field_div_def = 
60 Define
61   `field_div (x,y) = field_mult (x,field_inv y)`;
62
63val curve_neg_def = 
64 Define
65   `curve_neg (x1,y1) =
66       if (x1 = 0w) /\ (y1 = 0w) then (0w,0w)
67       else
68        let y = field_sub
69                  (field_sub
70                    (field_neg y1,field_mult (0w,x1)),1w)
71         in
72            (x1,y)`;
73
74val curve_double_def = 
75 Define
76   `curve_double (x1,y1) =
77      if (x1 = 0w) /\ (y1 = 0w) then (0w,0w)
78      else
79       let d = field_add
80                 (field_add
81                   (field_mult (2w,y1),
82                    field_mult (0w,x1)),1w)
83       in
84        if d = 0w then (0w,0w)
85        else
86         let l = field_div
87                  (field_sub
88                    (field_add
89                      (field_add
90                        (field_mult(3w,field_exp (x1,2w)),
91                         field_mult(field_mult (2w,0w),x1)),750w),
92                       field_mult (0w,y1)),d) in
93         let m = field_div
94                  (field_sub
95                    (field_add
96                      (field_add
97                           (field_neg (field_exp (x1,3w)),
98                            field_mult (750w,x1)),
99                       field_mult (2w,0w)),
100                     field_mult (1w,y1)),d) in
101         let x = field_sub
102                  (field_sub
103                    (field_add(field_exp (l,2w),
104                                   field_mult (0w,l)),0w),
105                     field_mult (2w,x1)) in
106         let y = field_sub
107                  (field_sub
108                     (field_mult
109                       (field_neg (field_add (l,0w)),x),m),1w)
110         in
111           (x,y)`;
112
113
114val curve_add_def = 
115 Define
116   `curve_add (x1,y1,x2,y2) =
117       if (x1 = x2) /\ (y1 = y2) then curve_double (x2,y2) else 
118       if (x1 = 0w) /\ (y1 = 0w) then (x2,y2) else
119       if (x2 = 0w) /\ (y2 = 0w) then (x1,y1) else
120       if x1 = x2 then (0w,0w)
121       else
122         let d = field_sub (x2,x1) in
123         let l = field_div (field_sub (y2,y1),d) in
124         let m = field_div
125                   (field_sub (field_mult (y1,x2),
126                                   field_mult (y2,x1)),d) in
127         let x = field_sub
128                  (field_sub
129                    (field_sub
130                      (field_add
131                        (field_exp (l,2w),
132                         field_mult (0w,l)),0w),x1),x2) in
133         let y = field_sub
134                  (field_sub
135                    (field_mult
136                      (field_neg (field_add (l,0w)),x),m),1w)
137         in
138          (x,y)`;
139
140val curve_mult_aux_def = 
141 Define
142   `curve_mult_aux (x,y,n:word32,acc_x,acc_y) =
143      if n = 0w then (acc_x:word32,acc_y:word32)
144      else
145       let (x',y') = curve_double (x,y) in
146       let n' = n >>> 1 in
147       let (acc_x',acc_y') =
148              (if n && 1w = 0w then (acc_x,acc_y)
149               else curve_add (x,y,acc_x,acc_y))
150       in
151        curve_mult_aux (x',y',n',acc_x',acc_y')`;
152
153val curve_mult_def = 
154 Define
155   `curve_mult (x,y,n) = curve_mult_aux (x,y,n,0w,0w)`;
156
157(* Following definitions need further massaging to be compilable:
158
159val field_exp_aux_def = 
160 Define
161   `elgamal_encrypt (m_x,m_y,k) =
162       let (a_x,a_y) = curve_mult (361w,383w,k) in
163       let (t_x,t_y) =
164                 curve_mult
165                   (FST
166                      (affine_case (curve (GF 751) 0 0 1 750 0) (0w,0w)
167                         (\x y. (n2w x,n2w y))
168                         (curve_mult (curve (GF 751) 0 0 1 750 0)
169                            (affine (GF 751) [361; 383]) 91)),
170                    SND
171                      (affine_case (curve (GF 751) 0 0 1 750 0) (0w,0w)
172                         (\x y. (n2w x,n2w y))
173                         (curve_mult (curve (GF 751) 0 0 1 750 0)
174                            (affine (GF 751) [361; 383]) 91)),k) in
175       let (b_x,b_y) = curve_add (t_x,t_y,m_x,m_y) 
176       in
177         (a_x,a_y,b_x,b_y)`;
178
179
180val field_exp_aux_def = 
181 Define
182   `elgamal_decrypt (a_x,a_y,b_x,b_y) =
183       let (t_x,t_y) = curve_neg (curve_mult (a_x,b_x,91w)) 
184        in
185          curve_add (t_x,t_y,b_x,b_y)`;
186
187*)
188
189
190(*---------------------------------------------------------------------------*)
191(* Compile the functions.                                                    *)
192(*---------------------------------------------------------------------------*)
193(*
194val fns = [field_neg_def, field_add_def, field_sub_def, 
195          field_mult_aux_def, field_mult_def, 
196          field_exp_aux_def, field_exp_def, 
197          field_inv_def, field_div_def, curve_neg_def, 
198          curve_double_def, curve_add_def, 
199          curve_mult_aux_def, curve_mult_def];
200
201compile1 fns;
202compile2 fns;  (* takes a long time on curve_double *)
203compile3 fns;
204compile4 fns;
205compile4a fns;
206compile5 fns;
207
208*)
209