OpcodeSoundnessCert
plain-language theorem explainer
OpcodeSoundnessCert certifies that every LNAL virtual-machine opcode possesses a parser string that round-trips to it. LNAL report generators and invariant checkers cite the certificate to confirm the opcode set is closed under the parser. The proof is an exhaustive case split on the Opcode inductive type, with each branch supplying a literal string and invoking simp on parseOpcode.
Claim. Let $O$ be the inductive type of LNAL opcodes. The certificate asserts that for every $op : O$ there exists a string $s$ such that parseOpcode $s =$ some $op$.
background
LNAL is the language whose virtual machine is defined by the Opcode type and the parseOpcode function; the module bundles this coverage check with VM preservation and token-unit bounds. The verified field is a Prop that ignores its certificate argument and simply states the universal quantification over opcodes. Upstream Schedule structures from Atomicity and TechnologicalAccess supply the one-per-tick ordering and 8-tick neutrality constraints that the broader LNAL invariants rely upon.
proof idea
The theorem verified_any introduces an arbitrary opcode and performs cases on its constructors. Each of the sixteen branches supplies an explicit string literal and closes with simp on the parseOpcode definition, confirming the match without further hypotheses.
why it matters
The certificate is consumed by opcode_soundness_report and opcode_soundness_report_json in LNALReports, which emit OK/FAIL strings or JSON for downstream URC adapters. It supplies the parser-coverage component of the LNAL invariants bundle, ensuring the VM layer that feeds schedule and token operations is syntactically closed. No open scaffolding remains for this fragment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.