Merge pull request #1054 from pq-code-package/stable-release

Prepare v1.0.0 release

Author: hanno-becker

.github/ISSUE_TEMPLATE/bug_report.md

@@ -20,6 +20,8 @@ A clear and concise description of what the bug is.
 
 **Compiler**: e.g., gcc 13.2.0 (installed through nix)
 
+**mlkem-native version**: e.g., v1.0.0 or main-branch
+
 **How to reproduce**
 Steps to reproduce the behavior:
 ```

.github/pull_request_template.md

@@ -72,12 +72,6 @@ through suitable barriers and constant-time patterns.
 Absence of secret-dependent branches, memory-access patterns and variable-latency instructions is also tested using `valgrind`
 with various combinations of compilers and compilation options.
 
-## State
-
-mlkem-native is in beta-release stage. We believe it is ready for use, and hope to spark experiments on
-integration into other software before issuing a stable release. If you have any feedback, please reach out! See
-[RELEASE.md](RELEASE.md) for details.
-
 ## Design
 
 mlkem-native is split into a _frontend_ and two _backends_ for arithmetic and FIPS202 / SHA3. The frontend is

README.md

@@ -1,44 +1,26 @@
 [//]: # (SPDX-License-Identifier: CC-BY-4.0)
-mlkem-native v1.0.0-beta
+mlkem-native v1.0.0
 ==================
 
-About
------
-
-mlkem-native is a secure, fast and portable C90 implementation of [ML-KEM](https://doi.org/10.6028/NIST.FIPS.203).
-It is a fork of the ML-KEM [reference implementation](https://github.com/pq-crystals/kyber/tree/main/ref).
-
-mlkem-native includes native backends for AArch64 and AVX2, offering competitive performance on most Arm, Intel and AMD platforms
-(see [benchmarks](https://pq-code-package.github.io/mlkem-native/dev/bench/)). The frontend and the C backend (i.e., all C code in [mlkem/*](mlkem) and [mlkem/src/fips202/*](mlkem/src/fips202)) are verified
-using [CBMC](https://github.com/diffblue/cbmc) to be free of undefined behaviour. In particular, there are no out of
-bounds accesses, nor integer overflows during optimized modular arithmetic.
-HOL-Light is used to verify functional correctness of selected AArch64 assembly routines.
-
-mlkem-native is supported by the [Post-Quantum Cryptography Alliance](https://pqca.org/) as part of the [Linux Foundation](https://linuxfoundation.org/).
-
 Release notes
-=============
+-------------
+
+v1.0.0 is the first stable release of mlkem-native, a secure, fast and portable C90 implementation of [ML-KEM](https://csrc.nist.gov/pubs/fips/202/final) derived from the ML-KEM reference implementation. mlkem-native v1.0.0 offers:
+* High maintainability and extensibility through modular frontend/backend design.
+* High performance through Arch64 and AVX2 assembly backends and the use of the [SLOTHY super-optimizer](https://github.com/slothy-optimizer/slothy).
+* High assurance through memory- and type-safety proofs for the C frontend + backend, functional correctness proofs for all AArch64 assembly, and extensive constant-time testing.
 
-This is the second official release of mlkem-native, a secure, fast and portable C90 implementation of [ML-KEM](https://doi.org/10.6028/NIST.FIPS.203).
-This beta release expands the scope of formal verification (using CBMC and HOL-Light), improves FIPS compliance by adding improves FIPS compliance by adding PCT, buffer zeroization, and documentation, and increases the confidence in resistance against timing side-channels through extensive Valgrind-based testing.
+mlkem-native-v1.0.0 is uniformly licensed Apache-2.0 OR MIT OR ISC, giving consumers the choice to use any of these licenses.
 
 What's New
 ----------
 
-Compared to [v1.0.0-alpha](https://github.com/pq-code-package/mlkem-native/releases/tag/v1.0.0-alpha) the following
+Compared to [v1.0.0-beta](https://github.com/pq-code-package/mlkem-native/releases/tag/v1.0.0-beta) the following
 major improvements have been integrated into mlkem-native:
-- Full CBMC proof coverage of the C frontend and backend including FIPS202
-- Destruction of intermediate values in https://github.com/pq-code-package/mlkem-native/pull/763
-- Functional correctness proofs for AArch64 NTT and INTT in https://github.com/pq-code-package/mlkem-native/pull/662
-- Functional correctness proofs for Keccakx1 in https://github.com/pq-code-package/mlkem-native/pull/826 and https://github.com/pq-code-package/mlkem-native/pull/821
-- Support for single compilation-unit builds in https://github.com/pq-code-package/mlkem-native/pull/612
-- Addition of the pair-wise consistency test in https://github.com/pq-code-package/mlkem-native/pull/769
-- Valgrind-based constant-time tests in https://github.com/pq-code-package/mlkem-native/pull/687
-- Valgrind-based detection of secret-dependent variable-latency instruction in https://github.com/pq-code-package/mlkem-native/pull/693
-- Improved x86_64 backend performance in https://github.com/pq-code-package/mlkem-native/pull/709
-- Documentation of differences to the reference implementation in https://github.com/pq-code-package/mlkem-native/pull/799
-- Addition of references to FIPS algorithms and equations to relevant functions in https://github.com/pq-code-package/mlkem-native/pull/776
+
+- Completion of functional correctness proofs of the AArch64 backend
+- Uniform licensing of all code in mlkem/* under Apache-2.0 OR ISC OR MIT
+- Numerous configuration option improvements
 - Numerous documentation improvements
-- Additional examples on using mlkem-native (see [examples/](examples/))
 
-See the full change log here: https://github.com/pq-code-package/mlkem-native/compare/v1.0.0-alpha...v1.0.0-beta
+See the full change log here: https://github.com/pq-code-package/mlkem-native/compare/v1.0.0-beta...v1.0.0