A finite exhaustive native Exact Triangle callee

This reference implementation enumerates the actual triples, loads all three encoded matrix weights, and compares the sums of their positive and negative magnitudes. No solver instruction, host execution premise or precomputed verdict occurs in its code. It is library code because its certification witnesses that Host.Callee can be satisfied by a concrete finite program.

Main definitions

• program: one fixed 24-register native triple scan.
• callee: a concrete certified finite block with charged cubic time and logarithmic width.

This exhaustive native implementation and its certification are original.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.side : Fin 24

Raw number of vertices per part.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.ab : Fin 24

AB matrix pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.bc : Fin 24

BC matrix pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.ac : Fin 24

AC matrix pointer.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.zero : Fin 24

The free-pointer argument is overwritten by zero after entry.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.out : Fin 24

Raw Boolean return value.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.current : Fin 24

Next flattened triple.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.area : Fin 24

Number of cells per matrix.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.stop : Fin 24

Number of triples.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.one : Fin 24

Loop increment.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.two : Fin 24

Sign-and-magnitude radix.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.iReg : Fin 24

First vertex index.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.jReg : Fin 24

Second vertex index.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.kReg : Fin 24

Third vertex index.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.address : Fin 24

Actual matrix-load address.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.word (j : Fin 3) : Fin 24

The three actual loaded edge words.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.positive : Fin 24

Sum of positive magnitudes.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.negative : Fin 24

Sum of negative magnitudes.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.magnitude : Fin 24

Magnitude of the current encoded edge.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.sign : Fin 24

Sign bit of the current encoded edge.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.remainder : Fin 24

Flattened second and third vertex indices.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.accumulate (j : Fin 3) : WordRAM.Code WordRAM.Basis.standard 24

Add one encoded edge to its positive or negative magnitude sum.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.loadTriple : WordRAM.Code WordRAM.Basis.standard 24

Compute three indices and load the three corresponding matrix cells.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.finish : WordRAM.Code WordRAM.Basis.standard 24

Retain a found zero-weight triangle and advance to the next triple.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.body : WordRAM.Code WordRAM.Basis.standard 24

One fully charged triple scan.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.setup : WordRAM.Code WordRAM.Basis.standard 24

Initialize every scratch value used before the first triple.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.program : WordRAM.Code WordRAM.Basis.standard 24

Exhaust all t³ triples using native division/remainder and actual matrix loads.

def Cslib.Algorithms.WordRAM.ThreeSum.Host.Slow.callee : Callee 17

Actual finite cubic-time solver used to inhabit the complete host's callee contract. It preserves all memory, works on arbitrary signed matrices, and never reads physical width.