Why the following rule passes?

[iirekm]

methods {
    function balances(address a) external returns(uint) envfree;
}

rule sameValue {
    method f;
    env e;
    calldataarg a;    
    mathint initValue = nativeBalances[e.msg.sender] + balances(e, e.msg.sender);
    f(e, a);
    assert initValue == nativeBalances[e.msg.sender] + balances(e, e.msg.sender);
}

// SPDX-License-Identifier: UNKNOWN 
pragma solidity ^0.8.30;
contract Vault {
    mapping(address => uint) public balances;

    function deposit() external payable {     
        //balances[msg.sender] += msg.value;
    }
}

The code contains and obvious bug (balances not updated, but certoraRun happily accepts it!!!
It's either a bug in the prover, or a bug in my rule - in the second case sanity checker should detect it but doesn't.

[iirekm]

Finally I figured it out, it's actually not 1 but 2 bugs in certoraRun:

• balances(e, ...) should be balances(...) - but certoraRun didn't even complain!!!
• require(msg.sender != address(this)); is required in deposit() - why??? this contract has no other methods, it can't call itself