Go prototype: Pickup run (ADR-0017 reservation) and in-test BFS state-space model checker #1834

This was generated by AI during triage.

Parent

#1830

What to build

Implement thirdshift pickup in the Go prototype—selecting the lowest-numbered Ready issue, reserving it on origin using the ADR-0017 reservation and Claim protocol, and dispatching a Ticket run—and implement an in-test bounded breadth-first state-space model checker in go test that verifies the ADR-0017 safety properties (one dispatch per Ready generation and one claimed dispatch per Ready generation) and demonstrates counterexample traces on the simplified protocol variants.

Acceptance criteria

• thirdshift pickup lists candidate open issues, verifies Ready issue trust and label-history rules, reserves the lowest-numbered Ready issue via origin ref creation (ADR-0017), re-verifies the issue and history after reservation, applies the Claim, and dispatches a Ticket run.
• When a competing host already holds the reservation or the issue is no longer Ready on re-read, Pickup skips or moves on without double-dispatching.
• A bounded BFS state-space model checker in go test exhaustively explores multi-host interleavings, Day shift label changes, and crashes for the ADR-0017 protocol, verifying one dispatch per Ready generation and one claimed dispatch per Ready generation.
• The model checker also runs against the unguarded protocol variants (WithoutClaimCount and UnconditionalCreate) and asserts that it finds minimal counterexample traces for each, matching the Rust stateright suite's coverage.
• End-to-end CLI tests with fake gh and a temporary origin repository cover Ready issue selection, reservation contention, and Ticket run dispatch.

Blocked by

• Go prototype: isolated static binary, embedded skills, and Ticket run through Harness session #1832