OpcodeSoundnessCert
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove semantic preservation or execution correctness of any opcode.
- Does not bound token deltas or J-costs associated with opcode sequences.
- Does not address parsing of invalid strings or error reporting.
- Does not interact with JMonotoneCert or UnitsKGateCert.
Lean usage
let cert := OpcodeSoundnessCert.fromSource src; if OpcodeSoundnessCert.verified cert then ... else ...formal statement (Lean)
83structure OpcodeSoundnessCert where deriving Repr
84
85/-- Parser covers all VM opcodes by name. -/
86@[simp] def OpcodeSoundnessCert.verified (_c : OpcodeSoundnessCert) : Prop :=
proof body
Definition body.
87 ∀ (op : IndisputableMonolith.LNAL.Opcode),
88 ∃ s : String, IndisputableMonolith.LNAL.parseOpcode s = some op
89
90@[simp] theorem OpcodeSoundnessCert.verified_any (c : OpcodeSoundnessCert) :
91 OpcodeSoundnessCert.verified c := by
92 intro op; cases op <;> first
93 | exact ⟨"LOCK", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
94 | exact ⟨"BALANCE", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
95 | exact ⟨"FOLD", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
96 | exact ⟨"UNFOLD", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
97 | exact ⟨"BRAID", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
98 | exact ⟨"HARDEN", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
99 | exact ⟨"SEED", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
100 | exact ⟨"SPAWN", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
101 | exact ⟨"MERGE", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
102 | exact ⟨"LISTEN", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
103 | exact ⟨"GIVE", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
104 | exact ⟨"REGIVE", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
105 | exact ⟨"FLIP", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
106 | exact ⟨"VECTOR_EQ", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
107 | exact ⟨"CYCLE", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
108 | exact ⟨"GC_SEED", by simp [IndisputableMonolith.LNAL.parseOpcode]⟩
109
110def OpcodeSoundnessCert.fromSource (_src : String) : OpcodeSoundnessCert :=
111 {}
112
113/-- Schedule neutrality certificate aggregating schedule-related checks. -/