Touch only the declared extent.

Map lane zero to the first element

The memory contract for Flyology_SIMD is logical, not machine-endian. Lane zero receives the element at Start. Lane one receives the next array element.

Use full access for one complete vector

Load and Store require one full vector of valid elements. These operations make no alignment assertion.

The explicitly named Load_Unaligned and Store_Unaligned operations have the same extent requirement. Their names make the absence of an alignment requirement visible at the call site.

declare
   Block : constant Flyology_SIMD.U8x16 :=
     Flyology_SIMD.Load_Unaligned (Data, Start);
begin
   Flyology_SIMD.Store_Unaligned (Output, Start, Block);
end;

Prove alignment before aligned access

Is_Aligned_16 checks the address of the selected first element. Load_Aligned and Store_Aligned require 16-byte alignment and a full valid extent.

When assertion checks are enabled, the Ada precondition detects a contract violation. A caller must still satisfy the precondition when checks are disabled.

Use partial access for every tail length

Load_Partial reads exactly Count elements and zero-fills the remaining lanes. A zero count reads no element.

Store_Partial writes exactly Count elements. It does not modify elements outside the caller-declared valid extent, and a zero count writes nothing.

Handle the final elements directly

Compute the number of remaining logical elements before the call. Pass that count to the partial operation.

declare
   Remaining : constant Flyology_SIMD.Lane_Count_8x16 :=
     Flyology_SIMD.Lane_Count_8x16 (Data'Last - Start + 1);
   Tail : constant Flyology_SIMD.U8x16 :=
     Flyology_SIMD.Load_Partial (Data, Start, Remaining);
begin
   --  Process Tail. Lanes Remaining through 15 contain zero.
   null;
end;

Do not round the valid extent up to a vector width. The partial operation exists so the caller can preserve the exact boundary.