perf(bivariate): in-place dense linear solver for GS interpolation

[olympichek]

Overview

This PR substantially speeds up the Guruswami-Sudan dense linear interpolation solve while preserving all of its correctness guarantees.

The previous solver copied the entire working matrix on every row operation. Because Gaussian elimination performs a number of row operations proportional to the matrix size, that copy pushed its cost from the expected cubic O(n³) up to quartic O(n⁴), and produced a large amount of short-lived allocation along the way. The new solver works in place, reusing its memory instead of copying it, which restores the O(n³) running time and relieves the allocation pressure on the interpolation step.

This is purely a performance change: the new implementation is proven equivalent to the old one, so it introduces no new assumptions.

This PR includes:

• The faster in-place dense solver (homogeneousWitnessInPlace), now the certified backend behind denseLinearKernelContext for Guruswami-Sudan interpolation.
• The equivalence proof to the previous solver (homogeneousWitnessInPlace_eq), which lets the existing correctness guarantees carry over unchanged.
• Benchmarks that run the old and new solvers side by side to measure the speedup.

[github-actions]

🤖 PR Summary

Performance Optimization

• Replaces the functional copying-based linear solver in Guruswami-Sudan interpolation with a memory-efficient, in-place implementation.
• Implements rrefInPlace and homogeneousKernelBasisInPlace, reducing algorithmic complexity from $O(n^4)$ to $O(n^3)$ by eliminating redundant matrix copies.
• Configures denseLinearKernelContext to use the homogeneousWitnessInPlace backend for improved performance in bivariate polynomial computations.

Mathematical Verification

• Provides formal equivalence proofs within the KernelInPlaceCorrectness module, specifically homogeneousWitnessInPlace_eq, ensuring the optimized solver matches the functional implementation's behavior.
• The implementation is fully verified; no sorry or admit placeholders are used in the proofs or the backend logic.

Infrastructure & Benchmarking

• Updates the CompPolyBench suite to include side-by-side performance comparisons between the copying-based and in-place methods.
• Adds benchmarking support for specific field implementations, including KoalaBear and KoalaBear.Fast.

---

Statistics

Metric	Count
📝 Files Changed	8
✅ Lines Added	458
❌ Lines Removed	12

---

Lean Declarations

✏️ **Added:** 23 declaration(s)

• theorem rrefLoopData_eq [Field F] [BEq F] : in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• def homogeneousKernelBasisInPlace [Field F] [BEq F] (M : DenseMatrix F) : in CompPoly/LinearAlgebra/Dense/KernelInPlace.lean
• theorem scaleRowData_eq [Field F] (M : DenseMatrix F) (r : Nat) (factor : F) : in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• theorem addScaledRowData_eq [Field F] (M : DenseMatrix F) (target source : Nat) in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• def addScaledRowData [Field F] (cols target source : Nat) (factor : F) in CompPoly/LinearAlgebra/Dense/KernelInPlace.lean
• private theorem getD_setD_ne [Zero F] (d : Array F) {i j : Nat} (h : i ≠ j) (v : F) : in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• theorem normalizeAndEliminateData_eq [Field F] [BEq F] (M : DenseMatrix F) in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• theorem findPivotRowData_eq [Zero F] [BEq F] (M : DenseMatrix F) (startRow col : Nat) : in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• def swapRowsData [Zero F] (cols rowA rowB : Nat) (data : Array F) : Array F in CompPoly/LinearAlgebra/Dense/KernelInPlace.lean
• def homogeneousWitnessInPlace [Field F] [BEq F] (M : DenseMatrix F) : in CompPoly/LinearAlgebra/Dense/KernelInPlace.lean
• def scaleRowData [Field F] (cols row : Nat) (factor : F) (data : Array F) : in CompPoly/LinearAlgebra/Dense/KernelInPlace.lean
• private theorem foldl_swap_self_eq_const [Zero F] in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• private theorem row_col_index_ne {a b cols c c' : Nat} (hrow : a ≠ b) in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• theorem rrefInPlace_eq [Field F] [BEq F] (M : DenseMatrix F) : rrefInPlace M = rref M in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• theorem swapRowsData_eq [Zero F] (M : DenseMatrix F) (rowA rowB : Nat) : in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• private theorem forIn_eliminate_eq [Field F] (cols pivotRow pivotCol : Nat) : in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• theorem homogeneousWitnessInPlace_eq [Field F] [BEq F] (M : DenseMatrix F) : in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• def rrefLoopData [Field F] [BEq F] : in CompPoly/LinearAlgebra/Dense/KernelInPlace.lean
• def findPivotRowData [Zero F] [BEq F] (rows cols startRow col : Nat) in CompPoly/LinearAlgebra/Dense/KernelInPlace.lean
• private theorem foldl_addScaled_self_eq_const [Field F] in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean
• def normalizeAndEliminateData [Field F] [BEq F] (rows cols pivotRow pivotCol : Nat) in CompPoly/LinearAlgebra/Dense/KernelInPlace.lean
• def rrefInPlace [Field F] [BEq F] (M : DenseMatrix F) : RrefResult F in CompPoly/LinearAlgebra/Dense/KernelInPlace.lean
• private theorem foldl_scale_self_eq_const [Field F] in CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

Pull Request Guidelines

• Title Format: The suggested title for this PR is perf(LinearAlgebra): implement in-place dense homogeneous kernels.
• Description:
  • Motivation: The PR improves the performance of the dense Gauss-Jordan homogeneous-kernel backend from $O(n^4)$ to $O(n^3)$ by utilizing in-place array mutation, avoiding costly array copies during row operations.
  • Contrast: It replaces the copying implementation DenseMatrix.homogeneousWitness with the mutating implementation DenseMatrix.homogeneousWitnessInPlace in the denseLinearKernelContext.
• Wiki Updates: The PR introduces two new files (CompPoly/LinearAlgebra/Dense/KernelInPlace.lean and CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean) which changes the repository structure. According to the guidelines, the matching page in docs/wiki/ should be updated in the same PR.

Style and Naming Guidelines

• File Naming: New files KernelInPlace.lean and KernelInPlaceCorrectness.lean follow the UpperCamelCase.lean convention.
• Declaration Naming:
  • Functions like swapRowsData, scaleRowData, and rrefInPlace correctly use lowerCamelCase.
  • Theorems like scaleRowData_eq, addScaledRowData_eq, and homogeneousWitnessInPlace_eq correctly use snake_case.
• Formatting:
  • Line Length: All lines in the new .lean files appear to be under the 100-character limit.
  • Indentation: The code uses the standard 2-space indentation.
  • Headers: Standard file headers including copyright (Apache 2.0) and authors are present.
  • Syntax: Use of fun x ↦ ... and by at the end of lines is consistent with the project's preferred style.
• Theorem Naming Logic: Equivalence lemmas for the in-place implementation correctly use the _eq suffix to denote bidirectional or bit-for-bit equality with the reference implementation.

Assessment against Framework

• Tier Transitions: This PR successfully optimizes the executable witness for the LinearKernelContext while maintaining the formal correctness requirements. The new implementation is discharged against existing correctness proofs for the copying-kernel via the bit-for-bit equivalence proved in KernelInPlaceCorrectness.lean.

---

📄 **Per-File Summaries**

• CompPoly.lean: This update adds an import for the KernelInPlaceCorrectness module, integrating new verification results for in-place kernel computations into the library's dense linear algebra component.
• CompPoly/Bivariate/GuruswamiSudan/Context.lean: This change updates the denseLinearKernelContext to use DenseMatrix.homogeneousWitnessInPlace for more efficient, in-place matrix reduction. The proofs for the context's properties were modified to utilize the equivalence between the in-place and copying versions, maintaining the existing correctness guarantees.
• CompPoly/Bivariate/GuruswamiSudan/Interpolation/Dense/Correctness.lean: This change modifies the proof of denseInterpolateWithBasis_exists_of_dimension_slack by incorporating the DenseMatrix.homogeneousWitnessInPlace_eq lemma into a simplification step. This ensures the correct relationship between the in-place witness computation and the interpolation polynomial basis.
• CompPoly/LinearAlgebra/Dense.lean: This update expands the dense linear algebra library by importing modules for in-place kernel computations and their associated correctness proofs. These additions integrate more efficient algorithmic implementations and their formal verifications into the top-level module.
• CompPoly/LinearAlgebra/Dense/KernelInPlace.lean: This file introduces a memory-efficient, in-place implementation of dense Gauss-Jordan elimination and homogeneous kernel extraction to optimize performance by avoiding unnecessary array copying. It defines several new executable functions, including rrefInPlace and homogeneousKernelBasisInPlace, which operate directly on the underlying data arrays to ensure linear-time row operations.
• CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean: This file introduces new theorems proving that in-place dense matrix row operations, RREF, and kernel calculations are functionally equivalent to their copying counterparts. It culminates in the proof of homogeneousWitnessInPlace_eq, allowing the certified backend to use the optimized in-place implementation without loss of correctness; no sorry placeholders are used.
• bench/CompPolyBench/Bivariate/GuruswamiSudan.lean: This update expands the Guruswami-Sudan interpolation benchmarks to compare copying versus in-place matrix solving methods. It refactors benchmark execution to call DenseMatrix methods directly and adds new benchmark records for evaluating in-place performance on the KoalaBear and KoalaBear.Fast fields.
• bench/CompPolyBench/Common.lean: This update expands the implementationMethodLabels list to include specific labels for 'copying' and 'in-place' variants of the homogeneous interpolation solve method, providing more granular identification in benchmarking results.

---

Last updated: 2026-06-20 23:42 UTC.

[dhsorens]

thank you @olympichek , merged in the related PR! (just so I could update the underlying branch)