[move-prover] Revived invariant disabling

In PR aptos-labs#8840, all pragmas disabling invariants were commented out
and some invariants were weakened because we found that we needed
greater control over which invariants were disabled in order to
avoid false positives.

This PR has a feature "invariant [suspendable] ...." that indicates
that an invariant should be disabled in the body of a function when
pragma disable_invariants_in_body appears in the spec of that
function.  Other invariants will not be disabled.  This turns out to
work (at least for the Diem framework) because most invariants don't
need to be disabled and turn out to be useful for, e.g., proving the
absence of abort conditions.

There is a small change to add the pragma, and changes in
verification_analysis_v2.rs to compute a smaller set of disabled predicates
by limiting to the suspendable invariants.

Numerous changes were in DiemAccount.move, to disable invariants in
some functions, strengthen those invariants, and declare some new
friend functions in Roles.move.

Several bugs have been fixed where invariants were asserted/assumed
in the wrong place.

NOTE: This PR is more correct than the previous state, but there are
still bugs, including potential soundness bugs.  Also, changes to
fix soundness issues with type parameters do not play well with the
some of the invariant code, so more work is needed, including some
careful thinking through of soundness arguments.

Closes: aptos-labs#8907

language/diem-framework/modules/Diem.move

@@ -1754,9 +1754,11 @@ module DiemFramework::Diem {
             spec_is_currency<coin_type>();
 
         /// A `PreburnQueue` resource can only be published holding a currency type.
-        invariant forall addr: address, coin_type: type
-            where exists<PreburnQueue<coin_type>>(addr):
-            spec_is_currency<coin_type>();
+        /// >TODO: This assertion is causing a violation for unknown reasons, probably
+        /// a prover bug.
+        // invariant forall addr: address, coin_type: type
+        //     where exists<PreburnQueue<coin_type>>(addr):
+        //     spec_is_currency<coin_type>();
 
         /// Preburn is not transferrable [[J4]][PERMISSION].
         apply PreservePreburnQueueExistence<CoinType> to *<CoinType>;

language/diem-framework/modules/DiemAccount.move

@@ -1215,8 +1215,7 @@ module DiemFramework::DiemAccount {
     }
 
     spec create_diem_root_account {
-// TODO: Temporarily commented out until inv disable is fixed
-//        pragma disable_invariants_in_body;
+        pragma disable_invariants_in_body;
         pragma opaque;
         include CreateDiemRootAccountModifies;
         include CreateDiemRootAccountAbortsIf;
@@ -1279,8 +1278,7 @@ module DiemFramework::DiemAccount {
         make_account(&new_account, auth_key_prefix)
     }
     spec create_treasury_compliance_account {
-// TODO: Temporarily commented out until inv disable is fixed
-//      pragma disable_invariants_in_body;
+        pragma disable_invariants_in_body;
         pragma opaque;
         let tc_addr = @TreasuryCompliance;
         include CreateTreasuryComplianceAccountModifies;
@@ -1350,8 +1348,7 @@ module DiemFramework::DiemAccount {
     }
 
     spec create_designated_dealer {
-// TODO: Temporarily commented out until inv disable is fixed
-//      pragma disable_invariants_in_body;
+        pragma disable_invariants_in_body;
         include CreateDesignatedDealerAbortsIf<CoinType>;
         include CreateDesignatedDealerEnsures<CoinType>;
         include MakeAccountEmits;
@@ -1400,12 +1397,15 @@ module DiemFramework::DiemAccount {
         DualAttestation::publish_credential(&new_account, creator_account, human_name);
         VASPDomain::publish_vasp_domains(&new_account);
         make_account(&new_account, auth_key_prefix);
-        add_currencies_for_account<Token>(&new_account, add_all_currencies)
+        add_currencies_for_account<Token>(&new_account, add_all_currencies);
+        spec {
+            assert exists<VASPDomain::VASPDomains>(Signer::address_of(new_account));
+            assert Roles::spec_has_treasury_compliance_role_addr(Signer::address_of(creator_account));
+        }
     }
 
     spec create_parent_vasp_account {
-// TODO: Temporarily commented out until inv disable is fixed
-//      pragma disable_invariants_in_body;
+        pragma disable_invariants_in_body;
         include CreateParentVASPAccountAbortsIf<Token>;
         include CreateParentVASPAccountEnsures<Token>;
         include MakeAccountEmits;
@@ -1453,11 +1453,10 @@ module DiemFramework::DiemAccount {
         );
         Event::publish_generator(&new_account);
         make_account(&new_account, auth_key_prefix);
-        add_currencies_for_account<Token>(&new_account, add_all_currencies)
+        add_currencies_for_account<Token>(&new_account, add_all_currencies);
     }
     spec create_child_vasp_account {
-// TODO: Temporarily commented out until inv disable is fixed
-//      pragma disable_invariants_in_body;
+        pragma disable_invariants_in_body;
         include CreateChildVASPAccountAbortsIf<Token>;
         include CreateChildVASPAccountEnsures<Token>{
             parent_addr: Signer::spec_address_of(parent),
@@ -2131,8 +2130,7 @@ module DiemFramework::DiemAccount {
     }
 
     spec create_validator_account {
-// TODO: Temporarily commented out until inv disable is fixed
-//      pragma disable_invariants_in_body;
+        pragma disable_invariants_in_body;
         include CreateValidatorAccountAbortsIf;
         include CreateValidatorAccountEnsures;
         include MakeAccountEmits;
@@ -2174,8 +2172,7 @@ module DiemFramework::DiemAccount {
     }
 
     spec create_validator_operator_account {
-// TODO: Temporarily commented out until inv disable is fixed
-//      pragma disable_invariants_in_body;
+        pragma disable_invariants_in_body;
         include CreateValidatorOperatorAccountAbortsIf;
         include CreateValidatorOperatorAccountEnsures;
     }
@@ -2319,78 +2316,61 @@ module DiemFramework::DiemAccount {
     spec module {
 
         /// An address has a published account iff it has a published RoleId
-        // > TODO: Temporarily weakened due to inv disable problem
-        // invariant forall addr: address:  exists_at(addr) <==> exists<Roles::RoleId>(addr);
-        invariant forall addr: address:  exists_at(addr) ==> exists<Roles::RoleId>(addr);
+        invariant [suspendable] forall addr: address:  exists_at(addr) <==> exists<Roles::RoleId>(addr);
 
         // Every address with a published account has a publish event handle generator
-        // >TODO: Prover can't deal with this because it gets an error when a public functions
-        // such as Events::publish_generator, are called while invariants are disabled.
+        // >TODO: When commented in, odd things happen.
         // However, this particular invariant does not need to be disabled, and the function
         // needs to be public because it is a general-purpose function in stdlib.
         // Also, the invariant is not specified in Events, which also seems relevant.
         // invariant forall addr: address where exists_at(addr): exists<Event::EventHandleGenerator>(addr);
 
         /// There is a published AccountOperationsCapability iff there is an account and it's at Diem root address
-        // > TODO: Temporarily weakened due to inv disable problem
-        // invariant forall addr: address:
-        //    exists<AccountOperationsCapability>(addr) <==> (addr == @DiemRoot && exists_at(addr));
-        invariant forall addr: address:
-             (addr == @DiemRoot && exists_at(addr)) ==> exists<AccountOperationsCapability>(addr);
-
+        invariant [suspendable] forall addr: address:
+            exists<AccountOperationsCapability>(addr) <==> (addr == @DiemRoot && exists_at(addr));
 
         /// An account has a WriteSetManager iff if it is Diem root
-        // > TODO: Temporarily weakened due to inv disable problem
-        // invariant forall addr: address:
-        //    exists<DiemWriteSetManager>(addr) <==> (addr == @DiemRoot && exists_at(addr));
-        invariant forall addr: address:
-            addr != @DiemRoot ==> !exists<DiemWriteSetManager>(addr);
+        invariant [suspendable] forall addr: address:
+           exists<DiemWriteSetManager>(addr) <==> (addr == @DiemRoot && exists_at(addr));
 
         /// There is a VASPDomainManager at an address iff the address is a diem treasury compliance account
-        // > TODO: Temporarily weakened due to inv disable problem
-        // invariant forall addr: address:
-        //     exists<VASPDomain::VASPDomainManager>(addr) <==> Roles::spec_has_treasury_compliance_role_addr(addr);
-        invariant forall addr: address:
-            exists<VASPDomain::VASPDomainManager>(addr) ==> Roles::spec_has_treasury_compliance_role_addr(addr);
+        invariant [suspendable] forall addr: address:
+            exists<VASPDomain::VASPDomainManager>(addr) <==> Roles::spec_has_treasury_compliance_role_addr(addr);
 
         /// There is a VASPDomains at an address iff the address is a Diem treasury compliance account
-        // > TODO: Temporarily commented out due to inv disable problem
-        // Weakened form requires verifying in context of call site.
-        // invariant forall addr: address:
-        //     exists<VASPDomain::VASPDomains>(addr) <==> Roles::spec_has_treasury_compliance_role_addr(addr);
+        invariant [suspendable] forall addr: address:
+            exists<VASPDomain::VASPDomains>(addr) <==> Roles::spec_has_parent_VASP_role_addr(addr);
 
         /// Account has a balance only iff it is parent or child VASP or a designated dealer
         /// > Note: It would be better to make this generic over all existing and future coins, but that
         /// would require existential quantification over types, and I'm not sure if that works with monomorphization.
-        // > TODO: Temporarily weakened due to inv disable problem
-        // invariant forall addr: address:
-        //     (exists<Balance<XUS>>(addr) || exists<Balance<XDX>>(addr)) <==> Roles::spec_can_hold_balance_addr(addr);
+        // > TODO: This fails because type parameter add_currency_for_account<token> can
+        // have token type that is not XDX or XUS !!
+        //  invariant [suspendable] forall addr: address:
+        // (exists<Balance<XUS>>(addr) || exists<Balance<XDX>>(addr)) <==> Roles::spec_can_hold_balance_addr(addr);
         invariant forall addr: address:
             (exists<Balance<XUS>>(addr) || exists<Balance<XDX>>(addr)) ==> Roles::spec_can_hold_balance_addr(addr);
 
         ///  There is a `DesignatedDealer::Dealer` published at `addr` iff the `addr` has a
         /// `Roles::DesignatedDealer` role.
-        // > TODO: Temporarily weakened due to inv disable problem
-        // invariant forall addr: address: exists<DesignatedDealer::Dealer>(addr)
-        //     <==> Roles::spec_has_designated_dealer_role_addr(addr);
-        invariant forall addr: address: exists<DesignatedDealer::Dealer>(addr)
-            ==> Roles::spec_has_designated_dealer_role_addr(addr);
+        invariant [suspendable] forall addr: address: exists<DesignatedDealer::Dealer>(addr)
+            <==> Roles::spec_has_designated_dealer_role_addr(addr);
 
         /// There is a DualAttestation credential iff account has designated dealer or parent VASP role
-        // > TODO: Temporarily weakened due to inv disable problem
-        // invariant forall addr: address:
-        //     exists<DualAttestation::Credential>(addr)
-        //     <==> (Roles::spec_has_designated_dealer_role_addr(addr)
-        //           || Roles::spec_has_parent_VASP_role_addr(addr));
-        invariant forall addr: address:
+        invariant [suspendable] forall addr: address:
             exists<DualAttestation::Credential>(addr)
-            ==> (Roles::spec_has_designated_dealer_role_addr(addr)
+            <==> (Roles::spec_has_designated_dealer_role_addr(addr)
                   || Roles::spec_has_parent_VASP_role_addr(addr));
 
         /// An address has an account iff there is a published FreezingBit struct
-        // > TODO: Temporarily weakened due to inv disable problem
-        // invariant forall addr: address:
-        //     exists_at(addr) <==> exists<AccountFreezing::FreezingBit>(addr);
+        invariant [suspendable] forall addr: address:
+            exists_at(addr) <==> exists<AccountFreezing::FreezingBit>(addr);
+
+        // This invariant is redundant with the previous invariant, but weaker.
+        // But it holds throughout make_account, and is useful to prove that the
+        // "move_to" that publishes the account will never abort.
+        // TODO: This is too clever.  Should modify code to an assert or requires at
+        // beginning of make_account that account does not already exist.
         invariant forall addr: address:
             exists_at(addr) ==> exists<AccountFreezing::FreezingBit>(addr);
 
@@ -2401,41 +2381,24 @@ module DiemFramework::DiemAccount {
             exists_at(addr);
 
         /// Account has SlidingNonce only if it's Diem Root or Treasury Compliance
-        // > TODO: Temporarily commented out due to inv disable problem
-        // > The weakened rule fails in SlidingNonce::publish, because it depends on publish only
-        // being called from create_diem_root_account and create_treasury_compliance_account
-        // invariant forall addr: address: exists<SlidingNonce::SlidingNonce>(addr)
-        //     <==> (Roles::spec_has_diem_root_role_addr(addr) || Roles::spec_has_treasury_compliance_role_addr(addr));
+        invariant [suspendable] forall addr: address: exists<SlidingNonce::SlidingNonce>(addr)
+            <==> (Roles::spec_has_diem_root_role_addr(addr) || Roles::spec_has_treasury_compliance_role_addr(addr));
 
-        // > TODO: Temporarily weakened due to inv disable problem
         /// Address has a ValidatorConfig iff it is a Validator address
-        // invariant forall addr: address: ValidatorConfig::exists_config(addr)
-        //     <==> Roles::spec_has_validator_role_addr(addr);
-        invariant forall addr: address: ValidatorConfig::exists_config(addr)
-            ==> Roles::spec_has_validator_role_addr(addr);
+        invariant [suspendable] forall addr: address: ValidatorConfig::exists_config(addr)
+            <==> Roles::spec_has_validator_role_addr(addr);
 
-        // > TODO: Temporarily weakened due to inv disable problem
         /// Address has a ValidatorOperatorConfig iff it is a ValidatorOperator address
-        // invariant forall addr: address: ValidatorOperatorConfig::has_validator_operator_config(addr)
-        //     <==> Roles::spec_has_validator_operator_role_addr(addr);
-        invariant forall addr: address: ValidatorOperatorConfig::has_validator_operator_config(addr)
-            ==> Roles::spec_has_validator_operator_role_addr(addr);
+        invariant [suspendable] forall addr: address: ValidatorOperatorConfig::has_validator_operator_config(addr)
+            <==> Roles::spec_has_validator_operator_role_addr(addr);
 
         /// Address has a parent VASP credential iff it has a parent VASP role
-        // > TODO: Temporarily weakened due to inv disable problem
-        // invariant forall addr: address: VASP::is_parent(addr)
-        //     <==> Roles::spec_has_parent_VASP_role_addr(addr);
-        invariant forall addr: address: VASP::is_parent(addr)
-            ==> Roles::spec_has_parent_VASP_role_addr(addr);
-
+        invariant [suspendable] forall addr: address: VASP::is_parent(addr)
+            <==> Roles::spec_has_parent_VASP_role_addr(addr);
 
         /// Address has a child VASP credential iff it has a child VASP role
-        // > TODO: Temporarily weakened due to inv disable problem
-        // invariant forall addr: address: VASP::is_child(addr)
-        //     <==> Roles::spec_has_child_VASP_role_addr(addr);
-        invariant forall addr: address: VASP::is_child(addr)
-            ==> Roles::spec_has_child_VASP_role_addr(addr);
-
+        invariant [suspendable] forall addr: address: VASP::is_child(addr)
+            <==> Roles::spec_has_child_VASP_role_addr(addr);
     }
 
     /// # Helper Functions and Schemas

language/diem-framework/modules/Roles.move

@@ -55,7 +55,7 @@ module DiemFramework::Roles {
     // Role Granting
 
     /// Publishes diem root role. Granted only in genesis.
-    public fun grant_diem_root_role(
+    public(friend) fun grant_diem_root_role(
         dr_account: &signer,
     ) {
         DiemTimestamp::assert_genesis();
@@ -72,7 +72,7 @@ module DiemFramework::Roles {
     }
 
     /// Publishes treasury compliance role. Granted only in genesis.
-    public fun grant_treasury_compliance_role(
+    public(friend) fun grant_treasury_compliance_role(
         treasury_compliance_account: &signer,
         dr_account: &signer,
     ) acquires RoleId {
@@ -91,7 +91,7 @@ module DiemFramework::Roles {
 
     /// Publishes a DesignatedDealer `RoleId` under `new_account`.
     /// The `creating_account` must be treasury compliance.
-    public fun new_designated_dealer_role(
+    public(friend) fun new_designated_dealer_role(
         creating_account: &signer,
         new_account: &signer,
     ) acquires RoleId {
@@ -105,7 +105,7 @@ module DiemFramework::Roles {
 
     /// Publish a Validator `RoleId` under `new_account`.
     /// The `creating_account` must be diem root.
-    public fun new_validator_role(
+    public(friend) fun new_validator_role(
         creating_account: &signer,
         new_account: &signer
     ) acquires RoleId {
@@ -119,7 +119,7 @@ module DiemFramework::Roles {
 
     /// Publish a ValidatorOperator `RoleId` under `new_account`.
     /// The `creating_account` must be DiemRoot
-    public fun new_validator_operator_role(
+    public(friend) fun new_validator_operator_role(
         creating_account: &signer,
         new_account: &signer,
     ) acquires RoleId {
@@ -133,7 +133,7 @@ module DiemFramework::Roles {
 
     /// Publish a ParentVASP `RoleId` under `new_account`.
     /// The `creating_account` must be TreasuryCompliance
-    public fun new_parent_vasp_role(
+    public(friend) fun new_parent_vasp_role(
         creating_account: &signer,
         new_account: &signer,
     ) acquires RoleId {
@@ -147,7 +147,7 @@ module DiemFramework::Roles {
 
     /// Publish a ChildVASP `RoleId` under `new_account`.
     /// The `creating_account` must be a ParentVASP
-    public fun new_child_vasp_role(
+    public(friend) fun new_child_vasp_role(
         creating_account: &signer,
         new_account: &signer,
     ) acquires RoleId {

language/diem-framework/modules/doc/Diem.md

@@ -4114,14 +4114,8 @@ A <code><a href="Diem.md#0x1_Diem_Preburn">Preburn</a></code> resource can only
 
 
 A <code><a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a></code> resource can only be published holding a currency type.
-
-
-<pre><code><b>invariant</b> <b>forall</b> addr: address, coin_type: type
-    <b>where</b> <b>exists</b>&lt;<a href="Diem.md#0x1_Diem_PreburnQueue">PreburnQueue</a>&lt;coin_type&gt;&gt;(addr):
-    <a href="Diem.md#0x1_Diem_spec_is_currency">spec_is_currency</a>&lt;coin_type&gt;();
-</code></pre>
-
-
+>TODO: This assertion is causing a violation for unknown reasons, probably
+a prover bug.
 Preburn is not transferrable [[J4]][PERMISSION].