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.

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)
├── 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

Add to your downstream lakefile.toml:

[[require]]
name = "CoreModels"
git = "https://github.com/cryspen/rust-core-models"
rev = "COMMIT_HASH_HERE"
subDir = "lean"

Use aeneas with the -core-models-lib option (currently only available with the following aeneas branch: https://github.com/cryspen/aeneas/tree/core-models-option)

Then the Aeneas-extracted code that uses std::* types will resolve through this library's core.* / alloc.* shims.

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]