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