Update master copies of AArch64 arithmetic back-end specs.

Signed-off-by: Rod Chapman <[email protected]>

Author: rod-chapman

dev/aarch64_clean/src/arith_native_aarch64.h

@@ -117,13 +117,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
     requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
@@ -134,13 +138,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
     requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
@@ -151,13 +159,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
     requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)

dev/aarch64_opt/src/arith_native_aarch64.h

@@ -116,13 +116,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k2(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k2.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 2 * MLKEM_N))
     requires(memory_no_alias(b, sizeof(int16_t) * 2 * MLKEM_N))
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 2 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 2 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k3 \
@@ -133,13 +137,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k3(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k3.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 3 * MLKEM_N))
     requires(memory_no_alias(b, sizeof(int16_t) * 3 * MLKEM_N))
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 3 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 3 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_polyvec_basemul_acc_montgomery_cached_asm_k4 \
@@ -150,13 +158,17 @@ void mlk_polyvec_basemul_acc_montgomery_cached_asm_k4(
 /* This must be kept in sync with the HOL-Light specification in
  * proofs/hol_light/arm/proofs/mlkem_poly_basemul_acc_montgomery_cached_k4.ml.
  */
+/* TODO - refine_bounds branch - Check HOL-Light specification has the
+ * INT16_MAX/2 bound on post-condition and re-prove/
+ */
 __contract__(
     requires(memory_no_alias(r, sizeof(int16_t) * MLKEM_N))
     requires(memory_no_alias(a, sizeof(int16_t) * 4 * MLKEM_N))
     requires(memory_no_alias(b, sizeof(int16_t) * 4 * MLKEM_N))
     requires(memory_no_alias(b_cache, sizeof(int16_t) * 4 * (MLKEM_N / 2)))
     requires(array_abs_bound(a, 0, 4 * MLKEM_N, MLKEM_UINT12_LIMIT + 1))
     assigns(memory_slice(r, sizeof(int16_t) * MLKEM_N))
+    ensures(array_abs_bound(r, 0, MLKEM_N, INT16_MAX/2))
 );
 
 #define mlk_rej_uniform_asm MLK_NAMESPACE(rej_uniform_asm)