ArghDA M6 follow-on: Lean #print axioms audit — honest Unknown→Proven#42
Merged
Merged
Conversation
A clean Lean elaboration is only `Unknown` on its own (sorry is a mere
warning; native_decide's axiom is invisible to a bare run). `check_file`
now runs a `#print axioms` audit on a clean elaboration and promotes the
verdict honestly.
Mechanism (std-only, no new dependency):
- `decl_names` parses the auditable declarations (theorem/lemma/def/abbrev/
instance), skipping leading `@[..]` attributes + modifiers and anonymous
decls. Conservative: a missed name just isn't audited; a mis-parsed name
makes `lean` error and the audit falls back to Unknown — never a wrong
verdict.
- `axiom_audit` copies the source into a fresh temp dir, appends
`#print axioms <name>` per decl, runs `lean`, and — only if that copy
elaborated cleanly — classifies the output. Temp dir is removed after.
- `classify_axioms` (ground-truthed vs Lean 4.13.0): all decls clean or
only {propext, Classical.choice, Quot.sound} → Proven; any `sorryAx` →
Admitted; any other axiom (e.g. `native_decide`'s) → Postulated.
Honest reach: import-free files (the temp-dir copy elaborates without
LEAN_PATH). Imported files can't be audited in a bare temp dir → the audit
returns None → they stay `Unknown` until lake-env resolution (the remaining
M6 follow-on).
## Verified (ran, not inferred)
- `cargo test` → 129 passing, 0 failed (+2 unit: `decl_names`,
`classify_axioms`; the pre-existing lean check_file test updated to be
audit-aware).
- clippy -D warnings, fmt, SPDX clean.
- Dogfooded REAL lean: `rfl` → proven-eligible; `Classical.em` →
proven-eligible (standard axioms); `native_decide` → **postulated** (the
audit catches the non-standard axiom a bare elaboration hides); `sorry`
→ admitted.
- STATE.a2ml: M6 now 92% (remaining: lake-env for imported files).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7
hyperpolymath
marked this pull request as ready for review
July 1, 2026 10:27
hyperpolymath
added a commit
that referenced
this pull request
Jul 1, 2026
) ## What The Flying-Logic reasoning graph can now source **real prover verdicts from a four-state workspace's `proven/` state** without re-running any tool, and demote a **stale-proven** node back to `unknown`. Honest by construction — a verdict only ever comes from a recorded promotion, and staleness always dominates a stale `Proven`. This is the last of the three refinement follow-ons (M4 `.ipkg` roots #41, M6 axiom audit #42, M3 workspace verdicts). ## How - **`reason::workspace_verdicts(dag, proven, stale) -> (verdicts, stale)`** — a pure mapping (no I/O, unit-testable): a node whose file basename is in the workspace's `proven/` set → `Proven`; if that same file is stale (content/closure hash changed since promotion) it is added to the returned stale set, so the existing demote-only fold lowers it to `Unknown`. Matched by file basename (documented collision caveat). Re-exported from `lib.rs`. - **`arghda reason <path> --workspace <ws>`** — reads the proven + stale-proven basename sets off the workspace (`Workspace::list(Proven)` / `Workspace::stale_proven`) and feeds them into `workspace_verdicts`. `--check` stays authoritative: a fresh typecheck overrides the workspace verdict and clears staleness for that node. - **Honest evidence strings** — `"prover: proven"` for a fresh promotion; `"prover: proven; stale: closure hash changed"` for a demoted stale one. ## Verification (actually run) - `cargo fmt --check` — clean - `cargo clippy --all-targets -- -D warnings` — clean - `cargo test` — **130 pass** (+1 reason unit: proven lights the cone, stale demotes) - `bash scripts/check-spdx.sh .` — OK **Dogfooded end-to-end** on a real workspace + Agda source tree: - Scenario A (fresh proven leaf): `Good` → `effective: proven` (`"prover: proven"`); un-proven root `All` → `unknown`. - Scenario B (proven file edited on disk → stale): `Good` demoted to `unknown` with `"prover: proven; stale: closure hash changed"`. ## Scope Additive only. `M3` base was already 100%; this refinement wires the reasoning graph to the triage workspace's ground truth. No change to the `reason/0.1` JSON contract keys. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7 --- _Generated by [Claude Code](https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7)_ Co-authored-by: Claude <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
2 participants
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.
Second refinement follow-on. A clean Lean elaboration is only
Unknownon its own (sorryis a mere warning;native_decide's axiom is invisible to a bare run).check_filenow runs a#print axiomsaudit on a clean elaboration and promotes the verdict honestly.Mechanism (std-only — no new dependency)
decl_namesparses auditable declarations (theorem/lemma/def/abbrev/instance), skipping leading@[..]attributes + modifiers and anonymous decls. Conservative: a missed name just isn't audited; a mis-parsed name makesleanerror and the audit falls back toUnknown— never a wrong verdict.axiom_auditcopies the source into a fresh temp dir, appends#print axioms <name>per decl, runslean, and — only if that copy elaborated cleanly — classifies the output. Temp dir removed after.classify_axioms(ground-truthed vs Lean 4.13.0): all decls clean or only{propext, Classical.choice, Quot.sound}→ Proven; anysorryAx→ Admitted; any other axiom (e.g.native_decide's) → Postulated.Honest reach
Import-free files (the temp-dir copy elaborates without
LEAN_PATH). Imported files can't be audited in a bare temp dir → the audit returnsNone→ they stayUnknownuntil lake-env resolution (the remaining M6 follow-on).Verified (ran, not inferred)
cargo test→ 129 passing, 0 failed (+2 unit:decl_names,classify_axioms; the pre-existing lean check_file test updated to be audit-aware).rfl→proven-eligible;Classical.em→proven-eligible(standard axioms);native_decide→postulated(the audit catches the non-standard axiom a bare elaboration hides);sorry→admitted.Status
M6 now ~92% (remaining: lake-env for imported files). Next: M3 (workspace-fed verdicts + staleness in
reason).Generated by Claude Code