comment

a16z · Oct 11, 2024 · 1259dbf · 1259dbf
1 parent 57bffaa
commit 1259dbf
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/src/halmos/utils.py b/src/halmos/utils.py
@@ -108,10 +108,14 @@ def f_sha3_name(bitsize: int) -> str:
     return f"f_sha3_{bitsize}"
 
 
+f_sha3_0_name = f_sha3_name(0)
 f_sha3_256_name = f_sha3_name(256)
 f_sha3_512_name = f_sha3_name(512)
 
-f_sha3_0_name = f_sha3_name(0)
+# NOTE: another way to encode the empty keccak is to use 0-ary function like:
+#         f_sha3_empty = Function(f_sha3_0_name, BitVecSort256)
+#       then `f_sha3_empty()` is equivalent to `BitVec(f_sha3_0_name, BitVecSort256)`.
+#       in both cases, decl() == f_sha3_0_name, and num_args() == 0.
 f_sha3_empty = BitVec(f_sha3_0_name, BitVecSort256)