source.lean

1 import LeanChecker
2 
3 /-!
4 Audit instrumentation, not a mathematical proof module. Rebuild the kernel
5 constant closure with no production module in the starting environment.
6 All unsafe declarations, unreviewed partial implementations and all upstream name overlaps are rejected. Fourteen exact inherited code-generation helpers are inventoried separately and cannot be used by a logical production declaration.
7 Uses the pinned official Lean kernel; not an independent proof assistant.
8 -/
9 open Lean
10 
11 unsafe def replayPaperIII : IO Unit := do
12   let modules : Array Name := #[
13     `KomorebiPaperIII.EdgeOperators, `KomorebiPaperIII.EdgeExtensions,
14     `KomorebiPaperIII.Transport, `KomorebiPaperIII.ReversibleConnections,
15     `KomorebiPaperIII.CoordinateNaturality, `KomorebiPaperIII.NonlinearObstructions,
16     `KomorebiPaperIII.HolonomyBlocks, `KomorebiPaperIII.PacketCoordinates,
17     `KomorebiPaperIII.NonlinearPacketCoordinates, `KomorebiPaperIII.PacketDirectSum, `KomorebiPaperIII.MultilinearPacketJets, `KomorebiPaperIII.BoundedPacketJetNorm,
18     `KomorebiPaperIII, `PaperIIIContinuation]
19   let generatedRuntime : Array Name := #[ `Komorebi.PaperIII.EdgeOperators.heterogeneousPathSum._unsafe_rec, `Komorebi.PaperIII.NonlinearObstructions.OperationTree.eval._unsafe_rec, `Komorebi.PaperIII.Transport.ReversibleConnection.pathTransport._unsafe_rec, `Komorebi.PaperIII.Transport.pathEndpoint._unsafe_rec, `Komorebi.PaperIII.EdgeOperators.SupportedPath._unsafe_rec, `Komorebi.PaperIII.Transport.exactPathTransport._unsafe_rec, `Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.terminalTarget._unsafe_rec, `Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp._unsafe_rec, `Komorebi.PaperIII.EdgeOperators.heterogeneousProduct._unsafe_rec, `Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.Composable._unsafe_rec, `Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordExpansion._unsafe_rec, `Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.reverseCoefficient._unsafe_rec, `Komorebi.PaperIII.NonlinearObstructions.OperationTree.inputs._unsafe_rec, `Komorebi.PaperIII.Transport.ReversibleConnection.indexedPathTransport._unsafe_rec ]
20   let mut upstream : Array Import := #[]
21   let mut constants : Std.HashMap Name ConstantInfo := {}
22   let mut owners : Std.HashMap Name Name := {}
23   let mut heldRegions : Array CompactedRegion := #[]
24   for module in modules do
25     let mFile ← findOLean module
26     let mut files := #[mFile]
27     let server := OLeanLevel.server.adjustFileName mFile
28     if ← server.pathExists then
29       files := files.push server
30       let priv := OLeanLevel.private.adjustFileName mFile
31       if ← priv.pathExists then files := files.push priv
32     let parts ← readModuleDataParts files
33     for part in parts do heldRegions := heldRegions.push part.2
34     let some first := parts[0]? | throw <| IO.userError s!"No data for {module}"
35     for imp in first.1.imports do
36       unless modules.contains imp.module do
37         unless upstream.any (fun j => j.module == imp.module) do
38           upstream := upstream.push { imp with importAll := true }
39     let some last := parts[parts.size - 1]? | throw <| IO.userError "No private module data"
40     let data := last.1
41     for name in data.constNames, ci in data.constants do
42       if ci.isUnsafe then
43         throw <| IO.userError s!"Unsafe production declaration {name}"
44       if ci.isPartial then
45         unless generatedRuntime.contains name do
46           throw <| IO.userError s!"Unreviewed partial production declaration {name}"
47         IO.println s!"REPLAY_EXCLUDED_GENERATED_RUNTIME {module} {name}"
48         continue
49       if generatedRuntime.contains name then
50         throw <| IO.userError s!"Generated runtime classification changed {name}"
51       for helper in generatedRuntime do
52         if ci.getUsedConstantsAsSet.contains helper then
53           throw <| IO.userError s!"Logical dependency on generated runtime: {name} -> {helper}"
54       if let some old := constants[name]? then
55         match old, ci with
56         | .thmInfo a, .thmInfo b =>
57           unless a.type == b.type && a.levelParams == b.levelParams && a.all == b.all && a.value == b.value do
58             throw <| IO.userError s!"Incompatible duplicate theorem {name}"
59           IO.println s!"REPLAY_IDENTICAL_THEOREM_COPY {module} {name}"
60         | _, _ => throw <| IO.userError s!"Non-theorem duplicate {name}"
61       else
62         constants := constants.insert name ci
63         owners := owners.insert name module
64     IO.println s!"REPLAY_MODULE {module} {data.constNames.size}"
65   let (_, state) ← importModulesCore upstream |>.run
66   let env ← finalizeImport state upstream {} 0 false false (isModule := true)
67   for module in modules do
68     if env.header.moduleNames.contains module then
69       throw <| IO.userError s!"Production already present in starting environment: {module}"
70   for (name, _) in constants.toList do
71     if (env.toKernelEnv.find? name).isSome then
72       throw <| IO.userError s!"Unreviewed upstream name overlap: {name}"
73   IO.println s!"REPLAY_UPSTREAM_ONLY_PASS {upstream.size} OVERLAPS 0"
74   if (← IO.getEnv "KOMOREBI_REPLAY_CORRUPT") == some "1" then
75     let name := `PaperIIIReplayControl.falseEquality
76     let type := mkApp3 (mkConst ``Eq [Level.succ Level.zero]) (mkConst ``Nat) (mkNatLit 0) (mkNatLit 1)
77     let value := mkApp2 (mkConst ``Eq.refl [Level.succ Level.zero]) (mkConst ``Nat) (mkNatLit 0)
78     constants := constants.insert name (.thmInfo { name, levelParams := [], type, value })
79     owners := owners.insert name `PaperIIIReplayControl
80     IO.println "REPLAY_CORRUPT_CONTROL_INJECTED"
81   let result ← env.toKernelEnv.replay constants
82   for (name, _) in constants.toList do
83     unless (result.find? name).isSome do
84       throw <| IO.userError s!"Kernel did not produce {name}"
85     IO.println ("REPLAY_CHECKED " ++ (Json.mkObj [
86       ("module", toJson (owners[name]!).toString), ("name", toJson name.toString)]).compress)
87   IO.println s!"REPLAY_CLOSURE_PASS MODULES {modules.size} CONSTANTS {constants.size} REGIONS {heldRegions.size}"
88   env.freeRegions
89 
90 #eval replayPaperIII

Back to source controls