Preliminary support for a Rust backend

[msprotz]

Trying to merge this now as I switch my focus back to eurydice -- want to avoid bitrot. In addition to the Rust backend itself (which is profusely commented), a change in this PR is that the datatypes compilation phase now generates well-typed AST nodes from the get-go rather than rely on the Checker module to infer types. This was a historical artifact, and didn't sit well with the Rust backend, which is adamant about having fully-inferred AST nodes, so now it's fixed.

Unfortunately I don't have any tests yet as I'm weary of embarking on a CI journey. This shall be added in due time once HACL-rs is ready to be merged (branch protz_rs of HACL).

For context, I shall quote myself from Slack...

For a long while, many users (such as Election Guard, along with a sizeable chunk of the HACS community) have requested a pure Rust version of HACL* rather than Rust bindings on top of the C library.

I have just pushed a work in progress to that effect, on the protz_rs branches of HACL* and krml. This is extremely preliminary work, but already chacha20, poly1305 and chacha20poly1305 from HACL* compile, along with some of the bignum routines (UPDATE: all of the bignum routines, except for k256 -- thanks @R1kM for your crucial help).

Some additional thoughts, hoping to address questions that may arise.

• For now, the goal is to extract HACL* -- as such, this compilation facility is very much geared towards the kind of code currently found in HACL*.
• For now, this operates post-everything -- post-monomorphization, post-data type compilation, post-equality generation... which should make the task of generating Rust code even easier. It would be nice, in the long run, to gradually disable as many of these phases as possible, but the immediate goal is to extract HACL* to Rust. (Patches welcome!)
• The first main difficulty when compiling to Rust is compiling pointers, specifically, compiling pointer arithmetic in Low* to Rust code that passes the borrow-checker. The current strategy is as follows.
  • Every pointer is compiled as a mutable slice (immutable if using LowStar.ConstPointer)
  • Every bit of pointer arithmetic (the sub operation from Low*) is compiled as a call to slice_at_mut, relying on a static analysis that records the various splits operations enacted on the original (base) pointer, in order to make sure no reference to a borrowed variable is generated. I also added an optimistic compilation strategy for when there is too much loss of precision (see comments in lib/AstToMiniRust.ml), relying on Rust's bounds checks to guarantee either sound compilation, or a runtime exception if the choice made was incorrect. That latter strategy assumes that the programmer is taking offsets into the original pointer left-to-right, and kicks in whenever the offsets cannot be statically compared.
• The second main difficulty when compiling to Rust is compiling functions that permit aliasing between their arguments in Low*, and specifically, uses of these functions, such as fmul(x, x, y) where x is both written to (first parameter, out) and read (second parameter, in). UPDATE FROM SLACK MESSAGE
  • Rather than adding a rewrite in krml that would incur yet more meta-arguments to justify the correctness, I instead fixed the source code with @R1kM's help. This has the advantage of not relying on a dubious meta-theoretic soundness argument, and wasn't that much of a burden to deal with.

The current strategy is to statically replace every call to fmul that is of the form fmul x x y (there are many such functions -- fmul is just an example, for "field multiplication") with fmul_a x x y where _a stands for the aliased version. The fmul_a wrapper is inline_for_extraction, has exactly the same signature as fmul (so it doesn't wreck the proofs), and merely does let fmul_a dst x y = push_frame (); let x_copy = copy x in let r = fmul dst x_copy y in pop_frame (); r

Other options would be to write a separate version of fmul that is in-place, but based on @karthikbhargavan's preliminary benchmarking, this doesn't necessarily translate to perf improvements.

It remains to be determined what this means for HACL-C (right now these changes are not conditional on C vs Rust so this means the C code is impacted in HACL) but we can deal with it later in the HACL PR itself.

It goes without saying that there is a huge amount of room for improvement in all of the above. Stay tuned...

[msprotz]

(Got an everest green locally)