Aeneas Level 2: compile + verify translated Rust (advances #1)#12
Merged
Conversation
…neas output) Models rules_rocq_rust's rust_to_rocq: translate -> compile -> (proof next). - aeneas_translate now emits a discrete <name>.lean (copies the single module out of aeneas's -dest dir; fails loudly on multi-file/-split output). This removes the TreeArtifact blocker so a lean_library can consume it directly. - tests/charon_llbc: wire the lean toolchain (4.28.0-rc1, dev-mode — must match @aeneas_lean_lib's oleans) and add `hello_compiled` = lean_library over the translated Lean, deps @aeneas_lean_lib//:Aeneas. Kernel-checks that the Rust model elaborates. - ci.yml: build-aeneas-lean-lib also builds //:hello_compiled. Next: a hand-written proof + lean_proof_test (the verify step), once the compile bridge is CI-green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
CI caught it via the aeneas Level-2 compile: Lean 4.28.0-rc1 (what Aeneas pins)
pairs with Mathlib v4.28.0-rc1, but _required_lean_from_rev did
base.split('-')[0] -> '4.28.0', falsely flagging skew against the '4.28.0-rc1'
toolchain. Mathlib tags track the Lean version exactly including pre-release
suffixes, so strip only the leading 'v'. Stable-version tests didn't exercise
this; the RC path did.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Level-2 compile exposed it: `import Aeneas` couldn't find Aeneas.olean. Lake v4 nests oleans under .lake/build/lib/lean/, and the consolidation copied the outer .../lib/. — landing them at lib/lean/Aeneas.olean instead of lib/Aeneas.olean, which the path_marker dir (lib/) can't resolve. Mirror the mathlib consolidation: prefer the .../lib/lean level and break on first match, so modules land flat in lib/. Latent bug — nothing compiled against @aeneas_lean_lib until now. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ath) Level-2 compile got past 'import Aeneas' to 'unknown module prefix Mathlib'. The #7 shallow-fetch made aeneas's mathlib a LOCAL-PATH dep, so its oleans live under mathlib4_src/.lake/build, not .lake/packages — the consolidation missed them, so Aeneas's transitive Mathlib imports couldn't resolve. Copy from mathlib4_src too, mirroring @mathlib's own consolidation. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…test The verification payoff. HelloProofs.lean states + kernel-checks properties of the Aeneas-translated functions (zero sorry/axiom), using Aeneas's ⦃ ⦄ progress-spec DSL: - add.spec: no-overflow add returns the exact sum. - identity.spec: identity returns its input. Wires a lean_proof_test over :hello_compiled + @aeneas_lean_lib and runs it in CI. Completes the Rust -> LLBC -> Lean -> compile -> PROVE chain (closes #1's Level-2 gap), modelled on rules_rocq_rust's point_proofs.v. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
CI: add.spec checked green; identity.spec hit 'No goals to be solved' at step, since already discharges ok x ⦃ y => y = x ⦄ (x = x). Remove the trailing step. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
avrabe
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Completes the Rust verification pipeline, modelled on
rules_rocq_rust/examples/rust_to_rocq. All CI green, including the heavyAeneas Lean lib buildjob which now runs the full chain.The full chain — now CI-proven
Rust → Charon (LLBC) → Aeneas (Lean) → compile → PROVE
charon_llbc(Rust→LLBC) andaeneas_translate(LLBC→Lean, now a discrete.leanmodule).hello_compiled:lean_librarycompiling the translated model against@aeneas_lean_lib.hello_verified:lean_proof_testkernel-checking properties of the translated functions (zerosorry/axiom):add.spec— no-overflow add returns the exact sum;identity.spec— identity returns its input.Fixes this surfaced (each only exposable by an actual compile/proof)
_required_lean_from_revstripped-rcN, falsely flagging RC Lean (4.28.0-rc1) vs RC Mathlib skew.aeneas_translatenow emits a discrete.lean(removes the TreeArtifact blocker)..lake/build/lib/lean(flat layout) and copy Mathlib frommathlib4_src(the aeneas_lean_lib has the same unpinned full-clone / silent-HEAD bug fixed for mathlib in #6 #7 local-path redirect moved it out of.lake/packages).bin/.light/rust-cpu); GitHub-hostedubuntu-latestno longer allocated.Shared infra
lean/private/mathlib_fetch.bzl— the #7 shallow-fetch helper used by bothmathlib_repoandaeneas_lean_lib.Advances #1 (FEAT-006). Dev-mode pin (no sha256 yet) — pin hashes follow-up. The
aeneas_verified_libraryconvenience macro (translate+compile+prove in one) is a remaining nicety; the example demonstrates the full pipeline.🤖 Generated with Claude Code