You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
fix(gate-manifest): reject shadowed bindings and value-changing provenance chains
Addresses both P2s from the re-review at 9f06c00.
Block/catch/loop shadowing. The proof modelled only function parameters, so a
`const entry` in a nested block — or a catch parameter, or a destructured
binding — shadowed the ownership callback parameter invisibly, and resolution
fell back to the ownership binding and exempted a dynamic rule.
Rather than model every scoping construct, shadowsParameter refuses the
exemption whenever the name is re-declared ANYWHERE inside the callback, by any
construct, including destructuring patterns. That over-refuses in principle — a
re-declaration in a sibling block cannot reach the call site — and fails closed,
which is the right direction for a proof whose job is to be conservative.
Provenance. iteratesOwnershipTable accepted any chain rooted at the table, so
`BUILD_OWNERSHIP.map(transform).map((entry) => entry.rule)` qualified even
though `transform` can return anything and the downstream elements are no longer
table entries. yieldsOwnershipEntries now walks the chain and requires every
intervening method to be value-preserving (filter/slice/reverse/sort/toSorted/
toReversed). `.map(transform)` mid-chain breaks the proof; the real
`BUILD_OWNERSHIP.filter(...).map(cb)` still holds.
Tests 46 → 50: nested-block re-declaration, catch parameter and destructured
re-declaration, a value-changing chain, and a value-preserving `.filter().slice()`
chain proving the legitimate case still resolves and loses no category.
rootIdentifier is gone — yieldsOwnershipEntries replaced it.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01SkS4S8XXrfkJ8TD1VBKkvJ
0 commit comments