Row-major packing indices #
These laws reduce the dependent coordinate equivalence used by pack and
unpack to flat row-major arithmetic. Native lowering uses the compact
formula, while correctness remains stated against the independent coordinate
semantics.
The concatenated segment index is the local index plus the lengths of all preceding segments.
Concatenating one segment into a packed axis has the expected row-major flat index: trailing coordinates are least significant, followed by the packed axis and then the leading coordinates.
The checked component-to-packed equivalence has a compact row-major formula.
Total packed-axis length occupied by components before component.
Instances For
Summing the segments before a component is the ordinary list-prefix sum.
This form is convenient for compilation because a concrete checked plan can evaluate the prefix once instead of traversing a finite sum for every scalar.
Compute a packed flat index directly from one component's flat index.
The trailing coordinates occupy the low-order digits, the component's star
region occupies the next digits, and the shared leading coordinates occupy
the high-order digits. offset is the total length of preceding components.
Instances For
Within one component row, unpack's direct mixed-radix index is a contiguous slice of the corresponding packed row.
This is the arithmetic fact used by native block unpack: row selects the
shared leading coordinate and column ranges across the component's complete
star-and-trailing block.
Compute one component-local flat index from a packed flat index.
The packed-axis position selects a segment. Subtracting that segment's compile-time prefix recovers the local star coordinate, while the leading and trailing coordinates retain their row-major positions.
Instances For
The direct component index lies inside the selected component buffer.
The selected packed-axis interval bounds the local star coordinate, while the packed output bound controls the leading coordinate. Applying the row-major encoding bound twice then accounts for the trailing coordinate.
The direct component index respects equality of its compile-time segment data.
Native pack lowering specializes the shapes, packed length, and component offset to literals while retaining the checked expression as its proof reference.
The direct component index is a left inverse of the verified unpack index inside the selected packed-axis segment.
This theorem is independent of component count. Native pack lowering uses one instance per generated segment branch.
The direct unpack index respects equality of its compile-time segment data.
This theorem lets elaboration specialize checked shapes, lengths, and offsets to literals without unfolding the arithmetic program in generated proofs.
Compute the packed flat index corresponding to one component flat index.
The definition is intentionally operation-level rather than compiler-level: it remains valid for symbolic shapes and is independently related to the checked coordinate semantics below.
Instances For
The direct mixed-radix formula agrees with the coordinate-based compact unpack index.
The compact unpack index is exactly the flat index selected by the independent packed-coordinate equivalence.
The compact unpack index is always inside the packed output buffer.
The compact unpack index as a bounded flat map into the packed tensor.
Instances For
The compact unpack map is the row-major form of the independent coordinate embedding.
One unpacked component is exactly a flat pullback through the compact segment index.
A bounded component-local index obtained from the direct inverse formula maps back to the packed output index that selected it.
The component interval hypotheses are exactly the facts established by one branch of native pack's generated segment dispatcher.
Specialize the inverse pack index through literal segment metadata.
Native lowering computes shapes, packed length, and the component prefix once during elaboration. This theorem transports those literal facts to the checked plan before invoking the general inverse law.
Reading a packed output through a component index is the inverse of the verified unpack flat map.
Native pack lowering uses this theorem after selecting one concrete segment: it only needs to prove that the generated component index maps back to the current packed output index.