hax-lib 0.4.0

Hax-specific helpers for Rust programs
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73



⚠️ **Note: A CI workflow (deploy_hax_lean.yml) will copy this directory into the repo https://github.com/cryspen/hax-lean. Use that repo as a dependency in your lakefile because Lean's Reservoir supports only that repo.** ⚠️


# Support library for hax/Lean-translated Rust code

[hax](https://hax.cryspen.com/) 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`:

```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.