Native zero/one matrices for an Exact Triangle instance

The input contains ordinary unsigned residues. Each output cell computes its row, middle vertex and label through charged division/remainder instructions. Cells outside the selected piece are zero; all other cells test the required modular adjacency. The same seventeen registers serve the left n×D and right D×n matrices, with no supplied indexing table.

The X/Y output entries are raw unsigned words 0 and 1. A consumer using canonical Signed.encode matrix entries must double each entry while copying it into that input and charge the conversion instruction. Scalar headers, pointers and query coordinates remain raw unsigned words.

This directly adapts the adjacency formulas in the pinned Theorem 17 instance builder. The native implementation visits each output cell once; the source clears and then marks cells.

Main definitions

• WriteMatrices.Args: matrix dimensions, residue/piece parameters and memory blocks.
• WriteMatrices.entry: the zero/one value at a flat output position.
• WriteMatrices.program: fixed native left/right matrix builders.

Main results

• WriteMatrices.exec: complete charged execution and the output/input frame.

structure Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.Args : Type

Runtime arguments of one matrix-building call.

• src : ℕ

  Residue matrix base.

• dst : ℕ

  Output matrix base.

• n : ℕ

  Number of vertices in each outer part.

• D : ℕ

  Padded middle dimension.

• p : ℕ

  Positive modulus.

• first : ℕ

  First vertex of the selected piece.

• length : ℕ

  Number of vertices in the piece.

• rho : ℕ

  A–B query residue.

def Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.entry (rightSide : Bool) (A : Args) (R : ℕ → ℕ) (q : ℕ) : ℕ

Raw unsigned zero/one row-major adjacency. A true side chooses the right D×n matrix; false chooses the left n×D matrix. The source residue matrix has shape n×n. A signed-matrix consumer encodes these entries by doubling them.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.src : Fin 17

Residue input pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.dst : Fin 17

Output matrix pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.size : Fin 17

Outer dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.dimension : Fin 17

Middle dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.modulus : Fin 17

Modulus.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.first : Fin 17

First vertex of the piece.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.length : Fin 17

Piece length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.rho : Fin 17

Query residue.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.idx : Fin 17

Flat output cursor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.area : Fin 17

Number of output cells.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.line : Fin 17

Selected source row.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.vertex : Fin 17

Selected vertex within the piece.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.label : Fin 17

Middle label.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.addr : Fin 17

Address temporary.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.value : Fin 17

Residue and output value temporary.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.zero : Fin 17

Constant zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.one : Fin 17

Constant one.

structure Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.Entry (A : Args) (x : WordRAM.Data 17) : Prop

The eight runtime arguments occupy registers 0–7.

• src : x.regs WriteMatrices.src = A.src

  Source pointer.

• dst : x.regs WriteMatrices.dst = A.dst

  Destination pointer.

• size : x.regs WriteMatrices.size = A.n

  Outer dimension.

• dimension : x.regs WriteMatrices.dimension = A.D

  Middle dimension.

• modulus : x.regs WriteMatrices.modulus = A.p

  Modulus.

• first : x.regs WriteMatrices.first = A.first

  First vertex.

• length : x.regs WriteMatrices.length = A.length

  Piece length.

• rho : x.regs WriteMatrices.rho = A.rho

  Query residue.

def Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.indices (rightSide : Bool) : WordRAM.Code WordRAM.Basis.standard 17

Compute the source row and decode the middle label using actual arithmetic instructions.

def Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.readLabel (rightSide : Bool) : WordRAM.Code WordRAM.Basis.standard 17

Read the selected residue and form its required label.

def Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.body (rightSide : Bool) : WordRAM.Code WordRAM.Basis.standard 17

Write one zero/one cell and increment the flat cursor.

def Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.program (rightSide : Bool) : WordRAM.Code WordRAM.Basis.standard 17

The complete builder initializes constants and visits all output positions once.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.program_fixed (rightSide : Bool) : (program rightSide).size ≤ 64 ∧ ¬(program rightSide).ReadsWidth

The instruction graph has fixed size and never reads the physical word width.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.WriteMatrices.exec {w : ℕ} (side : Bool) (A : Args) (R : ℕ → ℕ) (x : WordRAM.Data 17) (hx : Entry A x) (hrho : A.rho < A.p) (hpiece : A.first + A.length ≤ A.n) (hR : ∀ i < A.n * A.n, R i < A.p) (hinput : ∀ i < A.n * A.n, x.mem (A.src + i) = R i) (hsrc : WordRAM.Fits w (A.src + A.n * A.n)) (hdst : WordRAM.Fits w (A.dst + A.n * A.D)) (hmod : WordRAM.Fits w (2 * A.p)) (hdisj : A.src + A.n * A.n ≤ A.dst) : ∃ (y : WordRAM.Data 17), WordRAM.ExecWithin w (program side) x y (20 * (A.n * A.D) + 6) ∧ Entry A y ∧ y.regs idx = A.n * A.D ∧ ({ base := A.dst, length := A.n * A.D }.Realizes y.mem fun (i : Fin { base := A.dst, length := A.n * A.D }.length) => entry side A R ↑i) ∧ ∀ (a : ℕ), ¬{ base := A.dst, length := A.n * A.D }.Owns a → y.mem a = x.mem a

Construct every entry of a left or right instance matrix in 20nD+6 native instructions, excluding the halt. The source is an actual residue array below the output. All cells outside the output block and all eight arguments are preserved. No adjacency table is supplied.