def
definition
compiler_checks_report_json
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.URCAdapters.LNALReports on GitHub at line 85.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
82 let cert := LNALInvariantsCert.fromSource src
83 mkJson cert.ok cert.errors
84
85def compiler_checks_report_json (src : String) : String :=
86 let cert := CompilerChecksCert.fromSource src
87 mkJson cert.ok cert.errors
88
89def opcode_soundness_report_json (src : String) : String :=
90 let _ := OpcodeSoundnessCert.fromSource src
91 -- Parser coverage is structural; treat as ok with empty errors
92 mkJson true []
93
94def schedule_neutrality_report_json (src : String) : String :=
95 let cert := ScheduleNeutralityCert.fromSource src
96 mkJson cert.ok cert.errors
97
98def cost_ceiling_report_json (src : String) : String :=
99 let cert := CostCeilingCert.fromSource src
100 mkJson cert.ok cert.errors
101
102def su3_mask_report_json (src : String) : String :=
103 let _ := SU3MaskCert.fromSource src
104 -- SU3 mask is step-preservation; treat as ok with empty errors
105 mkJson true []
106
107def jmonotone_report_json (src : String) : String :=
108 let cert := JMonotoneCert.fromSource src
109 let violationSnapshot :=
110 match cert.firstViolation? with
111 | some idx =>
112 let before := (cert.budgets.get? idx).getD 0
113 let after := (cert.budgets.get? (idx + 1)).getD before
114 Lean.Json.obj [
115 ("index", Lean.Json.num idx),