Incorrect gas metering for CALL

[wolflo]

Summary of the problem

Gas metering for CALL instructions that do not cause accounts to be added to the state trie still deducts the 25000 gas account creation cost in some cases.

Manticore version

0.3.4

Python version

3.8.3

Step to reproduce the behavior

A script that makes some relevant calls and logs the deducted gas can be found here, and should result in the output below:

user: 0xdc50f787714f7694b8191991269e2cb684fce07b
existing account: 0xffbb4f64add523a9ac621b32c0f3173184b3e1c9
non-existant account: 0x137665008fce9edef4456904d5401c71c71c71c7

call to existing account with value
----------
call from 0x21a6b66ca8cc804bfccfe2902a121f1c5493e207 to 0xffbb4f64add523a9ac621b32c0f3173184b3e1c9
value: 1
gas consumed: 32400

call to non-existant account without value
----------
call from 0x21a6b66ca8cc804bfccfe2902a121f1c5493e207 to 0x137665008fce9edef4456904d5401c71c71c71c7
value: 0
gas consumed: 25700

call to existing account without value
----------
call from 0x21a6b66ca8cc804bfccfe2902a121f1c5493e207 to 0xffbb4f64add523a9ac621b32c0f3173184b3e1c9
value: 0
gas consumed: 700

Expected behavior

Disclaimer: This is from my own reference, so it would be good to check against another source

base_gas = 700 + mem_expansion_cost
if call_value > 0: # sending value with call
    base_gas += 9000
    if is_empty(target_addr): # forcing a new account to be created in the state trie by sending value to empty account
        base_gas += 25000
# In addition, any call with `call_value > 0` has a 2300 gas stipend added to the gas sent with the call, which is then refunded to the caller if unspent.

• A call to an existing account with call_value > 0 should deduct 700 + 9000 - 2300 stipend = 7400 gas
• A call to an non-existant account with call_value == 0 should deduct 700 gas

Actual behavior

• A call to an existing account with call_value > 0 deducts 700 + 9000 + 25000 - 2300 = 32400 gas
• A call to an non-existant account with call_value == 0 deducts 700 + 25000 = 25700 gas

The 25000 gas deduction is charged if call_value > 0 OR is_empty(target_addr), when it should be charged iff call_value > 0 AND is_empty(target_addr).

References

• EIP-158
• The geth implementation: go-ethereum/core/vm/gas_table.go
• The relevant section from the Jello Paper:

// Cextra is the cost of executing the call* op, and is added to the gas sent with the call to get the total cost
// Gcall < SCHED > is the constant portion of the gas cost (700 since Tangerine Whistle hardfork)
rule [Cextra]:
     Cextra(SCHED, ISEMPTY, VALUE)
  => Gcall < SCHED > +Int Cnew(SCHED, ISEMPTY, VALUE) +Int Cxfer(SCHED, VALUE)

// Cnew is the cost of adding a new account to the state trie, applied if nonzero value is sent to an empty account
rule [Cnew]:
     Cnew(SCHED, ISEMPTY:Bool, VALUE)
  => #if ISEMPTY andBool (VALUE =/=Int 0 orBool Gzerovaluenewaccountgas << SCHED >>) #then Gnewaccount < SCHED > #else 0 #fi

// Cxfer is the cost of sending value with a call*
rule [Cxfer.none]: Cxfer(_SCHED, 0) => 0
rule [Cxfer.some]: Cxfer( SCHED, N) => Gcallvalue < SCHED > requires N =/=Int 0