This PR, done jointly with @msprotz, improves the Rust backend by avoiding needless mutable borrows each time a value is borrowed.
A detailed explanation of the compilation scheme is provided at the top of lib/OptimizeMiniRust.ml. However, the core idea is the following:
First, the translation from Ast to MiniRust does not introduce any mutability, only shared borrows
In a second phase operating on the MiniRust AST, borrows and variables are marked as mutable through a backward analysis pass, only when required (e.g., when assigned to, or passed to a function expecting a mutable borrow). Importantly, this second phase is not trusted: it only modifies the mutability information in the program, which will therefore be rechecked by the Rust compiler.
In addition to the unit tests added in Rust7.fst, the currently supported part of HACL-rs also extracts, compiles, and passes tests with this PR.
This PR, done jointly with @msprotz, improves the Rust backend by avoiding needless mutable borrows each time a value is borrowed.
A detailed explanation of the compilation scheme is provided at the top of lib/OptimizeMiniRust.ml. However, the core idea is the following:
In addition to the unit tests added in Rust7.fst, the currently supported part of HACL-rs also extracts, compiles, and passes tests with this PR.