def
definition
opcode_soundness_report_json
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.URCAdapters.LNALReports on GitHub at line 89.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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),
116 ("window", Lean.Json.num (idx / 8)),
117 ("budget_before", Lean.Json.num before),
118 ("budget_after", Lean.Json.num after)
119 ]