mit-plv/fiat-crypto

Generate single binary for all synthesis

JasonGross opened this issue · 0 comments

It would be nice to be able to call something like synthesize word-by-word-montgomery args or fiat-cryptography word-by-word-montgomery args or whatever, instead of having separate binaries for each synthesis pipeline. To do this, I think we should add another module below

fiat-crypto/src/CLI.v

Lines 1333 to 1339 in dcd5678

Definition PipelineMain
{supported_languages : supported_languagesT}
{A}
{io_driver : IODriverAPI A}
(argv : list string)
: A
:= Parameterized.PipelineMain argv.

that contains a main function that reads argv into prog::kind::args, checks to see if kind is one of the recognized kinds and delegates to the relevant main method if so, and otherwise printing out USAGE: $0 <possible options>. Presumably we can reuse the infrastructure for parsing output languages to parse the possible kinds. parse_argv might need to be generalized to take an implicit argument of how many arguments to ignore for the program name, or else we'll have to adjust the quoting at https://github.com/mit-plv/fiat-crypto/blob/dcd567854191ad4e1abd293ddecd2a8df1048d8d/src/CLI.v#L1015C19-L1015C19

We can then replace

Definition main_gen
{supported_languages : ForExtraction.supported_languagesT}
(PipelineMain : forall (A := _)
(argv : list String.string),
A)
: IO_unit
:= cast_io
(argv <- getArgs;
prog <- getProgName;
PipelineMain
(prog::argv)).

and
Definition main_gen
{supported_languages : ForExtraction.supported_languagesT}
(PipelineMain : forall (A := _)
(argv : list String.string),
A)
: unit
:= let argv := List.map string_to_Coq_string sys_argv in
PipelineMain argv.

with a single main function (for #1720 we'll probably want first a function that specializes to all of the language-specific calls, and then finally something that passes in Sys.argv? Or we can just have a separate StandaloneJSofOCaml that implements all the language-specific stuff separately?).