LNALInvariantsCert
plain-language theorem explainer
LNALInvariantsCert packages a boolean success flag and error list to certify that LNAL programs preserve VM invariants under single steps and bound token-count changes to unit size. Report generators and manifest builders cite it to validate source before execution or aggregation. The verified property holds by direct appeal to the lStep preservation lemmas for VM states and token parity.
Claim. A certificate $C$ consisting of a boolean $ok$ and list of error strings such that $C.verified$ asserts: for every LNAL program $P$ and state $s$, if VMInvariant holds at $s$ then it holds after one lStep transition, and if TokenParityInvariant holds at $s$ then the token count changes by at most one unit.
background
LNAL is the Logic Native Assembly Language whose virtual machine states carry VMInvariant (state consistency) and TokenParityInvariant (controlled token evolution). The transition function lStep applies the program to a state; the two preservation lemmas guarantee that these invariants survive one step and that token deltas remain unit-bounded when parity holds. The certificate structure bundles these two properties into a single object that can be populated from source text via parsing and staticChecks.
proof idea
verified_any is a one-line wrapper: it constructs the conjunction of the two quantified statements, then applies simpa to discharge each conjunct by rewriting with lStep_preserves_VMInvariant and token_delta_unit. fromSource parses the input, extracts code and PhiIR analysis, runs staticChecks, and returns the resulting certificate record.
why it matters
The structure is the certificate object consumed by lnal_invariants_report, lnal_invariants_report_json and lnal_manifest_json in URCAdapters.LNALReports. It supplies the invariant check that closes the source-to-execution path inside the Recognition framework, supporting claims that LNAL respects the forcing-chain invariants and Recognition Composition Law. It touches the open question of scaling the same certificate pattern to full compiler soundness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.