⚠️ Note: The contents of this repo are copied mechanically from the hax repo. Please file any issues or PRs there. ⚠️

Support library for hax/Lean-translated Rust code

hax is a tool for translating a large subset of Rust into Lean and other languages.

This library contains the Lean infrastructure of hax. Most notably:

• the Lean extraction of our model of Rust core/std/alloc libraries and supporting infrastructure
• tactics for verification of extracted code

Using this library

hax's Lean backend will set up the lakefile.toml to require this Lean package automatically. So you typically don't need to set up anything.

To use this package without hax, add the following to your lakefile.toml:

[[require]]
name = "hax"
git = "https://github.com/cryspen/hax-lean"
rev = "VERSION_OR_COMMIT_HASH"

Avoid opening the Aeneas.Std namespace in your Lean code (i.e., open Aeneas.Std) because that will bring Aeneas's own model of core into reach. Instead, use

open CoreModels
open Aeneas.Std hiding namespace core alloc

The two libraries in this package: CoreModels and Hax

This Lean package contains two libraries: CoreModels and Hax:

CoreModels

The CoreModels library contains the Lean extraction of our model of Rust's core/std/alloc libraries and supporting infrastructure. The Rust code of these core models can be found in https://github.com/cryspen/hax/tree/main/hax-lib/core-models. See https://github.com/cryspen/hax/tree/main/hax-lib/core-models/README.md for more information about the core models and about how the extraction works.

The heart of this Lean library is automatically generated by hax from that Rust code:

• CoreModels/Core/Funs.lean
• CoreModels/Core/Types.lean
• CoreModels/Alloc/Funs.lean
• CoreModels/Alloc/Types.lean

Not all items extract smoothly. The files TypesPrologue.lean, FunsPrologue.lean and FunsEpilogue.lean contain manual workarounds for some items.

The crates hax_lib and rust_primitives are not intended to be extracted by hax. The Lean analogues of their items are defined manually in HaxLib/Funs.lean and RustPrimitives/Funs.lean.

Hax

The Hax library contains infrastructure for hax-generated Lean code in general. Most importantly, it contains the following tactics:

• hax_mvcgen: This tactic extends Lean's verification condition generator mvcgen to able to handle Hoare-triples inside pre- and postconditions. By default, it attempts to process all hypotheses and the goal. To run it only on a hypothesis h, use hax_mvcgen at h. To use it only on the goal, use mvcgen directly.

• for_loop_with_invariant: This tactic helps to rewrite the code that hax generates from Rust for-loops into a form that is easier to verify with mvcgen. See https://github.com/cryspen/hax/blob/main/examples/loop_equivalence/proofs/loop-equivalence/lean/LoopEquivalence/Verification/ProofObligations.lean for an example.