opcode_soundness_report_json
plain-language theorem explainer
The definition generates a JSON string reporting opcode soundness for an input source string by invoking a certificate constructor and a success-marking JSON builder. Developers integrating LNAL compiler outputs into audit pipelines would reference it for standardized reporting. The implementation is a direct wrapper that treats structural parser coverage as sufficient and supplies an empty error list.
Claim. A function mapping a source string $s$ to a JSON string obtained by constructing an opcode soundness certificate from $s$ and then applying the success constructor with an empty error list.
background
This definition sits inside the LNALReports adapter module, which supplies JSON emitters for compiler and certificate checks. It depends on OpcodeSoundnessCert.fromSource (imported from LNALCerts) to obtain a structural certificate and on the sibling mkJson to emit the report. Upstream results include the empty ledger definition and various is-structures for collision-free programs and continuum bridges, which supply the ledger and geometric primitives used in the broader LNAL compilation pipeline. The local setting is a collection of report generators that convert internal certificate objects into portable JSON without performing new verification steps.
proof idea
The definition is a one-line wrapper that applies mkJson true [] after the call to OpcodeSoundnessCert.fromSource src, with a comment noting that parser coverage is treated as structurally sufficient.
why it matters
The definition completes the JSON reporting layer for LNAL certificate checks inside the URC adapter suite. It supports external consumption of opcode soundness results by consent and ledger modules. No downstream theorems are listed, indicating it functions as a terminal reporting utility rather than an internal lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.