openzeppelin-contracts/certora/specs/helpers.spec

definition nonpayable(env e) returns bool = e.msg.value == 0;