Repository navigation
spec(queen): review_valve names an effect give-up instead of reading it as UNRECORDED (Closes #7092) - #7115
Merged
Conversation
…it as UNRECORDED (Closes #7092) control.t27 ends an attempt with DO_GIVE_UP after EFFECT_RUN_LIMIT runs of one effect key (#7059). No counter of an escalated row shows that, so the valve read it as KIND_UNRECORDED and the close note could not name the crash loop. - KIND_EFFECT_GAVE_UP = 8. Codes 0..7 do not move. A new invariant pins all nine values; with it removed, 8 -> 9 passes every test. - is_recorded_kind and recorded_escalation_kind. The counters decide first, and a record names only a row they leave UNRECORDED, with a kind that is a record's to name. escalation_kind is unchanged. - Timing: the 30-minute empty-attempt floor, one release, then close. The issue proposed an instant release. Dispatch has already moved the crash loop across runtimes, so an instant retry meets a deploy restart or a quota window again. The issue has a comment. - gen/c/queen/review_valve.c is regenerated. Checks: 7 pub fn, 2 invariants, 11 tests; zig 11/11, 0 vacuous; parse, typecheck, gen-rust, gen-verilog and gen-c exit 0; tri mutate spec on the lab 50/50 killed; 11 hand mutants killed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
gHashTag
enabled auto-merge (squash)
October 6, 2026 21:15
This was referenced Oct 6, 2026
Merged
Contributor
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
1 participant
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.
Closes #7092. Refs #6971.
What
specs/queen/review_valve.t27gainsKIND_EFFECT_GAVE_UP = 8, so a row whose attempt ended in control.t27'sDO_GIVE_UP(an effect key ranEFFECT_RUN_LIMITtimes, #7059 / #7091) is named as such instead of readingKIND_UNRECORDED.recorded_escalation_kind(recorded, ...): the counters decide first, inescalation_kind's order, so a record cannot hide a missing criterion or a spent ceiling. A record only names a row the counters leave UNRECORDED, and only with a kind that is a record's to name (is_recorded_kind).escalation_kindis unchanged: a runtime that records nothing gets the same answer as before.Not here: the runtime side (the supervisor still has to record the reason and mirror the new function).
Checks (printed by commands on this branch, rebased on 79d2d4c)
t27c gen+zig test: 11/11 passed,test-report: 0 vacuous of 11.tools/l2_regen_check.py:gen/c/queen/review_valve.cregenerated byte for byte.tri mutate specon the lab, whole file: 50 of 50 killed; 11 hand mutants of the new lines and constants, all killed.🤖 Generated with Claude Code