Phase 3 Rocq parity M2: LLM-replay closer + audit-H1 axiom gate

[levineuwirth]

What

Rocq mirror of `replayLlmScriptOrFail` (Lean PR #35). When a Tier-3 cert arrives with reason `Tier3_replay_deferred` (the LLM-as-backend `lean-tactic-script` cert from `Adapter_llm` — SDK-shared, no Rocq-specific adapter work needed for M2), `close_or_fail` routes it to a new `Llm_replay.replay_script` closer instead of the fragment-keyed chain.

Same audit-H1 contract as Lean: kernel replay + transitive-axiom subset check against the classical Rocq Stdlib allowlist (`ClassicalDedekindReals.sig_forall_dec`, `FunctionalExtensionality.functional_extensionality_dep`). A hallucinated `admit` / `Axiom Foo` / parse failure / non-closing script is a tactic failure with the goal left OPEN — never an admitted theorem.

How (audit H1)

New module `rocq-bridge/src/llm_replay.ml`:

• Parse the candidate via `Procq.parse_string Pltac.tactic` + `Tacintern.intern_pure_tactic` — same idiom `invoke_named_tactic` already uses for stdlib tactics.
• Capture the goal's evar; eval the tactic via `Tacinterp.eval_tactic`.
• After the script runs, query the sigma for the evar's assignment (`Evd.find` + `Evd.evar_body`). Empty body ⇒ script didn't close ⇒ audit-fail.
• Collect the proof term's transitive axioms via `Assumptions.assumptions` — the same kernel internal API Rocq's `Print Assumptions` vernacular uses. `add_opaque:false` so opaques are treated as black boxes (audited at their own define site). Dummy `indirect_accessor` is safe under that flag.
• Subset-check the `Axiom (Constant kn, _)` entries against the allowlist. Other variants (`Positive`/`Guarded`/etc.) are accepted as inherent Rocq machinery.
• Failure modes all surface via a shared `audit_fail` helper.

Wired into `close_or_fail` (`pb_rocq_main.ml`): a new `Tier3_replay_deferred _` arm extracts the script from `cert.payload` (`Tier3_proof_trace { trace_data = String script }`) and dispatches.

Test-only tactic (`g_proof_broker.mlg`): `llm_replay_test "<script>"` — direct entry to `Llm_replay.replay_script`, bypassing the cert envelope. Lets CI exercise the audit-H1 contract without a live LLM endpoint.

Tests (CI-stable, no network)

Positive `pb_llm_replay_axiom_free`: clean `intros; reflexivity` script closes a small Z-equality goal. Allowlisted `[]`.

Negative `assert_fails (llm_replay_test "idtac")` — script runs but doesn't close.

Negative `assert_fails (llm_replay_test "@@@ ...")` — script doesn't parse.

The first `admit`/`Axiom Foo` rejection test is deferred — needs a local `Axiom` declaration in the test file to drive into the proof term, which adds setup complexity I'd rather defer until M2 is landing.

Verification

Locally: SDK + Rocq plugin sources build clean (`dune build sdk rocq-bridge/src` rc=0). Python schema/gate suite green. JSON allowlist valid. The Rocq theory build path (incl. `pb_llm_replay_axiom_free` + the negative `assert_fails` examples) needs CI — local opam env still hits the same rocq-core 9.1.1 split-build-mode bug from M1.

Scope

M2 is the home-side replay closer + test-only tactic only — the same scope as Lean PR #35. The `Adapter_llm` is currently Lean-flavored (renders Lean syntax, mints `lean-tactic-script` certs) — making it bridge-aware (so it produces Ltac for Rocq home systems) is its own slice, naturally part of M3 / the LLM-assisted-reconstruction work or its own preceding mini-slice. M2's test-only tactic exercises the closer in isolation.

Remaining M's

• M3: LLM-assisted reconstruction fallback (`tryLlmReconstruct?` mirror) — wires the SDK's `Llm_reconstruct.translate` into `close_or_fail`'s try/catch fallback for un-replayable certs. Likely also needs a bridge-aware prompt on the SDK side.
• M4: Polish — `fragment_of_logic` consolidation (Phase-4 retro carry), docstring / docs / delta sync, retrospectives.

🤖 Generated with Claude Code