Skip to content

verified: the silicon queue -- automatic list, runs only on the owner's word, no orphaning reseal (Closes #8120) - #8121

Merged
gHashTag merged 1 commit into
masterfrom
claude/silicon-queue
Oct 9, 2026
Merged

gHashTag merged 1 commit into
masterfrom
claude/silicon-queue

Conversation

@gHashTag

@gHashTag gHashTag commented Oct 9, 2026

Copy link
Copy Markdown
Owner

Closes #8120
Refs #8095

Step 5 of #8095, spec first. specs/verified/silicon_queue.t27 defines three functions.

  • queue_state(): a spec that needs silicon is in one of four states.
    • NONE: its silicon verdict stands.
    • WAIT_SOFTWARE: its own tests do not pass.
    • QUEUE: its software is ready and its hardware step is UNPROVEN.
    • BENCH_BLOCKED: the adapter or the cable failed. This is reported apart from the others.
  • bench_may_run(): a run starts only on the owner's word and never writes flash, eFUSE or BBRAM. The queue itself is computed automatically. Owner decision 2026-10-09 (translated): "do what is best for us".
  • reseal_allowed(): a spec with silicon receipts must keep the producer those receipts name, or be resealed with --force.

Why the reseal guard: on 2026-10-09, re-minting ternary_link's seal made t27c run-record read R3-3 as RUN_PRODUCER_MISMATCH. That was caught before it merged (#8117).

Tests: 5/5 pass, 0 vacuous, 1 invariant proved. Three hand mutants each fail a test. The gen-rust output compiles.

Next: wire queue_state into t27c frontier --silicon-queue and reseal_allowed into t27c seal --save, after #8110 merges, within the foreign-line budget.

🤖 Generated with Claude Code

…'s word, no orphaning reseal (Closes #8120)

Step 5 of #8095. specs/verified/silicon_queue.t27:
- queue_state(): a spec that needs silicon is NONE (its verdict stands),
  WAIT_SOFTWARE (its own tests do not pass: not worth an hour on a board),
  QUEUE (software ready, hardware UNPROVEN) or BENCH_BLOCKED (the adapter or
  cable failed, reported apart so nobody re-queues a dead bench);
- bench_may_run(): a run starts only on the owner's word and never writes
  flash, eFUSE or BBRAM. Owner decision 2026-10-09: "do what is best for us" --
  the queue is computed automatically, a run on the boards is not;
- reseal_allowed(): a spec with silicon receipts keeps the producer they name,
  or is resealed with --force. Measured the same day: re-minting ternary_link's
  seal made t27c run-record read R3-3 as RUN_PRODUCER_MISMATCH.

t27c test-report: 5/5, 0 vacuous, 1 invariant proved. Three hand mutants (drop
the flash guard, the verified check, the producer check) each fail a test.
gen-rust output compiles. Sealed.

Closes #8120

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@gHashTag
gHashTag enabled auto-merge (squash) October 9, 2026 09:49
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-09 10:33:53 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 41
PRs with All Checks Green 9
READY 0
FAILING 41
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 41 + 0 + 0 = 41, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=3c0ade9e73e4 != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

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.

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

2 participants