rust-core-models

A model of Rust's core and alloc libraries, packaged as:

1. Rust crates (core-models, alloc, rust_primitives) that mirror the core::* and alloc::* items downstream verified-Rust code uses.
2. A Lean library (CoreModels) extracted from those crates by Aeneas, suitable for downstream Aeneas-extracted Lean projects to depend on as a drop-in core model.
3. A test suite (tests/) split into two surfaces:
   • tests/client_test/ — a regression "client" crate that exercises items from core::* / std::* end-to-end. Its only assertion is that the Aeneas extraction of the crate elaborates against our CoreModels shims; it does not check behavioural agreement.
   • tests/rust_lean_equiv_test/ — a rust↔lean equivalence framework. Each test pins one concrete behavioural observation (e.g. Some(7u8).is_some() == true), checked once on the Rust side via cargo test and once on the Lean side via a #guard against the Aeneas extraction. Divergence between Rust std and our model surfaces here.

Why this exists

Verified-Rust pipelines need a model of core and alloc to elaborate against. Writing that model in Rust (rather than directly in each verification tool's logic) has three advantages:

• Easy to extend: adding a new core::* item is just a Rust source edit, no proof-assistant boilerplate.
• Cross-testable against the real Rust core library: the model is ordinary Rust, so we can compile and run it side-by-side with std and check behavioral agreement.
• Shareable across verification tools: a single Rust model feeds multiple downstream backends — currently hax-F*, hax-Lean, and Aeneas-Lean — instead of each tool maintaining its own shadow core.

CI verifies that the committed extracted Lean files in lean/CoreModels/{Funs,Types,…}.lean match what a fresh extraction produces against the pinned toolchain. That means a downstream Lean consumer can just lake update this repo without installing the Rust toolchain.

Coverage

COVERAGE.md reports, per top-level module, how much of the real core / alloc public API the model crates provide. It is generated by tools/core-coverage (comparing rustdoc JSON of the real std crates against the model crates). Run make coverage to regenerate it (it also runs as part of the default make target). The numbers are an approximate, periodically-refreshed snapshot — not a CI-enforced invariant, because the model's rustdoc (via hax-lib proc macros) isn't bit-reproducible across machines.

Repository layout

.
├── core-models/           # main Rust crate: model of `core::*`
├── alloc/                 # model of `alloc::*` (separate crate so it
│                          #   can be extracted with charon's
│                          #   `alloc_models` rename trick — see Makefile)
├── rust_primitives/       # tiny crate of helpers (slice/array primitives)
├── lean/                  # the distributed Lean library
│   ├── lakefile.toml
│   ├── lean-toolchain
│   └── CoreModels/        # hand-written + extracted, both committed
├── tests/                 # test suite (workspace; see Testing section)
│   ├── client_test/       #   client-surface extraction smoke test
│   └── rust_lean_equiv_test/  # rust↔lean equivalence framework
│       ├── source/        #     crate carrying `#[rust_lean_test]` fns
│       ├── macro/         #     proc-macro defining the attribute
│       ├── gen_lean_tests.py  # scans source/, emits #guards
│       └── lean/          #     lake project consuming the extraction
├── patch_lean.py          # post-processes Aeneas's output of the
│                          #   parent library to match our package layout
│                          #   (see comment block at top of the file)
├── tools/                 # auxiliary tooling
│   └── core-coverage/     #   generates COVERAGE.md (rustdoc-JSON based)
├── COVERAGE.md            # per-module core/alloc coverage report (generated)
├── Makefile               # extraction + build orchestration
└── .github/workflows/ci.yml

Building

Prerequisites

• Rust toolchain pinned by rust-toolchain.toml.
• charon and aeneas on PATH (the upstream nix flakes are the recommended build path; CI uses nix build github:AeneasVerif/{charon,aeneas}). Override the Makefile lookup with make CHARON=/path/to/charon AENEAS=/path/to/aeneas.
• elan for Lean.

Targets

make lean           # extract Rust → Lean, patch, build the Aeneas library
make tests          # full test suite (both client_test/ and rust_lean_equiv_test/)

make clean          # remove all generated Lean + LLBC, keep hand-written

make lean is idempotent: re-running without source changes is a no-op modulo Lake's incremental build.

To run just one test surface in isolation:

make -C tests/client_test            # smoke-test extraction
make -C tests/rust_lean_equiv_test   # rust↔lean equivalence

Testing

Two test surfaces

tests/client_test/ is a "what a downstream user touches" probe. Its src/lib.rs calls a representative slice of core::* / std::* items; the test passes iff Aeneas can extract the resulting LLBC and the result elaborates against our CoreModels shims. Failures here mean the extraction pipeline is broken for some surface — they say nothing about whether Rust and Lean agree behaviourally.

tests/rust_lean_equiv_test/ is the rust↔lean equivalence framework. Each test pins one concrete observation and checks it twice:

• Rust side — cargo test runs every #[rust_lean_test] pub fn test_xxx() -> bool { ... }, generated by the rust_lean_test_macro crate, and asserts the body returns true.
• Lean side — gen_lean_tests.py scans source/src/**/*.rs for the same attribute, finds each function's Aeneas-emitted name in Funs.lean, and emits one #guard <fully-qualified-name> == .ok true into lean/RustLeanTests/LeanTests.lean. Lake fails the build for any guard whose Aeneas-evaluated body is not Result.ok true.

Both halves must pass. Together they say: "for this concrete input, Rust std and the Lean translation of core_models give the same answer." Disagreements show up as a failed #guard (Lean side knows the truth) or a failed cargo test assertion (Rust side knows the truth) — same code, different oracle.

Adding a new item to the model

When you add an item to core-models/src/core/foo.rs (or alloc/src/...):

1. Add one property-based test (proptest!) in the same file's #[cfg(test)] mod tests { ... } block. This is the broad randomized check that the model matches Rust std across the input domain.
2. Add several point tests in tests/rust_lean_equiv_test/source/src/{core,alloc}/foo.rs (mirroring the source file's path under core-models/). Each point test pins one concrete behaviour with a #[rust_lean_test] attribute. Cover boundaries: zero, MIN, MAX, empty, single element, signed/unsigned edges, the None/Err case, etc.

The point tests in (2) are what catch extraction bugs — the property-based test in (1) only knows about Rust, while the equivalence test exercises Aeneas's translation of the same item.

Pitfalls

• Typed None: Aeneas drops the T parameter of None::<T> in zero-arg functions, leaving Option.None polymorphic in the extracted Lean. Use the helpers in tests/rust_lean_equiv_test/source/src/helpers.rs (none_u8, none_i32, …) rather than inline None. Add a none_<T> if your type isn't covered.
• Closures: tests that rely on |x| ... (e.g. map, and_then, unwrap_or_else) currently extract poorly. Comment them out with // TODO(closure-extraction): ....
• Excluded items: things listed in CHARON_EXCLUDES / ALLOC_CHARON_EXCLUDES (core::mem::swap, core::slice::index::*, most Vec indexing, BinaryHeap, …) come from hand-written Lean definitions in lean/CoreModels/{Funs,Types}External.lean. Their equivalence tests live in the same file as the rest of the items in the same module (e.g. core::mem::swap tests live in source/src/core/mem.rs) — flagged with a section header noting they exercise a manual Lean def.

Using the Lean library downstream

See lean/README.md

Contributing

PRs welcome. Please:

• Run cargo fmt --all and make lean tests before opening a PR (CI enforces both).
• For every new core::* / alloc::* item:
  • Add one property-based test in the model crate's #[cfg(test)] block (see existing proptest! blocks in core-models/src/core/option.rs etc. for the pattern).
  • Add several #[rust_lean_test] point tests in tests/rust_lean_equiv_test/source/src/... covering corner cases of the input. See the Testing section for the motivation and the pitfalls.
• If your item is excluded from extraction (added to CHARON_EXCLUDES), the equivalence tests still go in the file that mirrors the item's core::* / alloc::* location — flag them with a section header like // ----- foo (manually defined in Lean, not extracted) ----- so a reader knows the Lean side is hitting a hand-written definition in lean/CoreModels/FunsExternal.lean rather than the extraction.

License

[fill in]