CompilerChecksCert
plain-language theorem explainer
CompilerChecksCert defines a certificate structure with a boolean success flag and error list for static validation of LNAL source programs. Reports in the LNAL adapter layer cite it to emit pass/fail summaries ahead of invariant analysis. The definition supplies a verified predicate and a fromSource constructor that runs parsing followed by staticChecks on extracted code and analysis results.
Claim. A compiler-check certificate $C$ is a pair $(ok, errors)$ with $ok : Bool$ and $errors : List String$, equipped with the predicate $verified(C) := (ok = true)$ and the constructor $fromSource(s)$ that parses source string $s$, substitutes empty analysis on failure, applies static checks to the resulting code and packets, and returns the assembled certificate.
background
LNAL expresses Recognition Science computations; its invariants certificate bundles VM preservation with token δ-unit bounds. CompilerChecksCert is a sibling structure focused on static compiler validation, identical in shape to the invariants certificate for the present implementation. It draws on the LNAL parser and staticChecks to confirm opcode sets and analysis outputs before deeper checks.
proof idea
The structure is declared with two fields and derives Repr. verified is a direct equality on the ok field. fromSource matches the parseProgramFull result, substitutes empty PhiAnalysis and PacketAnalysis on error, extracts code, phi, and packets on success, invokes staticChecks, and constructs the certificate from the returned report.
why it matters
The certificate is consumed by compiler_checks_report, compiler_checks_report_json, and lnal_manifest_json in LNALReports to produce outputs for the certificate engine v2. It sits in the URC generator layer that prepares LNAL programs for the Recognition framework, feeding the aggregate manifest that records ΔJ bars and falsifier flags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.