HOL-Light: add rej_uniform_eta proofs for AArch64

.github/workflows/hol_light.yml

@@ -103,6 +103,10 @@ jobs:
             needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
           - name: poly_use_hint_88_aarch64_asm
             needs: ["mldsa_specs.ml", "aarch64_utils.ml", "subroutine_signatures.ml"]
+          - name: rej_uniform_eta2_aarch64_asm
+            needs: ["mldsa_specs.ml", "aarch64_utils.ml", "mldsa_rej_uniform_eta_table.ml", "subroutine_signatures.ml"]
+          - name: rej_uniform_eta4_aarch64_asm
+            needs: ["mldsa_specs.ml", "aarch64_utils.ml", "mldsa_rej_uniform_eta_table.ml", "subroutine_signatures.ml"]
           - name: keccak_f1600_x1_scalar_aarch64_asm
             needs: ["keccak_spec.ml", "keccak_constants.ml", "subroutine_signatures.ml"]
           - name: keccak_f1600_x1_v84a_aarch64_asm

dev/aarch64_clean/src/arith_native_aarch64.h

@@ -114,15 +114,39 @@ __contract__(
   MLD_NAMESPACE(rej_uniform_eta2_aarch64_asm)
 MLD_MUST_CHECK_RETURN_VALUE
 uint64_t mld_rej_uniform_eta2_aarch64_asm(int32_t *r, const uint8_t *buf,
-                                          unsigned buflen,
-                                          const uint8_t *table);
+                                          unsigned buflen, const uint8_t *table)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/rej_uniform_eta2_aarch64_asm.ml */
+__contract__(
+  requires(buflen % 8 == 0)
+  requires(buflen >= 8)
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, buflen))
+  requires(table == mld_rej_uniform_eta_table)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(return_value <= MLDSA_N)
+  /* check-magic: 3 == 2 + 1 (asm is eta=2-specific) */
+  ensures(array_abs_bound(r, 0, return_value, 3))
+);
 
 #define mld_rej_uniform_eta4_aarch64_asm \
   MLD_NAMESPACE(rej_uniform_eta4_aarch64_asm)
 MLD_MUST_CHECK_RETURN_VALUE
 uint64_t mld_rej_uniform_eta4_aarch64_asm(int32_t *r, const uint8_t *buf,
-                                          unsigned buflen,
-                                          const uint8_t *table);
+                                          unsigned buflen, const uint8_t *table)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/rej_uniform_eta4_aarch64_asm.ml */
+__contract__(
+  requires(buflen % 8 == 0)
+  requires(buflen >= 8)
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, buflen))
+  requires(table == mld_rej_uniform_eta_table)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(return_value <= MLDSA_N)
+  /* check-magic: 5 == 4 + 1 (asm is eta=4-specific) */
+  ensures(array_abs_bound(r, 0, return_value, 5))
+);
 #endif /* !MLD_CONFIG_NO_KEYPAIR_API */
 
 #if !defined(MLD_CONFIG_NO_SIGN_API)

dev/aarch64_opt/src/arith_native_aarch64.h

@@ -114,15 +114,39 @@ __contract__(
   MLD_NAMESPACE(rej_uniform_eta2_aarch64_asm)
 MLD_MUST_CHECK_RETURN_VALUE
 uint64_t mld_rej_uniform_eta2_aarch64_asm(int32_t *r, const uint8_t *buf,
-                                          unsigned buflen,
-                                          const uint8_t *table);
+                                          unsigned buflen, const uint8_t *table)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/rej_uniform_eta2_aarch64_asm.ml */
+__contract__(
+  requires(buflen % 8 == 0)
+  requires(buflen >= 8)
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, buflen))
+  requires(table == mld_rej_uniform_eta_table)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(return_value <= MLDSA_N)
+  /* check-magic: 3 == 2 + 1 (asm is eta=2-specific) */
+  ensures(array_abs_bound(r, 0, return_value, 3))
+);
 
 #define mld_rej_uniform_eta4_aarch64_asm \
   MLD_NAMESPACE(rej_uniform_eta4_aarch64_asm)
 MLD_MUST_CHECK_RETURN_VALUE
 uint64_t mld_rej_uniform_eta4_aarch64_asm(int32_t *r, const uint8_t *buf,
-                                          unsigned buflen,
-                                          const uint8_t *table);
+                                          unsigned buflen, const uint8_t *table)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/rej_uniform_eta4_aarch64_asm.ml */
+__contract__(
+  requires(buflen % 8 == 0)
+  requires(buflen >= 8)
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, buflen))
+  requires(table == mld_rej_uniform_eta_table)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(return_value <= MLDSA_N)
+  /* check-magic: 5 == 4 + 1 (asm is eta=4-specific) */
+  ensures(array_abs_bound(r, 0, return_value, 5))
+);
 #endif /* !MLD_CONFIG_NO_KEYPAIR_API */
 
 #if !defined(MLD_CONFIG_NO_SIGN_API)

mldsa/src/native/aarch64/src/arith_native_aarch64.h

@@ -114,15 +114,39 @@ __contract__(
   MLD_NAMESPACE(rej_uniform_eta2_aarch64_asm)
 MLD_MUST_CHECK_RETURN_VALUE
 uint64_t mld_rej_uniform_eta2_aarch64_asm(int32_t *r, const uint8_t *buf,
-                                          unsigned buflen,
-                                          const uint8_t *table);
+                                          unsigned buflen, const uint8_t *table)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/rej_uniform_eta2_aarch64_asm.ml */
+__contract__(
+  requires(buflen % 8 == 0)
+  requires(buflen >= 8)
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, buflen))
+  requires(table == mld_rej_uniform_eta_table)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(return_value <= MLDSA_N)
+  /* check-magic: 3 == 2 + 1 (asm is eta=2-specific) */
+  ensures(array_abs_bound(r, 0, return_value, 3))
+);
 
 #define mld_rej_uniform_eta4_aarch64_asm \
   MLD_NAMESPACE(rej_uniform_eta4_aarch64_asm)
 MLD_MUST_CHECK_RETURN_VALUE
 uint64_t mld_rej_uniform_eta4_aarch64_asm(int32_t *r, const uint8_t *buf,
-                                          unsigned buflen,
-                                          const uint8_t *table);
+                                          unsigned buflen, const uint8_t *table)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/rej_uniform_eta4_aarch64_asm.ml */
+__contract__(
+  requires(buflen % 8 == 0)
+  requires(buflen >= 8)
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, buflen))
+  requires(table == mld_rej_uniform_eta_table)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(return_value <= MLDSA_N)
+  /* check-magic: 5 == 4 + 1 (asm is eta=4-specific) */
+  ensures(array_abs_bound(r, 0, return_value, 5))
+);
 #endif /* !MLD_CONFIG_NO_KEYPAIR_API */
 
 #if !defined(MLD_CONFIG_NO_SIGN_API)

mldsa/src/native/api.h

@@ -221,7 +221,8 @@ __contract__(
   requires(memory_no_alias(buf, buflen))
   assigns(memory_slice(r, sizeof(int32_t) * len))
   ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || (0 <= return_value && return_value <= len))
-  ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> (array_abs_bound(r, 0, return_value, MLDSA_ETA + 1)))
+  /* check-magic: 3 == 2 + 1 (decl gated on MLDSA_ETA == 2) */
+  ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> (array_abs_bound(r, 0, return_value, 3)))
 );
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_ETA == 2 */
 #endif /* MLD_USE_NATIVE_REJ_UNIFORM_ETA2 */
@@ -255,7 +256,8 @@ __contract__(
   requires(memory_no_alias(buf, buflen))
   assigns(memory_slice(r, sizeof(int32_t) * len))
   ensures(return_value == MLD_NATIVE_FUNC_FALLBACK || (0 <= return_value && return_value <= len))
-  ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> (array_abs_bound(r, 0, return_value, MLDSA_ETA + 1)))
+  /* check-magic: 5 == 4 + 1 (decl gated on MLDSA_ETA == 4) */
+  ensures((return_value != MLD_NATIVE_FUNC_FALLBACK) ==> (array_abs_bound(r, 0, return_value, 5)))
 );
 #endif /* MLD_CONFIG_MULTILEVEL_WITH_SHARED || MLDSA_ETA == 4 */
 #endif /* MLD_USE_NATIVE_REJ_UNIFORM_ETA4 */

proofs/cbmc/rej_uniform_eta_native_aarch64/Makefile

@@ -0,0 +1,54 @@
+# Copyright (c) The mldsa-native project authors
+# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+include ../Makefile_params.common
+
+HARNESS_ENTRY = harness
+HARNESS_FILE = rej_uniform_eta_native_aarch64_harness
+
+# This should be a unique identifier for this proof, and will appear on the
+# Litani dashboard. It can be human-readable and contain spaces if you wish.
+PROOF_UID = rej_uniform_eta_native_aarch64
+
+# We need to set MLD_CHECK_APIS as otherwise mldsa/src/native/api.h won't be
+# included, which contains the CBMC specifications.
+DEFINES += -DMLD_CONFIG_USE_NATIVE_BACKEND_ARITH -DMLD_CONFIG_ARITH_BACKEND_FILE="\"$(SRCDIR)/mldsa/src/native/aarch64/meta.h\"" -DMLD_CHECK_APIS
+INCLUDES +=
+
+REMOVE_FUNCTION_BODY +=
+UNWINDSET +=
+
+PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
+PROJECT_SOURCES += $(SRCDIR)/mldsa/src/poly_kl.c
+
+# ML-DSA-44 and ML-DSA-87 use eta=2; ML-DSA-65 uses eta=4.
+ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
+    CHECK_FUNCTION_CONTRACTS=mld_rej_uniform_eta2_native
+    USE_FUNCTION_CONTRACTS=mld_rej_uniform_eta2_aarch64_asm
+else ifeq ($(MLD_CONFIG_PARAMETER_SET),65)
+    CHECK_FUNCTION_CONTRACTS=mld_rej_uniform_eta4_native
+    USE_FUNCTION_CONTRACTS=mld_rej_uniform_eta4_aarch64_asm
+else ifeq ($(MLD_CONFIG_PARAMETER_SET),87)
+    CHECK_FUNCTION_CONTRACTS=mld_rej_uniform_eta2_native
+    USE_FUNCTION_CONTRACTS=mld_rej_uniform_eta2_aarch64_asm
+endif
+USE_FUNCTION_CONTRACTS += mld_sys_check_capability
+APPLY_LOOP_CONTRACTS=on
+USE_DYNAMIC_FRAMES=1
+
+# Disable any setting of EXTERNAL_SAT_SOLVER, and choose SMT backend instead
+EXTERNAL_SAT_SOLVER=
+CBMCFLAGS=--bitwuzla
+
+FUNCTION_NAME = rej_uniform_eta_native_aarch64
+
+# If this proof is found to consume huge amounts of RAM, you can set the
+# EXPENSIVE variable. With new enough versions of the proof tools, this will
+# restrict the number of EXPENSIVE CBMC jobs running at once. See the
+# documentation in Makefile.common under the "Job Pools" heading for details.
+# EXPENSIVE = true
+
+# This function is large enough to need...
+CBMC_OBJECT_BITS = 8
+
+include ../Makefile.common

proofs/cbmc/rej_uniform_eta_native_aarch64/rej_uniform_eta_native_aarch64_harness.c

@@ -0,0 +1,29 @@
+// Copyright (c) The mldsa-native project authors
+// SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+
+#include <stdint.h>
+#include "cbmc.h"
+#include "params.h"
+
+#if MLDSA_ETA == 2
+int mld_rej_uniform_eta2_native(int32_t *r, unsigned len, const uint8_t *buf,
+                                unsigned buflen);
+#elif MLDSA_ETA == 4
+int mld_rej_uniform_eta4_native(int32_t *r, unsigned len, const uint8_t *buf,
+                                unsigned buflen);
+#endif
+
+void harness(void)
+{
+  int32_t *r;
+  unsigned len;
+  const uint8_t *buf;
+  unsigned buflen;
+  int t;
+
+#if MLDSA_ETA == 2
+  t = mld_rej_uniform_eta2_native(r, len, buf, buflen);
+#elif MLDSA_ETA == 4
+  t = mld_rej_uniform_eta4_native(r, len, buf, buflen);
+#endif
+}

proofs/hol_light/README.md

@@ -126,6 +126,8 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
   * AArch64 pointwise multiplication-accumulation (l=5): [mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.S](aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.S)
   * AArch64 pointwise multiplication-accumulation (l=7): [mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.S](aarch64/mldsa/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.S)
   * AArch64 rejection sampling: [rej_uniform_aarch64_asm.S](aarch64/mldsa/rej_uniform_aarch64_asm.S)
+  * AArch64 rejection sampling (eta=2): [rej_uniform_eta2_aarch64_asm.S](aarch64/mldsa/rej_uniform_eta2_aarch64_asm.S)
+  * AArch64 rejection sampling (eta=4): [rej_uniform_eta4_aarch64_asm.S](aarch64/mldsa/rej_uniform_eta4_aarch64_asm.S)
 - FIPS202:
   * Keccak-F1600 using lazy rotations[^HYBRID]: [keccak_f1600_x1_scalar_aarch64_asm.S](aarch64/mldsa/keccak_f1600_x1_scalar_aarch64_asm.S)
   * Keccak-F1600 using v8.4-A SHA3 instructions: [keccak_f1600_x1_v84a_aarch64_asm.S](aarch64/mldsa/keccak_f1600_x1_v84a_aarch64_asm.S)

proofs/hol_light/aarch64/Makefile

@@ -63,6 +63,8 @@ OBJ = mldsa/intt_aarch64_asm.o \
       mldsa/mld_polyvecl_pointwise_acc_montgomery_l4_aarch64_asm.o \
       mldsa/mld_polyvecl_pointwise_acc_montgomery_l5_aarch64_asm.o \
       mldsa/mld_polyvecl_pointwise_acc_montgomery_l7_aarch64_asm.o \
+      mldsa/rej_uniform_eta2_aarch64_asm.o \
+      mldsa/rej_uniform_eta4_aarch64_asm.o \
       mldsa/keccak_f1600_x1_scalar_aarch64_asm.o \
       mldsa/keccak_f1600_x1_v84a_aarch64_asm.o \
       mldsa/keccak_f1600_x2_v84a_aarch64_asm.o \

proofs/hol_light/aarch64/mldsa/rej_uniform_eta2_aarch64_asm.S

@@ -0,0 +1,131 @@
+/*
+ * Copyright (c) The mldsa-native project authors
+ * Copyright (c) The mlkem-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+
+
+/*
+ * WARNING: This file is auto-derived from the mldsa-native source file
+ *   dev/aarch64_opt/src/rej_uniform_eta2_aarch64_asm.S using scripts/simpasm. Do not modify it directly.
+ */
+
+.text
+.balign 4
+#ifdef __APPLE__
+.global _PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta2_aarch64_asm
+_PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta2_aarch64_asm:
+#else
+.global PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta2_aarch64_asm
+PQCP_MLDSA_NATIVE_MLDSA44_rej_uniform_eta2_aarch64_asm:
+#endif
+
+        .cfi_startproc
+        sub sp, sp, #0x240
+        .cfi_adjust_cfa_offset 0x240
+        mov x7, #0x1                // =1
+        movk x7, #0x2, lsl #16
+        movk x7, #0x4, lsl #32
+        movk x7, #0x8, lsl #48
+        mov v31.d[0], x7
+        mov x7, #0x10               // =16
+        movk x7, #0x20, lsl #16
+        movk x7, #0x40, lsl #32
+        movk x7, #0x80, lsl #48
+        mov v31.d[1], x7
+        movi v30.8h, #0xf
+        mov x8, sp
+        mov x7, x8
+        mov x11, #0x0               // =0
+        eor v16.16b, v16.16b, v16.16b
+
+Lrej_uniform_eta2_initial_zero:
+        str q16, [x7], #0x40
+        stur q16, [x7, #-0x30]
+        stur q16, [x7, #-0x20]
+        stur q16, [x7, #-0x10]
+        add x11, x11, #0x20
+        cmp x11, #0x100
+        b.lt Lrej_uniform_eta2_initial_zero
+        mov x7, x8
+        mov x9, #0x0                // =0
+        mov x4, #0x100              // =256
+
+Lrej_uniform_eta2_loop8:
+        cmp x9, x4
+        b.hs Lrej_uniform_eta2_memory_copy
+        sub x2, x2, #0x8
+        ld1 { v0.8b }, [x1], #8
+        movi v26.8b, #0xf
+        and v27.8b, v0.8b, v26.8b
+        ushr v28.8b, v0.8b, #0x4
+        zip1 v26.8b, v27.8b, v28.8b
+        zip2 v29.8b, v27.8b, v28.8b
+        ushll v16.8h, v26.8b, #0x0
+        ushll v17.8h, v29.8b, #0x0
+        cmhi v4.8h, v30.8h, v16.8h
+        cmhi v5.8h, v30.8h, v17.8h
+        and v4.16b, v4.16b, v31.16b
+        and v5.16b, v5.16b, v31.16b
+        uaddlv s20, v4.8h
+        uaddlv s21, v5.8h
+        fmov w12, s20
+        fmov w13, s21
+        ldr q24, [x3, x12, lsl #4]
+        ldr q25, [x3, x13, lsl #4]
+        cnt v4.16b, v4.16b
+        cnt v5.16b, v5.16b
+        uaddlv s20, v4.8h
+        uaddlv s21, v5.8h
+        fmov w12, s20
+        fmov w13, s21
+        tbl v16.16b, { v16.16b }, v24.16b
+        tbl v17.16b, { v17.16b }, v25.16b
+        st1 { v16.8h }, [x7]
+        add x7, x7, x12, lsl #1
+        st1 { v17.8h }, [x7]
+        add x7, x7, x13, lsl #1
+        add x12, x12, x13
+        add x9, x9, x12
+        cmp x2, #0x8
+        b.hs Lrej_uniform_eta2_loop8
+
+Lrej_uniform_eta2_memory_copy:
+        cmp x9, x4
+        csel x9, x9, x4, lo
+        mov w7, #0x199a             // =6554
+        dup v26.8h, w7
+        movi v27.8h, #0x5
+        movi v7.8h, #0x2
+        mov x11, #0x0               // =0
+        mov x7, x8
+
+Lrej_uniform_eta2_final_copy:
+        ldr q16, [x7], #0x20
+        ldur q18, [x7, #-0x10]
+        sqdmulh v28.8h, v16.8h, v26.8h
+        mls v16.8h, v28.8h, v27.8h
+        sqdmulh v28.8h, v18.8h, v26.8h
+        mls v18.8h, v28.8h, v27.8h
+        sub v16.8h, v7.8h, v16.8h
+        sub v18.8h, v7.8h, v18.8h
+        sshll2 v17.4s, v16.8h, #0x0
+        sshll v16.4s, v16.4h, #0x0
+        sshll2 v19.4s, v18.8h, #0x0
+        sshll v18.4s, v18.4h, #0x0
+        str q16, [x0], #0x40
+        stur q17, [x0, #-0x30]
+        stur q18, [x0, #-0x20]
+        stur q19, [x0, #-0x10]
+        add x11, x11, #0x10
+        cmp x11, #0x100
+        b.lt Lrej_uniform_eta2_final_copy
+        mov x0, x9
+        add sp, sp, #0x240
+        .cfi_adjust_cfa_offset -0x240
+        ret
+        .cfi_endproc
+
+#if defined(__ELF__)
+.section .note.GNU-stack,"",%progbits
+#endif