InventoryOnly.lean

1 import PaperIIIContinuation
2 
3 open Lean Meta Elab Command
4 
5 -- This is an audit program, not a mathematical proof or a new axiom.
6 run_cmd do
7   let env ← getEnv
8   let moduleNames := env.header.moduleNames
9   let ownedModules : Array Name := #[`KomorebiPaperIII.EdgeOperators, `KomorebiPaperIII.EdgeExtensions, `KomorebiPaperIII.Transport, `KomorebiPaperIII.ReversibleConnections, `KomorebiPaperIII.CoordinateNaturality, `KomorebiPaperIII.NonlinearObstructions, `KomorebiPaperIII.HolonomyBlocks, `KomorebiPaperIII.PacketCoordinates, `KomorebiPaperIII.NonlinearPacketCoordinates, `KomorebiPaperIII.PacketDirectSum, `KomorebiPaperIII, `PaperIIIContinuation]
10   -- Compiler-generated partial helpers are separately inventoried, never proof-replayed.
11   let generatedRuntime : Array Name := #[]
12   let mut counts : Array Nat := ownedModules.map (fun _ => 0)
13   let mut total : Nat := 0
14   let mut outside : Nat := 0
15   for (name, info) in env.checked.get.constants.toList do
16     if let some idx := env.getModuleIdxFor? name then
17       let owner := moduleNames[idx.toNat]!
18       for mi in [:ownedModules.size] do
19         if owner == ownedModules[mi]! then
20           total := total + 1
21           counts := counts.modify mi (· + 1)
22           let inNamespace := Name.isPrefixOf `Komorebi name || Name.isPrefixOf `KomorebiVerification name
23           unless inNamespace do outside := outside + 1
24           if info.isUnsafe then throwError "OWNED AUDIT REJECTED unsafe: {name}"
25           if info.isPartial then liftIO <| IO.println s!"PARTIAL_CENSUS {owner} {name}"
26           if generatedRuntime.contains name && !info.isPartial then
27             throwError "OWNED AUDIT REJECTED runtime classification changed: {name}"
28           if !info.isPartial then
29             let dependencies := info.getUsedConstantsAsSet
30             for helper in generatedRuntime do
31               if dependencies.contains helper then
32                 throwError "OWNED AUDIT REJECTED logical runtime-helper dependency: {name} -> {helper}"
33           match info with
34           | .axiomInfo _ => throwError "OWNED AUDIT REJECTED axiom: {name}"
35           | .opaqueInfo _ => throwError "OWNED AUDIT REJECTED opaque: {name}"
36           | _ => pure ()
37           let axioms ← Lean.collectAxioms name
38           for ax in axioms do
39             unless ax == ``propext || ax == ``Classical.choice || ax == ``Quot.sound do
40               throwError "OWNED AUDIT REJECTED dependency {ax}: {name}"
41           let kind := match info with
42             | .thmInfo _ => "theorem"
43             | .defnInfo _ => "definition"
44             | .inductInfo _ => "inductive"
45             | .ctorInfo _ => "constructor"
46             | .recInfo _ => "recursor"
47             | .quotInfo _ => "quotient"
48             | .axiomInfo _ => "axiom"
49             | .opaqueInfo _ => "opaque"
50           let row := Json.mkObj [
51             ("module", toJson owner.toString), ("name", toJson name.toString),
52             ("kind", toJson kind), ("in_project_namespace", toJson inNamespace),
53             ("runtime_only", toJson info.isPartial),
54             ("type_expr", toJson (reprStr info.type)),
55             ("value_expr", toJson (if info.isPartial then (info.value? (allowOpaque := true)).map reprStr else none)),
56             ("level_params", toJson (if info.isPartial then info.levelParams.map Name.toString else [])),
57             ("axioms", toJson (axioms.map Name.toString))]
58           liftIO <| IO.println ("OWNED " ++ row.compress)
59   if total == 0 then throwError "OWNED AUDIT REJECTED empty inventory"
60   for mi in [:ownedModules.size] do
61     let m := ownedModules[mi]!
62     if !(#[`KomorebiPaperIII, `PaperIIIContinuation]).contains m && counts[mi]! == 0 then
63       throwError "OWNED AUDIT REJECTED missing declaration-bearing module: {m}"
64     liftIO <| IO.println s!"OWNED_MODULE {m} {counts[mi]!}"
65   liftIO <| IO.println s!"INVENTORY_ONLY_COMPLETE {total} OUTSIDE_NAMESPACE {outside}"

Back to source controls