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

lean-cbcl review cleanup + R5 linear-fuel regression guards #9

Merged
anuna-02 merged 0 commits from refs/pull/9/head into main 2026-05-05 02:02:36 +00:00
Conversation 0 Commits - Files changed -
anuna-02 commented 2026-05-05 01:50:33 +00:00 (Migrated from codeberg.org)
Copy link

Summary

Addresses the 8 actionable findings from the lean-cbcl review (lean-cbcl/review-fixes.spl) plus a follow-up runtime regression guard for the R5 fuel-bound change.

Code

  • DetParser — drop 16 trivial @[simp] literal lemmas; scope the heartbeat bump (800000 → 400000) to the two theorems that need it via set_option ... in, instead of a file-level maxHeartbeats.
  • Serializer / DeterministicUnion — remove unnecessary file-level maxHeartbeats bumps (proofs go through under the default 200000).
  • DialectParser — make parseDialectClauses total via termination_by clauses.length; no more partial def.
  • Pipeline — extract pipeline_success_eq_msg helper to deduplicate pipeline_success_implies_valid (~54% LOC reduction). Helper proof uses simp only + split at h to enumerate post-validation match leaves; closes each with cases h; rfl (success leaf) or cases h via noConfusion (validationError leaf).
  • R5 — tighten DFS fuel bound from quadratic |names|² + 1 to linear |names| + 1 for both checkAcyclicity and checkReachability; update related h_fuel proofs (now just rw [h_keys]; exact Nat.le_refl _) and docstrings. The new bound is exactly what dfsNoCycle_top_level_acyclic / dfsReaches_complete_top_level require — sound, not slack.
  • R5 (this branch's second commit) — add baseProtocol fixture (mirroring Rust's linear_protocol() test helper in crates/cbcl-core/src/protocol.rs) plus checkAcyclicity_base / checkReachability_base native_decide regression guards alongside R1's checkNoCycles_base. Pins runtime behaviour so any future fuel regression or DFS termination bug fails at compile time.
  • Lattice/Store + AxiomAudit + scripts/check-axioms.sh — remove unused ContentHash.instNonempty axiom and its allowlist entries (the audited theorems didn't transitively depend on it; documented in the AxiomAudit header for future re-introduction if needed).

Hygiene

  • Add **/.DS_Store to .gitignore.
  • Delete stale lean-cbcl/proof-gaps.spl (all tasks completed in the merged IMPL-005 PR).
  • Add lean-cbcl/review-fixes.spl documenting this work.

Verification

  • lake build clean — 40/40 jobs, exit 0.
  • scripts/check-axioms.sh — OK: 16 theorem(s) audited; all axioms allowlisted. Exit 0. The new _base regression guards are intentionally not added to the audit (same pattern as R1's checkNoCycles_base); they're concrete-instance runtime checks, not CON-515 contract obligations, and would otherwise leak Lean.ofReduceBool / Lean.trustCompiler into the allowlist.

Test plan

  • lake build is green on a fresh clone (clean + rebuild).
  • scripts/check-axioms.sh exits 0.
  • Spot-check the pipeline_success_eq_msg helper proof for soundness.
  • Confirm R5 linear-fuel change preserves runtime intent (checkAcyclicity_base / checkReachability_base evaluate instantly via native_decide).
## Summary Addresses the 8 actionable findings from the lean-cbcl review (`lean-cbcl/review-fixes.spl`) plus a follow-up runtime regression guard for the R5 fuel-bound change. ### Code - **DetParser** — drop 16 trivial `@[simp]` literal lemmas; scope the heartbeat bump (800000 → 400000) to the two theorems that need it via `set_option ... in`, instead of a file-level `maxHeartbeats`. - **Serializer / DeterministicUnion** — remove unnecessary file-level `maxHeartbeats` bumps (proofs go through under the default 200000). - **DialectParser** — make `parseDialectClauses` total via `termination_by clauses.length`; no more `partial def`. - **Pipeline** — extract `pipeline_success_eq_msg` helper to deduplicate `pipeline_success_implies_valid` (~54% LOC reduction). Helper proof uses `simp only` + `split at h` to enumerate post-validation match leaves; closes each with `cases h; rfl` (success leaf) or `cases h` via `noConfusion` (validationError leaf). - **R5** — tighten DFS fuel bound from quadratic `|names|² + 1` to linear `|names| + 1` for both `checkAcyclicity` and `checkReachability`; update related `h_fuel` proofs (now just `rw [h_keys]; exact Nat.le_refl _`) and docstrings. The new bound is exactly what `dfsNoCycle_top_level_acyclic` / `dfsReaches_complete_top_level` require — sound, not slack. - **R5** (this branch's second commit) — add `baseProtocol` fixture (mirroring Rust's `linear_protocol()` test helper in `crates/cbcl-core/src/protocol.rs`) plus `checkAcyclicity_base` / `checkReachability_base` `native_decide` regression guards alongside R1's `checkNoCycles_base`. Pins runtime behaviour so any future fuel regression or DFS termination bug fails at compile time. - **Lattice/Store + AxiomAudit + scripts/check-axioms.sh** — remove unused `ContentHash.instNonempty` axiom and its allowlist entries (the audited theorems didn't transitively depend on it; documented in the AxiomAudit header for future re-introduction if needed). ### Hygiene - Add `**/.DS_Store` to `.gitignore`. - Delete stale `lean-cbcl/proof-gaps.spl` (all tasks completed in the merged IMPL-005 PR). - Add `lean-cbcl/review-fixes.spl` documenting this work. ## Verification - `lake build` clean — 40/40 jobs, exit 0. - `scripts/check-axioms.sh` — `OK: 16 theorem(s) audited; all axioms allowlisted.` Exit 0. The new `_base` regression guards are intentionally not added to the audit (same pattern as R1's `checkNoCycles_base`); they're concrete-instance runtime checks, not CON-515 contract obligations, and would otherwise leak `Lean.ofReduceBool` / `Lean.trustCompiler` into the allowlist. ## Test plan - [x] `lake build` is green on a fresh clone (clean + rebuild). - [x] `scripts/check-axioms.sh` exits 0. - [x] Spot-check the `pipeline_success_eq_msg` helper proof for soundness. - [x] Confirm R5 linear-fuel change preserves runtime intent (`checkAcyclicity_base` / `checkReachability_base` evaluate instantly via `native_decide`).
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!9
No description provided.