Merge pull request #1779 from verus-lang/fix-no-cheating

Allow external_body/assume_specification inside vstd

Author: zhengyao-lin

source/vir/src/ast_util.rs

@@ -59,6 +59,13 @@ impl PathX {
             _ => false,
         }
     }
+
+    pub fn is_vstd_path(&self) -> bool {
+        match &self.krate {
+            Some(k) if &**k == "vstd" => true,
+            _ => false,
+        }
+    }
 }
 
 pub fn path_segments_match_prefix(target: &Idents, prefix: &Idents) -> bool {

source/vir/src/well_formed.rs

@@ -1174,10 +1174,16 @@ fn check_function(
     }
 
     if ctxt.no_cheating && (function.x.attrs.is_external_body || function.x.proxy.is_some()) {
-        return Err(error(
-            &function.span,
-            "external_body/assume_specification not allowed with --no-cheating",
-        ));
+        match &function.x.owning_module {
+            // Allow external_body/assume_specification inside vstd
+            Some(path) if path.is_vstd_path() => {}
+            _ => {
+                return Err(error(
+                    &function.span,
+                    "external_body/assume_specification not allowed with --no-cheating",
+                ));
+            }
+        }
     }
 
     Ok(())