Merge remote-tracking branch 'origin/master' into release

src/kontrol/prove.py

@@ -159,8 +159,11 @@ def _run_prover(_test_suite: list[FoundryTest], include_summaries: bool = False)
 
         constructor_results = _run_prover(constructor_tests, include_summaries=False)
         failed = [proof for proof in constructor_results if not proof.passed]
+        failed_contract_names = [proof.id.split('.')[0] for proof in failed]
         if failed:
-            raise ValueError(f'Running initialization code failed for {len(failed)} contracts: {failed}')
+            raise ValueError(
+                f"Running initialization code failed for {len(failed)} contracts: {', '.join(failed_contract_names)}"
+            )
 
     if options.verbose:
         _LOGGER.info(f'Running setup functions in parallel: {setup_method_names}')
@@ -170,8 +173,9 @@ def _run_prover(_test_suite: list[FoundryTest], include_summaries: bool = False)
     setup_results = _run_prover(setup_method_tests, include_summaries=False)
 
     failed = [proof for proof in setup_results if not proof.passed]
+    failed_contract_names = [proof.id.split('.')[0] for proof in failed]
     if failed:
-        raise ValueError(f'Running setUp method failed for {len(failed)} contracts: {failed}')
+        raise ValueError(f"Running setUp method failed for {len(failed)} contracts: {', '.join(failed_contract_names)}")
 
     if options.verbose:
         _LOGGER.info(f'Running test functions in parallel: {test_names}')
@@ -1440,7 +1444,7 @@ def _final_term(
 def _process_external_library_references(contract: Contract, foundry_contracts: dict[str, Contract]) -> list[KInner]:
     """Create a list of KInner accounts for external libraries used in the given contract.
 
-    This function identifies external library placeholders within the contract's deployed bytecode,
+    This function identifies external library placeholders within the contract's bytecode and deployed bytecode,
     deploys the required external libraries at the address generated based on the first 20 bytes of the hash of the
     unique id, replaces the placeholders with the actual addresses of the deployed libraries, and returns a list of
     KEVM account cells representing the deployed external libraries.
@@ -1454,39 +1458,51 @@ def _process_external_library_references(contract: Contract, foundry_contracts:
     external_libs: list[KInner] = []
     address_list: dict[str, str] = {}
 
-    for lib, ref_locations in contract.external_lib_refs.items():
-        ref_contract = foundry_contracts.get(lib)
-        if ref_contract is None:
-            raise ValueError(f'External library not found: {lib}')
-
-        if lib not in address_list:
-            new_address_hex = hash_str(lib)[:40].ljust(40, '0')
-            new_address_int = int(new_address_hex, 16)
-            _LOGGER.info(f'Deploying external library {lib} at address 0x{new_address_hex}')
-
-            ref_code = token(bytes.fromhex(ref_contract.deployed_bytecode))
-            external_libs.append(
-                KEVM.account_cell(
-                    id=token(new_address_int),
-                    balance=token(0),
-                    code=ref_code,
-                    storage=map_empty(),
-                    orig_storage=map_empty(),
-                    transient_storage=map_empty(),
-                    nonce=token(0),
+    for ref_type in ['bytecode_external_lib_refs', 'deployed_bytecode_external_lib_refs']:
+        lib_refs = getattr(contract, ref_type, {})
+
+        for lib, ref_locations in lib_refs.items():
+            ref_contract = foundry_contracts.get(lib)
+            if ref_contract is None:
+                raise ValueError(f'External library not found: {lib}')
+
+            if lib not in address_list:
+                new_address_hex = hash_str(lib)[:40].ljust(40, '0')
+                new_address_int = int(new_address_hex, 16)
+                _LOGGER.info(f'Deploying external library {lib} at address 0x{new_address_hex}')
+
+                # `deployed_bytecode` libraries are a subset of `bytecode` libraries
+                if ref_contract.bytecode_external_lib_refs:
+                    external_libs.extend(_process_external_library_references(ref_contract, foundry_contracts))
+
+                ref_code = token(bytes.fromhex(ref_contract.deployed_bytecode))
+                external_libs.append(
+                    KEVM.account_cell(
+                        id=token(new_address_int),
+                        balance=token(0),
+                        code=ref_code,
+                        storage=map_empty(),
+                        orig_storage=map_empty(),
+                        transient_storage=map_empty(),
+                        nonce=token(0),
+                    )
                 )
-            )
-            address_list[lib] = new_address_hex
-        else:
-            new_address_hex = address_list[lib]
-
-        for ref_start, ref_len in ref_locations:
-            placeholder_start = ref_start * 2
-            placeholder_len = ref_len * 2
-            contract.deployed_bytecode = (
-                contract.deployed_bytecode[:placeholder_start]
-                + new_address_hex
-                + contract.deployed_bytecode[placeholder_start + placeholder_len :]
-            )
+                address_list[lib] = new_address_hex
+            else:
+                new_address_hex = address_list[lib]
+
+            bytecode_field = 'bytecode' if ref_type == 'bytecode_external_lib_refs' else 'deployed_bytecode'
+
+            for ref_start, ref_len in ref_locations:
+                placeholder_start = ref_start * 2
+                placeholder_len = ref_len * 2
+
+                current_bytecode = getattr(contract, bytecode_field)
+                updated_bytecode = (
+                    current_bytecode[:placeholder_start]
+                    + new_address_hex
+                    + current_bytecode[placeholder_start + placeholder_len :]
+                )
+                setattr(contract, bytecode_field, updated_bytecode)
 
     return external_libs

src/kontrol/solc_to_k.py

@@ -768,7 +768,8 @@ def application(self) -> KInner:
     deployed_bytecode: str
     immutable_ranges: list[tuple[int, int]]
     link_ranges: list[tuple[int, int]]
-    external_lib_refs: dict[str, list[tuple[int, int]]]
+    bytecode_external_lib_refs: dict[str, list[tuple[int, int]]]
+    deployed_bytecode_external_lib_refs: dict[str, list[tuple[int, int]]]
     processed_link_refs: bool
     bytecode: str
     raw_sourcemap: str | None
@@ -792,29 +793,38 @@ def __init__(self, contract_name: str, contract_json: dict, foundry: bool = Fals
         evm = self.contract_json['evm'] if not foundry else self.contract_json
 
         deployed_bytecode = evm['deployedBytecode']
+        bytecode = evm['bytecode']
 
         self.immutable_ranges = [
             (rng['start'], rng['length'])
             for ref in deployed_bytecode.get('immutableReferences', {}).values()
             for rng in ref
         ]
 
-        self.external_lib_refs = {}
+        self.bytecode_external_lib_refs = {}
+        self.deployed_bytecode_external_lib_refs = {}
         self.link_ranges = []
 
-        for path, ref in deployed_bytecode.get('linkReferences', {}).items():
-            for contract_name, ranges in ref.items():
-                ref_name_with_path = contract_name_with_path(path, contract_name)
-                ranges = [(rng['start'], rng['length']) for rng in ranges]
-                self.link_ranges.extend(ranges)
-                self.external_lib_refs.setdefault(ref_name_with_path, []).extend(ranges)
+        def process_references(bytecode: dict, target_lib_refs: dict, update_link_ranges: bool = False) -> None:
+            for path, references in bytecode.get('linkReferences', {}).items():
+                for contract_name, ranges in references.items():
+                    ref_name_with_path = contract_name_with_path(path, contract_name)
+                    ranges = [(rng['start'], rng['length']) for rng in ranges]
+
+                    target_lib_refs.setdefault(ref_name_with_path, []).extend(ranges)
+
+                    if update_link_ranges:
+                        self.link_ranges.extend(ranges)
 
-        self.processed_link_refs = len(self.external_lib_refs) == 0
+        process_references(bytecode, self.bytecode_external_lib_refs)
+        process_references(deployed_bytecode, self.deployed_bytecode_external_lib_refs, update_link_ranges=True)
+
+        # `deployed_bytecode_external_lib_refs` is a subset of `bytecode_external_lib_refs`
+        self.processed_link_refs = len(self.bytecode_external_lib_refs) == 0
 
         self.deployed_bytecode = deployed_bytecode['object'].replace('0x', '')
         self.raw_sourcemap = deployed_bytecode['sourceMap'] if 'sourceMap' in deployed_bytecode else None
 
-        bytecode = evm['bytecode']
         self.bytecode = bytecode['object'].replace('0x', '')
         self.constructor = None
 

src/tests/integration/test-data/foundry-init-code

@@ -3,4 +3,5 @@ InitCodeTest.testFail_init()
 ConstructorArgsTest.test_constructor_args()
 ConstructorTest.test_constructor()
 ConstructorTest.testFail_constructor()
-ConstructorTest.run_constructor()
+ConstructorTest.run_constructor()
+ExternalNestedLibraryTest.testExtLibs()

src/tests/integration/test-data/foundry/test/ExternalNestedLibraryTest.t.sol

@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity ^0.8.13;
+
+import {Test, console} from "forge-std/Test.sol";
+
+library LibrarySum {
+    function sum(uint256 a, uint256 b) external pure returns (uint256 res) {
+        res = a + b;
+    }
+}
+
+library LibraryEq {
+    function eq(uint256 a, uint256 b, uint256 c) internal returns (bool res) {
+       uint256 sum = LibrarySum.sum(a, b);
+       return (sum == c);
+    }
+}
+
+contract ExternalNestedLibraryTest is Test {
+    uint256 public z = 10;
+
+    function testExtLibs() public {
+        uint256 x = 3;
+        uint256 y = 7;
+        bool res = LibraryEq.eq(x, y, z);
+        assert(res);
+    }
+}

src/tests/integration/test-data/show/contracts.k.expected

@@ -4915,6 +4915,144 @@ module S2KtestZModSimpleMath-CONTRACT
     rule  ( selector ( "square(uint256)" ) => 2066295049 )
 
 
+endmodule
+
+module S2KtestZModExternalNestedLibraryTest-CONTRACT
+    imports public FOUNDRY
+
+    syntax Contract ::= S2KtestZModExternalNestedLibraryTestContract
+
+    syntax S2KtestZModExternalNestedLibraryTestContract ::= "S2KtestZModExternalNestedLibraryTest" [symbol("contract_test%ExternalNestedLibraryTest")]
+
+    syntax Bytes ::= S2KtestZModExternalNestedLibraryTestContract "." S2KtestZModExternalNestedLibraryTestMethod [function, symbol("method_test%ExternalNestedLibraryTest")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KISZUndTEST" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KISZUndTEST_")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KexcludeArtifacts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KexcludeArtifacts_")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KexcludeContracts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KexcludeContracts_")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KexcludeSenders" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KexcludeSenders_")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2Kfailed" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2Kfailed_")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetArtifactSelectors_")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetArtifacts_")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetContracts" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetContracts_")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetSelectors" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetSelectors_")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtargetSenders" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtargetSenders_")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2KtestExtLibs" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2KtestExtLibs_")]
+
+    syntax S2KtestZModExternalNestedLibraryTestMethod ::= "S2Kz" "(" ")" [symbol("method_test%ExternalNestedLibraryTest_S2Kz_")]
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2KexcludeArtifacts ( ) => #abiCallData ( "excludeArtifacts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2KexcludeContracts ( ) => #abiCallData ( "excludeContracts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2KexcludeSenders ( ) => #abiCallData ( "excludeSenders" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2KtargetArtifacts ( ) => #abiCallData ( "targetArtifacts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2KtargetContracts ( ) => #abiCallData ( "targetContracts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2KtargetSelectors ( ) => #abiCallData ( "targetSelectors" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2KtargetSenders ( ) => #abiCallData ( "targetSenders" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2KtestExtLibs ( ) => #abiCallData ( "testExtLibs" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModExternalNestedLibraryTest . S2Kz ( ) => #abiCallData ( "z" , .TypedArgs ) )
+
+
+    rule  ( selector ( "IS_TEST()" ) => 4202047188 )
+
+
+    rule  ( selector ( "excludeArtifacts()" ) => 3041954473 )
+
+
+    rule  ( selector ( "excludeContracts()" ) => 3792478065 )
+
+
+    rule  ( selector ( "excludeSenders()" ) => 517440284 )
+
+
+    rule  ( selector ( "failed()" ) => 3124842406 )
+
+
+    rule  ( selector ( "targetArtifactSelectors()" ) => 1725540768 )
+
+
+    rule  ( selector ( "targetArtifacts()" ) => 2233625729 )
+
+
+    rule  ( selector ( "targetContracts()" ) => 1064470260 )
+
+
+    rule  ( selector ( "targetSelectors()" ) => 2439649222 )
+
+
+    rule  ( selector ( "targetSenders()" ) => 1046363171 )
+
+
+    rule  ( selector ( "testExtLibs()" ) => 4104885666 )
+
+
+    rule  ( selector ( "z()" ) => 3319234606 )
+
+
+endmodule
+
+module S2KtestZModLibraryEq-CONTRACT
+    imports public FOUNDRY
+
+    syntax Contract ::= S2KtestZModLibraryEqContract
+
+    syntax S2KtestZModLibraryEqContract ::= "S2KtestZModLibraryEq" [symbol("contract_test%LibraryEq")]
+
+endmodule
+
+module S2KtestZModLibrarySum-CONTRACT
+    imports public FOUNDRY
+
+    syntax Contract ::= S2KtestZModLibrarySumContract
+
+    syntax S2KtestZModLibrarySumContract ::= "S2KtestZModLibrarySum" [symbol("contract_test%LibrarySum")]
+
+    syntax Bytes ::= S2KtestZModLibrarySumContract "." S2KtestZModLibrarySumMethod [function, symbol("method_test%LibrarySum")]
+
+    syntax S2KtestZModLibrarySumMethod ::= "S2Ksum" "(" Int ":" "uint256" "," Int ":" "uint256" ")" [symbol("method_test%LibrarySum_S2Ksum_uint256_uint256")]
+
+    rule  ( S2KtestZModLibrarySum . S2Ksum ( V0_a : uint256 , V1_b : uint256 ) => #abiCallData ( "sum" , ( #uint256 ( V0_a ) , ( #uint256 ( V1_b ) , .TypedArgs ) ) ) )
+       ensures ( #rangeUInt ( 256 , V0_a )
+       andBool ( #rangeUInt ( 256 , V1_b )
+               ))
+
+
+    rule  ( selector ( "sum(uint256,uint256)" ) => 3402664347 )
+
+
 endmodule
 
 module S2KtestZModFfiTest-CONTRACT

src/tests/integration/test-data/show/foundry.k.expected

@@ -65,6 +65,9 @@ module FOUNDRY-MAIN
     imports public S2KtestZModReverterWithReturn-VERIFICATION
     imports public S2KtestZModExternalLibTest-VERIFICATION
     imports public S2KtestZModSimpleMath-VERIFICATION
+    imports public S2KtestZModExternalNestedLibraryTest-VERIFICATION
+    imports public S2KtestZModLibraryEq-VERIFICATION
+    imports public S2KtestZModLibrarySum-VERIFICATION
     imports public S2KtestZModFfiTest-VERIFICATION
     imports public S2KtestZModFilesTest-VERIFICATION
     imports public S2KtestZModForkTest-VERIFICATION
@@ -584,6 +587,27 @@ module S2KtestZModSimpleMath-VERIFICATION
 
 
 
+endmodule
+
+module S2KtestZModExternalNestedLibraryTest-VERIFICATION
+    imports public S2KtestZModExternalNestedLibraryTest-CONTRACT
+
+
+
+endmodule
+
+module S2KtestZModLibraryEq-VERIFICATION
+    imports public S2KtestZModLibraryEq-CONTRACT
+
+
+
+endmodule
+
+module S2KtestZModLibrarySum-VERIFICATION
+    imports public S2KtestZModLibrarySum-CONTRACT
+
+
+
 endmodule
 
 module S2KtestZModFfiTest-VERIFICATION