Add minimal reproducible example for freshUInt / *Int normalization i…

…ssue

See https://github.com/runtimeverification/hs-backend-booster/issues/261

tests/foundry/normalization-lemmas.k

@@ -0,0 +1,8 @@
+requires "foundry.md"
+
+module NORMALIZATION-LEMMAS
+    imports FOUNDRY
+
+    rule A *Int B => B *Int A [concrete(A), symbolic(B), simplification(40)]
+
+endmodule

tests/foundry/reproduce.sh

@@ -0,0 +1,2 @@
+kevm foundry-kompile --verbose --require normalization-lemmas.k --module-import FreshIntTest:NORMALIZATION-LEMMAS --regen --with-llvm-library
+kevm foundry-prove --test FreshIntTest.test_uint256 --verbose --reinit --kore-rpc-command "kore-rpc-booster --simplify-after-exec --llvm-backend-library out/kompiled-llvm/interpreter.so"

tests/foundry/test/FreshInt.t.sol

@@ -8,6 +8,11 @@ contract FreshIntTest is Test, KEVMCheats {
     int128 constant min = -170141183460469231731687303715884105728;
     int128 constant max = 170141183460469231731687303715884105727;
 
+    function test_uint256() public {
+        kevm.infiniteGas();
+        uint256 fresh_uint256 = kevm.freshUInt(32);
+    }
+
     function test_uint128() public {
         kevm.infiniteGas();
         uint256 fresh_uint128 = uint256(kevm.freshUInt(32));