Calling a queried product from an actual prepared record

The low 64 producer registers are retained. Register 64 selects an actual record ordinal; the native code computes its stride, reads its six words and places the original raw matrices and interleaved query coordinates at the actual producer heap end. The complete callable product occupies a separate 163-register bank. Its existing matrix-input code, not this adapter, performs raw-zero/one to canonical-signed doubling.

The logarithm is computed by NatLog.program. Under D=4^m, dividing its binary result by two recovers m exactly. No layout, logarithm, execution or solver certificate is a runtime input. These definitions are internal stages of the complete record consumer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.ordinal : Fin 320

Actual record ordinal supplied by the outer caller.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.result : Fin 320

Absolute result pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.base : Fin 320

Actual producer heap end, and the callee's local-memory base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.dimension : Fin 320

Original padded middle dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.size : Fin 320

Original outer dimension.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.record : Fin 320

Computed selected record pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.rho : Fin 320

Loaded residue and piece metadata, retained without reinterpreting them.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.piece : Fin 320

Loaded piece index.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.queries : Fin 320

Loaded interleaved query pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.count : Fin 320

Loaded number of query occurrences.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.left : Fin 320

Loaded left-matrix pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.right : Fin 320

Loaded right-matrix pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.area : Fin 320

Computed size of either matrix block.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.twiceArea : Fin 320

Computed combined matrix-block length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.depth : Fin 320

Recovered inner depth.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.level : Fin 320

Computed tensor level, nineteen times the inner depth.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.payloadLength : Fin 320

Computed original callee payload length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.one : Fin 320

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.two : Fin 320

Constant two.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.six : Fin 320

Record header length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.nineteen : Fin 320

Tensor-level multiplier.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.four : Fin 320

Original callee scalar header length.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.address : Fin 320

Adapter address scratch.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.source : Fin 320

Temporary source pointer, also the logarithm input.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.destination : Fin 320

Temporary destination pointer, also the logarithm result.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.Reg.length : Fin 320

Temporary copy length.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.logBank (i : Fin 4) : Fin 320

The logarithm and copy routines share an adapter-local temporary register bank.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.copyBank (i : Fin 7) : Fin 320

All seven registers of the real array-copy routine are relocated together.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.calleeBank (i : Fin 163) : Fin 320

The complete callable product bank is disjoint from producer and adapter registers.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.readRecord : WordRAM.Code WordRAM.Basis.standard 320

Compute the record pointer and read every actual descriptor field.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.logarithm : WordRAM.Code WordRAM.Basis.standard 320

Recover the exact power-of-four exponent with the existing charged binary logarithm.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.writeHeader : WordRAM.Code WordRAM.Basis.standard 320

Write the complete original local input header, including its length word.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.deliverLeft : WordRAM.Code WordRAM.Basis.standard 320

Deliver real source and destination pointers for the left-matrix copy.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.deliverRight : WordRAM.Code WordRAM.Basis.standard 320

The right block follows the left destination block.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.deliverQueries : WordRAM.Code WordRAM.Basis.standard 320

Preserve each query occurrence's two original raw coordinates, in its original order.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.copy : WordRAM.Code WordRAM.Basis.standard 320

Real copying, with every address calculation, load/store and loop instruction charged.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.copyInputs : WordRAM.Code WordRAM.Basis.standard 320

Three actual copies; no catalogue or virtual-window snapshot is made.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.invoke : WordRAM.Code WordRAM.Basis.standard 320

Runtime memory rebasing is provided by the callee; renaming moves only its registers.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.prepare : WordRAM.Code WordRAM.Basis.standard 320

Runtime preparation prefix, useful for admitted decoder/copy tests without the full solver.

def Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.program : WordRAM.Code WordRAM.Basis.standard 320

One selected actual producer record, including all copying and the complete native callee.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.program_fixed : program.size ≤ 131584 ∧ ¬program.ReadsWidth

One fixed finite native program, independent of dimensions, record ordinal and word width.