Improve documentation of binaries

2 files changed, 52 insertions, 6 deletions

diff --git a/src/Experiments/NewPipeline/CLI.v b/src/Experiments/NewPipeline/CLI.v
index f82d9e2a6..524def965 100644
--- a/src/Experiments/NewPipeline/CLI.v
+++ b/src/Experiments/NewPipeline/CLI.v
@@ -105,6 +105,21 @@ Module ForExtraction.
          => inr [res]
        end.
 
+  Definition curve_description_help
+    := "  curve_description       A string which will be prefixed to every function name generated".
+  Definition n_help
+    := "  n                       The number of limbs".
+  Definition s_help
+    := "  s                       The largest component of the prime (e.g., '2^255' in '2^255-19')".
+  Definition c_help
+    := "  c                       The semi-colon separated list of taps, each of which is specified as weight,value (no parentheses) (e.g., '2^96,1;1,-1' in '2^224 - 2^96 + 1')".
+  Definition machine_wordsize_help
+    := "  machine_wordsize        The machine bitwidth (e.g., 32 or 64)".
+  Definition function_to_synthesize_help (valid_names : string)
+    := "  function_to_synthesize  A list of functions that should be synthesized.  If no functions are given, all functions are synthesized."
+         ++ String.NewLine ++
+       "                            Valid options are " ++ valid_names.
+
   Module UnsaturatedSolinas.
     Definition PipelineLines
                (curve_description : string)
@@ -201,8 +216,18 @@ Module ForExtraction.
                error
          | nil => error ["empty argv"]
          | prog::args
-           => error ["Expected arguments curve_description, n, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog]
+           => error ["Expected arguments curve_description, n, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog;
+                       "";
+                       curve_description_help;
+                       n_help;
+                       s_help;
+                       c_help;
+                       machine_wordsize_help;
+                       function_to_synthesize_help UnsaturatedSolinas.valid_names;
+                       ""]
          end.
+
+
   End UnsaturatedSolinas.
 
   Module WordByWordMontgomery.
@@ -302,7 +327,14 @@ Module ForExtraction.
                error
          | nil => error ["empty argv"]
          | prog::args
-           => error ["Expected arguments curve_description, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog]
+           => error ["Expected arguments curve_description, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog;
+                       "";
+                       curve_description_help;
+                       s_help;
+                       c_help;
+                       machine_wordsize_help;
+                       function_to_synthesize_help WordByWordMontgomery.valid_names;
+                       ""]
          end.
   End WordByWordMontgomery.
 
@@ -396,7 +428,14 @@ Module ForExtraction.
                error
          | nil => error ["empty argv"]
          | prog::args
-           => error ["Expected arguments curve_description, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog]
+           => error ["Expected arguments curve_description, s, c, machine_wordsize, [function_to_synthesize*] got " ++ show false (List.length args) ++ " arguments in " ++ prog;
+                       "";
+                       curve_description_help;
+                       s_help;
+                       c_help;
+                       machine_wordsize_help;
+                       function_to_synthesize_help SaturatedSolinas.valid_names;
+                       ""]
          end.
   End SaturatedSolinas.
 End ForExtraction.
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 6eeee9f48..3f8da3a1a 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -1893,6 +1893,9 @@ Module Import UnsaturatedSolinas.
               ("to_bytes", srto_bytes);
               ("from_bytes", srfrom_bytes)].
 
+      Definition valid_names : string
+        := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions) ++ ", or 'carry_scmul' followed by a decimal literal".
+
       Definition synthesize_of_name (function_name_prefix : string) (name : string)
         : string * ErrorT Pipeline.ErrorMessage (list string * ToString.C.ident_infos)
         := fold_right
@@ -1904,7 +1907,7 @@ Module Import UnsaturatedSolinas.
              ((name,
                Error
                  (Pipeline.Invalid_argument
-                    ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ String.concat ", " (List.map (@fst _ _) known_functions) ++ ", or 'carry_scmul' followed by a decimal literal."))))
+                    ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ valid_names ++ "."))))
              ((map
                  (fun '(expected_name, resf) => if string_beq name expected_name then Some (resf function_name_prefix) else None)
                  known_functions)
@@ -2967,6 +2970,8 @@ Module WordByWordMontgomery.
               ("to_bytes", srto_bytes);
               ("from_bytes", srfrom_bytes)].
 
+      Definition valid_names : string := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions).
+
       Definition synthesize_of_name (function_name_prefix : string) (name : string)
         : string * ErrorT Pipeline.ErrorMessage (list string * ToString.C.ident_infos)
         := fold_right
@@ -2978,7 +2983,7 @@ Module WordByWordMontgomery.
              ((name,
                Error
                  (Pipeline.Invalid_argument
-                    ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ String.concat ", " (List.map (@fst _ _) known_functions)))))
+                    ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ valid_names ++ "."))))
              (map
                 (fun '(expected_name, resf) => if string_beq name expected_name then Some (resf function_name_prefix) else None)
                 known_functions).
@@ -3151,6 +3156,8 @@ Module SaturatedSolinas.
       Definition known_functions
         := [("mulmod", srmulmod)].
 
+      Definition valid_names : string := Eval compute in String.concat ", " (List.map (@fst _ _) known_functions).
+
       Definition synthesize_of_name (function_name_prefix : string) (name : string)
         : string * ErrorT Pipeline.ErrorMessage (list string * ToString.C.ident_infos)
         := fold_right
@@ -3162,7 +3169,7 @@ Module SaturatedSolinas.
              ((name,
                Error
                  (Pipeline.Invalid_argument
-                    ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ String.concat ", " (List.map (@fst _ _) known_functions) ++ "."))))
+                    ("Unrecognized request to synthesize """ ++ name ++ """; valid names are " ++ valid_names ++ "."))))
              (map
                 (fun '(expected_name, resf) => if string_beq name expected_name then Some (resf function_name_prefix) else None)
                 known_functions).