spec(queen): claim.t27 - the round's stateOfDispatch as a card, the review valve imported (Closes #8765)

[dmitrii-f-t27]

Closes #8765. Runtime half: gHashTag/trios#1767.

Description

specs/queen/claim.t27 (module QueenClaim) is the card for the rule the trios supervisor applies to every queen_dispatch row every round: does the row still claim its issue? The answer is one of running, accepted, rejected, awaitingReview, failed, cancelled. Today that rule is stateOfDispatch in trios/agent-server/apps/server/src/api/services/queen-tick.ts (gHashTag/trios queen @ 3654fdd2, lines 791-912), and it is written by hand.

Two specs describe older versions of the rule, and neither matches the code on queen. dispatch.t27 claim_of is the audit at pin 879799a8: an escalation is held with no clock, cancelled does not exist, and criteria are not read. trios rings/T27-02/tick_core.t27 has four states. dispatch.t27 is not edited here because #6934, #5452 and #7430 touch it.

fn	rule
claim_of(finished, verdict, idle_minutes, send_backs, ceiling, releases, criteria_read, criteria, free_attempts, reviewer_misses)	the rule as it runs on queen. A running bee claims. accept is done. failed, cancelled and stale-contract free the issue, and obsolete cancels it. empty waits for the retry floor. A send-back under the ceiling waits for its hour, then goes to the valve as KIND_SEND_BACK_CEILING. An escalation goes to the valve with the kind from its counters. A wait or no verdict under the ceiling is released after 6 h. Any other word is held with no clock
escalation_kind_of(...)	the escalation kind from the row's counters, in the valve's order. Unread criteria count as one, never zero
claim_of_step(step, held)	the valve's step as a claim: RELEASE -> failed, CLOSE -> cancelled, HOLD and BACKFILL keep the claim
criteria_read_as(read, n)	an unread criteria count is UNREAD_CRITERIA = 1

escalation_kind, next_step, the kind and step codes, RETRY_FLOOR_MINUTES and OBSOLETE_STATE are imported from review_valve.t27 with use, so nothing of the valve is restated. The seal's closure names review_valve.t27. The verdict word stays at the boundary: the supervisor maps review_state to a V_ code and maps the CL_ result back to its word.

Clocks are whole minutes since finished_at. Every floor is a whole number of minutes, so the supervisor's idle_ms >= floor_ms holds exactly when floor(idle_ms / 60000) >= floor_minutes. An unreadable or negative clock is 0, so it keeps the hold, as today.

Testing

All runs used ./target/release/t27c and ./target/release/tri built from this branch's tree (t27c 0.5.2 at c31c059), with Zig 0.16.0.

• t27c check specs/queen/claim.t27: OK, 0 errors. The one warning is about the 10 parameters of claim_of, which are the 10 inputs stateOfDispatch reads.
• t27c gen-c | gen-rust | gen | gen-verilog | gen-ts: all exit 0. The generated Rust compiles with bare rustc --crate-type lib.
• t27c test-report specs/queen/claim.t27: 11 tests, 11 pass, 0 FAIL, 0 vacuous, 2 invariants proved.
• t27c seal specs/queen/claim.t27 --save, then --verify: all hashes MATCH. Seal tests 11/11, zig 0.16.0.
• t27c check-now: OK.
• tri mutate spec --file specs/queen/claim.t27 --jobs 6 --timeout 60: 40 mutants (drop-guard 11, flip-cmp 21, swap-logic 4, ret-default 4). All 40 are killed by a failing test.
  • The first run left 4 survivors, and both causes are now closed.
  • Two came from the send-back's own floor (the guard dropped, and >= changed to >). With releases = 0 the valve gives the same answer at the hour, which hid the guard. They were a test gap, closed by asserting releases = 1, where the two answers differ.
  • Two came from the dead-letter and reviewer-miss ceilings (>= changed to >). They cannot change the claim, because the valve gives those kinds the step of an unrecorded kind. They are closed by escalation_kind_of and its own test at each ceiling.
• WASM, as the runtime will build it: t27c gen-c and then zig 0.16.0 cc --target=wasm32-wasi -Oz -DNDEBUG -mexec-model=reactor with one --export for each function of the card and each function it imports. Two builds give one hash. The module has 0 imports.

CI

The required checks (validate, check-linked-issue, parse-ratchet) are green. I compared each red check with master:

• Corpus ratchet: the same 5 unexpected failures as master at ddb84c5 (specs/a/b_c.t27, specs/a_b/c.t27, specs/compiler/optimizer.t27, specs/memory/graph/ingest.t27, orchestrator_bench.t27). claim.t27 is not among them.
• duplicate-bodies: the same three findings as master (bits, same, clear).
• emit-bitexact: specs/memory/graph/ingest.t27 does not generate. That spec is not touched here.
• Verilog widths: specs/tri/t27b/conformance/big_frame.t27. It is red on master since cd569e3.
• t27b-native-ratchet: one finding was mine. claim.t27 was UNLISTED: the reference and t27b both pass it, but the ledger did not name it. 25d2335 lists it in docs/reports/t27b_expectations.json. A replay of this run's run.json with the updated ledger no longer reports it. The other UNLISTED entries are master's.

Recorded, not changed

When a spent ceiling is handed back, the redispatch resets send_backs and keeps ceiling_releases = 1 (queen-dispatch.ts upsert). The first send-back of the new attempt therefore reaches the valve with a spent release, and the valve closes it as obsolete inside its hour. That contradicts the supervisor's own comment ("then one more set"). The card keeps the answer the supervisor gives today, and the test a_send_back_under_its_ceiling_goes_back_after_the_hour pins it. A change belongs to the valve and is filed separately on the trios side.

Not in this PR

• The runtime switch and its equality proof: The round's claim (stateOfDispatch) is decided by the claim card, proven equal to the hand-written rule first trios#1767.
• dispatch.t27 is unchanged.

Dmitrii Fedorov (@dmitrii-f-t27)

[dmitrii-f-t27]

Updated 2026-10-11 15:18 UTC. Head 4b6ee3b82 (a merge of master 5e5493c into this branch; no rebase, no force-push). The earlier table for d4cedbc is replaced by this one.

Required checks on 4b6ee3b82: validate, check-linked-issue, parse-ratchet, own-language are green. duplicate-bodies, Verilog widths and emit-bitexact are green now too.

Checked locally on the merged tree with t27c built from it (cargo build --release -p t27c, Zig 0.16):

• t27c seal specs/queen/claim.t27 --verify: all hashes MATCH (spec, zig, verilog, c, rust); the seal records tests 11/11 passed, 0 vacuous. review_valve.t27 and dispatch.t27 seals MATCH too.
• t27c test-report specs/queen/claim.t27: 11 pass, 0 fail, 0 vacuous.
• tools/dupe_scan.py, tools/check_verilog_widths.py --require, tools/check_specs_parse.py, tools/check_specs_generate.py: OK.

The four red checks are red on master with the same findings. This PR changes 4 files (specs/queen/claim.t27, its seal, one ledger line, one docs/now note) and none of them is in a finding.

Check	This PR (4b6ee3b82)	master	Only in this PR
Corpus ratchet	tri types ratchet: ledger 86, observed 89, NEW Entry, Inputs, SkillMeta (run)	identical at 5e5493c (run)	none
coverage	1 seal newly does not hold: queen_QueenHolds.json gen-drift (run)	identical at 5e5493c (run)	none
spec-guards	check_seal_currency: STALE queen_QueenHolds.json gen_hash_rust (run)	identical at 5e5493c (run)	none
cli-tri	census moved: quiet 185 → 188, run: steps 305 → 306 (run)	red on master a314273 (run); the same 185 → 188 / 305 → 306 on unrelated PR branch chat-cr00-lib (run)	none: this PR does not touch .github/
t27b-native-ratchet	17 UNLISTED (run)	the same 17 at 5e5493c (run), sets compared line by line	none: specs/queen/claim.t27 is in the ledger

Action needed outside this PR, on master: reseal specs/queen/holds.t27, bless or fix the three type-name conflicts, ledger the 17 unlisted specs and the CLI census. Changing those ledgers here would mix unrelated entries into this PR.

Dmitrii Fedorov (@dmitrii-f-t27)