structure
definition
CompilerChecksCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.URCGenerators.LNALCerts on GitHub at line 59.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
56 { ok := rep.ok, errors := rep.errors }
57
58/-- Certificate stub for compiler checks (identical to invariants for now). -/
59structure CompilerChecksCert where
60 ok : Bool
61 errors : List String := []
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). -/
83structure OpcodeSoundnessCert where deriving Repr
84
85/-- Parser covers all VM opcodes by name. -/
86@[simp] def OpcodeSoundnessCert.verified (_c : OpcodeSoundnessCert) : Prop :=
87 ∀ (op : IndisputableMonolith.LNAL.Opcode),
88 ∃ s : String, IndisputableMonolith.LNAL.parseOpcode s = some op
89