:: Operations of Points on Elliptic Curve in Affine Coordinates :: by Yuichi Futa , Hiroyuki Okazaki and Yasunari Shidama :: :: Received August 29, 2019 :: Copyright (c) 2019-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies CARD_1, FUNCT_1, RELAT_1, XBOOLE_0, ARYTM_3, NEWTON, MCART_1, SUBSET_1, ARYTM_1, XXREAL_0, BINOP_1, ZFMISC_1, SUPINF_2, ALGSTR_0, GROUP_1, MESFUNC1, INT_1, EC_PF_1, EC_PF_2, RLVECT_1, SETWISEO, ALGSTR_1, RECDEF_2, EC_PF_3; notations XBOOLE_0, SUBSET_1, FUNCT_1, MCART_1, FUNCT_2, BINOP_1, DOMAIN_1, SETWISEO, NUMBERS, XXREAL_0, NAT_1, INT_1, NEWTON, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, ALGSTR_1, BINOM, EC_PF_1, EC_PF_2; constructors NAT_D, NAT_3, REALSET1, GROUP_4, GR_CY_1, BHSP_1, POLYNOM5, ALGSTR_1, HURWITZ, FUNCT_4, RECDEF_1, RELSET_1, BINOM, SETWISEO, EC_PF_2; registrations XBOOLE_0, STRUCT_0, XREAL_0, ORDINAL1, INT_1, RELAT_1, FUNCT_2, ALGSTR_0, VECTSP_1, INT_3, NEWTON, SUBSET_1, EC_PF_2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: 1. Set of points on elliptic curve in affine coordinates reserve p for 5_or_greater Prime; reserve z for Element of EC_WParam p; theorem :: EC_PF_3:1 for p be Prime, a, b be Element of GF(p), P be Element of ProjCo(GF(p)) st (P = [0, 1, 0] or P`3_3 = 1) holds rep_pt(P) = P; theorem :: EC_PF_3:2 for p be 5_or_greater Prime, z be Element of EC_WParam p, P, O be Element of EC_SetProjCo(z`1,z`2,p) st O = [0, 1, 0] holds (P`3_3 = 0 iff P _EQ_ O); theorem :: EC_PF_3:3 for p be 5_or_greater Prime, z be Element of EC_WParam p, P be Element of EC_SetProjCo(z`1,z`2,p) holds (P`3_3 = 0 implies P _EQ_ compell_ProjCo(z,p).P); theorem :: EC_PF_3:4 for P, O be Element of EC_SetProjCo(z`1,z`2,p) st O = [0, 1, 0] holds addell_ProjCo(z,p).(P,compell_ProjCo(z,p).P) _EQ_ O; definition let p be 5_or_greater Prime; let z be Element of EC_WParam p; func EC_SetAffCo(z,p) -> non empty Subset of EC_SetProjCo(z`1,z`2,p) equals :: EC_PF_3:def 1 {P where P is Element of EC_SetProjCo(z`1,z`2,p) : P`3_3 = 1 or P = [0,1,0] }; end; theorem :: EC_PF_3:5 [0, 1, 0] is Element of EC_SetAffCo(z,p); theorem :: EC_PF_3:6 for p be 5_or_greater Prime, z be Element of EC_WParam p, P be Element of EC_SetProjCo(z`1,z`2,p) holds rep_pt(P) is Element of EC_SetAffCo(z,p); theorem :: EC_PF_3:7 for p be 5_or_greater Prime, z be Element of EC_WParam p, P be Element of EC_SetProjCo(z`1,z`2,p) st P in EC_SetAffCo(z,p) holds rep_pt(P) = P; theorem :: EC_PF_3:8 for P, O being Element of EC_SetProjCo(z`1,z`2,p) st O = [0, 1, 0] & not P _EQ_ O holds (rep_pt(P))`3_3 = 1; theorem :: EC_PF_3:9 for P, O being Element of EC_SetProjCo(z`1,z`2,p) st O = [0, 1, 0] & rep_pt(P) _EQ_ O holds rep_pt(P) = O & P _EQ_ O; theorem :: EC_PF_3:10 for P being Element of ProjCo(GF(p)) holds rep_pt(rep_pt(P)) = rep_pt(P); theorem :: EC_PF_3:11 for P, Q being Element of EC_SetProjCo(z`1,z`2,p) st rep_pt(P) _EQ_ rep_pt(Q) holds rep_pt(P) = rep_pt(Q); definition let p be 5_or_greater Prime, z be Element of EC_WParam p; func compell_AffCo(z,p) -> UnOp of EC_SetAffCo(z,p) means :: EC_PF_3:def 2 for P be Element of EC_SetAffCo(z,p) holds it.P = rep_pt(compell_ProjCo(z,p).P); end; definition let p be 5_or_greater Prime, z be Element of EC_WParam p; let F be Function of EC_SetAffCo(z,p), EC_SetAffCo(z,p); let P be Element of EC_SetAffCo(z,p); redefine func F.P -> Element of EC_SetAffCo(z,p); end; definition let p be 5_or_greater Prime, z be Element of EC_WParam p; func addell_AffCo(z,p) -> BinOp of EC_SetAffCo(z,p) means :: EC_PF_3:def 3 for P, Q be Element of EC_SetAffCo(z,p) holds it.(P,Q) = rep_pt(addell_ProjCo(z,p).(P,Q)); end; definition let p be 5_or_greater Prime, z be Element of EC_WParam p; let F be Function of [:EC_SetAffCo(z,p),EC_SetAffCo(z,p):], EC_SetAffCo(z,p); let Q,R be Element of EC_SetAffCo(z,p); redefine func F.(Q,R) -> Element of EC_SetAffCo(z,p); end; theorem :: EC_PF_3:12 for P, O being Element of EC_SetProjCo(z`1,z`2,p) st O = [0, 1, 0] holds addell_ProjCo(z,p).(P,O) _EQ_ P & addell_ProjCo(z,p).(O,P) _EQ_ P; theorem :: EC_PF_3:13 for P, O being Element of EC_SetAffCo(z,p) st O = [0, 1, 0] holds addell_AffCo(z,p).(O,P) = P; theorem :: EC_PF_3:14 for P, O being Element of EC_SetAffCo(z,p) st O = [0, 1, 0] holds addell_AffCo(z,p).(P,O) = P; theorem :: EC_PF_3:15 for O being Element of EC_SetAffCo(z,p) st O = [0, 1, 0] holds O is_a_unity_wrt addell_AffCo(z,p); theorem :: EC_PF_3:16 for P, O be Element of EC_SetAffCo(z,p) st O = [0, 1, 0] holds addell_AffCo(z,p).(P,compell_AffCo(z,p).P) = O; begin :: 2. Commutative property of operations of points on elliptic curve theorem :: EC_PF_3:17 for p be 5_or_greater Prime, z be Element of EC_WParam p, P, Q, O, PQ, QP being Element of EC_SetProjCo(z`1,z`2,p) st O = [0, 1, 0] & not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q holds (PQ = addell_ProjCo(z,p).(P,Q) & QP = addell_ProjCo(z,p).(Q,P)) implies QP`1_3 = -PQ`1_3 & QP`2_3 = -PQ`2_3 & QP`3_3 = -PQ`3_3; theorem :: EC_PF_3:18 for P, Q, O, PQ, QP being Element of EC_SetProjCo(z`1,z`2,p), d being Element of GF(p) st O = [0, 1, 0] & d <> 0.GF(p) & (Q`1_3) = d*(P`1_3) & (Q`2_3) = d*(P`2_3) & (Q`3_3) = d*(P`3_3) & not P _EQ_ O & not Q _EQ_ O & P _EQ_ Q & PQ = addell_ProjCo(z,p).(P,Q) & QP = addell_ProjCo(z,p).(Q,P) holds (QP`1_3) = (d |^6)*(PQ`1_3) & (QP`2_3) = (d |^6)*(PQ`2_3) & (QP`3_3) = (d |^6)*(PQ`3_3); theorem :: EC_PF_3:19 for P, Q being Element of EC_SetProjCo(z`1,z`2,p) holds addell_ProjCo(z,p).(P,Q) _EQ_ addell_ProjCo(z,p).(Q,P); theorem :: EC_PF_3:20 for P, Q being Element of EC_SetAffCo(z,p) holds addell_AffCo(z,p).(P,Q) = addell_AffCo(z,p).(Q,P); registration let p be 5_or_greater Prime, z be Element of EC_WParam p; cluster addell_AffCo(z,p) -> non empty commutative having_a_unity; end; definition let p be 5_or_greater Prime, z be Element of EC_WParam p; func 0_EC(z,p) -> Element of EC_SetAffCo(z,p) equals :: EC_PF_3:def 4 [0,1,0]; end; registration let p, z; cluster addMagma (# EC_SetAffCo(z,p), addell_AffCo(z,p) #) -> Abelian; cluster addLoopStr (# EC_SetAffCo(z,p), addell_AffCo(z,p), 0_EC(z,p) #) -> left_zeroed right_zeroed; end; registration let p,z; cluster addLoopStr (# EC_SetAffCo(z,p), addell_AffCo(z,p), 0_EC(z,p) #) -> complementable; end; registration let p be 5_or_greater Prime, z be Element of EC_WParam p; cluster multMagma (# EC_SetAffCo(z,p), addell_AffCo(z,p) #) -> unital; end; theorem :: EC_PF_3:21 for p be 5_or_greater Prime, z be Element of EC_WParam p holds 1_( multMagma (# EC_SetAffCo(z,p), addell_AffCo(z,p) #) ) = 0_EC(z,p); registration let p be 5_or_greater Prime, z be Element of EC_WParam p; cluster multMagma (# EC_SetAffCo(z,p), addell_AffCo(z,p) #) -> commutative Group-like non empty; end; theorem :: EC_PF_3:22 for P1, P2, Q being Element of EC_SetProjCo(z`1,z`2,p) st P1 _EQ_ P2 holds addell_ProjCo(z,p).(P1,Q) _EQ_ addell_ProjCo(z,p).(P2,Q); theorem :: EC_PF_3:23 for P, Q1, Q2 being Element of EC_SetProjCo(z`1,z`2,p) st Q1 _EQ_ Q2 holds addell_ProjCo(z,p).(P,Q1) _EQ_ addell_ProjCo(z,p).(P,Q2); theorem :: EC_PF_3:24 for P1, P2, Q1, Q2 being Element of EC_SetProjCo(z`1,z`2,p) st P1 _EQ_ P2 & Q1 _EQ_ Q2 holds addell_ProjCo(z,p).(P1,Q1) _EQ_ addell_ProjCo(z,p).(P2,Q2); theorem :: EC_PF_3:25 for P, O being Element of EC_SetProjCo(z`1,z`2,p) st O = [0, 1, 0] holds P _EQ_ O iff compell_ProjCo(z,p).P _EQ_ O; theorem :: EC_PF_3:26 for P, Q being Element of EC_SetProjCo(z`1,z`2,p), a being Element of GF(p) st a <> 0.GF(p) & P`1_3 = a * (Q`1_3) & P`2_3 = a * (Q`2_3) & P`3_3 = a * (Q`3_3) holds P _EQ_ Q; theorem :: EC_PF_3:27 for P, Q being Element of EC_SetProjCo(z`1,z`2,p), g2, gf1, gf2, gf3 being Element of GF(p) st not P _EQ_ Q & P`3_3 = 1 & Q`3_3 = 1 & g2 = 2 mod p & gf1 = Q`2_3 - P`2_3 & gf2 = Q`1_3 - P`1_3 & gf3 = (gf1 |^2) - (gf2 |^3) - g2*(gf2 |^2)*(P`1_3) holds addell_ProjCo(z,p).(P,Q) = [gf2*gf3, gf1 * ((gf2 |^2)*(P`1_3)-gf3) - (gf2 |^3)*(P`2_3), gf2 |^3]; theorem :: EC_PF_3:28 for P, Q being Element of EC_SetProjCo(z`1,z`2,p), g2, g3, g4, g8, gf1, gf2, gf3, gf4 being Element of GF(p) st P _EQ_ Q & P`3_3 = 1 & Q`3_3 = 1 & g2 = 2 mod p & g3 = 3 mod p & g4 = 4 mod p & g8 = 8 mod p & gf1 = z`1 + g3*(P`1_3 |^2) & gf2 = P`2_3 & gf3 = P`1_3*(P`2_3)*gf2 & gf4 = (gf1 |^2) - g8*gf3 holds addell_ProjCo(z,p).(P,Q) = [g2*gf4*gf2, gf1*(g4 * gf3-gf4) - g8*(P`2_3 |^2)*(gf2 |^2), g8*(gf2 |^3)]; theorem :: EC_PF_3:29 for P, Q being Element of EC_SetProjCo(z`1,z`2,p) st P`3_3 = 1 & Q`3_3 = 1 holds compell_ProjCo(z,p).(addell_ProjCo(z,p).(P,Q)) _EQ_ addell_ProjCo(z,p).(compell_ProjCo(z,p).P,compell_ProjCo(z,p).Q); theorem :: EC_PF_3:30 for P, Q being Element of EC_SetProjCo(z`1,z`2,p) holds compell_ProjCo(z,p).(addell_ProjCo(z,p).(P,Q)) _EQ_ addell_ProjCo(z,p).(compell_ProjCo(z,p).P,compell_ProjCo(z,p).Q); theorem :: EC_PF_3:31 for P, O being Element of EC_SetProjCo(z`1,z`2,p) st O = [0, 1, 0] & not P _EQ_ O holds (P`2_3 = 0.GF(p) iff addell_ProjCo(z,p).(P,P) _EQ_ O);