Update to display s and weights in c as 2^*

As per
#552 (comment)

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: */

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: */

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: */

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: */

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: */

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

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 <? max_dec
+               then Decimal.show_Z with_parens z
+               else if Z.abs (2^Z.log2_up z - z) <=? Z.abs (z - 2^Z.log2 z)
+                    then let log2z := Z.log2_up z in
+                         let z := 2^log2z - z in
+                         if z =? 0
+                         then "2^" ++ Decimal.show_Z false log2z
+                         else maybe_wrap_parens
+                                with_parens
+                                ("2^" ++ Decimal.show_Z false log2z
+                                      ++ (if neg then "+" else "-")
+                                      ++ show_Z_up_to' n' max_dec (negb neg) false z)
+                    else let log2z := Z.log2 z in
+                         let z := z - 2^log2z in
+                         if z =? 0
+                         then "2^" ++ Decimal.show_Z false log2z
+                         else maybe_wrap_parens
+                                with_parens
+                                ("2^" ++ Decimal.show_Z false log2z
+                                      ++ (if neg then "-" else "+")
+                                      ++ show_Z_up_to' n' max_dec neg false z)
+       end%Z%string.
+
+  Definition show_Z_up_to (max : nat) (max_dec : Z) : Show Z
+    := fun with_parens z
+       => (if z <? 0
+           then "-" ++ (show_Z_up_to' max max_dec false true (-z))
+           else if z =? 0
+                then "0"
+                else show_Z_up_to' max max_dec false with_parens z)%Z.
+
+  Definition show_Z : Show Z
+    := fun with_parens z => show_Z_up_to (S (Z.to_nat (Z.log2_up (Z.abs z)))) 32 with_parens z.
+End PowersOfTwo.