Add setGas cheatcode (#2101)

* Add `setGas` cheatcode * Set Version: 1.0.310 * Set Version: 1.0.311 --------- Co-authored-by: devops <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Oct 3, 2023 · c0e85ad · c0e85ad
1 parent b1de680
commit c0e85ad
Show file tree

Hide file tree

Showing 4 changed files with 24 additions and 5 deletions.
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.310"
+version = "1.0.311"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.310'
+VERSION: Final = '1.0.311'
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md
@@ -885,12 +885,30 @@ function stopPrank() external;
 Gas Manipulation
 ----------------
 
+### `setGas` - Sets the current gas left (reported by `GAS` opcode) to a specific amount.
+
+```
+function setGas(uint256 newGas) external;
+```
+
+`setGas` is useful when writing tests that depend on the gas used, and so a specific concrete amount is needed instead of the default infinite gas.
+
+```{.k .bytes}
+    rule [foundry.call.setGas]:
+         <k> #call_foundry SELECTOR ARGS => . ... </k>
+         <gas> _ => #asWord(ARGS) </gas>
+         <callGas> _ => 0 </callGas>
+      requires SELECTOR ==Int selector ( "setGas(uint256)" )
+```
+
+### `infiniteGas` - Sets the remaining gas to an infinite value.
+
 ```
 function infiniteGas() external;
 ```
 
-Set the remaining gas to an infinite value.
-This is useful for running tests without them running out of gas.
+`infiniteGas` is useful for running tests without them running out of gas.
+It is applied by default.
 
 ```{.k .bytes .symbolic}
     rule [foundry.call.infiniteGas]:
@@ -1460,6 +1478,7 @@ If the production is matched when no prank is active, it will be ignored.
     rule ( selector ( "allowCallsToAddress(address)" )             => 1850795572 )
     rule ( selector ( "allowChangesToStorage(address,uint256)" )   => 4207417100 )
     rule ( selector ( "infiniteGas()" )                            => 3986649939 )
+    rule ( selector ( "setGas(uint256)" )                          => 3713137314 )
 ```
 
 - selectors for unimplemented cheat code functions.

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.310
+1.0.311
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@
		from typing import Final


		VERSION: Final = '1.0.310'
		VERSION: Final = '1.0.311'