CBMC: Add missing function contract to shake128x4_absorb

Signed-off-by: Matthias J. Kannwischer <[email protected]>
pq-code-package · Dec 4, 2024 · 7ffd473 · 7ffd473
1 parent 11b8a2f
commit 7ffd473
Showing 1 changed file with 9 additions and 2 deletions.
diff --git a/fips202/fips202x4.h b/fips202/fips202x4.h
@@ -16,8 +16,15 @@
 #define shake128x4_absorb FIPS202_NAMESPACE(shake128x4_absorb)
 void shake128x4_absorb(keccakx4_state *state, const uint8_t *in0,
                        const uint8_t *in1, const uint8_t *in2,
-                       const uint8_t *in3, size_t inlen);
-
+                       const uint8_t *in3, size_t inlen)
+__contract__(
+  requires(memory_no_alias(state, sizeof(keccakx4_state)))
+  requires(memory_no_alias(in0, inlen))
+  requires(memory_no_alias(in1, inlen))
+  requires(memory_no_alias(in2, inlen))
+  requires(memory_no_alias(in3, inlen))
+  assigns(object_whole(state))
+);
 
 #define shake256x4_absorb FIPS202_NAMESPACE(shake256x4_absorb)
 void shake256x4_absorb(keccakx4_state *state, const uint8_t *in0,