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

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.