anvil-verifier · marshtompsxd · May 15, 2025 · May 9, 2025 · May 10, 2025 · May 10, 2025
diff --git a/src/kubernetes_api_objects/error.rs b/src/kubernetes_api_objects/error.rs
@@ -17,6 +17,7 @@ pub enum APIError {
     InternalError,
     Timeout,
     ServerTimeout,
+    TransactionAbort,
     Other
 }
 
@@ -34,6 +35,7 @@ impl std::fmt::Debug for APIError {
             APIError::InternalError => write!(f, "InternalError"),
             APIError::Timeout => write!(f, "Timeout"),
             APIError::ServerTimeout => write!(f, "ServerTimeout"),
+            APIError::TransactionAbort => write!(f, "TransactionAbort"),
             APIError::Other => write!(f, "Other"),
         }
     }

diff --git a/src/kubernetes_api_objects/exec/api_method.rs b/src/kubernetes_api_objects/exec/api_method.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: MIT
 use crate::kubernetes_api_objects::error::*;
 use crate::kubernetes_api_objects::exec::{
-    api_resource::*, dynamic::*, preconditions::*, resource::*,
+    api_resource::*, dynamic::*, owner_reference::*, preconditions::*, resource::*,
 };
 use crate::kubernetes_api_objects::spec::{api_method::*, common::ObjectRef};
 use crate::vstd_ext::option_lib::*;
@@ -30,6 +30,8 @@ pub enum KubeAPIRequest {
     DeleteRequest(KubeDeleteRequest),
     UpdateRequest(KubeUpdateRequest),
     UpdateStatusRequest(KubeUpdateStatusRequest),
+    GetThenDeleteRequest(KubeGetThenDeleteRequest),
+    GetThenUpdateRequest(KubeGetThenUpdateRequest),
 }
 
 // KubeGetRequest has the name as the parameter of Api.get(), and namespace to instantiate an Api.
@@ -193,6 +195,69 @@ impl View for KubeUpdateStatusRequest {
     }
 }
 
+// KubeGetThenDeleteRequest has the name as the parameter of Api.get() and Api.delete(), and namespace to instantiate an Api.
+//
+// TODO: KubeGetThenDeleteRequest should carry a Box<dyn Fn(DynamicObject) -> bool> when Verus supports dyn
+
+pub struct KubeGetThenDeleteRequest {
+    pub api_resource: ApiResource,
+    pub name: String,
+    pub namespace: String,
+    pub owner_ref: OwnerReference,
+}
+
+impl KubeGetThenDeleteRequest {
+    #[verifier(external)]
+    pub fn key(&self) -> std::string::String {
+        format!("{}/{}/{}", self.api_resource.as_kube_ref().kind, self.namespace, self.name)
+    }
+}
+
+impl View for KubeGetThenDeleteRequest {
+    type V = GetThenDeleteRequest;
+    open spec fn view(&self) -> GetThenDeleteRequest {
+        GetThenDeleteRequest {
+            key: ObjectRef {
+                kind: self.api_resource@.kind,
+                name: self.name@,
+                namespace: self.namespace@,
+            },
+            owner_ref: self.owner_ref@,
+        }
+    }
+}
+
+// KubeGetThenUpdateRequest has the name as the parameter of Api.get() and the obj as the parameter of Api.replace().
+//
+// TODO: KubeGetThenUpdateRequest should carry a Box<dyn Fn(DynamicObject) -> Option<DynamicObject>> when Verus supports dyn
+
+pub struct KubeGetThenUpdateRequest {
+    pub api_resource: ApiResource,
+    pub name: String,
+    pub namespace: String,
+    pub owner_ref: OwnerReference,
+    pub obj: DynamicObject,
+}
+
+impl KubeGetThenUpdateRequest {
+    #[verifier(external)]
+    pub fn key(&self) -> std::string::String {
+        format!("{}/{}/{}", self.api_resource.as_kube_ref().kind, self.namespace, self.name)
+    }
+}
+
+impl View for KubeGetThenUpdateRequest {
+    type V = GetThenUpdateRequest;
+    open spec fn view(&self) -> GetThenUpdateRequest {
+        GetThenUpdateRequest {
+            name: self.name@,
+            namespace: self.namespace@,
+            owner_ref: self.owner_ref@,
+            obj: self.obj@,
+        }
+    }
+}
+
 impl View for KubeAPIRequest {
     type V = APIRequest;
 
@@ -204,6 +269,8 @@ impl View for KubeAPIRequest {
             KubeAPIRequest::DeleteRequest(delete_req) => APIRequest::DeleteRequest(delete_req@),
             KubeAPIRequest::UpdateRequest(update_req) => APIRequest::UpdateRequest(update_req@),
             KubeAPIRequest::UpdateStatusRequest(update_status_req) => APIRequest::UpdateStatusRequest(update_status_req@),
+            KubeAPIRequest::GetThenDeleteRequest(req) => APIRequest::GetThenDeleteRequest(req@),
+            KubeAPIRequest::GetThenUpdateRequest(req) => APIRequest::GetThenUpdateRequest(req@),
         }
     }
 }
@@ -228,6 +295,8 @@ pub enum KubeAPIResponse {
     DeleteResponse(KubeDeleteResponse),
     UpdateResponse(KubeUpdateResponse),
     UpdateStatusResponse(KubeUpdateStatusResponse),
+    GetThenDeleteResponse(KubeGetThenDeleteResponse),
+    GetThenUpdateResponse(KubeGetThenUpdateResponse),
 }
 
 // KubeGetResponse has the object returned by KubeGetRequest.
@@ -278,7 +347,7 @@ impl View for KubeCreateResponse {
     }
 }
 
-// DeleteResponse has (last version of) the object deleted by DeleteRequest.
+// KubeDeleteResponse does NOT have the object.
 
 pub struct KubeDeleteResponse {
     pub res: Result<(), APIError>,
@@ -326,6 +395,38 @@ impl View for KubeUpdateStatusResponse {
     }
 }
 
+// KubeGetThenUpdateResponse has the object updated by KubeGetThenUpdateRequest.
+
+pub struct KubeGetThenUpdateResponse {
+    pub res: Result<DynamicObject, APIError>,
+}
+
+impl View for KubeGetThenUpdateResponse {
+    type V = GetThenUpdateResponse;
+    open spec fn view(&self) -> GetThenUpdateResponse {
+        match self.res {
+            Ok(o) => GetThenUpdateResponse { res: Ok(o@) },
+            Err(e) => GetThenUpdateResponse { res: Err(e) },
+        }
+    }
+}
+
+// KubeGetThenDeleteResponse does NOT have the object.
+
+pub struct KubeGetThenDeleteResponse {
+    pub res: Result<(), APIError>,
+}
+
+impl View for KubeGetThenDeleteResponse {
+    type V = GetThenDeleteResponse;
+    open spec fn view(&self) -> GetThenDeleteResponse {
+        match self.res {
+            Ok(_) => GetThenDeleteResponse { res: Ok(()) },
+            Err(e) => GetThenDeleteResponse { res: Err(e) },
+        }
+    }
+}
+
 impl View for KubeAPIResponse {
     type V = APIResponse;
     open spec fn view(&self) -> APIResponse {
@@ -336,6 +437,8 @@ impl View for KubeAPIResponse {
             KubeAPIResponse::DeleteResponse(delete_resp) => APIResponse::DeleteResponse(delete_resp@),
             KubeAPIResponse::UpdateResponse(update_resp) => APIResponse::UpdateResponse(
F438
update_resp@),
             KubeAPIResponse::UpdateStatusResponse(update_status_resp) => APIResponse::UpdateStatusResponse(update_status_resp@),
+            KubeAPIResponse::GetThenDeleteResponse(resp) => APIResponse::GetThenDeleteResponse(resp@),
+            KubeAPIResponse::GetThenUpdateResponse(resp) => APIResponse::GetThenUpdateResponse(resp@),
         }
     }
 }

diff --git a/src/kubernetes_api_objects/exec/object_meta.rs b/src/kubernetes_api_objects/exec/object_meta.rs
@@ -113,21 +113,21 @@ impl ObjectMeta {
     }
 
     #[verifier(external_body)]
-    pub fn owner_references_contains(&self, owner_ref: OwnerReference) -> (res: bool)
+    pub fn owner_references_contains(&self, owner_ref: &OwnerReference) -> (res: bool)
         ensures res == self@.owner_references_contains(owner_ref@),
     {
         match &self.inner.owner_references {
-            Some(owner_refs) => owner_refs.contains(&owner_ref.into_kube()),
+            Some(owner_refs) => owner_refs.contains(owner_ref.as_kube_ref()),
             None => false,
         }
     }
 
     #[verifier(external_body)]
-    pub fn owner_references_only_contains(&self, owner_ref: OwnerReference) -> (res: bool)
+    pub fn owner_references_only_contains(&self, owner_ref: &OwnerReference) -> (res: bool)
         ensures res == self@.owner_references_only_contains(owner_ref@),
     {
         match &self.inner.owner_references {
-            Some(owner_refs) => owner_refs.len() == 1 && owner_refs.contains(&owner_ref.into_kube()),
+            Some(owner_refs) => owner_refs.len() == 1 && owner_refs.contains(owner_ref.as_kube_ref()),
             None => false,
         }
     }

diff --git a/src/kubernetes_api_objects/exec/owner_reference.rs b/src/kubernetes_api_objects/exec/owner_reference.rs
@@ -41,6 +41,16 @@ impl OwnerReference {
             None => None,
         }
     }
+
+    #[verifier(external)]
+    pub fn as_kube_ref(&self) -> &deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference {
+        &self.inner
+    }
+
+    #[verifier(external)]
+    pub fn as_kube_mut_ref(&mut self) -> &mut deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference {
+        &mut self.inner
+    }
 }
 
 }

diff --git a/src/kubernetes_api_objects/spec/api_method.rs b/src/kubernetes_api_objects/spec/api_method.rs
@@ -4,6 +4,7 @@ use crate::kubernetes_api_objects::error::APIError;
 use crate::kubernetes_api_objects::spec::{
     common::{Kind, ObjectRef},
     dynamic::*,
+    owner_reference::*,
     preconditions::*,
 };
 use crate::vstd_ext::string_view::*;
@@ -26,6 +27,8 @@ pub enum APIRequest {
     DeleteRequest(DeleteRequest),
     UpdateRequest(UpdateRequest),
     UpdateStatusRequest(UpdateStatusRequest),
+    GetThenDeleteRequest(GetThenDeleteRequest),
+    GetThenUpdateRequest(GetThenUpdateRequest),
 }
 
 // GetRequest gets an object with the key (kind, name and namespace).
@@ -113,6 +116,44 @@ impl UpdateStatusRequest {
     }
 }
 
+// GetThenDeleteRequest deletes the object with the key only when it's owned by owner_ref and avoids conflicts caused by
+// version race.
+//
+// TODO: GetThenUpdateRequest should carry a spec_fn(DynamicObjectView) -> bool
+
+pub struct GetThenDeleteRequest {
+    pub key: ObjectRef,
+    pub owner_ref: OwnerReferenceView,
+}
+
+impl GetThenDeleteRequest {
+    pub open spec fn key(self) -> ObjectRef {
+        self.key
+    }
+}
+
+// GetThenUpdateRequest replaces the existing obj with a new one only when it's owned by owner_ref and avoids
+// conflicts caused by version race.
+//
+// TODO: GetThenUpdateRequest should carry a spec_fn(DynamicObjectView) -> Option<DynamicObjectView>
+
+pub struct GetThenUpdateRequest {
+    pub namespace: StringView,
+    pub name: StringView,
+    pub owner_ref: OwnerReferenceView,
+    pub obj: DynamicObjectView,
+}
+
+impl GetThenUpdateRequest {
+    pub open spec fn key(self) -> ObjectRef {
+        ObjectRef {
+            kind: self.obj.kind,
+            namespace: self.namespace,
+            name: self.name,
+        }
+    }
+}
+
 // APIResponse represents API responses sent from the Kubernetes API for specifications.
 
 #[is_variant]
@@ -123,6 +164,8 @@ pub enum APIResponse {
     DeleteResponse(DeleteResponse),
     UpdateResponse(UpdateResponse),
     UpdateStatusResponse(UpdateStatusResponse),
+    GetThenDeleteResponse(GetThenDeleteResponse),
+    GetThenUpdateResponse(GetThenUpdateResponse),
 }
 
 // GetResponse has the object returned by GetRequest.
@@ -161,4 +204,16 @@ pub struct UpdateStatusResponse {
     pub res: Result<DynamicObjectView, APIError>,
 }
 
+// GetThenUpdateResponse has the object updated by GetThenUpdateRequest.
+
+pub struct GetThenUpdateResponse {
+    pub res: Result<DynamicObjectView, APIError>,
+}
+
+// GetThenDeleteResponse does NOT contain the object that gets deleted.
+
+pub struct GetThenDeleteResponse {
+    pub res: Result<(), APIError>,
+}
+
 }
diff --git a/src/v2/controllers/fluent_controller/fluentbit/exec/resource/daemon_set.rs b/src/v2/controllers/fluent_controller/fluentbit/exec/resource/daemon_set.rs
@@ -44,7 +44,7 @@ impl ResourceBuilder<FluentBit, FluentBitReconcileState, model_resource::DaemonS
         let ds = DaemonSet::unmarshal(obj);
         if ds.is_ok() {
             let found_ds = ds.unwrap();
-            if found_ds.metadata().owner_references_only_contains(fb.controller_owner_ref()) && found_ds.spec().is_some() {
+            if found_ds.metadata().owner_references_only_contains(&fb.controller_owner_ref()) && found_ds.spec().is_some() {
                 return Ok(update_daemon_set(fb, found_ds).marshal());
             }
         }

diff --git a/src/v2/controllers/rabbitmq_controller/exec/resource/stateful_set.rs b/src/v2/controllers/rabbitmq_controller/exec/resource/stateful_set.rs
@@ -52,7 +52,7 @@ impl ResourceBuilder<RabbitmqCluster, RabbitmqReconcileState, model_resource::St
         let sts = StatefulSet::unmarshal(obj);
         if sts.is_ok() {
             let found_sts = sts.unwrap();
-            if found_sts.metadata().owner_references_only_contains(rabbitmq.controller_owner_ref())
+            if found_sts.metadata().owner_references_only_contains(&rabbitmq.controller_owner_ref())
             && state.latest_config_map_rv_opt.is_some() && found_sts.spec().is_some() {
                 return Ok(update_stateful_set(rabbitmq, found_sts, state.latest_config_map_rv_opt.as_ref().unwrap()).marshal());
             }

diff --git a/src/v2/controllers/vdeployment_controller/exec/reconciler.rs b/src/v2/controllers/vdeployment_controller/exec/reconciler.rs
@@ -1,19 +1,17 @@
 #![allow(unused_imports)]
 
-use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::kubernetes_api_objects::exec::{
-    prelude::*,
-    pod_template_spec::PodTemplateSpec,
-    label_selector::LabelSelector,
+    label_selector::LabelSelector, pod_template_spec::PodTemplateSpec, prelude::*,
 };
+use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::reconciler::exec::{io::*, reconciler::*};
-use crate::vreplicaset_controller::trusted::{exec_types::*, spec_types::*};
 use crate::vdeployment_controller::model::reconciler as model_reconciler;
 use crate::vdeployment_controller::trusted::{exec_types::*, step::*};
+use crate::vreplicaset_controller::trusted::{exec_types::*, spec_types::*};
 use crate::vstd_ext::option_lib::*;
-use vstd::{prelude::*, seq_lib::*};
 use crate::vstd_ext::{seq_lib::*, string_map::*, string_view::*};
 use deps_hack::tracing::{error, info};
+use vstd::{prelude::*, seq_lib::*};
 
 verus! {
 
@@ -434,7 +432,7 @@ ensures
         forall |i: int| 0 <= i < filtered_vrs_list.len() ==> #[trigger] filtered_vrs_list[i]@.well_formed(),
     {
         let vrs = &vrs_list[idx];
-        if vrs.metadata().owner_references_contains(vd.controller_owner_ref()) 
+        if vrs.metadata().owner_references_contains(&vd.controller_owner_ref())
         && !vrs.metadata().has_deletion_timestamp()
         && vrs.well_formed() {
             filtered_vrs_list.push(vrs.clone());
@@ -642,4 +640,4 @@ ensures
     owner_references
 }
 
-} // verus!
+} // verus!
diff --git a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs b/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
@@ -387,7 +387,7 @@ fn filter_pods(pods: Vec<Pod>, v_replica_set: &VReplicaSet) -> (filtered_pods: V
         // TODO: check other conditions such as pod status
         // Check the following conditions:
         // (1) the pod's label should match the replica set's selector
-        if pod.metadata().owner_references_contains(v_replica_set.controller_owner_ref())
+        if pod.metadata().owner_references_contains(&v_replica_set.controller_owner_ref())
         && v_replica_set.spec().selector().matches(pod.metadata().labels().unwrap_or(StringMap::new()))
         // (2) the pod should not be terminating (its deletion timestamp is nil)
         && !pod.metadata().has_deletion_timestamp() {