methods {
  // REVERTS IF DECLARED:
  // upgradeAdmin() returns address envfree;
  function governorAdmin()
  external returns address envfree;
}

rule only_upgrade_admin_can_set_governor_admin(address a) {
  env e;
  address admin = upgradeAdmin(e);
  setGovernorAdmin@withrevert(e, a);

  assert lastReverted <=> (e.msg.sender != admin || a == 0), "did revert";

  require !lastReverted;
  assert governorAdmin() == a, "new admin not set";
}