Skip to content

Commit

Permalink
Added some alternative definitions of Jacobian-coordinate elliptic
Browse files Browse the repository at this point in the history 
curve operations with fewer special case distinctions,
"jacobian_add_unexceptional" and "jacobian_double_unexceptional". The
key theorems still work for these, with the exception of using the
addition formula for doubling, which still needs to be handled
separately. Also added a few miscelleneous arithmetical and machine
word theorems. New definitions:

        jacobian_add_unexceptional
        jacobian_double_unexceptional

and theorems:

        DIGITSUM_UNIQUE
        DIV_ADD_EQ
        DIV_ADD_EQ_EQ
        MOD_ADD_EQ
        MOD_ADD_EQ_EQ
        VAL_EXPAND_SUBWORDS
        VAL_SUBWORDS_EQ
        WEIERSTRASS_OF_JACOBIAN_ADD_UNEXCEPTIONAL
        WEIERSTRASS_OF_JACOBIAN_DOUBLE_UNEXCEPTIONAL
        WORD_SUBWORDS_EQ
        WORD_SUBWORD_ADD
  • Loading branch information
@jrh13
jrh13 committed Feb 22, 2024
1 parent 575f952 commit 3d231f3
Show file tree
Hide file tree
Showing 4 changed files with 298 additions and 1 deletion.
103 changes: 103 additions & 0 deletions CHANGES
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,109 @@
* page: https://github.com/jrh13/hol-light/commits/master *
* *****************************************************************

Wed 21st Feb 2024 EC/jacobian.ml

Added some alternative definitions of Jacobian-coordinate elliptic curve
operations with fewer special case distinctions, "jacobian_add_unexceptional"
and "jacobian_double_unexceptional". The key theorems still work for these,
with the exception of using the addition formula for doubling, which still
needs to be handled separately:

WEIERSTRASS_OF_JACOBIAN_ADD_UNEXCEPTIONAL =
|- !f a b p q.
field f /\ ~(ring_char f = 2) /\ ~(ring_char f = 3) /\
a IN ring_carrier f /\ b IN ring_carrier f /\
jacobian_point f p /\ jacobian_point f q /\
~(jacobian_eq f p q)
==> weierstrass_of_jacobian f (jacobian_add_unexceptional (f,a,b) p q) =
weierstrass_add (f,a,b)
(weierstrass_of_jacobian f p)
(weierstrass_of_jacobian f q)

WEIERSTRASS_OF_JACOBIAN_DOUBLE_UNEXCEPTIONAL =
|- !f a b p.
field f /\ ~(ring_char f = 2) /\ ~(ring_char f = 3) /\
a IN ring_carrier f /\ b IN ring_carrier f /\
jacobian_point f p
==> weierstrass_of_jacobian f (jacobian_double_unexceptional (f,a,b) p) =
weierstrass_add (f,a,b)
(weierstrass_of_jacobian f p)
(weierstrass_of_jacobian f p)

Wed 21st Feb 2024 calc_rat.ml, class.ml, define.ml, fusion.ml, int.ml, tactics.ml, Library/words.ml, Help/passim

Added an update from June Lee with two new tactics

NAME_ASSUMS_TAC - names unlabelled assumptions ("H0", "H1" etc.)

PRINT_GOAL_TAC - prints the current subgoal, useful for debugging

as well as several improvements in the error messages from automated
rules and tactics.

Wed 21st Feb 2024 Proofrecording/README

Fixed a broken link, thanks to Yiyuan Cao, in the Proofrecording
documentation, with an updated link to Chantal Keller's code for
replaying HOL Light proofs in Coq.

Tue 20th Feb 2024 Library/words.ml

Added a few additional word lemmas:

DIGITSUM_UNIQUE =
|- !B b c s n.
FINITE s /\ (!i. i IN s ==> b i < B) /\ (!i. i IN s ==> c i < B)
==> (nsum s (\i. B EXP i * b i) = nsum s (\i. B EXP i * c i) <=>
(!i. i IN s ==> b i = c i))

VAL_EXPAND_SUBWORDS =
|- !k m x.
dimindex (:M) = k /\ dimindex (:N) = k * m
==> nsum {i | i < m}
(\i. 2 EXP (k * i) * val (word_subword x (k * i,k))) =
val x

VAL_SUBWORDS_EQ =
|- !k m f x.
dimindex (:M) = k /\ dimindex (:N) = k * m
==> ((!i. i < m ==> val (word_subword x (k * i,k)) = f i) <=>
(!i. i < m ==> f i < 2 EXP k) /\
val x = nsum {i | i < m} (\i. 2 EXP (k * i) * f i))

WORD_SUBWORD_ADD =
|- !x y.
dimindex (:M) = len /\
pos + len <= dimindex (:N) /\
val x MOD 2 EXP pos + val y MOD 2 EXP pos < 2 EXP pos
==> word_subword (word_add x y) (pos,len) =
word_add (word_subword x (pos,len)) (word_subword y (pos,len))

WORD_SUBWORDS_EQ =
|- !k m f x.
dimindex (:M) = k /\ dimindex (:N) = k * m
==> ((!i. i < m ==> val (word_subword x (k * i,k)) = f i) <=>
(!i. i < m ==> f i < 2 EXP k) /\
word (nsum {i | i < m} (\i. 2 EXP (k * i) * f i)) = x)

Tue 13th Feb 2024 arith.ml

Added a few more conditions for distributing DIV or MOD over addition:

DIV_ADD_EQ =
|- !n x y. x MOD n + y MOD n < n ==> (x + y) DIV n = x DIV n + y DIV n

DIV_ADD_EQ_EQ =
|- !n x y.
(x + y) DIV n = x DIV n + y DIV n <=> n = 0 \/ x MOD n + y MOD n < n

MOD_ADD_EQ =
|- !n x y. x MOD n + y MOD n < n ==> (x + y) MOD n = x MOD n + y MOD n

MOD_ADD_EQ_EQ =
|- !n x y.
(x + y) MOD n = x MOD n + y MOD n <=> n = 0 \/ x MOD n + y MOD n < n

Tue 6th Feb 2024 Library/words.ml

Added a couple of little word lemmas:
Expand Down
95 changes: 95 additions & 0 deletions EC/jacobian.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -341,3 +341,98 @@ let JACOBIAN_OF_WEIERSTRASS_ADD = prove
JACOBIAN_POINT_ADD; WEIERSTRASS_POINT_ADD;
WEIERSTRASS_OF_JACOBIAN_ADD;
WEIERSTRASS_OF_JACOBIAN_OF_WEIERSTRASS]);;

(* ------------------------------------------------------------------------- *)
(* Some simpler variants that don't take such care over special cases. *)
(* ------------------------------------------------------------------------- *)

let jacobian_add_unexceptional = new_definition
`jacobian_add_unexceptional (f:A ring,a:A,b:A) (x1,y1,z1) (x2,y2,z2) =
if z1 = ring_0 f then (x2,y2,z2)
else if z2 = ring_0 f then (x1,y1,z1)
else
let r = ring_mul f x1 (ring_pow f z2 2)
and s = ring_mul f x2 (ring_pow f z1 2)
and t = ring_mul f y1 (ring_pow f z2 3)
and u = ring_mul f y2 (ring_pow f z1 3) in
let v = ring_sub f s r
and w = ring_sub f u t in
let x3 =
ring_add f
(ring_sub f (ring_neg f (ring_pow f v 3))
(ring_mul f (ring_of_num f 2) (ring_mul f r (ring_pow f v 2))))
(ring_pow f w 2) in
x3,
ring_add f (ring_mul f (ring_neg f t) (ring_pow f v 3))
(ring_mul f (ring_sub f (ring_mul f r (ring_pow f v 2)) x3) w),
ring_mul f v (ring_mul f z1 z2)`;;

let WEIERSTRASS_OF_JACOBIAN_ADD_UNEXCEPTIONAL = prove
(`!(f:A ring) a b p q.
field f /\ ~(ring_char f = 2) /\ ~(ring_char f = 3) /\
a IN ring_carrier f /\ b IN ring_carrier f /\
jacobian_point f p /\ jacobian_point f q /\
~(jacobian_eq f p q)
==> weierstrass_of_jacobian f (jacobian_add_unexceptional (f,a,b) p q) =
weierstrass_add (f,a,b)
(weierstrass_of_jacobian f p)
(weierstrass_of_jacobian f q)`,
REWRITE_TAC[FIELD_CHAR_NOT23; FORALL_PAIR_THM; jacobian_point] THEN
MAP_EVERY X_GEN_TAC
[`f:A ring`; `a:A`; `b:A`; `x1:A`; `y1:A`; `z1:A`;
`x2:A`; `y2:A`; `z2:A`] THEN
REWRITE_TAC[weierstrass_of_jacobian; jacobian_add_unexceptional] THEN
REWRITE_TAC[jacobian_eq] THEN
MAP_EVERY ASM_CASES_TAC [`z1:A = ring_0 f`; `z2:A = ring_0 f`] THEN
ASM_REWRITE_TAC[weierstrass_of_jacobian; weierstrass_add] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[jacobian_neg; jacobian_0] THEN
ASM_SIMP_TAC[ring_div; RING_INV_POW] THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
REPEAT LET_TAC THEN REWRITE_TAC[weierstrass_of_jacobian] THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
REWRITE_TAC[option_DISTINCT; option_INJ; PAIR_EQ] THEN
RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM]) THEN
REPEAT(FIRST_X_ASSUM(DISJ_CASES_TAC) ORELSE
FIRST_X_ASSUM(CONJUNCTS_THEN ASSUME_TAC)) THEN
FIELD_TAC THEN NOT_RING_CHAR_DIVIDES_TAC);;

let jacobian_double_unexceptional = new_definition
`jacobian_double_unexceptional (f:A ring,a:A,b:A) (x1,y1,z1) =
let v = ring_mul f (ring_of_num f 4) (ring_mul f x1 (ring_pow f y1 2))
and w =
ring_add f (ring_mul f (ring_of_num f 3) (ring_pow f x1 2))
(ring_mul f a (ring_pow f z1 4)) in
let x3 =
ring_add f (ring_mul f (ring_neg f (ring_of_num f 2)) v)
(ring_pow f w 2) in
x3,
ring_add f (ring_mul f (ring_neg f (ring_of_num f 8)) (ring_pow f y1 4))
(ring_mul f (ring_sub f v x3) w),
ring_mul f (ring_of_num f 2) (ring_mul f y1 z1)`;;

let WEIERSTRASS_OF_JACOBIAN_DOUBLE_UNEXCEPTIONAL = prove
(`!(f:A ring) a b p.
field f /\ ~(ring_char f = 2) /\ ~(ring_char f = 3) /\
a IN ring_carrier f /\ b IN ring_carrier f /\
jacobian_point f p
==> weierstrass_of_jacobian f (jacobian_double_unexceptional (f,a,b) p) =
weierstrass_add (f,a,b)
(weierstrass_of_jacobian f p)
(weierstrass_of_jacobian f p)`,
REWRITE_TAC[FIELD_CHAR_NOT23; FORALL_PAIR_THM; jacobian_point] THEN
MAP_EVERY X_GEN_TAC [`f:A ring`; `a:A`; `b:A`; `x1:A`; `y1:A`; `z1:A`] THEN
REWRITE_TAC[weierstrass_of_jacobian; jacobian_double_unexceptional] THEN
ASM_CASES_TAC `z1:A = ring_0 f` THEN
ASM_REWRITE_TAC[weierstrass_of_jacobian; weierstrass_add] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[jacobian_neg; jacobian_0] THEN
ASM_SIMP_TAC[ring_div; RING_INV_POW] THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
REPEAT LET_TAC THEN REWRITE_TAC[weierstrass_of_jacobian] THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
REWRITE_TAC[option_DISTINCT; option_INJ; PAIR_EQ] THEN
RULE_ASSUM_TAC(REWRITE_RULE[DE_MORGAN_THM]) THEN
REPEAT(FIRST_X_ASSUM(DISJ_CASES_TAC) ORELSE
FIRST_X_ASSUM(CONJUNCTS_THEN ASSUME_TAC)) THEN
FIELD_TAC THEN NOT_RING_CHAR_DIVIDES_TAC);;
83 changes: 82 additions & 1 deletion Library/words.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,6 +190,15 @@ let DIGITSUM_DIV_MOD = prove
ASM_REWRITE_TAC[EMPTY_GSPEC; NSUM_CLAUSES] THEN
REWRITE_TAC[SING_GSPEC; NSUM_SING; SUB_REFL; MULT_CLAUSES; EXP]);;

let DIGITSUM_UNIQUE = prove
(`!B b c s n.
FINITE s /\
(!i. i IN s ==> b i < B) /\
(!i. i IN s ==> c i < B)
==> (nsum s (\i. B EXP i * b i) = nsum s (\i. B EXP i * c i) <=>
!i. i IN s ==> b i = c i)`,
MESON_TAC[DIGITSUM_DIV_MOD; NSUM_EQ]);;

(* ------------------------------------------------------------------------- *)
(* Mapping a Boolean to the natural number 1 (true) or 0 (false) *)
(* ------------------------------------------------------------------------- *)
Expand Down Expand Up @@ -3413,7 +3422,7 @@ let WORD_BITWISE_TAC =
CONV_TAC TAUT;;

let WORD_BITWISE_RULE tm =
try
try
prove(tm,WORD_BITWISE_TAC)
with Failure m ->
failwith ("WORD_BITWISE_RULE `" ^ (string_of_term tm) ^ "`: " ^ m);;
Expand Down Expand Up @@ -4077,6 +4086,20 @@ let WORD_SUBWORD_NOT = prove
REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[DE_MORGAN_THM] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN ASM_ARITH_TAC);;

let WORD_SUBWORD_ADD = prove
(`!x y:N word.
dimindex(:M) = len /\ pos + len <= dimindex(:N) /\
val x MOD 2 EXP pos + val y MOD 2 EXP pos < 2 EXP pos
==> word_subword (word_add x y) (pos,len):M word =
word_add (word_subword x (pos,len))
(word_subword y (pos,len))`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[GSYM VAL_EQ; VAL_WORD_ADD; VAL_WORD_SUBWORD] THEN
FIRST_ASSUM SUBST1_TAC THEN REWRITE_TAC[ARITH_RULE `MIN n n = n`] THEN
CONV_TAC MOD_DOWN_CONV THEN ASM_SIMP_TAC[GSYM DIV_ADD_EQ] THEN
REWRITE_TAC[DIV_MOD; GSYM EXP_ADD; MOD_MOD_EXP_MIN] THEN
ASM_SIMP_TAC[ARITH_RULE `m <= n ==> MIN n m = m`]);;

let WORD_SUBWORD_AS_IWORD = prove
(`!(w:N word) pos len.
pos + len <= dimindex(:N)
Expand Down Expand Up @@ -4123,6 +4146,64 @@ let WORD_SXFROM_SUBWORD_AS_ISHR_SHL = prove
(CONJ_TAC THENL [ALL_TAC; STRIP_TAC THEN AP_THM_TAC THEN AP_TERM_TAC]) THEN
ASM_ARITH_TAC);;

let VAL_EXPAND_SUBWORDS = prove
(`!k m (x:N word).
dimindex(:M) = k /\ dimindex(:N) = k * m
==> nsum {i | i < m}
(\i. 2 EXP (k * i) *
val(word_subword x (k * i,k):M word)) =
val x`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[val_def; GSYM NSUM_LMUL; BIT_WORD_SUBWORD] THEN
POP_ASSUM_LIST(CONV_TAC o SUBS_CONV) THEN
REWRITE_TAC[MULT_ASSOC; GSYM EXP_ADD; ARITH_RULE `MIN n n = n`] THEN
SIMP_TAC[NSUM_NSUM_PRODUCT; FINITE_NUMSEG_LT] THEN
MATCH_MP_TAC NSUM_EQ_GENERAL_INVERSES THEN
MAP_EVERY EXISTS_TAC [`\(i,j). (k:num) * i + j`; `\n. n DIV k,n MOD k`] THEN
REWRITE_TAC[FORALL_IN_GSPEC] THEN
REWRITE_TAC[IN_ELIM_PAIR_THM; PAIR_EQ] THEN SIMP_TAC[IN_ELIM_THM] THEN
ASM_CASES_TAC `k = 0` THEN ASM_REWRITE_TAC[LT; MULT_CLAUSES] THEN
ASM_SIMP_TAC[DIV_MULT_ADD; DIVISION_SIMP; MOD_MULT_ADD; DIV_LT; MOD_LT] THEN
ASM_SIMP_TAC[MOD_LT_EQ; RDIV_LT_EQ; ADD_CLAUSES] THEN
REPEAT STRIP_TAC THEN TRANS_TAC LTE_TRANS `k * i + k:num` THEN
ASM_REWRITE_TAC[LT_ADD_LCANCEL] THEN
ASM_REWRITE_TAC[ARITH_RULE `k * i + k = k * (i + 1)`] THEN
REWRITE_TAC[LE_MULT_LCANCEL] THEN ASM_ARITH_TAC);;

let VAL_SUBWORDS_EQ = prove
(`!k m f (x:N word).
dimindex(:M) = k /\ dimindex(:N) = k * m
==> ((!i. i < m ==> val(word_subword x (k * i,k):M word) = f i) <=>
(!i. i < m ==> f i < 2 EXP k) /\
val x = nsum {i | i < m} (\i. 2 EXP (k * i) * f i))`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`!i. i < m ==> val(word_subword (x:N word) (k * i,k):M word) < 2 EXP k`
ASSUME_TAC THENL
[REPEAT(FIRST_X_ASSUM(SUBST1_TAC o SYM)) THEN REWRITE_TAC[VAL_BOUND];
ALL_TAC] THEN
MATCH_MP_TAC(TAUT `(p ==> q) /\ (q ==> (p <=> r)) ==> (p <=> q /\ r)`) THEN
CONJ_TAC THENL [ASM_MESON_TAC[]; DISCH_TAC] THEN
MP_TAC(SPECL [`k:num`; `m:num`; `x:N word`] VAL_EXPAND_SUBWORDS) THEN
ANTS_TAC THENL [ASM_MESON_TAC[]; DISCH_THEN(SUBST1_TAC o SYM)] THEN
ASM_SIMP_TAC[DIGITSUM_UNIQUE; EXP_MULT; IN_ELIM_THM; FINITE_NUMSEG_LT] THEN
MESON_TAC[]);;

let WORD_SUBWORDS_EQ = prove
(`!k m f (x:N word).
dimindex(:M) = k /\ dimindex(:N) = k * m
==> ((!i. i < m ==> val(word_subword x (k * i,k):M word) = f i) <=>
(!i. i < m ==> f i < 2 EXP k) /\
word(nsum {i | i < m} (\i. 2 EXP (k * i) * f i)) = x)`,
REPEAT GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP VAL_SUBWORDS_EQ th]) THEN
MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN
DISCH_TAC THEN REWRITE_TAC[GSYM VAL_EQ; VAL_WORD] THEN
CONV_TAC(RAND_CONV SYM_CONV) THEN AP_TERM_TAC THEN
CONV_TAC SYM_CONV THEN MATCH_MP_TAC MOD_LT THEN
FIRST_X_ASSUM(SUBST1_TAC o CONJUNCT2) THEN
ASM_SIMP_TAC[EXP_MULT; DIGITSUM_BOUND; IN_ELIM_THM; FINITE_NUMSEG_LT]);;

(* ------------------------------------------------------------------------- *)
(* Extract bottom len bits of x' and insert into x at position pos. *)
(* ------------------------------------------------------------------------- *)
Expand Down
18 changes: 18 additions & 0 deletions arith.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1508,6 +1508,24 @@ let DIV_ADD_MOD = prove
ASM_REWRITE_TAC[EQ_ADD_RCANCEL; EQ_ADD_LCANCEL; EQ_MULT_RCANCEL] THEN
REWRITE_TAC[EQ_SYM_EQ]);;

let MOD_ADD_EQ_EQ = prove
(`!n x y. (x + y) MOD n = x MOD n + y MOD n <=>
n = 0 \/ x MOD n + y MOD n < n`,
MESON_TAC[MOD_ZERO; MOD_EQ_SELF; MOD_ADD_MOD]);;

let DIV_ADD_EQ_EQ = prove
(`!n x y. (x + y) DIV n = x DIV n + y DIV n <=>
n = 0 \/ x MOD n + y MOD n < n`,
METIS_TAC[DIV_ZERO; ADD_CLAUSES; DIV_ADD_MOD; MOD_ADD_EQ_EQ]);;

let DIV_ADD_EQ = prove
(`!n x y. x MOD n + y MOD n < n ==> (x + y) DIV n = x DIV n + y DIV n`,
SIMP_TAC[DIV_ADD_EQ_EQ]);;

let MOD_ADD_EQ = prove
(`!n x y. x MOD n + y MOD n < n ==> (x + y) MOD n = x MOD n + y MOD n`,
SIMP_TAC[MOD_ADD_EQ_EQ]);;

let DIV_REFL = prove
(`!n. ~(n = 0) ==> (n DIV n = 1)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC DIV_UNIQ THEN
Expand Down

0 comments on commit 3d231f3

Please sign in to comment.