@@ -720,9 +720,10 @@ Safety argument:
720720 unaligned intrinsics, so no alignment precondition is required.
721721- The SSSE3/SSE4.1 target-feature contract enables every intrinsic used by
722722 the prototype.
723- - The prototype copies only the validated decoded length to caller output and
724- wipes local value, packed, and scalar-validation staging buffers before
725- returning.
723+ - The prototype copies only the validated decoded length to caller output after
724+ an unconditional release-mode equality check proves the vector-packed prefix
725+ matches the scalar-validation prefix. It wipes local value, packed, and
726+ scalar-validation staging buffers before returning.
726727- Runtime decode dispatch does not call this function. Future admission must
727728 update this inventory, generated-code evidence, fuzzing, backend reporting,
728729 benchmarks, and release notes in the same commit that makes any decode SIMD
@@ -784,9 +785,10 @@ Safety argument:
784785 prototype.
785786- VBMI compaction indices are constants in ` 0..=59 ` , so the permute reads only
786787 bytes produced by the lane-local decode shuffle.
787- - The prototype copies only the validated decoded length to caller output and
788- wipes local value, packed, and scalar-validation staging buffers before
789- returning.
788+ - The prototype copies only the validated decoded length to caller output after
789+ an unconditional release-mode equality check proves the vector-packed prefix
790+ matches the scalar-validation prefix. It wipes local value, packed, and
791+ scalar-validation staging buffers before returning.
790792- Runtime decode dispatch does not call this function. Future admission must
791793 update this inventory, generated-code evidence, fuzzing, backend reporting,
792794 benchmarks, and release notes in the same commit that makes any decode SIMD
@@ -846,9 +848,10 @@ Safety argument:
846848- AVX2 byte shuffle is lane-local, so the prototype explicitly compacts the
847849 second 12-byte decoded lane from offsets ` 16..28 ` to ` 12..24 ` inside local
848850 staging before copying to caller output.
849- - The prototype copies only the validated decoded length to caller output and
850- wipes local value, packed, and scalar-validation staging buffers before
851- returning.
851+ - The prototype copies only the validated decoded length to caller output after
852+ an unconditional release-mode equality check proves the vector-packed prefix
853+ matches the scalar-validation prefix. It wipes local value, packed, and
854+ scalar-validation staging buffers before returning.
852855- Runtime decode dispatch does not call this function. Future admission must
853856 update this inventory, generated-code evidence, fuzzing, backend reporting,
854857 benchmarks, and release notes in the same commit that makes any decode SIMD
@@ -977,7 +980,9 @@ Safety argument:
977980 prototype copies bytes to caller-visible output.
978981- The input and output array types provide fixed readable and writable bounds.
979982- The vector store writes only to a local 16-byte packed buffer; the caller
980- output receives at most the scalar-validated ` written ` prefix.
983+ output receives at most the scalar-validated ` written ` prefix, and only after
984+ an unconditional release-mode equality check proves the vector-packed prefix
985+ matches the scalar-validation prefix.
981986- The compaction mask contains only valid source indices or zero lanes.
982987- Staging, packed, and scalar-output buffers are wiped before successful return
983988 or along the error path.
0 commit comments