Skip to content

Add Go Pickup and bounded reservation model checking - #1850

Merged
JacobStephens2 merged 3 commits into
issue-1830from
issue-1834
Nov 6, 2026
Merged

JacobStephens2 merged 3 commits into
issue-1830from
issue-1834

Conversation

@JacobStephens2

@JacobStephens2 JacobStephens2 commented Nov 6, 2026 •

Copy link
Copy Markdown
Owner

Summary

Add Pickup to the isolated Go prototype, selecting the lowest-numbered Ready Ticket and holding an ADR-0017 reservation through its Ticket run and Claim ending.

pickup
  list Ready candidates by issue number
  reserve origin ref with empty create lease
  recheck trust, readiness and Claim generation
  Claim through one whole-label PUT
  dispatch Ticket run → opening Harness session
  end Claim → release reservation with owner's token lease

The in-test BFS checks both safety properties across three hosts, Day shift changes and crashes: 1,993,250 guarded states; shortest negative traces of 19 actions (WithoutClaimCount) and 16 (UnconditionalCreate). Bounds and request mapping are in prototype/go/PICKUP-MODEL.md.

This Ticket keeps the prototype's existing scope: Ticket runs only, checked-out Base branch, and refusal to resume an existing local branch/Worktree. Specs are passed over. Delivery and production Pass limits remain separate work.

Closes #1834

Evidence

Execution evidence

  • Before: PATH=/usr/local/go/bin:$PATH go test -C prototype/go -run '^TestPickupSelectsLowestReadyAcrossPages$' -count=1 -v failed: Pickup run: exit status 1: invalid Issue URL: pickup.
    After: the same command passed: --- PASS: TestPickupSelectsLowestReadyAcrossPages.
  • Review regression before: python3 /tmp/issue-1834-run-atomic-label-regression.py ran the supplied Go regression against a temporary copy and failed: want one label PUT for Claim acquisition and one for ending, got 0, identifying both split gh issue edit calls.
    After: the same command passed: --- PASS: TestPickupClaimRequestsMatchModelAtomicTransitions. The complete test is retained in prototype/go/spec_atomic_label_regression_test.go; reproduce from the Go module with go test -count=1 -run '^TestPickupClaimRequestsMatchModelAtomicTransitions$' -v ./....
  • Real gh against a local TLS mock also confirmed separate LabelAdd and LabelRemove requests; no GitHub writes were involved. The fix uses a whole-label REST PUT for both transitions, matching the model. GitHub CLI source.
  • Final-source PATH=/usr/local/go/bin:$PATH go test -C prototype/go ./... passed in 46.579s; go vet passed. CLI coverage includes paginated selection/trust/history, competing same-identity clones, stale refresh, permission failure, interrupted release and replacement-token preservation.
  • PATH=/usr/local/go/bin:$PATH scripts/affected-tests issue-1830: Go passed (67.09s). The older local review ref conservatively selected Rust too: 1,657 unit tests and the completed integration suites passed before that redundant portion was interrupted. The fetched PR base (origin/issue-1830, 1bbcc4fc) already contains Go prototype: isolated static binary, embedded skills, and Ticket run through Harness session #1832, and all 15 files in the actual PR diff are under prototype/go/. Final-source Go tests/vet and exact-head Go CI passed; no local validation task remains running.
  • Exact-head CI: Go prototype, site and Console jobs passed. The broader Rust job remains in progress at hand-off.
  • python3 -m unittest discover -s scripts -p 'test_*.py': 37 tests passed. python3 prototype/go/bundle-skills.py --check: passed.
  • Both optional PICKUP_MODEL_VARIANT negative assertions exited 1 with their expected minimal counterexamples; the ordinary model safety and sensitivity tests pass.

Seams under test

  • Compiled Go CLI with fake GitHub/Harness executables and real temporary origin repositories: selection, trust/history gates, contention, Claim, dispatch and reservation completion.
  • In-test BFS checker: exhaustive bounded protocol exploration, safety predicates, reachability and minimal mutation counterexamples.

Review coverage

Independent Standards and Spec reviews used fixed point issue-1830 (305923a8e93a286b6fa546ddfc02fa30abc23f64), then reviewed all fix hunks through fef1253c. Each axis read all 24 hand-written changed files. prototype/go/factory-skills.json was intentionally unread: both confirmed its exclusion after reviewing root skill sources, bundle-skills.py, skills.go, the passing snapshot check, and the passing linked-skill/Worktree/streaming behavior test. No other changed file remains unread.

Standards raised 1 finding (duplicate Launch/origin discovery), fixed with launchOrigin. Spec raised 1 finding (atomic model versus split label requests), reproduced and fixed with the retained regression. Counts include fixed findings.

Unaddressed findings

Standards

None.

Spec

None.

Security

None.

Security review outcome

No unaddressed introduced findings.

Merge Danger

Door: two-way

The isolated prototype can be reverted. Real Pickup use creates temporary origin reservation refs; a crashed owner requires confirmed-dead manual recovery, as documented in ADR-0017.

Blast Radius: prototype

No production Rust behavior changes. Go tests use temporary repositories and fake external executables.

Built with codex codex-cli 0.164.0 · gpt-6.1-sol · xhigh

Pickup built its whole-label PUT from the issue snapshot taken before history and trust checks. A gate label applied in that window was left out of the replacement, so the PUT deleted it and the Harness still started. Re-read at the PUT, skip the claim when that read shows the gate closed, and keep every other label from the new read.
@JacobStephens2
JacobStephens2 merged commit fb48663 into issue-1830 Nov 6, 2026
5 checks passed
@JacobStephens2
JacobStephens2 deleted the issue-1834 branch November 6, 2026 22:42
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.

1 participant