Skip to content

R3 gate #21: int refinement overflow proven parametric - #2674

Merged
briansrls merged 3 commits into
mainfrom
session/witty-dove-427
May 11, 2026
Merged

briansrls merged 3 commits into
mainfrom
session/witty-dove-427

Conversation

@briansrls

@briansrls briansrls commented May 11, 2026 •

Copy link
Copy Markdown
Contributor

Summary

Strengthens the R3 gate #21 receipt for int_refinement_overflow_proven_parametric by extending the integration coverage for fixed-width integer overflow through the shared MagnitudeOutOfRange path. The receipt now covers additional signed/unsigned width refinements, including Int64, representable Int128::MAX + 1, upper UInt64, and the existing UInt128 lower-bound case.

This is a test-harness receipt change only; no substrate or compiler runtime behavior is changed.

P5 Receipt

P5 explicit deferral receipt: this PR expands an existing hand-authored v3 Rust integration test under src/v3/compiler/tests/integration/int_literal_cardinality_test.rs without adding a new SG-0 path. Lane = T-PB-B / T-Tests-As-Data-Completeness. Concrete ROADMAP row = ROADMAP.md §"Release R1 Program" / "Hand-Rust census" row, which states that the test subset of the SG-0 census migrates to .dag TestClaim declarations and trends to zero Rust-authored tests. This PR keeps the receipt in the existing hand-Rust harness because gate #21 needs executable coverage before the Cluster M / gate #84 bulk migration lands.

SG-0 hand-path delta: 0 (no edits to src/v3/compiler/tests/integration/sg0_census_test.rs; no new hand-authored test path added).

Test plan

  • cargo fmt -p v3-compiler — passed
  • cargo test -p v3-compiler --test integration int_refinement_overflow_is_proven_parametric_for_representable_widths -- --nocapture — passed on BuildBuddy

@briansrls
briansrls marked this pull request as ready for review May 11, 2026 04:47
@briansrls

Copy link
Copy Markdown
Contributor Author

Addressed the P5 receipt finding by replacing the dashboard-template PR body with a concrete hand-Rust deferral receipt: T-PB-B / T-Tests-As-Data-Completeness, ROADMAP.md Hand-Rust census row, plus SG-0 hand-path delta: 0. No code change was needed for this review item. — sent from witty-dove-427

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: 433fa712 · Trigger: schedule
  • Thinking: 141s wall

✅ The test-only expansion looks scoped and clean; it exercises the shared MagnitudeOutOfRange path for Int64, Int128, and UInt64 upper-bound overflow without adding substrate state.

@briansrls
briansrls merged commit 0f9a5b6 into main May 11, 2026
7 of 8 checks passed
@briansrls
briansrls deleted the session/witty-dove-427 branch June 1, 2026 18:43
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