hacspec
[rengine]: Missing support for fresh modules
Some phases of Hax (namely, bundling for F*) may introduce "fresh modules", modules that were not present in the rust code. Items that are moved from their original module to some fresh module have a their moved field set to a fresh module. Currently, the Rust engine cannot render FreshModule identifiers into a View, so rust-based backend (aka, Lean) cannot print them.
They should not appear in the Lean pipeline, as the bundling phase is specific to F*.
Probably low priority, as it is not needed for the Lean backend (in the current plan). Will be need when porting the Fstar backend to rust.
Fresh modules are used by the phase that inserts bundles; those are useful in backends in which two mutually dependent items must live in the same namespace. This is not the case of Lean, but it is the case of Coq and F*.
So it's not a F* thing, it's a not-Lean thing. The port of any backend but Lean and Rust to the Rust engine will require the support of fresh modules.
