Rust: const fn support

[tarcieri]

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: rust-lang/rust#129195

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

[tarcieri]

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]

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

[JasonGross]

If I understand correctly, simply replacing fn with const fn at

fiat-crypto/src/Stringification/Rust.v

Line 395 in 58481a8

((if inline then "#[inline]" ++ String.NewLine else "") ++ (if private then "fn " else "pub fn ") ++ name ++

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]

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]

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

fiat-crypto/src/CLI.v

Line 387 in 58481a8

:= ([Arg.long_key "inline"], Arg.Unit, ["Declare all functions as inline."]).

(and perhaps then inline and static and const should be merged into a "function declaration options" type class a la

fiat-crypto/src/Stringification/Language.v

Line 156 in 58481a8

Class output_options_opt :=

)
If you want to do this and any of the control flow is unclear, let me know and I can clarify.

[tarcieri]

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]

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.

fiat-crypto/src/Stringification/Rust.v

Lines 390 to 397 in 58481a8

	Definition to_function_lines {language_naming_conventions : language_naming_conventions_opt} {skip_typedefs : skip_typedefs_opt} (internal_private : bool) (private : bool) (all_private : bool) (inline : bool) (prefix : string) (name : string)
	{t}
	(f : type.for_each_lhs_of_arrow var_data t * var_data (type.base (type.final_codomain t)) * IR.expr)
	: list string :=
	let '(args, rets, body) := f in
	((if inline then "#[inline]" ++ String.NewLine else "") ++ (if private then "fn " else "pub fn ") ++ name ++
	"(" ++ String.concat ", " (to_arg_list internal_private all_private prefix Out rets ++ to_arg_list_for_each_lhs_of_arrow internal_private all_private prefix args) ++
	") {")%string :: (List.map (fun s => " " ++ s)%string (to_strings internal_private prefix body)) ++ ["}"%string]%list.

is responsible for emitting the entire function (except for docstring, which is added at

fiat-crypto/src/Stringification/Rust.v

Lines 425 to 434 in 58481a8

	inl (((List.map (fun s => if (String.length s =? 0)%nat then "///" else ("/// " ++ s))%string (comment indata outdata))
	++ match input_bounds_to_string indata inbounds with
	| nil => nil
	| ls => ["/// Input Bounds:"] ++ List.map (fun v => "/// " ++ v)%string ls
	end
	++ match bound_to_string outdata outbounds with
	| nil => nil
	| ls => ["/// Output Bounds:"] ++ List.map (fun v => "/// " ++ v)%string ls
	end
	++ to_function_lines internal_private private all_private inline prefix name (indata, outdata, f))%list%string,

), so it could just emit the function twice.