1(* ========================================================================= *) 2(* Create "ellipticTheory" setting up the theory of elliptic curves *) 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 12 ["Algebra", 13 "bossLib", "metisLib", "res_quanTools", 14 "optionTheory", "listTheory", 15 "arithmeticTheory", "dividesTheory", "gcdTheory", 16 "pred_setTheory", "pred_setSyntax", 17 "primalityTools", "fieldTools"]; 18val () = quietdec := true; 19*) 20 21open HolKernel Parse boolLib bossLib metisLib res_quanTools; 22open optionTheory listTheory arithmeticTheory dividesTheory gcdTheory; 23open pred_setTheory; 24open primalityTools; 25open groupTheory groupTools fieldTheory fieldTools; 26 27(* 28val () = quietdec := false; 29*) 30 31(* ------------------------------------------------------------------------- *) 32(* Start a new theory called "elliptic". *) 33(* ------------------------------------------------------------------------- *) 34 35val _ = new_theory "elliptic"; 36 37val ERR = mk_HOL_ERR "elliptic"; 38val Bug = mlibUseful.Bug; 39val Error = ERR ""; 40 41val Bug = fn s => (print ("\n\nBUG: " ^ s ^ "\n\n"); Bug s); 42 43(* ------------------------------------------------------------------------- *) 44(* Sort out the parser. *) 45(* ------------------------------------------------------------------------- *) 46 47val () = Parse.add_infix ("/", 600, HOLgrammars.LEFT); 48 49(* ------------------------------------------------------------------------- *) 50(* Show oracle tags. *) 51(* ------------------------------------------------------------------------- *) 52 53val () = show_tags := true; 54 55(* ------------------------------------------------------------------------- *) 56(* The subtype context. *) 57(* ------------------------------------------------------------------------- *) 58 59val context = field_context; 60val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 61 62(* ------------------------------------------------------------------------- *) 63(* Helper proof tools. *) 64(* ------------------------------------------------------------------------- *) 65 66infixr 0 << 67infixr 1 ++ || THENC ORELSEC 68infix 2 >> 69 70val op ++ = op THEN; 71val op << = op THENL; 72val op >> = op THEN1; 73val op || = op ORELSE; 74val Know = Q_TAC KNOW_TAC; 75val Suff = Q_TAC SUFF_TAC; 76val REVERSE = Tactical.REVERSE; 77val lemma = Tactical.prove; 78(*** 79fun bool_compare (true,false) = LESS 80 | bool_compare (false,true) = GREATER 81 | bool_compare _ = EQUAL; 82 83fun trace_conv name conv tm = 84 let 85 val th = conv tm 86 val () = (print (name ^ ": "); print_thm th; print "\n") 87 in 88 th 89 end 90 handle e as HOL_ERR _ => 91 (print (name ^ ": "); print_term tm; print " --> HOL_ERR\n"; raise e) 92 93fun trans_conv c th = 94 let 95 val (_,tm) = dest_eq (concl th) 96 val th' = c tm 97 in 98 TRANS th th' 99 end; 100***) 101val norm_rule = 102 SIMP_RULE (simpLib.++ (pureSimps.pure_ss, resq_SS)) 103 [GSYM LEFT_FORALL_IMP_THM, GSYM RIGHT_FORALL_IMP_THM, 104 AND_IMP_INTRO, GSYM CONJ_ASSOC]; 105 106fun match_tac th = 107 let 108 val th = norm_rule th 109 val (_,tm) = strip_forall (concl th) 110 in 111 (if is_imp tm then MATCH_MP_TAC else MATCH_ACCEPT_TAC) th 112 end; 113(*** 114val clean_assumptions = 115 let 116 fun eq x y = aconv (concl x) (concl y) 117 in 118 POP_ASSUM_LIST (STRIP_ASSUME_TAC o LIST_CONJ o rev o op_mk_set eq) 119 end; 120 121fun flexible_solver solver cond = 122 let 123 val cond_th = solver cond 124 val cond_tm = concl cond_th 125 in 126 if cond_tm = cond then cond_th 127 else if cond_tm = mk_eq (cond,T) then EQT_ELIM cond_th 128 else raise Bug "flexible_solver: solver didn't prove condition" 129 end; 130 131fun cond_rewr_conv rewr = 132 let 133 val rewr = SPEC_ALL (norm_rule rewr) 134 val rewr_tm = concl rewr 135 val (no_cond,eq) = 136 case total dest_imp_only rewr_tm of 137 NONE => (true,rewr_tm) 138 | SOME (_,eq) => (false,eq) 139 val pat = lhs eq 140 in 141 fn solver => fn tm => 142 let 143 val sub = match_term pat tm 144 val th = INST_TY_TERM sub rewr 145 in 146 if no_cond then th 147 else MP th (flexible_solver solver (rand (rator (concl th)))) 148 end 149 end; 150 151fun cond_rewrs_conv ths = 152 let 153 val solver_convs = map cond_rewr_conv ths 154 fun mk_conv solver solver_conv = solver_conv solver 155 in 156 fn solver => FIRST_CONV (map (mk_conv solver) solver_convs) 157 end; 158 159fun repeat_rule (rule : rule) th = 160 repeat_rule rule (rule th) handle HOL_ERR _ => th; 161 162fun first_rule [] _ = raise ERR "first_rule" "" 163 | first_rule ((rule : rule) :: rules) th = 164 rule th handle HOL_ERR _ => first_rule rules th; 165 166val dest_in = dest_binop pred_setSyntax.in_tm (ERR "dest_in" ""); 167 168val is_in = can dest_in; 169 170val abbrev_tm = ``Abbrev``; 171 172fun dest_abbrev tm = 173 let 174 val (c,t) = dest_comb tm 175 val () = if same_const c abbrev_tm then () else raise ERR "dest_abbrev" "" 176 in 177 dest_eq t 178 end; 179 180val is_abbrev = can dest_abbrev; 181 182fun solver_conv_to_simpset_conv solver_conv = 183 let 184 val {name : string, key : term, conv : conv -> conv} = solver_conv 185 val key = SOME ([] : term list, key) 186 and conv = fn c => fn tms : term list => conv (c tms) 187 and trace = 2 188 in 189 {name = name, key = key, conv = conv, trace = trace} 190 end; 191 192(* ------------------------------------------------------------------------- *) 193(* Helper theorems. *) 194(* ------------------------------------------------------------------------- *) 195 196val THREE = DECIDE ``3 = SUC 2``; 197 198val DIV_THEN_MULT = store_thm 199 ("DIV_THEN_MULT", 200 ``!p q. SUC q * (p DIV SUC q) <= p``, 201 NTAC 2 STRIP_TAC 202 ++ Know `?r. p = (p DIV SUC q) * SUC q + r` 203 >> (Know `0 < SUC q` >> DECIDE_TAC 204 ++ PROVE_TAC [DIVISION]) 205 ++ STRIP_TAC 206 ++ Suff `p = SUC q * (p DIV SUC q) + r` 207 >> (POP_ASSUM_LIST (K ALL_TAC) ++ DECIDE_TAC) 208 ++ PROVE_TAC [MULT_COMM]); 209 210val MOD_EXP = store_thm 211 ("MOD_EXP", 212 ``!a n m. 0 < m ==> (((a MOD m) ** n) MOD m = (a ** n) MOD m)``, 213 RW_TAC std_ss [] 214 ++ Induct_on `n` 215 ++ RW_TAC std_ss [EXP] 216 ++ MP_TAC (Q.SPEC `m` MOD_TIMES2) 217 ++ ASM_REWRITE_TAC [] 218 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 219 ++ ASM_SIMP_TAC std_ss [MOD_MOD]); 220 221val MULT_EXP = store_thm 222 ("MULT_EXP", 223 ``!a b n. (a * b) ** n = (a ** n) * (b ** n)``, 224 RW_TAC std_ss [] 225 ++ Induct_on `n` 226 ++ RW_TAC std_ss [EXP, EQ_MULT_LCANCEL, GSYM MULT_ASSOC] 227 ++ RW_TAC std_ss 228 [EXP, ONCE_REWRITE_RULE [MULT_COMM] EQ_MULT_LCANCEL, MULT_ASSOC] 229 ++ METIS_TAC [MULT_COMM]); 230 231val EXP_EXP = store_thm 232 ("EXP_EXP", 233 ``!a b c. (a ** b) ** c = a ** (b * c)``, 234 RW_TAC std_ss [] 235 ++ Induct_on `b` 236 ++ RW_TAC std_ss [EXP, MULT, EXP_1] 237 ++ RW_TAC std_ss [MULT_EXP, EXP_ADD] 238 ++ METIS_TAC [MULT_COMM]); 239***) 240val EL_ETA = store_thm 241 ("EL_ETA", 242 ``!l1 l2. 243 (LENGTH l1 = LENGTH l2) /\ (!n. n < LENGTH l1 ==> (EL n l1 = EL n l2)) = 244 (l1 = l2)``, 245 Induct 246 >> (Cases ++ RW_TAC arith_ss [LENGTH]) 247 ++ STRIP_TAC 248 ++ Cases 249 ++ RW_TAC arith_ss [LENGTH] 250 ++ REVERSE (Cases_on `h = h'`) 251 >> (RW_TAC std_ss [] 252 ++ DISJ2_TAC 253 ++ Q.EXISTS_TAC `0` 254 ++ RW_TAC arith_ss [EL, HD]) 255 ++ RW_TAC arith_ss [] 256 ++ Q.PAT_ASSUM `!x. P x` (fn th => REWRITE_TAC [GSYM th]) 257 ++ EQ_TAC 258 >> (RW_TAC std_ss [] 259 ++ Q.PAT_ASSUM `!x. P x` (MP_TAC o Q.SPEC `SUC n`) 260 ++ RW_TAC arith_ss [EL, TL]) 261 ++ RW_TAC std_ss [] 262 ++ Q.PAT_ASSUM `n < SUC X` MP_TAC 263 ++ Cases_on `n` 264 ++ RW_TAC arith_ss [EL, HD, TL]); 265 266val el_append = store_thm 267 ("el_append", 268 ``!n p q. 269 n < LENGTH p + LENGTH q ==> 270 (EL n (APPEND p q) = 271 if n < LENGTH p then EL n p else EL (n - LENGTH p) q)``, 272 Induct 273 ++ Cases 274 ++ RW_TAC arith_ss [EL, HD, TL, APPEND, LENGTH]); 275 276(* ========================================================================= *) 277(* Vector spaces *) 278(* ========================================================================= *) 279 280(* ------------------------------------------------------------------------- *) 281(* The basic definitions *) 282(* ------------------------------------------------------------------------- *) 283 284val () = type_abbrev ("vector", Type `:'a list`); 285 286val dimension_def = Define `dimension = (LENGTH : 'a vector -> num)`; 287 288val coord_def = Define `coord = (EL : num -> 'a vector -> 'a)`; 289 290val coords_def = Define `coords (v : 'a vector) = { i | i < dimension v }`; 291 292val vector_space_def = Define 293 `vector_space (f : 'a field) n = 294 { v | (dimension v = n) /\ !i :: coords v. coord i v IN f.carrier }`; 295 296val origin_def = Define 297 `(origin (f : 'a field) 0 = []) /\ 298 (origin (f : 'a field) (SUC n) = field_zero f :: origin f n)`; 299 300val nonorigin_def = Define 301 `nonorigin (f : 'a field) = 302 { v | v IN vector_space f (dimension v) /\ ~(v = origin f (dimension v)) }`; 303 304val vector_space_origin = store_thm 305 ("vector_space_origin", 306 ``!f :: Field. !n. origin f n IN vector_space f n``, 307 RW_TAC resq_ss 308 [vector_space_def, dimension_def, coord_def, GSYM EVERY_EL, 309 coords_def, GSPECIFICATION] 310 >> (Induct_on `n` ++ RW_TAC std_ss [origin_def, LENGTH]) 311 ++ Induct_on `n` 312 ++ RW_TAC std_ss [origin_def, EVERY_DEF, field_zero_carrier]); 313 314val origin_eq = store_thm 315 ("origin_eq", 316 ``!f n p. 317 (p = origin f n) = 318 (dimension p = n) /\ !i :: coords p. coord i p = field_zero f``, 319 RW_TAC resq_ss 320 [dimension_def, coord_def, GSYM EVERY_EL, coords_def, GSPECIFICATION] 321 ++ Q.SPEC_TAC (`p`,`p`) 322 ++ (Induct_on `n` 323 ++ RW_TAC std_ss [origin_def, LENGTH_NIL, LENGTH_CONS]) 324 >> (EQ_TAC ++ RW_TAC std_ss [EVERY_DEF]) 325 ++ EQ_TAC 326 ++ RW_TAC std_ss [] 327 ++ FULL_SIMP_TAC std_ss [EVERY_DEF] 328 ++ METIS_TAC []); 329 330val origin_eq' = store_thm 331 ("origin_eq'", 332 ``!f n p. 333 (origin f n = p) = 334 (dimension p = n) /\ !i :: coords p. coord i p = field_zero f``, 335 METIS_TAC [origin_eq]); 336 337val nonorigin_alt = store_thm 338 ("nonorigin_alt", 339 ``!f p. 340 p IN nonorigin f = 341 EVERY (\x. x IN f.carrier) p /\ 342 ~(EVERY (\x. x = field_zero f) p)``, 343 RW_TAC resq_ss 344 [nonorigin_def, GSPECIFICATION, dimension_def, coords_def, coord_def, 345 vector_space_def, origin_eq, GSYM EVERY_EL]); 346 347(* ========================================================================= *) 348(* Projective geometry *) 349(* ========================================================================= *) 350 351(* ------------------------------------------------------------------------- *) 352(* The basic definitions *) 353(* ------------------------------------------------------------------------- *) 354 355(* Tuned to always be an equivalence relation on type 'a when f is a Field *) 356val project_def = Define 357 `project (f : 'a field) v1 v2 = 358 (v1 = v2) \/ 359 (v1 IN nonorigin f /\ v2 IN nonorigin f /\ 360 (dimension v1 = dimension v2) /\ 361 ?c :: (f.carrier). !i :: coords v1. 362 field_mult f c (coord i v1) = coord i v2)`; 363 364(* Must use the primitive GSPEC to get around the set binding heuristic *) 365val projective_space_def = Define 366 `projective_space (f : 'a field) n = 367 GSPEC (\v. (project f v, v IN (vector_space f (n + 1) INTER nonorigin f)))`; 368 369val affine_def = Define `affine f v = project f (v ++ [field_one f])`; 370 371val project_refl = store_thm 372 ("project_refl", 373 ``!f p. project f p p``, 374 RW_TAC std_ss [project_def]); 375 376val project_refl' = store_thm 377 ("project_refl'", 378 ``!f p q. (p = q) ==> project f p q``, 379 METIS_TAC [project_refl]); 380 381val project_sym = store_thm 382 ("project_sym", 383 ``!f :: Field. !p1 p2. project f p1 p2 ==> project f p2 p1``, 384 SIMP_TAC resq_ss [project_def, nonorigin_def, vector_space_def] 385 ++ RW_TAC std_ss [GSPECIFICATION, coords_def, dimension_def, coord_def] 386 ++ DISJ2_TAC 387 ++ RW_TAC std_ss [] 388 ++ Know `c IN field_nonzero f` 389 >> (RW_TAC std_ss [field_nonzero_def, IN_DIFF, IN_SING] 390 ++ STRIP_TAC 391 ++ RW_TAC std_ss [] 392 ++ Q.PAT_ASSUM `~(p2 = X)` MP_TAC 393 ++ RW_TAC resq_ss 394 [origin_eq, EVERY_EL, dimension_def, coords_def, 395 coord_def, GSPECIFICATION] 396 ++ Q.PAT_ASSUM `!n. P n` (MP_TAC o Q.SPEC `i`) 397 ++ RW_TAC std_ss [field_mult_lzero]) 398 ++ RW_TAC std_ss [] 399 ++ Q.EXISTS_TAC `field_inv f c` 400 ++ RW_TAC alg_ss [] 401 ++ match_tac field_mult_lcancel_imp 402 ++ Q.EXISTS_TAC `f` 403 ++ Q.EXISTS_TAC `c` 404 ++ RW_TAC alg_ss [] 405 ++ Q.PAT_ASSUM `!i. i < LENGTH p2 ==> X` (MP_TAC o Q.SPEC `i`) 406 ++ RW_TAC alg_ss []); 407 408val project_trans = store_thm 409 ("project_trans", 410 ``!f :: Field. !p1 p2 p3. 411 project f p1 p2 /\ project f p2 p3 ==> project f p1 p3``, 412 SIMP_TAC resq_ss [project_def, nonorigin_def, vector_space_def] 413 ++ RW_TAC std_ss [GSPECIFICATION, coords_def, dimension_def, coord_def] 414 << [METIS_TAC [], 415 METIS_TAC [], 416 DISJ2_TAC 417 ++ RW_TAC std_ss [] 418 ++ Q.EXISTS_TAC `field_mult f c' c` 419 ++ RW_TAC std_ss [field_mult_carrier] 420 ++ RW_TAC std_ss [field_mult_assoc]]); 421 422val project_eq = store_thm 423 ("project_eq", 424 ``!f :: Field. !v1 v2. 425 ((project f v1 = project f v2) = project f v1 v2)``, 426 RW_TAC resq_ss [] 427 ++ MATCH_MP_TAC EQ_SYM 428 ++ Q.SPEC_TAC (`v2`,`v2`) 429 ++ Q.SPEC_TAC (`v1`,`v1`) 430 ++ SIMP_TAC std_ss [GSYM relationTheory.ALT_equivalence] 431 ++ RW_TAC std_ss [relationTheory.equivalence_def] 432 << [RW_TAC std_ss [relationTheory.reflexive_def] 433 ++ METIS_TAC [project_refl], 434 RW_TAC std_ss [relationTheory.symmetric_def] 435 ++ METIS_TAC [project_sym], 436 RW_TAC std_ss [relationTheory.transitive_def] 437 ++ METIS_TAC [project_trans]]); 438 439val affine_eq = store_thm 440 ("affine_eq", 441 ``!f :: Field. !v1 v2. (affine f v1 = affine f v2) = (v1 = v2)``, 442 RW_TAC resq_ss [project_eq, affine_def, project_def, APPEND_11] 443 ++ REVERSE EQ_TAC >> RW_TAC std_ss [] 444 ++ RW_TAC resq_ss 445 [dimension_def, coords_def, GSPECIFICATION, nonorigin_alt, coord_def] 446 ++ REPEAT (Q.PAT_ASSUM `~(EVERY P L)` (K ALL_TAC)) 447 ++ REPEAT (POP_ASSUM MP_TAC) 448 ++ RW_TAC std_ss [EVERY_APPEND, LENGTH_APPEND, LENGTH, GSYM ADD1, EVERY_DEF] 449 ++ RW_TAC std_ss [GSYM EL_ETA] 450 ++ Suff `c = field_one f` 451 >> (Q.PAT_ASSUM `!i. P i` (MP_TAC o Q.SPEC `n`) 452 ++ RW_TAC arith_ss [el_append] 453 ++ POP_ASSUM (fn th => ONCE_REWRITE_TAC [GSYM th]) 454 ++ MATCH_MP_TAC EQ_SYM 455 ++ match_tac field_mult_lone 456 ++ Q.PAT_ASSUM `EVERY P v1` MP_TAC 457 ++ RW_TAC std_ss [EVERY_EL]) 458 ++ Q.PAT_ASSUM `!i. P i` (MP_TAC o Q.SPEC `LENGTH v1`) 459 ++ RW_TAC arith_ss [el_append, LENGTH, EL, HD] 460 ++ POP_ASSUM (fn th => ONCE_REWRITE_TAC [GSYM th]) 461 ++ MATCH_MP_TAC EQ_SYM 462 ++ match_tac field_mult_rone 463 ++ RW_TAC std_ss []); 464 465(* ========================================================================= *) 466(* Elliptic curves *) 467(* ========================================================================= *) 468 469(* ------------------------------------------------------------------------- *) 470(* The basic definitions *) 471(* ------------------------------------------------------------------------- *) 472 473val () = Hol_datatype 474 `curve = 475 <| field : 'a field; 476 a1 : 'a; 477 a2 : 'a; 478 a3 : 'a; 479 a4 : 'a; 480 a6 : 'a |>`; 481 482val curve_accessors = fetch "-" "curve_accessors"; 483 484val curve_b2_def = Define 485 `curve_b2 e = 486 let f = e.field in 487 let $& = field_num f in 488 let $+ = field_add f in 489 let $* = field_mult f in 490 let $** = field_exp f in 491 let a1 = e.a1 in 492 let a2 = e.a2 in 493 a1 ** 2 + & 4 * a2`; 494 495val curve_b4_def = Define 496 `curve_b4 e = 497 let f = e.field in 498 let $& = field_num f in 499 let $+ = field_add f in 500 let $* = field_mult f in 501 let a1 = e.a1 in 502 let a3 = e.a3 in 503 let a4 = e.a4 in 504 a1 * a3 + & 2 * a4`; 505 506val curve_b6_def = Define 507 `curve_b6 e = 508 let f = e.field in 509 let $& = field_num f in 510 let $+ = field_add f in 511 let $* = field_mult f in 512 let $** = field_exp f in 513 let a3 = e.a3 in 514 let a6 = e.a6 in 515 a3 ** 2 + & 4 * a6`; 516 517val curve_b8_def = Define 518 `curve_b8 e = 519 let f = e.field in 520 let $& = field_num f in 521 let $+ = field_add f in 522 let $- = field_sub f in 523 let $* = field_mult f in 524 let $** = field_exp f in 525 let a1 = e.a1 in 526 let a2 = e.a2 in 527 let a3 = e.a3 in 528 let a4 = e.a4 in 529 let a6 = e.a6 in 530 a1 ** 2 * a6 + & 4 * a2 * a6 - a1 * a3 * a4 + a2 * a3 ** 2 - a4 ** 2`; 531 532val discriminant_def = Define 533 `discriminant e = 534 let f = e.field in 535 let $& = field_num f in 536 let $- = field_sub f in 537 let $* = field_mult f in 538 let $** = field_exp f in 539 let b2 = curve_b2 e in 540 let b4 = curve_b4 e in 541 let b6 = curve_b6 e in 542 let b8 = curve_b8 e in 543 & 9 * b2 * b4 * b6 - b2 * b2 * b8 - & 8 * b4 ** 3 - & 27 * b6 ** 2`; 544 545val non_singular_def = Define 546 `non_singular e = ~(discriminant e = field_zero e.field)`; 547 548val Curve_def = Define 549 `Curve = 550 { e | 551 e.field IN Field /\ 552 e.a1 IN e.field.carrier /\ 553 e.a2 IN e.field.carrier /\ 554 e.a3 IN e.field.carrier /\ 555 e.a4 IN e.field.carrier /\ 556 e.a6 IN e.field.carrier /\ 557 non_singular e }`; 558 559val curve_points_def = Define 560 `curve_points e = 561 let f = e.field in 562 let $+ = field_add f in 563 let $* = field_mult f in 564 let $** = field_exp f in 565 let a1 = e.a1 in 566 let a2 = e.a2 in 567 let a3 = e.a3 in 568 let a4 = e.a4 in 569 let a6 = e.a6 in 570 GSPEC (\ (x,y,z). 571 (project f [x; y; z], 572 [x; y; z] IN nonorigin f /\ 573 (y ** 2 * z + a1 * x * y * z + a3 * y * z ** 2 = 574 x ** 3 + a2 * x ** 2 * z + a4 * x * z ** 2 + a6 * z ** 3)))`; 575 576val curve_zero_def = Define 577 `curve_zero e = 578 project e.field 579 [field_zero e.field; field_one e.field; field_zero e.field]`; 580 581val affine_case_def = Define 582 `affine_case e z f p = 583 if p = curve_zero e then z 584 else @t. ?x y. (p = affine e.field [x; y]) /\ (t = f x y)`; 585 586val curve_neg_def = Define 587 `curve_neg e = 588 let f = e.field in 589 let $~ = field_neg f in 590 let $+ = field_add f in 591 let $- = field_sub f in 592 let $* = field_mult f in 593 let a1 = e.a1 in 594 let a3 = e.a3 in 595 affine_case e (curve_zero e) 596 (\x1 y1. 597 let x = x1 in 598 let y = ~y1 - a1 * x1 - a3 in 599 affine f [x; y])`; 600 601val curve_double_def = Define 602 `curve_double e = 603 let f = e.field in 604 let $& = field_num f in 605 let $~ = field_neg f in 606 let $+ = field_add f in 607 let $- = field_sub f in 608 let $* = field_mult f in 609 let $/ = field_div f in 610 let $** = field_exp f in 611 let a1 = e.a1 in 612 let a2 = e.a2 in 613 let a3 = e.a3 in 614 let a4 = e.a4 in 615 let a6 = e.a6 in 616 affine_case e (curve_zero e) 617 (\x1 y1. 618 let d = & 2 * y1 + a1 * x1 + a3 in 619 if d = field_zero f then curve_zero e 620 else 621 let l = (& 3 * x1 ** 2 + & 2 * a2 * x1 + a4 - a1 * y1) / d in 622 let m = (~(x1 ** 3) + a4 * x1 + & 2 * a6 - a3 * y1) / d in 623 let x = l ** 2 + a1 * l - a2 - &2 * x1 in 624 let y = ~(l + a1) * x - m - a3 in 625 affine e.field [x; y])`; 626 627val curve_add_def = Define 628 `curve_add e p1 p2 = 629 if p1 = p2 then curve_double e p1 630 else 631 let f = e.field in 632 let $& = field_num f in 633 let $~ = field_neg f in 634 let $+ = field_add f in 635 let $- = field_sub f in 636 let $* = field_mult f in 637 let $/ = field_div f in 638 let $** = field_exp f in 639 let a1 = e.a1 in 640 let a2 = e.a2 in 641 let a3 = e.a3 in 642 let a4 = e.a4 in 643 let a6 = e.a6 in 644 affine_case e p2 645 (\x1 y1. 646 affine_case e p1 647 (\x2 y2. 648 if x1 = x2 then curve_zero e 649 else 650 let d = x2 - x1 in 651 let l = (y2 - y1) / d in 652 let m = (y1 * x2 - y2 * x1) / d in 653 let x = l ** 2 + a1 * l - a2 - x1 - x2 in 654 let y = ~(l + a1) * x - m - a3 in 655 affine e.field [x; y]) p2) p1`; 656 657val curve_mult_def = Define 658 `(curve_mult (e : 'a curve) p 0 = curve_zero e) /\ 659 (curve_mult (e : 'a curve) p (SUC n) = curve_add e p (curve_mult e p n))`; 660 661val curve_group_def = Define 662 `curve_group e = 663 <| carrier := curve_points e; 664 id := curve_zero e; 665 inv := curve_neg e; 666 mult := curve_add e |>`; 667 668val curve_field = store_thm 669 ("curve_field", 670 ``!e :: Curve. e.field IN Field``, 671 RW_TAC resq_ss [Curve_def, GSPECIFICATION]); 672 673val context = subtypeTools.add_reduction2 curve_field context; 674val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 675 676val curve_a1_carrier = store_thm 677 ("curve_a1_carrier", 678 ``!e :: Curve. e.a1 IN e.field.carrier``, 679 RW_TAC resq_ss [Curve_def, GSPECIFICATION]); 680 681val context = subtypeTools.add_reduction2 curve_a1_carrier context; 682val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 683 684val curve_a2_carrier = store_thm 685 ("curve_a2_carrier", 686 ``!e :: Curve. e.a2 IN e.field.carrier``, 687 RW_TAC resq_ss [Curve_def, GSPECIFICATION]); 688 689val context = subtypeTools.add_reduction2 curve_a2_carrier context; 690val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 691 692val curve_a3_carrier = store_thm 693 ("curve_a3_carrier", 694 ``!e :: Curve. e.a3 IN e.field.carrier``, 695 RW_TAC resq_ss [Curve_def, GSPECIFICATION]); 696 697val context = subtypeTools.add_reduction2 curve_a3_carrier context; 698val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 699 700val curve_a4_carrier = store_thm 701 ("curve_a4_carrier", 702 ``!e :: Curve. e.a4 IN e.field.carrier``, 703 RW_TAC resq_ss [Curve_def, GSPECIFICATION]); 704 705val context = subtypeTools.add_reduction2 curve_a4_carrier context; 706val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 707 708val curve_a6_carrier = store_thm 709 ("curve_a6_carrier", 710 ``!e :: Curve. e.a6 IN e.field.carrier``, 711 RW_TAC resq_ss [Curve_def, GSPECIFICATION]); 712 713val context = subtypeTools.add_reduction2 curve_a6_carrier context; 714val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 715 716val curve_cases = store_thm 717 ("curve_cases", 718 ``!e :: Curve. !p :: curve_points e. 719 (p = curve_zero e) \/ 720 ?x y :: (e.field.carrier). p = affine e.field [x; y]``, 721 RW_TAC resq_ss 722 [curve_points_def, curve_zero_def, 723 GSPECIFICATION, LET_DEF, affine_def, APPEND] 724 ++ POP_ASSUM MP_TAC 725 ++ Know `?x1 y1 z1. x = (x1,y1,z1)` 726 >> METIS_TAC [pairTheory.ABS_PAIR_THM] 727 ++ STRIP_TAC 728 ++ RW_TAC alg_ss [project_eq] 729 ++ Q.PAT_ASSUM `X IN Y` MP_TAC 730 ++ RW_TAC resq_ss 731 [nonorigin_def, GSPECIFICATION, coords_def, dimension_def, 732 vector_space_def, coord_def, GSYM EVERY_EL, EVERY_DEF] 733 ++ Cases_on `z1 = field_zero e.field` 734 << [RW_TAC std_ss [] 735 ++ DISJ1_TAC 736 ++ Q.PAT_ASSUM `X = Y` MP_TAC 737 ++ RW_TAC alg_ss [] 738 ++ Q.PAT_ASSUM `~(X = Y)` MP_TAC 739 ++ RW_TAC resq_ss 740 [origin_eq, dimension_def, coords_def, GSPECIFICATION, 741 coord_def, GSYM EVERY_EL, EVERY_DEF] 742 ++ RW_TAC resq_ss 743 [project_def, nonorigin_alt, EVERY_DEF, field_one_carrier, 744 field_one_zero, dimension_def, LENGTH] 745 ++ DISJ2_TAC 746 ++ Know `y1 IN field_nonzero e.field` 747 >> RW_TAC std_ss [field_nonzero_def, IN_DIFF, IN_SING] 748 ++ RW_TAC alg_ss [] 749 ++ Q.EXISTS_TAC `field_inv e.field y1` 750 ++ RW_TAC alg_ss 751 [coords_def, GSPECIFICATION, dimension_def, LENGTH] 752 ++ Know `(i = 0) \/ (i = SUC 0) \/ (i = SUC (SUC 0))` 753 >> DECIDE_TAC 754 ++ STRIP_TAC 755 ++ RW_TAC bool_ss [EL, HD, TL, coord_def] 756 ++ RW_TAC alg_ss [], 757 Q.PAT_ASSUM `X = Y` (K ALL_TAC) 758 ++ DISJ2_TAC 759 ++ Q.EXISTS_TAC `field_mult e.field (field_inv e.field z1) x1` 760 ++ Know `z1 IN field_nonzero e.field` 761 >> RW_TAC std_ss [field_nonzero_def, IN_DIFF, IN_SING] 762 ++ RW_TAC alg_ss [] 763 ++ Q.EXISTS_TAC `field_mult e.field (field_inv e.field z1) y1` 764 ++ RW_TAC alg_ss [] 765 ++ RW_TAC resq_ss 766 [project_def, nonorigin_alt, EVERY_DEF, dimension_def, LENGTH] 767 ++ RW_TAC alg_ss [] 768 ++ DISJ2_TAC 769 ++ Q.EXISTS_TAC `field_inv e.field z1` 770 ++ RW_TAC alg_ss 771 [coords_def, dimension_def, LENGTH, coord_def, GSPECIFICATION] 772 ++ Know `(i = 0) \/ (i = SUC 0) \/ (i = SUC (SUC 0))` 773 >> DECIDE_TAC 774 ++ STRIP_TAC 775 ++ RW_TAC bool_ss [EL, HD, TL, coord_def] 776 ++ RW_TAC alg_ss []]); 777 778local 779 val case_th = 780 CONV_RULE 781 (RES_FORALL_CONV THENC 782 QUANT_CONV 783 (RAND_CONV RES_FORALL_CONV THENC 784 RIGHT_IMP_FORALL_CONV THENC 785 QUANT_CONV 786 (REWR_CONV AND_IMP_INTRO))) curve_cases; 787 788 fun cases_on e p = MP_TAC (SPECL [e,p] case_th); 789in 790 fun ec_cases_on e p (asl,g) = 791 let 792 val fvs = free_varsl (g :: asl) 793 val e_tm = Parse.parse_in_context fvs e 794 and p_tm = Parse.parse_in_context fvs p 795 in 796 cases_on e_tm p_tm 797 end (asl,g); 798end; 799 800val curve_distinct = store_thm 801 ("curve_distinct", 802 ``!e :: Curve. !x y. 803 ~(curve_zero e = affine e.field [x; y])``, 804 RW_TAC resq_ss 805 [affine_case_def, affine_def, Curve_def, GSPECIFICATION, 806 curve_zero_def, APPEND, project_eq] 807 ++ STRIP_TAC 808 ++ FULL_SIMP_TAC resq_ss 809 [project_def, field_zero_one, coords_def, GSPECIFICATION, 810 dimension_def, coord_def, LENGTH] 811 >> (POP_ASSUM MP_TAC 812 ++ RW_TAC std_ss [field_zero_one]) 813 ++ Q.PAT_ASSUM `!i. P i` (MP_TAC o Q.SPEC `SUC (SUC 0)`) 814 ++ RW_TAC arith_ss [EL, HD, TL, field_mult_rzero, field_zero_one]); 815 816val affine_case = store_thm 817 ("affine_case", 818 ``!e :: Curve. !z f. 819 (affine_case e z f (curve_zero e) = z) /\ 820 !x y. affine_case e z f (affine e.field [x; y]) = f x y``, 821 RW_TAC resq_ss 822 [affine_case_def, affine_eq, Curve_def, GSPECIFICATION, 823 curve_distinct]); 824 825(* 826val curve_quadratic = store_thm 827 ("curve_quadratic", 828 ``!e :: Curve. !x1 y1 y2 :: (e.field.carrier). 829 let f = e.field in 830 let $~ = field_neg f in 831 let $+ = field_add f in 832 let $* = field_mult f in 833 let a1 = e.a1 in 834 let a3 = e.a3 in 835 affine [x1; y1] IN curve_points e /\ 836 affine [x1; y2] IN curve_points e ==> 837 (y2 = y1) \/ (y2 = ~(y1 + a1 * x1 + a3))``, 838*) 839 840val curve_zero_eq = store_thm 841 ("curve_zero_eq", 842 ``!e :: Curve. !x y z :: (e.field.carrier). 843 (project e.field [x; y; z] = curve_zero e) = 844 (x = field_zero e.field) /\ 845 ~(y = field_zero e.field) /\ 846 (z = field_zero e.field)``, 847 RW_TAC resq_ss [] 848 ++ RW_TAC alg_ss 849 [GSPECIFICATION, curve_zero_def, 850 project_eq, project_def, nonorigin_alt, EVERY_DEF, dimension_def, 851 LENGTH, field_zero_carrier, field_one_carrier, field_one_zero, 852 coords_def, coord_def] 853 ++ RW_TAC resq_ss [GSPECIFICATION] 854 ++ REVERSE (Cases_on `x = field_zero e.field`) 855 >> (RW_TAC std_ss [] 856 ++ REVERSE (Cases_on `c IN e.field.carrier`) 857 ++ RW_TAC std_ss [] 858 ++ MATCH_MP_TAC (PROVE [] ``(~c ==> F) ==> c``) 859 ++ STRIP_TAC 860 ++ Know `~(c = field_zero e.field)` 861 >> (STRIP_TAC 862 ++ Q.PAT_ASSUM `~X` MP_TAC 863 ++ RW_TAC std_ss [] 864 ++ Q.EXISTS_TAC `SUC 0` 865 ++ RW_TAC std_ss [EL, HD, TL] 866 ++ RW_TAC alg_ss []) 867 ++ STRIP_TAC 868 ++ Q.PAT_ASSUM `~?x. P x` MP_TAC 869 ++ RW_TAC std_ss [] 870 ++ Q.EXISTS_TAC `0` 871 ++ RW_TAC alg_ss [EL, HD, TL]) 872 ++ REVERSE (Cases_on `z = field_zero e.field`) 873 >> (RW_TAC std_ss [] 874 ++ REVERSE (Cases_on `c IN e.field.carrier`) 875 ++ RW_TAC std_ss [] 876 ++ MATCH_MP_TAC (PROVE [] ``(~c ==> F) ==> c``) 877 ++ STRIP_TAC 878 ++ Know `~(c = field_zero e.field)` 879 >> (STRIP_TAC 880 ++ Q.PAT_ASSUM `~X` MP_TAC 881 ++ RW_TAC std_ss [] 882 ++ Q.EXISTS_TAC `SUC 0` 883 ++ RW_TAC std_ss [EL, HD, TL] 884 ++ RW_TAC alg_ss []) 885 ++ STRIP_TAC 886 ++ Q.PAT_ASSUM `~?x. P x` MP_TAC 887 ++ RW_TAC std_ss [] 888 ++ Q.EXISTS_TAC `SUC (SUC 0)` 889 ++ RW_TAC alg_ss [EL, HD, TL]) 890 ++ RW_TAC alg_ss [] 891 ++ Cases_on `y = field_zero e.field` 892 ++ RW_TAC alg_ss [] 893 ++ DISJ2_TAC 894 ++ Know `y IN field_nonzero e.field` 895 >> RW_TAC alg_ss [field_nonzero_alt] 896 ++ RW_TAC std_ss [] 897 ++ Q.EXISTS_TAC `field_inv e.field y` 898 ++ RW_TAC alg_ss [] 899 ++ Know `(i = 0) \/ (i = SUC 0) \/ (i = SUC (SUC 0))` >> DECIDE_TAC 900 ++ STRIP_TAC 901 ++ RW_TAC alg_ss [EL, HD, TL]); 902 903val curve_zero_eq' = store_thm 904 ("curve_zero_eq'", 905 ``!e :: Curve. !x y z :: (e.field.carrier). 906 (curve_zero e = project e.field [x; y; z]) = 907 (x = field_zero e.field) /\ 908 ~(y = field_zero e.field) /\ 909 (z = field_zero e.field)``, 910 RW_TAC std_ss [curve_zero_eq]); 911 912val curve_neg_optimized = store_thm 913 ("curve_neg_optimized", 914 ``!e :: Curve. !x1 y1 z1 :: (e.field.carrier). 915 project e.field [x1; y1; z1] IN curve_points e ==> 916 (curve_neg e (project e.field [x1; y1; z1]) = 917 let f = e.field in 918 let $~ = field_neg f in 919 let $+ = field_add f in 920 let $* = field_mult f in 921 let a1 = e.a1 in 922 let a3 = e.a3 in 923 let x = x1 in 924 let y = ~(y1 + a1 * x1 + a3 * z1) in 925 let z = z1 in 926 project f [x; y; z])``, 927 RW_TAC resq_ss [LET_DEF, curve_neg_def] 928 ++ Know `e IN Curve` >> RW_TAC std_ss [] 929 ++ REWRITE_TAC [Curve_def] 930 ++ RW_TAC std_ss [GSPECIFICATION] 931 ++ ec_cases_on `e` `project e.field [x1; y1; z1]` 932 ++ RW_TAC resq_ss [] 933 >> (RW_TAC std_ss [affine_case] 934 ++ POP_ASSUM MP_TAC 935 ++ RW_TAC std_ss [curve_zero_eq] 936 ++ RW_TAC std_ss [field_mult_rzero, field_add_rzero] 937 ++ RW_TAC std_ss [curve_zero_eq', field_neg_carrier] 938 ++ RW_TAC std_ss [field_neg_eq_swap, field_neg_zero]) 939 ++ RW_TAC std_ss [affine_case] 940 ++ POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) 941 ++ ASM_SIMP_TAC resq_ss [affine_def, APPEND, project_eq] 942 ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [project_def])) 943 ++ RW_TAC resq_ss 944 [dimension_def, coords_def, coord_def, LENGTH, GSPECIFICATION] 945 >> (MATCH_MP_TAC project_refl' 946 ++ RW_TAC std_ss [] 947 ++ RW_TAC alg_ss' []) 948 ++ Know `~(c = field_zero e.field)` 949 >> (STRIP_TAC 950 ++ Q.PAT_ASSUM `X IN nonorigin Y` MP_TAC 951 ++ Q.PAT_ASSUM `!i. P i` 952 (fn th => MP_TAC (Q.SPEC `0` th) 953 ++ MP_TAC (Q.SPEC `SUC 0` th) 954 ++ MP_TAC (Q.SPEC `SUC (SUC 0)` th)) 955 ++ RW_TAC std_ss 956 [EL, HD, TL, nonorigin_alt, field_mult_lzero, field_one_carrier, 957 EVERY_DEF]) 958 ++ STRIP_TAC 959 ++ Know `~(z1 = field_zero e.field)` 960 >> (STRIP_TAC 961 ++ Q.PAT_ASSUM `!i. P i` (MP_TAC o Q.SPEC `SUC (SUC 0)`) 962 ++ RW_TAC std_ss 963 [EL, HD, TL, field_entire, field_one_carrier, field_one_zero]) 964 ++ STRIP_TAC 965 ++ RW_TAC resq_ss 966 [project_def, GSPECIFICATION, dimension_def, LENGTH, nonorigin_alt, 967 EVERY_DEF, coords_def, coord_def, field_one_carrier, field_one_zero] 968 ++ DISJ2_TAC 969 ++ CONJ_TAC >> RW_TAC alg_ss [] 970 ++ CONJ_TAC >> RW_TAC alg_ss [] 971 ++ Q.EXISTS_TAC `z1` 972 ++ RW_TAC std_ss [field_mult_carrier] 973 ++ Q.PAT_ASSUM `!i. P i` (fn th => MP_TAC (Q.SPEC `0` th) 974 ++ MP_TAC (Q.SPEC `SUC 0` th) 975 ++ MP_TAC (Q.SPEC `SUC (SUC 0)` th)) 976 ++ RW_TAC std_ss [EL, HD, TL] 977 ++ Know `(i = 0) \/ (i = SUC 0) \/ (i = SUC (SUC 0))` >> DECIDE_TAC 978 ++ STRIP_TAC 979 ++ RW_TAC std_ss [EL, HD, TL, field_mult_rone] 980 ++ RW_TAC alg_ss' [field_distrib]); 981 982val curve_affine = store_thm 983 ("curve_affine", 984 ``!e :: Curve. !x y :: (e.field.carrier). 985 affine e.field [x; y] IN curve_points e = 986 let f = e.field in 987 let $+ = field_add f in 988 let $* = field_mult f in 989 let $** = field_exp f in 990 let a1 = e.a1 in 991 let a2 = e.a2 in 992 let a3 = e.a3 in 993 let a4 = e.a4 in 994 let a6 = e.a6 in 995 y ** 2 + a1 * x * y + a3 * y = 996 x ** 3 + a2 * x ** 2 + a4 * x + a6``, 997 RW_TAC resq_ss 998 [curve_points_def, LET_DEF, affine_def, GSPECIFICATION, APPEND] 999 ++ REVERSE EQ_TAC 1000 >> (RW_TAC alg_ss [] 1001 ++ Q.EXISTS_TAC `(x, y, field_one e.field)` 1002 ++ POP_ASSUM MP_TAC 1003 ++ RW_TAC alg_ss [nonorigin_alt, EVERY_DEF]) 1004 ++ STRIP_TAC 1005 ++ POP_ASSUM MP_TAC 1006 ++ Know `?x1 y1 z1. x' = (x1,y1,z1)` 1007 >> METIS_TAC [pairTheory.ABS_PAIR_THM] 1008 ++ STRIP_TAC 1009 ++ RW_TAC alg_ss [] 1010 ++ Q.PAT_ASSUM `X IN Y` MP_TAC 1011 ++ RW_TAC std_ss [nonorigin_alt] 1012 ++ Q.PAT_ASSUM `EVERY P L` MP_TAC 1013 ++ RW_TAC std_ss [EVERY_DEF] 1014 ++ Q.PAT_ASSUM `project X Y = Z` (MP_TAC o ONCE_REWRITE_RULE [EQ_SYM_EQ]) 1015 ++ RW_TAC alg_ss [project_eq, project_def] 1016 >> (Q.PAT_ASSUM `X = Y` MP_TAC 1017 ++ RW_TAC alg_ss' []) 1018 ++ REPEAT (POP_ASSUM MP_TAC) 1019 ++ RW_TAC resq_ss 1020 [dimension_def, coords_def, coord_def, LENGTH, GSPECIFICATION] 1021 ++ Q.PAT_ASSUM `!i. P i` (fn th => MP_TAC (Q.SPEC `0` th) 1022 ++ MP_TAC (Q.SPEC `SUC 0` th) 1023 ++ MP_TAC (Q.SPEC `SUC (SUC 0)` th)) 1024 ++ RW_TAC std_ss [EL, HD, TL] 1025 ++ Know `c IN field_nonzero e.field` 1026 >> (RW_TAC std_ss [field_nonzero_def, IN_DIFF, IN_SING] 1027 ++ STRIP_TAC 1028 ++ Q.PAT_ASSUM `X = field_one Y` MP_TAC 1029 ++ RW_TAC alg_ss []) 1030 ++ Know `z1 IN field_nonzero e.field` 1031 >> (RW_TAC std_ss [field_nonzero_def, IN_DIFF, IN_SING] 1032 ++ STRIP_TAC 1033 ++ Q.PAT_ASSUM `X = field_one Y` MP_TAC 1034 ++ RW_TAC alg_ss []) 1035 ++ RW_TAC std_ss [] 1036 ++ Know `c = field_inv e.field z1` 1037 >> (match_tac field_mult_rcancel_imp 1038 ++ Q.EXISTS_TAC `e.field` 1039 ++ Q.EXISTS_TAC `z1` 1040 ++ ASM_REWRITE_TAC [] 1041 ++ RW_TAC alg_ss []) 1042 ++ RW_TAC std_ss [] 1043 ++ match_tac field_mult_lcancel_imp 1044 ++ Q.EXISTS_TAC `e.field` 1045 ++ Q.EXISTS_TAC `field_exp e.field z1 3` 1046 ++ REPEAT (Q.PAT_ASSUM `X = Y` MP_TAC) 1047 ++ RW_TAC alg_ss' [field_distrib]); 1048 1049val curve_affine_reduce_3 = store_thm 1050 ("curve_affine_reduce_3", 1051 ``!e :: Curve. !x y :: (e.field.carrier). 1052 affine e.field [x; y] IN curve_points e = 1053 (field_exp e.field x 3 = 1054 field_add e.field 1055 (field_neg e.field e.a6) 1056 (field_add e.field 1057 (field_mult e.field e.a3 y) 1058 (field_add e.field 1059 (field_exp e.field y 2) 1060 (field_add e.field 1061 (field_neg e.field (field_mult e.field e.a4 x)) 1062 (field_add e.field 1063 (field_mult e.field e.a1 (field_mult e.field x y)) 1064 (field_neg e.field 1065 (field_mult e.field e.a2 (field_exp e.field x 2))))))))``, 1066 RW_TAC resq_ss [] 1067 ++ CONV_TAC (RAND_CONV (REWR_CONV EQ_SYM_EQ)) 1068 ++ RW_TAC alg_ss [curve_affine, LET_DEF] 1069 ++ RW_TAC alg_ss' []); 1070 1071local 1072 val exp_tm = ``field_exp e.field (x : 'a)``; 1073 1074 val context_tms = strip_conj 1075 ``e IN Curve /\ (x : 'a) IN e.field.carrier /\ y IN e.field.carrier``; 1076 1077 val affine_tm = ``affine e.field [(x : 'a); y] IN curve_points e``; 1078 1079 val context_ths = map ASSUME context_tms; 1080 1081 val affine = ASSUME affine_tm; 1082 1083 val reduce_3_eq = 1084 (repeat UNDISCH o SPEC_ALL) 1085 (CONV_RULE 1086 (REDEPTH_CONV (RES_FORALL_CONV ORELSEC 1087 HO_REWR_CONV (GSYM RIGHT_FORALL_IMP_THM) ORELSEC 1088 REWR_CONV (GSYM AND_IMP_INTRO))) 1089 curve_affine_reduce_3); 1090 1091 val reduce_3 = EQ_MP reduce_3_eq affine; 1092 1093 fun reduce_n 3 = [reduce_3] 1094 | reduce_n n = 1095 let 1096 val reduce_ths = reduce_n (n - 1) 1097 val n1_tm = numLib.term_of_int (n - 1) 1098 val suc_th = reduceLib.SUC_CONV (numSyntax.mk_suc n1_tm) 1099 val reduce_tm = mk_comb (exp_tm, numLib.term_of_int n) 1100 val reduce_th = 1101 (RAND_CONV (REWR_CONV (SYM suc_th)) THENC 1102 REWR_CONV (CONJUNCT2 field_exp_def) THENC 1103 RAND_CONV (REWR_CONV (hd reduce_ths)) THENC 1104 with_flag (ORACLE_field_poly,true) 1105 (Count.apply 1106 (SIMP_CONV (field_poly_ss context reduce_ths) context_ths))) 1107 reduce_tm 1108 in 1109 reduce_th :: reduce_ths 1110 end; 1111 1112 val weakening_th = PROVE [] ``(a ==> b) ==> (a = a /\ b)``; 1113in 1114 fun curve_affine_reduce_n n = 1115 let 1116 val th = DISCH affine_tm (LIST_CONJ (tl (rev (reduce_n n)))) 1117 val th = MATCH_MP weakening_th th 1118 val th = CONV_RULE (RAND_CONV (LAND_CONV (K reduce_3_eq))) th 1119 val th = foldl (uncurry DISCH) th (rev context_tms) 1120 in 1121 th 1122 end; 1123end; 1124 1125val curve_affine_reduce = save_thm 1126 ("curve_affine_reduce", 1127 with_flag (subtypeTools.ORACLE,true) 1128 (Count.apply curve_affine_reduce_n) 12); 1129 1130val curve_zero_carrier = store_thm 1131 ("curve_zero_carrier", 1132 ``!e :: Curve. curve_zero e IN curve_points e``, 1133 RW_TAC resq_ss [curve_zero_def, curve_points_def, LET_DEF, GSPECIFICATION] 1134 ++ Q.EXISTS_TAC `(field_zero e.field, field_one e.field, field_zero e.field)` 1135 ++ RW_TAC alg_ss [nonorigin_alt, EVERY_DEF]); 1136 1137val context = subtypeTools.add_reduction2 curve_zero_carrier context; 1138val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1139 1140val curve_neg_carrier = Count.apply store_thm 1141 ("curve_neg_carrier", 1142 ``!e :: Curve. !p :: curve_points e. curve_neg e p IN curve_points e``, 1143 RW_TAC resq_ss [] 1144 ++ ec_cases_on `e` `p` 1145 ++ RW_TAC resq_ss [curve_neg_def, LET_DEF] 1146 ++ RW_TAC alg_ss [affine_case] 1147 ++ Q.PAT_ASSUM `affine X Y IN Z` MP_TAC 1148 ++ ASM_SIMP_TAC alg_ss [curve_affine, LET_DEF] 1149 ++ RW_TAC alg_ss' [field_distrib, field_binomial_2]); 1150 1151val context = subtypeTools.add_reduction2 curve_neg_carrier context; 1152val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1153 1154val curve_double_carrier = Count.apply store_thm 1155 ("curve_double_carrier", 1156 ``!e :: Curve. !p :: curve_points e. curve_double e p IN curve_points e``, 1157 RW_TAC resq_ss [] 1158 ++ ec_cases_on `e` `p` 1159 ++ RW_TAC resq_ss [curve_double_def] 1160 ++ normalForms.REMOVE_ABBR_TAC 1161 ++ RW_TAC std_ss [] 1162 ++ RW_TAC alg_ss [affine_case] 1163 ++ RW_TAC alg_ss [] 1164 ++ POP_ASSUM MP_TAC 1165 ++ RW_TAC alg_ss [field_nonzero_eq, curve_affine, LET_DEF] 1166 ++ match_tac field_sub_eq_zero_imp 1167 ++ Q.EXISTS_TAC `e.field` 1168 ++ RW_TAC alg_ss [] 1169 ++ Q.UNABBREV_TAC `x'` 1170 ++ Q.UNABBREV_TAC `y'` 1171 ++ Q.UNABBREV_TAC `l` 1172 ++ Q.UNABBREV_TAC `m` 1173 ++ Count.apply (RW_TAC (field_div_elim_ss context) []) 1174 ++ Q.UNABBREV_TAC `d` 1175 ++ POP_ASSUM (K ALL_TAC) 1176 ++ Q.PAT_ASSUM `affine X Y IN Z` MP_TAC 1177 ++ ASM_SIMP_TAC alg_ss [curve_affine_reduce] 1178 ++ with_flag (ORACLE_field_poly,true) 1179 (with_flag (subtypeTools.ORACLE,true) 1180 (Count.apply (ASM_SIMP_TAC (field_poly_basis_ss context) [])))); 1181 1182val context = subtypeTools.add_reduction2 curve_double_carrier context; 1183val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1184 1185val curve_add_carrier = Count.apply store_thm 1186 ("curve_add_carrier", 1187 ``!e :: Curve. !p q :: curve_points e. curve_add e p q IN curve_points e``, 1188 RW_TAC resq_ss [] 1189 ++ ec_cases_on `e` `p` 1190 ++ ec_cases_on `e` `q` 1191 ++ RW_TAC resq_ss [curve_add_def] 1192 ++ UNABBREV_ALL_TAC 1193 ++ RW_TAC alg_ss [affine_case] 1194 ++ RW_TAC alg_ss [] 1195 ++ Know `~(d = field_zero e.field)` 1196 >> (Q.UNABBREV_TAC `d` 1197 ++ RW_TAC alg_ss [field_sub_eq_zero]) 1198 ++ RW_TAC alg_ss [field_nonzero_eq, curve_affine, LET_DEF] 1199 ++ match_tac field_sub_eq_zero_imp 1200 ++ Q.EXISTS_TAC `e.field` 1201 ++ RW_TAC alg_ss [] 1202 ++ Q.UNABBREV_TAC `x''` 1203 ++ Q.UNABBREV_TAC `y''` 1204 ++ Q.UNABBREV_TAC `l` 1205 ++ Q.UNABBREV_TAC `m` 1206 ++ Count.apply (RW_TAC (field_div_elim_ss context) []) 1207 ++ Q.UNABBREV_TAC `d` 1208 ++ POP_ASSUM (K ALL_TAC) 1209 ++ Q.PAT_ASSUM `affine X Y IN Z` MP_TAC 1210 ++ Q.PAT_ASSUM `affine X Y IN Z` MP_TAC 1211 ++ ASM_SIMP_TAC alg_ss [curve_affine_reduce] 1212 ++ SIMP_TAC bool_ss [AND_IMP_INTRO, GSYM CONJ_ASSOC] 1213 ++ with_flag (ORACLE_field_poly,true) 1214 (with_flag (subtypeTools.ORACLE,true) 1215 (Count.apply (ASM_SIMP_TAC (field_poly_basis_ss context) [])))); 1216 1217val context = subtypeTools.add_reduction2 curve_add_carrier context; 1218val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1219 1220val curve_double_zero = store_thm 1221 ("curve_double_zero", 1222 ``!e :: Curve. curve_double e (curve_zero e) = curve_zero e``, 1223 RW_TAC resq_ss [] 1224 ++ RW_TAC resq_ss [curve_double_def] 1225 ++ normalForms.REMOVE_ABBR_TAC 1226 ++ RW_TAC std_ss [] 1227 ++ RW_TAC alg_ss [affine_case]); 1228 1229val context = subtypeTools.add_rewrite2 curve_double_zero context; 1230val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1231 1232val curve_add_lzero = store_thm 1233 ("curve_add_lzero", 1234 ``!e :: Curve. !p :: curve_points e. curve_add e (curve_zero e) p = p``, 1235 RW_TAC resq_ss [] 1236 ++ ec_cases_on `e` `p` 1237 ++ RW_TAC resq_ss [curve_add_def] 1238 ++ UNABBREV_ALL_TAC 1239 ++ RW_TAC alg_ss [affine_case]); 1240 1241val context = subtypeTools.add_rewrite2 curve_add_lzero context; 1242val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1243 1244val curve_add_lneg = store_thm 1245 ("curve_add_lneg", 1246 ``!e :: Curve. !p :: curve_points e. 1247 curve_add e (curve_neg e p) p = curve_zero e``, 1248 RW_TAC resq_ss [] 1249 ++ ec_cases_on `e` `p` 1250 ++ RW_TAC resq_ss [curve_add_def, curve_neg_def, LET_DEF] 1251 ++ RW_TAC alg_ss [] 1252 ++ UNABBREV_ALL_TAC 1253 ++ RW_TAC alg_ss [affine_case] 1254 ++ Q.PAT_ASSUM `X = Y` MP_TAC 1255 ++ RW_TAC alg_ss [affine_case, affine_eq] 1256 ++ RW_TAC alg_ss [curve_double_def, LET_DEF, affine_case, curve_distinct] 1257 ++ Q.PAT_ASSUM `X = Y` MP_TAC 1258 ++ PURE_ONCE_REWRITE_TAC [EQ_SYM_EQ] 1259 ++ Q.PAT_ASSUM `~(X = Y)` MP_TAC 1260 ++ RW_TAC alg_ss' []); 1261 1262val context = subtypeTools.add_rewrite2 curve_add_lneg context; 1263val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1264 1265val curve_add_comm = Count.apply store_thm 1266 ("curve_add_comm", 1267 ``!e :: Curve. !p q :: curve_points e. curve_add e p q = curve_add e q p``, 1268 RW_TAC resq_ss [] 1269 ++ Cases_on `p = q` >> RW_TAC alg_ss [] 1270 ++ RW_TAC alg_ss [curve_add_def] 1271 ++ UNABBREV_ALL_TAC 1272 ++ ec_cases_on `e` `p` 1273 ++ ec_cases_on `e` `q` 1274 ++ RW_TAC resq_ss [] 1275 ++ RW_TAC alg_ss [affine_case] 1276 ++ RW_TAC alg_ss [] 1277 ++ ASM_SIMP_TAC alg_ss [affine_eq] 1278 ++ Suff `(x''' = x'') /\ ((x''' = x'') ==> (y''' = y''))` 1279 >> RW_TAC std_ss [] 1280 ++ Know `~(d = field_zero e.field)` 1281 >> (Q.UNABBREV_TAC `d` 1282 ++ RW_TAC alg_ss [field_sub_eq_zero]) 1283 ++ Know `~(d' = field_zero e.field)` 1284 >> (Q.UNABBREV_TAC `d'` 1285 ++ RW_TAC alg_ss [field_sub_eq_zero]) 1286 ++ RW_TAC alg_ss [field_nonzero_eq] 1287 ++ match_tac field_sub_eq_zero_imp 1288 ++ Q.EXISTS_TAC `e.field` 1289 ++ RW_TAC alg_ss [] 1290 ++ Q.UNABBREV_TAC `x''` 1291 ++ Q.UNABBREV_TAC `y''` 1292 ++ Q.UNABBREV_TAC `l` 1293 ++ Q.UNABBREV_TAC `m` 1294 ++ TRY (Q.UNABBREV_TAC `x'''`) 1295 ++ Q.UNABBREV_TAC `y'''` 1296 ++ Q.UNABBREV_TAC `l'` 1297 ++ Q.UNABBREV_TAC `m'` 1298 ++ Count.apply (RW_TAC (field_div_elim_ss context) []) 1299 ++ Q.UNABBREV_TAC `d` 1300 ++ Q.UNABBREV_TAC `d'` 1301 ++ with_flag (ORACLE_field_poly,true) 1302 (with_flag (subtypeTools.ORACLE,true) 1303 (Count.apply (ASM_SIMP_TAC (field_poly_ss context []) [])))); 1304 1305val curve_add_rzero = store_thm 1306 ("curve_add_rzero", 1307 ``!e :: Curve. !p :: curve_points e. curve_add e p (curve_zero e) = p``, 1308 METIS_TAC [curve_add_lzero,curve_add_comm,curve_zero_carrier]); 1309 1310val context = subtypeTools.add_rewrite2 curve_add_rzero context; 1311val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1312 1313val curve_add_rneg = store_thm 1314 ("curve_add_rneg", 1315 ``!e :: Curve. !p :: curve_points e. 1316 curve_add e p (curve_neg e p) = curve_zero e``, 1317 METIS_TAC [curve_add_lneg,curve_add_comm,curve_neg_carrier]); 1318 1319val context = subtypeTools.add_rewrite2 curve_add_rneg context; 1320val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1321 1322(*** 1323val curve_add_assoc = store_thm 1324 ("curve_add_assoc", 1325 ``!e :: Curve. !p q r :: curve_points e. 1326 curve_add e p (curve_add e q r) = curve_add e (curve_add e p q) r``, 1327 RW_TAC resq_ss [] 1328 ++ ec_cases_on `e` `p` 1329 ++ ASM_SIMP_TAC alg_ss [] 1330 ++ STRIP_TAC >> RW_TAC alg_ss [curve_add_lzero] 1331 ++ ec_cases_on `e` `q` 1332 ++ ASM_SIMP_TAC alg_ss [] 1333 ++ STRIP_TAC >> RW_TAC alg_ss [curve_add_lzero, curve_add_rzero] 1334 ++ ec_cases_on `e` `r` 1335 ++ ASM_SIMP_TAC alg_ss [] 1336 ++ STRIP_TAC >> RW_TAC alg_ss [curve_add_rzero] 1337 ++ (Cases_on `p = q` ++ Cases_on `q = r`) 1338 >> (METIS_TAC [curve_add_comm,curve_add_carrier]) 1339 ++ RW_TAC alg_ss [] 1340 ++ clean_assumptions 1341 1342 1343 1344 1345 ++ REPEAT (POP_ASSUM MP_TAC) 1346 ++ RW_TAC resq_ss [] 1347 ++ RW_TAC alg_ss 1348 [curve_add_def, curve_double_def, affine_case, LET_DEF, 1349 affine_eq, curve_distinct] 1350 ++ REPEAT (POP_ASSUM MP_TAC) 1351 ++ RW_TAC alg_ss 1352 [curve_add_def, curve_double_def, affine_case, LET_DEF, 1353 affine_eq, curve_distinct] 1354 1355 ++ UNABBREV_ALL_TAC 1356 ++ ec_cases_on `e` `p` 1357 ++ ec_cases_on `e` `q` 1358 ++ RW_TAC resq_ss [] 1359 1360val curve_group = store_thm 1361 ("curve_group", 1362 ``!e :: Curve. curve_group e IN AbelianGroup``, 1363 RW_TAC resq_ss 1364 [curve_group_def, AbelianGroup_def, Group_def, 1365 GSPECIFICATION, combinTheory.K_THM] 1366 ++ RW_TAC alg_ss [] 1367, curve_zero_carrier, 1368 curve_add_carrier, curve] 1369 << [ 1370 1371 1372val context = subtypeTools.add_reduction2 curve_group context; 1373val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1374***) 1375 1376(*** 1377val curve_mult_eval = prove 1378 (``!e :: Curve. !p :: curve_points e. !n. 1379 curve_mult e p n = 1380 if n = 0 then curve_zero e 1381 else 1382 let p' = curve_double e p in 1383 let n' = n DIV 2 in 1384 if EVEN n then curve_mult e p' n' 1385 else curve_add e p (curve_mult e p' n')``, 1386 proof should just reference group_exp_eval 1387***) 1388 1389(*** 1390val curve_hom_field = store_thm 1391 ("curve_hom_field", 1392 ``!f1 f2 :: Field. !f :: FieldHom f1 f2. !e :: Curve. 1393 project_map f IN 1394 GroupHom (curve_group e) (curve_group (curve_map f e))``, 1395***) 1396 1397(*** 1398(* ------------------------------------------------------------------------- *) 1399(* Examples *) 1400(* ------------------------------------------------------------------------- *) 1401 1402(*** Testing the primality checker 1403val prime_65537 = Count.apply prove 1404 (``65537 IN Prime``, 1405 RW_TAC std_ss [Prime_def, GSPECIFICATION] 1406 ++ CONV_TAC prime_checker_conv); 1407***) 1408 1409(* From exercise VI.2.3 of Koblitz (1987) *) 1410 1411val example_prime_def = Define `example_prime = 751`; 1412 1413val example_field_def = Define `example_field = GF example_prime`; 1414 1415val example_curve_def = Define 1416 `example_curve = curve example_field 0 0 1 (example_prime - 1) 0`; 1417 1418val context = subtypeTools.add_rewrite2 example_prime_def context; 1419val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1420 1421val context = subtypeTools.add_rewrite2 example_field_def context; 1422val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1423 1424val example_prime = lemma 1425 (``example_prime IN Prime``, 1426 RW_TAC alg_ss [Prime_def, GSPECIFICATION] 1427 ++ CONV_TAC prime_checker_conv); 1428 1429val context = 1430 subtypeTools.add_reduction2 (SIMP_RULE alg_ss [] example_prime) context; 1431val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1432 1433val example_field = lemma 1434 (``example_field IN Field``, 1435 RW_TAC alg_ss []); 1436 1437val context = 1438 subtypeTools.add_reduction2 (SIMP_RULE alg_ss [] example_field) context; 1439val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1440 1441val example_curve = lemma 1442 (``example_curve IN Curve``, 1443 RW_TAC alg_ss 1444 [example_curve_def, Curve_def, GSPECIFICATION, discriminant_def, 1445 non_singular_def, LET_DEF] ++ 1446 RW_TAC alg_ss 1447 [LET_DEF, GF_alt, curve_b2_def, curve_b4_def, 1448 curve_b6_def, curve_b8_def, field_exp_small] ++ 1449 CONV_TAC EVAL); 1450 1451val context = subtypeTools.add_reduction2 example_curve context; 1452val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1453 1454val example_curve_field = lemma 1455 (``example_curve.field = example_field``, 1456 RW_TAC std_ss [curve_accessors, example_curve_def]); 1457 1458fun example_curve_pt pt = lemma 1459 (``^pt IN curve_points example_curve``, 1460 RW_TAC std_ss [GSYM example_curve_field] 1461 ++ MP_TAC (Q.ISPEC `example_curve` (CONV_RULE RES_FORALL_CONV curve_affine)) 1462 ++ SIMP_TAC alg_ss [] 1463 ++ RW_TAC alg_ss [example_curve_def, LET_DEF] 1464 ++ POP_ASSUM (K ALL_TAC) 1465 ++ RW_TAC alg_ss [field_exp_small] 1466 ++ RW_TAC alg_ss [GF_alt]); 1467 1468val execute_conv = 1469 SIMP_CONV 1470 alg_ss 1471 [GSYM example_curve_field, curve_neg_def, curve_add_def, 1472 curve_double_def, affine_case, LET_DEF] THENC 1473 SIMP_CONV 1474 alg_ss 1475 [example_curve_def, curve_accessors, GF_alt, affine_eq, CONS_11] THENC 1476 RAND_CONV EVAL; 1477 1478val pt1 = ``affine example_field [361; 383]`` 1479and pt2 = ``affine example_field [241; 605]``; 1480 1481val pt1_on_example_curve = example_curve_pt pt1 1482and pt2_on_example_curve = example_curve_pt pt2; 1483 1484Count.apply execute_conv ``curve_neg example_curve ^pt1``; 1485Count.apply example_curve_pt (rhs (concl it)); 1486 1487Count.apply execute_conv ``curve_add example_curve ^pt1 ^pt2``; 1488Count.apply example_curve_pt (rhs (concl it)); 1489 1490Count.apply execute_conv ``curve_double example_curve ^pt1``; 1491Count.apply example_curve_pt (rhs (concl it)); 1492 1493(* ------------------------------------------------------------------------- *) 1494(* A formalized version of random binary maps in HOL. *) 1495(* ------------------------------------------------------------------------- *) 1496 1497val () = Hol_datatype 1498 `randomMap = 1499 Leaf 1500 | Node of num => randomMap => 'a => 'b => randomMap`; 1501 1502val emptyMap_def = Define `emptyMap : ('a,'b) randomMap = Leaf`; 1503 1504val singletonMap_def = Define 1505 `singletonMap p a b : ('a,'b) randomMap = Node p Leaf a b Leaf`; 1506 1507(* ------------------------------------------------------------------------- *) 1508(* Compilable versions of multiword operations *) 1509(* ------------------------------------------------------------------------- *) 1510 1511fun compilable_multiword_operations words bits = 1512 1513(* ------------------------------------------------------------------------- *) 1514(* Compilable versions of elliptic curve operations *) 1515(* ------------------------------------------------------------------------- *) 1516 1517fun compilable_curve_operations prime words bits = 1518 let 1519 val {inject,add,mod,...} = compilable_multiword_operations words bits 1520 in 1521 end; 1522 1523val curve_add_example_def = Define 1524 `curve_add_example (x_1_1 : word5) x_1_2 y_1_1 y_1_2 x_2_1 x_2_2 y_2_1 y_2_2 = 1525 let x_1 = FCP i. if i=0 then x_1_1 else x_1_2 in 1526 let y_1 = FCP i. if i=0 then y_1_1 else y_1_2 in 1527 let x_2 = FCP i. if i=0 then x_2_1 else x_1_2 in 1528 let y_2 = FCP i. if i=0 then y_2_1 else y_2_2 in 1529 curve_add 1530 ec 1531 (affine (GF 751) [mw2n x_1; mw2n y_1]) 1532 (affine (GF 751) [mw2n x_2; mw2n y_2])`; 1533 1534val curve_add_example_compilable = 1535 CONV_RULE (RAND_CONV execute_conv) curve_add_example_def; 1536***) 1537 1538val _ = html_theory "elliptic"; 1539 1540val () = export_theory (); 1541