1 files changed, 101 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/CLI.v b/src/Experiments/NewPipeline/CLI.v
index 79189637b..3d219049f 100644
--- a/src/Experiments/NewPipeline/CLI.v
+++ b/src/Experiments/NewPipeline/CLI.v
@@ -204,6 +204,107 @@ Module ForExtraction.
          end.
   End UnsaturatedSolinas.
 
+  Module WordByWordMontgomery.
+    Definition PipelineLines
+               (curve_description : string)
+               (s : string)
+               (c : string)
+               (machine_wordsize : string)
+               (requests : list string)
+    : list (string * Pipeline.ErrorT (list string)) + list string
+      := let prefix := ("fiat_" ++ curve_description ++ "_")%string in
+         let str_machine_wordsize := machine_wordsize in
+         let str_c := c in
+         let str_s := s in
+         let machine_wordsize := parse_machine_wordsize machine_wordsize in
+         let show_requests := match requests with nil => "(all)" | _ => String.concat ", " requests end in
+         match parse_s s, parse_c c with
+         | None, None
+           => inr ["Could not parse s (" ++ s ++ ") nor c (" ++ c ++ ")"]
+         | None, _
+           => inr ["Could not parse s (" ++ s ++ ")"]
+         | _, None
+           => inr ["Could not parse c (" ++ c ++ ")"]
+         | Some s, Some c
+           => let '(res, types_used)
+                 := WordByWordMontgomery.Synthesize s c machine_wordsize prefix requests in
+             let header :=
+                 ((["/* Autogenerated */";
+                       "/* curve description: " ++ curve_description ++ " */";
+                       "/* requested operations: " ++ show_requests ++ " */";
+                       "/* s = " ++ Hex.show_Z false s ++ " (from """ ++ str_s ++ """) */";
+                       "/* c = " ++ show false c ++ " (from """ ++ str_c ++ """) */";
+                       "/* machine_wordsize = " ++ show false machine_wordsize ++ " (from """ ++ str_machine_wordsize ++ """) */";
+                       "/*                                                                    */";
+                       "/* NOTE: In addition to the bounds specified above each function, all */";
+                       "/*   functions synthesized for this Montgomery arithmetic require the */";
+                       "/*   input to be strictly less than the prime modulus (s-c), and also */";
+                       "/*   require the input to be in the unique saturated representation.  */";
+                       "/*   All functions also ensure that these two properties are true of  */";
+                       "/*   return values.                                                   */";
+                       ""]%string)
+                     ++ ToString.C.String.typedef_header prefix types_used
+                     ++ [""])%list in
+             inl
+               ([("check_args" ++ NewLine ++ String.concat NewLine header,
+                  WordByWordMontgomery.check_args
+                    s c machine_wordsize
+                    (ErrorT.Success header))%string]
+                  ++ res)%list
+         end.
+
+    Definition ProcessedLines
+               (curve_description : string)
+               (s : string)
+               (c : string)
+               (machine_wordsize : string)
+               (requests : list string)
+      : list string + list string
+      := match CollectErrors (PipelineLines curve_description s c machine_wordsize requests) with
+         | inl ls
+           => inl
+               (List.map (fun s => String.concat NewLine s ++ NewLine ++ NewLine)
+                         ls)
+         | inr nil => inr nil
+         | inr (l :: ls)
+           => inr (l ++ (List.flat_map
+                           (fun e => NewLine :: e)
+                           ls))%list
+         end.
+
+    Definition Pipeline
+               {A}
+               (curve_description : string)
+               (s : string)
+               (c : string)
+               (machine_wordsize : string)
+               (requests : list string)
+               (success : list string -> A)
+               (error : list string -> A)
+      : A
+      := match ProcessedLines curve_description s c machine_wordsize requests with
+         | inl s => success s
+         | inr s => error s
+         end.
+
+    Definition PipelineMain
+               {A}
+               (argv : list string)
+               (success : list string -> A)
+               (error : list string -> A)
+      : A
+      := match argv with
+         | _::curve_description::s::c::machine_wordsize::requests
+           => Pipeline
+               curve_description s c machine_wordsize requests
+               success
+               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]
+         end.
+  End WordByWordMontgomery.
+
   Module SaturatedSolinas.
     Definition PipelineLines
                (curve_description : string)