mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat
http://adam.chlipala.net/papers/FiatCryptoSP19/FiatCryptoSP19.pdf
Other
718 stars 147 forks source link

Generate single binary for all synthesis #1724

Closed JasonGross closed 1 year ago

JasonGross commented 1 year ago

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 https://github.com/mit-plv/fiat-crypto/blob/dcd567854191ad4e1abd293ddecd2a8df1048d8d/src/CLI.v#L1333-L1339 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 https://github.com/mit-plv/fiat-crypto/blob/dcd567854191ad4e1abd293ddecd2a8df1048d8d/src/StandaloneHaskellMain.v#L104-L114 and https://github.com/mit-plv/fiat-crypto/blob/dcd567854191ad4e1abd293ddecd2a8df1048d8d/src/StandaloneOCamlMain.v#L196-L203 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?).