Correct bound pre-condition on basemul_cached()

rod-chapman · rod-chapman · commit b5bde83ed175 · 2025-01-17T13:31:47.000Z
Signed-off-by: Rod Chapman &lt;rodchap@amazon.com&gt;
diff --git a/mlkem/poly.c b/mlkem/poly.c
@@ -488,7 +488,7 @@ __contract__(
   requires(memory_no_alias(r, 2 * sizeof(int16_t)))
   requires(memory_no_alias(a, 2 * sizeof(int16_t)))
   requires(memory_no_alias(b, 2 * sizeof(int16_t)))
-  requires(array_abs_bound(a, 0, 2, UINT12_LIMIT))
+  requires(array_bound(a, 0, 2, 0, UINT12_LIMIT))
   assigns(memory_slice(r, 2 * sizeof(int16_t)))
   ensures(array_abs_bound(r, 0, 2, 2 * MLKEM_Q))
 )

Original file line number	Diff line number	Diff line change
`@@ -488,7 +488,7 @@ __contract__(`
`488`	`488`	`requires(memory_no_alias(r, 2 * sizeof(int16_t)))`
`489`	`489`	`requires(memory_no_alias(a, 2 * sizeof(int16_t)))`
`490`	`490`	`requires(memory_no_alias(b, 2 * sizeof(int16_t)))`
`491`		`- requires(array_abs_bound(a, 0, 2, UINT12_LIMIT))`
	`491`	`+ requires(array_bound(a, 0, 2, 0, UINT12_LIMIT))`
`492`	`492`	`assigns(memory_slice(r, 2 * sizeof(int16_t)))`
`493`	`493`	`ensures(array_abs_bound(r, 0, 2, 2 * MLKEM_Q))`
`494`	`494`	`)`