perf(bivariate): in-place dense linear solver for GS interpolation (#256)#259
Conversation
🤖 PR SummaryPerformance Optimization
Mathematical Formalization
Benchmarking
Statistics
Lean Declarations ✏️ **Added:** 23 declaration(s)
📋 **Additional Analysis**Style and Naming
Module Layout and Documentation
Benchmarks and Performance
📄 **Per-File Summaries**
Last updated: 2026-06-26 11:57 UTC. |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
🤖 AI Review
Overall Summary:
TL;DR: The PR successfully implements and verifies an optimized, in-place dense matrix reduction algorithm for the Guruswami-Sudan interpolation solver. The mathematical logic, array mutation safety, and proofs are rigorous, requiring only a minor structural export fix in the package root.
Mechanical Pre-Check Results: No escape hatches (sorry, axiom, native_decide, opaque, implemented_by, sorryAx) or file size issues were detected.
Checklist Coverage: No explicit specification checklist was provided. However, the in-place operations mathematically perfectly match the functional implementation, successfully maintaining kernel dimension invariants and soundness guarantees.
Cross-File Issues: The cross-file dependencies form a sound and well-isolated abstraction boundary. The behavioral equivalence lemma (homogeneousWitnessInPlace_eq) is correctly exported, cleanly consumed at the composition boundaries in Context.lean, and efficiently threaded into downstream proofs.
Key Lean 4 / Mathlib Issues:
- The newly added module
CompPoly.LinearAlgebra.Dense.KernelInPlaceis missing from the top-level exports in the package root. Package root files should explicitly list all modules, even if they are transitively imported elsewhere. (CompPoly.lean:112)
Overall Verdict: Needs Minor Revisions
🔗 **Cross-File Analysis**
Cross-File Analysis:
The PR introduces an optimized, in-place dense matrix reduction algorithm (homogeneousWitnessInPlace in KernelInPlace.lean) and integrates it into the Guruswami-Sudan interpolation solver.
-
Composition Chains & Type Flow: The core logic changes the backing implementation of
denseLinearKernelContext(inContext.lean) fromDenseMatrix.homogeneousWitnesstoDenseMatrix.homogeneousWitnessInPlace. To satisfy the correctness contracts (witness_width,witness_sound,witness_nonzero,witness_complete) required by theLinearKernelContexttypeclass, the PR uses a behavioral equivalence lemma (homogeneousWitnessInPlace_eqproven inKernelInPlaceCorrectness.lean). This cleanly decouples the imperative array mutation proofs from the higher-level interpolation soundness and completeness proofs. -
Theorem Propagation: The behavioral equivalence lemma is correctly exported and consumed at the composition boundary in
Context.lean. Furthermore, it is appropriately threaded intodenseInterpolateWithBasis_exists_of_dimension_slackinInterpolation/Dense/Correctness.lean, where unfoldingdenseLinearKernelContextnow exposes the in-place version, requiring the equivalence lemma in thesimpcall to match the existential witness constructed from the copying version. -
Escape Hatches & Externals: The mechanical checks report no new axioms or escape hatches. The use of
Id.runfor mutation scopes is safely constrained and standardArrayoperations are used. No external dependencies are misused. -
Benchmarks: The benchmarks in
bench/CompPolyBench/Bivariate/GuruswamiSudan.leanand their metadata labels inCommon.leanare appropriately wired to time both the copying and in-place routines, confirming proper integration.
The cross-file dependencies form a sound and well-isolated abstraction boundary.
Cross-File Composition Issues: None
Axiom/Escape Hatch Impact: None
External Dependency Issues: None
Missing Cross-File Verification: None
Cluster: Dense Linear Algebra In-Place Kernel (critical)
Does the in-place mutable algorithm correctly implement the same math as the functional copying one, and does the equivalence proof cleanly connect them without unstated side effects or gaps?
📄 **Review for `CompPoly/LinearAlgebra/Dense/KernelInPlace.lean`**
Analysis:
- Mathematical operations: The file implements an optimized, in-place version of Gauss-Jordan elimination for computing homogeneous kernels. Instead of operating on a boxed
DenseMatrixstructure which may incur array copying due to multiple references, the algorithm extracts the backingArray Fand mutates it sequentially insideId.runblocks. The functions correctly implement primitive row operations (swap, scale, eliminate) by indexing into a row-major 1D array usingrow * cols + col. - Specification and Checklist: There is no specific checklist for this PR. The module docstring serves as the spec, guaranteeing bit-for-bit equivalence with the functional
rrefimplementation, which is formally proven in the contextual correctness file. - Riskiest aspects: The main risks in this type of implementation in Lean 4 are unboxing failures (where the array is aliased and copied anyway, destroying the O(1) mutation performance) and off-by-one index arithmetic. The destructuring of
MviamatchinrrefInPlacesuccessfully consumes the wrapper structure, leaving a unique array reference for the loop. The arithmetic indices (row * cols + col) are completely correct for row-major layouts, and the use of safe getters/setters (getD,setD) ensures no runtime panics even on bounds errors. - Ambiguities: There are no mathematical ambiguities. The usage of
[BEq F]instead of[DecidableEq F]is idiomatic for computationally-focused code paths in Lean 4 and perfectly consistent with the project's algebraic execution conventions.
Overall, this is an exceptionally clean, well-optimized, and fully verified piece of executable mathematics.
Verdict: Approved
Critical Misformalizations: None
Lean 4 / Mathlib Issues: None
Nitpicks: None
📄 **Review for `CompPoly/LinearAlgebra/Dense/KernelInPlaceCorrectness.lean`**
Analysis:
Step-by-step analysis of the changes:
- Mathematical Functionality: The PR introduces the correctness proof for the
Id.runin-place mutable dense matrix kernel backend. It proves that the step-by-step array mutations (setD) within the sequential loops match the behavior of the previously verified pure, copyingRowOpsmatrix backend. The file operates bottom-up: proving the equivalence of loop accumulators (List.foldl) for row scaling, adding scaled rows, and swapping rows, then linking these to Gauss-Jordan elimination primitives, and finally establishingrrefInPlace_eqandhomogeneousWitnessInPlace_eq. - Riskiest Aspects: The primary mathematical and formalization risk with verifying in-place loops via
Id.runis aliasing—ensuring that intermediate mutations to the backing array do not inadvertently alter the data being read in subsequent loop iterations. The PR gracefully mitigates this by abstracting the iterations intoList.foldlsteps and maintaining invariants (e.g.,hT,hS, andhagree) guaranteeing the accumulator strictly agrees with the original pre-loop array on the relevant read bounds. It uses index injectivity logic (row_col_index_ne) to formalize that distinct row targets never overlap. - Ambiguities: None. The logic strictly adheres to standard dense row operations and accurately maps the
Id.runvariables to the functional ones without gaps. - Checklist Results: No spec checklist was provided.
Verdict: Approved
Critical Misformalizations: None
Lean 4 / Mathlib Issues: None
Nitpicks: None
Cluster: Guruswami-Sudan Interpolation Context (high)
Does substituting the in-place kernel extraction into the dense GS context properly discharge the linear kernel context obligations, and do the correctness proofs adapt safely?
📄 **Review for `CompPoly/Bivariate/GuruswamiSudan/Context.lean`**
Analysis:
- Mathematical operations: The diff replaces the copying linear kernel computation
DenseMatrix.homogeneousWitnesswith its optimized in-place variantDenseMatrix.homogeneousWitnessInPlacewithin thedenseLinearKernelContext. To satisfy the structure's proof obligations (witness_width,witness_sound,witness_nonzero,witness_complete), it prependsrw [DenseMatrix.homogeneousWitnessInPlace_eq] at hto each proof. This leverages the established correctness of the copying variant by cleanly substituting the in-place equality. - Riskiest aspects: The main risk when transitioning to in-place implementations is that proofs might fail if the equivalence lemma (
homogeneousWitnessInPlace_eq) is incorrectly oriented or applied. However, therw ... at hformulation correctly converts the hypotheses about the in-place witness back into hypotheses about the copying witness, perfectly aligning with the preexisting proof steps. - Ambiguities: None. The changes are transparent, and the cluster context verifies that downstream completeness lemmas have been appropriately adapted with simp additions.
- Spec checklist: No checklist provided.
Verdict: Approved
Critical Misformalizations: None
Lean 4 / Mathlib Issues: None
Nitpicks: None
📄 **Review for `CompPoly/Bivariate/GuruswamiSudan/Interpolation/Dense/Correctness.lean`**
Analysis:
- Mathematical Correctness & Intent: The PR modifies the proof of
denseInterpolateWithBasis_exists_of_dimension_slackto accommodate a change in the underlyingdenseLinearKernelContext. The context was updated to usehomogeneousWitnessInPlaceinstead ofhomogeneousWitness. To ensure the proof still works, the theoremDenseMatrix.homogeneousWitnessInPlace_eqis added to thesimpcontext, which rewrites the in-place function to the standard one, allowing the existing hypothesishw(which concernshomogeneousWitness) to trigger and correctly simplify the goal. - Riskiest Aspects: The main risk when swapping a matrix backend (e.g., to an in-place version) is that the kernel dimension invariants or soundness guarantees change. By utilizing
homogeneousWitnessInPlace_eq, the author mathematically guarantees that the in-place extraction exactly mirrors the purely functional one, safely preserving all correctness properties. - Ambiguities: None. The change is purely a proof repair tied to an implementation swap, and the equivalence is formally proven by the
_eqlemma. - Checklist Mapping: The cross-file question asking if the discharging theorems properly rewrite
homogeneousWitnessInPlacetohomogeneousWitnessis definitively addressed here. The simp array specifically includesDenseMatrix.homogeneousWitnessInPlace_eqfor exactly this purpose.
Verdict: Approved
Critical Misformalizations: None
Lean 4 / Mathlib Issues: None
Nitpicks: None
Cluster: Benchmarks and Exports (medium)
Are the benchmarks correctly configured to measure both the copying and in-place backend independently and are new modules properly exported?
📄 **Review for `CompPoly.lean`**
Analysis:
The diff adds an import for CompPoly.LinearAlgebra.Dense.KernelInPlaceCorrectness to CompPoly.lean, which serves as the top-level package root exporting all modules in the library. However, the associated implementation module CompPoly.LinearAlgebra.Dense.KernelInPlace is missing from the import list. While it is likely transitively imported by the correctness module, standard Lean library structure (e.g., as enforced by lake's typical auto-generation of package roots) dictates that top-level root files should explicitly import all source modules. Furthermore, the review cluster context explicitly flags to verify that both KernelInPlace and KernelInPlaceCorrectness are exposed in the package roots.
Verdict: Needs Minor Revisions
Critical Misformalizations: None
Lean 4 / Mathlib Issues: None
Nitpicks:
- The newly added module
CompPoly.LinearAlgebra.Dense.KernelInPlaceis missing from the top-level exports. Package root files should explicitly list all modules. Although it may be transitively imported viaKernelInPlaceCorrectness, standard practice is to include all files. (CompPoly.lean:112)
📄 **Review for `CompPoly/LinearAlgebra/Dense.lean`**
Analysis:
- Mathematical Code Changes: The diff modifies the facade module
CompPoly.LinearAlgebra.Denseto expose two new modules:KernelInPlaceandKernelInPlaceCorrectness. - Riskiest Aspects: The primary concern for a facade module is whether the imports correctly match the existing file structure and successfully compile. The toolchain output confirms these modules exist and are available for import.
- Ambiguities: There are no mathematical ambiguities as this is purely structural configuration.
- Checklist Mapping: The changes properly expose the implementations benchmarked in
bench/CompPolyBench/Bivariate/GuruswamiSudan.lean(specificallyDenseMatrix.homogeneousWitnessInPlace), which validates the cross-file hypothesis.
Verdict: Approved
Critical Misformalizations: None
Lean 4 / Mathlib Issues: None
Nitpicks: None
📄 **Review for `bench/CompPolyBench/Bivariate/GuruswamiSudan.lean`**
Analysis:
- Mathematically, the code is a benchmark script for the Guruswami-Sudan list decoding interpolation step. It measures the performance of dense linear algebra solvers over a finite field (KoalaBear). The diff specifically replaces older generic 'kernelContext' abstractions with explicit calls to both copying (
DenseMatrix.homogeneousWitness) and in-place (DenseMatrix.homogeneousWitnessInPlace) algorithms. - The most error-prone aspect of benchmark updates is failing to keep the timing variables or iterations aligned, which would lead to statistically biased metrics. Here,
measured,fastMeasured,inPlaceMeasured, andfastInPlaceMeasuredare distinct and successfully passed into their respectiverunTimedclosures. - The mathematical and functional intent is clear and aligns perfectly with the overarching goal of separating in-place memory mutations from default purely functional matrix algorithms.
- N/A (no spec checklist).
Verdict: Approved
Critical Misformalizations: None
Lean 4 / Mathlib Issues: None
Nitpicks: None
📄 **Review for `bench/CompPolyBench/Common.lean`**
Analysis:
The change adds two string mappings to the implementationMethodLabels list in the benchmark configuration file bench/CompPolyBench/Common.lean. It maps the method names "Homogeneous interpolation solve, copying" and "Homogeneous interpolation solve, in-place" to their human-readable display labels "Dense solve (copying)" and "Dense solve (in-place)". This perfectly matches the benchmarking logic presented in the broader cluster context, which updates the Guruswami-Sudan benchmarks to measure and compare the in-place kernel basis computation with the previous copying implementation. There are no mathematical changes, no typeclass or logical errors, and no escape hatches.
Verdict: Approved
Critical Misformalizations: None
Lean 4 / Mathlib Issues: None
Nitpicks: None
| import CompPoly.LinearAlgebra.Dense.Basic | ||
| import CompPoly.LinearAlgebra.Dense.Kernel | ||
| import CompPoly.LinearAlgebra.Dense.KernelCorrectness | ||
| import CompPoly.LinearAlgebra.Dense.KernelInPlaceCorrectness |
There was a problem hiding this comment.
💡 Nitpick: The newly added module CompPoly.LinearAlgebra.Dense.KernelInPlace is missing from the top-level exports. Package root files should explicitly list all modules. Although it may be transitively imported via KernelInPlaceCorrectness, standard practice is to include all files.
Suggested fix: import CompPoly.LinearAlgebra.Dense.KernelCorrectness
import CompPoly.LinearAlgebra.Dense.KernelInPlace
import CompPoly.LinearAlgebra.Dense.KernelInPlaceCorrectness
Build Timing Report
Incremental Rebuild Signal
This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark. Slowest Current Clean-Build FilesShowing 20 slowest current targets, with comparison against the selected baseline when available.
|
2 participants
Summary
Merges #256 after reconciling with current
master. The original fork branch was 2 commits behind; this branch integrates those commits and includes the in-place dense linear solver work.Closes #256.
Test plan
lake buildpasses locally after mergeMade with Cursor