CompilerChecksCert
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not execute the program or perform runtime VM simulation.
- Does not establish semantic preservation or full invariant proofs.
- Does not compute J-cost, defect distances, or phi-ladder masses.
- Does not validate token δ-unit bounds (handled by LNALInvariantsCert).
formal statement (Lean)
59structure CompilerChecksCert where
60 ok : Bool
61 errors : List String := []
proof body
Definition body.
62deriving Repr
63
64@[simp] def CompilerChecksCert.verified (c : CompilerChecksCert) : Prop := c.ok = true
65
66def CompilerChecksCert.fromSource (src : String) : CompilerChecksCert :=
67 let parsed := parseProgramFull src
68 let emptyPhi : PhiIR.PhiAnalysis := { literals := #[], errors := #[], duplicateNames := [] }
69 let emptyPackets : PhiIR.PacketAnalysis := {}
70 let code := match parsed with
71 | .ok out => out.code
72 | .error _ => #[]
73 let phi := match parsed with
74 | .ok out => out.phi
75 | .error _ => emptyPhi
76 let packets := match parsed with
77 | .ok out => out.packets
78 | .error _ => emptyPackets
79 let rep := staticChecks code phi packets
80 { ok := rep.ok, errors := rep.errors }
81
82/-- Opcode soundness certificate (parsing validates opcode set). -/