CBMC: Update to Version 6 (#71)

* CBMC: Update to Version 6 Signed-off-by: Hanno Becker <[email protected]> * Remove no longer needed INDENT-OFF/ON annotations Previously, those were needed to avoid `astyle` turning a CBMC implication `==>` into `== >`, but it has since been reconfigured to not do that. The annotations are therefore unnecessary. Signed-off-by: Hanno Becker <[email protected]> * CBMC: Remove `--object-bits` from goto-cc command line `--object-bits` has been moved from `goto-cc` to `CBMC` in CBMC 6. Signed-off-by: Hanno Becker <[email protected]> * CBMC: Work around naming but As documented in diffblue/cbmc#8337, problems arise when there's a name clash between a variable name in a `CPROVER_forall` annotation, and a variable used in the code it applies to. Avoid this issue by using separate variable names. Signed-off-by: Hanno Becker <[email protected]> * Appease `astyle` Signed-off-by: Hanno Becker <[email protected]> * Update cbmc/proofs/Makefile.common Signed-off-by: Hanno Becker <[email protected]> --------- Signed-off-by: Hanno Becker <[email protected]>
pq-code-package · Jun 21, 2024 · e07383c · e07383c
1 parent b84f0a3
commit e07383c
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 14 deletions.
diff --git a/cbmc/proofs/Makefile.common b/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)

diff --git a/cbmc/proofs/poly_compress/poly_compress_harness.c b/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);
 }
diff --git a/cbmc/proofs/poly_decompress/poly_decompress_harness.c b/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*
 }
diff --git a/flake.nix b/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=";
             };
           });
 

diff --git a/mlkem/poly.c b/mlkem/poly.c
@@ -166,15 +166,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;