HOL-Light: Add HOL Light poly_use_hint proofs for AArch64

.github/workflows/hol_light.yml

@@ -97,6 +97,10 @@ jobs:
             needs: ["aarch64_utils.ml"]
           - name: mldsa_poly_chknorm
             needs: ["aarch64_utils.ml"]
+          - name: poly_use_hint_32_aarch64_asm
+            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: keccak_f1600_x1_scalar
             needs: ["keccak_spec.ml"]
           - name: keccak_f1600_x1_v84a

dev/aarch64_clean/src/arith_native_aarch64.h

@@ -117,10 +117,32 @@ __contract__(
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 #define mld_poly_use_hint_32_asm MLD_NAMESPACE(poly_use_hint_32_asm)
-void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h);
+void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml */
+__contract__(
+  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
+  requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
+  requires(array_bound(h, 0, MLDSA_N, 0, 2))
+  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(b, 0, MLDSA_N, 0, 16))
+);
 
 #define mld_poly_use_hint_88_asm MLD_NAMESPACE(poly_use_hint_88_asm)
-void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h);
+void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml */
+__contract__(
+  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
+  requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
+  requires(array_bound(h, 0, MLDSA_N, 0, 2))
+  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(b, 0, MLDSA_N, 0, 44))
+);
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
 #define mld_poly_chknorm_asm MLD_NAMESPACE(poly_chknorm_asm)

dev/aarch64_opt/src/arith_native_aarch64.h

@@ -117,10 +117,32 @@ __contract__(
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 #define mld_poly_use_hint_32_asm MLD_NAMESPACE(poly_use_hint_32_asm)
-void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h);
+void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml */
+__contract__(
+  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
+  requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
+  requires(array_bound(h, 0, MLDSA_N, 0, 2))
+  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(b, 0, MLDSA_N, 0, 16))
+);
 
 #define mld_poly_use_hint_88_asm MLD_NAMESPACE(poly_use_hint_88_asm)
-void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h);
+void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml */
+__contract__(
+  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
+  requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
+  requires(array_bound(h, 0, MLDSA_N, 0, 2))
+  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(b, 0, MLDSA_N, 0, 44))
+);
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
 #define mld_poly_chknorm_asm MLD_NAMESPACE(poly_chknorm_asm)

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

@@ -117,10 +117,32 @@ __contract__(
 
 #if !defined(MLD_CONFIG_NO_VERIFY_API)
 #define mld_poly_use_hint_32_asm MLD_NAMESPACE(poly_use_hint_32_asm)
-void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h);
+void mld_poly_use_hint_32_asm(int32_t *b, const int32_t *a, const int32_t *h)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/poly_use_hint_32_aarch64_asm.ml */
+__contract__(
+  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
+  requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
+  requires(array_bound(h, 0, MLDSA_N, 0, 2))
+  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(b, 0, MLDSA_N, 0, 16))
+);
 
 #define mld_poly_use_hint_88_asm MLD_NAMESPACE(poly_use_hint_88_asm)
-void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h);
+void mld_poly_use_hint_88_asm(int32_t *b, const int32_t *a, const int32_t *h)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/poly_use_hint_88_aarch64_asm.ml */
+__contract__(
+  requires(memory_no_alias(b, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(a, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(h, sizeof(int32_t) * MLDSA_N))
+  requires(array_bound(a, 0, MLDSA_N, 0, MLDSA_Q))
+  requires(array_bound(h, 0, MLDSA_N, 0, 2))
+  assigns(memory_slice(b, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(b, 0, MLDSA_N, 0, 44))
+);
 #endif /* !MLD_CONFIG_NO_VERIFY_API */
 
 #define mld_poly_chknorm_asm MLD_NAMESPACE(poly_chknorm_asm)

proofs/cbmc/poly_use_hint_native_aarch64/Makefile

@@ -0,0 +1,53 @@
+# 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 = poly_use_hint_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 = poly_use_hint_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
+
+ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
+    CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_88_native
+    USE_FUNCTION_CONTRACTS=mld_poly_use_hint_88_asm
+else ifeq ($(MLD_CONFIG_PARAMETER_SET),65)
+    CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_32_native
+    USE_FUNCTION_CONTRACTS=mld_poly_use_hint_32_asm
+else ifeq ($(MLD_CONFIG_PARAMETER_SET),87)
+    CHECK_FUNCTION_CONTRACTS=mld_poly_use_hint_32_native
+    USE_FUNCTION_CONTRACTS=mld_poly_use_hint_32_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=--smt2
+
+FUNCTION_NAME = poly_use_hint_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/poly_use_hint_native_aarch64/poly_use_hint_native_aarch64_harness.c

@@ -0,0 +1,24 @@
+// 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_GAMMA2 == ((MLDSA_Q - 1) / 88)
+int mld_poly_use_hint_88_native(int32_t *b, const int32_t *a, const int32_t *h);
+#else
+int mld_poly_use_hint_32_native(int32_t *b, const int32_t *a, const int32_t *h);
+#endif
+
+void harness(void)
+{
+  int32_t *b, *a, *h;
+  int t;
+
+#if MLDSA_GAMMA2 == ((MLDSA_Q - 1) / 88)
+  t = mld_poly_use_hint_88_native(b, a, h);
+#else
+  t = mld_poly_use_hint_32_native(b, a, h);
+#endif
+}

proofs/hol_light/README.md

@@ -54,6 +54,8 @@ echo '1+1;;' | nc -w 5 127.0.0.1 2012
 - ML-DSA Arithmetic:
   * AArch64 poly_caddq: [mldsa_poly_caddq.S](aarch64/mldsa/mldsa_poly_caddq.S)
   * AArch64 poly_chknorm: [mldsa_poly_chknorm.S](aarch64/mldsa/mldsa_poly_chknorm.S)
+  * AArch64 poly_use_hint (l=5,7): [poly_use_hint_32_aarch64_asm.S](aarch64/mldsa/poly_use_hint_32_aarch64_asm.S)
+  * AArch64 poly_use_hint (l=4): [poly_use_hint_88_aarch64_asm.S](aarch64/mldsa/poly_use_hint_88_aarch64_asm.S)
   * AArch64 pointwise multiplication: [mldsa_pointwise.S](aarch64/mldsa/mldsa_pointwise.S)
   * AArch64 pointwise multiplication-accumulation (l=4): [mldsa_pointwise_acc_l4.S](aarch64/mldsa/mldsa_pointwise_acc_l4.S)
   * AArch64 pointwise multiplication-accumulation (l=5): [mldsa_pointwise_acc_l5.S](aarch64/mldsa/mldsa_pointwise_acc_l5.S)

proofs/hol_light/aarch64/Makefile

@@ -56,17 +56,19 @@ SPLIT=tr ';' '\n'
 OBJ = mldsa/mldsa_ntt.o \
       mldsa/mldsa_pointwise.o \
       mldsa/mldsa_poly_caddq.o \
-      mldsa/mldsa_poly_chknorm.o \
-      mldsa/mldsa_pointwise_acc_l4.o \
-      mldsa/mldsa_pointwise_acc_l5.o \
-      mldsa/mldsa_pointwise_acc_l7.o \
-      mldsa/keccak_f1600_x1_scalar.o \
-      mldsa/keccak_f1600_x1_v84a.o \
-      mldsa/keccak_f1600_x2_v84a.o \
-      mldsa/keccak_f1600_x4_v8a_scalar.o \
-      mldsa/keccak_f1600_x4_v8a_v84a_scalar.o \
-      mldsa/mldsa_polyz_unpack_17.o \
-      mldsa/mldsa_polyz_unpack_19.o
+      mldsa/mldsa_poly_chknorm.o                        \
+      mldsa/mldsa_pointwise_acc_l4.o                    \
+      mldsa/mldsa_pointwise_acc_l5.o                    \
+      mldsa/mldsa_pointwise_acc_l7.o                    \
+      mldsa/keccak_f1600_x1_scalar.o                    \
+      mldsa/keccak_f1600_x1_v84a.o                      \
+      mldsa/keccak_f1600_x2_v84a.o                      \
+      mldsa/keccak_f1600_x4_v8a_scalar.o                \
+      mldsa/keccak_f1600_x4_v8a_v84a_scalar.o            \
+      mldsa/mldsa_polyz_unpack_17.o                     \
+      mldsa/mldsa_polyz_unpack_19.o                     \
+      mldsa/poly_use_hint_32_aarch64_asm.o              \
+      mldsa/poly_use_hint_88_aarch64_asm.o
 
 # According to
 # https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms,

proofs/hol_light/aarch64/mldsa/poly_use_hint_32_aarch64_asm.S

@@ -0,0 +1,98 @@
+/*
+ * Copyright (c) The mldsa-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/poly_use_hint_32_asm.S using scripts/simpasm. Do not modify it directly.
+ */
+
+.text
+.balign 4
+#ifdef __APPLE__
+.global _PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_asm
+_PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_asm:
+#else
+.global PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_asm
+PQCP_MLDSA_NATIVE_MLDSA44_poly_use_hint_32_asm:
+#endif
+
+        .cfi_startproc
+        mov w4, #0xe001             // =57345
+        movk w4, #0x7f, lsl #16
+        dup v20.4s, w4
+        mov w5, #0xe100             // =57600
+        movk w5, #0x7b, lsl #16
+        dup v21.4s, w5
+        mov w7, #0xfe00             // =65024
+        movk w7, #0x7, lsl #16
+        dup v22.4s, w7
+        mov w11, #0x401             // =1025
+        movk w11, #0x4010, lsl #16
+        dup v23.4s, w11
+        movi v24.4s, #0xf
+        mov x3, #0x10               // =16
+
+Lpoly_use_hint_32_loop:
+        ldr q1, [x1, #0x10]
+        ldr q2, [x1, #0x20]
+        ldr q3, [x1, #0x30]
+        ldr q0, [x1], #0x40
+        ldr q5, [x2, #0x10]
+        ldr q6, [x2, #0x20]
+        ldr q7, [x2, #0x30]
+        ldr q4, [x2], #0x40
+        sqdmulh v17.4s, v1.4s, v23.4s
+        srshr v17.4s, v17.4s, #0x12
+        cmgt v25.4s, v1.4s, v21.4s
+        mls v1.4s, v17.4s, v22.4s
+        bic v17.16b, v17.16b, v25.16b
+        add v1.4s, v1.4s, v25.4s
+        cmle v1.4s, v1.4s, #0
+        orr v1.4s, #0x1
+        mla v17.4s, v1.4s, v5.4s
+        and v17.16b, v17.16b, v24.16b
+        sqdmulh v18.4s, v2.4s, v23.4s
+        srshr v18.4s, v18.4s, #0x12
+        cmgt v25.4s, v2.4s, v21.4s
+        mls v2.4s, v18.4s, v22.4s
+        bic v18.16b, v18.16b, v25.16b
+        add v2.4s, v2.4s, v25.4s
+        cmle v2.4s, v2.4s, #0
+        orr v2.4s, #0x1
+        mla v18.4s, v2.4s, v6.4s
+        and v18.16b, v18.16b, v24.16b
+        sqdmulh v19.4s, v3.4s, v23.4s
+        srshr v19.4s, v19.4s, #0x12
+        cmgt v25.4s, v3.4s, v21.4s
+        mls v3.4s, v19.4s, v22.4s
+        bic v19.16b, v19.16b, v25.16b
+        add v3.4s, v3.4s, v25.4s
+        cmle v3.4s, v3.4s, #0
+        orr v3.4s, #0x1
+        mla v19.4s, v3.4s, v7.4s
+        and v19.16b, v19.16b, v24.16b
+        sqdmulh v16.4s, v0.4s, v23.4s
+        srshr v16.4s, v16.4s, #0x12
+        cmgt v25.4s, v0.4s, v21.4s
+        mls v0.4s, v16.4s, v22.4s
+        bic v16.16b, v16.16b, v25.16b
+        add v0.4s, v0.4s, v25.4s
+        cmle v0.4s, v0.4s, #0
+        orr v0.4s, #0x1
+        mla v16.4s, v0.4s, v4.4s
+        and v16.16b, v16.16b, v24.16b
+        str q17, [x0, #0x10]
+        str q18, [x0, #0x20]
+        str q19, [x0, #0x30]
+        str q16, [x0], #0x40
+        subs x3, x3, #0x1
+        b.ne Lpoly_use_hint_32_loop
+        ret
+        .cfi_endproc
+
+#if defined(__ELF__)
+.section .note.GNU-stack,"",%progbits
+#endif