access_smt.sol

contract C
{
    constructor() payable {}
	function f(address payable a) public returns(bool) {
		require(1000 == address(this).balance);
		require(100 == a.balance);
		a.send(600);
		// a == this is not possible because address(this).balance == 1000
		// and a.balance == 100,
		// so this should hold in CHC, ignoring the transfer revert.
		return a.balance == 700;
	}
}
contract D {
    Forwarded immutable public f = new Forwarded();
    constructor() payable {}
    receive() payable external {
        // If `f` is not warm, then the call will go out of gas.
        // Need to call warm_it_up or use access lists to fix this.
        if (msg.value == 600)
            address(f).call{value: 600, gas: 0}("");
    }
    // Poor man's access list for warming up f
    function warm_it_up() external {
        address(f).call("");
    }
}

contract Forwarded {
    receive() payable external { }
    fallback() external {}
}

contract Test {
    C immutable c = new C{value: 1000}();
    D immutable d = new D{value: 100}();
    constructor() payable {}
    function test_with_warm() external returns (bool) {
        // This makes the `call` in a.transfer(600) cost 100 gas.
        // And `address(f).call{value: 600}("")` cost 100 gas
        d.warm_it_up();
        return c.f(payable(d));
    }
    function test_without_warming() external returns (bool) {
        return c.f(payable(d));
    }
}
// ====
// compileViaYul: also
// ----
// constructor(), 1100 wei ->
// gas legacy: 542327
// test_with_warm() -> false
// test_without_warming() -> false