1(* ========================================================================= *) 2(* Create "elliptic_exampleTheory" compiling elliptic curve operations. *) 3(* ========================================================================= *) 4 5(* ------------------------------------------------------------------------- *) 6(* Load and open relevant theories. *) 7(* (Comment out "load"s and "quietdec"s for compilation.) *) 8(* ------------------------------------------------------------------------- *) 9(* 10val () = loadPath := [] @ !loadPath; 11val () = app load ["bossLib", "metisLib", "wordsLib", 12 "primalityTools", "ellipticTools"]; 13val () = quietdec := true; 14*) 15 16open HolKernel Parse boolLib bossLib metisLib 17 arithmeticTheory pred_setTheory wordsTheory 18 primalityTools 19 groupTheory groupTools 20 fieldTheory fieldTools 21 ellipticTheory ellipticTools; 22 23(* 24val () = quietdec := false; 25*) 26 27(* ------------------------------------------------------------------------- *) 28(* Start a new theory. *) 29(* ------------------------------------------------------------------------- *) 30 31val _ = new_theory "elliptic_example"; 32 33(* ------------------------------------------------------------------------- *) 34(* Sort out the parser. *) 35(* ------------------------------------------------------------------------- *) 36 37val () = Parse.add_infix ("/", 600, HOLgrammars.LEFT); 38 39(* ------------------------------------------------------------------------- *) 40(* The subtype context. *) 41(* ------------------------------------------------------------------------- *) 42 43val context = elliptic_context; 44val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 45 46(* ------------------------------------------------------------------------- *) 47(* Helper proof tools. *) 48(* ------------------------------------------------------------------------- *) 49 50infixr 0 << 51infixr 1 ++ || THENC ORELSEC 52infix 2 >> 53 54val op ++ = op THEN; 55val op << = op THENL; 56val op >> = op THEN1; 57val op || = op ORELSE; 58val Know = Q_TAC KNOW_TAC; 59val Suff = Q_TAC SUFF_TAC; 60 61(* ------------------------------------------------------------------------- *) 62(* Extensions to HOL theories to define the ex_ constants. *) 63(* ------------------------------------------------------------------------- *) 64 65 66(* ========================================================================= *) 67(* Smallest elliptic curve example to be compiled. *) 68(* ========================================================================= *) 69 70(* ------------------------------------------------------------------------- *) 71(* First define the parameters for the example using HOL types. *) 72(* ------------------------------------------------------------------------- *) 73 74val example1_prime_def = Define `example1_prime = 751`; 75 76val example1_field_def = Define `example1_field = GF example1_prime`; 77 78val example1_curve_def = Define 79 `example1_curve = curve example1_field 0 0 1 (example1_prime - 1) 0`; 80 81val example1_elgamal_g_def = Define 82 `example1_elgamal_g = affine example1_field [361; 383]`; 83 84val example1_elgamal_x_def = Define `example1_elgamal_x = 91`; 85 86val example1_elgamal_h_def = Define 87 `example1_elgamal_h = 88 curve_mult example1_curve example1_elgamal_g example1_elgamal_x`; 89 90val example1_prime = Count.apply prove 91 (``example1_prime IN Prime``, 92 RW_TAC alg_ss [example1_prime_def, Prime_def, GSPECIFICATION] 93 ++ CONV_TAC prime_checker_conv); 94 95val context = subtypeTools.add_reduction2 example1_prime context; 96val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 97 98val example1_field = prove 99 (``example1_field IN Field``, 100 RW_TAC alg_ss [example1_field_def]); 101 102val context = subtypeTools.add_reduction2 example1_field context; 103val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 104 105val example1_curve = prove 106 (``example1_curve IN Curve``, 107 RW_TAC alg_ss [example1_curve_def, Curve_def, GSPECIFICATION] 108 ++ RW_TAC alg_ss [example1_field_def, example1_prime_def] 109 ++ RW_TAC alg_ss [non_singular_def, LET_DEF, discriminant_def] 110 ++ RW_TAC alg_ss 111 [LET_DEF, GF_alt, curve_b2_def, curve_b4_def, 112 curve_b6_def, curve_b8_def, field_exp_small] 113 ++ CONV_TAC EVAL); 114 115val context = subtypeTools.add_reduction2 example1_curve context; 116val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 117 118val example1_curve_field = prove 119 (``example1_curve.field = example1_field``, 120 RW_TAC alg_ss [example1_curve_def]); 121 122(*** Need to reduce elgamal_h before anything happens 123val example1_elgamal_h_alt = 124 SIMP_CONV 125 (simpLib.++ (alg_ss,numSimps.SUC_FILTER_ss)) 126 [curve_mult_def, 127 example1_elgamal_g_def, 128 example1_elgamal_x_def, 129 example1_elgamal_h_def] 130 ``example1_elgamal_h``; 131***) 132 133(* ------------------------------------------------------------------------- *) 134(* Converting HOL types to words. *) 135(* ------------------------------------------------------------------------- *) 136 137val ex1_prime_def = Define `ex1_prime : word32 = n2w example1_prime`; 138 139val ex1_field_elt_def = Define 140 `ex1_field_elt (n : num) : word32 = n2w n`; 141 142val ex1_field_num_def = Define 143 `ex1_field_num (n : num) : word32 = ex1_field_elt (n MOD example1_prime)`; 144 145val ex1_curve_point_def = Define 146 `ex1_curve_point = 147 affine_case example1_curve 148 (0w,0w) (\x y. (ex1_field_elt x, ex1_field_elt y))`; 149 150val ex1_elgamal_g_x = Define 151 `ex1_elgamal_g_x = FST (ex1_curve_point example1_elgamal_g)`; 152 153val ex1_elgamal_g_y = Define 154 `ex1_elgamal_g_y = SND (ex1_curve_point example1_elgamal_g)`; 155 156val ex1_elgamal_h_x = Define 157 `ex1_elgamal_h_x = FST (ex1_curve_point example1_elgamal_h)`; 158 159val ex1_elgamal_h_y = Define 160 `ex1_elgamal_h_y = SND (ex1_curve_point example1_elgamal_h)`; 161 162val ex1_elgamal_x = Define `ex1_elgamal_x = n2w example1_elgamal_x`; 163 164(* ------------------------------------------------------------------------- *) 165(* Representing GF(p) field elements with words. *) 166(* ------------------------------------------------------------------------- *) 167 168val ex1_field_zero_def = Define 169 `ex1_field_zero = ex1_field_num 0`; 170 171val ex1_field_neg_def = Define 172 `ex1_field_neg (x : word32) = 173 if x = 0w then 0w else ex1_prime - x`; 174 175val ex1_field_add_def = Define 176 `ex1_field_add (x : word32, y : word32) = 177 let z = x + y in 178 if z < ex1_prime then z else z - ex1_prime`; 179 180val ex1_field_sub_def = Define 181 `ex1_field_sub (x : word32, y : word32) = 182 ex1_field_add (x, ex1_field_neg y)`; 183 184val ex1_field_mult_aux_def = 185 Define 186 `ex1_field_mult_aux (x : word32, y : word32, acc : word32) = 187 if y = 0w then acc 188 else 189 let x' = ex1_field_add (x,x) in 190 let y' = y >>> 1 in 191 let acc' = if y && 1w = 0w then acc else ex1_field_add (acc,x) 192 in 193 ex1_field_mult_aux (x',y',acc')`; 194 195 196val ex1_field_mult_def = Define 197 `ex1_field_mult (x : word32, y : word32) = ex1_field_mult_aux (x,y,0w)`; 198 199val ex1_field_exp_aux_def = 200 Define 201 `ex1_field_exp_aux (x : word32, n : word32, acc : word32) = 202 if n = 0w then acc 203 else 204 let x' = ex1_field_mult (x,x) in 205 let n' = n >>> 1 in 206 let acc' = if n && 1w = 0w then acc else ex1_field_mult (acc,x) 207 in ex1_field_exp_aux (x',n',acc')`; 208 209val ex1_field_exp_def = Define 210 `ex1_field_exp (x : word32, n : word32) = ex1_field_exp_aux (x,n,1w)`; 211 212val ex1_field_inv_def = Define 213 `ex1_field_inv (x : word32) = ex1_field_exp (x, n2w (example1_prime - 2))`; 214 215val ex1_field_div_def = Define 216 `ex1_field_div (x:word32, y:word32) = ex1_field_mult (x, ex1_field_inv y)`; 217 218(* ------------------------------------------------------------------------- *) 219(* Elliptic curve operations in terms of the above field operations. *) 220(* ------------------------------------------------------------------------- *) 221 222val ex1_curve_zero_def = Define 223 `ex1_curve_zero = ex1_curve_point (curve_zero example1_curve)`; 224 225val ex1_curve_neg_def = Define 226 `ex1_curve_neg (x1,y1) = 227 let $~ = ex1_field_neg in 228 let $- = CURRY ex1_field_sub in 229 let $* = CURRY ex1_field_mult in 230 let a1 = ex1_field_elt example1_curve.a1 in 231 let a3 = ex1_field_elt example1_curve.a3 232 in 233 if (x1,y1) = ex1_curve_zero 234 then ex1_curve_zero 235 else let x = x1 in 236 let y = ~y1 - a1 * x1 - a3 237 in (x,y)`; 238 239val ex1_curve_double_def = Define 240 `ex1_curve_double (x1,y1) = 241 let $& = ex1_field_num in 242 let $~ = ex1_field_neg in 243 let $+ = CURRY ex1_field_add in 244 let $- = CURRY ex1_field_sub in 245 let $* = CURRY ex1_field_mult in 246 let $/ = CURRY ex1_field_div in 247 let $** = CURRY ex1_field_exp in 248 let a1 = ex1_field_elt example1_curve.a1 in 249 let a2 = ex1_field_elt example1_curve.a2 in 250 let a3 = ex1_field_elt example1_curve.a3 in 251 let a4 = ex1_field_elt example1_curve.a4 in 252 let a6 = ex1_field_elt example1_curve.a6 253 in 254 if (x1,y1) = ex1_curve_zero then ex1_curve_zero 255 else 256 let d = & 2 * y1 + a1 * x1 + a3 257 in if d = ex1_field_zero then ex1_curve_zero 258 else 259 let l = (& 3 * x1 ** 2w + & 2 * a2 * x1 + a4 - a1 * y1) / d in 260 let m = (~(x1 ** 3w) + a4 * x1 + & 2 * a6 - a3 * y1) / d in 261 let x = l ** 2w + a1 * l - a2 - &2 * x1 in 262 let y = ~(l + a1) * x - m - a3 263 in (x,y)`; 264 265val ex1_curve_add_def = Define 266 `ex1_curve_add (x1,y1,x2,y2) = 267 if (x1 = x2) /\ (y1 = y2) then ex1_curve_double (x1,y1) 268 else 269 let $& = ex1_field_num in 270 let $~ = ex1_field_neg in 271 let $+ = CURRY ex1_field_add in 272 let $- = CURRY ex1_field_sub in 273 let $* = CURRY ex1_field_mult in 274 let $/ = CURRY ex1_field_div in 275 let $** = CURRY ex1_field_exp in 276 let a1 = ex1_field_elt example1_curve.a1 in 277 let a2 = ex1_field_elt example1_curve.a2 in 278 let a3 = ex1_field_elt example1_curve.a3 in 279 let a4 = ex1_field_elt example1_curve.a4 in 280 let a6 = ex1_field_elt example1_curve.a6 in 281 if (x1,y1) = ex1_curve_zero then (x2,y2) 282 else if (x2,y2) = ex1_curve_zero then (x1,y1) 283 else if x1 = x2 then ex1_curve_zero 284 else 285 let d = x2 - x1 in 286 let l = (y2 - y1) / d in 287 let m = (y1 * x2 - y2 * x1) / d in 288 let x = l ** 2w + a1 * l - a2 - x1 - x2 in 289 let y = ~(l + a1) * x - m - a3 in 290 (x,y)`; 291 292val ex1_curve_mult_aux_def = 293 tDefine "ex1_curve_mult_aux" 294 `ex1_curve_mult_aux (x : word32, y : word32, n : word32, 295 acc_x : word32, acc_y : word32) = 296 if n = 0w then (acc_x,acc_y) 297 else 298 let (x',y') = ex1_curve_double (x,y) in 299 let n' = n >>> 1 in 300 let (acc_x',acc_y') = 301 if n && 1w = 0w then (acc_x,acc_y) 302 else ex1_curve_add (x,y,acc_x,acc_y) 303 in 304 ex1_curve_mult_aux (x',y',n',acc_x',acc_y')` 305 (WF_REL_TAC `measure (w2n o FST o SND o SND)` 306 THEN SRW_TAC [] [wordsTheory.LSR_LESS] 307 THEN pairLib.GEN_BETA_TAC 308 THEN SRW_TAC [] [wordsTheory.LSR_LESS]); 309 310val ex1_curve_mult_def = 311 Define 312 `ex1_curve_mult (x:word32, y:word32, n:word32) 313 = ex1_curve_mult_aux (x,y,n,0w,0w)`; 314 315(* ------------------------------------------------------------------------- *) 316(* Elliptic curve encryption and decryption functions. *) 317(* These form the API, and need to be compiled. *) 318(* ------------------------------------------------------------------------- *) 319 320val ex1_elgamal_encrypt_def = Define 321 `ex1_elgamal_encrypt (m_x : word32, m_y : word32, k : word32) = 322 let (a_x,a_y) = ex1_curve_mult (ex1_elgamal_g_x,ex1_elgamal_g_y,k) in 323 let (t_x,t_y) = ex1_curve_mult (ex1_elgamal_h_x,ex1_elgamal_h_y,k) in 324 let (b_x,b_y) = ex1_curve_add (t_x,t_y,m_x,m_y) in 325 (a_x,a_y,b_x,b_y)`; 326 327val ex1_elgamal_decrypt_def = Define 328 `ex1_elgamal_decrypt (a_x,a_y,b_x,b_y) = 329 let (t_x,t_y) = ex1_curve_neg (ex1_curve_mult (a_x,b_x,ex1_elgamal_x)) in 330 ex1_curve_add (t_x,t_y,b_x,b_y)`; 331 332(* ------------------------------------------------------------------------- *) 333(* The first stage of compiling is to propagate all constants, especially to *) 334(* eliminate HOL types that are not just tuples of word32s. *) 335(* ------------------------------------------------------------------------- *) 336 337local 338 val is_word_tuple = 339 let 340 fun f ty = 341 if wordsSyntax.is_word_type ty then () 342 else let val (x,y) = pairLib.dest_prod ty in f x; f y end 343 in 344 can f 345 end; 346 347 fun blocked (f,x) = 348 is_word_tuple (type_of x) andalso 349 not (is_var x) andalso 350 not (wordsSyntax.is_n2w x); 351in 352 fun constant_propagation_let_conv tm = 353 if blocked (dest_let tm) then 354 raise ERR "constant_propagation_let_conv" "blocked" 355 else 356 REWR_CONV LET_THM tm; 357end; 358 359val constant_propagation_SS = 360 simpLib.SSFRAG 361 {name = NONE, 362 convs = [{name = "constant_propagation_let_conv", 363 key = SOME ([], ``LET f x``), 364 trace = 2, 365 conv = K (K constant_propagation_let_conv)}], 366 rewrs = [curve_a1, 367 curve_a2, 368 curve_a3, 369 curve_a4, 370 curve_a6, 371 affine_case, 372 curve_mult_def], 373 ac = [], 374 filter = NONE, 375 dprocs = [], 376 congs = []}; 377 378val constant_propagation_ss = 379 simpLib.++ 380 (simpLib.++ (alg_ss,numSimps.REDUCE_ss), constant_propagation_SS); 381 382val ex1_constant_propagation = 383 CONV_RULE 384 (SIMP_CONV 385 constant_propagation_ss 386 [GSYM example1_curve_field, 387 example1_elgamal_g_def, 388 example1_elgamal_h_def, 389 example1_elgamal_x_def, 390 ex1_curve_zero_def, 391 ex1_curve_point_def, 392 ex1_elgamal_g_x, 393 ex1_elgamal_g_y, 394 ex1_elgamal_h_x, 395 ex1_elgamal_h_y, 396 ex1_elgamal_x] THENC 397 SIMP_CONV 398 constant_propagation_ss 399 [example1_curve_field, 400 example1_prime_def, 401 example1_field_def, 402 example1_curve_def, 403 ex1_prime_def, 404 ex1_field_elt_def, 405 ex1_field_num_def, 406 ex1_field_zero_def]); 407 408val ex1_field_neg_alt = save_thm 409 ("ex1_field_neg_alt", 410 ex1_constant_propagation ex1_field_neg_def); 411 412val ex1_field_add_alt = save_thm 413 ("ex1_field_add_alt", 414 ex1_constant_propagation ex1_field_add_def); 415 416val ex1_field_sub_alt = save_thm 417 ("ex1_field_sub_alt", 418 ex1_constant_propagation ex1_field_sub_def); 419 420val ex1_field_mult_aux_alt = save_thm 421 ("ex1_field_mult_aux_alt", 422 ex1_constant_propagation ex1_field_mult_aux_def); 423 424val ex1_field_mult_alt = save_thm 425 ("ex1_field_mult_alt", 426 ex1_constant_propagation ex1_field_mult_def); 427 428val ex1_field_exp_aux_alt = save_thm 429 ("ex1_field_exp_aux_alt", 430 ex1_constant_propagation ex1_field_exp_aux_def); 431 432val ex1_field_exp_alt = save_thm 433 ("ex1_field_exp_alt", 434 ex1_constant_propagation ex1_field_exp_def); 435 436val ex1_field_inv_alt = save_thm 437 ("ex1_field_inv_alt", 438 ex1_constant_propagation ex1_field_inv_def); 439 440val ex1_field_div_alt = save_thm 441 ("ex1_field_div_alt", 442 ex1_constant_propagation ex1_field_div_def); 443 444val ex1_curve_neg_alt = save_thm 445 ("ex1_curve_neg_alt", 446 ex1_constant_propagation ex1_curve_neg_def); 447 448val ex1_curve_double_alt = save_thm 449 ("ex1_curve_double_alt", 450 ex1_constant_propagation ex1_curve_double_def); 451 452val ex1_curve_add_alt = save_thm 453 ("ex1_curve_add_alt", 454 ex1_constant_propagation ex1_curve_add_def); 455 456val ex1_curve_mult_aux_alt = save_thm 457 ("ex1_curve_mult_aux_alt", 458 ex1_constant_propagation ex1_curve_mult_aux_def); 459 460val ex1_curve_mult_alt = save_thm 461 ("ex1_curve_mult_alt", 462 ex1_constant_propagation ex1_curve_mult_def); 463 464val ex1_elgamal_encrypt_alt = save_thm 465 ("ex1_elgamal_encrypt_alt", 466 ex1_constant_propagation ex1_elgamal_encrypt_def); 467 468val ex1_elgamal_decrypt_alt = save_thm 469 ("ex1_elgamal_decrypt_alt", 470 ex1_constant_propagation ex1_elgamal_decrypt_def); 471 472(* ========================================================================= *) 473(* A multiword elliptic curve example to be compiled. *) 474(* ========================================================================= *) 475 476(* ------------------------------------------------------------------------- *) 477(* First define the parameters for the example using HOL types. *) 478(* ------------------------------------------------------------------------- *) 479 480val example2_prime_def = Define `example2_prime = 751`; 481 482val example2_field_def = Define `example2_field = GF example2_prime`; 483 484(* ------------------------------------------------------------------------- *) 485(* Converting HOL types to words. *) 486(* ------------------------------------------------------------------------- *) 487 488val ex2_prime0 = Define 489 `ex2_prime0 : word32 = n2w example2_prime`; 490 491val ex2_prime1 = Define 492 `ex2_prime1 : word32 = n2w (example2_prime DIV 2 ** 32)`; 493 494val ex2_field_neg_def = Define 495 `ex2_field_neg (x0 : word32, x1 : word32) = 496 if (x0 = 0w) /\ (x1 = 0w) then (0w,0w) 497 else 498 let y0 = ex2_prime0 - x0 in 499 let y1 = if y0 <= ex2_prime0 then ex2_prime1 - x1 500 else ex2_prime1 - (x1 + 1w) in 501 (y0,y1)`; 502 503val _ = html_theory "elliptic_example"; 504 505val () = export_theory (); 506