Use infinite gas by default, add setGas cheatcode (#57)

* Use infinite gas by default; add `setGas` * Set Version: 0.1.10 * Set Version: 0.1.15 * Update invariant for `LoopsTest.sum_N` * Remove `infiniteGas()` from `FreshIntTest` * Update loop invariant for `sum_n`, expected output * Set Version: 0.1.16 * Set Version: 0.1.17 --------- Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
runtimeverification · Oct 4, 2023 · 336c92e · 336c92e
1 parent f624112
commit 336c92e
Show file tree

Hide file tree

Showing 26 changed files with 1,065 additions and 1,049 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.16
+0.1.17
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.16"
+version = "0.1.17"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
@@ -425,7 +425,7 @@ def _init_cterm(
         'MEMORYUSED_CELL': intToken(0),
         'WORDSTACK_CELL': KApply('.WordStack_EVM-TYPES_WordStack'),
         'PC_CELL': intToken(0),
-        'GAS_CELL': intToken(9223372036854775807),
+        'GAS_CELL': KEVM.inf_gas(KVariable('VGAS')),
         'K_CELL': KSequence([KEVM.sharp_execute(), KVariable('CONTINUATION')]),
         'ACCOUNTS_CELL': KEVM.accounts(
             [

diff --git a/src/tests/integration/test-data/contracts.k.expected b/src/tests/integration/test-data/contracts.k.expected
@@ -5177,6 +5177,8 @@ module GasTest-CONTRACT
 
     syntax S2KGasTestMethod ::= "S2KtestInfiniteGas" "(" ")" [symbol(), klabel(method_GasTest_S2KtestInfiniteGas_)]
 
+    syntax S2KGasTestMethod ::= "S2KtestSetGas" "(" ")" [symbol(), klabel(method_GasTest_S2KtestSetGas_)]
+
     rule  ( S2KGasTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) )
 
 
@@ -5213,6 +5215,9 @@ module GasTest-CONTRACT
     rule  ( S2KGasTest . S2KtestInfiniteGas ( ) => #abiCallData ( "testInfiniteGas" , .TypedArgs ) )
 
 
+    rule  ( S2KGasTest . S2KtestSetGas ( ) => #abiCallData ( "testSetGas" , .TypedArgs ) )
+
+
     rule  ( selector ( "IS_TEST()" ) => 4202047188 )
 
 
@@ -5248,6 +5253,9 @@ module GasTest-CONTRACT
 
     rule  ( selector ( "testInfiniteGas()" ) => 1677640502 )
 
+
+    rule  ( selector ( "testSetGas()" ) => 2307678515 )
+
 
 endmodule
 
@@ -5633,6 +5641,8 @@ module KEVMCheatsBase-CONTRACT
 
     syntax S2KKEVMCheatsBaseMethod ::= "S2KinfiniteGas" "(" ")" [symbol(), klabel(method_KEVMCheatsBase_S2KinfiniteGas_)]
 
+    syntax S2KKEVMCheatsBaseMethod ::= "S2KsetGas" "(" Int ":" "uint256" ")" [symbol(), klabel(method_KEVMCheatsBase_S2KsetGas_uint256)]
+
     syntax S2KKEVMCheatsBaseMethod ::= "S2KsymbolicStorage" "(" Int ":" "address" ")" [symbol(), klabel(method_KEVMCheatsBase_S2KsymbolicStorage_address)]
 
     rule  ( S2KKEVMCheatsBase . S2KallowCallsToAddress ( V0_ : address ) => #abiCallData ( "allowCallsToAddress" , #address ( V0_ ) , .TypedArgs ) )
@@ -5697,6 +5707,10 @@ module KEVMCheatsBase-CONTRACT
     rule  ( S2KKEVMCheatsBase . S2KinfiniteGas ( ) => #abiCallData ( "infiniteGas" , .TypedArgs ) )
 
 
+    rule  ( S2KKEVMCheatsBase . S2KsetGas ( V0_ : uint256 ) => #abiCallData ( "setGas" , #uint256 ( V0_ ) , .TypedArgs ) )
+       ensures #rangeUInt ( 256 , V0_ )
+
+
     rule  ( S2KKEVMCheatsBase . S2KsymbolicStorage ( V0_ : address ) => #abiCallData ( "symbolicStorage" , #address ( V0_ ) , .TypedArgs ) )
        ensures #rangeAddress ( V0_ )
 
@@ -5737,6 +5751,9 @@ module KEVMCheatsBase-CONTRACT
     rule  ( selector ( "infiniteGas()" ) => 3986649939 )
 
 
+    rule  ( selector ( "setGas(uint256)" ) => 3713137314 )
+
+
     rule  ( selector ( "symbolicStorage(address)" ) => 769677742 )
 
 
@@ -6038,6 +6055,8 @@ module LoopsTest-CONTRACT
 
     syntax S2KLoopsTestMethod ::= "S2Kfailed" "(" ")" [symbol(), klabel(method_LoopsTest_S2Kfailed_)]
 
+    syntax S2KLoopsTestMethod ::= "S2Kkevm" "(" ")" [symbol(), klabel(method_LoopsTest_S2Kkevm_)]
+
     syntax S2KLoopsTestMethod ::= "S2KsumZUndN" "(" Int ":" "uint256" ")" [symbol(), klabel(method_LoopsTest_S2KsumZUndN_uint256)]
 
     syntax S2KLoopsTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol(), klabel(method_LoopsTest_S2KtargetArtifactSelectors_)]
@@ -6095,6 +6114,9 @@ module LoopsTest-CONTRACT
     rule  ( S2KLoopsTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
 
 
+    rule  ( S2KLoopsTest . S2Kkevm ( ) => #abiCallData ( "kevm" , .TypedArgs ) )
+
+
     rule  ( S2KLoopsTest . S2KsumZUndN ( V0_n : uint256 ) => #abiCallData ( "sum_N" , #uint256 ( V0_n ) , .TypedArgs ) )
        ensures #rangeUInt ( 256 , V0_n )
 
@@ -6176,6 +6198,9 @@ module LoopsTest-CONTRACT
     rule  ( selector ( "failed()" ) => 3124842406 )
 
 
+    rule  ( selector ( "kevm()" ) => 3601001590 )
+
+
     rule  ( selector ( "sum_N(uint256)" ) => 2123244496 )
 
 

diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all
@@ -120,6 +120,7 @@ ForkTest.testRollForkId()
 ForkTest.testRPCUrl()
 ForkTest.testRPCUrlRevert()
 GasTest.testInfiniteGas()
+GasTest.testSetGas()
 GetCodeTest.testGetCode()
 LabelTest.testLabel()
 LoopsTest.sum_N(uint256)

diff --git a/src/tests/integration/test-data/foundry/src/KEVMCheats.sol b/src/tests/integration/test-data/foundry/src/KEVMCheats.sol
@@ -23,8 +23,10 @@ interface KEVMCheatsBase {
     function allowCallsToAddress(address) external;
     // Adds an address and a storage slot to the whitelist.
     function allowChangesToStorage(address,uint256) external;
-    // Set the current <gas> cell
+    // Sets the remaining gas to an infinite value.
     function infiniteGas() external;
+    // Sets the current <gas> cell to the supplied amount.
+    function setGas(uint256) external;
     // Returns a symbolic unsigned integer
     function freshUInt(uint8) external returns (uint256);
     // Returns a symbolic boolean value

diff --git a/src/tests/integration/test-data/foundry/test/CounterTest.t.sol b/src/tests/integration/test-data/foundry/test/CounterTest.t.sol
@@ -25,7 +25,6 @@ contract CounterTest is Test, KEVMCheats {
     // }
 
     function testIncrement() public {
-        kevm.infiniteGas();
         counter = new Counter();
         counter.setNumber(0);
         counter.increment();
@@ -34,7 +33,6 @@ contract CounterTest is Test, KEVMCheats {
 
     function testSetNumber(uint256 x) public {
         //setUp();
-        kevm.infiniteGas();
         counter = new Counter();
         counter.setNumber(0);
         counter.setNumber(x);

diff --git a/src/tests/integration/test-data/foundry/test/FreshInt.t.sol b/src/tests/integration/test-data/foundry/test/FreshInt.t.sol
@@ -9,28 +9,24 @@ contract FreshIntTest is Test, KEVMCheats {
     int128 constant max = 170141183460469231731687303715884105727;
 
     function test_uint128() public {
-        kevm.infiniteGas();
         uint256 fresh_uint128 = uint256(kevm.freshUInt(32));
         assertGe(fresh_uint128, type(uint128).min);
         assertLe(fresh_uint128, type(uint128).max);
     }
 
     function test_bool() public {
-        kevm.infiniteGas();
         uint256 fresh_uint256 = kevm.freshBool();
         assertGe(fresh_uint256, 0);
         assertLe(fresh_uint256, 1);
     }
 
     function test_int128() public {
-        kevm.infiniteGas();
         int128 val = int128(uint128(kevm.freshUInt(16)));
         assertGe(val, min);
         assertLe(val, max);
     }
 
     function testFail_int128() public {
-        kevm.infiniteGas();
         int128 val = int128(uint128(kevm.freshUInt(16)));
         assertGt(val, max);
     }

diff --git a/src/tests/integration/test-data/foundry/test/GasTest.t.sol b/src/tests/integration/test-data/foundry/test/GasTest.t.sol
@@ -6,7 +6,7 @@ import "../src/KEVMCheats.sol";
 
 contract GasTest is Test, KEVMCheats {
     function testInfiniteGas() public {
-        kevm.infiniteGas();
+        // Infinite gas is used by default
         uint256 gasLeftBefore = gasleft();
         uint256 x = 345;
         uint256 y = 928;
@@ -15,4 +15,11 @@ contract GasTest is Test, KEVMCheats {
         assert(gasLeftBefore <= gasLeftAfter);
         assert(gasLeftAfter <= gasLeftBefore);
     }
-}
+
+    function testSetGas() public {
+        kevm.setGas(33000);
+        uint256 gasLeftBefore = gasleft();
+        uint256 gasLeftAfter  = gasleft();
+        assert(gasLeftBefore > gasLeftAfter);
+    }
+}
diff --git a/src/tests/integration/test-data/foundry/test/Loops.t.sol b/src/tests/integration/test-data/foundry/test/Loops.t.sol
@@ -2,8 +2,9 @@
 pragma solidity =0.8.13;
 
 import "forge-std/Test.sol";
+import "../src/KEVMCheats.sol";
 
-contract LoopsTest is Test {
+contract LoopsTest is Test, KEVMCheats {
 
     uint constant WAD = 10 ** 18;
     uint constant RAY = 10 ** 27;
@@ -54,6 +55,8 @@ contract LoopsTest is Test {
         // Number of iterations: n
         // 9223372036854772642 // 178 = 51816696836262767
         vm.assume(n <= 51816696836262767);
+        // Allocating enough gas for the loop to be analyzed
+        kevm.setGas(9223372036854772693);
         uint s = 0;
         while (0 < n) {
             s = s + n;

diff --git a/src/tests/integration/test-data/foundry/test/Simple.t.sol b/src/tests/integration/test-data/foundry/test/Simple.t.sol
@@ -29,7 +29,6 @@ contract AssertTest is Test, KEVMCheats {
     }
 
     function test_branch_merge(uint x) public {
-        kevm.infiniteGas();
         if (x < 10) {
             y = 0;
         } else {