native_proof_regressions: 16 tests red on main, and the suite is not per-PR gated #7245

Activity

1. proggeramlug commented on Aug 2, 2026

   

   proggeramlug

   on Aug 2, 2026

   ContributorAuthor

   More actions

   Confirmed still open on main = d4ac65f21. Re-verified in the sweep #7262.

   cargo test --profile perry-dev -p perry-codegen --test native_proof_regressions
   → test result: FAILED. 235 passed; 16 failed; 0 ignored
   

   The failing set is byte-identical to the one in this issue — 15 × invalidation::* plus typed_f64_receiver_method_clone_raw_loads_after_composed_guards:

   invalidation::body_counter_mutation_does_not_emit_inbounds_buffer_gep
   invalidation::body_mutation_of_local_bound_does_not_use_local_length_bound_fact
   invalidation::decrementing_loop_update_does_not_emit_inbounds_buffer_gep
   invalidation::inclusive_length_loop_does_not_emit_inbounds_buffer_gep
   invalidation::inclusive_local_length_bound_does_not_use_local_length_bound_fact
   invalidation::inner_loop_bounded_buffer_fact_is_removed_after_outer_fact_invalidation
   invalidation::localset_invalidates_active_bounded_buffer_index_facts
   invalidation::localset_invalidates_buffer_view_local_length_sources
   invalidation::localset_invalidates_min_length_facts
   invalidation::localset_invalidates_native_i32_alias_facts
   invalidation::negative_loop_counter_does_not_emit_inbounds_buffer_gep
   invalidation::negative_loop_counter_does_not_use_local_length_bound_fact
   invalidation::negative_loop_counter_does_not_use_min_length_bound_fact
   invalidation::update_invalidates_buffer_view_local_length_sources
   invalidation::update_invalidates_native_i32_alias_facts
   typed_f64_receiver_method_clone_raw_loads_after_composed_guards
   

   So the count has neither grown nor shrunk across #7243/#7249/#7250/#7252/#7253/#7256 — consistent with this issue's finding that they are unrelated to #7242, and evidence that nothing is actively churning them.

   Ask (1) — are these stale expectations or real invalidation regressions — is still unanswered and is the one that matters, for the reason stated: if they are real, type proofs are surviving events that should kill them, which is a soundness surface.
2. proggeramlug

   added 2 commits that reference this issue on Aug 5, 2026

   fix(codegen): reserve `$` for generated clone suffixes so user member…

   ...

   6111156

   fix(codegen): unforgeable generated-clone symbol namespace (#6927) (#…

   ...

   835a381
3. proggeramlug commented on Aug 10, 2026

   

   proggeramlug

   on Aug 10, 2026

   ContributorAuthor

   More actions

   All three asks are satisfied on main @ db44b31b7. Re-measured rather than trusted, because this issue's own count is the kind that goes stale.

   Ask 1 — triage the 16

   15 of the 16 have self-healed. cargo test -p perry-codegen --test native_proof_regressions now reports:

   test result: FAILED. 261 passed; 1 failed
       typed_f64_receiver_method_clone_raw_loads_after_composed_guards
   

   and the invalidation::* family specifically is 44 passed / 0 failed. So the answer to "stale expectations or real invalidation regressions?" is: neither, any more — they were fixed by unrelated work between the filing and now, with nothing recording it. That is the same bookkeeping failure #7708 hit (4 of its 6 named failures had already been fixed) and #797 records for the parity skip-list, so it is worth stating plainly: re-measure before acting on a ticket's failure list.

   The one survivor is #7506's subject — the guard-failure edge no longer calling $generic — which is open and tracked separately.

   Ask 2 — get it per-PR gated

   Done, by #7748. native_proof_regressions is in ci_e2e_scope.py's SOURCE_SUITE_MAP (one of 22 mapped perry-codegen suites), and test.yml's e2e-scoped job runs on pull_request. ci_e2e_scope.py --self-test passes, and the tool refuses to pass if a suite on disk is in neither the map nor the exclusions — so a new suite cannot go dark the way this one did.

   Ask 3 — the suite must not be left red

   Handled the way this repo's own note in that file demands: exclude a TEST, never a SUITE. SUITE_EXCLUSIONS names exactly

   perry-codegen | native_proof_regressions
     | typed_f64_receiver_method_clone_raw_loads_after_composed_guards
     | "#7506 — … The other 261 tests pass."
   

   so 261 tests' worth of proof-invalidation coverage runs on every PR instead of being held out for one failure. And the exclusion cannot rot: e2e-scoped runs exactly the excluded tests and fails the job if one PASSES, with instructions to delete the entry — a fix for #7506 cannot land while leaving its exclusion behind.

   Closing. The soundness concern this issue raised — that the machinery deciding when a type proof stops being valid was not consulted on any PR — no longer holds: invalidation::* is green and gated.
4. proggeramlug

   closed this as completedon Aug 10, 2026