R4 — the syntactic half (4a), structural core #

StableHLO.lean closes the semantic half of R4: den (emit g) = fderiv. The syntactic half asks that the emitted text be a faithful, recoverable encoding of the graph — parse (pretty a) = a (the doc's "4a"). A verified lexer/parser of the literal SSA StableHLO text (with multi-instruction op expansion + name resolution) is a large separate build; this file lands its structural core, which is the load-bearing part:

• Raw — the renderable skeleton of an SHlo graph (opcodes + shapes + leaf SSA names, with the ℝ operand values and the shape index erased: the text never carries the runtime values, only the op structure).
• skel : SHlo n → Raw — extract that skeleton.
• toToks : Raw → List Tok — a postorder token serialization (the order pretty already emits in: children before parent).
• parse : List Tok → Option Raw — a stack reconstructor.
• parse_skel / roundtrip — parse (toToks (skel a)) = some (skel a): the op-graph is recovered exactly from its serialization. Proven by structural induction (no string reasoning, no SSA-freshness bookkeeping).

What this buys: the structure of the emitted graph (which op, which operands, which shapes) is now proven recoverable — it leaves the trusted surface. What remains audited (the thin lexical boundary): the per-op Tok ↔ StableHLO text map — i.e. that stablehlo.dot_general … contracting_dims = [1] x [0] is the string for a dotIn token. That, plus per-op spec conformance, IREE lowering, and float32 ≈ ℝ, is the residue (validated by iree-compile + the GPU runs). Closes under [propext, Classical.choice, Quot.sound].