The dot-product arrays have seven elements. One full F32x4 load consumes four. The final iteration must read exactly three elements from each array.
Pass typed arrays and Ada indexes
Ordinary memory operations accept a typed array such as F32_Array. They also accept the Ada index of the first selected element.
Lane 0 receives Data (Start). The API does not expose an access value or native address in a vector representation.
Use a full operation only for one complete vector
Load and Store require four valid binary32 elements. They do not require 16-byte alignment.
Load_Unaligned and Store_Unaligned have the same extent and no alignment requirement. Their names make that fact explicit at the call site.
Check alignment before an aligned operation
Is_Aligned_16 reports whether Data (Start) has a 16-byte-aligned address. Before calling Load_Aligned or Store_Aligned, confirm that Is_Aligned_16 (Data, Start) returns true.
The aligned operations have a precondition that requires both a full valid extent and 16-byte alignment. A program must meet the precondition even when assertion checks are disabled.
Declare the exact partial extent
Load_Partial reads exactly Count elements and fills remaining lanes with zero. Store_Partial writes exactly Count elements.
If Count is zero, a partial operation does not evaluate an element address or touch memory. It does not perform an out-of-bounds full-vector access and mask the result.
Apply the same rules to Wide vectors
A full F32x8 operation requires eight valid binary32 elements. An aligned Wide operation requires a 32-byte-aligned address. Is_Aligned_32 checks that address.
Wide Load_Partial reads exactly Count elements and zero-fills the remaining lanes. Wide Store_Partial writes exactly Count elements. For F32x8, Count is in the range 0 through 8. Both operations retain the 128-bit zero-count rule.
The Native implementation composes selected 128-bit memory operations across private parts. This composition does not change the public lane order, extent, or alignment contract.
Load the final three dot-product elements
A Lane_Count_32x4 value is in the range 0 through 4. The loop selects the smaller of four lanes and the remaining array extent.
Remaining : constant Natural := Left'Last - Start + 1;
Count : constant Lane_Count_32x4 :=
Lane_Count_32x4'Min (4, Remaining);
Left_Block : constant F32x4 :=
Vector_Load_Partial (Left, Start, Count);
Right_Block : constant F32x4 :=
Vector_Load_Partial (Right, Start, Count);The second iteration uses Count = 3. Each load reads indexes 5 through 7 and places zero in lane 3. The unused product is therefore 0.0 * 0.0.
The loop exits after it consumes the final Remaining elements. It does not calculate an index after Left'Last.
Verify extent separately from values
guard_page_tests places byte tails next to an inaccessible page. It exercises 128-bit partial byte operations for counts 0 through 16 and Wide partial byte operations for counts 0 through 32.
The complete-memory tests check ordinary, unaligned, and aligned loads and stores for all ten 128-bit value types. Independent lane and array expectations cover fixed inputs and 250 deterministic inputs per type. Floating cases include raw IEEE encodings, and store checks preserve sentinel elements outside the complete-vector extent.
The Wide tests cover every memory form for all ten value types. Independent expectations check fixed inputs and 128 deterministic inputs per type. Floating cases use raw bit encodings. Partial tests cover every valid count, preserve sentinel elements outside the store extent, and use Start = Natural'Last when Count is zero. AddressSanitizer builds provide another out-of-bounds check where the toolchain supports them.
A store consumes its vector value before it writes the destination. The API has no raw-address overload in v0.1.