[move-prover] V2 invariant support

* New pragmas: disable_invariants_in_body and delegate_invariants_to_caller.

language/move-model/src/model.rs

@@ -59,7 +59,8 @@ use crate::{
         ConditionKind, Exp, GlobalInvariant, ModuleName, PropertyBag, PropertyValue, Spec,
         SpecBlockInfo, SpecFunDecl, SpecVarDecl, Value,
     },
-    pragmas::{FRIEND_PRAGMA, INTRINSIC_PRAGMA, OPAQUE_PRAGMA, VERIFY_PRAGMA},
+    pragmas::{FRIEND_PRAGMA, INTRINSIC_PRAGMA, OPAQUE_PRAGMA, VERIFY_PRAGMA,
+              DISABLE_INVARIANTS_IN_BODY_PRAGMA, DELEGATE_INVARIANTS_TO_CALLER_PRAGMA},
     symbol::{Symbol, SymbolPool},
     ty::{PrimitiveType, Type},
 };
@@ -2360,6 +2361,17 @@ impl<'env> FunctionEnv<'env> {
             }
     }
 
+    /// Returns true if invariants are declared disabled in body of function
+    pub fn are_invariants_disabled_in_body(&self) -> bool {
+        self.is_pragma_true(DISABLE_INVARIANTS_IN_BODY_PRAGMA, || false)
+    }
+
+    /// Returns true if invariants are declared disabled in body of function
+    pub fn are_invariants_disabled_at_call(&self) -> bool {
+        self.is_pragma_true(DELEGATE_INVARIANTS_TO_CALLER_PRAGMA, || false)
+    }
+
+
     /// Returns true if this function mutates any references (i.e. has &mut parameters).
     pub fn is_mutating(&self) -> bool {
         self.get_parameters()

language/move-model/src/pragmas.rs

@@ -55,6 +55,14 @@ pub const EXPORT_ENSURES_PRAGMA: &str = "export_ensures";
 /// of a boolean or a number.
 pub const FRIEND_PRAGMA: &str = "friend";
 
+/// Pragma indicating that invariants are not to be checked between entry and exit
+/// to this function
+pub const DISABLE_INVARIANTS_IN_BODY_PRAGMA: &str = "disable_invariants_in_body";
+
+/// Pragma indicating that invariants are not to be checked between entry and exit
+/// to this function
+pub const DELEGATE_INVARIANTS_TO_CALLER_PRAGMA: &str = "delegate_invariants_to_caller";
+
 /// Checks whether a pragma is valid in a specific spec block.
 pub fn is_pragma_valid_for_block(target: &SpecBlockContext<'_>, pragma: &str) -> bool {
     use crate::builder::module_builder::SpecBlockContext::*;
@@ -82,6 +90,8 @@ pub fn is_pragma_valid_for_block(target: &SpecBlockContext<'_>, pragma: &str) ->
                 | ASSUME_NO_ABORT_FROM_HERE_PRAGMA
                 | EXPORT_ENSURES_PRAGMA
                 | FRIEND_PRAGMA
+                | DISABLE_INVARIANTS_IN_BODY_PRAGMA
+                | DELEGATE_INVARIANTS_TO_CALLER_PRAGMA
         ),
         _ => false,
     }