Native matrix pairs and instance records

One call writes a six-word record (rho,piece,queries,count,X,Y) and the actual raw unsigned zero/one matrices X : n×D and Y : D×n immediately after it. Both matrices reuse WriteMatrices.program; all pointer arithmetic, argument delivery and record stores are charged. The query words remain in the earlier computed catalogue and are shared by reference.

setup, writeHeader, deliverLeft, deliverRight and matrix are internal program stages. They are exposed so that the complete catalogue controller can reuse the same fixed program.

Main definitions

• InstancePair.program: fixed thirty-two-register matrix-pair and record writer.
• InstancePair.leftArgs, InstancePair.rightArgs: existing matrix-writer arguments read directly from the runtime registers.

Main results

• InstancePair.exec: both exact matrices and the real record, with a combined outside frame and a 40nD+38 charged instruction bound before halt.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.srcLeft : Fin 32

Computed A–C residue-array pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.srcRight : Fin 32

Computed B–C residue-array pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.base : Fin 32

First word of the instance record.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.size : Fin 32

Outer matrix dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.dimension : Fin 32

Padded middle matrix dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.modulus : Fin 32

Positive residue modulus.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.first : Fin 32

First original vertex in the piece.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.length : Fin 32

Actual number of vertices in the piece.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.rho : Fin 32

Query residue.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.queries : Fin 32

Actual query-pair pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.count : Fin 32

Actual number of query pairs.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.piece : Fin 32

Index of the original piece.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.one : Fin 32

Constant one, preserved by both matrix calls.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.addr : Fin 32

Header cursor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.area : Fin 32

Number of words in one matrix.

def Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.leftArgs (x : WordRAM.Data 32) : WriteMatrices.Args

Existing left-matrix arguments, with its output following the six-word record.

def Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.rightArgs (x : WordRAM.Data 32) : WriteMatrices.Args

Existing right-matrix arguments, immediately following the left matrix.

def Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.setup : WordRAM.Code WordRAM.Basis.standard 32

Compute the left output pointer and matrix area with native arithmetic.

def Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.writeHeader : WordRAM.Code WordRAM.Basis.standard 32

Write the actual query reference and both computed matrix pointers.

def Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.deliverLeft : WordRAM.Code WordRAM.Basis.standard 32

Deliver the seven remaining left-matrix arguments; its destination is already computed.

def Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.deliverRight : WordRAM.Code WordRAM.Basis.standard 32

The left writer preserves its argument registers, so only the source and output pointer change for the right call.

def Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.matrix (side : Bool) : WordRAM.Code WordRAM.Basis.standard 32

Reuse either native matrix writer in the lower seventeen registers.

def Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.program : WordRAM.Code WordRAM.Basis.standard 32

Complete record and matrix-pair construction.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.program_fixed : program.size ≤ 160 ∧ ¬program.ReadsWidth

Finite code independent of every runtime dimension and physical width.

def Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.recordWords (x : WordRAM.Data 32) : Fin 6 → ℕ

Six raw unsigned record words: residue, piece index, shared query pointer/count, then the two computed matrix pointers. Matrix entries themselves are raw zero/one words.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.InstancePair.exec {w : ℕ} (x : WordRAM.Data 32) (L R : ℕ → ℕ) (hrho : x.regs rho < x.regs modulus) (hpiece : x.regs first + x.regs length ≤ x.regs size) (hL : ∀ i < x.regs size * x.regs size, L i < x.regs modulus) (hR : ∀ i < x.regs size * x.regs size, R i < x.regs modulus) (hleft : ∀ i < x.regs size * x.regs size, x.mem (x.regs srcLeft + i) = L i) (hright : ∀ i < x.regs size * x.regs size, x.mem (x.regs srcRight + i) = R i) (hsL : x.regs srcLeft + x.regs size * x.regs size ≤ x.regs base) (hsR : x.regs srcRight + x.regs size * x.regs size ≤ x.regs base) (hfit : WordRAM.Fits w (x.regs base + 6 + 2 * (x.regs size * x.regs dimension) + x.regs srcLeft + x.regs srcRight + 2 * (x.regs size * x.regs size) + 2 * x.regs modulus + 7)) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin w program x y (40 * (x.regs size * x.regs dimension) + 38) ∧ { base := x.regs base, length := 6 }.Realizes y.mem (recordWords x) ∧ ({ base := (leftArgs x).dst, length := x.regs size * x.regs dimension }.Realizes y.mem fun (i : Fin { base := (leftArgs x).dst, length := x.regs size * x.regs dimension }.length) => WriteMatrices.entry false (leftArgs x) L ↑i) ∧ ({ base := (rightArgs x).dst, length := x.regs size * x.regs dimension }.Realizes y.mem fun (i : Fin { base := (rightArgs x).dst, length := x.regs size * x.regs dimension }.length) => WriteMatrices.entry true (rightArgs x) R ↑i) ∧ ∀ (a : ℕ), ¬(x.regs base ≤ a ∧ a < x.regs base + 6 + 2 * (x.regs size * x.regs dimension)) → y.mem a = x.mem a

Write both actual matrices and their shared-query instance record. The source arrays are ordinary residue words before the output region. Existing WriteMatrices.entry supplies the semantics; no adjacency array, execution or time contract is an input. Halt is excluded.