verified: the silicon queue -- automatic list, runs only on the owner's word, no reseal that orphans a run (step 5 of #8095) #8120

Problem

Step 5 of #8095: which specs go to the three boards, who may start a run, and a guard against orphaning a silicon run. Measured 2026-10-09: re-minting ternary_link's seal gave it a new producer and t27c run-record read R3-3 as RUN_PRODUCER_MISMATCH.

Spec

specs/verified/silicon_queue.t27: queue_state (NONE / WAIT_SOFTWARE / QUEUE / BENCH_BLOCKED), bench_may_run (only on the owner's word, never flash/eFUSE/BBRAM), reseal_allowed (a spec with receipts keeps its producer unless forced). Owner decision 2026-10-09: "do what is best for us" -- the queue is automatic, a run is not.

Tests

t27c test-report: 5/5, 0 vacuous; three mutants (drop the flash guard, the verified check, the producer check) each fail a test.

Acceptance

The spec is sealed; the next PR wires queue_state into t27c frontier --silicon-queue and reseal_allowed into t27c seal --save (within the foreign budget, after #8110).

User Scenarios

• Given a new specs/verified/silicon_queue.t27 defining queue_state (NONE / WAIT_SOFTWARE / QUEUE / BENCH_BLOCKED), bench_may_run (owner-only, never flash/eFUSE/BBRAM), and reseal_allowed (producer preserved unless forced), When the spec is compiled and tested, Then the queue operates automatically while runs require explicit owner approval and resealing cannot orphan an in-progress silicon run.

Requirements

• FR-001: The spec MUST define queue_state with exactly the four enumerated values.
• FR-002: The spec MUST define bench_may_run such that a run starts only on the owner's word and never triggers on flash, eFUSE, or BBRAM events.
• FR-003: The spec MUST define reseal_allowed so that a spec with receipts retains its original producer unless an explicit force flag is given.
• FR-004: The spec MUST be sealed and pass all mutation tests (dropping the flash guard, the verified check, or the producer check each fails a test).

Success Criteria

• t27c test-report specs/verified/silicon_queue.t27 exits 0 with output "5/5, 0 vacuous"
• Each of the three mutation tests (flash guard removed, verified check removed, producer check removed) fails at least one test case
• t27c seal --save specs/verified/silicon_queue.t27 exits 0 (spec is sealed)

Boundary

• specs/verified/silicon_queue.t27
• specs/tools/tri/reseal.t27
• specs/tri/collections/queue.t27
• specs/tri/collections/list.t27
• cli/tri/src/reseal.rs