Native execution of the encoding forms #
The form code reads seven strided entries and uses only the existing native signed arithmetic blocks. These results account for those blocks' actual instructions and their scratch registers.
Main results #
Encoding.exec_summand: a coefficient in{0, 1, -1}takes at most 23 instructions.
References #
The linear forms are from [AlmanWilliams2026, Section 2.4.1]; see Encoding for provenance.
Registers outside the signed workspace and the form's three local registers.
Instances For
Form frames compose without changing any memory cell.
A single coefficient is executed by real loads and signed arithmetic. The seven address computations fit whenever the one-past-end address fits. The two operands must fit the signed source range; the sum itself may use the two extra target bits supplied by the arithmetic block.
Execute any finite list of the fixed digit/coefficients. Partial sums are bounded by
|a| + length * B; the theorem derives each arithmetic operand's fit from that inequality.
A complete coefficient row, including initialization, costs at most 163 instructions.
All seven entries have absolute value at most B, so every partial sum has magnitude at
most 7B; this ordinary explicit width condition is sufficient for every signed operation.
The finite term dispatch costs at most three instructions per inspected row in addition to the row's 163-instruction bound. All ten forms share the same native register file.