Skip to content

Reduce Erdos97ConvexOctagon peak compiler memory #717

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Vilin97 wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Reduce Erdos97ConvexOctagon peak compiler memory #717

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
61 changes: 60 additions & 1 deletion LeanPool/Erdos97ConvexOctagon/CoveragePairRowIndexMaskSoundness.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,13 +18,72 @@ import Mathlib.Tactic.NormNum.GCD

namespace Erdos97Octagon.RawIncidence

-- Bound each kernel reduction cache to one centre of the finite table.
private theorem pairRowIndexMasks_bit_centre_0 :
∀ (pairIndex : Fin 64) (rowIndex : Fin 35),
bitSetB ((pairRowIndexMasks.getD 0 #[]).getD pairIndex.val 0) rowIndex.val =
bitSetB (searchRowChoiceAt 0 rowIndex).pairMask pairIndex.val := by
decide +kernel

private theorem pairRowIndexMasks_bit_centre_1 :
∀ (pairIndex : Fin 64) (rowIndex : Fin 35),
bitSetB ((pairRowIndexMasks.getD 1 #[]).getD pairIndex.val 0) rowIndex.val =
bitSetB (searchRowChoiceAt 1 rowIndex).pairMask pairIndex.val := by
decide +kernel

private theorem pairRowIndexMasks_bit_centre_2 :
∀ (pairIndex : Fin 64) (rowIndex : Fin 35),
bitSetB ((pairRowIndexMasks.getD 2 #[]).getD pairIndex.val 0) rowIndex.val =
bitSetB (searchRowChoiceAt 2 rowIndex).pairMask pairIndex.val := by
decide +kernel

private theorem pairRowIndexMasks_bit_centre_3 :
∀ (pairIndex : Fin 64) (rowIndex : Fin 35),
bitSetB ((pairRowIndexMasks.getD 3 #[]).getD pairIndex.val 0) rowIndex.val =
bitSetB (searchRowChoiceAt 3 rowIndex).pairMask pairIndex.val := by
decide +kernel

private theorem pairRowIndexMasks_bit_centre_4 :
∀ (pairIndex : Fin 64) (rowIndex : Fin 35),
bitSetB ((pairRowIndexMasks.getD 4 #[]).getD pairIndex.val 0) rowIndex.val =
bitSetB (searchRowChoiceAt 4 rowIndex).pairMask pairIndex.val := by
decide +kernel

private theorem pairRowIndexMasks_bit_centre_5 :
∀ (pairIndex : Fin 64) (rowIndex : Fin 35),
bitSetB ((pairRowIndexMasks.getD 5 #[]).getD pairIndex.val 0) rowIndex.val =
bitSetB (searchRowChoiceAt 5 rowIndex).pairMask pairIndex.val := by
decide +kernel

private theorem pairRowIndexMasks_bit_centre_6 :
∀ (pairIndex : Fin 64) (rowIndex : Fin 35),
bitSetB ((pairRowIndexMasks.getD 6 #[]).getD pairIndex.val 0) rowIndex.val =
bitSetB (searchRowChoiceAt 6 rowIndex).pairMask pairIndex.val := by
decide +kernel

private theorem pairRowIndexMasks_bit_centre_7 :
∀ (pairIndex : Fin 64) (rowIndex : Fin 35),
bitSetB ((pairRowIndexMasks.getD 7 #[]).getD pairIndex.val 0) rowIndex.val =
bitSetB (searchRowChoiceAt 7 rowIndex).pairMask pairIndex.val := by
decide +kernel

/-- The transposed pair table records exactly which row choices contain each pair bit. -/
theorem pairRowIndexMasks_bit
(centre : Vertex) (pairIndex : Fin 64) (rowIndex : Fin 35) :
bitSetB ((pairRowIndexMasks.getD centre.val #[]).getD pairIndex.val 0)
rowIndex.val =
bitSetB (searchRowChoiceAt centre rowIndex).pairMask pairIndex.val := by
revert centre pairIndex rowIndex
decide +kernel
as_aux_lemma =>
intro centre
fin_cases centre
· exact pairRowIndexMasks_bit_centre_0
· exact pairRowIndexMasks_bit_centre_1
· exact pairRowIndexMasks_bit_centre_2
· exact pairRowIndexMasks_bit_centre_3
· exact pairRowIndexMasks_bit_centre_4
· exact pairRowIndexMasks_bit_centre_5
· exact pairRowIndexMasks_bit_centre_6
· exact pairRowIndexMasks_bit_centre_7

end Erdos97Octagon.RawIncidence
122 changes: 120 additions & 2 deletions LeanPool/Erdos97ConvexOctagon/CoverageSearchRowChoiceSoundness.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,13 +44,72 @@ theorem searchRowChoiceAt_mem (centre : Vertex) (index : Fin 35) :
rw [hequal]
exact Array.getElem_mem hindex

-- Check each centre separately to keep the kernel reduction caches bounded.
private theorem searchRowChoices_complete_centre_0 :
(rowOptions 0).reverse =
List.ofFn (fun index : Fin 35 =>
packedRow (searchRowChoiceAt 0 index).rowMask) := by
decide +kernel

private theorem searchRowChoices_complete_centre_1 :
(rowOptions 1).reverse =
List.ofFn (fun index : Fin 35 =>
packedRow (searchRowChoiceAt 1 index).rowMask) := by
decide +kernel

private theorem searchRowChoices_complete_centre_2 :
(rowOptions 2).reverse =
List.ofFn (fun index : Fin 35 =>
packedRow (searchRowChoiceAt 2 index).rowMask) := by
decide +kernel

private theorem searchRowChoices_complete_centre_3 :
(rowOptions 3).reverse =
List.ofFn (fun index : Fin 35 =>
packedRow (searchRowChoiceAt 3 index).rowMask) := by
decide +kernel

private theorem searchRowChoices_complete_centre_4 :
(rowOptions 4).reverse =
List.ofFn (fun index : Fin 35 =>
packedRow (searchRowChoiceAt 4 index).rowMask) := by
decide +kernel

private theorem searchRowChoices_complete_centre_5 :
(rowOptions 5).reverse =
List.ofFn (fun index : Fin 35 =>
packedRow (searchRowChoiceAt 5 index).rowMask) := by
decide +kernel

private theorem searchRowChoices_complete_centre_6 :
(rowOptions 6).reverse =
List.ofFn (fun index : Fin 35 =>
packedRow (searchRowChoiceAt 6 index).rowMask) := by
decide +kernel

private theorem searchRowChoices_complete_centre_7 :
(rowOptions 7).reverse =
List.ofFn (fun index : Fin 35 =>
packedRow (searchRowChoiceAt 7 index).rowMask) := by
decide +kernel

/-- The generated table is the complete legal-row enumeration, in search order. -/
theorem searchRowChoices_complete (centre : Vertex) :
(rowOptions centre).reverse =
List.ofFn (fun index : Fin 35 =>
packedRow (searchRowChoiceAt centre index).rowMask) := by
revert centre
decide +kernel
as_aux_lemma =>
intro centre
fin_cases centre
· exact searchRowChoices_complete_centre_0
· exact searchRowChoices_complete_centre_1
· exact searchRowChoices_complete_centre_2
· exact searchRowChoices_complete_centre_3
· exact searchRowChoices_complete_centre_4
· exact searchRowChoices_complete_centre_5
· exact searchRowChoices_complete_centre_6
· exact searchRowChoices_complete_centre_7

/-- Every mathematical incidence row occurs at one lightweight search index. -/
theorem exists_searchRowChoiceIndex (Q : OctagonIncidence) (centre : Vertex) :
Expand All @@ -63,12 +122,71 @@ theorem exists_searchRowChoiceIndex (Q : OctagonIncidence) (centre : Vertex) :
obtain ⟨index, hrow⟩ := hrow
exact ⟨index, hrow.symm⟩

-- Reuse the same bounded checks for the independently generated pair masks.
private theorem searchRowChoiceAt_pairMask_centre_0 (index : Fin 35) :
(searchRowChoiceAt 0 index).pairMask =
rowPairMask (searchRowChoiceAt 0 index).rowMask := by
revert index
decide +kernel

private theorem searchRowChoiceAt_pairMask_centre_1 (index : Fin 35) :
(searchRowChoiceAt 1 index).pairMask =
rowPairMask (searchRowChoiceAt 1 index).rowMask := by
revert index
decide +kernel

private theorem searchRowChoiceAt_pairMask_centre_2 (index : Fin 35) :
(searchRowChoiceAt 2 index).pairMask =
rowPairMask (searchRowChoiceAt 2 index).rowMask := by
revert index
decide +kernel

private theorem searchRowChoiceAt_pairMask_centre_3 (index : Fin 35) :
(searchRowChoiceAt 3 index).pairMask =
rowPairMask (searchRowChoiceAt 3 index).rowMask := by
revert index
decide +kernel

private theorem searchRowChoiceAt_pairMask_centre_4 (index : Fin 35) :
(searchRowChoiceAt 4 index).pairMask =
rowPairMask (searchRowChoiceAt 4 index).rowMask := by
revert index
decide +kernel

private theorem searchRowChoiceAt_pairMask_centre_5 (index : Fin 35) :
(searchRowChoiceAt 5 index).pairMask =
rowPairMask (searchRowChoiceAt 5 index).rowMask := by
revert index
decide +kernel

private theorem searchRowChoiceAt_pairMask_centre_6 (index : Fin 35) :
(searchRowChoiceAt 6 index).pairMask =
rowPairMask (searchRowChoiceAt 6 index).rowMask := by
revert index
decide +kernel

private theorem searchRowChoiceAt_pairMask_centre_7 (index : Fin 35) :
(searchRowChoiceAt 7 index).pairMask =
rowPairMask (searchRowChoiceAt 7 index).rowMask := by
revert index
decide +kernel

/-- Every stored unordered-pair mask is exactly computed from its row mask. -/
theorem searchRowChoiceAt_pairMask (centre : Vertex) (index : Fin 35) :
(searchRowChoiceAt centre index).pairMask =
rowPairMask (searchRowChoiceAt centre index).rowMask := by
revert centre index
decide +kernel
as_aux_lemma =>
intro centre
fin_cases centre
· exact searchRowChoiceAt_pairMask_centre_0
· exact searchRowChoiceAt_pairMask_centre_1
· exact searchRowChoiceAt_pairMask_centre_2
· exact searchRowChoiceAt_pairMask_centre_3
· exact searchRowChoiceAt_pairMask_centre_4
· exact searchRowChoiceAt_pairMask_centre_5
· exact searchRowChoiceAt_pairMask_centre_6
· exact searchRowChoiceAt_pairMask_centre_7

/-- The centre-two row table uses exactly the public fixed-branch ordering. -/
theorem searchRowChoiceAt_two_mask (index : Fin 35) :
Expand Down
Loading