add comment

a16z · Sep 12, 2023 · daee470 · daee470
1 parent bd2c78c
commit daee470
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
@@ -1173,6 +1173,9 @@ def decode(cls, loc: Any) -> Any:
 
     @classmethod
     def simple_hash(cls, x: BitVecRef) -> BitVecRef:
+        # simple injective function for collision-free (though not secure) hash semantics, comprising:
+        # - left-shift by 256 bits to ensure sufficient logical domain space
+        # - an additional 1-bit for disambiguation (e.g., between map[key] vs array[i][j])
         return simplify(Concat(x, con(0, 257)))
 
     @classmethod