/lean4

Handoff Contract (run-contract/v1)

The versioned protocol that binds the parent, worker, and human roles across proving commands (prove, autoprove) and proof-editing agents. It has two records — a dispatch record (parent → worker) and a handoff record (worker → parent/human) — plus a rerun guard that stops a proving mode from relaunching on the same blocker without new evidence.

This contract is documentation, not runtime code: it defines what the roles exchange, not an enforcement engine. "Durable" here means each record is serializable and transferable across a subagent, an inline pass, and a human handoff — the same record shape regardless of who plays a role. Filesystem persistence of these records is the separate storage primitive in run-store.md (run-store/v1, #82A); prove/autoprove --persist write their runs through it (cycle-engine.md § Run Persistence, #82B) and cite stored items only as <run_id>#<seq>; prior-run reuse (#82C) records a local source-note bridging to the prior run's <run_id>#<seq> citations — Replan cites stay same-run — and carries the prior blocker forward (cycle-engine.md § Prior-Run Reuse); resume and inspect remain open under Issue #82.

The contract binds the logical roles, not processes: a host without subagents plays parent and worker inline in the main thread and satisfies the same records (see No-subagent fallback).

It does not invent vocabulary — it names pieces the cycle engine already uses: the blocker signature, the pre-flight dispatch block, the file-baseline/v1 custody chain, the Blocked-Goal Triage classes from sorry-filling.md, and the review stuck-mode next_action enum.

Dispatch record (parent → worker)

The concrete instantiation is the Pre-flight Context block; this table is its canonical field contract. Every field is required unless a nullability is given.

context carries the pre-flight state — every member is required (never omitted). Its two nullable members (prior_failure, goal_state) use null when there is no data, the array members use [], and scratch_location is always a non-null string (there is always a scratch dir):

Ownership rule: never dispatch concurrent workers with overlapping owned_files; serialize or keep one in-thread. The single file_baseline covers the owned set so the worker can check before every mutation and advance only what it changed (custody chain).

Worker parameters

parameters is a typed object keyed by worker ({} for an inline pass):

Handoff record (worker → parent/human)

Emitted at every stop or stuck boundary — compact enough for a human or another agent to consume in one pass.

Malformed dispatch. So that even an unparseable dispatch yields a valid handoff, a protocol-error handoff reporting a malformed dispatch echoes whatever it could parse and sets the rest (target/scope/mode, file_baseline) to null; stop_detail names the defect. same_task is then unevaluable, so the operational rerun branch governs the relaunch (a nonempty evidence_delta resolving stop_detail). In every other handoff these fields are non-null.

Blocker fields (blocker_kind, blocker_signature, new_evidence_required_for_rerun) are non-null iff the stop was blocker-driven — status == stuck, or status == stopped with stop_reason == max-stuck. blocker_class is non-null only when blocker_kind == proof (the seven proof-triage classes); a safety-guard stop (deep regression, deep scope exceeded, header-fence violation, rollback failure) or a false-statement/capability blocker sets blocker_kind accordingly and leaves blocker_class null. All blocker fields are null for status == solved and for every non-blocker stop — budget/user/queue (max-cycles / max-runtime / user-stop / queue-empty) and operational aborts (protocol-error / operational-error), which carry their cause in stop_detail. A queue-empty stop with claims remaining therefore reruns freely — no blocker_signature for the guard to match.

Custody vs effect. files_owned reports custody (echoing the dispatch's owned_files); files_changed reports effect (what the worker wrote). The file_baseline is the single file-baseline/v1 record for the owned set: a direct-editing worker advances it after each mutation and returns the final one, which the parent adopts as-is — re-advancing at handoff would bless drift occurring after the worker's last check. A patch-only worker (e.g. proof-repair) does not edit: it returns files_changed: [], the parent's own file_baseline unchanged, and its diff in artifacts as {"kind": "unified-diff", "content": "..."}; the parent then checks, applies, and advances the patch itself.

Rerun guard

The predicate is evaluated from the two records — no future blocker is guessed. The handoff echoes target/scope/mode, so the task triple is self-identifying:

same_task =
     new_dispatch.target == prior_handoff.target
  && new_dispatch.scope  == prior_handoff.scope
  && new_dispatch.mode   == prior_handoff.mode

A relaunch is forbidden when all four hold:

• same_task, and
• prior_handoff.blocker_signature is non-null (the prior stop was blocker-driven), and
• new_dispatch.prior_blocker == prior_handoff.blocker_signature (the same blocker), and
• new_dispatch.evidence_delta is empty (nothing new to try).

The non-null condition is load-bearing: a non-blocker stop (queue-empty/max-cycles/max-runtime/user-stop) has a null signature, and a null == null match must not forbid the rerun — those reruns are always allowed. A first dispatch carries prior_blocker: null and an empty evidence_delta, so it is never forbidden. A qualifying evidence_delta entry is any of:

• a materially changed goal or diagnostic,
• an advanced file-baseline/v1 baseline (accepted new content),
• a newly verified candidate lemma,
• changed source, or
• a newly available capability/tool.

When the predicate forbids a relaunch, route to review --mode=stuck, formalize, or human handoff instead.

Operational and protocol stops. A protocol-error or operational-error handoff has null blocker fields, so the signature predicate above never applies — but it must not be relaunched blindly either (the same malformed dispatch, unavailable checker, or unreconciled drift would just repeat). When the prior handoff carries a task identity (target/scope/mode non-null), this rule is scoped to same_task; a malformed-dispatch handoff with a null identity has no task to compare, so it applies to any paired retry of that stop. Such a stop may be relaunched only when the new dispatch's evidence_delta is nonempty and describes how the prior stop_detail was resolved (e.g. baseline reconciled, checker restored, dispatch corrected). An unrelated task is not a relaunch. Normal queue/budget/user stops remain freely rerunnable.

This is the single definition of the rule; prove.md, autoprove.md, and SKILL.md reference it rather than restating the predicate.

Human-in-the-loop

After a clear blocker in an interactive session, the parent presents options (continue with new evidence / switch to formalize / review --mode=stuck / stop and hand off) and never assumes autonomous continuation. The handoff record is the artifact the human reads to choose — the same record a subagent or inline worker would return.

Blocker-class vocabulary and the stuck review

/lean4:review --mode=stuck reports a Primary blocker class as human phrases; the handoff record's blocker_class is their kebab-case enum:

The stuck review block is not itself a complete handoff record — it carries no schema/record/status, no blocker_signature, and no custody fields. It supplies the evidence and the blocker vocabulary; the parent wraps that into a run-contract/v1 handoff record (mapping the phrase to the enum above).

See Also

• cycle-engine.md § Run Contract — roles, delegation expectations, no-subagent fallback
• cycle-engine.md § Stuck Definition — the blocker_signature
• cycle-engine.md § File baselines and drift — file-baseline/v1 custody
• sorry-filling.md — Blocked-Goal Triage classes