Implement handler for deletion

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

src/executable_model/api_server.rs

@@ -147,15 +147,15 @@ fn object_transition_validity_check(obj: &DynamicObject, old_obj: &DynamicObject
 pub fn handle_get_request(req: &KubeGetRequest, s: &ApiServerState) -> (ret: KubeGetResponse)
     ensures ret@ == model::handle_get_request(req@, s@)
 {
-    let object_ref = KubeObjectRef {
+    let req_key = KubeObjectRef {
         kind: req.api_resource.kind(),
         name: req.name.clone(),
         namespace: req.namespace.clone(),
     };
-    if !s.resources.contains_key(&object_ref) {
+    if !s.resources.contains_key(&req_key) {
         KubeGetResponse{res: Err(APIError::ObjectNotFound)}
     } else {
-        KubeGetResponse{res: Ok(s.resources.get(&object_ref).unwrap())}
+        KubeGetResponse{res: Ok(s.resources.get(&req_key).unwrap())}
     }
 }
 
@@ -223,6 +223,38 @@ pub fn handle_create_request(req: &KubeCreateRequest, s: &mut ApiServerState) ->
     }
 }
 
+pub fn handle_delete_request(req: &KubeDeleteRequest, s: &mut ApiServerState) -> (ret: KubeDeleteResponse)
+    requires old(s).resource_version_counter < i64::MAX // No integer overflow
+    ensures (s@, ret@) == model::handle_delete_request(req@, old(s)@)
+{
+    let req_key = KubeObjectRef {
+        kind: req.api_resource.kind(),
+        name: req.name.clone(),
+        namespace: req.namespace.clone(),
+    };
+    if !s.resources.contains_key(&req_key) {
+        KubeDeleteResponse{res: Err(APIError::ObjectNotFound)}
+    } else {
+        let mut obj = s.resources.get(&req_key).unwrap();
+        if obj.metadata().finalizers().is_some() && obj.metadata().finalizers().unwrap().len() > 0 {
+            if obj.metadata().has_deletion_timestamp() {
+                KubeDeleteResponse{res: Ok(())}
+            } else {
+                obj.set_current_deletion_timestamp();
+                obj.set_resource_version(s.resource_version_counter);
+                let stamped_obj_with_new_rv = obj; // This renaming is just to stay consistent with the model
+                s.resources.insert(req_key, stamped_obj_with_new_rv);
+                s.resource_version_counter = s.resource_version_counter + 1;
+                KubeDeleteResponse{res: Ok(())}
+            }
+        } else {
+            s.resources.remove(&req_key);
+            s.resource_version_counter = s.resource_version_counter + 1;
+            KubeDeleteResponse{res: Ok(())}
+        }
+    }
+}
+
 fn allow_unconditional_update(kind: &Kind) -> (ret: bool)
     ensures ret == model::allow_unconditional_update(*kind)
 {

src/executable_model/common.rs

@@ -256,6 +256,18 @@ impl DynamicObject {
         self.as_kube_mut_ref().metadata.deletion_timestamp = other.as_kube_ref().metadata.deletion_timestamp.clone();
     }
 
+
+    // This function sets the deletion timestamp to the current time.
+    // This seems a bit inconsistent with the model's behavior which
+    // always sets it to the return value of deletion_timestamp().
+    // However, this function is actually closer to Kubernetes' real behavior.
+    #[verifier(external_body)]
+    pub fn set_current_deletion_timestamp(&mut self)
+        ensures self@ == old(self)@.set_deletion_timestamp(model::deletion_timestamp()),
+    {
+        self.as_kube_mut_ref().metadata.deletion_timestamp = Some(deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::Time(deps_hack::chrono::Utc::now()));
+    }
+
     #[verifier(external_body)]
     pub fn eq(&self, other: &DynamicObject) -> (ret: bool)
         ensures ret == (self@ == other@)

src/kubernetes_api_objects/exec/api_method.rs

@@ -62,8 +62,6 @@ impl View for KubeGetRequest {
 }
 
 /// KubeListRequest has the namespace to instantiate an Api.
-///
-/// Note that the kind is indicated by the upper layer Kube{ObjectKind}Request.
 
 pub struct KubeListRequest {
     pub api_resource: ApiResource,

src/kubernetes_cluster/spec/api_server/state_machine.rs

@@ -228,6 +228,14 @@ pub open spec fn handle_create_request<K: CustomResourceView>(req: CreateRequest
     }
 }
 
+// Here we make a compromise when modeling the behavior of setting
+// deletion timestamp to each object that is deemed to be deleted.
+// The real Kubernetes' behavior uses the current timestamp as the
+// deletion timestamp, but we only use an opaque string here.
+// This is fine because the request handling logic we want to model
+// only cares whether the object has a deletion timestamp or not.
+// By using this closed deletion_timestamp() function, we make the
+// modeling and proof much easier compared to modelling the real clock.
 pub closed spec fn deletion_timestamp() -> StringView;
 
 pub open spec fn handle_delete_request(req: DeleteRequest, s: ApiServerState) -> (ApiServerState, DeleteResponse) {
@@ -240,11 +248,12 @@ pub open spec fn handle_delete_request(req: DeleteRequest, s: ApiServerState) ->
         if obj.metadata.finalizers.is_Some() && obj.metadata.finalizers.get_Some_0().len() > 0 {
             // With the finalizer(s) in the object, we cannot immediately delete it from the key-value store.
             // Instead, we set the deletion timestamp of this object.
-            let stamped_obj = obj.set_deletion_timestamp(deletion_timestamp());
-            if stamped_obj == obj {
+            // If the object already has a deletion timestamp, then skip.
+            if obj.metadata.deletion_timestamp.is_Some() {
                 (s, DeleteResponse{res: Ok(())})
             } else {
-                let stamped_obj_with_new_rv = stamped_obj.set_resource_version(s.resource_version_counter);
+                let stamped_obj_with_new_rv = obj.set_deletion_timestamp(deletion_timestamp())
+                                                    .set_resource_version(s.resource_version_counter);
                 (ApiServerState {
                     // Here we use req.key, instead of stamped_obj.object_ref(), to insert to the map.
                     // This is intended because using stamped_obj.object_ref() will require us to use