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

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

**Bridge-aware SDK** (`sdk/lib/adapter_llm.ml`, `llm_reconstruct.ml`):
- New `rocq_ty` / `rocq_term` / `rocq_paren` parallel to the
  existing Lean rendering helpers — translate IR's bridge-agnostic
  type-ref vocabulary (Int / Real / Prop + arrow chains) to Rocq
  Stdlib syntax (Z / R / Prop with ASCII `->`), and render
  shell_terms with Rocq's `/\` `\/` `~` 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` (safer
  LLM-familiar default).
- `Adapter_llm.dispatch` and `Llm_reconstruct.translate` both pick
  the dialect upfront — 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).

**Closers tightened** (M3.b): 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
(misconfigured manifest pointing this bridge at a Lean-flavored
LLM endpoint, or future bug) is a clean user error rather than a
silent parse failure when Ltac tries to chew on Lean syntax.

**Reconstruction fallback** (M3.c, `rocq-bridge/src/pb_rocq_main.ml`):
Mirror of Lean's `closeOrFailPrimary` + `closeOrFail` wrap.
- The existing `close_or_fail` is renamed `close_or_fail_primary`.
- New `replay_reconstructed_script trace_format script` runs the
  candidate through `Llm_replay.replay_script` (the same audit-H1
  gate from M2) and on success emits a `Feedback.msg_info` line
  naming the source trace format — audit trail visible in build
  output.
- New `try_llm_reconstruct ir cert?` gates on Tier-3 cert with
  `trace_format ≠ rocq-tactic-script`, calls
  `Proof_broker.Llm_reconstruct.translate` (direct-linked, no FFI),
  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.

**Test-only tactic** (`g_proof_broker.mlg`): new `llm_reconstruct_test
"<format>" "<script>"` drives `replay_reconstructed_script`
directly with a string literal — exercises the audit-H1 contract
without a live LLM endpoint. Mirror of Lean's evalLlmReconstructTest.

**Tests** (Rocq-side mirror of Lean's `llm_reconstruct_test` block):
- 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 translation.
- Negative `assert_fails (llm_reconstruct_test ... "@@@ ...")` —
  parse failure.

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

Locally verified: SDK + Rocq plugin sources build clean (`dune
build sdk rocq-bridge/src` rc=0). Full SDK suite passes including
the new Rocq tests. Python schema/gate suite green. JSON
allowlist valid. The Rocq theory build path (incl. the new
fallback test and Print Assumptions on `pb_llm_reconstruct_axiom_free`)
needs CI per the same broken-local-rocq-env caveat from M1/M2.

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.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: levineuwirth

rocq-bridge/src/g_proof_broker.mlg

@@ -58,3 +58,23 @@ END
 TACTIC EXTEND ProofBrokerLlmReplayTest
 | [ "llm_replay_test" string(s) ] -> { Llm_replay.replay_script s }
 END
+
+(* TEST-ONLY tactic for the LLM-assisted Tier-3 reconstruction
+   fallback (roadmap §Phase 3 #4, Rocq parity M3). The live SDK
+   path ([Llm_reconstruct.translate]) only runs when an endpoint
+   is configured — for CI we skip the translation call and feed
+   the candidate script directly into the {e same} closer the
+   production path invokes after a successful translation
+   ([Pb_rocq_main.replay_reconstructed_script]). This pins the
+   integration: a translated script flows through
+   [Llm_replay.replay_script] (kernel replay + axiom-footprint
+   gate), the same audit-H1 contract [llm_replay_test] exercises
+   for primary LLM certs. First argument is the trace format of
+   the (notionally un-replayable) source cert — surfaces in the
+   audit feedback line. Mirror of [llm_reconstruct_test] in
+   lean-bridge/Test/Tactic.lean. *)
+TACTIC EXTEND ProofBrokerLlmReconstructTest
+| [ "llm_reconstruct_test" string(fmt) string(s) ] -> {
+    Pb_rocq_main.replay_reconstructed_script fmt s
+  }
+END

rocq-bridge/src/pb_rocq_main.ml

@@ -211,7 +211,13 @@ let closer_for_fragment fragment : unit Proofview.tactic =
               cert-gated closer in the core plugin)"
              other))
 
-let close_or_fail (p : path) : unit Proofview.tactic =
+(* Primary closer chain: fragment-keyed dispatch for verified
+   reasons, plus the LLM-replay arm for [rocq-tactic-script]
+   certs. Renamed from [close_or_fail] in M3.c — the public
+   [close_or_fail] (below) is now a wrapper that catches a
+   primary failure and tries LLM-assisted Tier-3 reconstruction
+   before re-raising the error. *)
+let close_or_fail_primary (p : path) : unit Proofview.tactic =
   match p.cert, p.verify_reason with
   | None, _ ->
     CErrors.user_err Pp.(
@@ -229,14 +235,30 @@ let close_or_fail (p : path) : unit Proofview.tactic =
         Rocq Stdlib allowlist. Audit H1: a hallucinated [admit]
         or [Axiom Foo] is a tactic failure, never an admitted
         theorem. *)
-     | Tier3_replay_deferred _ ->
+     | Tier3_replay_deferred { trace_format = "rocq-tactic-script" } ->
+       (* M3.b: tightened to only accept the Rocq-flavored cert.
+          A [lean-tactic-script] cert reaching the Rocq closer is
+          a configuration error (LLM adapter saw this bridge as
+          Lean-flavored), not a tactic-soundness issue — surface
+          it as a clear user error rather than silently trying to
+          parse Lean tactics as Ltac. *)
        (match cert.payload with
         | Tier3_proof_trace { trace_data = `String script; _ } ->
           Llm_replay.replay_script script
         | _ ->
           CErrors.user_err Pp.(
             str "proof_broker: Tier-3 replay-deferred cert payload \
                  is not a string trace; cannot replay"))
+     | Tier3_replay_deferred { trace_format } ->
+       CErrors.user_err Pp.(
+         str (Printf.sprintf
+                "proof_broker: LLM cert has trace_format=%S but the \
+                 Rocq home-system replayer only accepts \
+                 'rocq-tactic-script'. The LLM adapter likely saw \
+                 this IR as a Lean source_system; ensure the Rocq \
+                 reifier sets ir.source_system.name = \"rocq\" so \
+                 [Adapter_llm.dialect_of_ir] picks the Rocq dialect."
+                trace_format))
      | Verified_envelope | Verified_farkas
      | Verified_case_split | Verified_tier3
      (* Verified_tier3_provenance gates the home-system closer
@@ -270,6 +292,73 @@ let close_or_fail (p : path) : unit Proofview.tactic =
     CErrors.user_err Pp.(
       str "proof_broker: internal — cert present but verify outcome missing")
 
+(* --- M3.c: LLM-assisted Tier-3 reconstruction fallback ----------- *)
+
+(* Run [Llm_replay.replay_script] on a candidate the LLM produced
+   via reconstruction (rather than the primary LLM-as-backend
+   path). On success, emit a [Feedback.msg_info] line naming the
+   source trace format so the audit trail of how the goal closed
+   is visible in the build output. Mirror of Lean's
+   [replayReconstructedScript]. *)
+let replay_reconstructed_script (trace_format : string)
+    (script : string) : unit Proofview.tactic =
+  let announce =
+    Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+      Feedback.msg_info (Pp.str (Printf.sprintf
+        "proof_broker: closed via LLM Tier-3 reconstruction \
+         (%s trace → Rocq Ltac script, kernel-checked, audit H1)."
+        trace_format))))
+  in
+  Proofview.tclBIND (Llm_replay.replay_script script) (fun () -> announce)
+
+(* Decide whether to invoke LLM-assisted reconstruction on the
+   current cert + return a fallback tactic if so. Gates (no-op
+   unless all hold):
+   * a cert is in hand,
+   * tier is 3 with a [Tier3_proof_trace] payload,
+   * [trace_format] is not already [rocq-tactic-script] (which the
+     primary LLM-replay arm at the top of [close_or_fail_primary]
+     handles),
+   * the SDK's [Llm_reconstruct.translate] returns a non-empty
+     script (so this is silent when no endpoint is configured —
+     the primary failure is re-raised).
+
+   The translate call runs immediately when this function is
+   invoked; callers should only invoke it from the [tclORELSE]
+   handler so the HTTP request is lazy (fires only on primary
+   failure). *)
+let try_llm_reconstruct (ir : Ir.t) (cert_opt : Cert.t option)
+  : unit Proofview.tactic option =
+  match cert_opt with
+  | None -> None
+  | Some (cert : Cert.t) ->
+    if cert.tier <> 3 then None
+    else match cert.payload with
+    | Tier3_proof_trace { trace_format = "rocq-tactic-script"; _ } ->
+      None
+    | Tier3_proof_trace { trace_format; _ } ->
+      (match Proof_broker.Llm_reconstruct.translate ir cert with
+       | Error _ -> None
+       | Ok script ->
+         Some (replay_reconstructed_script trace_format script))
+    | _ -> None
+
+(* Public closer: try the primary fragment-keyed chain; on any
+   failure, try LLM-assisted Tier-3 reconstruction before
+   re-raising the primary error. Mirror of Lean's [closeOrFail]
+   try/catch wrap. Audit H1: the reconstruction path goes
+   through the SAME audit gate [replay_reconstructed_script] →
+   [Llm_replay.replay_script] uses for primary
+   [rocq-tactic-script] certs — kernel replay + axiom-footprint
+   subset check — so the LLM never widens the trust base. *)
+let close_or_fail (p : path) : unit Proofview.tactic =
+  Proofview.tclORELSE
+    (close_or_fail_primary p)
+    (fun (primary_exn, primary_info) ->
+      match try_llm_reconstruct p.ir p.cert with
+      | None -> Proofview.tclZERO ~info:primary_info primary_exn
+      | Some fallback -> fallback)
+
 (* --- public entry points ------------------------------------------- *)
 
 let run_close (names : Names.Id.t list option) : unit Proofview.tactic =

rocq-bridge/src/pb_rocq_main.mli

@@ -38,3 +38,13 @@ val run_close_term : Names.Id.t list option -> unit Proofview.tactic
     arity > 2, non-Le hypotheses, etc.) — the user explicitly
     opted into term mode by typing [proof_broker_term] over
     plain [proof_broker]. *)
+
+val replay_reconstructed_script :
+  string -> string -> unit Proofview.tactic
+(** [replay_reconstructed_script trace_format script] feeds the
+    LLM-translated script through [Llm_replay.replay_script]
+    (the audit-H1 gate) and, on success, emits a
+    [Feedback.msg_info] line naming the source trace format so
+    the audit trail is visible in build output. Exported for the
+    test-only [llm_reconstruct_test] tactic to drive the
+    reconstruction-side closer without a live LLM endpoint. *)

rocq-bridge/theories/Test.v

@@ -703,3 +703,49 @@ Proof.
   assert_fails (llm_replay_test "@@@ not lean @@@").
   exact I.
 Qed.
+
+(* ============================================================
+   LLM-assisted Tier-3 reconstruction fallback
+   (roadmap §Phase 3 deliverable 4, Rocq parity M3).
+
+   [llm_reconstruct_test "<traceFmt>" "<script>"] simulates a
+   successful [Llm_reconstruct.translate] call (the LLM was
+   asked to translate an un-replayable Tier-3 trace and
+   returned the script) and routes the candidate through the
+   SAME audit-H1 gate the production fallback uses. The
+   translation step itself is a pure I/O wrapper around an
+   untrusted oracle — no soundness contribution — so swapping
+   the live SDK call for a literal script is faithful to what's
+   being tested: that a candidate script makes it through
+   [replay_reconstructed_script] → [Llm_replay.replay_script],
+   with the audit-H1 gate firing identically. Mirror of the
+   llm_reconstruct_test block in lean-bridge/Test/Tactic.lean. *)
+
+(* Positive: a translated script the kernel independently
+   accepts (axiom-free [intros; reflexivity]) closes the goal
+   via the reconstruction fallback's replay closer. The build
+   log carries the "closed via LLM Tier-3 reconstruction …"
+   audit line. *)
+Theorem pb_llm_reconstruct_axiom_free : forall x : Z, x = x.
+Proof.
+  llm_reconstruct_test "alethe-2024" "intros x; reflexivity".
+Qed.
+
+Print pb_llm_reconstruct_axiom_free.
+Print Assumptions pb_llm_reconstruct_axiom_free.
+
+(* Negative: a translation that runs without error but does not
+   close the goal is a tactic failure, never a silent pass. *)
+Example pb_llm_reconstruct_rejects_non_closing : True.
+Proof.
+  assert_fails (llm_reconstruct_test "alethe-2024" "idtac").
+  exact I.
+Qed.
+
+(* Negative: a translation that does not parse as Rocq Ltac is
+   a tactic failure, not an admitted theorem. *)
+Example pb_llm_reconstruct_rejects_unparsable : True.
+Proof.
+  assert_fails (llm_reconstruct_test "tstp-fof" "@@@ not lean @@@").
+  exact I.
+Qed.