fix: centralise the module-system Array/Vector kernel-reduction workarounds

.gitignore

@@ -10,3 +10,6 @@ conformance-failures/*.json
 .pod/
 sessions/
 _out/
+
+# Accidentally-committed scratch benchmark tree; see PR #9044.
+/scratch-mvpoly-bench/

HexBasic.lean

@@ -6,7 +6,10 @@ Authors: Kim Morrison
 
 module
 
+public import HexBasic.ArrayDecEq
 public import HexBasic.Fold
+public import HexBasic.ModuleBoundaryTests
+public import HexBasic.OfFn
 public import HexBasic.ListShim
 public import HexBasic.Vector.Modify
 
@@ -17,5 +20,7 @@ public section
 general-purpose helpers that clearly belong in the standard library and are
 reproduced here only until they migrate up to lean4. It provides the shared
 `List.foldl` algebra (`HexBasic.Fold`), the `Batteries` list lemmas reproduced
-in `HexBasic.ListShim`, and the `Vector.modify` update helper.
+in `HexBasic.ListShim`, the `Vector.modify` update helper, and
+kernel-reducible `Array`/`Vector` equality (`HexBasic.ArrayDecEq`) and
+`ofFn` (`HexBasic.OfFn`).
 -/

HexBasic/ArrayDecEq.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import Std
+
+public section
+
+/-!
+Kernel-reducible `DecidableEq` for `Array` and `Vector`.
+
+Three exposure gaps in core stop `decide` / `rfl` reducing over these types
+across a module boundary. In each case an exposed definition delegates to a
+plain `def` whose body is unavailable downstream, so reduction stalls:
+
+* `Array.instDecidableEq` delegates its nonempty/nonempty case to
+  `Array.instDecidableEqImpl`;
+* every `deriving DecidableEq` instance delegates to a generated `decEq`,
+  which is how `Vector` gets its instance;
+* `Array.ofFn` delegates to its `ofFn.go` auxiliary.
+
+The instances below route through `List` equality, which is fully exposed, and
+take priority over the core ones. They are `scoped`, so they apply only inside
+`namespace Hex` or after `open scoped Hex`, and never leak into the released
+libraries that depend on `hex-basic` or into their consumers. A module that
+forgets to activate them gets a stuck `decide`, which is loud. `List` is the wrong shape for compiled code,
+where `Array.toList` is an `O(n)` conversion that allocates both lists in full
+before comparison begins and gives up early exit, so each carries a `@[csimp]`
+redirect back to the core instance. The `List` route is then paid only in the
+kernel, which is where it is needed.
+
+**Delete this file** once
+[leanprover/lean4#14270](https://github.com/leanprover/lean4/pull/14270) lands
+and the toolchain is bumped past it. `HexBasic.OfFn` covers the third gap.
+-/
+
+namespace Hex
+
+/-- `DecidableEq (Array α)` that reduces in the kernel under the module system,
+routing through the fully exposed `List` equality. -/
+scoped instance (priority := 1100) instDecidableEqArray
+    {α : Type u} [DecidableEq α] : DecidableEq (Array α) := fun a b =>
+  match h : decEq a.toList b.toList with
+  | isTrue ht => isTrue (by cases a; cases b; exact congrArg Array.mk ht)
+  | isFalse hf => isFalse (by intro hab; exact hf (congrArg Array.toList hab))
+
+/-- `DecidableEq (Vector α n)` that reduces in the kernel under the module
+system. `Vector`'s core instance is derived, and derived instances are opaque
+across a module boundary. -/
+scoped instance (priority := 1100) instDecidableEqVector
+    {α : Type u} {n : Nat} [DecidableEq α] : DecidableEq (Vector α n) := fun a b =>
+  match h : decEq a.toArray.toList b.toArray.toList with
+  | isTrue ht => isTrue (by
+      cases a with | mk ba ha => cases b with | mk bb hb =>
+      have hba : ba = bb := by cases ba; cases bb; exact congrArg Array.mk ht
+      subst hba; rfl)
+  | isFalse hf => isFalse (by intro hab; subst hab; exact hf rfl)
+
+/-- Compiled code uses the core `Array` decider, which compares in place. The
+`List` route exists only so that the kernel can reduce it. `DecidableEq` is a
+subsingleton, so the two agree. -/
+@[csimp] theorem instDecidableEqArray_eq :
+    @instDecidableEqArray = @_root_.Array.instDecidableEq := by
+  funext α _ a b; exact Subsingleton.elim _ _
+
+/-- As `instDecidableEqArray_eq`. -/
+@[csimp] theorem instDecidableEqVector_eq :
+    @instDecidableEqVector = @_root_.instDecidableEqVector := by
+  funext α n _ a b; exact Subsingleton.elim _ _
+
+end Hex

HexBasic/ModuleBoundaryTests.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import HexBasic.ArrayDecEq
+public import HexBasic.OfFn
+
+open scoped Hex   -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq
+
+public section
+
+/-!
+Regression tests for the three module-system exposure gaps worked around by
+`HexBasic.ArrayDecEq` and `HexBasic.OfFn`.
+
+These have to live in a *separate module* from the definitions they exercise:
+the defect is that a callee's body is unavailable across a module boundary, so
+a same-module test passes whether or not the workaround is present and proves
+nothing. Every example below fails against core's `Array.instDecidableEq`,
+`Vector`'s derived instance, or `Array.ofFn`.
+
+Delete alongside the workarounds once
+[leanprover/lean4#14270](https://github.com/leanprover/lean4/pull/14270) lands,
+after first re-pointing them at the core definitions and confirming they still
+pass. That is the check that the upstream fix actually works.
+-/
+
+namespace Hex.ModuleBoundaryTests
+
+/-! ## `Array` equality, both sides nonempty -/
+
+example : (#[0, 1] : Array Nat) ≠ #[1] := by decide
+example : (#[2, 3] : Array Nat) = #[2, 3] := by decide
+example : (#[1, 2, 3] : Array Nat) ≠ #[1, 2, 4] := by decide +kernel
+example : decide ((#[0, 1] : Array Nat) = #[0, 1]) = true := by rfl
+
+/-! Cases that reduced even before the workaround, kept so a regression in the
+empty/nonempty branches is caught too. -/
+
+example : (#[] : Array Nat) = #[] := by decide
+example : (#[] : Array Nat) ≠ #[1] := by decide
+
+/-! ## `Vector` equality, whose core instance is derived -/
+
+example : (#v[0, 1, 2] : Vector Nat 3) ≠ #v[0, 0, 0] := by decide
+example : (#v[0, 1, 2] : Vector Nat 3) = #v[0, 1, 2] := by decide +kernel
+
+/-! ## `ofFn` -/
+
+example : (Array.ofFn' (n := 3) (fun i => i.val)).size = 3 := by decide
+example : Array.ofFn' (n := 3) (fun i => i.val) = #[0, 1, 2] := by decide
+example : Vector.ofFn' (n := 4) (fun i => i.val * 2) = #v[0, 2, 4, 6] := by
+  decide +kernel
+
+/-! ## The combination, which is the shape `hex-mv-poly` will use: an exponent
+vector built with `ofFn'` and compared for equality. -/
+
+example :
+    (Vector.ofFn' (n := 3) (fun j => if j = 1 then 1 else 0) : Vector Nat 3)
+      ≠ Vector.ofFn' (fun j => if j = 2 then 1 else 0) := by
+  decide +kernel
+
+end Hex.ModuleBoundaryTests

HexBasic/OfFn.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import Std
+
+public section
+
+/-!
+Kernel-reducible `ofFn` for `Array` and `Vector`.
+
+`Array.ofFn` delegates to its `ofFn.go` auxiliary, which is not exposed, so
+under the module system its body is unavailable downstream and
+`(Array.ofFn f)` does not reduce in the kernel. `Vector.ofFn` is itself
+`@[expose]` but calls `Array.ofFn`, so it inherits the stall.
+
+`List.ofFn` is fully exposed and reduces, so the definitions below go through
+it. That is the wrong shape for compiled code, which wants to push into an
+array of known capacity rather than build a linked list and convert, so each
+carries a `@[csimp]` lemma redirecting the compiler back to the core version.
+The `List` route is then paid only in the kernel, which is where it is needed.
+
+**Delete this file** once
+[leanprover/lean4#14270](https://github.com/leanprover/lean4/pull/14270) lands
+and the toolchain is bumped past it, replacing uses with `Array.ofFn` and
+`Vector.ofFn`. See `progress/lean4-array-decidableeq-module-repro.md` for the
+full cleanup checklist.
+-/
+
+namespace Hex
+
+/-- `Array.ofFn` that reduces in the kernel under the module system. -/
+@[expose] def Array.ofFn' {α : Type u} {n : Nat} (f : Fin n → α) : Array α :=
+  (List.ofFn f).toArray
+
+/-- `Vector.ofFn` that reduces in the kernel under the module system. -/
+@[expose] def Vector.ofFn' {n : Nat} {α : Type u} (f : Fin n → α) : Vector α n :=
+  ⟨(List.ofFn f).toArray, by simp⟩
+
+@[simp] theorem Array.ofFn'_eq_ofFn {α : Type u} {n : Nat} (f : Fin n → α) :
+    Array.ofFn' f = Array.ofFn f := by
+  simp [Array.ofFn']
+
+@[simp] theorem Vector.ofFn'_eq_ofFn {n : Nat} {α : Type u} (f : Fin n → α) :
+    Vector.ofFn' f = Vector.ofFn f := by
+  simp [Vector.ofFn', _root_.Vector.ofFn]
+
+/-- Compiled code uses the core `Array.ofFn`, which fills an array of known
+capacity instead of building a `List` first. The `List` route exists only so
+that the kernel can reduce it. -/
+@[csimp] theorem Array.ofFn'_eq_ofFn' : @Array.ofFn' = @_root_.Array.ofFn := by
+  funext α n f; exact Array.ofFn'_eq_ofFn f
+
+/-- As `Array.ofFn'_eq_ofFn'`. -/
+@[csimp] theorem Vector.ofFn'_eq_ofFn' : @Vector.ofFn' = @_root_.Vector.ofFn := by
+  funext n α f; exact Vector.ofFn'_eq_ofFn f
+
+end Hex

HexBerlekampZassenhaus/BhksCandidates.lean

@@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility
 public import HexHensel.Multifactor
 public import HexHensel.QuadraticMultifactor
 public import HexLLL.Basic
--- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the
--- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the
--- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under
--- the module system. Drop once that impl is exposed upstream (lean4).
-import all Init.Data.Array.DecidableEq
+-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`.
+-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it.
+public import HexBasic.ArrayDecEq
 
 public import HexBerlekampZassenhaus.Lattice
 public meta import HexBerlekampZassenhaus.Lattice
@@ -36,6 +34,8 @@ import all HexBerlekampZassenhaus.ChoosePrimeData
 import all HexBerlekampZassenhaus.ReassemblyProofs
 import all HexBerlekampZassenhaus.Lattice
 
+open scoped Hex   -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq
+
 public section
 set_option backward.proofsInPublic true
 

HexBerlekampZassenhaus/BhksRecover.lean

@@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility
 public import HexHensel.Multifactor
 public import HexHensel.QuadraticMultifactor
 public import HexLLL.Basic
--- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the
--- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the
--- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under
--- the module system. Drop once that impl is exposed upstream (lean4).
-import all Init.Data.Array.DecidableEq
+-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`.
+-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it.
+public import HexBasic.ArrayDecEq
 
 public import HexBerlekampZassenhaus.BhksCandidates
 public meta import HexBerlekampZassenhaus.BhksCandidates
@@ -37,6 +35,8 @@ import all HexBerlekampZassenhaus.ReassemblyProofs
 import all HexBerlekampZassenhaus.Lattice
 import all HexBerlekampZassenhaus.BhksCandidates
 
+open scoped Hex   -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq
+
 public section
 set_option backward.proofsInPublic true
 

HexBerlekampZassenhaus/Certificate.lean

@@ -21,17 +21,17 @@ public import HexBerlekamp.Irreducibility
 public import HexHensel.Multifactor
 public import HexHensel.QuadraticMultifactor
 public import HexLLL.Basic
--- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the
--- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the
--- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under
--- the module system. Drop once that impl is exposed upstream (lean4).
-import all Init.Data.Array.DecidableEq
+-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`.
+-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it.
+public import HexBasic.ArrayDecEq
 
 public import HexBerlekampZassenhaus.Records
 public meta import HexBerlekampZassenhaus.Records
 import all HexBerlekampZassenhaus.PrimeSelection
 import all HexBerlekampZassenhaus.Records
 
+open scoped Hex   -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq
+
 public section
 set_option backward.proofsInPublic true
 

HexBerlekampZassenhaus/ChoosePrimeData.lean

@@ -21,18 +21,18 @@ public import HexBerlekamp.Irreducibility
 public import HexHensel.Multifactor
 public import HexHensel.QuadraticMultifactor
 public import HexLLL.Basic
--- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the
--- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the
--- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under
--- the module system. Drop once that impl is exposed upstream (lean4).
-import all Init.Data.Array.DecidableEq
+-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`.
+-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it.
+public import HexBasic.ArrayDecEq
 
 public import HexBerlekampZassenhaus.Certificate
 public meta import HexBerlekampZassenhaus.Certificate
 import all HexBerlekampZassenhaus.PrimeSelection
 import all HexBerlekampZassenhaus.Records
 import all HexBerlekampZassenhaus.Certificate
 
+open scoped Hex   -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq
+
 public section
 set_option backward.proofsInPublic true
 

HexBerlekampZassenhaus/FactorEntryPoints.lean

@@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility
 public import HexHensel.Multifactor
 public import HexHensel.QuadraticMultifactor
 public import HexLLL.Basic
--- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the
--- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the
--- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under
--- the module system. Drop once that impl is exposed upstream (lean4).
-import all Init.Data.Array.DecidableEq
+-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`.
+-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it.
+public import HexBasic.ArrayDecEq
 
 public import HexBerlekampZassenhaus.Recombination
 public meta import HexBerlekampZassenhaus.Recombination
@@ -39,6 +37,8 @@ import all HexBerlekampZassenhaus.BhksCandidates
 import all HexBerlekampZassenhaus.BhksRecover
 import all HexBerlekampZassenhaus.Recombination
 
+open scoped Hex   -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq
+
 public section
 set_option backward.proofsInPublic true
 

HexBerlekampZassenhaus/IrreducibleCore.lean

@@ -21,11 +21,9 @@ public import HexBerlekamp.Irreducibility
 public import HexHensel.Multifactor
 public import HexHensel.QuadraticMultifactor
 public import HexLLL.Basic
--- Needed so `decide`/`rfl` over `DensePoly`/`Array` equality reduces in the
--- kernel: the core `Array.instDecidableEq` delegates its nonempty case to the
--- non-`@[expose]` `Array.instDecidableEqImpl`, which is otherwise opaque under
--- the module system. Drop once that impl is exposed upstream (lean4).
-import all Init.Data.Array.DecidableEq
+-- Kernel-reducible `Array`/`Vector` equality; see `HexBasic.ArrayDecEq`.
+-- Drop once leanprover/lean4#14270 lands and the toolchain is bumped past it.
+public import HexBasic.ArrayDecEq
 
 public import HexBerlekampZassenhaus.FactorEntryPoints
 public meta import HexBerlekampZassenhaus.FactorEntryPoints
@@ -40,6 +38,8 @@ import all HexBerlekampZassenhaus.BhksRecover
 import all HexBerlekampZassenhaus.Recombination
 import all HexBerlekampZassenhaus.FactorEntryPoints
 
+open scoped Hex   -- kernel-reducible Array/Vector equality; see HexBasic.ArrayDecEq
+
 public section
 set_option backward.proofsInPublic true