Merge branch 'pq-code-package:main' into prove_coeff_signed_to_unsigned

README.md

@@ -5,13 +5,14 @@
 ## Goals of mlkem-c-aarch64
 
 The primary goals of this project are as follows:
-- _Assurance:_ Clean code that's extensively tested and amenable for audit and verification
-- _Ease of use:_ Permissive licensing, modularity, few dependencies
+- _Assurance:_ Offer code that's extensively tested and amenable for audit and verification
+- _Ease of use:_ Permissive licensing, modularity, adaptability, few dependencies
 - _Performance:_ Competitive performance for most Armv8-A/Armv9-A platforms
 
 There are tensions between these goals:
 - Optimal code is target-specific, but a large variety of CPU-specific implementations makes a library harder to both use and maintain.
-- Optimal code is complex (e.g. relying on handwritten assembly), impeding maintainenance and amenability for audit or verification.
+- Optimal code is complex (e.g. relying on handwritten assembly and extensive interleaving), impeding maintainenance and
+  amenability for audit, and potentially hardening verification efforts.
 
 In doubt, **mlkem-c-aarch64** chooses assurance and ease of use over performance: We only include implementations into **mlkem-c-aarch64** which are manually auditable or (ideally _and_) for which we see a path towards formal verification. All assembly should be as readable as possible and micro-optimization ideally deferred to automated tooling such as [SLOTHY](https://slothy-optimizer.github.io/slothy/). Ultimately, **mlkem-c-aarch64** strives for constant-time implementations for which the C-code is, at minimum, verified to be free of undefined behaviour, and where all assembly is functionally verified.
 

cbmc/proofs/Makefile.common

@@ -517,7 +517,6 @@ COMMA :=,
 CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
 
 # --object_bits is removed in goto-cc 6.0.0
-COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS)
 
 DEFINES += -DCBMC=1
 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)

cbmc/proofs/poly_compress/poly_compress_harness.c

@@ -26,10 +26,9 @@ void harness(void)
     poly r;
     uint8_t a[KYBER_POLYCOMPRESSEDBYTES];
 
-    // *INDENT-OFF*
-    __CPROVER_assume(__CPROVER_forall {
+    __CPROVER_assume(__CPROVER_forall
+    {
         unsigned i; (i < KYBER_N) ==> ( -KYBER_Q <= r.coeffs[i] && r.coeffs[i] < KYBER_Q )
     });
-    // *INDENT-ON*
     poly_compress(a, &r);
 }

cbmc/proofs/poly_decompress/poly_decompress_harness.c

@@ -31,9 +31,8 @@ void harness(void)
     // TODO: We're replicating the post-condition of the function contract of
     // poly_decompress here. Ideally, we'd use CBMC's function contract mechanism
     // here, but there are still issues. cf. a similar comment in the Makefile.
-    // *INDENT-OFF*
-    __CPROVER_assert(__CPROVER_forall {
+    __CPROVER_assert(__CPROVER_forall
+    {
         unsigned i; (i < KYBER_N) ==> ( 0 <= r.coeffs[i] && r.coeffs[i] < KYBER_Q )
     }, "failed to prove post-condition for poly_decompress");
-    // *INDENT-ON*
 }

flake.nix

@@ -28,12 +28,12 @@
             };
           });
           cbmc = pkgs.cbmc.overrideAttrs (old: rec {
-            version = "731338d5d82ac86fc447015e0bd24cdf7a74c442";
+            version = "a8b8f0fd2ad2166d71ccce97dd6925198a018144";
             src = pkgs.fetchFromGitHub {
               owner = "diffblue";
               repo = old.pname;
               rev = "${version}";
-              hash = "sha256-fDLSo5EeHyPTliAqFp+5mfaB0iZXIMXeMyF21fjl5k4=";
+              hash = "sha256-mPRkkKN7Hz9Qi6a3fEwVFh7a9OaBFcksNw9qwNOarao=";
             };
           });
 

mlkem/poly.c

@@ -198,15 +198,16 @@ void poly_compress(uint8_t r[KYBER_POLYCOMPRESSEDBYTES], const poly *a)
 **************************************************/
 void poly_decompress(poly *r, const uint8_t a[KYBER_POLYCOMPRESSEDBYTES])
 /* ------ CBMC contract ------ */
-// *INDENT-OFF*
 __CPROVER_requires(__CPROVER_is_fresh(r, sizeof(*r)))
 __CPROVER_requires(__CPROVER_is_fresh(a, sizeof(KYBER_POLYCOMPRESSEDBYTES)))
 __CPROVER_ensures(
-/* Output coefficients are unsigned canonical */
-__CPROVER_forall {
-  unsigned i; (i < KYBER_N) ==> ( 0 <= r->coeffs[i] && r->coeffs[i] < KYBER_Q )
+    /* Output coefficients are unsigned canonical */
+    /* NOTE: Because of https://github.com/diffblue/cbmc/issues/8337 we have to
+             avoid a variable name clash with variables used by poly_decompress. */
+    __CPROVER_forall
+{
+    unsigned _i; (_i < KYBER_N) ==> ( 0 <= r->coeffs[_i] && r->coeffs[_i] < KYBER_Q )
 })
-// *INDENT-ON*
 /* --- End of CBMC contract --- */
 {
     unsigned int i;