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

Hax Lean Library

This Lean 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

Add to your lakefile.toml:

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

Core Models

The Lean extraction of our model of Rust core/std/alloc libraries and supporting infrastructure can be found in the CoreModels directory.

The heart of the package is automatically generated by Aeneas:

• 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 Aeneas. The Lean analogues of their items are defined manually in HaxLib/Funs.lean and RustPrimitives/Funs.lean.

Tactics

The main tactic provided by this package is hax_mvcgen. It extends Lean's verification condition generator mvcgen to able to handle Hoare-triples inside pre- and postconditions.