ADR-072: Post-Success Claim Recheck (Prove-Time Race Fix)

Field	Value
Decision ID	ADR-072
Initiative	unsorry Phase 3 — coordination correctness
Proposed By	unsorry maintainers
Date	2026-06-18
Status	Accepted

WH(Y) Decision Statement

In the context of the ADR-004 claims branch, where an agent reserves a goal by pushing claims/<goal>.<agent>.aisp first-push-wins and claim_goal rechecks the per-mode cap (prove 1 / translate 2) only when a push is rejected (the #184/#185 rejection race), facing the duplicate-proof root cause behind the post-ADR-064 dead PRs: because claim files are per-agent, two agents claiming the same goal write different paths, so the second agent’s push is a clean fast-forward — not a rejection — whenever its claims base already contained the first agent’s claim (it fetched after they pushed); the on-rejection recheck never runs, both pushes succeed, and both agents prove the same goal, producing the sibling queued/prove/<goal>/<agent>-* branches that ADR-064/ADR-071 then only clean up downstream, we decided for adding a post-SUCCESS recheck in claim_goal: after a successful push, re-fetch origin/claims and re-apply the same per-mode cap that the rejection path uses; if other agents now meet the cap, withdraw (remove the just-pushed claim via release_claim, emit collision, return failure) so the agent does not prove the goal, and neglected a deterministic tie-break to let exactly one racer proceed (rejected — a recheck that runs before the rival’s claim has landed cannot rank safely, so any “proceed if I look like the winner” rule can let both proceed; the conservative “withdraw if the cap is met by others” never yields two provers, at the cost that a tight tie makes both withdraw and the goal is simply re-selected next cycle), and switching to a per-goal lock file or non-per-agent claim path (rejected — invasive to the claims schema, Gate B, and the reaper; the post-success recheck reuses the existing cap helper, DRY), to achieve at-most-cap provers per goal enforced at claim time — stopping duplicate proofs at the source rather than sweeping their PRs, accepting that each successful claim now costs one extra git fetch + re-check, a tight race can waste a claim round (re-selected next cycle, never a duplicate or a permanent stall — the goal stays in the open pool), and the guarantee is best-effort under infra failure (a failed re-fetch keeps the claim; the TTL reaper and Gate B remain the backstop).

Context

Completes the ADR-064 / ADR-071 line: ADR-064 dedups at dispatch, ADR-071 closes the dispatch stale-snapshot window, and this ADR removes the upstream cause — two agents proving one goal. The fix is confined to claim_goal’s success path and is hermetically self-tested (test_claim_post_success_recheck) against a real git claims remote where the rival’s claim is already in the base so the push is a clean fast-forward.

Options Considered

Option 1: Conservative post-success recheck (Selected)

Pros: never two provers; reuses the existing per-mode cap helper; tiny; symmetric with the on-rejection recheck. Cons: a tight tie wastes a claim round (both withdraw, re-selected next cycle).

Option 2: Post-success recheck with deterministic tie-break (Rejected)

Let the lexicographic/earliest-ts winner proceed. Cons: a recheck that runs before the rival’s claim lands sees only itself and proceeds, so the rival — which may be the tie-break winner — also proceeds → both prove. Not safe without a barrier.

Option 3: Per-goal lock file / non-per-agent claim path (Rejected)

Make the claim push genuinely conflict for the same goal. Cons: breaks the per-agent claim model that translate’s cap-2 needs; invasive to the schema, Gate B, and reaper.

Dependencies

References

| Reference ID | Title | Type | Location | |————–|——-|——|———-| | REF-1 | SPEC-072-A — Post-success claim recheck | Specification | specs/SPEC-072-A-Post-Success-Claim-Recheck.md |

Status History

| Status | Approver | Date | |——–|———-|——| | Proposed | unsorry maintainers | 2026-06-18 | | Accepted | unsorry maintainers | 2026-06-18 |