First version of coverage tools.

.gitignore

@@ -43,3 +43,6 @@ tests/rust_lean_equiv_test/lean/lake-manifest.json
 .idea/
 .vscode/
 .claude/
+
+# Python
+__pycache__/

COVERAGE.md

@@ -0,0 +1,77 @@
+# core / alloc model coverage
+
+Auto-generated by `tools/core-coverage/gen.sh` — **do not edit by hand**. CI fails if this file is out of date; regenerate with `make coverage`.
+
+Denominator: rustdoc JSON of the real `core`/`alloc` (`nightly-2026-02-07`). Numerator: rustdoc JSON of the model crates. See `tools/core-coverage/README.md` for what is counted and how modules are scoped.
+
+## `core`
+
+**Targeted coverage: 681/3888 items (18%) across 35 modules — 21 have at least a partial model.**
+
+| module | covered | total | coverage |
+|---|--:|--:|---|
+| `(root)` | 0 | 37 | 0% |
+| `any` | 0 | 9 | 0% |
+| `array` | 3 | 25 | 12% |
+| `ascii` | 0 | 29 | 0% |
+| `borrow` | 2 | 4 | 50% |
+| `cell` | 0 | 81 | 0% |
+| `char` | 0 | 67 | 0% |
+| `clone` | 2 | 7 | 29% |
+| `cmp` | 20 | 35 | 57% |
+| `convert` | 13 | 17 | 76% |
+| `default` | 2 | 2 | 100% |
+| `error` | 1 | 15 | 7% |
+| `f128` | 0 | 91 | 0% |
+| `f16` | 0 | 92 | 0% |
+| `f32` | 1 | 107 | 1% |
+| `f64` | 0 | 107 | 0% |
+| `fmt` | 7 | 111 | 6% |
+| `from` | 0 | 1 | 0% |
+| `hash` | 3 | 29 | 10% |
+| `hint` | 2 | 15 | 13% |
+| `index` | 0 | 2 | 0% |
+| `iter` | 27 | 170 | 16% |
+| `marker` | 6 | 35 | 17% |
+| `mem` | 19 | 80 | 24% |
+| `num` | 417 | 1835 | 23% |
+| `ops` | 84 | 151 | 56% |
+| `option` | 26 | 57 | 46% |
+| `panicking` | 2 | 31 | 6% |
+| `pin` | 0 | 27 | 0% |
+| `profiling` | 0 | 2 | 0% |
+| `ptr` | 0 | 191 | 0% |
+| `range` | 0 | 19 | 0% |
+| `result` | 30 | 42 | 71% |
+| `slice` | 8 | 205 | 4% |
+| `str` | 6 | 160 | 4% |
+| **subtotal** | **681** | **3888** | **18%** |
+
+<details><summary>Out-of-scope modules (20 modules, 0/14842 items — platform/runtime surface not targeted)</summary>
+
+`alloc`, `arch`, `async_iter`, `autodiff`, `bstr`, `contracts`, `ffi`, `future`, `intrinsics`, `io`, `net`, `os`, `panic`, `pat`, `random`, `simd`, `sync`, `task`, `time`, `unsafe_binder`
+</details>
+
+## `alloc`
+
+**Targeted coverage: 43/608 items (7%) across 11 modules — 7 have at least a partial model.**
+
+| module | covered | total | coverage |
+|---|--:|--:|---|
+| `(root)` | 0 | 2 | 0% |
+| `alloc` | 1 | 6 | 17% |
+| `borrow` | 3 | 9 | 33% |
+| `boxed` | 2 | 54 | 4% |
+| `collections` | 12 | 315 | 4% |
+| `fmt` | 1 | 1 | 100% |
+| `rc` | 0 | 71 | 0% |
+| `slice` | 0 | 6 | 0% |
+| `str` | 0 | 1 | 0% |
+| `string` | 5 | 63 | 8% |
+| `vec` | 19 | 80 | 24% |
+| **subtotal** | **43** | **608** | **7%** |
+
+<details><summary>Out-of-scope modules (4 modules, 0/106 items — platform/runtime surface not targeted)</summary>
+
+`bstr`, `ffi`, `sync`, `task`
+</details>

Makefile

@@ -42,9 +42,10 @@ ALLOC_CHARON_EXCLUDES = \
     --exclude '{impl core::ops::index::Index<_> for alloc_models::vec::Vec<_, _>}::*'
 
 .PHONY: all llbc extract patch lean build clean clean-generated tests \
-        tests-clean alloc-stage alloc-llbc alloc-extract alloc-clean
+        tests-clean alloc-stage alloc-llbc alloc-extract alloc-clean \
+        coverage
 
-all: lean
+all: lean coverage
 
 # 1. Run charon to produce LLBC from the Rust crate.
 #
@@ -162,3 +163,12 @@ tests: lean
 
 tests-clean:
 	$(MAKE) -C tests clean
+
+# -----------------------------------------------------------------------------
+# Coverage report: how much of real core/alloc the model crates provide.
+# (rustdoc-JSON based; independent of the charon/aeneas pipeline above.)
+# -----------------------------------------------------------------------------
+
+# Regenerate COVERAGE.md + tools/core-coverage/coverage.json.
+coverage:
+	./tools/core-coverage/gen.sh

README.md

@@ -40,6 +40,17 @@ CI verifies that the *committed* extracted Lean files in
 against the pinned toolchain. That means a downstream Lean consumer can
 just `lake update` this repo without installing the Rust toolchain.
 
+## Coverage
+
+[`COVERAGE.md`](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`](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
 
 ```
@@ -63,6 +74,10 @@ just `lake update` this repo without installing the Rust toolchain.
 ├── 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)
+│   └── aeneas-compat/     #   per-crate compatibility estimate vs the lib
+├── COVERAGE.md            # per-module core/alloc coverage report (generated)
 ├── Makefile               # extraction + build orchestration
 └── .github/workflows/ci.yml
 ```

tools/aeneas-compat/README.md

@@ -0,0 +1,163 @@
+# aeneas-compat
+
+Estimate a crate's compatibility with the `CoreModels` Aeneas library.
+
+There are two tools here, working at different altitudes:
+
+- **`aeneas_compat.py`** (described below) — a *pre-flight estimate* from the
+  crate's charon **LLBC**, before you run aeneas. Needs only `charon`. Fast, but
+  the covered set is derived from the model's LLBC rather than its Lean library,
+  so it has known false-positive categories (see bottom).
+- **`lean_extract_compat.py`** — a *post-extraction* check from the crate's
+  aeneas-emitted **Lean**. The most precise of the tools, but needs the crate to
+  have been extracted by aeneas already. See
+  [The Lean-extraction check](#the-lean-extraction-check).
+
+Given a target crate, it reports:
+
+- **used** — the `core::*` / `alloc::*` / `std::*` items the crate actually
+  reaches (after charon has desugared operators, resolved trait dispatch, etc.);
+- **covered** — those the model in this repo provides;
+- **MISSING** — those it does not, i.e. the gaps you'd hit.
+
+## Usage
+
+```sh
+# on a crate (runs charon for you):
+python3 tools/aeneas-compat/aeneas_compat.py path/to/crate
+
+# on an already-built LLBC (skips charon on the target):
+python3 tools/aeneas-compat/aeneas_compat.py --llbc path/to/target.llbc
+
+# machine-readable (for the planned axiom / exclude-flag generators):
+python3 tools/aeneas-compat/aeneas_compat.py --llbc target.llbc --json
+```
+
+It needs `charon` on `PATH` (override with `--charon` or `$CHARON`) and the
+model LLBCs `core_models.llbc` / `alloc.llbc` at the repo root (build them with
+`make llbc alloc-llbc` — they are git-ignored artifacts).
+
+Useful flags: `--show-covered`, `--no-manifest` (raw auto-derived result),
+`--manifest PATH`, `--rustflags` (defaults to `--cfg charon`, matching the main
+Makefile).
+
+## How it works
+
+Everything is read out of charon's **LLBC**, which is the right altitude for
+this question: the external (`core`/`alloc`/`std`) items in a crate's LLBC are
+*exactly* what aeneas will need the library to resolve. A source-level (`syn`)
+scan would miss operator desugaring (`a == b` → `PartialEq::eq`), trait-method
+resolution and deref coercions — charon has already done all of that.
+
+- **used set** — `charon pretty-print` the target LLBC and collect every
+  fully-qualified path under `core` / `alloc` / `std`.
+- **covered set** — same, over the model's own LLBCs. Anything `core`/`alloc`/
+  `std` that the model *defines* (its `core_models::*` / `alloc_models::*`
+  items, renamed back) **or** *references and still extracts against* is treated
+  as provided.
+- **MISSING** = used − covered − manifest.
+
+Items are matched on a **module-independent key**: generics and lifetimes are
+stripped, and trait impls are keyed on `{impl Trait for Type}::method` rather
+than the module they are authored in (the model often writes an impl in a
+different module than real core — e.g. `impl Default for u8` lives in
+`core_models::num`, not `core::default`).
+
+## The manifest
+
+`manifest.txt` patches the residue the pure-LLBC scan gets wrong. Two sections:
+
+- `[ignore]` — compiler-internal items that appear in every crate but are never
+  a real gap (drop glue, marker traits). Dropped from the *used* set.
+- `[covered]` — `core`/`alloc`/`std` items the library *does* provide but that
+  don't name-match the model LLBC.
+
+Paste keys **exactly** as they appear in the `MISSING` output (they are already
+in normalized form).
+
+## Known false-positive categories (triage into the manifest)
+
+This is a compatibility *estimate*. Because the covered set is derived from the
+model's LLBC rather than its final Lean library, a few categories show up as
+`MISSING` even though the Lean library handles them. When you confirm one is
+actually covered, add its key to `[covered]`:
+
+- **Glue routed through `rust_primitives` / hand-written Lean.** e.g.
+  `u32::leading_zeros` is modeled as a free function, not the `u32` inherent
+  method, so it won't name-match. (Contrast `u32::div_ceil`, which is a *real*
+  gap — genuinely not in the model.)
+- **Abstract default trait methods** (`Iterator::map`, `Iterator::collect`,
+  `Sum::sum`, …) the model never calls internally, so they never appear in its
+  LLBC even when the Lean library provides the default.
+- **Blanket vs concrete impls** — the model has `impl AsRef<T> for T` while the
+  target uses `impl AsRef<[T]> for [T]`; these don't string-match even though
+  the blanket impl applies.
+- **Items removed via `CHARON_EXCLUDES`** and re-supplied as hand-written Lean
+  (`*External.lean`).
+
+Inspecting `MISSING` and growing `manifest.txt` is the intended workflow; over
+time the false-positive list shrinks to the genuine gaps.
+
+## The Lean-extraction check
+
+`lean_extract_compat.py` answers the same question — *which `core`/`alloc` items
+does this crate need that the model doesn't provide?* — but from the **other
+end** of the pipeline: the Lean that aeneas has already emitted for the crate.
+
+```sh
+python3 tools/aeneas-compat/lean_extract_compat.py --lean-dir path/to/crate/lean
+python3 tools/aeneas-compat/lean_extract_compat.py --lean-dir <dir> --json
+python3 tools/aeneas-compat/lean_extract_compat.py --lean-dir <dir> --show-candidates
+```
+
+It needs a **built** `CoreModels` lake project (the repo's `lean/`, used to
+resolve names; override with `--core-models-lean`). It does *not* need charon or
+aeneas — only the crate's already-extracted `.lean` files.
+
+### Why it's more precise
+
+The extracted `Funs.lean` / `Types.lean` reference `core`/`alloc` as the exact
+mangled identifiers aeneas chose (e.g.
+`core.slice.iter.Iter.Insts.CoreIterTraitsIteratorIteratorSharedAT.map`).
+Reading them directly avoids *reconstructing* those names, so none of aeneas'
+mangling subtleties can produce a false positive.
+
+It is also better than just running `lake build` and reading the errors:
+
+- **deduplicated** — a missing name used at 10 sites is reported once, not ten
+  times;
+- **no cascade noise** — a build emits unrelated type errors once a definition
+  fails; this tool only ever reports unknown `core`/`alloc` names;
+- **strictly more complete** — once a definition fails on its first unknown
+  identifier, the build *masks* the remaining unknowns in that definition; this
+  tool sees them all (on `tests/list_coverage` it surfaces 5 genuine gaps the
+  build never prints).
+
+### How it works
+
+1. Scan the crate's `.lean` files for referenced `core.*` / `alloc.*` names and
+   for the names the crate *defines itself*.
+2. Drop any reference whose name — or any ancestor prefix — is self-defined.
+   This is the Lean-level analogue of charon's `is_local`: test crates that
+   mirror std paths (e.g. `tests/rust_lean_equiv_test`) emit their own functions
+   and lifted closures under literal `core.*` / `alloc.*` namespaces, which are
+   textually indistinguishable from real `core` references.
+3. Resolve the survivors against `CoreModels` with `check_lean_missing.lean`.
+   Resolution uses the **elaborator**, so a dot-notation projection on an
+   instance term (`<instance>.partial_cmp`) counts as covered even though it is
+   not itself a standalone constant — exactly as it would during a real build.
+
+Validated against `lake build` on the bundled test crates: **zero false
+negatives** (it never clears a name the build rejects), `0` missing on the two
+crates that build clean (`client_test`, `rust_lean_equiv_test`), and a
+deduplicated, build-masking-aware gap list on `list_coverage`.
+
+## Planned extensions
+
+The `--json` output is the foundation for:
+
+1. emitting a `.lean` file declaring the missing items as axioms with their
+   reconstructed types (needs type reconstruction from the target LLBC);
+2. emitting `charon --exclude` flags (and/or a list of the target's
+   modules/items) that carve out an analyzable subset touching only covered
+   features.