assert_buffer_store_uses_dynamic_fallback greps the whole module for 'getelementptr inbounds i8' — the shadow frame emits one, so 16 tests misfire under PERRY_RS4GC=0

[proggeramlug]

Split out of #7493, which worked around this with a pin. The workaround is correct for today's default but the underlying assertion is wrong, and it will misfire again.

The assertion

crates/perry-codegen/tests/native_proof_regressions.rs:

fn assert_buffer_store_uses_dynamic_fallback(ir: &str) {
    assert!(ir.contains("call void @js_buffer_set"), ...);
    assert!(!ir.contains("getelementptr inbounds i8"), ...);   // <— this one
}

Same shape at native_proof_regressions.rs:846 and twice in native_proof_buffer_views.rs (:606, :682).

The intent is "no native buffer GEP was emitted for this store". What it actually says is "this module contains no getelementptr inbounds i8 anywhere".

Why that breaks

The shadow-stack lowering's inline slot addressing (#7088) computes the slot address with getelementptr inbounds i8, for reasons that have nothing to do with a buffer. So under PERRY_RS4GC=0 — the sweep a GC engineer runs, and the one #7493's own diagnosis was built on — sixteen tests report a stale proof that was never emitted:

native_proof_regressions/invalidation.rs (15): localset_invalidates_native_i32_alias_facts, update_invalidates_native_i32_alias_facts, localset_invalidates_min_length_facts, localset_invalidates_active_bounded_buffer_index_facts, inner_loop_bounded_buffer_fact_is_removed_after_outer_fact_invalidation, localset_invalidates_buffer_view_local_length_sources, update_invalidates_buffer_view_local_length_sources, negative_loop_counter_does_not_emit_inbounds_buffer_gep, decrementing_loop_update_does_not_emit_inbounds_buffer_gep, body_counter_mutation_does_not_emit_inbounds_buffer_gep, inclusive_length_loop_does_not_emit_inbounds_buffer_gep, inclusive_local_length_bound_does_not_use_local_length_bound_fact, negative_loop_counter_does_not_use_local_length_bound_fact, body_mutation_of_local_bound_does_not_use_local_length_bound_fact, negative_loop_counter_does_not_use_min_length_bound_fact

native_proof_buffer_views.rs (1): loop_length_bound_does_not_prove_multibyte_buffer_read_inbounds

#7493 pinned all sixteen to NativeRootsPin::native(). That is honest — the assertion is only valid under native roots today — and it stops the false alarm. It does not make the assertion right.

Why the pin is not the fix

The proxy is unsound in the other direction too. It cannot distinguish:

• a native buffer GEP for the store under test (what it means to catch), from
• a native buffer GEP for an unrelated proven access elsewhere in the same module (a false positive it would also report), from
• any other inbounds i8 the backend happens to emit (what actually bit us).

Any future pass that emits an inbounds i8 — a string-data address, an inline-cache slot, a native field offset — turns all sixteen red for a reason unrelated to their subject, exactly as the shadow frame did.

What to build

Scope the search to the store/read site:

• cut the function body under test (the file already has enclosing_function / init_ir style helpers), then
• find the js_buffer_set / typed-array call the fixture drives, and assert that the operand feeding it was not produced by an inbounds GEP off the buffer's data pointer — i.e. follow the data-flow rather than grepping the text. temp_root_operand_temporaries.rs already walks defs backwards this way (def_of / reaches_alloc), so the technique is in-tree.

Then remove the sixteen NativeRootsPin::native() pins: the fact-invalidation contract is lowering-independent and should be asserted that way.

Acceptance

• The sixteen pass under BOTH lowerings, unpinned.
• Sabotage-checked: restoring the stale proof (letting the invalidated fact through) must fail each of them.
• grep -rn 'contains("getelementptr inbounds i8")' crates/perry-codegen/tests/ returns nothing module-scoped.

[proggeramlug]

Fixed in #7675. Verdict: vacuous — the assertion was satisfiable by any instruction in the module, and had been since the shadow lowering started emitting getelementptr inbounds i8 for slot addressing.

What replaced it. native_proof_support::native_buffer_element_geps accepts an inbounds i8 GEP only when its base pointer was loaded out of a Buffer view's DATA slot. A data slot is recognised by either shape codegen materialises one with — the initialising store (and i64 …, 0xFFFF_FFFF_FFFF → inttoptr → header-skip GEP → store ptr), or the header length read (load ptr → getelementptr i8 by the length offset → load i32 …, !invariant.load). Both suites share the one reader via the existing #[path] include, so a third copy cannot drift.

Two properties the old proxy did not have:

• it is scoped to @probe, cut from the define line rather than a substring — perf(repsel): resolve object-literal element types in the element-shape loop clone (#7480) #7669's fast_clone_slice is why that is now written down; and
• assert_no_native_buffer_element_access panics when the function lowered no buffer view at all, so "no native GEP" and "nothing here to have one" cannot be confused. The self-test a_body_with_no_buffer_view_refuses_to_certify_the_absence_of_one asserts that refusal.

All sixteen NativeRootsPin::native() pins are removed. The tests pass under the native default and under PERRY_RS4GC=0.

Sabotage, run. Deleting the slots.contains(&slot) filter in native_buffer_element_geps — i.e. degrading the reader back into the module-wide grep this issue is about — turns 19 tests red under PERRY_RS4GC=0: the fifteen invalidation tests, the new control, and the self-test the_buffer_gep_reader_ignores_the_shadow_frames_own_inline_slot_gep, which plants the exact shadow-frame GEP shape that caused the false alarm.

Non-vacuity in the other direction. invalidation::the_native_buffer_gep_detector_fires_on_a_proven_store compiles the same store with its proof intact and requires the reader to SEE the unchecked native address, under both lowerings, then requires the invalidated twin not to. Without that, the fifteen negatives would again be a claim nobody has watched go the other way.

grep -rn 'contains("getelementptr inbounds i8")' crates/perry-codegen/tests/ now returns nothing.