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

fix(lean): close three audit findings (BUG-001/002/003) #2

Merged
hugooconnor merged 0 commits from refs/pull/2/head into main 2026-04-18 11:14:45 +00:00
Conversation 0 Commits - Files changed -
hugooconnor commented 2026-04-17 22:32:51 +00:00 (Migrated from codeberg.org)
Copy link

Adversarial audit of the Lean 4 formalisation against the LangSec '26
camera-ready flagged three issues: one vacuous theorem and two with
vestigial premises that misrepresented what the proofs actually establish.
This PR files the reports and lands fixes so the Lean artefact is honest
in isolation. The paper is already submitted — paper-prose mismatches are
noted for the next arXiv revision.

  • BUG-001 (Parser.lean, S3): WellFormedSExpr admitted every SExpr,
    making allSExpr_wellFormed vacuous. Renamed to IsSExpr (structural
    classifier, documented), and added not_roundTrippable_empty_symbol in
    Serializer.lean as a concrete non-vacuity witness against the stronger
    RoundTrippable' predicate.
  • BUG-002 (R3CorePreservation.lean / Agent.lean, S3): install_preserves_core
    carried _hr3 : verifyR3 d = true as an unused premise over a trivial
    wellFormed invariant. Strengthened Agent.wellFormed to a positional
    invariant (base dialect is first + every installed non-base dialect
    satisfies noCoreRedefinition), made hr3 load-bearing, and added
    install_no_core_redefinition as the composition witness.
    Follow-up commit closes a base-name spoofing gap surfaced by
    cross-model review: spoofedBaseDialect (name "cbcl-base", redefines
    tell) passed verifyR3's name short-circuit but now fails
    noCoreRedefinition; hname premise ensures the short-circuit cannot
    be used to bypass the obligation.
  • BUG-003 (DeterministicUnion.lean, S2): dcfl_preserved and the
    parallel decidable_preserved each carried vestigial _hwf/_hR3
    premises. DCFL is a grammar-union closure property; R3's semantic core
    constraint is at the wrong layer to compose through. Dropped the
    vestigial premises; the retained namesUnique + hFresh signature is
    strictly stronger than what the paper claimed. Comments at each site
    explain why R3/wellFormed are not premises.

Implementation tracked in plans/FIX-LEAN-AUDIT.spl (hence plan).
Audit writeup lives in the sibling repo at
cbcl-paper/plans/lean-audit-findings.md.

Test plan

  • lake build in lean-cbcl/: 35/35 jobs green
  • cargo test --workspace: 508 passed
  • Regression: spoofedBaseDialect is rejected by the new
    wellFormed invariant (BUG-002 follow-up)
  • dcfl_preserved and decidable_preserved signatures contain no
    underscore-prefixed parameters
  • not_roundTrippable_empty_symbol witnesses non-vacuity for
    RoundTrippable'
  • Cross-model review of the fix commits (per USDD Tier 2 — partially
    done, revealed the spoof; another pass recommended before merge)
Adversarial audit of the Lean 4 formalisation against the LangSec '26 camera-ready flagged three issues: one vacuous theorem and two with vestigial premises that misrepresented what the proofs actually establish. This PR files the reports and lands fixes so the Lean artefact is honest in isolation. The paper is already submitted — paper-prose mismatches are noted for the next arXiv revision. - **BUG-001** (`Parser.lean`, S3): `WellFormedSExpr` admitted every `SExpr`, making `allSExpr_wellFormed` vacuous. Renamed to `IsSExpr` (structural classifier, documented), and added `not_roundTrippable_empty_symbol` in `Serializer.lean` as a concrete non-vacuity witness against the stronger `RoundTrippable'` predicate. - **BUG-002** (`R3CorePreservation.lean` / `Agent.lean`, S3): `install_preserves_core` carried `_hr3 : verifyR3 d = true` as an unused premise over a trivial `wellFormed` invariant. Strengthened `Agent.wellFormed` to a positional invariant (base dialect is first + every installed non-base dialect satisfies `noCoreRedefinition`), made `hr3` load-bearing, and added `install_no_core_redefinition` as the composition witness. **Follow-up commit closes a base-name spoofing gap** surfaced by cross-model review: `spoofedBaseDialect` (name `"cbcl-base"`, redefines `tell`) passed `verifyR3`'s name short-circuit but now fails `noCoreRedefinition`; `hname` premise ensures the short-circuit cannot be used to bypass the obligation. - **BUG-003** (`DeterministicUnion.lean`, S2): `dcfl_preserved` and the parallel `decidable_preserved` each carried vestigial `_hwf`/`_hR3` premises. DCFL is a grammar-union closure property; R3's semantic core constraint is at the wrong layer to compose through. Dropped the vestigial premises; the retained `namesUnique` + `hFresh` signature is strictly stronger than what the paper claimed. Comments at each site explain why R3/wellFormed are not premises. Implementation tracked in `plans/FIX-LEAN-AUDIT.spl` (hence plan). Audit writeup lives in the sibling repo at `cbcl-paper/plans/lean-audit-findings.md`. ## Test plan - [x] `lake build` in `lean-cbcl/`: 35/35 jobs green - [x] `cargo test --workspace`: 508 passed - [x] Regression: `spoofedBaseDialect` is rejected by the new `wellFormed` invariant (BUG-002 follow-up) - [x] `dcfl_preserved` and `decidable_preserved` signatures contain no underscore-prefixed parameters - [x] `not_roundTrippable_empty_symbol` witnesses non-vacuity for `RoundTrippable'` - [ ] Cross-model review of the fix commits (per USDD Tier 2 — partially done, revealed the spoof; another pass recommended before 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!2
No description provided.