1load "wordsLib";
2
3val field_neg_def = 
4 Define
5   `field_neg (x:word32) = if x = 0w then (0w:word32) else 751w - x`;
6
7val field_add_def =
8 Define
9  `field_add (x:word32,y:word32) =
10     let z = x + y 
11      in 
12       if z < 751w then z else z - 751w`;
13
14val field_sub_def =
15 Define
16  `field_sub (x,y) = field_add(x,field_neg y)`;
17
18val field_mult_aux_def = 
19 Define 
20  `field_mult_aux (x:word32,y:word32,acc:word32) =
21      if y = 0w then acc 
22      else let 
23        x' = field_add (x,x) in let 
24        y' = y >>> 1         in let 
25        acc' = (if y && 1w = 0w then acc else field_add (acc,x))
26        in
27          field_mult_aux (x',y',acc')`;
28
29val field_mult_def = 
30 Define
31  `field_mult (x,y) = field_mult_aux (x,y,0w)`;
32
33val field_exp_aux_def = 
34 Define
35  `field_exp_aux (x:word32,n:word32,acc:word32) =
36      if n = 0w then acc
37      else
38       let x' = field_mult (x,x) in
39       let n' = n >>> 1 in
40       let acc' = (if n && 1w = 0w then acc else field_mult (acc,x))
41        in
42          field_exp_aux (x',n',acc')`;
43
44val field_exp_def = 
45 Define
46  `field_exp (x,n) = field_exp_aux (x,n,1w)`;
47
48val field_inv_def =
49 Define 
50  `field_inv x = field_exp (x,749w)`;
51
52val field_div_def = 
53 Define
54  `field_div (x,y) = field_mult (x,field_inv y)`;
55
56val curve_neg_def = 
57 Define
58  `curve_neg (x1,y1) =
59       if (x1 = 0w) /\ (y1 = 0w) then (0w,0w)
60       else
61        let y = field_sub
62                  (field_sub
63                    (field_neg y1,field_mult (0w,x1)),1w)
64         in
65            (x1,y)`;
66
67val curve_double_def = 
68 Define
69  `curve_double (x1,y1) =
70      if (x1 = 0w) /\ (y1 = 0w) then (0w,0w)
71      else
72       let d = field_add
73                 (field_add
74                   (field_mult (2w,y1),
75                    field_mult (0w,x1)),1w)
76       in
77        if d = 0w then (0w,0w)
78        else
79         let l = field_div
80                  (field_sub
81                    (field_add
82                      (field_add
83                        (field_mult(3w,field_exp (x1,2w)),
84                         field_mult(field_mult (2w,0w),x1)),750w),
85                       field_mult (0w,y1)),d) in
86         let m = field_div
87                  (field_sub
88                    (field_add
89                      (field_add
90                           (field_neg (field_exp (x1,3w)),
91                            field_mult (750w,x1)),
92                       field_mult (2w,0w)),
93                     field_mult (1w,y1)),d) in
94         let x = field_sub
95                  (field_sub
96                    (field_add(field_exp (l,2w),
97                                   field_mult (0w,l)),0w),
98                     field_mult (2w,x1)) in
99         let y = field_sub
100                  (field_sub
101                     (field_mult
102                       (field_neg (field_add (l,0w)),x),m),1w)
103         in
104           (x,y)`;
105
106
107val curve_add_def = 
108 Define
109  `curve_add (x1,y1,x2,y2) =
110       if (x1 = x2) /\ (y1 = y2) then curve_double (x2,y2) else 
111       if (x1 = 0w) /\ (y1 = 0w) then (x2,y2) else
112       if (x2 = 0w) /\ (y2 = 0w) then (x1,y1) else
113       if x1 = x2 then (0w,0w)
114       else
115         let d = field_sub (x2,x1) in
116         let l = field_div (field_sub (y2,y1),d) in
117         let m = field_div
118                   (field_sub (field_mult (y1,x2),
119                                   field_mult (y2,x1)),d) in
120         let x = field_sub
121                  (field_sub
122                    (field_sub
123                      (field_add
124                        (field_exp (l,2w),
125                         field_mult (0w,l)),0w),x1),x2) in
126         let y = field_sub
127                  (field_sub
128                    (field_mult
129                      (field_neg (field_add (l,0w)),x),m),1w)
130         in
131          (x,y)`;
132
133val curve_mult_aux_def = 
134 Define
135  `curve_mult_aux (x,y,n:word32,acc_x,acc_y) =
136      if n = 0w then (acc_x:word32,acc_y:word32)
137      else
138       let (x',y') = curve_double (x,y) in
139       let n' = n >>> 1 in
140       let (acc_x',acc_y') =
141              (if n && 1w = 0w then (acc_x,acc_y)
142               else curve_add (x,y,acc_x,acc_y))
143       in
144        curve_mult_aux (x',y',n',acc_x',acc_y')`;
145
146val curve_mult_def = 
147 Define
148  `curve_mult (x,y,n) = curve_mult_aux (x,y,n,0w,0w)`;
149
150(*---------------------------------------------------------------------------*)
151(* The following re-definition are derived from running the compiler on      *)
152(* the original defns and allocating registers.                              *)
153(* All except for curve_mult_aux, which tickles a bug in the register        *)
154(* allocator.                                                                *)
155(*---------------------------------------------------------------------------*)
156
157val field_neg_def = 
158 Define
159  `field_neg (r0:word32) =
160    let r0 = (if r0 = 0w then 0w else (let r0 = 751w - r0 in r0)) 
161    in r0`;
162
163val field_add_def = 
164 Define 
165   `field_add(r0:word32,r1:word32) =
166      let r0 = r1 + r0 in let 
167          r0 = if r0 < 751w then r0 else (let r0 = r0 - 751w in r0)
168      in
169        r0`;
170
171val field_sub_def = 
172 Define
173   `field_sub (r0,r1) =
174      let r1 = field_neg r1 in let 
175          r0 = field_add (r0,r1) in r0`;
176
177val field_mult_aux_def =
178 Define
179   `field_mult_aux(r0:word32,r1:word32,r2:word32) =
180      let r0 = (if r1 = 0w then r2
181                else
182                 let r3 = field_add (r0,r0) in
183                 let r4 = r1 >>> 1 in
184                 let r1 = r1 && 1w in
185                 let r0 = (if r1 = 0w then r2
186                           else (let r0 = field_add (r2,r0) in r0)) in
187                 let r0 = field_mult_aux (r3,r4,r0) 
188                 in r0)
189      in
190         r0`;
191
192val field_mult_aux_ind = fetch "-" "field_mult_aux_ind";
193
194val field_mult_def = 
195 Define
196   `field_mult(r0,r1) = let r0 = field_mult_aux (r0,r1,0w) in r0`;
197
198val field_exp_aux_def = 
199 Define 
200   `field_exp_aux(r0:word32,r1:word32,r2:word32) =
201      let r0 = (if r1 = 0w then r2
202                else
203                  let r3 = field_mult (r0,r0) in
204                  let r4 = r1 >>> 1 in
205                  let r1 = r1 && 1w in
206                  let r0 = (if r1 = 0w then r2
207                             else (let r0 = field_mult (r2,r0) in r0)) in
208                  let r0 = field_exp_aux (r3,r4,r0) 
209                   in r0)
210       in
211         r0`;
212
213val field_exp_aux_ind = fetch "-" "field_exp_aux_ind";
214
215
216val field_exp_def = 
217 Define
218   `field_exp(r0,r1) = let r0 = field_exp_aux (r0,r1,1w) in r0`;
219
220val field_inv_def = 
221 Define
222   `field_inv r0 = let r0 = field_exp (r0,749w) in r0`;
223
224val field_div_def = 
225 Define
226  `field_div (r0,r1) =
227     let r1 = field_inv r1 in let 
228         r0 = field_mult (r0,r1) 
229     in r0`;
230
231val curve_neg_def =
232 Define
233  `curve_neg (r0,r1) =
234     let r2 = field_neg r1 in
235     let r3 = field_mult (0w,r0) in
236     let r2 = field_sub (r2,r3) in
237     let r2 = field_sub (r2,1w) in
238     let (r0,r1) =
239           (if r0 = 0w then
240               (let (r0,r1) = if r1 = 0w then (0w,0w) else (0w,r2) 
241                in (r0,r1))
242            else(r0,r2))
243     in
244       (r0,r1)`;
245
246val curve_double_def =
247 Define
248   `curve_double(r0,r1) =
249      let r2 = field_mult (2w,r1) in
250      let r3 = field_mult (0w,r0) in
251      let r2 = field_add (r2,r3) in
252      let r2 = field_add (r2,1w) in
253      let (r2,r3) =
254        (if r2 = 0w then(0w,0w)
255         else
256          let r3 = field_exp (r0,2w) in
257          let r3 = field_mult (3w,r3) in
258          let r4 = field_mult (2w,0w) in
259          let r4 = field_mult (r4,r0) in
260          let r3 = field_add (r3,r4) in
261          let r3 = field_add (r3,750w) in
262          let r4 = field_mult (0w,r1) in
263          let r3 = field_sub (r3,r4) in
264          let r3 = field_div (r3,r2) in
265          let r4 = field_exp (r0,3w) in
266          let r4 = field_neg r4 in
267          let r5 = field_mult (750w,r0) in
268          let r4 = field_add (r4,r5) in
269          let r5 = field_mult (2w,0w) in
270          let r4 = field_add (r4,r5) in
271          let r5 = field_mult (1w,r1) in
272          let r4 = field_sub (r4,r5) in
273          let r2 = field_div (r4,r2) in
274          let r4 = field_exp (r3,2w) in
275          let r5 = field_mult (0w,r3) in
276          let r4 = field_add (r4,r5) in
277          let r4 = field_sub (r4,0w) in
278          let r5 = field_mult (2w,r0) in
279          let r4 = field_sub (r4,r5) in
280          let r3 = field_add (r3,0w) in
281          let r3 = field_neg r3 in
282          let r3 = field_mult (r3,r4) in
283          let r2 = field_sub (r3,r2) in
284          let r2 = field_sub (r2,1w) 
285           in (r4,r2)) in
286      let (r0,r1) =
287          (if r0 = 0w then
288                (let (r0,r1) = if r1 = 0w then (0w,0w) else (r2,r3) 
289                 in (r0,r1))
290           else (r2,r3))
291      in
292       (r0,r1)`;
293
294val curve_add_def = 
295 Define
296  `curve_add(r0,r1,r2,r3) =
297     let (r4,r5) =
298           (if r0 = r2 then (0w,0w)
299            else
300              let r4 = field_sub (r2,r0) in
301              let r5 = field_sub (r3,r1) in
302              let r5 = field_div (r5,r4) in
303              let r6 = field_mult (r1,r2) in
304              let r7 = field_mult (r3,r0) in
305              let r6 = field_sub (r6,r7) in
306              let r4 = field_div (r6,r4) in
307              let r6 = field_exp (r5,2w) in
308              let r7 = field_mult (0w,r5) in
309              let r6 = field_add (r6,r7) in
310              let r6 = field_sub (r6,0w) in
311              let r6 = field_sub (r6,r0) in
312              let r6 = field_sub (r6,r2) in
313              let r5 = field_add (r5,0w) in
314              let r5 = field_neg r5 in
315              let r5 = field_mult (r5,r6) in
316              let r4 = field_sub (r5,r4) in
317              let r4 = field_sub (r4,1w) 
318               in
319                 (r6,r4)) in
320     let (r4,r5) =
321          if r2 = 0w then
322             let (r4,r5) = if r3 = 0w then (r0,r1) else (r4,r5) 
323             in (r4,r5)
324          else (r4,r5) in
325     let (r4,r5) =
326          if r0 = 0w then
327              (let (r4,r5) = if r1 = 0w then (r2,r3) else (r4,r5)
328               in  (r4,r5))
329          else (r4,r5) in
330     let (r0,r1) =
331          if r0 = r2 then
332              (let (r0,r1) =
333                  (if r1 = r3 then
334                      (let (r0,r1) = curve_double (r2,r3) 
335                       in (r0,r1))
336                   else (r4,r5))
337               in (r0,r1))
338          else (r4,r5)
339     in
340       (r0,r1)`;
341
342val curve_mult_aux_def = Define `
343  curve_mult_aux (r0,r1,r2,r3,r4) =
344       let (r0,r1) =
345          (if r2 = 0w then (r3,r4)
346           else
347               (let (r5,r6) = curve_double (r0,r1)
348                in
349                  let r7 = r2 >>> 1 in
350                  let r2 = r2 && 1w in
351                  let (r0,r1) =
352                    (if r2 = 0w then (r3,r4)
353                     else
354                       (let (r0,r1) = curve_add (r0,r1,r3,r4) in (r0,r1)))
355 	          in
356                    let (r0,r1) = curve_mult_aux (r5,r6,r7,r0,r1) in
357                    (r0,r1)))
358        in
359        (r0,r1)`;
360
361val curve_mult_def = Define `
362  curve_mult (r0,r1,r2) =
363      let (r0,r1) = curve_mult_aux (r0,r1,r2,0w,0w)
364      in 
365      (r0,r1)`;
366