Finish Aeneas end-to-end pipeline: add hermetic Charon, reuse rules_verus sysroot pattern

[avrabe]

Context

The Aeneas half of the pipeline is already wired:

• aeneas_release downloads prebuilt Aeneas for macOS (aarch64/x86_64) and Linux x86_64 — aeneas/private/repo.bzl
• aeneas_lean_lib builds the Aeneas Lean support library from source
• aeneas_translate runs aeneas -backend lean -dest OUT SRC.llbc — aeneas/private/aeneas.bzl

Across the workspace there are already ~3,259 lines of hand-written Lean proofs (gale, relay, spar, sigil) that are specs waiting to be connected to Rust implementations. Aeneas is the missing refinement link.

What blocked the work

The pipeline starts at .llbc, but nothing produces LLBC from Rust. aeneas_translate.srcs accepts only .llbc. Charon is the tool that produces LLBC, and it's hard to Bazel-ify because:

1. Charon is a rustc driver — it dynamically links against librustc_driver and needs a matching Rust sysroot at runtime.
2. Charon pins a specific dated nightly Rust toolchain (via rust-toolchain.toml).
3. Charon ships source, not prebuilt binaries — official distribution is nix run github:AeneasVerif/charon.
4. Aeneas, Charon, and Lean form a three-way version coupling that has to stay consistent (Aeneas commit → Charon pin → Lean version).

Additionally, aeneas_lean_lib's current implementation calls lake update + lake exe cache get + lake build Aeneas inside a repository rule — that's network-at-load-time and not hash-pinned, which fails reproducibility goals.

What changed: we've already solved the hard parts — twice

Two sister repos in the same toolchain already solve the pieces this needs:

rules_verus — Verus is architecturally identical to Charon (a rustc driver that replaces codegen with analysis, dynamically linked against librustc_driver). rules_verus/verus/private/repo.bzl already implements the tricky part:

• Read the bundled version.json to extract the required Rust toolchain
• Download rustc-{v}-{triple}.tar.xz and rust-std-{v}-{triple}.tar.xz from static.rust-lang.org
• Merge them into rust_sysroot/ using the tar --strip-components=2 trick (documented there because download_and_extract + cp -R silently drops .rlib files on some platforms)
• Verify libcore-*.rlib exists for the target, fail loudly if not
• Expose the sysroot as a Bazel filegroup

This transfers directly. The only delta is:

```diff

• "https://static.rust-lang.org/dist/rustc-{v}-{t}.tar.xz" # stable

• "https://static.rust-lang.org/dist/{date}/rustc-nightly-{t}.tar.xz" # dated nightly
  ```

rules_rocq_rust — provides a working Nix-hermetic OCaml-based toolchain (Rocq 9.0.1 + coqutil + CoqHammer + smpl). Charon is also OCaml-based (plus Rust). Reusing the same Nix pattern for Charon keeps the workspace architecturally consistent: prebuilt-binary tools via the rules_verus pattern, OCaml/complex-build tools via the rules_rocq_rust Nix pattern.

Proposed plan

Stage 1 — Hermetic Charon toolchain (~1 day)

• Add charon_release repo rule modeled on verus_release (rules_verus/verus/private/repo.bzl:105). Build Charon via a Nix derivation pinned by the commit in Aeneas's charon-pin.
• Reuse the rustc + rust-std download/merge/verify block from rules_verus/verus/private/repo.bzl:155-215 verbatim, swapping the stable URL for a dated-nightly URL.
• Expose :charon_bin, :rust_sysroot_files, :all_files using the same filegroup shape as verus_release.

Stage 2 — charon_llbc build rule (~1 day)

• New rule charon_llbc(name, srcs, cargo_toml) that invokes charon cargo --preset=aeneas with environment variables pointing at the hermetic sysroot. Model the env-var plumbing on rules_verus/verus/private/verus.bzl.
• Output: <crate>.llbc, feeds straight into the existing aeneas_translate.

Stage 3 — Clean up aeneas_lean_lib (~0.5 day)

• Move lake build out of the repository rule. Either build the Aeneas Lean library as part of the Nix derivation from Stage 1 and drop prebuilt .olean files in, or move the lake steps into a regular genrule with declared inputs and outputs.
• Pin Aeneas by commit SHA, not by build-<timestamp> tag — the timestamp string rolls on every nightly build; the SHA is what actually matters for reproducibility.

Stage 4 — First end-to-end example (~1 day)

Pick the cleanest candidate first: sigil Ed25519 (pure crypto, no unsafe, no embedded types, matches the SymCrypt reference pattern that the Aeneas+Lean flagship user follows). sigil/lean/Ed25519.lean already exists as a target spec.

• Wire charon_llbc → aeneas_translate → lean_library → lean_proof_test end-to-end.
• Verify the generated Lean compiles and imports correctly against the existing Ed25519.lean spec.
• Document the pipeline in rules_lean/docs/getting-started.md.

Stage 5 — Second candidate: gale ring_buf

Refinement against the existing 9-invariant RingBuf.lean spec (z/gale/proofs/lean/RingBuf.lean). This is where the work actually pays out — proving the Rust implementation refines the mathematical spec.

Non-goals

• Translating embedded code that uses unsafe, raw pointers, or trait objects. Charon will mark those declarations as missing. Gale MPU, SysTick, and intrusive-list code are out of scope.
• Replacing Verus. The two provers answer different questions; Aeneas adds the Lean refinement track that the other provers can't express.

Known constraints

From AeneasVerif/charon#142 the following Rust features are currently not supported:

dyn Trait, HRTB quantified where-clauses, string literals, enum as isize casts, type alias LLBC export, associated type equalities, mutually recursive traits, defaulted trait methods, Drop semantics, vec![] macro, unsafe code, GATs, RPITIT, thread-locals, contract annotations.

Aeneas additionally rejects: return inside nested loops, break/continue to outer loops, interior mutability, concurrency.

These restrictions dictate which crates are viable translation candidates.

References

• rules_verus/verus/private/repo.bzl — sysroot handling to reuse
• rules_rocq_rust — Nix-hermetic toolchain pattern to reuse
• aeneas/private/repo.bzl — current Aeneas wiring
• aeneas/private/aeneas.bzl — current aeneas_translate rule
• AeneasVerif/aeneas
• AeneasVerif/charon
• Charon paper (arXiv 2410.18042v3)