Phase 3 Rocq parity M3: bridge-aware LLM adapter + reconstruction fallback

[levineuwirth]

What

Rocq mirror of Lean PR #36 (LLM-assisted Tier-3 reconstruction fallback) — plus the load-bearing prerequisite that makes the fallback work cross-bridge: the SDK's `Adapter_llm` and `Llm_reconstruct` now produce bridge-appropriate prompts and trace_formats based on `ir.source_system.name`.

Without bridge-awareness, Rocq home systems would receive Lean syntax in LLM responses and the audit_fail path would always fire — fallback exists but never produces parseable scripts. M3 fixes both layers in one PR.

Pieces

M3.a — bridge-aware SDK (`sdk/lib/adapter_llm.ml` + `llm_reconstruct.ml`)

New `rocq_ty` / `rocq_term` / `rocq_paren` parallels to the existing Lean helpers — translate IR's bridge-agnostic vocabulary (Int / Real / Prop + arrow chains) to Rocq Stdlib syntax (Z / R / Prop + ASCII `->`), and render shell_terms with `/\` `\/` `~` connectives, `forall (x : T), body` quantifiers, ASCII Z-scope arithmetic.

New `dialect` record bundles per-bridge state (system_prompt, render_prompt, ty, term, trace_format, cert_format, annotation). `dialect_of_ir` dispatches on `ir.source_system.name`: `"rocq"` → `rocq_dialect`, everything else → `lean_dialect`. Rocq home systems get Rocq-flavored prompts asking for Ltac in a fenced ```coq block; minted certs carry `format = trace_format = "rocq-tactic-script"`.

`Verifier.verify` extends its Tier-3 dispatch to recognize both `lean-tactic-script` and `rocq-tactic-script` → both return `Tier3_replay_deferred { trace_format }` (envelope-only; soundness deferred to the home kernel's audit-H1 replay gate).

M3.b — tightened closers

Rocq's `close_or_fail` now matches `Tier3_replay_deferred { trace_format = "rocq-tactic-script" }` specifically. A `lean-tactic-script` cert reaching the Rocq closer is a clean user error rather than silently trying to parse Lean syntax as Ltac. Lean's `closeOrFail` already gated on `lean-tactic-script`.

M3.c — reconstruction fallback wiring (`rocq-bridge/src/pb_rocq_main.ml`)

Mirror of Lean's `closeOrFailPrimary` + `closeOrFail` wrap from PR #36.

• Existing `close_or_fail` → `close_or_fail_primary`.
• New `replay_reconstructed_script` routes through `Llm_replay.replay_script` (the audit-H1 gate from M2) and emits a `Feedback.msg_info` audit line on success.
• New `try_llm_reconstruct` gates on Tier-3 cert with `trace_format ≠ rocq-tactic-script`, calls `Proof_broker.Llm_reconstruct.translate` (direct-linked, no FFI on Rocq), returns `Some fallback_tac` or `None`.
• New `close_or_fail` wraps primary in `Proofview.tclORELSE`; on primary failure invokes `try_llm_reconstruct` lazily (HTTP only fires when primary actually fails) and routes to the fallback if a script came back, else re-raises the primary error.

Audit H1: reconstruction goes through the SAME audit gate as primary LLM-replay (kernel replay + axiom-footprint subset check), so the LLM never widens the trust base.

M3.d — test-only tactic + tests

`llm_reconstruct_test "" "<script>"` TACTIC EXTEND drives `replay_reconstructed_script` directly with a string literal — exercises the audit-H1 contract without a live LLM endpoint. Mirror of Lean's `evalLlmReconstructTest`.

Rocq tests in `Test.v`:

• Positive `pb_llm_reconstruct_axiom_free`: clean `intros; reflexivity` translation closes a Z-equality goal. Allowlisted `[]`.
• Negative `assert_fails (llm_reconstruct_test ... "idtac")` — non-closing.
• Negative `assert_fails (llm_reconstruct_test ... "@@@ ...")` — parse failure.

SDK tests added Rocq-flavored coverage: `test_prompt_render_rocq` and `test_mock_endpoint_rocq` for `Adapter_llm` verify Z translation, `Theorem ... Proof. ... Qed.` scaffold, ```coq fence, and that the Rocq-flavored cert's verify reason carries `trace_format = "rocq-tactic-script"`. Same for `Llm_reconstruct`.

Verification

Locally: SDK + Rocq plugin sources build clean. SDK suite passes including the new Rocq render/transport tests for both `adapter_llm` and `llm_reconstruct`. Python schema/gate suite green. JSON allowlist valid. Rocq theory build path needs CI per the same broken-local-rocq-env caveat from M1/M2.

Scope

With this, Phase 3 Rocq parity is structurally complete for deliverables #3 and #4. M4 (polish) carries the `fragment_of_logic` consolidation (Phase-4 retro carry) plus a README/delta sync to record the Rocq Phase-3 surface.

🤖 Generated with Claude Code