String storage issues

[jinxinglim]

Version

Kontrol version: 3135126 (v0.1.278) - latest as of 16 May 2024

Issue

I am running some conformance checks via Kontrol for the ERC4626 vault, src/tokens/ERC4626.sol.

I have added the following test in test/ERC4626.t.sol to check if the function name() is callable:

    // name is callable
    function test_name_callable() public {
        vault.name();
    }

I ran the test with Kontrol and the proof failed unexpected:

Command:

kontrol build
kontrol prove --match-test test_name_callable --use-booster

Output:

Running functions: ['test%ERC4626Test.test_name_callable()']
PROOF FAILED: test%ERC4626Test.test_name_callable():0
time: 3m 35s
6 Failure nodes. (5 pending and 1 failing)

Pending nodes: [28, 29, 30, 31, 32]

Failing nodes:

  Node id: 27
  Failure reason:
    Matching failed.
    The remaining implication is:
    { true #Equals 0 <=Int CALLER_ID:Int }
    #And { true #Equals 0 <=Int ORIGIN_ID:Int }
    #And { true #Equals 0 <=Int NUMBER_CELL:Int }
    #And { true #Equals 0 <=Int TIMESTAMP_CELL:Int }
    #And #Not ( { CALLER_ID:Int #Equals 645326474426547203313410069153905908525362434349 } )
    #And #Not ( { ORIGIN_ID:Int #Equals 645326474426547203313410069153905908525362434349 } )
    #And #Not ( { CONTRACT_ID:Int #Equals 645326474426547203313410069153905908525362434349 } )
    #And { true #Equals CALLER_ID:Int <Int pow160 }
    #And { true #Equals ORIGIN_ID:Int <Int pow160 }
    #And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
    #And { true #Equals TIMESTAMP_CELL:Int <Int pow256 }
    #And #Not ( { 0 #Equals 1 &Int #lookup ( ?STORAGE:Map , 0 ) } )
    #And { false #Equals #range ( 0 < CALLER_ID:Int <= 9 ) }
    #And { false #Equals #range ( 0 < ORIGIN_ID:Int <= 9 ) }
    #And { 0 #Equals chop ( 1 &Int #lookup ( ?STORAGE:Map , 0 ) -Int bool2Word ( #lookup ( ?STORAGE:Map , 0 ) >>Int 1 <Int 32 ) ) } #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) }
  Path condition:
    #Not ( { 1 &Int #lookup ( ?STORAGE:Map , 0 ) #Equals 0 } )
#And { 0 #Equals chop ( 1 &Int #lookup ( ?STORAGE:Map , 0 ) -Int bool2Word ( #lookup ( ?STORAGE:Map , 0 ) >>Int 1 <Int 32 ) ) }
  Model:
    TIMESTAMP_CELL = 0
    ORIGIN_ID = 10
    ?STORAGE = ?STORAGE:Map
    CALLER_ID = 10
    CONTRACT_ID = 2
    NUMBER_CELL = 0

Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN

See `foundry_success` predicate for more information:
https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/foundry.md#foundry-success-predicate

Access documentation for Kontrol at https://docs.runtimeverification.com/kontrol

I have kontrol prove another similar test that check if the decimals() function is callable and it passed.

After discussion with @palinatolmach, we believe that this is most probably due to the storage for string variable as we think the proof got stuck at #lookup ( ?STORAGE:Map , 0 ). We also know that the storage layout for strings in solidity is different from how an uint is being stored (see this).

Question

Does anyone have experience this and could share how this could be addressed?

Remark

Ideally, this could be addressed at the backend side instead of requiring the user to add more assumption/s in such a simple test as it may deter users from running Kontrol over their existing Foundry tests. I have also created a new branch for anyone reproduce the outputs: https://github.com/runtimeverification/secureum-kontrol/tree/string-storage-issues, although I have added the kontrol outputs as well.

[palinatolmach]

String support is also relevant for CSE as discussed today with @PetarMax.

[PetarMax]

This is also relevant, from the official documentation.

[PetarMax]

I would suggest that the first PR handle only the case in which the length of the string is less than 32 bytes, which is the case that we need currently to work.

[nwatson22]

The reason test_name_callable is failing is because it branches on 0 ==Int chop ( ( ( 1 &Int #lookup ( ?STORAGE:Map , 0 ) ) -Int bool2Word ( #lookup ( ?STORAGE:Map , 0 ) >>Int 1 <Int 32 ) ) ), i.e. the lowest bit is 0 and the length portion is less than 32, or the lowest bit is 1 and the length portion is 32 or higher. This should never happen with bytecode that correctly encodes strings in storage.

I was thinking, and @PetarMax confirmed, that we should add a constraint using #lookUp for each string storage slot for each contract account that would allow these types of condition to simplify to false if the lookup is being done on the storage of some contract C's storage slot A if A is a string storage slot in C.

The problem is, given an account cell in the configuration, it is hard to tell which solidity contract it was created from and therefore which compiled definition we can use to get the storage layout metadata from. In the case where we are constructing the account cell ourselves during initialization, such as we do for CONTRACT_ID in summary mode and address_TEST_CONTRACT for test mode, we know this information, but in the case of this issue, the account we care about is created during execution.

I thought maybe we could match bytecode, since every solidity compiled definition has deployedBytecode and the accounts created from these contracts also has bytecode, but these can actually differ, at least in the case where there are immutables.

[nwatson22]

@jinxinglim @palinatolmach After discussion with @PetarMax I am wondering, is there any reason why we need the name field to be callable after abstracting the storage in the setUp function?

[PetarMax]

I have not fully understood the test until now. The function that's being called is a test function, and the storage is being abstracted manually as part of the setUp function. Moreover, the test just checks whether the function is callable, but I'm not sure how it could not be. It is not the idea, and was never the idea, to support structuring symbolic storage automatically in test functions. There, this needs to be done manually. The more informative test would be to:

1. Have the test contract have a string memory str field;
2. Create a symbolic string (I'm not sure how to do that) and assign it to str;
3. Pass that symbolic string to the constructor of `Vault``;
4. In the test, assert that vault.name() == str, or whatever the correct way to test string equality is.

Even like this, this would be a bit problematic because:

1. the representation of strings differs if its length is not greater than 31 and otherwise; and
2. when length is greater than 31, then we would run into the 32-byte copying loop, and so we would have to enforce a bound on the length of the symbolic string.

In any case, this is not something that we should be handling automatically in these scenarios. This should be handled automatically when analysing non-test functions, to construct their initial configuration.

[jinxinglim]

Hi @PetarMax and @nwatson22. Our ERCx tool does conformance checks for properties stated in the EIP standard. In this case, EIP-4626 stated that
"""
All EIP-4626 tokenized Vaults MUST implement EIP-20’s optional metadata extensions. The name and symbol functions SHOULD reflect the underlying token’s name and symbol in some way.
"""

Thus, in our ERC4626 test suite from ERCx, we have a Foundry test that checks for callability of the function name (see here:

    // name is callable
    function test_name_callable() public {
        vault.name();
    }

In the effort to make all tests in our ERC-4626 test suite to be runnable by Kontrol, I have tested each test one at a time to see if it can be run by Kontrol. And it somehow failed at this test, and hence, creating this issue to see if there is a need to make Kontrol able to run this test or any test with regards to string storage.

But after reading your points, I agree that it would be too problematic/troublesome just to find a fix for this. I can simply ignore the tests with regards to string storage from the ERC-4626 test suite.

@palinatolmach Do you think this is okay?

[palinatolmach]

@jinxinglim yes, I also think we can skip this test, probably not worth the trouble with getting it formally verified.

I think it would actually be beneficial to have structured symbolic storage for tests as well (we've discussed it with @anvacaru a few weeks ago and opened an issue on it), but I agree it's not the goal right now.

Since we need it for CSE, I think we can just add these string constraints for non-tests during the initial configuration construction, as @PetarMax said, and somewhat similar to what we're trying to do here: #600 — in _init_cterm, for example, we have access to bytecode and Contract object and fields (contract.fields) that we can use to identify the storage slot, variable name, etc., and add constraints. Another relevant PR that we didn't end up merging is #571.

[palinatolmach]

Closed as #627 has been merged.