group-worker-proving

name	group-worker-proving
description	由 group-worker 使用，读取 group_worker_input.json，在 group worktree 中证明 assigned witness blocks，并只在 group-local case_lib 中新增带当前 group_id suffix 的 helper declarations 和必要 Rocq 官方库 import。

Group Worker Proving

只读取 startup message 指定的 group_worker_input.json。其结构化字段是唯一 source of truth；不得依赖 parent chat context。 problem_context、annotation_design_summary 和 vc_checking_plan 若存在，必须优先作为 proof strategy 起点；缺失时在本次 spawn 内直接分析 assigned witnesses，不返回确认请求。

文档

• docs/coq-tooling-policy.md：固定 Coq tooling 和 group-check evidence。
• docs/separation-logic-whole-proof-tactics.md：separation logic proof tactic 操作规则、side goal 形态和常见证明骨架。
• docs/refinement-proof-tactics.md：refinement / safeExec proof 规则、prog_nf 工作流和禁止的低层 reconstruction。
• docs/pure-proposition-proof-patterns.md：annotation-facing pure predicate 的 proof-side bridge、rewrite 和 helper 规则。
• docs/reference-cases.md：允许参考的 case 范围。

允许工作

• 只编辑 group worktree 中 assigned witness proof bodies。
• 只在 group-local case_lib 新增已证明的顶层 Lemma、Theorem、Fact 或 Remark。
• 允许在 group-local case_lib 新增证明所需的 Rocq 官方库 import，例如 Require Import Coq... 或 From Coq... Require Import ...。
• 不修改 generated files、witness statements、unassigned witness blocks 或 seed case_lib declarations。
• formal output 只写 group worktree；machine output 只写声明的 group_worker_report.json。
• 必须在单次 spawn 内尽量完成本 group 的所有 assigned witnesses。失败 tactic、proof route 不确定、缺少 optional hint、或需要当前 group suffixed helper，都应在本次 spawn 内调试、改 proof、补 helper、重跑 fixed group-check。

Blocking 原则

group-worker 的 blocked 只用于两类情况：

• 某个 assigned witness lemma 在当前 source_goal_version 下完全不可证：经过 proof state 分析、必要 helper 尝试和 fixed group-check/debug 后，确认缺少的 premise 不能从当前 VC、当前 case_lib 或允许新增的当前 suffix helper 中推出，必须回到 annotation/spec。
• 必要工具发生重大错误：fixed coq_tooling.py debug / check 或 group-check workspace 完全不可运行，且已记录具体 command evidence。

以下情况不得 blocked，必须在本次 spawn 内自行解决：单个 tactic 失败、proof route 不确定、需要新增当前 group suffix helper、vc-checking plan 缺字段、optional reference 缺失、同构 helper 可能被其他 group 也需要、或某个 witness 需要多轮 debug。输入版本失效写 stale。context compaction 只写 compact-error 事实；是否重试或最终 block 由 controller / main agent 判定。

Helper namespace

每个新 case_lib helper 名称必须以 group_worker_input.json.helper_namespace.suffix 结尾。

• policy 必须是 group-id-suffixed。
• suffix 形如 __<sanitized_group_id>。
• 不新增 unsuffixed helper。
• 不使用其他 group 的 suffix。
• 如果 helper 必须跨 group 共享，停止并报告 blocker，让该事实回到 annotation 成为 seed case_lib declaration。
• 不要把“多个 group 可能需要同构 helper”作为 blocker；当前 group 可以新增带自己 suffix 的 helper 并证明。

每个新增 helper 和新增 Rocq 官方库 import 都要写入 agent_result.vc_proving.group.case_lib_added_declarations，包含 name、kind 和 statement_hash。import 的 kind 写 Import，不得记录或新增非 Rocq 官方库 import。

Coq feedback

• 只使用 handoff 声明的 coq_tooling.py debug 和 coq_tooling.py check。
• 不手写 Coq flags，不调用 Dune，不调用 Rocq MCP，不使用 _CoqProject derived command，不使用 coqc -o。
• final group evidence 必须满足 target_kind == "group-check"，并记录当前 source_goal_version。
• JSON 检查使用 python3 或 shell builtins，不使用 jq。

Report 输出

group_worker_report.json 必须设置 agent_result.vc_proving.group.status 为 completed、blocked、stale 或 compact-error。completed report 包含 solved/unsolved witness lists、blockers/errors、candidate file paths、helper namespace、added helper declarations 和 Coq evidence。compact-error report 只记录 compaction 事实和可复用 evidence pointer，不声明 witness 不可证。

不得遗留 Admitted.、Abort.、extra Axiom、debug commands，或在 *_proof_manual.v 中新增 helper declarations。

同时写 group_worker_output.txt 作为 non-authoritative reuse note。第一行必须是 # Reuse Note，正文包含 Note kind: non-authoritative reuse note 和 This file is not acceptance evidence.。如果 output note 与 structured/current sources 冲突，以 group_worker_report.json、group_worker_input.json、group_workers_manifest.json、source versions 和当前 worktree files 为准。