Repository navigation
t27b: check_elide_plan, two overflow traps that cannot fire leave the hot loop (Refs #12871) - #13397
Merged
Merged
Conversation
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…t for the lab (Refs #12871) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ements (Refs #12871) Glue in lower.rs rewrites sites accepted by check_elide_plan.t27 to AddW/SubW. The gen is the lab output of check_elide_plan.t27. Deletes an unreferenced script to pay the foreign-line budget. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…DIT Keep row (Refs #12871) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Contributor
induction_elides takes nested_loop, the glue reports writes under a nested while, a witness and a refusal test follow. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Contributor
PR DashboardGenerated at: 2026-11-09 07:12:32 UTC
Summary
Seal Status
|
…1509 (Refs #12871) Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Contributor
PR DashboardGenerated at: 2026-11-09 07:17:22 UTC
Summary
Seal Status
|
Collaborator
Author
|
Review fix: an increment inside an inner while keeps its trap (induction_elides takes nested_loop; witness nested_inc plus a refusal test). Head ae5cfe7. Lab run 42578328864 green: check_elide_plan 16/16, check_elide 11/11, bench_audit 1/1, inline_select 17/17, no vacuous; bench_audit asm t27b=15 gcc_O2=10 (master 16). The trapping input nested_inc(255, 254) is not asserted, a test cannot catch a trap. 🤖 Generated with Claude Code |
gHashTag
marked this pull request as ready for review
November 9, 2026 07:39
This was referenced Nov 9, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
t27b drops the overflow trap of two checked ops that cannot fire. The law is
specs/tri/t27b/check_elide_plan.t27(15 tests, refusals included): (a) the induction incrementi = i + 1underwhile (i < n), and (b)x - k(k <= c) afterx = x + c. The witnesses arespecs/tri/shootout/check_elide.t27(u64, i64, u8, both (b) shapes, five refusal shapes; 10 tests). Glue incli/t27b/src/lower.rsreads the facts and rewrites accepted sites from Add/Sub to AddW/SubW; the decisions come from the generatedgen/rust/tri/t27b/check_elide_plan.rs(lab output, committed unedited, mounted with#[path]). First seals for both specs are included. Also deletes the unreferencedscripts/bulk-create-notebooks.sh(its port spec is on master) and drops its name from theMIGRATION_AUDIT.mdKeep row.Lab
Run 42576632198 at 8489c93,
m6=false, all green, no vacuous, no blocked:verdict_benchmark_200m: t27b 16 (master 9aa6005, run 42573573304) -> 15 words; gcc -O2 10. Static word count only, no speed claim.eachin lower.rs, fixed in 8489c93).Budget
Hand-written
.rs, excluding gen:cli/t27b/src/lower.rs+39;scripts/bulk-create-notebooks.sh-47. Added 39 <= deleted 47, under 40 per file and 80 per PR.Not verified
python3 tools/dupe_scan.pyshows only the inheritedbytes_equal9 -> 10.Refs #12871
🤖 Generated with Claude Code