Spec: Go vertical-slice prototype and comparison against the Rust binary

.github/workflows/go-prototype.yml

@@ -0,0 +1,31 @@
+name: Go prototype
+
+on:
+  pull_request:
+    paths: ['prototype/go/**', '.github/workflows/go-prototype.yml']
+  push:
+    branches: [main]
+    paths: ['prototype/go/**', '.github/workflows/go-prototype.yml']
+
+concurrency:
+  group: go-prototype-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  go-prototype:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 10
+    defaults:
+      run:
+        working-directory: prototype/go
+    steps:
+      - uses: actions/checkout@v7
+      - uses: actions/setup-go@v6
+        with:
+          go-version-file: prototype/go/go.mod
+          cache: false
+      - run: python3 bundle-skills.py --check
+      - run: test -z "$(gofmt -l *.go)"
+      - run: go vet ./...
+      - run: go test ./...
+      - run: CGO_ENABLED=0 go build -o "$RUNNER_TEMP/thirdshift-go" .

docs/research/go-vs-rust-benchmark-2026-11-06/1-go-model_check.log

@@ -0,0 +1,13 @@
+$ /tmp/thirdshift-benchmark-sl4wkj08/go-tests '-test.run=^TestPickupModel' -test.count=1 -test.v
+=== RUN   TestPickupModelSafety
+    pickup_model_test.go:267: ADR-0017: 1993250 unique states
+--- PASS: TestPickupModelSafety (4.15s)
+=== RUN   TestPickupModelMutations
+=== RUN   TestPickupModelMutations/WithoutClaimCount
+    pickup_model_test.go:285: WithoutClaimCount: 119601 states; shortest dispatch trace (19): [ListReady(0) SelectHistory(0) CreateReservation(0) RefreshIssue(0) RefreshHistory(0) ListReady(1) SelectHistory(1) PutClaimLabels(0) PrepareWorktree(0) Dispatch(0) KeepClaimWithOriginWork(0) ReleaseReservation(0) CreateReservation(1) DayHandsBack RefreshIssue(1) RefreshHistory(1) PutClaimLabels(1) PrepareWorktree(1) Dispatch(1)]; shortest claimed trace (19): [ListReady(0) SelectHistory(0) CreateReservation(0) RefreshIssue(0) RefreshHistory(0) ListReady(1) SelectHistory(1) PutClaimLabels(0) PrepareWorktree(0) Dispatch(0) KeepClaimWithOriginWork(0) ReleaseReservation(0) CreateReservation(1) DayHandsBack RefreshIssue(1) RefreshHistory(1) PutClaimLabels(1) PrepareWorktree(1) Dispatch(1)]
+=== RUN   TestPickupModelMutations/UnconditionalCreate
+    pickup_model_test.go:285: UnconditionalCreate: 223036 states; shortest dispatch trace (16): [ListReady(0) SelectHistory(0) CreateReservation(0) RefreshIssue(0) RefreshHistory(0) ListReady(1) SelectHistory(1) CreateReservation(1) RefreshIssue(1) RefreshHistory(1) PutClaimLabels(0) PrepareWorktree(0) Dispatch(0) PutClaimLabels(1) PrepareWorktree(1) Dispatch(1)]; shortest claimed trace (16): [ListReady(0) SelectHistory(0) CreateReservation(0) RefreshIssue(0) RefreshHistory(0) ListReady(1) SelectHistory(1) CreateReservation(1) RefreshIssue(1) RefreshHistory(1) PutClaimLabels(0) PrepareWorktree(0) Dispatch(0) PutClaimLabels(1) PrepareWorktree(1) Dispatch(1)]
+--- PASS: TestPickupModelMutations (0.76s)
+    --- PASS: TestPickupModelMutations/WithoutClaimCount (0.26s)
+    --- PASS: TestPickupModelMutations/UnconditionalCreate (0.50s)
+PASS

docs/research/go-vs-rust-benchmark-2026-11-06/1-rust-model_check.log

@@ -0,0 +1,69 @@
+$ /tmp/thirdshift-benchmark-sl4wkj08/rust-target/debug/deps/pickup_model-1d72f02ce05acf2e --test-threads=1 --nocapture
+
+running 5 tests
+test assert_requested_property ... ignored, known pre-Claim dispatch finding; run explicitly to see the failure
+test current_protocol_reports_pre_claim_dispatch_counterexample ... Current, Dispatch: 7093 unique states
+KNOWN FINDING: the literal dispatch property fails: Path[14]:
+- ListReady(0)
+- SelectHistory(0)
+- CreateReservation(0)
+- RefreshIssue(0)
+- RefreshHistory(0)
+- Dispatch(0)
+- FailBeforeClaim(0)
+- ReleaseReservation(0)
+- ListReady(1)
+- SelectHistory(1)
+- CreateReservation(1)
+- RefreshIssue(1)
+- RefreshHistory(1)
+- Dispatch(1)
+
+ok
+test pickup_claimed_dispatch_safety ... Current, ClaimedDispatch: 86745 unique states
+ok
+test removing_claim_count_recheck_is_detected ... WithoutClaimCount, ClaimedDispatch: 20675 unique states
+Claim-count mutation counterexample: Path[19]:
+- ListReady(0)
+- SelectHistory(0)
+- CreateReservation(0)
+- RefreshIssue(0)
+- RefreshHistory(0)
+- Dispatch(0)
+- ReadClaimLabels(0)
+- ListReady(1)
+- SelectHistory(1)
+- PutClaimLabels(0)
+- KeepClaim(0)
+- ReleaseReservation(0)
+- CreateReservation(1)
+- DayHandsBack
+- RefreshIssue(1)
+- RefreshHistory(1)
+- Dispatch(1)
+- ReadClaimLabels(1)
+- PutClaimLabels(1)
+
+ok
+test removing_empty_create_lease_is_detected ... UnconditionalCreate, ClaimedDispatch: 22520 unique states
+Empty-lease mutation counterexample: Path[15]:
+- ListReady(0)
+- SelectHistory(0)
+- CreateReservation(0)
+- RefreshIssue(0)
+- RefreshHistory(0)
+- Dispatch(0)
+- ReadClaimLabels(0)
+- ListReady(1)
+- SelectHistory(1)
+- CreateReservation(1)
+- RefreshIssue(1)
+- RefreshHistory(1)
+- PutClaimLabels(0)
+- Dispatch(1)
+- ReadClaimLabels(1)
+
+ok
+
+test result: ok. 4 passed; 0 failed; 1 ignored; 0 measured; 0 filtered out; finished in 1.12s
+

docs/research/go-vs-rust-benchmark-2026-11-06/2-go-model_check.log

@@ -0,0 +1,13 @@
+$ /tmp/thirdshift-benchmark-f7shrf8g/go-tests '-test.run=^TestPickupModel' -test.count=1 -test.v
+=== RUN   TestPickupModelSafety
+    pickup_model_test.go:267: ADR-0017: 1993250 unique states
+--- PASS: TestPickupModelSafety (4.15s)
+=== RUN   TestPickupModelMutations
+=== RUN   TestPickupModelMutations/WithoutClaimCount
+    pickup_model_test.go:285: WithoutClaimCount: 119601 states; shortest dispatch trace (19): [ListReady(0) SelectHistory(0) CreateReservation(0) RefreshIssue(0) RefreshHistory(0) ListReady(1) SelectHistory(1) PutClaimLabels(0) PrepareWorktree(0) Dispatch(0) KeepClaimWithOriginWork(0) ReleaseReservation(0) CreateReservation(1) DayHandsBack RefreshIssue(1) RefreshHistory(1) PutClaimLabels(1) PrepareWorktree(1) Dispatch(1)]; shortest claimed trace (19): [ListReady(0) SelectHistory(0) CreateReservation(0) RefreshIssue(0) RefreshHistory(0) ListReady(1) SelectHistory(1) PutClaimLabels(0) PrepareWorktree(0) Dispatch(0) KeepClaimWithOriginWork(0) ReleaseReservation(0) CreateReservation(1) DayHandsBack RefreshIssue(1) RefreshHistory(1) PutClaimLabels(1) PrepareWorktree(1) Dispatch(1)]
+=== RUN   TestPickupModelMutations/UnconditionalCreate
+    pickup_model_test.go:285: UnconditionalCreate: 223036 states; shortest dispatch trace (16): [ListReady(0) SelectHistory(0) CreateReservation(0) RefreshIssue(0) RefreshHistory(0) ListReady(1) SelectHistory(1) CreateReservation(1) RefreshIssue(1) RefreshHistory(1) PutClaimLabels(0) PrepareWorktree(0) Dispatch(0) PutClaimLabels(1) PrepareWorktree(1) Dispatch(1)]; shortest claimed trace (16): [ListReady(0) SelectHistory(0) CreateReservation(0) RefreshIssue(0) RefreshHistory(0) ListReady(1) SelectHistory(1) CreateReservation(1) RefreshIssue(1) RefreshHistory(1) PutClaimLabels(0) PrepareWorktree(0) Dispatch(0) PutClaimLabels(1) PrepareWorktree(1) Dispatch(1)]
+--- PASS: TestPickupModelMutations (0.65s)
+    --- PASS: TestPickupModelMutations/WithoutClaimCount (0.20s)
+    --- PASS: TestPickupModelMutations/UnconditionalCreate (0.46s)
+PASS

docs/research/go-vs-rust-benchmark-2026-11-06/2-rust-model_check.log

@@ -0,0 +1,69 @@
+$ /tmp/thirdshift-benchmark-f7shrf8g/rust-target/debug/deps/pickup_model-1d72f02ce05acf2e --test-threads=1 --nocapture
+
+running 5 tests
+test assert_requested_property ... ignored, known pre-Claim dispatch finding; run explicitly to see the failure
+test current_protocol_reports_pre_claim_dispatch_counterexample ... Current, Dispatch: 7093 unique states
+KNOWN FINDING: the literal dispatch property fails: Path[14]:
+- ListReady(0)
+- SelectHistory(0)
+- CreateReservation(0)
+- RefreshIssue(0)
+- RefreshHistory(0)
+- Dispatch(0)
+- FailBeforeClaim(0)
+- ReleaseReservation(0)
+- ListReady(1)
+- SelectHistory(1)
+- CreateReservation(1)
+- RefreshIssue(1)
+- RefreshHistory(1)
+- Dispatch(1)
+
+ok
+test pickup_claimed_dispatch_safety ... Current, ClaimedDispatch: 86745 unique states
+ok
+test removing_claim_count_recheck_is_detected ... WithoutClaimCount, ClaimedDispatch: 20675 unique states
+Claim-count mutation counterexample: Path[19]:
+- ListReady(0)
+- SelectHistory(0)
+- CreateReservation(0)
+- RefreshIssue(0)
+- RefreshHistory(0)
+- Dispatch(0)
+- ReadClaimLabels(0)
+- ListReady(1)
+- SelectHistory(1)
+- PutClaimLabels(0)
+- KeepClaim(0)
+- ReleaseReservation(0)
+- CreateReservation(1)
+- DayHandsBack
+- RefreshIssue(1)
+- RefreshHistory(1)
+- Dispatch(1)
+- ReadClaimLabels(1)
+- PutClaimLabels(1)
+
+ok
+test removing_empty_create_lease_is_detected ... UnconditionalCreate, ClaimedDispatch: 22520 unique states
+Empty-lease mutation counterexample: Path[15]:
+- ListReady(0)
+- SelectHistory(0)
+- CreateReservation(0)
+- RefreshIssue(0)
+- RefreshHistory(0)
+- Dispatch(0)
+- ReadClaimLabels(0)
+- ListReady(1)
+- SelectHistory(1)
+- CreateReservation(1)
+- RefreshIssue(1)
+- RefreshHistory(1)
+- PutClaimLabels(0)
+- Dispatch(1)
+- ReadClaimLabels(1)
+
+ok
+
+test result: ok. 4 passed; 0 failed; 1 ignored; 0 measured; 0 filtered out; finished in 1.12s
+