search

mit-plv / fiat-crypto

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

Rust: `const fn` support #1955

Open tarcieri opened 2 months ago

tarcieri commented 2 months ago

This is a (perhaps a bit early) request to at least optionally generate Rust source code use const fn instead of fn.

Though current stable Rust doesn't support the use of mutable references in const fn, that's about to change with this stabilization PR: https://github.com/rust-lang/rust/pull/129195

Once that PR lands, the existing emitted Rust code should be valid under const fn.

tarcieri commented 1 month ago

The PR has been merged, and the fiat-crypto emitted code should be valid under const fn in Rust 1.83 to be released November 28th, 2024.

I guess for now I can just do find/replace on the generated code, but first-class support would be great.

tarcieri commented 3 weeks ago

Rust 1.83.0-beta.1 has been released with stabilized support for const_mut_refs

JasonGross commented 3 weeks ago

If I understand correctly, simply replacing fn with const fn at https://github.com/mit-plv/fiat-crypto/blob/58481a8feca6c38b1d3f9e23c5eaab27319929f4/src/Stringification/Rust.v#L395 will do the trick. I'm a bit short on time, but if you prepare a PR, updating both this line and the generated files (either by find/replace, or by downloading the artifacts that the CI generates), I'd be happy to merge it.

Do we need to update any Rust version constraints anywhere?

tarcieri commented 3 weeks ago

Great, thanks!

If you do accept this change, the generated code will only work under Rust 1.83, which is quite a jump.

If there's some way to make it optional, it might make sense for the immediate future, so older Rust versions can still be supported.

I can also do find/replace to make use of it in const contexts for the time being.

JasonGross commented 3 weeks ago

Is there any way to make the generated code condition on Rust version, a la C/C++ preprocessor macros?

If not, the crates package will still need to pick a single version to be compatible with, and I imagine most of the users of the Rust codegen use it via the crate. Users of older Rusts can still (I presume?) get the older versions of the crates package, and users who want the older codegen can still download previous releases. Fiat Crypto development itself is not moving particularly quickly, so I imagine the use case of "old Rust version, new Fiat Crypto features" will be quite niche.

Still, if you (or anyone else) is interested in putting in the work to make it optional, I'd accept a PR adding threading through a --const argument a la --inline at https://github.com/mit-plv/fiat-crypto/blob/58481a8feca6c38b1d3f9e23c5eaab27319929f4/src/CLI.v#L387 (and perhaps then inline and static and const should be merged into a "function declaration options" type class a la https://github.com/mit-plv/fiat-crypto/blob/58481a8feca6c38b1d3f9e23c5eaab27319929f4/src/Stringification/Language.v#L156 ) If you want to do this and any of the control flow is unclear, let me know and I can clarify.

tarcieri commented 3 weeks ago

Is there any way to make the generated code condition on Rust version, a la C/C++ preprocessor macros?

Not really for this particular case. Every function definition would have to be duplicated to make that work, and at that point, a toggle seems in order.

Still, if you (or anyone else) is interested in putting in the work to make it optional, I'd accept a PR adding threading through a --const argument a la --inline

Sounds good!

JasonGross commented 3 weeks ago

Not really for this particular case. Every function definition would have to be duplicated to make that work, and at that point, a toggle seems in order.

Note that since the code is autogenerated, this should actually be pretty easy to implement. https://github.com/mit-plv/fiat-crypto/blob/58481a8feca6c38b1d3f9e23c5eaab27319929f4/src/Stringification/Rust.v#L390-L397 is responsible for emitting the entire function (except for docstring, which is added at https://github.com/mit-plv/fiat-crypto/blob/58481a8feca6c38b1d3f9e23c5eaab27319929f4/src/Stringification/Rust.v#L425-L434 ), so it could just emit the function twice.