def
definition
opcode_soundness_report
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 24.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
21 if cert.ok then "OK: Compiler static checks pass"
22 else s!"FAIL: {String.intercalate "; " cert.errors}"
23
24def opcode_soundness_report (src : String) : String :=
25 let cert := OpcodeSoundnessCert.fromSource src
26 if cert.ok then "OK: Opcode set sound (parser accepted only LNAL opcodes)"
27 else s!"FAIL: {String.intercalate "; " cert.errors}"
28
29def schedule_neutrality_report (src : String) : String :=
30 let cert := ScheduleNeutralityCert.fromSource src
31 if cert.ok then "OK: Schedule neutrality checks pass (BALANCE/8, VECTOR_EQ/1024, FLIP present)"
32 else s!"FAIL: {String.intercalate "; " cert.errors}"
33
34def cost_ceiling_report (src : String) : String :=
35 let cert := CostCeilingCert.fromSource src
36 if cert.ok then "OK: Cost ceiling respected (|net GIVE−REGIVE| ≤ 4)"
37 else s!"FAIL: {String.intercalate "; " cert.errors}"
38
39def su3_mask_report (src : String) : String :=
40 let cert := SU3MaskCert.fromSource src
41 if cert.ok then "OK: SU(3) braid mask (placeholder)"
42 else s!"FAIL: {String.intercalate "; " cert.errors}"
43
44def previewNatArray (arr : Array Nat) (limit : Nat := 4) : String :=
45 let previewVals := (arr.toList.take limit).map (fun n => toString n)
46 let body := String.intercalate ", " previewVals
47 if previewVals.isEmpty then "[]"
48 else
49 let ellipsis := if arr.size > previewVals.length then ", …" else ""
50 "[" ++ body ++ ellipsis ++ "]"
51
52def jmonotone_report (src : String) : String :=
53 let cert := JMonotoneCert.fromSource src
54 if cert.ok then