[WIP] riscv64: Add RVV assembly arithmetic backend and Zbb Keccak

.github/workflows/bench.yml

@@ -63,13 +63,13 @@ jobs:
         - system: bpi
           name: SpacemiT K1 8 (Banana Pi F3) benchmarks
           bench_pmu: PERF
-          archflags: "-march=rv64imafdcv_zicsr_zifencei"
+          archflags: "-march=rv64imafdcv_zicsr_zifencei_zbb"
           cflags: ""
           ldflags: "-static"
           bench_extra_args: -w exec-on-bpi
           cross_prefix: riscv64-unknown-linux-gnu-
           nix_shell: cross-riscv64
-          only_no_opt: true
+          only_no_opt: false
           zephyr_target: ""
         - system: m1-mac-mini
           name: Mac Mini (M1, 2020) benchmarks

BIBLIOGRAPHY.md

@@ -297,6 +297,7 @@ source code and documentation.
   - [dev/aarch64_opt/README.md](dev/aarch64_opt/README.md)
   - [dev/aarch64_opt/src/mldsa_intt_aarch64_asm.S](dev/aarch64_opt/src/mldsa_intt_aarch64_asm.S)
   - [dev/aarch64_opt/src/mldsa_ntt_aarch64_asm.S](dev/aarch64_opt/src/mldsa_ntt_aarch64_asm.S)
+  - [dev/riscv64/README.md](dev/riscv64/README.md)
   - [mldsa/src/native/aarch64/src/mldsa_intt_aarch64_asm.S](mldsa/src/native/aarch64/src/mldsa_intt_aarch64_asm.S)
   - [mldsa/src/native/aarch64/src/mldsa_ntt_aarch64_asm.S](mldsa/src/native/aarch64/src/mldsa_ntt_aarch64_asm.S)
   - [proofs/hol_light/aarch64/mldsa/mldsa_intt_aarch64_asm.S](proofs/hol_light/aarch64/mldsa/mldsa_intt_aarch64_asm.S)
@@ -420,6 +421,15 @@ source code and documentation.
   - [proofs/hol_light/x86_64/mldsa/mldsa_rej_uniform_eta2_avx2_asm.S](proofs/hol_light/x86_64/mldsa/mldsa_rej_uniform_eta2_avx2_asm.S)
   - [proofs/hol_light/x86_64/mldsa/mldsa_rej_uniform_eta4_avx2_asm.S](proofs/hol_light/x86_64/mldsa/mldsa_rej_uniform_eta4_avx2_asm.S)
 
+### `RVPSABI`
+
+* RISC-V ABIs Specification
+* Author(s):
+  - RISC-V International
+* URL: https://github.com/riscv-non-isa/riscv-elf-psabi-doc
+* Referenced from:
+  - [test/abicheck/riscv64/abicheck_riscv64.c](test/abicheck/riscv64/abicheck_riscv64.c)
+
 ### `Round3_Spec`
 
 * CRYSTALS-Dilithium Algorithm Specifications and Supporting Documentation (Version 3.1)

BIBLIOGRAPHY.yml

@@ -241,6 +241,12 @@
   - Mitchell, Mark
   url: https://gitlab.com/x86-psABIs/x86-64-ABI
 
+- id: RVPSABI
+  short: RISC-V psABI
+  name: "RISC-V ABIs Specification"
+  author: RISC-V International
+  url: https://github.com/riscv-non-isa/riscv-elf-psabi-doc
+
 - id: ArmARMv8M
   short: Armv8-M ARM
   name: "Armv8-M Architecture Reference Manual (DDI 0553)"

dev/fips202/riscv64/auto.h

@@ -0,0 +1,14 @@
+/*
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+
+#ifndef MLD_DEV_FIPS202_RISCV64_AUTO_H
+#define MLD_DEV_FIPS202_RISCV64_AUTO_H
+/* Default FIPS202 assembly profile for RISC-V 64 systems */
+
+#if defined(__riscv_zbb)
+#include "x1_zbb.h"
+#endif
+
+#endif /* !MLD_DEV_FIPS202_RISCV64_AUTO_H */

dev/fips202/riscv64/src/fips202_native_riscv64.h

@@ -0,0 +1,28 @@
+/*
+ * Copyright (c) The mldsa-native project authors
+ * SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
+ */
+#ifndef MLD_DEV_FIPS202_RISCV64_SRC_FIPS202_NATIVE_RISCV64_H
+#define MLD_DEV_FIPS202_RISCV64_SRC_FIPS202_NATIVE_RISCV64_H
+
+#include "../../../../cbmc.h"
+#include "../../../../common.h"
+
+#define mld_keccakf1600_round_constants \
+  MLD_NAMESPACE(keccakf1600_round_constants)
+MLD_INTERNAL_DATA_DECLARATION const uint64_t
+    mld_keccakf1600_round_constants[24];
+
+#define mld_keccak_f1600_x1_zbb_riscv64_asm \
+  MLD_NAMESPACE(keccak_f1600_x1_zbb_riscv64_asm)
+void mld_keccak_f1600_x1_zbb_riscv64_asm(uint64_t state[25],
+                                         const uint64_t rc[24])
+/* This must be kept in sync with the HOL-Light specification
+ * in proofs/hol_light/riscv64/proofs/keccak_f1600_x1_zbb_riscv64_asm.ml */
+__contract__(
+  requires(memory_no_alias(state, sizeof(uint64_t) * 25 * 1))
+  requires(rc == mld_keccakf1600_round_constants)
+  assigns(memory_slice(state, sizeof(uint64_t) * 25 * 1))
+);
+
+#endif /* !MLD_DEV_FIPS202_RISCV64_SRC_FIPS202_NATIVE_RISCV64_H */