Keccak: include input buffer sizes in injectivity assumptions

CHANGELOG.md

@@ -14,6 +14,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - EVM.Solidity.toCode to include contractName in error string
 - Better cex reconstruction in cases where branches do not refer to all input variables in calldata
 - Correctly handle empty bytestring compiled contracts' JSON
+- No more false positives when keccak is called with inputs of different sizes
 
 ## Changed
 

src/EVM/Keccak.hs

@@ -56,7 +56,7 @@ minProp _ = internalError "expected keccak expression"
 
 injProp :: (Expr EWord, Expr EWord) -> Prop
 injProp (k1@(Keccak b1), k2@(Keccak b2)) =
-  POr (PEq b1 b2) (PNeg (PEq k1 k2))
+  POr ((b1 .== b2) .&& (bufLength b1 .== bufLength b2)) (PNeg (PEq k1 k2))
 injProp _ = internalError "expected keccak expression"
 
 -- Takes a list of props, find all keccak occurences and generates two kinds of assumptions:
@@ -90,7 +90,7 @@ computeKeccakProp :: Prop -> [Prop]
 computeKeccakProp p = foldProp compute [] p
 
 keccakCompute :: [Prop] -> [Expr Buf] -> [Expr Storage] -> [Prop]
-keccakCompute ps buf stores = 
+keccakCompute ps buf stores =
   concatMap computeKeccakProp ps <>
   concatMap computeKeccakExpr buf <>
   concatMap computeKeccakExpr stores

test/test.hs

@@ -1931,6 +1931,21 @@ tests = testGroup "hevm"
           (_, [Qed _]) <- withSolvers Z3 1 Nothing $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
           putStrLn "oob byte reads always return 0"
         ,
+        testCase "injectivity of keccak (diff sizes)" $ do
+          Just c <- solcRuntime "A"
+            [i|
+            contract A {
+              function f(uint128 x, uint256 y) external pure {
+                assert(
+                    keccak256(abi.encodePacked(x)) !=
+                    keccak256(abi.encodePacked(y))
+                );
+              }
+            }
+            |]
+          Right _ <- reachableUserAsserts c (Just $ Sig "f(uint128,uint256)" [AbiUIntType 128, AbiUIntType 256])
+          pure ()
+        ,
         testCase "injectivity of keccak (32 bytes)" $ do
           Just c <- solcRuntime "A"
             [i|