Native ExactTriangle instance preparation

The input header is (D,g,n,p), followed by the three signed weight matrices. The program first computes the real class/chunk catalogue. It then visits each actual chunk and piece, reads that chunk's descriptor, computes the piece boundaries and writes its record and two zero/one matrices. The records share the already computed query arrays. Every visit uses the existing native InstancePair.program rather than assuming a matrix-preparation routine.

The output records and matrices occupy consecutive variable-size blocks. Register output names the first record, produced gives their actual number and heap is their final allocation end. Each block has six record words followed by 2nD matrix words. This module prepares instances; it does not choose a prime, evaluate their queried products or decide ExactTriangle.

Main definitions

• Instances.program: fixed sixty-four-register initialized instance-preparation program.
• Instances.visit: one computed class/chunk/piece visit, including both native matrix calls.
• Instances.timeBound: the catalogue cost plus the full native visit and loop budgets, including the final halt.
• Instances.Output: actual catalogue, record, matrix and frame readback.

Main results

• Instances.exec_at: complete native execution from the original header and weight arrays.

PreparationInput supplies the initialized flat-program interface and derived width bounds; PreparationBounds proves the preparation time bound in the source's parameter regime. Code-stage definitions are exposed for kernel-checked interpreter clients. Proof helpers are private.

References

The matrix geometry follows the pinned Theorem 17 matrix construction. The native controller and resource proofs are original.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.size : Fin 64

Outer matrix dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.dimension : Fin 64

Target padded middle dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.modulus : Fin 64

Residue modulus.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.pieceLength : Fin 64

Computed maximum vertices per piece.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.pieces : Fin 64

Computed number of pieces.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.chunks : Fin 64

Actual number of nonempty query chunks.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.descriptors : Fin 64

Computed chunk-descriptor array.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.output : Fin 64

First output record.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.produced : Fin 64

Number of completely written instance blocks.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.total : Fin 64

Actual chunk count times piece count.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.heap : Fin 64

Next free output record.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.stride : Fin 64

Words per record and its two matrices.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.one : Fin 64

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.three : Fin 64

Words per chunk descriptor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.six : Fin 64

Words per instance record.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.area : Fin 64

Words in one matrix.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.srcLeft : Fin 64

Original A–C residue matrix.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.srcRight : Fin 64

Original B–C residue matrix.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.addr : Fin 64

Descriptor/header address temporary.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.chunkIndex : Fin 64

Current chunk ordinal.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.pieceIndex : Fin 64

Current piece ordinal.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.rho : Fin 64

Residue loaded from the actual chunk descriptor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.queries : Fin 64

Query pointer loaded from the actual chunk descriptor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.queryCount : Fin 64

Query count loaded from the actual chunk descriptor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.first : Fin 64

First vertex of the current piece.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.length : Fin 64

Actual length of the current piece.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.Instances.temp : Fin 64

Original weight-matrix area temporary.

def Cslib.Algorithms.WordRAM.ExactTriangle.Instances.catalogue : WordRAM.Code WordRAM.Basis.standard 64

Existing catalogue computation in the lower thirty-two registers.

def Cslib.Algorithms.WordRAM.ExactTriangle.Instances.setup : WordRAM.Code WordRAM.Basis.standard 64

Save the actual catalogue outputs and compute the allocation stride and residue bases.

def Cslib.Algorithms.WordRAM.ExactTriangle.Instances.select : WordRAM.Code WordRAM.Basis.standard 64

Compute the chunk and piece ordinals, then load the real query reference and piece bounds.

def Cslib.Algorithms.WordRAM.ExactTriangle.Instances.deliver : WordRAM.Code WordRAM.Basis.standard 64

Deliver every actual pointer, coordinate and count to the existing instance-pair ABI.

def Cslib.Algorithms.WordRAM.ExactTriangle.Instances.pair : WordRAM.Code WordRAM.Basis.standard 64

Existing native record and matrix-pair writer.

def Cslib.Algorithms.WordRAM.ExactTriangle.Instances.advance : WordRAM.Code WordRAM.Basis.standard 64

Advance only after the complete pair has been written.

def Cslib.Algorithms.WordRAM.ExactTriangle.Instances.visit : WordRAM.Code WordRAM.Basis.standard 64

One actual instance; every selection, argument-delivery and matrix instruction is native.

def Cslib.Algorithms.WordRAM.ExactTriangle.Instances.program : WordRAM.Code WordRAM.Basis.standard 64

Prepare every actual chunk/piece pair after computing the catalogue.

def Cslib.Algorithms.WordRAM.ExactTriangle.Instances.timeBound (n D p K H : ℕ) : ℕ

The catalogue prefix, twenty-six setup instructions, each 40nD+66 visit and its two loop instructions, the two loop-exit instructions and the final halt are accounted separately.

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

Original-header bound for all arithmetic and allocated addresses. The conservative maximum p*n² chunk count and n pieces cover every actual catalogue entry. Signed weights have their separate magnitude fit premise; no layout information is supplied by the caller.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.Instances.program_fixed : program.size ≤ 640 ∧ ¬program.ReadsWidth

One bounded instruction graph with no word-size reads.

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

Exact computed catalogue, record and raw zero/one matrix readback, with the complete input/output frame. The matrix predicates reuse the existing writer arguments and entry semantics.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.Instances.exec_at {w : ℕ} (n D g p : ℕ) (values : ℕ → ℤ) (initial : WordRAM.Data 64) (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)) : have N := n * n; have R := fun (q : ℕ) => (values q % ↑p).toNat; have C := fun (rho : ℕ) => Nat.count (fun (q : ℕ) => R q = rho) N; have K := ChunkCatalogue.before C (ExactTriangle.queryCap n D) p; have H := ExactTriangle.numPieces n D g; ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin (w + 2) program initial y (timeBound n D p K H - 1) ∧ Output n D g p values initial y

Execute the complete preparation from the real header and signed matrices. Every output record refers to the actual computed query chunk, followed by its raw zero/one matrix pair. The only resource premises concern the original signed values and the explicit numeric budget; neither a catalogue nor a layout or execution certificate is an input. The final halt is excluded here and added by the initialized flat-program client.