opcode_soundness_report
plain-language theorem explainer
The opcode soundness report function accepts a source string and emits a diagnostic message that confirms whether the string parses exclusively to valid LNAL opcodes. Compiler verification work in the Recognition monolith invokes it to obtain immediate pass/fail output on opcode coverage. The definition builds the certificate from the source and selects the success or failure string according to the certificate's validity flag.
Claim. For a source string $s$, the report equals the string ``OK: Opcode set sound (parser accepted only LNAL opcodes)'' when the certificate constructed from $s$ has its ok flag true, and otherwise equals the failure string formed by intercalating the certificate's error list with semicolons.
background
The LNALReports module supplies string diagnostics for LNAL compiler properties inside the URC adapter layer. The opcode soundness certificate is a structure whose verified property asserts that every VM opcode admits a string representation that the parser recovers exactly. Construction of the certificate from source therefore checks that the supplied text contains only recognized opcodes. The module also imports the soundness theorems for integers and rationals extracted from logic, which guarantee that the mk constructors for these types respect the underlying equivalence relations.
proof idea
The definition is a direct computation: it calls fromSource on the input string to obtain the certificate, then branches on the ok flag to choose either the fixed success message or the concatenated error string. No additional lemmas are invoked.
why it matters
This definition completes the reporting interface for opcode soundness inside the LNAL adapter suite, exposing the certificate result as a plain string for downstream tooling. It sits alongside sibling reports for invariants, cost ceilings and schedule neutrality, thereby closing the diagnostic layer that validates the LNAL compiler before it is used in higher Recognition derivations. The certificate itself rests on the parser completeness property rather than on J-uniqueness or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.