compiler_checks_report
plain-language theorem explainer
compiler_checks_report defines a function that maps an LNAL source string to a human-readable status string. Developers building LNAL certification pipelines cite it when assembling report adapters. The body constructs a CompilerChecksCert via fromSource and branches on its ok flag to emit either a success message or a semicolon-joined error list.
Claim. Let $f(s)$ denote the map that returns the string ``OK: Compiler static checks pass'' whenever the certificate obtained from source string $s$ satisfies verified, and otherwise returns the string ``FAIL:'' followed by the semicolon-separated concatenation of the certificate's error list.
background
The LNALReports module supplies adapter definitions that convert LNAL compiler artifacts into string reports. It imports LNAL.Compiler and LNAL.JBudget together with the LNALCerts generator. The sole dependency is CompilerChecksCert, a structure whose fields are a Bool ok flag and a List String of errors, equipped with the predicate verified(c) defined by c.ok = true. This structure is described as a certificate stub identical in form to the invariants certificate.
proof idea
The definition is a direct term that first binds the result of CompilerChecksCert.fromSource applied to the input string. It then evaluates an if-then-else on the ok field of that certificate: the true branch yields the fixed success string while the false branch interpolates the errors list via String.intercalate.
why it matters
The definition supplies the string formatter for compiler static checks inside the URCAdapters layer. It completes the family of report generators that includes lnal_invariants_report and cost_ceiling_report, allowing uniform textual output for LNAL verification steps. No downstream theorems yet reference it, but it supports the framework's requirement that compiler invariants be exposed through readable certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.