`abi.encodeWith{Selector/Signature}` issues

Version

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

Issue

There seems to be an issue for running abi.encodeWith{Selector/Signature} with 1 (and perhaps more) parameters.

I have added the following tests in test/ERC4626.t.sol to check that the maxRedeem(address) does not revert:

    function test_maxRedeem_doesNotRevert_default(address owner)
    public {
        _notBuiltinAddress(owner);
        vault.maxRedeem(owner);
    }

    function test_maxRedeem_doesNotRevert_selector(address owner)
    public {
        _notBuiltinAddress(owner);
        bytes memory data = abi.encodeWithSelector(vault.maxRedeem.selector, owner);
        (bool success, ) = address(vault).call(data);
        assertTrue(success);
    }

    function test_maxRedeem_doesNotRevert_signature(address owner)
    public {
        _notBuiltinAddress(owner);
        bytes memory data = abi.encodeWithSignature("maxRedeem(address)", owner);
        (bool success, ) = address(vault).call(data);
        assertTrue(success);
    }

The above shows 3 versions of the same test - first one calls the function directly, the second uses abi.encodeWithSelector and the last uses abi.encodeWithSignature.

I ran the tests with Kontrol and the proofs of the 2nd and 3rd kontrol prove failed unexpected:

Command:

kontrol build
kontrol prove --match-test test_maxRedeem_doesNotRevert_default --use-booster
kontrol prove --match-test test_maxRedeem_doesNotRevert_selector --use-booster
kontrol prove --match-test test_maxRedeem_doesNotRevert_signature --use-booster

Output:

Running functions: ['test%ERC4626Test.test_maxRedeem_doesNotRevert_signature(address)']
PROOF FAILED: test%ERC4626Test.test_maxRedeem_doesNotRevert_signature(address):0
time: 14m 8s
28 Failure nodes. (27 pending and 1 failing)

Pending nodes: [80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106]

Failing nodes:

  Node id: 79
  Failure reason:
    Matching failed.
    The remaining implication is:
    #Not ( { VV0_owner_114b9705:Int #Equals 0 } )
    #And { 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 { true #Equals 0 <=Int VV0_owner_114b9705:Int }
    #And #Not ( { CALLER_ID:Int #Equals 645326474426547203313410069153905908525362434349 } )
    #And #Not ( { ORIGIN_ID:Int #Equals 645326474426547203313410069153905908525362434349 } )
    #And #Not ( { CONTRACT_ID:Int #Equals 645326474426547203313410069153905908525362434349 } )
    #And #Not ( { VV0_owner_114b9705:Int #Equals 263400868551549723330807389252719309078400616203 } )
    #And #Not ( { VV0_owner_114b9705:Int #Equals 491460923342184218035706888008750043977755113263 } )
    #And #Not ( { VV0_owner_114b9705:Int #Equals 645326474426547203313410069153905908525362434349 } )
    #And #Not ( { VV0_owner_114b9705:Int #Equals 728815563385977040452943777879061427756277306518 } )
    #And { true #Equals CALLER_ID:Int <Int pow160 }
    #And { true #Equals ORIGIN_ID:Int <Int pow160 }
    #And { true #Equals VV0_owner_114b9705:Int <Int pow160 }
    #And { true #Equals NUMBER_CELL:Int <=Int maxSInt256 }
    #And { true #Equals TIMESTAMP_CELL:Int <Int pow256 }
    #And { false #Equals #range ( 0 < CALLER_ID:Int <= 9 ) }
    #And { false #Equals #range ( 0 < ORIGIN_ID:Int <= 9 ) }
    #And { selector ( "approve(address,uint256)" ) #Equals 98161547082661246336730578112765835914329829418966647972474272684651600412672 |Int #asWord ( #range ( #buf ( 32 , VV0_owner_114b9705:Int ) , 0 , 28 ) ) >>Int 224 } #Implies { true #Equals foundry_success ( ... statusCode: EVMC_REVERT , failed: #lookup ( .Map , 46308022326495007027972728677917914892729792999299745830475596687180801507328 ) , revertExpected: false , opcodeExpected: false , recordEventExpected: false , eventExpected: false ) }
  Path condition:
    { true #Equals 98161547082661246336730578112765835914329829418966647972474272684651600412672 |Int #asWord ( #range ( #buf ( 32 , VV0_owner_114b9705:Int ) , 0 , 28 ) ) >>Int 224 <Int selector ( "pause()" ) }
#And { true #Equals 98161547082661246336730578112765835914329829418966647972474272684651600412672 |Int #asWord ( #range ( #buf ( 32 , VV0_owner_114b9705:Int ) , 0 , 28 ) ) >>Int 224 <Int selector ( "decimals()" ) }
#And { true #Equals selector ( "approve(address,uint256)" ) <=Int 98161547082661246336730578112765835914329829418966647972474272684651600412672 |Int #asWord ( #range ( #buf ( 32 , VV0_owner_114b9705:Int ) , 0 , 28 ) ) >>Int 224 }
#And { selector ( "approve(address,uint256)" ) #Equals 98161547082661246336730578112765835914329829418966647972474272684651600412672 |Int #asWord ( #range ( #buf ( 32 , VV0_owner_114b9705:Int ) , 0 , 28 ) ) >>Int 224 }
  Model:
    VV0_owner_114b9705 = 1
    ORIGIN_ID = 10
    CALLER_ID = 10
    TIMESTAMP_CELL = 0
    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

For some reasons, it is trying to prove some conditions about "approve(address,uint256)", "decimals()" and "pause()".

Furthermore, I made these 3 tests for the function asset() and balanceOf(address) and check if the parameter of abi.encodeWith{Signature/Selector} is causing the issue.

For the 3 tests for asset(), all tests passed. But for the 3 tests for balanceOf(address), only the test_balanceOf_doesNotRevert_default passed and the other 2 failed with a similar failed output of proving some conditions about "approve(address,uint256)", "decimals()" and "pause()".

Hence, I deduced that passing a parameter in abi.encodeWith{Signature/Selector} is causing the issue.

Remark

I have created a new branch for anyone reproduce the outputs: https://github.com/runtimeverification/secureum-kontrol/tree/abi-encode-issue, although I have added the kontrol outputs as well.

Start with the abi-encode-issue reproduction branch and the added tests in test/ERC4626.t.sol. Run kontrol build and the three kontrol prove commands for the direct, selector, and signature maxRedeem(address) cases, then compare them with the balanceOf(address) cases. Done means parameterized ABI calls prove without unrelated obligations involving approve(address,uint256), decimals(), or pause().