Move unit tests out of verus! { ... } (#491)

Signed-off-by: Xudong Sun <[email protected]>

Cargo.toml

@@ -10,6 +10,3 @@ vstd = { path = "../verus/source/vstd" }
 deps_hack = { path = "src/deps_hack" }
 tungstenite = "0.20.1"
 rand = "0.8"
-
-[dev-dependencies]
-proptest = "1.4.0"

src/conformance_tests/api_server.rs

@@ -8,8 +8,8 @@ use deps_hack::kube::{
     api::{Api, DeleteParams, ListParams, ObjectMeta, PostParams},
     Client,
 };
+use deps_hack::proptest::prelude::*;
 use deps_hack::tokio::runtime::Runtime;
-use proptest::prelude::*;
 use rand::Rng;
 use std::process::Command;
 use vstd::prelude::*;
@@ -98,12 +98,14 @@ fn create_new_testing_namespace(len: usize) -> Option<std::string::String> {
             ..Default::default()
         };
 
-        namespace_api.create(&PostParams::default(), &namespace_obj).await
+        namespace_api
+            .create(&PostParams::default(), &namespace_obj)
+            .await
     });
 
     match resp {
         Ok(_) => Some(namespace_name),
-        Err(_) => None
+        Err(_) => None,
     }
 }
 

src/deps_hack/Cargo.toml

@@ -33,3 +33,4 @@ base64 = "0.13.0"
 rand = "0.8"
 zookeeper = "0.8"
 chrono = "0.4.19"
+proptest = "1.4.0"

src/deps_hack/src/lib.rs

@@ -7,6 +7,7 @@ pub use kube;
 pub use kube_client;
 pub use kube_core;
 pub use kube_derive;
+pub use proptest;
 pub use rand;
 pub use schemars;
 pub use serde;

src/unit_tests/kubernetes_api_objects/affinity.rs

@@ -9,10 +9,7 @@ use deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::Time;
 use vstd::prelude::*;
 use vstd::string::*;
 
-verus! {
-// Tests for affinity
 #[test]
-#[verifier(external)]
 pub fn test_kube() {
     let kube_affinity = deps_hack::k8s_openapi::api::core::v1::Affinity {
         node_affinity: Some(deps_hack::k8s_openapi::api::core::v1::NodeAffinity {
@@ -30,4 +27,3 @@ pub fn test_kube() {
 
     assert_eq!(affinity.into_kube(), kube_affinity);
 }
-}