structure
definition
CompilerChecksCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
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