KernelAudit.lean

1 import KomorebiVerification.Basic
2 import KomorebiVerification.ExactCoordinates
3 import KomorebiVerification.FibreRefinement
4 import KomorebiVerification.ResidueProjectors
5 import KomorebiVerification.PaperITransport
6 import KomorebiVerification.PaperIBlockCompletion
7 import KomorebiVerification.SeedRankBasics
8 import KomorebiVerification.SemisimpleSeedRank
9 import KomorebiVerification.FullMatrixCyclicity
10 import KomorebiVerification.PathGraphKrylov
11 import KomorebiVerification.SeedRankOperations
12 import KomorebiVerification.SemisimpleCompletion
13 import KomorebiVerification.SingleOperatorGraph
14 import KomorebiVerification.PacketNaturalityCompletion
15 import KomorebiVerification.TopologicalCompletion
16 import KomorebiVerification.EllipticAlgorithms
17 import Mathlib.Util.AssertNoSorry
18 
19 /-!
20 # Kernel audit and concrete smoke tests
21 
22 Author: Komorebi P.
23 
24 The examples below instantiate the abstract results on four rational
25 coordinates. The declaration list is exactly the unique compiled surface of
26 the versioned theorem map. The final command then fails compilation if any
27 project declaration depends on a nonstandard axiom or is unsafe.
28 -/
29 
30 set_option autoImplicit false
31 
32 namespace Komorebi.Verification
33 
34 open Komorebi.Foundation
35 open Komorebi.Foundation.LinearProjectorFamily
36 open Komorebi.Packet
37 
38 /-- Fine addresses are the four individual coordinates. -/
39 def fineAddress (i : Fin 4) : Fin 4 := i
40 
41 /-- Coarse addresses merge the four coordinates into their parity classes. -/
42 def parityAddress (i : Fin 4) : Fin 2 :=
43   ⟨i.val % 2, Nat.mod_lt _ (by omega)⟩
44 
45 /-- The concrete coordinate masks form a complete orthogonal linear family. -/
46 def fourCoordinateFamily :
47     LinearProjectorFamily ℚ (Fin 4 → ℚ) (Fin 4) :=
48   fibreLinearProjectorFamily (R := ℚ) (M := ℚ) fineAddress
49 
50 /-- Exact recovery holds in the concrete four-coordinate model. -/
51 example (x : Fin 4 → ℚ) :
52     fourCoordinateFamily.rangeSynthesis
53       (fourCoordinateFamily.rangeAnalysis x) = x := by
54   exact fourCoordinateFamily.rangeSynthesis_rangeAnalysis x
55 
56 /-- Every valid tuple of range packets is recovered by analysis after synthesis. -/
57 example (packets : fourCoordinateFamily.PacketSpace) :
58     fourCoordinateFamily.rangeAnalysis
59       (fourCoordinateFamily.rangeSynthesis packets) = packets := by
60   exact fourCoordinateFamily.rangeAnalysis_rangeSynthesis packets
61 
62 /--
63 The independently defined parity mask is exactly the sum of its fine
64 coordinate masks.  This is a concrete `Fin 4 → Fin 2` refinement test.
65 -/
66 theorem parity_refinement (b : Fin 2) (x : Fin 4 → ℚ) :
67     fibreProj parityAddress b x =
68       ∑ c, if parityAddress c = b then fibreProj fineAddress c x else 0 := by
69   simpa [fineAddress] using
70     (fibreProj_refinement fineAddress parityAddress b x)
71 
72 /-- A linear operator is recovered exactly from all sixteen packet blocks. -/
73 example (T : (Fin 4 → ℚ) →ₗ[ℚ] (Fin 4 → ℚ)) (x : Fin 4 → ℚ) :
74     (∑ j, ∑ i,
75       fourCoordinateFamily.proj j (T (fourCoordinateFamily.proj i x))) = T x := by
76   exact transferBlock_reconstruction
77     fourCoordinateFamily fourCoordinateFamily T x
78 
79 end Komorebi.Verification
80 
81 #print axioms Komorebi.FiniteAlgorithms.assembleTransferBlockTable
82 #print axioms Komorebi.FiniteAlgorithms.exactGraphSeedRank
83 #print axioms Komorebi.FiniteAlgorithms.exactGraphSeedRank_isLeast
84 #print axioms Komorebi.FiniteAlgorithms.orbitClosureIter_eq_orbitHull_of_stop
85 #print axioms Komorebi.FiniteAlgorithms.orbitHull_algorithm_terminates_and_correct
86 #print axioms Komorebi.FiniteAlgorithms.transferBlockTable
87 #print axioms Komorebi.FiniteAlgorithms.transferBlock_algorithm_correct
88 #print axioms Komorebi.FiniteAlgorithms.transferGraph_iff_block_ne_zero
89 #print axioms Komorebi.Foundation.LinearProjectorFamily.conjugate
90 #print axioms Komorebi.Foundation.LinearProjectorFamily.exactPacketCoordinates
91 #print axioms Komorebi.Foundation.LinearProjectorFamily.rangeAnalysis_rangeSynthesis
92 #print axioms Komorebi.Foundation.LinearProjectorFamily.rangeSynthesis_rangeAnalysis
93 #print axioms Komorebi.Foundation.conjugate_transferBlock
94 #print axioms Komorebi.Foundation.end_comp_eq_sum_transferBlock_comps
95 #print axioms Komorebi.Foundation.transferBlock_comp_end
96 #print axioms Komorebi.Foundation.transferBlock_comp_linearMap
97 #print axioms Komorebi.Foundation.transferBlock_reconstruction_end
98 #print axioms Komorebi.Foundation.transferBlock_reconstruction_linearMap
99 #print axioms Komorebi.PacketNaturalityCompletion.FullBlocks.blockMulClosed_iff_transitive
100 #print axioms Komorebi.PacketNaturalityCompletion.FullBlocks.end_finrank_eq_packet_sum_eq_square
101 #print axioms Komorebi.PacketNaturalityCompletion.FullBlocks.finrank_eq_sum_packet_finrank
102 #print axioms Komorebi.PacketNaturalityCompletion.FullBlocks.fullBlockAlgEquiv
103 #print axioms Komorebi.PacketNaturalityCompletion.FullBlocks.identity_blocks_supported_iff_reflexive
104 #print axioms Komorebi.PacketNaturalityCompletion.FullBlocks.packetBlockAlgebra_mul_eq_blockMul
105 #print axioms Komorebi.PacketNaturalityCompletion.FullBlocks.restrictBlocks_synthesizeBlocks
106 #print axioms Komorebi.PacketNaturalityCompletion.FullBlocks.synthesizeBlocks_restrictBlocks
107 #print axioms Komorebi.PacketNaturalityCompletion.Packets.eq_iff_projectors_eq
108 #print axioms Komorebi.PacketNaturalityCompletion.Packets.transferBlock_pow_eq_packetPathSum
109 #print axioms Komorebi.PacketNaturalityCompletion.Reachability.algebraicOrbitHull_le_reachable_support
110 #print axioms Komorebi.PacketNaturalityCompletion.Reachability.conjugate_reachableFrom_iff
111 #print axioms Komorebi.PacketNaturalityCompletion.Reachability.conjugate_transferEdge_iff
112 #print axioms Komorebi.PacketNaturalityCompletion.Reachability.unreachable_nonzero_packet_obstruction
113 #print axioms Komorebi.PacketNaturalityCompletion.StrictNaturality.full_transfer_edge_zero_pattern_correspondence
114 #print axioms Komorebi.PacketNaturalityCompletion.StrictNaturality.generatedHull_natural
115 #print axioms Komorebi.PacketNaturalityCompletion.StrictNaturality.strict_naturality_package
116 #print axioms Komorebi.PacketNaturalityCompletion.StrictNaturality.strict_seedRank_eq_of_bijective
117 #print axioms Komorebi.PacketNaturalityCompletion.StrictNaturality.strict_seedRank_le
118 #print axioms Komorebi.PacketNaturalityCompletion.TypedQuiver.typed_reachability_certificate
119 #print axioms Komorebi.SeedRankBasics.generates_singleton_iff_surjective
120 #print axioms Komorebi.SeedRankBasics.multiSeedQuotientEquiv
121 #print axioms Komorebi.SeedRankBasics.multiSeedQuotientEquivRange
122 #print axioms Komorebi.SeedRankBasics.multiSeedQuotientEquivRange_apply_mk
123 #print axioms Komorebi.SeedRankBasics.oneSeedQuotientEquivRange
124 #print axioms Komorebi.SeedRankBasics.oneSeedQuotientEquivRange_apply_mk
125 #print axioms Komorebi.SeedRankOperations.seedFinrank_isLeast_free_surjection
126 #print axioms Komorebi.SeedRankOperations.cyclic_iff_seedRank_eq_one
127 #print axioms Komorebi.SeedRankOperations.seedRank_le_of_surjective_semilinear
128 #print axioms Komorebi.SeedRankOperations.seedRank_imageAlgebra_eq
129 #print axioms Komorebi.SeedRankOperations.seedRank_prod_le_add
130 #print axioms Komorebi.SeedRankOperations.seedRank_prod_productAlgebra
131 #print axioms Komorebi.SeedRankOperations.seedRank_tensorProduct_le_mul
132 #print axioms Komorebi.SeedRankOperations.finrank_le_seedRank_of_scalar_quotient
133 #print axioms Komorebi.SeedRankOperations.tensorOperator_smul_tmul
134 #print axioms Komorebi.SemisimpleCompletion.fullMatrix_every_nonzero_vector_generates
135 #print axioms Komorebi.SemisimpleCompletion.fullMatrix_seedRank_eq_one
136 #print axioms Komorebi.SemisimpleCompletion.multiplicity_obstruction
137 #print axioms Komorebi.SemisimpleCompletion.multiplicity_seedRank_formula
138 #print axioms Komorebi.SemisimpleCompletion.semisimple_seedRank_eq_maxCeilDiv_of_equivalences
139 #print axioms Komorebi.SemisimpleCompletion.splitProduct_seedRank_eq_maxCeilDiv
140 #print axioms Komorebi.SingleOperatorGraph.complex_cycle_seedNumber_isLeast_two
141 #print axioms Komorebi.SingleOperatorGraph.cyclic_matrix_criterion_of_primary_decomposition
142 #print axioms Komorebi.SingleOperatorGraph.cyclic_matrix_four_way_iff_of_primary_decomposition
143 #print axioms Komorebi.SingleOperatorGraph.graph_seedNumber_eq_max_eigenspace_multiplicity
144 #print axioms Komorebi.SingleOperatorGraph.graph_seedNumber_eq_max_eigenspace_multiplicity_of_distinct
145 #print axioms Komorebi.SingleOperatorGraph.operatorAlgebra_seedFinrank_eq_of_seedNumber_isLeast
146 #print axioms Komorebi.SingleOperatorGraph.operatorAlgebra_seedRank_eq_of_seedNumber_isLeast
147 #print axioms Komorebi.SingleOperatorGraph.path_endpoint_seedNumber_isLeast_one
148 #print axioms Komorebi.SingleOperatorGraph.singleOperator_operatorAlgebra_seedRanks_eq_of_primary_decomposition
149 #print axioms Komorebi.SingleOperatorGraph.singleOperator_seedNumber_isLeast_of_primary_decomposition
150 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.BilateralShiftRepresentation.concretePower_apply
151 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.adjoint_transferBlock
152 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.closure_le_ker_of_le_ker
153 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.completionEquivOfIsometryDense
154 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.completionEquivOfIsometryDense_intertwines
155 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.completionEquivOfIsometryDense_unique
156 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.concreteBilateralShift_seedCardinality_isLeast
157 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.concreteBilateralShift_topologicallyCyclic
158 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.dense_operatorHull_image
159 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.idempotentRange_eq_closure_map
160 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.map_packetRange_eq
161 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.packetEquiv
162 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.packetRange_eq_closure_map
163 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.topological_packet_isomorphism
164 #print axioms KomorebiVerification.TopologicalCompletion.BoundedProjectorFamily.topological_reachability_obstruction
165 
166 /-! ## Fail-closed project audit -/
167 
168 open Lean Meta Elab Command
169 
170 /-
171 Audit every imported declaration owned by either project namespace. This
172 turns the trust boundary into a compilation gate instead of a review of
173 selected diagnostic output.
174 -/
175 run_cmd do
176   let env ← getEnv
177   let mut audited : Nat := 0
178   for (name, info) in env.checked.get.constants.toList do
179     if Name.isPrefixOf `Komorebi name || Name.isPrefixOf `KomorebiVerification name then
180       audited := audited + 1
181       if info.isUnsafe then
182         throwError "unsafe project declaration: {name}"
183       match info with
184       | .axiomInfo _ =>
185           throwError "project axiom declaration: {name}"
186       | .opaqueInfo _ =>
187           throwError "opaque project declaration: {name}"
188       | _ => pure ()
189       let axioms ← Lean.collectAxioms name
190       for axiomName in axioms do
191         unless axiomName == ``propext || axiomName == ``Classical.choice ||
192             axiomName == ``Quot.sound do
193           throwError "unexpected axiom {axiomName} in project declaration {name}"
194   if audited == 0 then
195     throwError "kernel audit found no project declarations"
196   logInfo m!"FAIL-CLOSED KERNEL AUDIT PASS: {audited} project declarations; allowed axioms only: propext, Classical.choice, Quot.sound"

Back to source controls