Modular sum of two packed residues below q. The unreduced sum fits in a
UInt32 because q < 2^31, so one conditional subtraction canonicalizes it.
Instances For
The modulus as a packed word.
Equations
Instances For
Read a packed word as a residue.
Equations
Instances For
Write a residue as a packed word.
Equations
Instances For
A residue is below 2 ^ 32, so ofZMod loses nothing: ZMod64.Bounds
caps the modulus at 2 ^ 31.
Packing a residue preserves its numeral.
ofZMod is a section of toZMod: packing then reading recovers the
residue.
Reading an arbitrary packed word canonicalizes it modulo p.
Not @[simp]: ZMod64.toNat_eq_val rewrites the ZMod64.toNat head of the
left-hand side, so this shape is not simp-normal.
The packed modulus word carries the modulus faithfully.
The modulus is below 2 ^ 32, so it is faithful as a packed word.
mulMod computes the modular product of its operands as naturals. The
UInt64 widening keeps the unreduced product exact for arbitrary UInt32
inputs, so no reducedness hypothesis is needed.
addMod computes the modular sum of two reduced operands. Reducedness is
required: the single conditional subtraction only canonicalizes a sum that is
below 2 * p.
Modular inverse of a packed residue, routed through Hex.ZMod64.inv.
This runs once per pivot column, so it never appears in the inner loop and does
not need a word-level extended-Euclid specialization.
Equations
Instances For
The packed inverse of a packed word is the packed inverse residue.
invMod returns a reduced residue for any input word.
Reading an entry of a representing packed matrix recovers the residue
entry. This is the form Rep is consumed in once the goal is stated over
residues rather than over toNat.
Scale row i of a packed matrix by the packed residue c. Mirrors
Hex.Matrix.rowScale, which is the same per-entry in-place
Hex.Matrix.modifyEntries with the generic product replaced by the
modular one.
Equations
- Hex.Berlekamp.Packed.rowScale q A i c = A.modifyEntries ↑i fun (x : Fin m) (x_1 : UInt32) => Hex.Berlekamp.Packed.mulMod q c x_1
Instances For
Replace row dst of a packed matrix by row dst + c * rsrc, with the source
row supplied by the caller instead of read out of the matrix.
rsrc must be a freshly materialized row, as Hex.Matrix.getRow produces.
A borrow of A's own backing buffer would leave that buffer multiply
referenced, and the Hex.Matrix.modifyEntries below would copy the whole
matrix per row addition instead of writing in place.
Equations
- Hex.Berlekamp.Packed.rowAddFrom q A rsrc dst c = A.modifyEntries ↑dst fun (k : Fin m) (x : UInt32) => Hex.Berlekamp.Packed.addMod q x (Hex.Berlekamp.Packed.mulMod q c rsrc[k])
Instances For
Replace row dst of a packed matrix by row dst + c * row src. Mirrors
Hex.Matrix.rowAdd: the source row is read once, then the destination
row's entries are updated in place.
Equations
- Hex.Berlekamp.Packed.rowAdd q A src dst c = Hex.Berlekamp.Packed.rowAddFrom q A (A.getRow src) dst c
Instances For
Entrywise characterisation of rowAdd, the rowAddFrom special case that
reads the source row out of the matrix.
A packed row scaling by a word representing γ interprets the reference
row scaling by γ.
A caller-supplied source row that agrees entrywise with row src of the
packed matrix interprets the reference row addition, just as reading the row out
of the matrix does.
A packed row addition by a word representing γ interprets the reference
row addition by γ.
Packed pivot search: the first row at or below start whose col entry is
nonzero. Mirrors Hex.Matrix.findPivotAux.
Equations
- One or more equations did not get rendered due to their size.
- Hex.Berlekamp.Packed.findPivotAux A col start 0 = none
Instances For
Packed pivot search from start. Mirrors Hex.Matrix.findPivot?.
Equations
- Hex.Berlekamp.Packed.findPivot? A col start = Hex.Berlekamp.Packed.findPivotAux A col start (n - start)
Instances For
Eliminate every non-pivot entry of a packed pivot column. Mirrors
Hex.Matrix.eliminateColumn with the transform component dropped.
The pivot row is read once for the whole column rather than once per row
addition: the fold skips j = pivotRow, so nothing it writes can change what
the next row addition reads. A dense column's n - 1 source-row copies become
one.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Running state of the packed Gauss-Jordan loop. Mirrors
Hex.Matrix.RowReduceState without the transform.
- row : Nat
Rows already assigned a pivot.
The partially reduced packed matrix.
Pivot columns found so far, in increasing order.
Instances For
The packed Gauss-Jordan loop. Mirrors Hex.Matrix.rowReduceLoop.
Equations
- One or more equations did not get rendered due to their size.
- Hex.Berlekamp.Packed.reduceLoop p q col 0 s = s
Instances For
The packed column elimination represents the reference column elimination.
The source row rsrc is hoisted out of the fold, so the fold carries the
invariant that it still agrees with the accumulated buffer's pivot row.
The packed Gauss-Jordan loop simulates Hex.Matrix.rowReduceLoop: it
finds the same pivot columns in the same order, advances the same row counter,
and its packed buffer represents the reference echelon matrix at every step.
The reference transform is carried along on the right and never inspected.
Packed Gauss-Jordan elimination of A. Mirrors Hex.Matrix.rowReduce
without the transform.
Equations
- Hex.Berlekamp.Packed.reduce p q A = Hex.Berlekamp.Packed.reduceLoop p q 0 m { row := 0, echelon := A, pivots := [] }
Instances For
The packed reduction finds the reference pivot columns.
The packed reduction finds the reference rank.
The packed reduction's buffer represents the reference echelon form.
The pivot row of column j, searching from row i. Mirrors
Hex.Matrix.IsRowReduced.pivotIndexAux walking the pivot-column list.
Equations
- Hex.Berlekamp.Packed.pivotRowOf [] x✝¹ x✝ = none
- Hex.Berlekamp.Packed.pivotRowOf (c :: cs) x✝¹ x✝ = if c = x✝¹ then some x✝ else Hex.Berlekamp.Packed.pivotRowOf cs x✝¹ (x✝ + 1)
Instances For
The non-pivot columns, in increasing order. Mirrors
Hex.Matrix.IsEchelonForm.freeColsList with the echelon witness dropped.
Equations
- Hex.Berlekamp.Packed.freeColsList pivots = List.filter (fun (j : Fin m) => decide ¬j ∈ pivots) (List.finRange m)
Instances For
The nullspace basis read straight off a reduced packed buffer: one vector
per free column, with a 1 in its own free column, the negated pivot-row entry
in each pivot column, and 0 elsewhere.
The i < n test is never false on a reduction's own output -- there are at most
n pivots -- and nullspaceArray_eq discharges it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The packed nullspace readback reproduces Hex.Matrix.nullspace.
The fixed-space matrix Q_f - I, built directly into a packed buffer from
the Berlekamp column polynomials.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The packed fixed-space buffer represents
Hex.Berlekamp.fixedSpaceMatrix.
The Berlekamp fixed-space kernel basis, computed on the packed
representation: build the packed Q_f - I, reduce it in place with the
specialized Gauss-Jordan loop, and read the basis off the reduced buffer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The correspondence theorem. The packed kernel computation returns
exactly Hex.Matrix.nullspace of the fixed-space matrix.
The packed implementation of
Hex.Berlekamp.fixedSpaceKernelVectors, selected in compiled code by the
@[csimp] theorem fixedSpaceKernelVectors_eq_packed below.
Equations
- Hex.Berlekamp.fixedSpaceKernelVectorsPacked f hmonic = Vector.mk (Hex.Berlekamp.Packed.kernelArray p f hmonic) ⋯
Instances For
The packed fixed-space kernel is the generic one. Registered @[csimp], so
compiled code runs the packed reduction while every Berlekamp soundness and
completeness proof keeps reasoning about Matrix (ZMod64 p) and
Hex.Matrix.nullspace.
The fixed-space kernel basis converted back to polynomial representatives.
Compute the vector basis once and map the conversion over it. Keep the basis outside any per-index body so matrix construction and row reduction remain shared; mapping also carries its dependent length without recomputing rank.
Equations
Instances For
Every polynomial representative returned by fixedSpaceKernel satisfies the
executable fixed-space kernel condition.