[WIP] Calldata generation for bytes, bytes[] parameters

package/version

@@ -1 +1 @@
-0.1.127
+0.1.128

pyproject.toml

@@ -4,15 +4,15 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.127"
+version = "0.1.128"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
 ]
 
 [tool.poetry.dependencies]
 python = "^3.10"
-kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.427", subdirectory = "kevm-pyk" }
+kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", branch = "dynamic-tuple", subdirectory = "kevm-pyk" }
 
 [tool.poetry.group.dev.dependencies]
 autoflake = "*"

src/kontrol/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.127'
+VERSION: Final = '0.1.128'

src/kontrol/foundry.py

@@ -245,7 +245,7 @@ def custom_view(self, contract_name: str, element: KCFGElem) -> Iterable[str]:
 
     def build(self) -> None:
         try:
-            run_process(['forge', 'build', '--root', str(self._root)], logger=_LOGGER)
+            run_process(['forge', 'build', '--root', str(self._root), '--extra-output', 'devdoc'], logger=_LOGGER)
         except FileNotFoundError:
             print("Error: 'forge' command not found. Please ensure that 'forge' is installed and added to your PATH.")
             sys.exit(1)

src/kontrol/kdist/cheatcodes.md

@@ -345,6 +345,7 @@ The `<output>` cell will be updated with the value of the address generated from
          <k> #call_foundry SELECTOR ARGS => . ... </k>
          <output> _ => #bufStrict(32, #addrFromPrivateKey(#unparseDataBytes(ARGS))) </output>
       requires SELECTOR ==Int selector ( "addr(uint256)" )
+      [preserves-definedness]
 ```
 
 #### `load` - Loads a storage slot from an address.
@@ -896,6 +897,7 @@ The `ECDSASign` function returns the signed data in [r,s,v] form, which we conve
          <k> #call_foundry SELECTOR ARGS => . ... </k>
          <output> _ => #sign(#range(ARGS, 32, 32),#range(ARGS,0,32)) </output>
       requires SELECTOR ==Int selector ( "sign(uint256,bytes32)" )
+      [preserves-definedness]
 ```
 
 Otherwise, throw an error for any other call to the Foundry contract.
@@ -943,6 +945,7 @@ Utils
            <code> _ => #if #asWord(CODE) ==Int 0 #then .Bytes #else CODE #fi </code>
            ...
          </account>
+    [preserves-definedness]
 ```
 
 - `#returnNonce ACCTID` takes the nonce of a given account and places it on the `<output>` cell.
@@ -997,6 +1000,7 @@ Utils
            <storage> STORAGE => STORAGE [ LOC <- VALUE ] </storage>
              ...
          </account>
+    [preserves-definedness]
 ```
 
 `#setSymbolicStorage ACCTID` takes a given account and makes its storage fully symbolic.

src/kontrol/prove.py

@@ -478,6 +478,10 @@ def _update_cterm_from_node(cterm: CTerm, node: KCFG.Node, contract_name: str) -
     new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'GAS_CELL', gas_cell), [])
     new_init_cterm = CTerm(set_cell(new_init_cterm.config, 'CALLGAS_CELL', callgas_cell), [])
 
+    # adding constraints from the initial cterm
+    for constraint in cterm.constraints:
+        new_init_cterm = new_init_cterm.add_constraint(constraint)
+
     return new_init_cterm