Add Go Pickup and bounded reservation model checking

prototype/go/PICKUP-MODEL.md

@@ -0,0 +1,100 @@
+# Bounded Pickup model
+
+`pickup_model_test.go` is an independent, deterministic BFS model of the Go
+prototype's ADR-0017 protocol. It stores comparable states in a visited set and
+FIFO queue, retaining predecessor/action links. The first counterexample is
+minimal in action count; mutation tests pin its length and replay the witness.
+This is bounded exploration, not a proof for arbitrary host counts or GitHub
+consistency. No external model checker or Go dependency is required.
+
+## Bounds and assumptions
+
+- Three hosts, one initially open Ready issue, one attempt per host, at most
+  three Claim applications. Each selection records the Claim count as its Ready
+  generation. Later hosts may select after a failed winner or Day shift hand-back.
+- Git ref creates and owner-leased deletes are atomic. Tokens are unique per
+  attempt; an existing reservation is never adopted or expired. The Day shift
+  observes the token and confirms the owner crashed before deleting it.
+- Issue labels and complete, ordered history are linearizable snapshots. History
+  pagination/snapshot consistency, network failures, permissions and trust are
+  outside the model. CLI tests cover pagination, trust and remote errors. All
+  other Ready gates are fixed favorable, for a Ticket (Spec runs are unsupported).
+- A successful label edit atomically adds Claim/removes Ready. Applying Claim
+  when already present adds no event. Distinct reads, writes, local dispatch,
+  completion and crashes remain separate actions. Constant reads such as label
+  creation, branch/PR absence, and setup details are projected out.
+- Each host may crash at every live phase and never resumes that attempt. Its
+  reservation remains until confirmed-dead recovery. A failure before dispatch
+  still executes Claim ending; a lost response after a write has the state of
+  a crash or failed request after that write. A dispatched session may leave
+  origin work and keep its Claim, leave no work and restore entry labels, or
+  close its issue. Issue closure and ending's label read/write are separate
+  actions. Day shift hand-back can reopen a closed issue.
+- Day shift can withdraw Ready. Hand-back removes Claim/adds Ready only after
+  dispatched work ended. Day shift does not delete a live reservation.
+
+## Requests and control flow
+
+| Model action | Go request or control |
+| --- | --- |
+| `ListReady` | `pickupRun`: paginated open Ready listing; nonessential data projected out |
+| `SelectHistory` | `readReady`: complete events history, reject active Claim, capture generation |
+| `CreateReservation` | `reserve`: push unique parentless commit with empty create lease |
+| `RefreshIssue` | `pickupReserved` → `readReady`: current issue/labels, retained as Claim entry |
+| `RefreshHistory` | `readReady`: history check; `pickupReserved`: selected-generation comparison |
+| `PutClaimLabels` | `runTicket` → `makeClaim` → `changeLabels`: re-read labels, then one REST whole-label PUT, Ready off / Claim on. A gate label applied after the refresh snapshot skips the PUT and the dispatch |
+| `PrepareWorktree` | `runTicket`: local preparation after successful Claim |
+| `Dispatch` | `runTicket` → `harnessSession`: start the opening Harness session |
+| `FailBeforeDispatch` | Claim request/setup/session-start failure; no dispatched session |
+| `RunEndsWithoutOriginWork` | session ends, origin branch and PR absent |
+| `ReadEndingLabels` | `endClaim` → `readIssue`; branch/PR reads fixed absent |
+| `RestoreEntryLabels` | `endClaim`: undo this attempt's Claim/Ready changes, or remove Claim if the ending read found the issue closed |
+| `KeepClaimWithOriginWork` | `endClaim`: origin work exists, keep Claim |
+| `IssueClosed` | session closes issue; subsequent ending reads state and removes Claim without restoring Ready |
+| `ReleaseReservation` | `reservation.release`: token-leased delete on a completion context |
+| `Crash` | process death; no deferred completion |
+| `DayReadsReservation` | operator observes the owner token |
+| `DayDeletesCrashedReservation` | owner-token lease after confirmed death |
+| `DayWithdrawsReady`, `DayHandsBack` | Day shift label changes |
+
+The Go slice applies Claim **before Harness dispatch**, as requested by #1834.
+`TestPickupClaimRequestsMatchModelAtomicTransitions` keeps acquisition and ending
+on single whole-label PUTs: `gh issue edit` splits add/remove into concurrent
+mutations and does not implement the modeled swap.
+The Rust model's documented pre-Claim dispatch counterexample concerns its
+earlier dispatch marker. It is not silently removed from the Rust model and a
+green Go suite does not establish the Rust literal property. Here, both
+`one dispatch per Ready generation` and `one claimed dispatch per Ready generation`
+hold at the documented Go dispatch marker. Both predicates remain explicit.
+Reachability assertions cover three competing selections, failed-winner Ready
+restoration, pre-dispatch failures, issue closure, crash recovery and hand-back.
+
+## Counterexamples and sensitivity
+
+`WithoutClaimCount` removes only the generation comparison after reservation.
+Host B selects generation 0; host A claims, dispatches and ends. After Ready is
+restored, B reserves and dispatches its stale generation-0 selection. The
+shortest witness has 19 actions.
+
+`UnconditionalCreate` replaces the empty create lease with an unconditional
+overwrite. Both hosts reserve and refresh before either Claim. Their idempotent
+Claim edits then permit both sessions to dispatch generation 0. The shortest
+witness has 16 actions. Owner-token release remains guarded in both mutations.
+
+Run safety and positive counterexample regressions:
+
+```sh
+go test -run '^TestPickupModel' -count=1 -v
+```
+
+These optional negative assertions intentionally exit nonzero with the trace:
+
+```sh
+PICKUP_MODEL_VARIANT=WithoutClaimCount go test -run '^TestPickupModelMutations/WithoutClaimCount$' -count=1 -v
+PICKUP_MODEL_VARIANT=UnconditionalCreate go test -run '^TestPickupModelMutations/UnconditionalCreate$' -count=1 -v
+```
+
+When changing `pickup.go`, `ready.go`, `reservation.go`, `claim.go` or the
+dispatch ordering in `run.go`, compare the requests and interleavings here
+with the code before relying on the checker. Preserve counterexamples rather
+than weakening either property to obtain a passing suite.

prototype/go/README.md

@@ -1,8 +1,9 @@
 # Go Ticket-run prototype
 
-An isolated, Linux-only experiment for #1830 / #1832. The production Rust
+An isolated, Linux-only experiment for #1830 / #1832 / #1834. The production Rust
 binary and ADR 0001 stay as they are. This slice stops after the opening
-Harness session, before Delivery, CI watch, Repair or Pickup.
+Harness session, before Delivery, CI watch or Repair. Pickup can select and
+reserve a Ready issue and start that same Ticket run.
 
 Requires Go (the version in `go.mod`), Python 3 for tests/generation, Git,
 authenticated `gh`, and Claude Code (`claude`) for real sessions. Tests use
@@ -21,6 +22,7 @@ Run it from the Launch directory of a disposable repository:
 
 ```sh
 /tmp/thirdshift-go https://github.com/owner/repo/issues/7
+/tmp/thirdshift-go pickup
 ```
 
 It checks Origin match, an open issue, and the issue author's Trusted account
@@ -29,8 +31,14 @@ Launch directory must have a checked-out Base branch. This first slice creates
 `issue-7` and a sibling Worktree `<launch-name>-issue-7`; an existing branch
 or directory fails safely rather than resuming or overwriting it.
 
-The Claim replaces `ready-for-agent` and clears `agent-failed`, preserving
-other labels. The session gets `.thirdshift-issue.md` with the title, body,
+The Claim re-reads labels immediately before one whole-label REST PUT.
+If that read shows the issue is no longer open, Ready was removed, or an
+unready label was applied after the readiness snapshot, Pickup skips the
+issue and a direct Ticket run stops, without writing labels. Otherwise the
+PUT replaces `ready-for-agent`, clears `agent-failed`, and preserves every
+other label from the re-read. Ending uses the same single PUT and re-reads
+before it, so a label applied while branch and PR state is checked is kept.
+The session gets `.thirdshift-issue.md` with the title, body,
 and paginated comments, replacing each untrusted comment with a notice.
 Factory skills are linked under `.claude/skills/thirdshift-*`. Both those
 links and the issue file are excluded through the shared Git `info/exclude`.
@@ -51,6 +59,42 @@ restored (`ready-for-agent` only if it was present before acquisition, and
 `in-progress` removed only if this run added it). Work left on origin keeps
 its Claim, with `agent-failed` on failed or interrupted runs.
 
+## Pickup
+
+`pickup` lists every page of open `ready-for-agent` issues and tries the lowest
+number first. It checks the author, the latest Ready label's actor and subsequent
+title/body edits against the Trusted account rule. Complete label history rejects
+an active Claim and requires a Ready hand-back after a previous Claim ended,
+including either ordering of a same-second hand-back. It passes over triage
+labels, Base/Security fixes, sub-issues, open blockers, and issues shaped within
+30 minutes. Existing origin Issue branches or PRs in any state require a hand-back.
+
+Only Ticket runs are supported: issues with sub-issues (Specs) are passed over.
+This experiment has no production Pass limits, Sweep, CI checks or notifications,
+and inherits the first slice's refusal to resume an existing local branch or
+Worktree. It uses the checked-out Base branch and takes no Pickup options.
+
+For each candidate, ADR-0017 creates `refs/heads/thirdshift/pickup/<number>` on
+origin with an empty create lease and a unique, parentless, empty-tree commit.
+Its message records the token, host, Launch directory, PID and start time.
+Pickup then rechecks the issue, trust, complete history and Claim-application
+count. A busy reservation or stale selection moves on to the next candidate;
+no available candidate exits successfully without starting a session.
+
+A successful Claim precedes Harness dispatch. The reservation lasts through
+Claim ending, even on interruption, and release requires the owner's exact
+commit as its lease. Remote errors fail closed; uncertain create or failed
+release names the ref and token for manual recovery. Crashes retain reservations
+until the Day shift confirms the owner stopped; reservations never expire.
+
+The independent in-test BFS model checks both dispatch properties with three
+hosts and requires shortest counterexamples for `WithoutClaimCount` and
+`UnconditionalCreate`. See [the request mapping and limits](PICKUP-MODEL.md).
+
+```sh
+go test -run '^TestPickupModel' -count=1 -v
+```
+
 ## Embedded Factory skills
 
 Go cannot embed files outside its module. `factory-skills.json` is a generated

prototype/go/claim.go

@@ -2,21 +2,82 @@ package main
 
 import (
 	"context"
+	"encoding/json"
+	"errors"
 	"fmt"
+	"slices"
 )
 
+// errStaleClaim means the issue read that authorized this Claim is no longer
+// the issue's labels. Pickup passes over it. A direct Ticket run stops.
+// The whole-label PUT must not erase that newer decision.
+var errStaleClaim = errors.New("ready state changed after the readiness read")
+
+// Labels that stop a Claim when they appear after the readiness snapshot.
+// agent-failed and in-progress are included so a later failure or Claim is
+// not cleared by this attempt's replacement.
+var claimGateLabels = []string{
+	"in-progress", "agent-failed", "needs-triage", "needs-info",
+	"ready-for-human", "wontfix", "base-fix", "security-fix",
+}
+
 func makeClaim(ctx context.Context, issue issueURL, data issueData) error {
 	if _, err := command(ctx, "", "gh", "label", "create", "in-progress", "--repo", issue.repo,
 		"--description", "A Claim: thirdshift has taken this issue", "--force"); err != nil {
 		return err
 	}
-	args := []string{"issue", "edit", issue.number, "--repo", issue.repo, "--add-label", "in-progress"}
-	for _, label := range []string{"ready-for-agent", "agent-failed"} {
-		if data.hasLabel(label) {
-			args = append(args, "--remove-label", label)
+	// The readiness snapshot is from before history, trust and reservation
+	// checks. Replace labels from a new read, and do not claim if that read
+	// shows the Day shift closed the gate.
+	fresh, err := readIssue(ctx, issue)
+	if err != nil {
+		return err
+	}
+	if err := rejectStaleClaim(data, fresh); err != nil {
+		return err
+	}
+	return changeLabels(ctx, issue, fresh, []string{"in-progress"}, []string{"ready-for-agent", "agent-failed"})
+}
+
+func rejectStaleClaim(before, fresh issueData) error {
+	if before.State == "open" && fresh.State != "open" {
+		return fmt.Errorf("%w: issue is no longer open", errStaleClaim)
+	}
+	if len(before.PullRequest) == 0 && len(fresh.PullRequest) != 0 {
+		return fmt.Errorf("%w: issue is now a pull request", errStaleClaim)
+	}
+	if before.hasLabel("ready-for-agent") && !fresh.hasLabel("ready-for-agent") {
+		return fmt.Errorf("%w: ready-for-agent was removed", errStaleClaim)
+	}
+	for _, label := range claimGateLabels {
+		if fresh.hasLabel(label) && !before.hasLabel(label) {
+			return fmt.Errorf("%w: %s was applied", errStaleClaim, label)
 		}
 	}
-	_, err := command(ctx, "", "gh", args...)
+	return nil
+}
+
+// One whole-label PUT matches the model's atomic Ready/Claim transition.
+// gh issue edit starts independent add/remove mutations and cannot do that.
+func changeLabels(ctx context.Context, issue issueURL, current issueData, add, remove []string) error {
+	labels := []string{}
+	for _, label := range current.Labels {
+		if !slices.Contains(remove, label.Name) {
+			labels = append(labels, label.Name)
+		}
+	}
+	for _, label := range add {
+		if !slices.Contains(labels, label) {
+			labels = append(labels, label)
+		}
+	}
+	payload, err := json.Marshal(struct {
+		Labels []string `json:"labels"`
+	}{labels})
+	if err != nil {
+		return err
+	}
+	_, err = commandInput(ctx, "", payload, "gh", "api", "repos/"+issue.repo+"/issues/"+issue.number+"/labels", "--method", "PUT", "--input", "-")
 	return err
 }
 
@@ -30,8 +91,7 @@ func endClaim(ctx context.Context, launch string, issue issueURL, branch string,
 	if !data.hasLabel("in-progress") {
 		return nil
 	}
-	args := []string{"issue", "edit", issue.number, "--repo", issue.repo}
-	unchanged := len(args)
+	var add, remove []string
 	if data.State == "open" {
 		refs, err := command(ctx, launch, "git", "ls-remote", "--heads", "origin", "refs/heads/"+branch)
 		if err != nil {
@@ -50,24 +110,29 @@ func endClaim(ctx context.Context, launch string, issue issueURL, branch string,
 			if _, err := command(ctx, "", "gh", "label", "create", "agent-failed", "--repo", issue.repo, "--description", "Failed Ticket run", "--force"); err != nil {
 				return err
 			}
-			args = append(args, "--add-label", "agent-failed")
+			add = append(add, "agent-failed")
 		} else {
 			if !initial.hasLabel("in-progress") {
-				args = append(args, "--remove-label", "in-progress")
+				remove = append(remove, "in-progress")
 			}
 			if initial.hasLabel("ready-for-agent") {
-				args = append(args, "--add-label", "ready-for-agent")
+				add = append(add, "ready-for-agent")
 			}
 		}
 	} else {
-		args = append(args, "--remove-label", "in-progress")
+		remove = append(remove, "in-progress")
 		if data.hasLabel("agent-failed") {
-			args = append(args, "--remove-label", "agent-failed")
+			remove = append(remove, "agent-failed")
 		}
 	}
-	if len(args) == unchanged {
+	if len(add) == 0 && len(remove) == 0 {
 		return nil
 	}
-	_, err = command(ctx, "", "gh", args...)
-	return err
+	// Branch and PR reads sit between the ending snapshot and this PUT.
+	// Replace from a current read so a label applied in that window is kept.
+	fresh, err := readIssue(ctx, issue)
+	if err != nil {
+		return err
+	}
+	return changeLabels(ctx, issue, fresh, add, remove)
 }

prototype/go/cli_test.go

@@ -152,10 +152,6 @@ func TestTicketRunLinksEmbeddedSkillsAndStreamsSession(t *testing.T) {
 	if err != nil || !strings.Contains(string(data), "Good and Bad Tests") {
 		t.Fatalf("embedded supporting skill file: %v", err)
 	}
-	calls, _ := os.ReadFile(filepath.Join(f.root, "calls.jsonl"))
-	if !strings.Contains(string(calls), `"--add-label", "in-progress"`) || !strings.Contains(string(calls), `"--remove-label", "ready-for-agent"`) {
-		t.Fatalf("missing Claim transition: %s", calls)
-	}
 	f.assertLabels("enhancement", "ready-for-agent")
 }
 
@@ -216,10 +212,13 @@ func waitFor(t *testing.T, description string, check func() bool) {
 	t.Fatalf("timed out waiting for %s", description)
 }
 
-func (f *fixture) start(mode string) (*exec.Cmd, <-chan error) {
+func (f *fixture) start(mode string, args ...string) (*exec.Cmd, <-chan error) {
 	f.t.Helper()
 	f.writeState("open", "OWNER", mode)
-	cmd := exec.Command(binary, "https://github.com/acme/widgets/issues/7")
+	if len(args) == 0 {
+		args = []string{"https://github.com/acme/widgets/issues/7"}
+	}
+	cmd := exec.Command(binary, args...)
 	cmd.Dir, cmd.Env = f.repo, f.env
 	output, err := os.Create(filepath.Join(f.root, "output"))
 	if err != nil {

prototype/go/main.go

@@ -14,10 +14,15 @@ func entry() int {
 	ctx, stop := signal.NotifyContext(context.Background(), os.Interrupt, syscall.SIGTERM)
 	defer stop()
 	if len(os.Args) != 2 {
-		fmt.Fprintln(os.Stderr, "usage: thirdshift <https://github.com/owner/repo/issues/number>")
+		fmt.Fprintln(os.Stderr, "usage: thirdshift <https://github.com/owner/repo/issues/number> | pickup")
 		return 2
 	}
-	err := ticketRun(ctx, os.Args[1])
+	var err error
+	if os.Args[1] == "pickup" {
+		err = pickupRun(ctx)
+	} else {
+		err = ticketRun(ctx, os.Args[1])
+	}
 	if err != nil {
 		fmt.Fprintln(os.Stderr, err)
 	}