Rust codegen support?

[tarcieri]

I apologize in advance if this question doesn't make sense as I'm still wrapping my brain around Vale/HACL*.

We would potentially like to use some of the cryptographic implementations from HACL* in the @RustCrypto project.

The ideal way for us to consume them would be using Rust inline assembly syntax, as this approach eliminates all platform-specific concerns around linking by passing assembly directly to LLVM.

I thought I'd at least inquire as to whether it would make sense for Vale to have first-class support for this in some form. We could potentially build our own tooling to do this, but if it makes sense as a first-class feature that seems like a much better solution to me.

[Chris-Hawblitzel]

Vale has multiple printers for various assembly syntaxes, particularly gcc and masm ( https://github.com/project-everest/vale/blob/master/fstar/specs/hardware/X64.Print_s.fst and https://github.com/hacl-star/hacl-star/blob/main/vale/specs/hardware/Vale.X64.Print_s.fst ). Also, there's a printer for inline assembly embedded inside gcc C code ( https://github.com/hacl-star/hacl-star/blob/main/vale/specs/hardware/Vale.X64.Print_Inline_s.fst ). All of these printers just provide ways to emit the same underlying verified assembly language code in multiple formats. Would it be sufficient to add a Rust inline assembly syntax printer alongside these printers?

[tarcieri]

Yes, that sounds great!