Fixed native code for pruned tensor queries

The controller uses an explicit depth-first stack. Query and value directories have one row per depth. A shared timestamp directory deduplicates child suffixes without clearing a dense array at every node. Encoded products and sums use the existing native signed kernels.

Main definitions

• PrunedQuery.kernel: evaluator with explicit caller-supplied array and scratch addresses.
• PrunedQuery.program: initialized-input wrapper computing all addresses from the depth and query-count headers.

Client execution interfaces are exec_kernel in Pruned.Kernel, runs and runs_bilinear in Pruned.Flat, and runs_wide in Pruned.Width. Other stage exec_* lemmas and controller invariants under Pruned/ are internal implementation APIs. They are public to compose proofs across the stage modules, rather than intended as independent caller contracts.

References

The query-set recursion is from [AlmanWilliams2026, Section 2.4.2], selectively adapted from Anthropic's formal-math revision 16a5ce41304fcdaea4e0be7c132e1c361dc26da5, pinned source. The explicit iterative stack and timestamp implementation are new native code; the source machine is not imported.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.registers : ℕ

The program has a fixed register bank, including nine signed-arithmetic scratch registers.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.inputDepth : Fin registers

Original tensor depth, loaded from the ordinary input header.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.span : Fin registers

Computed encoding-array length and per-depth directory capacity, 10^L.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.arrayA : Fin registers

Pointer to the left canonical signed encoding array.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.arrayB : Fin registers

Pointer to the right canonical signed encoding array.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queries : Fin registers

Pointer to the original unsigned query-code list, including repeats.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.queryCount : Fin registers

Number of supplied queries, before native deduplication.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.output : Fin registers

Pointer to the answer list, in the original query order.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scratch : Fin registers

Caller-supplied start of the explicit stack and directory workspace.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.epoch : Fin registers

Current timestamp generation for native query deduplication.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.frames : Fin registers

Pointer to the first four-word stack frame.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.lists : Fin registers

Pointer to the first per-depth distinct-query row.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.values : Fin registers

Pointer to the first per-depth signed-value row.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.stamps : Fin registers

Pointer to the shared query-membership timestamp directory.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.level : Fin registers

Current stack depth, with zero denoting the root.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.mode : Fin registers

Controller phase: zero for entry, one for dispatch, two for returned-child accumulation.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.active : Fin registers

Traversal flag; returning from the root sets this to zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.one : Fin registers

Raw unsigned constant one for counters and offsets.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ten : Fin registers

Raw unsigned radix ten for the fixed term and query dictionaries.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.nine : Fin registers

Inner-output wildcard digit, in the existing term numbering.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.frameWidth : Fin registers

Raw unsigned width of a stack frame: four words.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.frame : Fin registers

Address of the currently loaded stack frame.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.count : Fin registers

Number of distinct requests stored in the current frame.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.leafPrefix : Fin registers

Processed least-significant leaf digits of the current node.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.stride : Fin registers

Place value of the next leaf digit, 10^level.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.term : Fin registers

Next term number to dispatch or accumulate.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.index : Fin registers

Loop counter for powers, scans, clearing, accumulation and reporting.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childCount : Fin registers

Distinct child count computed by the actual timestamp scan.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.query : Fin registers

Current numerical output-string code loaded from a query list.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.digit : Fin registers

First output digit computed by remainder modulo ten.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.suffix : Fin registers

Remaining output digits computed by division by ten.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.address : Fin registers

Scratch address used by native indexed loads and stores.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.temporary : Fin registers

Scratch word for arithmetic, branch fallbacks and loaded values.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.temporary₂ : Fin registers

Scratch word for row-size and address products.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.marker : Fin registers

Timestamp loaded from the membership directory.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.listBase : Fin registers

Address of the current depth's request row.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.valueBase : Fin registers

Address of the current depth's accumulator row.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childList : Fin registers

Address of the next depth's computed request row.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childValues : Fin registers

Address of the next depth's returned-value row.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.nextLevel : Fin registers

Computed child stack depth.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childFrame : Fin registers

Computed address of the frame about to be pushed.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childPrefix : Fin registers

Computed leaf prefix of the child about to be pushed.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childStride : Fin registers

Computed leaf place value for the child about to be pushed.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.nil : Fin registers

Raw unsigned constant zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.two : Fin registers

Raw unsigned constant two, initialized with the fixed scalar constants.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.powerSetup : WordRAM.Code WordRAM.Basis.standard registers

Constant initialization, before the depth-controlled power loop.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.powerStep : WordRAM.Code WordRAM.Basis.standard registers

One charged power multiplication and counter increment.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.powers : WordRAM.Code WordRAM.Basis.standard registers

Initialize constants and compute the actual encoding-array length 10^L.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.locate : WordRAM.Code WordRAM.Basis.standard registers

Separate stack frames, query lists, value directories and membership timestamps.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.emit : WordRAM.Code WordRAM.Basis.standard registers

Append one previously unseen suffix and mark it with the current epoch.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.putSuffix (child : Bool) : WordRAM.Code WordRAM.Basis.standard registers

The two fixed suffix kernels either divide a selected child query or copy a root query.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.selectSuffix : WordRAM.Code WordRAM.Basis.standard registers

A selected child suffix is computed by an actual unsigned division.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scanLoad : WordRAM.Code WordRAM.Basis.standard registers

Load the next supplied query and compute its actual first digit.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scanDispatch (child : Bool) : WordRAM.Code WordRAM.Basis.standard registers

Root queries are copied directly; child queries are filtered by the native digit tests.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scanStep (child : Bool) : WordRAM.Code WordRAM.Basis.standard registers

One deduplicating scan step, including input indexing, dispatch and counter increment.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scanSetup : WordRAM.Code WordRAM.Basis.standard registers

Initialize one query scan with a genuinely fresh native epoch.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scan (child : Bool) : WordRAM.Code WordRAM.Basis.standard registers

Scan and deduplicate an explicit source list.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.rootScanSetup : WordRAM.Code WordRAM.Basis.standard registers

Point the deduplicating root scan at the actual supplied query list.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.rootFinish : WordRAM.Code WordRAM.Basis.standard registers

Store the four actual root-frame words and enter its first controller phase.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.rootList : WordRAM.Code WordRAM.Basis.standard registers

Deduplicate supplied queries into the root list; the original list remains read-only.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.loadFrame : WordRAM.Code WordRAM.Basis.standard registers

Load the current frame and compute its depth-specific list/value addresses.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.pop : WordRAM.Code WordRAM.Basis.standard registers

Return to the parent's accumulation phase, or finish the root.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.leafLoad : WordRAM.Code WordRAM.Basis.standard registers

Load both actual encoded words at the current leaf prefix.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.leafProduct : WordRAM.Code WordRAM.Basis.standard registers

One requested leaf product, using the existing native signed multiplication kernel.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.leaf : WordRAM.Code WordRAM.Basis.standard registers

Evaluate a requested leaf from the actual two encoded words.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.clearValueStep : WordRAM.Code WordRAM.Basis.standard registers

One actual indexed store for an explicitly listed requested value.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.clearRequested : WordRAM.Code WordRAM.Basis.standard registers

Clear exactly the requested parent values, not the full dense directory.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.storeTerm : WordRAM.Code WordRAM.Basis.standard registers

Store the actual next-term counter and enter the frame's dispatch phase.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.clearValuesFinish : WordRAM.Code WordRAM.Basis.standard registers

Initialize the stored next-term counter after sparse accumulator clearing.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.clearValues : WordRAM.Code WordRAM.Basis.standard registers

Initialize requested values and the frame's next-term counter.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.enter : WordRAM.Code WordRAM.Basis.standard registers

Entry phase: multiply at a leaf; otherwise initialize the requested accumulators.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.buildChild : WordRAM.Code WordRAM.Basis.standard registers

Form and deduplicate a child request set using actual tests, loads and stores.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.advance : WordRAM.Code WordRAM.Basis.standard registers

Advance the parent's term after an empty child or after accumulating its returned values.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.push : WordRAM.Code WordRAM.Basis.standard registers

Push a nonempty child, with the exact least-significant-first leaf leafPrefix.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.dispatch : WordRAM.Code WordRAM.Basis.standard registers

Dispatch the next of the ten actual terms, recursing only on nonempty computed sets.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.addValueLoad : WordRAM.Code WordRAM.Basis.standard registers

Load the two encoded operands at the actual parent query and child suffix addresses.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.addValueStore : WordRAM.Code WordRAM.Basis.standard registers

Store the signed sum back at the computed parent query address.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.addValue : WordRAM.Code WordRAM.Basis.standard registers

Add one returned child value to its parent's actual signed accumulator.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.accumulateDispatch : WordRAM.Code WordRAM.Basis.standard registers

Select the returned child by the same two real digit comparisons as child construction.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.accumulateStep : WordRAM.Code WordRAM.Basis.standard registers

Load, dispatch and advance one actual parent query.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.accumulateLoop : WordRAM.Code WordRAM.Basis.standard registers

Consume a returned child's values at the explicitly listed contributing parent queries.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.accumulate : WordRAM.Code WordRAM.Basis.standard registers

Traverse the parent requests once, then advance the stored term counter.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.step : WordRAM.Code WordRAM.Basis.standard registers

One explicit-stack controller step. Every branch and frame address is native work.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.reportStep : WordRAM.Code WordRAM.Basis.standard registers

One actual lookup and indexed output store, including the reporting counter.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.report : WordRAM.Code WordRAM.Basis.standard registers

Report results in the original input query order, including repeated queries.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.controller : WordRAM.Code WordRAM.Basis.standard registers

The common stack evaluator after powers and caller parameters have been initialized.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.work : WordRAM.Code WordRAM.Basis.standard registers

Evaluate the computed root, then report the original query list.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.kernel : WordRAM.Code WordRAM.Basis.standard registers

Generic native evaluator with explicit pointer arguments and a fresh timestamp epoch.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.header : WordRAM.Code WordRAM.Basis.standard registers

Load the two ordinary scalar input headers.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.parameters : WordRAM.Code WordRAM.Basis.standard registers

Compute all initial array/output/scratch pointers from the actual array and query lengths.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.program : WordRAM.Code WordRAM.Basis.standard registers

One finite program reading the header and encoded arrays from ordinary initialized memory.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.not_readsWidth : ¬program.ReadsWidth

The same program is used at every word width; it never reads the physical word size.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.program_length_le : List.length (program.program output) ≤ 4096

A fixed bound on both control code and all arithmetic blocks, including the final halt.