source.lean

1 import BadPartial
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 := #[`BadPartial]
10   -- Compiler-generated partial helpers are separately inventoried, never proof-replayed.
11   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 ]
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 && !(generatedRuntime.contains name) then
26             throwError "OWNED AUDIT REJECTED unreviewed partial declaration: {name}"
27           if generatedRuntime.contains name && !info.isPartial then
28             throwError "OWNED AUDIT REJECTED runtime classification changed: {name}"
29           if !info.isPartial then
30             let dependencies := info.getUsedConstantsAsSet
31             for helper in generatedRuntime do
32               if dependencies.contains helper then
33                 throwError "OWNED AUDIT REJECTED logical runtime-helper dependency: {name} -> {helper}"
34           match info with
35           | .axiomInfo _ => throwError "OWNED AUDIT REJECTED axiom: {name}"
36           | .opaqueInfo _ => throwError "OWNED AUDIT REJECTED opaque: {name}"
37           | _ => pure ()
38           let axioms ← Lean.collectAxioms name
39           for ax in axioms do
40             unless ax == ``propext || ax == ``Classical.choice || ax == ``Quot.sound do
41               throwError "OWNED AUDIT REJECTED dependency {ax}: {name}"
42           let kind := match info with
43             | .thmInfo _ => "theorem"
44             | .defnInfo _ => "definition"
45             | .inductInfo _ => "inductive"
46             | .ctorInfo _ => "constructor"
47             | .recInfo _ => "recursor"
48             | .quotInfo _ => "quotient"
49             | .axiomInfo _ => "axiom"
50             | .opaqueInfo _ => "opaque"
51           let row := Json.mkObj [
52             ("module", toJson owner.toString), ("name", toJson name.toString),
53             ("kind", toJson kind), ("in_project_namespace", toJson inNamespace),
54             ("runtime_only", toJson info.isPartial),
55             ("type_expr", toJson (reprStr info.type)),
56             ("value_expr", toJson (if info.isPartial then (info.value? (allowOpaque := true)).map reprStr else none)),
57             ("level_params", toJson (if info.isPartial then info.levelParams.map Name.toString else [])),
58             ("axioms", toJson (axioms.map Name.toString))]
59           liftIO <| IO.println ("OWNED " ++ row.compress)
60   if total == 0 then throwError "OWNED AUDIT REJECTED empty inventory"
61   for mi in [:ownedModules.size] do
62     let m := ownedModules[mi]!
63     if !(#[`KomorebiPaperIII, `PaperIIIContinuation]).contains m && counts[mi]! == 0 then
64       throwError "OWNED AUDIT REJECTED missing declaration-bearing module: {m}"
65     liftIO <| IO.println s!"OWNED_MODULE {m} {counts[mi]!}"
66   liftIO <| IO.println s!"OWNED_AUDIT_PASS {total} OUTSIDE_NAMESPACE {outside}"

Back to source controls