Rocq Alethe walker R-1: foundation module (parse wrapper)

Begins the Rocq-side Alethe walker port (mirror of the Lean arc
PRs #41-#52). Goal: end-to-end "cert IS the proof" reconstruction
for cvc5 alethe-2024 traces on Rocq, with UF + LIA mixed-theory
closure as the primary capability gain. Currently Rocq's LIA arm
is bare `lia` and its UF arm is a congruence chain; neither
composes for mixed-theory goals cvc5 handles natively. The
walker shifts Rocq from "can solve LIA, can solve UF, struggles
on mixed" to "can replay anything cvc5 closed".

R-1 establishes the module file and a Result-typed wrapper over
the SDK's already-shared `Proof_broker.Alethe.parse`. Walker
elaborators arrive starting R-2 (clausal layer). The SDK's ADT
(Sexp.t, step, proof) and parser are shared by both bridges, so
the Rocq side reuses them directly — no mirror-in-OCaml work
like Lean PR #41 needed (Lean had to build its own Sexp ADT and
FFI envelope; Rocq just uses the OCaml SDK directly).

Audit H1 contract (same as Lean): walker failure surfaces as a
tactic failure, with the existing lia fallback re-running.
Wired into close_or_fail in R-9; no closer integration yet.

Subsequent PRs follow the Lean cluster decomposition: R-2
clausal, R-3 arithmetic, R-4 multi-literal resolution, R-5
equality, R-6 trust-tagged leaves, R-7 boolean cleanup, R-8
equiv_simplify, R-9 wire into closer, R-10 equiv_pos1/equiv_pos2,
R-11 cong over operators (visible payoff PR), R-12 snapshot test
against the real cvc5 trace pinned in Lean #52.

Validation: local Rocq env is broken (missing zarith,
rocq-runtime per project memory); rely on CI for the full build.
The OCaml file itself is 15 lines of `Result`-typed exception
wrapping — confident in syntax.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

Author: levineuwirth

rocq-bridge/src/alethe_walker.ml

@@ -0,0 +1,22 @@
+(** Rocq-side Alethe walker. R-1: foundation only — the parse
+    wrapper that surfaces the SDK's already-shared
+    [Proof_broker.Alethe.parse] in a [Result] form for the Rocq
+    plugin. Walker elaborators arrive starting R-2.
+
+    See [.mli] for the multi-PR plan and audit-H1 contract. *)
+
+module Alethe = Proof_broker.Alethe
+
+type proof = Alethe.proof
+
+let parse_trace (s : string) : (proof, string) result =
+  try Ok (Alethe.parse s)
+  with
+  | Alethe.Parse_error msg ->
+    Error ("alethe parse: " ^ msg)
+  | exn ->
+    (* Defensive: any other exception (e.g. an unexpected stack
+       overflow not caught by [parse]'s own backstop) becomes an
+       Error so the caller falls through to [lia] cleanly,
+       rather than propagating and crashing the tactic. *)
+    Error ("alethe parse: unexpected exception: " ^ Printexc.to_string exn)

rocq-bridge/src/alethe_walker.mli

@@ -0,0 +1,47 @@
+(** Rocq-side Alethe walker — R-1 foundation.
+
+    Mirror of [lean-bridge/ProofBroker/Alethe.lean]'s walker module
+    (PR #41-#52 on the Lean side). This module elaborates cvc5's
+    alethe-2024 trace into a Coq kernel proof term — the "cert IS
+    the proof" architectural play, parallel to the Tier-1 Farkas
+    [Term_mode] closer for Tier-1 certs but for Tier-3 alethe-2024.
+
+    Audit H1: walker failure surfaces as a tactic failure, with
+    the existing [lia] fallback re-running (closer chain in
+    [Pb_rocq_main.close_or_fail]). No axioms are introduced by the
+    walker itself — proof-term construction goes through the
+    kernel like every other tactic, and the cert never widens the
+    trust footprint.
+
+    R-1 scope (this PR): module file scaffolding + the parse
+    wrapper exposing the SDK's [Proof_broker.Alethe.parse] in a
+    Result-typed form. No walking yet; the per-rule elaborators
+    arrive in R-2 (clausal layer) and onward. The SDK's ADT
+    ([Sexp.t], [step], [proof]) and parser are shared across both
+    bridges, so the Rocq side reuses them directly via
+    [Proof_broker.Alethe] rather than mirroring in OCaml the way
+    Lean had to mirror them in Lean.
+
+    Subsequent PRs follow the same cluster decomposition as the
+    Lean arc: R-2 clausal, R-3 arithmetic, R-4 multi-literal
+    resolution, R-5 equality, R-6 trust-tagged leaves, R-7
+    boolean cleanup, R-8 [equiv_simplify], R-9 wire into closer,
+    R-10 [equiv_pos1]/[equiv_pos2], R-11 [cong] over operators,
+    R-12 snapshot test. See plan in [.claude/]. *)
+
+(** Re-export of the SDK's [proof] type as the canonical Alethe
+    proof representation used by the walker. The SDK is shared by
+    both bridges and already includes named-reference expansion,
+    so the walker consumes a fully-resolved proof from the start. *)
+type proof = Proof_broker.Alethe.proof
+
+(** Parse an alethe-2024 trace string into a [proof].
+
+    Failure modes:
+    - parser error (malformed trace, unterminated S-expression,
+      depth exceeded) → [Error msg];
+    - stack overflow (deeply-nested untrusted solver output) →
+      [Error msg];
+    - any other unexpected exception is converted to [Error msg]
+      so the caller can fall through to [lia] cleanly. *)
+val parse_trace : string -> (proof, string) result