Initialized signed weights to native residue classes

The flat input is an unsigned (n,p) header followed by the signed encodings of the three n×n weight matrices. Native arithmetic allocates a residue array, class counts and disjoint query blocks. The existing signed residue kernel processes every weight before the class scanner reads the A–B residues. Neither residues nor class/layout tables are input certificates.

Main definitions

• ResidueClasses.input: the mixed unsigned-header/signed-weight encoding.
• ResidueClasses.programAt: the same preparation at a fixed caller header offset.
• ResidueClasses.program: fixed thirty-two-register native preparation.
• ResidueClasses.addressBound: explicit arithmetic and allocation bound.

Main results

• ResidueClasses.exec_at: callable execution from a fixed caller header.
• ResidueClasses.exec_input: initialized execution, residues, class counts, queries and frame.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.temp : Fin 32

Header cursor and class-scanner source register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.scanSize : Fin 32

Class-scanner side register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.weightSrc : Fin 32

Signed-residue source register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.weightDst : Fin 32

Signed-residue destination register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.weightLen : Fin 32

Signed-residue length register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.encodedMod : Fin 32

Signed modulus and subsequent class-count pointer register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.scanQueries : Fin 32

Class-scanner query pointer register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.scanModulus : Fin 32

Class-scanner modulus register.

@[reducible, inline]

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

Unsigned side length.

@[reducible, inline]

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

Unsigned positive modulus.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.weights : Fin 32

Start of the signed weights.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.residues : Fin 32

Start of all three unsigned residue matrices.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.counts : Fin 32

Start of the computed class-count array.

@[reducible, inline]

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

Start of the class query blocks.

@[reducible, inline]

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

Area of one weight matrix.

@[reducible, inline]

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

Constant one, preserved by both callees.

def Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.input (n p : ℕ) (values : List ℤ) : List ℕ

Header followed by the three signed weight matrices in A–B, B–C, A–C order.

def Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.addressBoundAt (header n p : ℕ) : ℕ

A fitting value covering every allocation endpoint and temporary for a caller header. The adjacent header cells contain n,p, followed by the three signed matrices.

def Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.addressBound (n p : ℕ) : ℕ

The standard input places its n,p header immediately after the machine's length cell.

def Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.reduce : WordRAM.Code WordRAM.Basis.standard 32

The existing signed residue conversion, including unsigned decoding of each remainder.

def Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.classify : WordRAM.Code WordRAM.Basis.standard 32

Reuse the complete native class scanner.

def Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.setupAt (header : ℕ) : WordRAM.Code WordRAM.Basis.standard 32

Read a fixed caller header and compute all array bases, lengths and the encoded modulus. The offset is a code parameter; the complete ET caller uses one fixed input format.

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

Read the standard initialized input header.

def Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.deliver : WordRAM.Code WordRAM.Basis.standard 32

Deliver the five actual scanner arguments after residue conversion.

def Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.programAt (header : ℕ) : WordRAM.Code WordRAM.Basis.standard 32

Native setup, reduction and enumeration for a fixed caller header.

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

All setup, reduction and enumeration is native code.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.programAt_fixed (header : ℕ) : (programAt header).size ≤ 160 ∧ ¬(programAt header).ReadsWidth

Changing the fixed header offset changes constants but not the instruction graph.

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

Fixed instruction graph, independent of dimensions and physical width.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.exec_at {w : ℕ} (header n p : ℕ) (values : ℕ → ℤ) (initial : WordRAM.Data 32) (hnHeader : initial.mem header = n) (hpHeader : initial.mem (header + 1) = p) (hinput : ∀ q < 3 * (n * n), initial.mem (header + 2 + q) = WordRAM.Signed.encode (values q)) (hp : 0 < p) (hmod : GenericRAM.Signed.Fits w ↑p) (hvalues : ∀ q < 3 * (n * n), GenericRAM.Signed.Fits w (values q)) (haddress : WordRAM.Fits (w + 2) (addressBoundAt header n p)) : have base := header + 2; ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin (w + 2) (programAt header) initial y (69 * (n * n) + p * (14 * (n * n) + 14) + 30) ∧ y.regs residues = base + 3 * (n * n) ∧ y.regs counts = base + 6 * (n * n) ∧ y.regs queries = base + 6 * (n * n) + p ∧ (∀ q < 3 * (n * n), y.mem (base + 3 * (n * n) + q) = (values q % ↑p).toNat) ∧ (∀ j < p, y.mem (base + 6 * (n * n) + j) = Nat.count (fun (q : ℕ) => (values q % ↑p).toNat = j) (n * n)) ∧ (∀ j < p, ∀ q < n * n, (values q % ↑p).toNat = j → y.mem (base + 6 * (n * n) + p + 2 * (n * n) * j + 2 * Nat.count (fun (k : ℕ) => (values k % ↑p).toNat = j) q) = q / n ∧ y.mem (base + 6 * (n * n) + p + 2 * (n * n) * j + 2 * Nat.count (fun (k : ℕ) => (values k % ↑p).toNat = j) q + 1) = q % n) ∧ ∀ (a : ℕ), a < base + 3 * (n * n) ∨ base + 6 * (n * n) + p + 2 * (n * n) * p ≤ a → y.mem a = initial.mem a

Callable residue/class preparation from a concrete caller header and signed matrix words. The fixed offset selects the adjacent n,p cells; no initialized-memory shape is assumed outside that payload. The cost and output frame include every setup, signed reduction and class scan.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.ResidueClasses.exec_input {w : ℕ} (n p : ℕ) (values : List ℤ) (hlen : values.length = 3 * (n * n)) (hp : 0 < p) (hmod : GenericRAM.Signed.Fits w ↑p) (hvalues : ∀ q < values.length, GenericRAM.Signed.Fits w (values.getD q 0)) (haddress : WordRAM.Fits (w + 2) (addressBound n p)) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin (w + 2) program (WordRAM.Data.init (input n p values)) y (69 * (n * n) + p * (14 * (n * n) + 14) + 30) ∧ y.regs residues = 3 + 3 * (n * n) ∧ y.regs counts = 3 + 6 * (n * n) ∧ y.regs queries = 3 + 6 * (n * n) + p ∧ (∀ q < 3 * (n * n), y.mem (3 + 3 * (n * n) + q) = (values.getD q 0 % ↑p).toNat) ∧ (∀ j < p, y.mem (3 + 6 * (n * n) + j) = Nat.count (fun (q : ℕ) => (values.getD q 0 % ↑p).toNat = j) (n * n)) ∧ (∀ j < p, ∀ q < n * n, (values.getD q 0 % ↑p).toNat = j → y.mem (3 + 6 * (n * n) + p + 2 * (n * n) * j + 2 * Nat.count (fun (k : ℕ) => (values.getD k 0 % ↑p).toNat = j) q) = q / n ∧ y.mem (3 + 6 * (n * n) + p + 2 * (n * n) * j + 2 * Nat.count (fun (k : ℕ) => (values.getD k 0 % ↑p).toNat = j) q + 1) = q % n) ∧ ∀ (a : ℕ), a < 3 + 3 * (n * n) ∨ 3 + 6 * (n * n) + p + 2 * (n * n) * p ≤ a → y.mem a = (WordRAM.Data.init (input n p values)).mem a

Read the input header, compute all three residue matrices and enumerate the A–B queries. The signed width is w, and execution uses the existing signed compiler's w+2 unsigned width. The cost includes every header, reduction, argument-delivery and class-scan instruction; the final halt is excluded. This subroutine does not choose a prime or solve an instance.