Alethe walker foundation: FFI parse method + Lean step ADT - #41
Merged
Conversation
First slice of the Lean-side Alethe walker work (PR-α-foundation).
The walker proper — per-rule elaborators, closeOrFail wiring,
worked LIA example — lands in PR-β following this one. This PR
ships only the foundation that future walker work depends on: a
way to get cvc5's parsed alethe-2024 trace across the FFI as a
structured Lean ADT.
**SDK FFI** (`sdk/ffi/proof_broker_ffi.ml`): new
`parse_alethe_proof` method takes `{"proof": "<alethe-text>"}`
and returns `{"assumes": [...], "steps": [...], "anchors":
[...]}`. Reuses the existing `Alethe.parse` + `Alethe.step_to_json`
+ `Alethe.Sexp.to_json` machinery — the parser is already
exercised by the OCaml provenance verifier in `Tier3_alethe.verify`,
so the new method is pure structural surfacing of an already-
parsed proof. Failure modes: decode_error / json_parse_error /
new alethe_parse_error.
**Lean module** (`lean-bridge/ProofBroker/Alethe.lean`, new):
mirrors the OCaml shape with:
- `Sexp`: atom | list (with `Sexp.fromJson?` partial decoder).
- `Step`: { id, rule, clause, args?, premises?, discharge? }.
- `Assume`: { id, literal } (the top-level proof assumptions).
- `Proof`: { assumes, steps, anchors }.
- `runParseAletheProof : String → Except FfiError Proof` — the
Lean-side Bridge call, layered on top of pbCall +
decodeEnvelope.
The audit narrative for the eventual walker: the OCaml-side
`Tier3_alethe.verify` covers provenance (steps reference valid
premises, the proof walks to the empty clause). The Lean walker
covers soundness (per-step kernel elaboration). Together they
deliver "cert IS the proof" for cvc5's Tier-3 alethe-2024 path,
parallel to the Tier-1 Farkas term-mode closer's play for
Tier-1 certs.
Locally verified: SDK build clean, Lean `ProofBroker` library
build clean (`lake build ProofBroker` — 23 jobs).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
levineuwirth
added a commit
that referenced
this pull request
May 21, 2026
…/false) Second slice of the Lean-side Alethe walker. The foundation (PR #41) shipped the FFI + step ADTs; this PR adds the walker proper for the clausal-reasoning layer. The architectural play: turn a cvc5 Tier-3 alethe-2024 cert from a cert-gated omega trigger into the proof itself — per-step kernel elaboration, parallel to how the Tier-1 Farkas term-mode closer consumes Tier-1 certs. **Walker** (`ProofBroker/Alethe.lean`): - `WalkerContext` (Alethe atom → Lean local hypothesis Expr, harvested from the goal's `LocalContext` by `mkContext`) + `WalkerM` (`StateRefT` over a step-id → proof-term map). - `sexpToExpr` / `listToExpr` / `andOrChain` (mutual): translate an Alethe `Sexp` to a Lean `Expr` over the LIA fragment — integer literals (incl. cvc5's `n/1` rational-of-integer form), variable/hypothesis refs, `+`/`-`/`*`, `<=`/`<`/`>=`/ `>`/`=`, `not`/`and`/`or`/`=>`, and the clausal `cl` constructor (`(cl)` → `False`, `(cl L)` → `L`, `(cl L1 …)` → `L1 ∨ …`). - Rule elaborators for the clausal layer: `resolution` (binary ¬-elimination shape — the empty-clause closing step), `or` (clause restatement), `false` (`¬False` premise). - `walkProof`: two-phase — seed each top-level `assume` by `isDefEq`-matching its literal against a local hypothesis, then fold `elabStep` over the step list, returning the last step's proof term. **closeOrFail wiring** (`ProofBroker/Tactic.lean`): the LIA arm now tries `tryAletheWalkerLIA` first for alethe-2024 certs over a `False` goal — walker success closes via the reconstructed term; any walker failure (unsupported rule, non-`False` goal, parse failure) returns `false` and falls through to the existing `omega`. Behavior on every current test is unchanged: real cvc5 LIA traces use ~14 rules of which M1.β covers 4, so the walker throws and omega runs — but the architecture is in place to extend rule-cluster by rule-cluster. **Test-only tactic** `alethe_walker_test "<trace>"` drives the walker on a hand-written alethe-2024 trace (no live cvc5 needed) — same CI-stable pattern as `llm_replay_test`. **Tests**: `alethe_walker_clausal_axiom_free` and its premise-order-flipped twin reconstruct `False` from `A`/`¬A` via `assume` + `resolution`. Both close **axiom-free** — the walker emits `hNA hA` directly, no decision procedure, no axiom. Pinned `[]` in `tools/axiom_allowlist.json`. Scope honesty: even a tiny cvc5 Farkas proof (`x ≥ 3, x ≤ 1 ⊢ False`) uses ~14 rules. M1.β is the clausal foundation; follow-up PRs add `la_generic`+`la_mult_neg` (arithmetic), `refl`/`symm`/`trans`/`cong` (equality), and the boolean- cleanup cluster (`hole`/`rare_rewrite`/`equiv_*`/`implies`/ `and_neg`) cvc5 sprinkles everywhere. Until then real cvc5 traces fall through to omega — no regression, no progression. Verified: full lean-bridge build (16695 jobs) with pinned Vampire, trust-footprint gate, roundtripTest, SDK suite, Python gates — all green. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 25, 2026
levineuwirth
added a commit
that referenced
this pull request
May 27, 2026
Begins the Rocq-side Alethe walker port (mirror of the Lean arc PRs #41-#52). Goal: end-to-end "cert IS the proof" reconstruction for cvc5 alethe-2024 traces on Rocq, with UF + LIA mixed-theory closure as the primary capability gain. Currently Rocq's LIA arm is bare `lia` and its UF arm is a congruence chain; neither composes for mixed-theory goals cvc5 handles natively. The walker shifts Rocq from "can solve LIA, can solve UF, struggles on mixed" to "can replay anything cvc5 closed". R-1 establishes the module file and a Result-typed wrapper over the SDK's already-shared `Proof_broker.Alethe.parse`. Walker elaborators arrive starting R-2 (clausal layer). The SDK's ADT (Sexp.t, step, proof) and parser are shared by both bridges, so the Rocq side reuses them directly — no mirror-in-OCaml work like Lean PR #41 needed (Lean had to build its own Sexp ADT and FFI envelope; Rocq just uses the OCaml SDK directly). Audit H1 contract (same as Lean): walker failure surfaces as a tactic failure, with the existing lia fallback re-running. Wired into close_or_fail in R-9; no closer integration yet. Subsequent PRs follow the Lean cluster decomposition: R-2 clausal, R-3 arithmetic, R-4 multi-literal resolution, R-5 equality, R-6 trust-tagged leaves, R-7 boolean cleanup, R-8 equiv_simplify, R-9 wire into closer, R-10 equiv_pos1/equiv_pos2, R-11 cong over operators (visible payoff PR), R-12 snapshot test against the real cvc5 trace pinned in Lean #52. Validation: local Rocq env is broken (missing zarith, rocq-runtime per project memory); rely on CI for the full build. The OCaml file itself is 15 lines of `Result`-typed exception wrapping — confident in syntax. Co-Authored-By: Claude Opus 4.7 <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.
What
First slice of the Lean-side Alethe walker work — the foundation the walker proper depends on. No walker logic in this PR.
The Alethe walker is the architectural play that turns cvc5's Tier-3 `alethe-2024` cert from a cert-gated `omega`-trigger into the proof itself (parallel to how the Tier-1 Farkas term-mode closer already consumes Tier-1 certs as proofs rather than as triggers for `lia`). This PR ships only the bridge between the SDK's existing parser and the Lean side; per-rule elaboration lands in M1.b+.
Pieces
SDK FFI (`sdk/ffi/proof_broker_ffi.ml`)
Lean module (`lean-bridge/ProofBroker/Alethe.lean`, new)
Verification
SDK build clean (`dune build sdk`), Lean `ProofBroker` library build clean (`lake build ProofBroker`). No new tests in this PR — the build success is the test for the foundation; subsequent walker PRs will exercise the FFI heavily at lake-build elaboration time.
Next
🤖 Generated with Claude Code