Also display the carry chain in a comment

10 files changed, 38 insertions, 15 deletions

diff --git a/curve25519_32.c b/curve25519_32.c
index 820a5c9bb..83453d82b 100644
--- a/curve25519_32.c
+++ b/curve25519_32.c
@@ -6,6 +6,9 @@
 /* c = [(1, 19)] (from "1,19") */
 /* machine_wordsize = 32 (from "32") */
 
+/* Computed values: */
+/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 0, 1] */
+
 #include <stdint.h>
 typedef unsigned char fiat_25519_uint1;
 typedef signed char fiat_25519_int1;
diff --git a/curve25519_64.c b/curve25519_64.c
index 23bf361d8..59beaf93a 100644
--- a/curve25519_64.c
+++ b/curve25519_64.c
@@ -6,6 +6,9 @@
 /* c = [(1, 19)] (from "1,19") */
 /* machine_wordsize = 64 (from "64") */
 
+/* Computed values: */
+/* carry_chain = [0, 1, 2, 3, 4, 0, 1] */
+
 #include <stdint.h>
 typedef unsigned char fiat_25519_uint1;
 typedef signed char fiat_25519_int1;
diff --git a/p448_solinas_64.c b/p448_solinas_64.c
index af57a7611..37cb13e10 100644
--- a/p448_solinas_64.c
+++ b/p448_solinas_64.c
@@ -6,6 +6,9 @@
 /* c = [(26959946667150639794667015087019630673637144422540572481103610249216, 1), (1, 1)] (from "2^224,1;1,1") */
 /* machine_wordsize = 64 (from "64") */
 
+/* Computed values: */
+/* carry_chain = [3, 7, 4, 0, 5, 1, 6, 2, 7, 3, 4, 0] */
+
 #include <stdint.h>
 typedef unsigned char fiat_p448_uint1;
 typedef signed char fiat_p448_int1;
diff --git a/p521_32.c b/p521_32.c
index 7d929b584..6bc3ae0b4 100644
--- a/p521_32.c
+++ b/p521_32.c
@@ -6,6 +6,9 @@
 /* c = [(1, 1)] (from "1,1") */
 /* machine_wordsize = 32 (from "32") */
 
+/* Computed values: */
+/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 0, 1] */
+
 #include <stdint.h>
 typedef unsigned char fiat_p521_uint1;
 typedef signed char fiat_p521_int1;
diff --git a/p521_64.c b/p521_64.c
index 503368e0d..971aee4c3 100644
--- a/p521_64.c
+++ b/p521_64.c
@@ -6,6 +6,9 @@
 /* c = [(1, 1)] (from "1,1") */
 /* machine_wordsize = 64 (from "64") */
 
+/* Computed values: */
+/* carry_chain = [0, 1, 2, 3, 4, 5, 6, 7, 8, 0, 1] */
+
 #include <stdint.h>
 typedef unsigned char fiat_p521_uint1;
 typedef signed char fiat_p521_int1;
diff --git a/src/CLI.v b/src/CLI.v
index 32cc3fd1e..41a705cc2 100644
--- a/src/CLI.v
+++ b/src/CLI.v
@@ -222,7 +222,7 @@ Module ForExtraction.
                            ; ("c", c, parse_c c:Dyn)] with
          | inr errs => inr errs
          | inl (n, machine_wordsize, s, c)
-           => let '(res, types_used)
+           => let '(extra_comment_header, res, types_used)
                  := UnsaturatedSolinas.Synthesize n s c machine_wordsize prefix requests in
              let header :=
                  ((["/* Autogenerated */";
@@ -233,8 +233,9 @@ Module ForExtraction.
                        "/* c = " ++ show false c ++ " (from """ ++ str_c ++ """) */";
                        "/* machine_wordsize = " ++ show false machine_wordsize ++ " (from """ ++ str_machine_wordsize ++ """) */";
                        ""]%string)
-                     ++ ToString.C.String.typedef_header prefix types_used
-                     ++ [""])%list in
+                    ++ extra_comment_header
+                    ++ ToString.C.String.typedef_header prefix types_used
+                    ++ [""])%list in
              inl
                ([("check_args" ++ NewLine ++ String.concat NewLine header,
                   UnsaturatedSolinas.check_args
@@ -323,7 +324,7 @@ Module ForExtraction.
                              ("m", m, parse_m m:Dyn)] with
          | inr errs => inr errs
          | inl (machine_wordsize, m)
-           => let '(res, types_used)
+           => let '(extra_comment_header, res, types_used)
                   := WordByWordMontgomery.Synthesize m machine_wordsize prefix requests in
              let header :=
                  ((["/* Autogenerated */";
@@ -339,8 +340,9 @@ Module ForExtraction.
                        "/*   All functions also ensure that these two properties are true of  */";
                        "/*   return values.                                                   */";
                        ""]%string)
-                     ++ ToString.C.String.typedef_header prefix types_used
-                     ++ [""])%list in
+                    ++ extra_comment_header
+                    ++ ToString.C.String.typedef_header prefix types_used
+                    ++ [""])%list in
              inl
                ([("check_args" ++ NewLine ++ String.concat NewLine header,
                   WordByWordMontgomery.check_args
@@ -424,7 +426,7 @@ Module ForExtraction.
                            ; ("c", c, parse_c c:Dyn)] with
          | inr errs => inr errs
          | inl (machine_wordsize, s, c)
-           => let '(res, types_used)
+           => let '(extra_comment_header, res, types_used)
                  := SaturatedSolinas.Synthesize s c machine_wordsize prefix requests in
              let header :=
                  ((["/* Autogenerated */";
@@ -434,6 +436,7 @@ Module ForExtraction.
                       "/* c = " ++ show false c ++ " (from """ ++ str_c ++ """) */";
                       "/* machine_wordsize = " ++ show false machine_wordsize ++ " (from """ ++ str_machine_wordsize ++ """) */";
                       ""]%string)
+                    ++ extra_comment_header
                     ++ ToString.C.String.typedef_header prefix types_used
                     ++ [""])%list in
              inl
diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v
index 4afa64433..f36f4cb9c 100644
--- a/src/PushButtonSynthesis/Primitives.v
+++ b/src/PushButtonSynthesis/Primitives.v
@@ -369,15 +369,16 @@ Section __.
 
     (** Note: If you change the name or type signature of this
           function, you will need to update the code in CLI.v *)
-    Definition Synthesize (function_name_prefix : string) (requests : list string)
-      : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *)
+    Definition Synthesize (comment_header : list string) (function_name_prefix : string) (requests : list string)
+      : list string (* comment header *) * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *)
       := let ls := match requests with
                    | nil => List.map (fun '(_, sr) => sr function_name_prefix) known_functions
                    | requests => List.map (synthesize_of_name function_name_prefix) requests
                    end in
          let infos := aggregate_infos ls in
          let '(extra_ls, extra_bit_widths) := extra_synthesis function_name_prefix infos in
-         (extra_ls ++ List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls,
+         (comment_header,
+          extra_ls ++ List.map (fun '(name, res) => (name, (res <- res; Success (fst res))%error)) ls,
           PositiveSet.union extra_bit_widths (ToString.C.bitwidths_used infos)).
   End for_stringification.
 End __.
diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v
index bcb93c4a1..334c2a475 100644
--- a/src/PushButtonSynthesis/SaturatedSolinas.v
+++ b/src/PushButtonSynthesis/SaturatedSolinas.v
@@ -176,9 +176,9 @@ Section __.
     (** Note: If you change the name or type signature of this
           function, you will need to update the code in CLI.v *)
     Definition Synthesize (function_name_prefix : string) (requests : list string)
-      : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *)
+      : list string * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *)
       := Primitives.Synthesize
            machine_wordsize valid_names known_functions (fun _ => nil)
-           function_name_prefix requests.
+           [] function_name_prefix requests.
   End for_stringification.
 End __.
diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v
index cd70771d2..8923aa10e 100644
--- a/src/PushButtonSynthesis/UnsaturatedSolinas.v
+++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v
@@ -13,6 +13,7 @@ Require Import Crypto.Util.ListUtil.FoldBool.
 Require Import Crypto.Util.Strings.Decimal.
 Require Import Crypto.Util.Strings.Equality.
 Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.Strings.Show.
 Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.Zselect.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
@@ -623,9 +624,12 @@ else:
     (** Note: If you change the name or type signature of this
           function, you will need to update the code in CLI.v *)
     Definition Synthesize (function_name_prefix : string) (requests : list string)
-      : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *)
+      : list string * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *)
       := Primitives.Synthesize
            machine_wordsize valid_names known_functions (extra_special_synthesis function_name_prefix)
+           ["/* Computed values: */";
+              "/* carry_chain = " ++ show false idxs ++ " */";
+              ""]%string
            function_name_prefix requests.
   End for_stringification.
 End __.
diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v
index 3b28329c5..a97c829e2 100644
--- a/src/PushButtonSynthesis/WordByWordMontgomery.v
+++ b/src/PushButtonSynthesis/WordByWordMontgomery.v
@@ -754,9 +754,9 @@ Section __.
     (** Note: If you change the name or type signature of this
           function, you will need to update the code in CLI.v *)
     Definition Synthesize (function_name_prefix : string) (requests : list string)
-      : list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *)
+      : list string * list (string * Pipeline.ErrorT (list string)) * PositiveSet.t (* types used *)
       := Primitives.Synthesize
            machine_wordsize valid_names known_functions (fun _ => nil)
-           function_name_prefix requests.
+           [] function_name_prefix requests.
   End for_stringification.
 End __.