HOL-Light: Add HOL Light proof for aarch64 polyz_unpack_{17,19}

.github/workflows/hol_light.yml

@@ -13,6 +13,7 @@ on:
      - 'proofs/hol_light/aarch64/Makefile'
      - 'proofs/hol_light/aarch64/**/*.S'
      - 'proofs/hol_light/aarch64/**/*.ml'
+     - 'proofs/hol_light/common/**/*.ml'
      - 'proofs/hol_light/x86_64/Makefile'
      - 'proofs/hol_light/x86_64/**/*.S'
      - 'proofs/hol_light/x86_64/**/*.ml'
@@ -28,6 +29,7 @@ on:
       - 'proofs/hol_light/aarch64/Makefile'
       - 'proofs/hol_light/aarch64/**/*.S'
       - 'proofs/hol_light/aarch64/**/*.ml'
+      - 'proofs/hol_light/common/**/*.ml'
       - 'proofs/hol_light/x86_64/Makefile'
       - 'proofs/hol_light/x86_64/**/*.S'
       - 'proofs/hol_light/x86_64/**/*.ml'
@@ -87,6 +89,10 @@ jobs:
             needs: ["aarch64_utils.ml"]
           - name: mldsa_poly_chknorm
             needs: ["aarch64_utils.ml"]
+          - name: mldsa_polyz_unpack_17
+            needs: ["aarch64_utils.ml", "mldsa_polyz_unpack_consts.ml", "mldsa_specs.ml"]
+          - name: mldsa_polyz_unpack_19
+            needs: ["aarch64_utils.ml", "mldsa_polyz_unpack_consts.ml", "mldsa_specs.ml"]
     name: AArch64 HOL Light proof for ${{ matrix.proof.name }}.S
     runs-on: pqcp-arm64
     if: github.repository_owner == 'pq-code-package' && !github.event.pull_request.head.repo.fork

dev/aarch64_clean/src/arith_native_aarch64.h

@@ -121,11 +121,29 @@ __contract__(
 
 #define mld_polyz_unpack_17_asm MLD_NAMESPACE(polyz_unpack_17_asm)
 void mld_polyz_unpack_17_asm(int32_t *r, const uint8_t *buf,
-                             const uint8_t *indices);
+                             const uint8_t *indices)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_17.ml */
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, 576))
+  requires(indices == mld_polyz_unpack_17_indices)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(r, 0, MLDSA_N, -((1 << 17) - 1), (1 << 17) + 1))
+);
 
 #define mld_polyz_unpack_19_asm MLD_NAMESPACE(polyz_unpack_19_asm)
 void mld_polyz_unpack_19_asm(int32_t *r, const uint8_t *buf,
-                             const uint8_t *indices);
+                             const uint8_t *indices)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_19.ml */
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, 640))
+  requires(indices == mld_polyz_unpack_19_indices)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(r, 0, MLDSA_N, -((1 << 19) - 1), (1 << 19) + 1))
+);
 
 #define mld_poly_pointwise_montgomery_asm \
   MLD_NAMESPACE(poly_pointwise_montgomery_asm)

dev/aarch64_opt/src/arith_native_aarch64.h

@@ -121,11 +121,29 @@ __contract__(
 
 #define mld_polyz_unpack_17_asm MLD_NAMESPACE(polyz_unpack_17_asm)
 void mld_polyz_unpack_17_asm(int32_t *r, const uint8_t *buf,
-                             const uint8_t *indices);
+                             const uint8_t *indices)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_17.ml */
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, 576))
+  requires(indices == mld_polyz_unpack_17_indices)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(r, 0, MLDSA_N, -((1 << 17) - 1), (1 << 17) + 1))
+);
 
 #define mld_polyz_unpack_19_asm MLD_NAMESPACE(polyz_unpack_19_asm)
 void mld_polyz_unpack_19_asm(int32_t *r, const uint8_t *buf,
-                             const uint8_t *indices);
+                             const uint8_t *indices)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_19.ml */
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, 640))
+  requires(indices == mld_polyz_unpack_19_indices)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(r, 0, MLDSA_N, -((1 << 19) - 1), (1 << 19) + 1))
+);
 
 #define mld_poly_pointwise_montgomery_asm \
   MLD_NAMESPACE(poly_pointwise_montgomery_asm)

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

@@ -121,11 +121,29 @@ __contract__(
 
 #define mld_polyz_unpack_17_asm MLD_NAMESPACE(polyz_unpack_17_asm)
 void mld_polyz_unpack_17_asm(int32_t *r, const uint8_t *buf,
-                             const uint8_t *indices);
+                             const uint8_t *indices)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_17.ml */
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, 576))
+  requires(indices == mld_polyz_unpack_17_indices)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(r, 0, MLDSA_N, -((1 << 17) - 1), (1 << 17) + 1))
+);
 
 #define mld_polyz_unpack_19_asm MLD_NAMESPACE(polyz_unpack_19_asm)
 void mld_polyz_unpack_19_asm(int32_t *r, const uint8_t *buf,
-                             const uint8_t *indices);
+                             const uint8_t *indices)
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/aarch64/proofs/mldsa_polyz_unpack_19.ml */
+__contract__(
+  requires(memory_no_alias(r, sizeof(int32_t) * MLDSA_N))
+  requires(memory_no_alias(buf, 640))
+  requires(indices == mld_polyz_unpack_19_indices)
+  assigns(memory_slice(r, sizeof(int32_t) * MLDSA_N))
+  ensures(array_bound(r, 0, MLDSA_N, -((1 << 19) - 1), (1 << 19) + 1))
+);
 
 #define mld_poly_pointwise_montgomery_asm \
   MLD_NAMESPACE(poly_pointwise_montgomery_asm)

nix/s2n_bignum/default.nix

@@ -4,12 +4,12 @@
 { stdenv, fetchFromGitHub, writeText, ... }:
 stdenv.mkDerivation rec {
   pname = "s2n_bignum";
-  version = "3bfe68deb9fbdaf23be0a927c362a87a799adc28";
+  version = "cba3956c7a20d22f08ef6f49fe162e9d7c07867c";
   src = fetchFromGitHub {
     owner = "awslabs";
     repo = "s2n-bignum";
     rev = "${version}";
-    hash = "sha256-C3SdYZ/PhfTmHefz3klO3l/lbEgtA8Hq9wjDmjd+Fek=";
+    hash = "sha256-5UOu1aUqPGiDPhpBlUDjkM/GqP4SILT/p4pKL9DBFjg=";
   };
   setupHook = writeText "setup-hook.sh" ''
     export S2N_BIGNUM_DIR="$1"

proofs/cbmc/polyz_unpack_17_native_aarch64/Makefile

@@ -0,0 +1,63 @@
+# 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 = polyz_unpack_17_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 = polyz_unpack_17_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 $(SRCDIR)/mldsa/src/native/aarch64/src/polyz_unpack_table.c
+
+# polyz_unpack_17 is only used with ML-DSA-44
+ifeq ($(MLD_CONFIG_PARAMETER_SET),44)
+CHECK_FUNCTION_CONTRACTS=mld_polyz_unpack_17_native
+USE_FUNCTION_CONTRACTS = mld_polyz_unpack_17_asm
+else
+CHECK_FUNCTION_CONTRACTS=
+USE_FUNCTION_CONTRACTS =
+endif
+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 = polyz_unpack_17_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
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly_kl.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly_kl.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

proofs/cbmc/polyz_unpack_17_native_aarch64/polyz_unpack_17_native_aarch64_harness.c

@@ -0,0 +1,19 @@
+// 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"
+
+int mld_polyz_unpack_17_native(int32_t *r, const uint8_t *a);
+
+void harness(void)
+{
+  /* mld_polyz_unpack_17_native is only defined for ML-DSA-44 */
+#if MLD_CONFIG_PARAMETER_SET == 44
+  int32_t *r;
+  const uint8_t *a;
+  int t;
+  t = mld_polyz_unpack_17_native(r, a);
+#endif /* MLD_CONFIG_PARAMETER_SET == 44 */
+}

proofs/cbmc/polyz_unpack_19_native_aarch64/Makefile

@@ -0,0 +1,66 @@
+# 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 = polyz_unpack_19_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 = polyz_unpack_19_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 $(SRCDIR)/mldsa/src/native/aarch64/src/polyz_unpack_table.c
+
+# polyz_unpack_19 is only used with ML-DSA-65 and ML-DSA-87
+ifeq ($(MLD_CONFIG_PARAMETER_SET),65)
+CHECK_FUNCTION_CONTRACTS=mld_polyz_unpack_19_native
+USE_FUNCTION_CONTRACTS = mld_polyz_unpack_19_asm
+else ifeq ($(MLD_CONFIG_PARAMETER_SET),87)
+CHECK_FUNCTION_CONTRACTS=mld_polyz_unpack_19_native
+USE_FUNCTION_CONTRACTS = mld_polyz_unpack_19_asm
+else
+CHECK_FUNCTION_CONTRACTS=
+USE_FUNCTION_CONTRACTS =
+endif
+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 = polyz_unpack_19_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
+
+# If you require access to a file-local ("static") function or object to conduct
+# your proof, set the following (and do not include the original source file
+# ("mldsa/poly_kl.c") in PROJECT_SOURCES).
+# REWRITTEN_SOURCES = $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i
+# include ../Makefile.common
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_SOURCE = $(SRCDIR)/mldsa/src/poly_kl.c
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_FUNCTIONS = foo bar
+# $(PROOFDIR)/<__SOURCE_FILE_BASENAME__>.i_OBJECTS = baz
+# Care is required with variables on the left-hand side: REWRITTEN_SOURCES must
+# be set before including Makefile.common, but any use of variables on the
+# left-hand side requires those variables to be defined. Hence, _SOURCE,
+# _FUNCTIONS, _OBJECTS is set after including Makefile.common.
+
+include ../Makefile.common

proofs/cbmc/polyz_unpack_19_native_aarch64/polyz_unpack_19_native_aarch64_harness.c

@@ -0,0 +1,19 @@
+// 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"
+
+int mld_polyz_unpack_19_native(int32_t *r, const uint8_t *a);
+
+void harness(void)
+{
+  /* mld_polyz_unpack_19_native is only defined for ML-DSA-65 and ML-DSA-87 */
+#if MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87
+  int32_t *r;
+  const uint8_t *a;
+  int t;
+  t = mld_polyz_unpack_19_native(r, a);
+#endif /* MLD_CONFIG_PARAMETER_SET == 65 || MLD_CONFIG_PARAMETER_SET == 87 */
+}

proofs/hol_light/aarch64/Makefile

@@ -55,7 +55,9 @@ SPLIT=tr ';' '\n'
 
 OBJ = mldsa/mldsa_ntt.o \
       mldsa/mldsa_poly_caddq.o \
-      mldsa/mldsa_poly_chknorm.o
+      mldsa/mldsa_poly_chknorm.o \
+      mldsa/mldsa_polyz_unpack_17.o \
+      mldsa/mldsa_polyz_unpack_19.o
 
 # According to
 # https://developer.apple.com/documentation/xcode/writing-arm64-code-for-apple-platforms,

proofs/hol_light/aarch64/mldsa/mldsa_polyz_unpack_17.S

@@ -0,0 +1,68 @@
+/*
+ * 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/polyz_unpack_17_asm.S using scripts/simpasm. Do not modify it directly.
+ */
+
+#if defined(__ELF__)
+.section .note.GNU-stack,"",@progbits
+#endif
+
+.text
+.balign 4
+#ifdef __APPLE__
+.global _PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_asm
+_PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_asm:
+#else
+.global PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_asm
+PQCP_MLDSA_NATIVE_MLDSA44_polyz_unpack_17_asm:
+#endif
+
+        .cfi_startproc
+        ldr	q24, [x2]
+        ldr	q25, [x2, #0x10]
+        ldr	q26, [x2, #0x20]
+        ldr	q27, [x2, #0x30]
+        mov	x3, #0xfe00000000       // =1090921693184
+        mov	v28.d[0], x3
+        mov	x3, #0xfc               // =252
+        movk	x3, #0xfa, lsl #32
+        mov	v28.d[1], x3
+        movi	v29.4s, #0x3, msl #16
+        movi	v30.4s, #0x2, lsl #16
+        mov	x9, #0x10               // =16
+
+Lpolyz_unpack_17_loop:
+        ld1	{ v0.16b, v1.16b }, [x1]
+        add	x1, x1, #0x14
+        ld1	{ v2.16b }, [x1], #16
+        tbl	v4.16b, { v0.16b }, v24.16b
+        tbl	v5.16b, { v0.16b, v1.16b }, v25.16b
+        tbl	v6.16b, { v1.16b }, v26.16b
+        tbl	v7.16b, { v1.16b, v2.16b }, v27.16b
+        ushl	v4.4s, v4.4s, v28.4s
+        and	v4.16b, v4.16b, v29.16b
+        sub	v4.4s, v30.4s, v4.4s
+        ushl	v5.4s, v5.4s, v28.4s
+        and	v5.16b, v5.16b, v29.16b
+        sub	v5.4s, v30.4s, v5.4s
+        ushl	v6.4s, v6.4s, v28.4s
+        and	v6.16b, v6.16b, v29.16b
+        sub	v6.4s, v30.4s, v6.4s
+        ushl	v7.4s, v7.4s, v28.4s
+        and	v7.16b, v7.16b, v29.16b
+        sub	v7.4s, v30.4s, v7.4s
+        str	q5, [x0, #0x10]
+        str	q6, [x0, #0x20]
+        str	q7, [x0, #0x30]
+        str	q4, [x0], #0x40
+        subs	x9, x9, #0x1
+        b.ne	Lpolyz_unpack_17_loop
+        ret
+        .cfi_endproc