docs(repsel): pin why the delete barrier's per-module scope is sound for proven-this (#7143)

[proggeramlug]

repsel: document and pin why the delete shape barrier's per-module scope is sound for proven-this (#7143)

Investigated #7143 ("the Phase 5a delete shape barrier is module-scoped,
but a proven-this receiver is aliased across modules by construction").
Confirmed the asymmetry the issue describes: ModuleDispatchFacts::has_shape_barrier_sites()
is computed per module (collect_module_dispatch_facts), and Phase 5a's
proven-this admission (collectors/proven_this.rs::method_proven_this)
consults only its OWN module's copy — a delete/Reflect.deleteProperty on
a class instance in a module that imports the class, rather than declaring
it, sets no flag the declaring module's admission decision can see.

No miscompile exists. Built a two-module reproducer
(test-files/test_issue_7143_delete_barrier_cross_module.ts +
test-files/fixtures/issue_7143_pkg/shared.ts) matching the issue's own
suggested shape — module A declares class C { a; b; c } plus a method
reading this.c, admits a $pshape clone since it contains no delete
itself; module B holds an instance A handed it, deletes b off it (which
relocates c's packed slot via perry-runtime's keys-array compaction),
then calls back into module A, which dispatches inst.readC() on the
now-mutated object. The compiled binary's output matches
node --experimental-strip-types exactly (3, 3, 3), and the
--trace llvm IR shows why: EVERY routing site that can call a $pshape
clone independently re-derives soundness at the point it matters, rather
than trusting the per-module admission fact —

• method_direct.fast (lower_call/method_override.rs) sits behind
  js_typed_feedback_method_direct_call_guard / js_method_direct_shape_guard,
  whose contract includes a raw pointer compare of the receiver's live
  keys_array against the class's canonical keys token. delete's only
  code path for a class instance with a keys array
  (perry-runtime/src/object/delete_rest.rs::js_object_delete_field, shared
  by Reflect.deleteProperty) always clones a FRESH keys array, so this
  compare can never pass on a post-delete receiver, from any module.
• The Phase 3b guard-free Ptr<Shape> receiver arm needs no runtime check:
  its containment proof (collectors/ptr_shape.rs rule 2) already rules out
  any alias to the object existing anywhere, so there is nothing for a
  cross-module delete to reach through.
• The repsel Phase 5a: route the class-id dispatch tower to __pshape under an inline keys check (batch.ts: 4 guard calls + 3 by-name field calls per call) #7142 class-id dispatch-tower case
  (dynamic_dispatch.rs::emit_tower_pshape_call) already carries its own
  explicit keys-token re-check, added specifically for this reason — its doc
  comment already cited repsel Phase 5a: the delete shape barrier is module-scoped, but a proven-this receiver is aliased across modules by construction #7143 by number.

Landed as a documentation + regression-test PR, not a bug fix: added a
"delete is aliased across modules by construction" section to
collectors/proven_this.rs stating this invariant explicitly (module-wide
barrier facts are a cost heuristic for Phase 5a, never the correctness
mechanism — a future 4th routing site must independently re-derive a
dominating runtime check or genuine containment), a cross-reference from
collectors/ptr_shape.rs's module-wide barrier rule, a new
guarded_pshape_call_site_is_preceded_by_a_keys_token_guard IR ratchet in
proven_this_routing_tests.rs pinning the method_direct.fast guard
dominance (mirroring the existing tower ratchet), and the two-file
reproducer above as a permanent parity-suite fixture.

Summary by CodeRabbit

• Documentation

  • Clarified safety guarantees for cross-module property deletion and receiver checks.
  • Added a changelog entry documenting the behavior and validation coverage.

• Tests

  • Added regression coverage for cross-module deletion and property access consistency.
  • Added checks confirming appropriate runtime guards are emitted.

• Chores

  • Incremented the project version to 0.5.1417.

[coderabbitai]

📝 Walkthrough

Walkthrough

The changes document cross-module delete barrier safety for proven-this routing, add LLVM IR and runtime regression tests, add a cross-module fixture, update the changelog, and increment the project version to 0.5.1417.

Changes

Cross-module delete barrier validation

Layer / File(s)	Summary
Routing safety documentation and IR regression crates/perry-codegen/src/collectors/proven_this.rs, crates/perry-codegen/src/collectors/ptr_shape.rs, crates/perry-codegen/src/collectors/proven_this_routing_tests.rs	Documents per-module barrier heuristics and adds an IR test that requires guards before proven-this $pshape calls.
Cross-module runtime regression test-files/fixtures/issue_7143_pkg/shared.ts, test-files/test_issue_7143_delete_barrier_cross_module.ts	Adds a shared class fixture and checks direct and callback-based field access after an aliased delete.
Changelog and version updates changelog.d/7722-delete-barrier-scope.md, CLAUDE.md, Cargo.toml	Records the investigation and updates the documented and workspace versions to 0.5.1417.

Estimated code review effort: 2 (Simple) | ~15 minutes

Possibly related issues

• repsel Phase 5a: the delete shape barrier is module-scoped, but a proven-this receiver is aliased across modules by construction #7143 — Adds the cross-module delete regression test and documents per-routing-site safety guarantees.

Possibly related PRs

• PerryTS/perry#6911 — Covers related shape-barrier handling for Ptr<Shape> locals and proven-this routing.
• PerryTS/perry#6925 — Introduces related proven-this clone and Ptr<Shape> barrier logic.
• PerryTS/perry#7141 — Contains related proven-this routing work.

Suggested labels: parity

🚥 Pre-merge checks | ✅ 3 | ❌ 2

❌ Failed checks (2 warnings)

Check name	Status	Explanation	Resolution
Linked Issues check	⚠️ Warning	The changes address issue #7143, but the directly linked issue #39 requires BigInt bitwise and masking fixes that this PR does not provide.	Address issue #39's BigInt XOR, 64-bit masking, and multiplication-wrap requirements, or correct the linked issue association to the delete-barrier issue.
Out of Scope Changes check	⚠️ Warning	The documentation and regression tests concern the cross-module delete barrier, while linked issue #39 concerns incorrect 64-bit BigInt operations.	Unlink issue #39 and link the relevant delete-barrier issue, or limit the PR to changes that address #39's BigInt requirements.

✅ Passed checks (3 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title clearly identifies the documentation focus and the specific proven-this delete-barrier scope addressed by the changes.
Description check	✅ Passed	The description provides a detailed summary, concrete changes, related issue context, and verification results, although it does not follow the template headings exactly.
Docstring Coverage	✅ Passed	Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%.

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch repsel/7143-delete-barrier-scope

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[coderabbitai]

Actionable comments posted: 1

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In `@test-files/test_issue_7143_delete_barrier_cross_module.ts`:
- Around line 3-5: Correct the fixture comment to state that module A
(fixtures/issue_7143_pkg/shared.ts) never mentions delete, while preserving the
existing explanation of module B and the readC$pshape aliasing.

🪄 Autofix

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro Plus

Run ID: 6ccbd1ff-c5f2-4e3d-a15b-7c4674a72921

📥 Commits

Reviewing files that changed from the base of the PR and between 72ef47a and 209e7e9.

⛔ Files ignored due to path filters (1)

• Cargo.lock is excluded by !**/*.lock

📒 Files selected for processing (8)

• CLAUDE.md
• Cargo.toml
• changelog.d/7722-delete-barrier-scope.md
• crates/perry-codegen/src/collectors/proven_this.rs
• crates/perry-codegen/src/collectors/proven_this_routing_tests.rs
• crates/perry-codegen/src/collectors/ptr_shape.rs
• test-files/fixtures/issue_7143_pkg/shared.ts
• test-files/test_issue_7143_delete_barrier_cross_module.ts

[coderabbitai]

📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win

Correct the module reference in the fixture comment.

Line 3 says module B never mentions delete. Line 18 deletes inst.b in module B. State that module A never mentions delete.

Proposed fix

-// aliased across modules by construction. This module (B) never mentions
-// `delete`, so module A (fixtures/issue_7143_pkg/shared.ts) is free to admit
+// aliased across modules by construction. Module A
+// (fixtures/issue_7143_pkg/shared.ts) never mentions `delete`, so it is free to admit

📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change

	// aliased across modules by construction. This module (B) never mentions
	// `delete`, so module A (fixtures/issue_7143_pkg/shared.ts) is free to admit
	// a `readC$pshape` clone for `C.readC` and route `readViaA`'s call to it.
	// aliased across modules by construction. Module A
	// (fixtures/issue_7143_pkg/shared.ts) never mentions `delete`, so it is free to admit
	// a `readC$pshape` clone for `C.readC` and route `readViaA`'s call to it.

🤖 Prompt for AI Agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

In `@test-files/test_issue_7143_delete_barrier_cross_module.ts` around lines 3 -
5, Correct the fixture comment to state that module A
(fixtures/issue_7143_pkg/shared.ts) never mentions delete, while preserving the
existing explanation of module B and the readC$pshape aliasing.

[proggeramlug]

Merging as v0.5.1417 — the answer is "no miscompile", and that is the finding

The asymmetry #7143 describes is real: has_shape_barrier_sites() is per-module, a proven-this receiver is aliased across modules by construction, and a delete in a module that never declares the class sets no flag the declaring module's Phase 5a admission can see.

It is not a miscompile, because in Phase 5a that fact is a cost heuristic only. Correctness comes from elsewhere: every routing site that can call a $pshape clone independently re-derives it via a runtime keys-token guard. The contrast with rule 2 in ptr_shape.rs — where the same per-module fact is the correctness argument, because containment holds there — is now written down in both files instead of being re-derived by whoever looks next.

Why spend a test on a non-bug. The distinction is invisible in the source: nothing at the Phase 5a call site says "this use is advisory". Someone tidying the two uses into a shared helper would silently make the advisory one load-bearing, or the load-bearing one advisory — and that edit would look like a cleanup.

guarded_pshape_call_site_is_preceded_by_a_keys_token_guard asserts every emitted $pshape call site is preceded by js_typed_feedback_method_direct_call_guard or js_method_direct_shape_guard, and first asserts a $pshape call was emitted at all, so it cannot pass by finding nothing to check.

I sabotage-verified it rather than trusting it: pointing the guard predicate at a non-existent symbol fails with

perry_method_pshape_guarded_ts__Counter__bump$pshape: no keys-token guard call
precedes it in `probe` — a post-`delete` receiver (deleted from through an alias
in another module, #7143) would reach this clone's stale fixed-slot loads unguarded

cargo test -p perry-codegen --lib proven_this_routing: 8 passed, 0 failed. Lint 19/19.

One incidental: the added module note pushed ptr_shape.rs to 2003 lines against the 2000-line cap. Condensed to 2000 rather than allowlisted — an allowlist entry for three lines of prose would be the wrong trade.