formal(refinement): Tier-3 bridge — extracted Rust refines Authority.lean (Aeneas)#244
Open
hartsock wants to merge 1 commit into
Open
formal(refinement): Tier-3 bridge — extracted Rust refines Authority.lean (Aeneas)#244hartsock wants to merge 1 commit into
hartsock wants to merge 1 commit into
Conversation
…lean
Stands up the Charon/Aeneas refinement toolchain (roadmap Phase 0.6) and proves,
on the ACTUAL extracted Rust of agent-bridle-ceremony, the Authority.lean laws.
Pipeline (formal/refinement/): charon cargo --preset=aeneas → LLBC →
aeneas -backend lean → generated Types/Funs/FunsExternal → hand-written
Refinement.lean → lake build ✅.
12 refinement theorems, all by `cases <;> rfl` over the finite domain (the
extracted monadic functions reduce cleanly):
- axis + product `meet` commutativity and idempotence
- attenuation (L4/PO-4) as absorption `(a⊓c) ⊓ a = a⊓c`, i.e. `(a⊓c) ≤ a`
under the meet-order Authority.lean defines
- `attenuate = meet` (the extracted definition)
This is the concrete instance of the roadmap's central claim: the Rust waist
refines the Lean model. The frozen algebra is no longer just an abstract Lean
theorem set — the shipping implementation provably obeys it.
Design/plumbing:
- Separate, HEAVY tier: the generated code imports Aeneas + mathlib, so this
is NOT in the mandatory pre-push/CI gate (mathlib is too heavy per push).
Run via `just check-refinement` (skips gracefully without the toolchain).
- Portable: `aeneas-lean` is a gitignored symlink created by setup.sh
(honours AENEAS_LEAN_LIB) — no absolute path / username committed.
- regenerate.sh reproduces the extraction; aeneas-commit.txt pins provenance.
- Toolchain gotcha handled: this harness overrides CARGO_TARGET_DIR, which
breaks Charon's Makefile copy step; regenerate.sh unsets it.
KNOWN GAP: `resolve` uses a slice iterator (`iter().fold`), which Aeneas
axiomatizes (opaque `fold`/`split_first`), so it does not reduce and its laws
are not yet proven here. Fix = rewrite `resolve` as explicit recursion in the
kernel (ROADMAP 1c follow-up).
NOTE: the generated Lean was extracted from a crate including boundary.rs (the
enforcement-boundary module), which landed on the #241 branch AFTER #241 merged
(authority-only). Pairs with the boundary PR; merge that first for regenerate.sh
provenance parity.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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.
The Rust waist provably refines the Lean model
Stands up the Charon/Aeneas toolchain (roadmap Phase 0.6, now ✅ on gnuc) and proves, on the actual extracted Rust of
agent-bridle-ceremony, theAuthority.leanalgebraic laws.Pipeline (
formal/refinement/):charon cargo --preset=aeneas→ LLBC →aeneas -backend lean→ generatedTypes/Funs/FunsExternal→ hand-writtenRefinement.lean→lake build✅.12 refinement theorems, all
cases <;> rflover the finite domain (the extracted monadic functions reduce cleanly):meetcommutativity and idempotence(a⊓c) ⊓ a = a⊓c— i.e.(a⊓c) ≤ aunder the meet-orderAuthority.leandefinesattenuate = meet(the extracted definition)The shipping implementation is no longer just tested against the frozen algebra — it's proven to refine it.
Design / plumbing
just check-refinement(skips gracefully without the toolchain). The fastformal/gate now prunesrefinement/(Gate.lean).aeneas-leanis a gitignored symlink fromsetup.sh(honoursAENEAS_LEAN_LIB) — no absolute path / username committed.regenerate.shreproduces the extraction;aeneas-commit.txtpins provenance.Known gap (tracked, ROADMAP 1c)
resolveuses a slice iterator (iter().fold), which Aeneas axiomatizes (opaquefold/split_first), so it doesn't reduce and its laws aren't provable yet. Fix = rewriteresolveas explicit recursion in the kernel.Test plan
just check-refinement→lake buildinformal/refinement/, exit 0 (verified on gnuc).just check-formalstill green withrefinement/present (pruned from the scan).Pairs with the boundary re-land
The generated Lean was extracted from a crate including
boundary.rs, which landed on the #241 branch after #241 merged (authority-only). Merge the boundary PR first forregenerate.shprovenance parity.Risk
Low — additive
formal/refinement/+ aGate.leanprune + onejustfilerecipe + ROADMAP notes. No mandatory-gate behavior change for existing code; nothing deleted.