structure
definition
def or abbrev
CompilerChecksCert
show as:
view Lean formalization →
formal statement (Lean)
59structure CompilerChecksCert where
60 ok : Bool
61 errors : List String := []
proof body
Definition body.
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). -/