From f1e7bdf11d972dbdd444426a74d232e0b7a36085 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Jun 2019 03:38:27 -0400 Subject: [PATCH] Update to display `s` and weights in `c` as 2^* As per https://github.com/mit-plv/fiat-crypto/pull/552#issuecomment-498529650 --- curve25519_32.c | 2 +- curve25519_64.c | 2 +- p448_solinas_64.c | 2 +- p521_32.c | 2 +- p521_64.c | 2 +- src/CLI.v | 9 ++++++--- src/Util/Strings/Show.v | 41 +++++++++++++++++++++++++++++++++++++++++ 7 files changed, 52 insertions(+), 8 deletions(-) diff --git a/curve25519_32.c b/curve25519_32.c index 5d3c190bfb..abdd0fe9c0 100644 --- a/curve25519_32.c +++ b/curve25519_32.c @@ -2,7 +2,7 @@ /* curve description: 25519 */ /* requested operations: carry_mul, carry_square, carry_scmul121666, carry, add, sub, opp, selectznz, to_bytes, from_bytes */ /* n = 10 (from "10") */ -/* s-c = 0x8000000000000000000000000000000000000000000000000000000000000000 - [(1, 19)] (from "2^255 - 19") */ +/* s-c = 2^255 - [(1, 19)] (from "2^255 - 19") */ /* machine_wordsize = 32 (from "32") */ /* Computed values: */ diff --git a/curve25519_64.c b/curve25519_64.c index 6f299bbfd5..6199ce4de4 100644 --- a/curve25519_64.c +++ b/curve25519_64.c @@ -2,7 +2,7 @@ /* curve description: 25519 */ /* requested operations: carry_mul, carry_square, carry_scmul121666, carry, add, sub, opp, selectznz, to_bytes, from_bytes */ /* n = 5 (from "5") */ -/* s-c = 0x8000000000000000000000000000000000000000000000000000000000000000 - [(1, 19)] (from "2^255 - 19") */ +/* s-c = 2^255 - [(1, 19)] (from "2^255 - 19") */ /* machine_wordsize = 64 (from "64") */ /* Computed values: */ diff --git a/p448_solinas_64.c b/p448_solinas_64.c index 6ac6f11389..f2b2b6ef8a 100644 --- a/p448_solinas_64.c +++ b/p448_solinas_64.c @@ -2,7 +2,7 @@ /* curve description: p448 */ /* requested operations: (all) */ /* n = 8 (from "8") */ -/* s-c = 0x10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 - [(26959946667150639794667015087019630673637144422540572481103610249216, 1), (1, 1)] (from "2^448 - 2^224 - 1") */ +/* s-c = 2^448 - [(2^224, 1), (1, 1)] (from "2^448 - 2^224 - 1") */ /* machine_wordsize = 64 (from "64") */ /* Computed values: */ diff --git a/p521_32.c b/p521_32.c index aaca4f2d6b..c05de6e19f 100644 --- a/p521_32.c +++ b/p521_32.c @@ -2,7 +2,7 @@ /* curve description: p521 */ /* requested operations: (all) */ /* n = 17 (from "17") */ -/* s-c = 0x20000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 - [(1, 1)] (from "2^521 - 1") */ +/* s-c = 2^521 - [(1, 1)] (from "2^521 - 1") */ /* machine_wordsize = 32 (from "32") */ /* Computed values: */ diff --git a/p521_64.c b/p521_64.c index 400b65fad8..6370b9c302 100644 --- a/p521_64.c +++ b/p521_64.c @@ -2,7 +2,7 @@ /* curve description: p521 */ /* requested operations: (all) */ /* n = 9 (from "9") */ -/* s-c = 0x20000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 - [(1, 1)] (from "2^521 - 1") */ +/* s-c = 2^521 - [(1, 1)] (from "2^521 - 1") */ /* machine_wordsize = 64 (from "64") */ /* Computed values: */ diff --git a/src/CLI.v b/src/CLI.v index ecb2cc27b7..8c663d946e 100644 --- a/src/CLI.v +++ b/src/CLI.v @@ -68,6 +68,9 @@ Module ForExtraction. Definition parse_m (s : string) : option Z := parseZ_arith s. + Definition show_c : Show (list (Z * Z)) + := @show_list _ (@show_prod _ _ PowersOfTwo.show_Z Decimal.show_Z). + Local Open Scope string_scope. Local Notation NewLine := (String "010" "") (only parsing). @@ -109,7 +112,7 @@ Module ForExtraction. Definition n_help := " n The number of limbs". Definition sc_help - := " s-c The prime, which must make exponentiation explicit (e.g., '2^255 - 19')". + := " s-c The prime, which must be expressed as a difference of a power of two and a small field element (e.g., '2^255 - 19', '2^448 - 2^224 - 1')". Definition m_help := " m The prime (e.g., '2^434 - (2^216*3^137 - 1)')". Definition machine_wordsize_help @@ -197,7 +200,7 @@ Module ForExtraction. "/* curve description: " ++ curve_description ++ " */"; "/* requested operations: " ++ show_requests ++ " */"; "/* n = " ++ show false n ++ " (from """ ++ str_n ++ """) */"; - "/* s-c = " ++ Hex.show_Z false s ++ " - " ++ show false c ++ " (from """ ++ str_sc ++ """) */"; + "/* s-c = " ++ PowersOfTwo.show_Z false s ++ " - " ++ show_c false c ++ " (from """ ++ str_sc ++ """) */"; "/* machine_wordsize = " ++ show false machine_wordsize ++ " (from """ ++ str_machine_wordsize ++ """) */"; ""]%string) ++ extra_comment_header @@ -393,7 +396,7 @@ Module ForExtraction. ((["/* Autogenerated */"; "/* curve description: " ++ curve_description ++ " */"; "/* requested operations: " ++ show_requests ++ " */"; - "/* s-c = " ++ Hex.show_Z false s ++ " - " ++ show false c ++ " (from """ ++ str_sc ++ """) */"; + "/* s-c = " ++ PowersOfTwo.show_Z false s ++ " - " ++ show_c false c ++ " (from """ ++ str_sc ++ """) */"; "/* machine_wordsize = " ++ show false machine_wordsize ++ " (from """ ++ str_machine_wordsize ++ """) */"; ""]%string) ++ extra_comment_header diff --git a/src/Util/Strings/Show.v b/src/Util/Strings/Show.v index 44929aed5c..22777a8e5f 100644 --- a/src/Util/Strings/Show.v +++ b/src/Util/Strings/Show.v @@ -128,3 +128,44 @@ Module Hex. parens (show_Z true (Qnum q) ++ " / " ++ show_positive true (Qden q)). End Hex. + +Module PowersOfTwo. + Fixpoint show_Z_up_to' (max : nat) (max_dec : Z) (neg : bool) : Show Z + := match max with + | O => Hex.show_Z + | S n' + => fun with_parens z + => if z (if z show_Z_up_to (S (Z.to_nat (Z.log2_up (Z.abs z)))) 32 with_parens z. +End PowersOfTwo.