Charged bound for native wanted-query grouping

Main definitions

• Wanted.timeBound: sum of actual parameter/table, zero/count, prefix and scatter charges.

Main results

• Wanted.timeBound_add_one_le: a bound polynomial in depth times query, tile and mask counts.

These are original instruction bounds for the native implementation. Actual executions are proved separately; no execution or complexity certificate is an input to the program.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.timeBound (L m N Q : ℕ) : ℕ

Prefix instruction budget, before the final flat halt. All initialization and loops count.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.timeBound_add_one_le (L m N Q : ℕ) : timeBound L m N Q + 1 ≤ 128 * (L + 1) * (Q + MatrixMultiplication.Schonhage.numBands L m N ^ 2 + 2 ^ L + 1)

Including halt, routing is polynomial in depth times the original query, tile and subset-table sizes. In particular it does not scan 10^L cells per query or tile.