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