Computing an ExactTriangle instance catalogue

The fixed input format is (D,g,n,p) followed by the three signed weight matrices. The program computes residues and query classes, computes the splitting parameters from D,g,n, and concatenates the actual query-chunk descriptors. The caller supplies neither the parameters nor a class, prefix or descriptor table. Subsequent matrix preparation consumes this catalogue.

This is native composition of the existing Theorem 17 residue, parameter, class and chunk kernels. The modulus remains a supplied positive argument; prime selection belongs to the outer ExactTriangle host.

Main definitions

• Catalogue.program: fixed thirty-two-register native catalogue computation.
• Catalogue.budget: input-derived numeric bound for arithmetic and allocated addresses.
• Catalogue.cost: charged cost before the final halt.
• Catalogue.Output: computed parameters, residues, queries, descriptors and memory frame.

Main results

• Catalogue.exec_at: actual execution from the fixed input header, exact parameters, residue and query readback, concatenated descriptors and a combined memory frame.

References

The class/query layout follows the pinned Theorem 17 construction. The native composition and instruction bounds are original.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Catalogue.pieceLength : Fin 32

Computed maximum vertices per piece, preserved by descriptor enumeration.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Catalogue.pieces : Fin 32

Computed number of pieces, preserved by descriptor enumeration.

def Cslib.Algorithms.WordRAM.ExactTriangle.Catalogue.parameters : WordRAM.Code WordRAM.Basis.standard 32

Existing parameter computation in the lower register bank.

def Cslib.Algorithms.WordRAM.ExactTriangle.Catalogue.deliverParameters : WordRAM.Code WordRAM.Basis.standard 32

Internal argument delivery from the fixed D,g,n,p header.

def Cslib.Algorithms.WordRAM.ExactTriangle.Catalogue.deliverChunks : WordRAM.Code WordRAM.Basis.standard 32

Internal argument delivery and allocation after the computed query blocks. Copying the count/query pointers precedes overwriting their old registers with the computed piece data.

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

All class, parameter and chunk work is performed by actual native instructions.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.Catalogue.program_fixed : program.size ≤ 320 ∧ ¬program.ReadsWidth

One finite instruction graph, independent of runtime sizes and physical width.

def Cslib.Algorithms.WordRAM.ExactTriangle.Catalogue.budget (n D g p : ℕ) : ℕ

A single explicit bound covering the fourth-power square-root input, all ceiling temporaries and the worst-case descriptor reservation. Signed payloads have a separate bound.

def Cslib.Algorithms.WordRAM.ExactTriangle.Catalogue.cost (n D p : ℕ) : ℕ

Every setup, parameter, signed residue, class scan and descriptor instruction is charged; the final halt is added by the flat caller.

def Cslib.Algorithms.WordRAM.ExactTriangle.Catalogue.Output (n D g p : ℕ) (values : ℕ → ℤ) (initial y : WordRAM.Data 32) : Prop

Exact computed parameters, residue/query arrays, concatenated descriptors and memory frame. This is the readback established by the actual native catalogue execution.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.Catalogue.exec_at {w : ℕ} (n D g p : ℕ) (values : ℕ → ℤ) (initial : WordRAM.Data 32) (hDHeader : initial.mem 1 = D) (hgHeader : initial.mem 2 = g) (hnHeader : initial.mem 3 = n) (hpHeader : initial.mem 4 = p) (hinput : ∀ q < 3 * (n * n), initial.mem (5 + q) = WordRAM.Signed.encode (values q)) (hD : 1 ≤ D) (hDn : D ≤ n) (hg : 1 ≤ g) (hp : 0 < p) (hmod : GenericRAM.Signed.Fits w ↑p) (hvalues : ∀ q < 3 * (n * n), GenericRAM.Signed.Fits w (values q)) (hbudget : WordRAM.Fits (w + 2) (budget n D g p)) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin (w + 2) program initial y (cost n D p) ∧ Output n D g p values initial y

Prepare the actual catalogue at the fixed header, computing both splitting parameters and every class/chunk. The result contains no supplied layout or execution certificates. The two input-dependent fit premises cover ordinary signed values and the explicit numeric budget.