lnal_invariants_report_json
plain-language theorem explainer
The definition maps an input source string to a JSON report string that encodes the verification status and any errors for LNAL invariants. It is referenced by LNAL compiler pipelines and external audit tools that require machine-readable certification output. The body is a direct two-step composition that instantiates the certificate via fromSource and delegates serialization to mkJson.
Claim. Let $f(s)$ be the function that sends a source string $s$ to the pretty-printed JSON object whose fields are the boolean verification flag and the list of error strings taken from the LNAL invariants certificate of $s$.
background
LNALInvariantsCert is the structure that packages a boolean ok flag together with a list of error strings; its doc-comment states that it bundles VM preservation and token δ-unit bound checks. The helper mkJson builds a Lean.Json object with keys 'ok' and 'errors' and renders it via pretty-printing. The surrounding module URCAdapters.LNALReports supplies adapter functions that turn LNAL compiler artifacts into consumable reports.
proof idea
The definition is a one-line wrapper that first applies LNALInvariantsCert.fromSource to the input string and then feeds the resulting ok and errors fields directly into mkJson.
why it matters
The definition supplies the JSON serialization layer for LNAL invariant certificates, allowing downstream tooling to consume verification results without re-implementing the certificate structure. It sits inside the URC adapter layer that bridges the core LNAL compiler to external reporting and consent mechanisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.