anuna-research/cbcl-rs
1
0
Fork 0
Code Issues 2 Pull requests Projects Packages Wiki Activity Actions

lean-cbcl review cleanup: simp hygiene, heartbeat scoping, total recursion, proof refactor #8

Closed
anuna-02 wants to merge 0 commits from refs/pull/8/head into main AGit
pull from: refs/pull/8/head
merge into: anuna-research:main
Conversation 0 Commits - Files changed -
anuna-02 commented 2026-05-04 11:48:13 +00:00 (Migrated from codeberg.org)
Copy link

Summary

Address all 8 actionable findings from a recent lean-cbcl/ review pass on main (no sorries / axiom regressions found — every finding was quality / style).

Plan: lean-cbcl/review-fixes.spl — hence SPL with 11 dependency-aware tasks (10 fix tasks + 1 final-audit task). All 11 completed.

Changes

Finding Fix
DetParser: 16 trivial @[simp] literal lemmas (one_lt_200..ninetyNine_ne_zero) polluting global simp set Removed; langDetParser_step_state_lt / _ne_zero proofs use <;> omega
DetParser: bump/reset pair set_option maxHeartbeats 800000/200000 Scoped via set_option maxHeartbeats 400000 in on the two theorems that need it
Serializer: file-level set_option maxHeartbeats 3200000 (32×) Removed entirely — no theorem actually needed it
DeterministicUnion: file-level set_option maxHeartbeats 1600000 (16×) Removed entirely — no theorem actually needed it
DialectParser: partial def parseDialectClauses Made total via termination_by clauses.length (no decreasing_by needed)
Pipeline: 70-line repetitive pipeline_success_implies_valid Extracted private helper pipeline_success_eq_msg; 54% LOC reduction on the proof body
R5: quadratic DFS fuel |names|² + 1 Tightened to linear |names| + 1 for both checkAcyclicity and checkReachability; h_fuel proofs simplified
AxiomAudit: ContentHash.instNonempty listed in allowlist but not exercised Axiom removed (Lattice/Store.lean), removed from AxiomAudit.lean allowlist + scripts/check-axioms.sh
Stale lean-cbcl/proof-gaps.spl (all tasks marked completed) Deleted
.DS_Store artefacts repeatedly appearing in git status Added **/.DS_Store to .gitignore

Verification

  • cd lean-cbcl && lake build — clean (40/40 jobs) on leanprover/lean4:v4.27.0
  • bash scripts/check-axioms.sh — OK: 16 theorem(s) audited; all axioms allowlisted
  • Audited axiom set: standard kernel (propext, Classical.choice, Quot.sound) + 4 custom (ContentHash, contentHash, contentHash_injective, Message.causedBy) — net one fewer custom axiom than before (instNonempty was unused)
  • All CON-510..516 contract theorems still elaborate without modification

Test plan

  • lake build is green on a fresh clone
  • scripts/check-axioms.sh exits 0
  • Spot-check the pipeline_success_eq_msg helper proof
  • Confirm R5.lean linear-fuel change preserves runtime intent (checkAcyclicity_base / checkReachability_base native_decide baselines still fast)

🤖 Generated with Claude Code

## Summary Address all 8 actionable findings from a recent `lean-cbcl/` review pass on `main` (no sorries / axiom regressions found — every finding was quality / style). Plan: [`lean-cbcl/review-fixes.spl`](./lean-cbcl/review-fixes.spl) — hence SPL with 11 dependency-aware tasks (10 fix tasks + 1 final-audit task). All 11 completed. ## Changes | Finding | Fix | |---|---| | `DetParser`: 16 trivial `@[simp]` literal lemmas (`one_lt_200`..`ninetyNine_ne_zero`) polluting global simp set | Removed; `langDetParser_step_state_lt` / `_ne_zero` proofs use `<;> omega` | | `DetParser`: bump/reset pair `set_option maxHeartbeats 800000`/`200000` | Scoped via `set_option maxHeartbeats 400000 in` on the two theorems that need it | | `Serializer`: file-level `set_option maxHeartbeats 3200000` (32×) | Removed entirely — no theorem actually needed it | | `DeterministicUnion`: file-level `set_option maxHeartbeats 1600000` (16×) | Removed entirely — no theorem actually needed it | | `DialectParser`: `partial def parseDialectClauses` | Made total via `termination_by clauses.length` (no `decreasing_by` needed) | | `Pipeline`: 70-line repetitive `pipeline_success_implies_valid` | Extracted `private` helper `pipeline_success_eq_msg`; **54% LOC reduction** on the proof body | | `R5`: quadratic DFS fuel `\|names\|² + 1` | Tightened to linear `\|names\| + 1` for both `checkAcyclicity` and `checkReachability`; `h_fuel` proofs simplified | | `AxiomAudit`: `ContentHash.instNonempty` listed in allowlist but not exercised | Axiom removed (`Lattice/Store.lean`), removed from `AxiomAudit.lean` allowlist + `scripts/check-axioms.sh` | | Stale `lean-cbcl/proof-gaps.spl` (all tasks marked completed) | Deleted | | `.DS_Store` artefacts repeatedly appearing in `git status` | Added `**/.DS_Store` to `.gitignore` | ## Verification - `cd lean-cbcl && lake build` — clean (40/40 jobs) on `leanprover/lean4:v4.27.0` - `bash scripts/check-axioms.sh` — `OK: 16 theorem(s) audited; all axioms allowlisted` - Audited axiom set: standard kernel (`propext`, `Classical.choice`, `Quot.sound`) + 4 custom (`ContentHash`, `contentHash`, `contentHash_injective`, `Message.causedBy`) — net **one fewer** custom axiom than before (`instNonempty` was unused) - All CON-510..516 contract theorems still elaborate without modification ## Test plan - [ ] `lake build` is green on a fresh clone - [ ] `scripts/check-axioms.sh` exits 0 - [ ] Spot-check the `pipeline_success_eq_msg` helper proof - [ ] Confirm `R5.lean` linear-fuel change preserves runtime intent (`checkAcyclicity_base` / `checkReachability_base` `native_decide` baselines still fast) 🤖 Generated with [Claude Code](https://claude.com/claude-code)

Pull request closed

Please reopen this pull request to perform a merge.
Sign in to join this conversation.
Reviewers
No reviewers
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Assignees
Clear assignees
No assignees
1 participant
Notifications
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference
anuna-research/cbcl-rs!8
No description provided.