message: [stdlib]PackageTxnManager Spec.
diff: @@ -105,11 +105,13 @@ address 0x1 {
  aborts_if !exists<ModuleUpgradeStrategy>(Signer::address_of(account)) && strategy == 0;
  aborts_if strategy == 1 && exists<UpgradePlanCapability>(Signer::address_of(account));
  + aborts_if strategy == 1 && !exists<Config::ModifyConfigCapabilityHolder<Version::Version>>(Signer::address_of(account));
  + let holder = global<Config::ModifyConfigCapabilityHolder<Version::Version>>(Signer::address_of(account));
  + aborts_if strategy == 1 && Option::spec_is_none<Config::ModifyConfigCapability<Version::Version>>(holder.cap);
  aborts_if strategy == 1 && exists<TwoPhaseUpgrade>(Signer::address_of(account));
  aborts_if exists<ModuleUpgradeStrategy>(Signer::address_of(account)) && global<ModuleUpgradeStrategy>(Signer::address_of(account)).strategy == 1
  && !exists<TwoPhaseUpgrade>(Signer::address_of(account));
  - pragma verify = false;
  }
  public fun account_address(cap: &UpgradePlanCapability): address {
  @@ -304,7 +306,8 @@ address 0x1 {
  spec fun finish_upgrade_plan {
  aborts_if !exists<TwoPhaseUpgrade>(package_address);
  - pragma verify = false;
  + let tpu = global<TwoPhaseUpgrade>(package_address);
  + aborts_if Option::spec_is_some(tpu.plan) && !exists<Config::Config<Version::Version>>(tpu.version_cap.account_address);
  }
  public fun package_txn_prologue(account: &signer, package_address: address, package_hash: vector<u8>) acquires TwoPhaseUpgrade, ModuleUpgradeStrategy {
  @@ -341,7 +344,9 @@ address 0x1 {
  aborts_if Signer::address_of(account) != CoreAddresses::SPEC_GENESIS_ADDRESS();
  aborts_if spec_get_module_upgrade_strategy(package_address) == 1
  && success && !exists<TwoPhaseUpgrade>(package_address);
  - pragma verify = false;
  + aborts_if spec_get_module_upgrade_strategy(package_address) == 1
  + && success && Option::spec_is_some(global<TwoPhaseUpgrade>(package_address).plan)
  + && !exists<Config::Config<Version::Version>>(global<TwoPhaseUpgrade>(package_address).version_cap.account_address);
  }
  }
  