Guarded native matrix reads for band arrays

Main definitions

• BandPreparation.matrixAddress: real row-major matrix addresses in the protected input.

Main results

• BandPreparation.exec_readCell: the actual guarded read returns exactly one encoded band value; padded rows are rejected before row-major multiplication.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.matrixOffset (m N : ℕ) (rightSide : Bool) (r k : ℕ) : ℕ

Offset in the concatenated original matrix inputs. The right matrix has D rows and N columns, while its band specification labels a column by r.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.matrixAddress (L m N : ℕ) (rightSide : Bool) (r k : ℕ) : ℕ

Address of an original signed input word in its protected snapshot.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.matrixAddress_lt_inverse {L m N r k : ℕ} (side : Bool) (hr : r < N) (hk : k < MatrixMultiplication.Schonhage.D m) : matrixAddress L m N side r k < inverseBase L m N

A real matrix cell lies strictly inside its protected snapshot. This uses the real row/column guard, before constructing its flat address.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_readCell {w L m N : ℕ} (side : Bool) (a : Fin (7 ^ L)) (β : ℕ) (x : WordRAM.Data 96) (hx : BandParameters L m N x) (hβ : β < MatrixMultiplication.Schonhage.numBands L m N) (hb : x.regs band = β) (hm : x.regs maskAcc = (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).mask) (ho : x.regs outerAcc = (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).outer) (hi : x.regs innerAcc = (MatrixMultiplication.Schonhage.BandDigits.parts L ↑a).inner) (htable : ∀ t < 2 ^ L, x.mem (inverseBase L m N + t) = MatrixMultiplication.Schonhage.MaskTable.lookup L m t) (matrix : ℕ → ℕ → ℤ) (hmat : ∀ r < N, ∀ k < MatrixMultiplication.Schonhage.D m, x.mem (matrixAddress L m N side r k) = WordRAM.Signed.encode (matrix r k)) (hfit : WordRAM.Fits w (wordBudget L m N)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w (readCell side) x y 24 ∧ y.regs value = WordRAM.Signed.encode (bandValue L m N β side matrix ↑a) ∧ y.mem = x.mem

The complete guarded load uses at most twenty-four actual target instructions. All intermediate products are bounded using the original parameters and the real r<N guard. No hypothesis bounds an arbitrary intermediate machine state.