Skip to content

test(repsel): drive the #7480 element-shape revocation matrix through real mutators - #7608

Merged
proggeramlug merged 5 commits into
mainfrom
perf/7480-element-shape-matrix
Aug 7, 2026
Merged

test(repsel): drive the #7480 element-shape revocation matrix through real mutators#7608
proggeramlug merged 5 commits into
mainfrom
perf/7480-element-shape-matrix

Conversation

@proggeramlug

@proggeramlug proggeramlug commented Aug 7, 2026

Copy link
Copy Markdown
Contributor

Closes the acceptance gap left by #7496: the element-shape invariant shipped with a revocation matrix that never drove a single mutator.

The hole

element_shape_tests.rs has one test for the whole bulk-mutator family:

// `shift`/`unshift`/`splice`/`fill`/`copyWithin`/`reverse`/`sort` all
// mutate slots with bare writes and then land in `rebuild_array_layout`.
let arr = built_from_pushes(CLASS_A, 4);
unsafe { crate::array::header::rebuild_array_layout(arr) };
assert!(proof(arr).is_none());

It calls rebuild_array_layout directly. The comment names seven mutators; the test exercises none of them. Every one could stop reaching that funnel and the suite would stay green — CLAUDE.md's fourth way a gate cannot fail, "the gate runs but its subject never did".

That matters more here than for a normal invariant. The consumers #7480 sequences next (the #5093 versioned-loop clone, then element Ptr<Shape>) hoist a guard out of the loop and emit unguarded reads inside it. A mutation family that silently stops revoking is not a slow path — it is a miscompile that reads a B through an A's layout.

What this adds

crates/perry-runtime/src/array/element_shape_matrix_tests.rs — 25 tests, each driving a real FFI entry point against a proven array and asserting the documented verdict. Contract stated once at the top of the file: MAINTAIN / REVOKE / STRUCTURAL REVOKE.

Beyond "the proof is gone", each revoke also asserts the global epoch advanced — that is the word a consumer's hoisted guard re-reads, so a revoke the epoch does not advertise is a revoke the consumer misses. And each family that is a permutation or same-class rewrite asserts it re-proves with a fresh identity, which separates a conservative revoke from genuine heterogeneity and stops a future "optimisation" from replacing a revoke with a no-op.

Two vacuity guards, both added after sabotage-testing the first cut caught nothing:

  • shaped() asserts the fixture is proven before every op, so a step that found nothing to revoke fails loudly instead of passing.
  • reverse/sort/copyWithin assert the returned receiver is the array that was proven. Without this, returning a fresh (trivially unproven) array satisfies the revoke assertion while revoking nothing.

Audit result: the invariant is sound

Every element-writing site was traced to a funnel. No unhooked path found — the shipped design holds.

family driven through verdict covered by
in-bounds store, matching class js_array_set_f64 MAINTAIN store funnel
contiguous append, matching js_array_push_f64 MAINTAIN + extend store funnel
unchecked store (codegen fast path) js_array_set_f64_unchecked maintain / revoke store funnel
store of a different class / primitive js_array_set_f64 REVOKE store funnel
delete arr[i] js_array_delete REVOKE TAG_HOLE store
arr.length = n (both directions) js_array_set_length REVOKE structural + hole store
pop js_array_pop_f64 STRUCTURAL verified_len mismatch
shift / unshift js_array_{shift,unshift}_f64 REVOKE rebuild + structural
reverse js_array_reverse REVOKE, re-proves rebuild_array_layout
sort js_array_sort_default REVOKE, re-proves store funnel, not rebuild
copyWithin js_array_copy_within REVOKE, re-proves rebuild_array_layout
fill (whole) js_array_fill REVOKE → heals to the filled class rebuild_array_layout
fill (range) js_array_fill_range REVOKE, stays mixed rebuild_array_layout
splice, equal-length replacement js_array_splice REVOKE rebuild_array_layout alone
splice (pure delete) js_array_splice REVOKE, re-proves rebuild + structural
spread build js_array_clone_for_spread never inherits source identity rebuild_array_layout_exact
Array.from family js_array_from_values establishes, never a wrong class store funnel
JSON.parse / #7539 tape (audited) establishes as it fills store funnel

Two findings worth recording:

sort's default path does not use rebuild_array_layout. It is a rank permutation written back through RootedArrayElems::set, so it revokes via the store funnel. Verified by sabotage, not by reading: removing the revoke from rebuild_array_layout leaves the sort test green; removing it from layout_note_slot turns it red. Defence in depth, not redundancy — and not what the shipped comment claims.

Equal-length splice is guarded by exactly one thing. arr.splice(1, 1, otherClassInstance) leaves length unchanged, so the structural verified_len check cannot see it, and the inserted item is written with a bare ptr::write that never reaches the store funnel. Only splice's own rebuild_array_layout catches it.

Sabotage evidence

Each funnel was removed in turn and the suite re-run.

sabotage result
revoke removed from rebuild_array_layout 7 red — reverse, copyWithin, fill, fill-range, equal-length splice, the roll-up, and the pre-existing proxy test
store funnel removed from layout_note_slot 39 red — nothing can establish
revoke removed from js_array_splice only exactly 1 redmatrix_splice_equal_length_replacement_revokes

The third is the load-bearing one: it shows that test is the unique guard for a case no other mechanism can catch. All sabotages reverted; the tree is clean.

Scope and cost

Test-only. The diff is one new #[cfg(test)] file plus its #[cfg(test)] mod declaration. No runtime code, no emitted code, no bookkeeping added — so standing cost on push_cls / churn_alloc / churn_read is zero by construction, not by measurement, and there is no behaviour to A/B against the gap suite. The invariant's own maintenance cost was #7496's to account for.

GC: unchanged, and the argument holds without new work. The record holds four plain integers and no heap pointer — class_id is a registry index that is compared, never dereferenced — so it is correctly absent from gc_register_mutable_root_scanner. Element class_ids live in ObjectHeaders that move with their contents, and the record's address key is moved by transfer_element_shape from inside layout_transfer. The two shipped copying-minor tests in gc/tests/layout_trace/element_shape.rs pass.

Validation

Local, and stated plainly as such — CI's backlog is deep.

  • cargo test -p perry-runtime --no-fail-fast — 1880 passed, 0 failed
  • cargo test -p perry-codegen --lib — green
  • cargo fmt --all -- --check — clean
  • scripts/raw_handle_debt.py — 998 (baseline 998)
  • scripts/addr_class_inventory.py — passed
  • scripts/class_id_collisions.py — passed
  • scripts/check_file_size.sh — passed

Root-dominance corpus not run: no codegen changes.

Follow-up worth filing separately: rebuild_array_layout's doc comment lists sort among the mutators that revoke through it, which the sabotage disproves.

Summary by CodeRabbit

  • Tests

    • Added comprehensive end-to-end coverage for array element-shape validation across mutation operations.
    • Verified proof preservation for valid updates and proper revocation for invalid stores, bulk mutations, length changes, mixed arrays, and holes.
    • Added coverage for proof recovery and class restoration after array fills and rebuilds.
  • Documentation

    • Added a changelog entry summarizing the new validation matrix and audit findings.

Ralph Küpper added 3 commits August 8, 2026 00:42
The shipped invariant's bulk-mutator test calls `rebuild_array_layout`
directly, so it asserts the proxy rather than the subject: every mutator
could stop reaching that funnel and the suite would stay green. That is
CLAUDE.md's fourth way a gate cannot fail.

Adds an end-to-end matrix that drives each mutation family through its real
FFI entry point and asserts the documented verdict, plus the epoch move a
consumer's hoisted guard actually reads.

Claude-Session: https://claude.ai/code/session_01Y1QZ5wUP9gRSwpiweT4Wix
Three additions after sabotage-testing the first cut:

- `reverse`/`sort`/`copyWithin` now assert the returned receiver IS the array
  that was proven. Without it, an implementation returning a fresh (trivially
  unproven) array would satisfy the revoke assertion while revoking nothing.
- Builder cases: a spread clone must never inherit the source's proof
  identity, and `Array.from`-style builders may leave a result unproven but
  must never leave it proven at the wrong class.
- The rebuild-regains-it case #7480 names as acceptance.

Claude-Session: https://claude.ai/code/session_01Y1QZ5wUP9gRSwpiweT4Wix
@coderabbitai

coderabbitai Bot commented Aug 7, 2026

Copy link
Copy Markdown

Review Change Stack

Warning

Review limit reached

@proggeramlug, you've reached your PR review limit, so we couldn't start this review.

Next review available in: 13 minutes

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

How can I continue?

After more reviews become available, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews.

How do review limits work?

CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability.

For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window.

Please refer docs for additional details.

Review details
⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro Plus

Run ID: 61ee4f4d-5ca0-4b7a-af90-2df3a2513fa7

📥 Commits

Reviewing files that changed from the base of the PR and between 677695d and 9ca67b5.

⛔ Files ignored due to path filters (1)
  • Cargo.lock is excluded by !**/*.lock
📒 Files selected for processing (3)
  • CLAUDE.md
  • Cargo.toml
  • crates/perry-runtime/src/array/header.rs
📝 Walkthrough

Walkthrough

This test-only change adds an end-to-end element-shape revocation matrix. It exercises real array FFI mutators and builders, and verifies proof maintenance, epoch changes, fresh identities, structural revocation, and mixed-value rejection.

Changes

Element-shape validation

Layer / File(s) Summary
Proof contract and test fixtures
crates/perry-runtime/src/array/element_shape.rs, crates/perry-runtime/src/array/element_shape_matrix_tests.rs
Adds the matrix test module, verdict definitions, shaped-array fixtures, proof helpers, and fresh-identity assertions.
Direct mutation proof maintenance
crates/perry-runtime/src/array/element_shape_matrix_tests.rs
Tests valid stores and appends, mismatched classes, primitive values, unchecked stores, and deletion.
Bulk and structural revocation
crates/perry-runtime/src/array/element_shape_matrix_tests.rs
Tests reverse, sort, copyWithin, fill, splice, unshift, shift, pop, and length changes through real entry points.
Builder and matrix validation
crates/perry-runtime/src/array/element_shape_matrix_tests.rs, changelog.d/7608-element-shape-revocation-matrix.md
Tests spread clones, rebuilds, Array.from-style construction, homogeneous recovery, mixed-value rejection, and aggregate bulk-mutation coverage. Documents the test scope and audit results.

Estimated code review effort: 3 (Moderate) | ~25 minutes

Possibly related PRs

  • PerryTS/perry#7424: Covers Proxy routing for several array mutators also exercised by this matrix.
  • PerryTS/perry#7496: Implements the element-shape invariant tested by these FFI revocation cases.
  • PerryTS/perry#7501: Introduces runtime layout-revocation behavior covered by the mutation tests.
🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Title check ✅ Passed The title clearly identifies the test-only change and its use of real mutators for the element-shape revocation matrix.
Description check ✅ Passed The description provides a detailed summary, concrete changes, related issue context, test validation, scope, and audit findings.
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check ✅ Passed Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check ✅ Passed Check skipped because no linked issues were found for this pull request.
✨ 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 perf/7480-element-shape-matrix

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

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

Ralph Küpper added 2 commits August 8, 2026 00:53
…vokes through it

Established by #7608's sabotage: removing the revoke here leaves the sort
matrix test green -- sort's default path writes its rank permutation back
through RootedArrayElems::set and revokes through the store funnel.
@proggeramlug
proggeramlug merged commit a211da7 into main Aug 7, 2026
@proggeramlug
proggeramlug deleted the perf/7480-element-shape-matrix branch August 7, 2026 22:54
@proggeramlug

Copy link
Copy Markdown
Contributor Author

Audit before merge — verified, merged as v0.5.1347

The unique-guard proof reproduces exactly: removing js_array_splice's own
rebuild_array_layout call turns exactly one test red —
matrix_splice_equal_length_replacement_revokes — confirming that equal-length
splice has a single guard and this matrix is now its only tripwire. That is the
most valuable kind of sabotage evidence: not "the tests can fail" but "this
specific test is the sole coverage for this specific hole".

Full element-shape family 52/52 green, fmt/file-size/raw-handle (998) clean.
Test-only diff, so no root-dominance or perf surface — the "zero cost by
construction" claim is structurally true.

Folded in at merge: the one-line doc fix the report flagged and correctly
left out of a test-only PR — rebuild_array_layout's comment claimed the dense
sort write-back revokes through it, and #7608's own sabotage proves it does
not (sort revokes through the store funnel via RootedArrayElems::set). A
wrong claim about which funnel revokes is exactly the kind of comment that
misleads the next #5093 implementer, and it now cites the sabotage that
corrected it.

On the scope call: finding the assigned work already merged (#7496) and
pivoting to "does the shipped thing actually have coverage" — rather than
rebuilding it or padding the PR — was the right judgement. It is the sixth
measure-first catch of this campaign, and the first that found the gap in a
merged deliverable's verification rather than in a ticket's numbers. The
#5093 versioned-loop consumer is now genuinely unblocked: unguarded reads in a
cloned loop body are a miscompile if a revocation funnel silently drops out,
and the matrix is what makes that failure visible.

proggeramlug pushed a commit that referenced this pull request Aug 8, 2026
The first consumer of the per-array homogeneous element-shape invariant
(#7496, matrix #7608), which landed with no consumer on purpose.

`for (let j = 0; j < n; j++) sum += keep[j].v` gets a specialized clone
behind a preheader guard on "this array holds the element-shape invariant
at class C". The element read becomes a bare gep+load off a cached
elements base and the field read a bare raw-f64 slot load; the generic
body survives unchanged as the cold arm. Measured 41ms -> 13ms (3.15x),
now at parity with node, at +0 bytes on a program with no qualifying loop.

Revocation mechanism: restrict-the-body, enforced twice — by shape in the
matcher (a single store-free `acc = <pure numeric>` statement) and by
construction in the lowering, which scans every emitted block of the fast
clone for a GC-unsafe call and branches unconditionally to the slow clone
if one survived. Call-freeness is exactly the right property: every way to
revoke the invariant (element store, length change, delete, defineProperty,
prototype surgery) is a runtime call, and so is every allocation that could
move the array. Failure mode: conservative, never unsound.

Claude-Session: https://claude.ai/code/session_01Y1QZ5wUP9gRSwpiweT4Wix
proggeramlug pushed a commit that referenced this pull request Aug 8, 2026
The first consumer of the per-array homogeneous element-shape invariant
(#7496, matrix #7608), which landed with no consumer on purpose.

`for (let j = 0; j < n; j++) sum += keep[j].v` gets a specialized clone
behind a preheader guard on "this array holds the element-shape invariant
at class C". The element read becomes a bare gep+load off a cached
elements base and the field read a bare raw-f64 slot load; the generic
body survives unchanged as the cold arm. Measured 41ms -> 13ms (3.15x),
now at parity with node, at +0 bytes on a program with no qualifying loop.

Revocation mechanism: restrict-the-body, enforced twice — by shape in the
matcher (a single store-free `acc = <pure numeric>` statement) and by
construction in the lowering, which scans every emitted block of the fast
clone for a GC-unsafe call and branches unconditionally to the slow clone
if one survived. Call-freeness is exactly the right property: every way to
revoke the invariant (element store, length change, delete, defineProperty,
prototype surgery) is a runtime call, and so is every allocation that could
move the array. Failure mode: conservative, never unsound.

Claude-Session: https://claude.ai/code/session_01Y1QZ5wUP9gRSwpiweT4Wix
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant