Remove stable related fields; fix a broken proof

Signed-off-by: Xudong Sun <[email protected]>
anvil-verifier · Oct 5, 2024 · b0eba1b · b0eba1b
1 parent ac749c4
commit b0eba1b
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 10 deletions.
diff --git a/src/v2/kubernetes_cluster/proof/controller_runtime_safety.rs b/src/v2/kubernetes_cluster/proof/controller_runtime_safety.rs
@@ -2,14 +2,14 @@
 // SPDX-License-Identifier: MIT
 #![allow(unused_imports)]
 use crate::kubernetes_api_objects::spec::prelude::*;
-use crate::temporal_logic::{defs::*, rules::*};
 use crate::kubernetes_cluster::spec::{
     api_server::{state_machine::transition_by_etcd, types::*},
     cluster::*,
     controller::types::*,
     external::{state_machine::*, types::*},
     message::*,
 };
+use crate::temporal_logic::{defs::*, rules::*};
 use vstd::prelude::*;
 
 verus! {
@@ -91,11 +91,15 @@ pub proof fn lemma_always_triggering_cr_has_lower_uid_than_uid_counter(self, spe
 //   - If the response is processed by the controller, the controller will create a new pending request in flight which
 //   allows the invariant to still hold.
 
+pub open spec fn state_comes_with_a_pending_request(self, controller_id: int, state: spec_fn(ReconcileLocalState) -> bool) -> bool {
+    &&& forall |s| #[trigger] state(s) ==> s != (self.controller_models[controller_id].reconcile_model.init)()
+    &&& forall |cr, resp_o, pre_state| #[trigger] state((self.controller_models[controller_id].reconcile_model.transition)(cr, resp_o, pre_state).0) ==> (self.controller_models[controller_id].reconcile_model.transition)(cr, resp_o, pre_state).1.is_Some()
+}
+
 pub proof fn lemma_always_pending_req_in_flight_or_resp_in_flight_at_reconcile_state(self, spec: TempPred<ClusterState>, controller_id: int, key: ObjectRef, state: spec_fn(ReconcileLocalState) -> bool)
     requires
         self.controller_models.contains_key(controller_id),
-        forall |s| (#[trigger] state(s)) ==> s != (self.controller_models[controller_id].reconcile_model.init)(),
-        forall |cr, resp_o, pre_state| #[trigger] state((self.controller_models[controller_id].reconcile_model.transition)(cr, resp_o, pre_state).0) ==> (self.controller_models[controller_id].reconcile_model.transition)(cr, resp_o, pre_state).1.is_Some(),
+        self.state_comes_with_a_pending_request(controller_id, state),
         spec.entails(lift_state(self.init())),
         spec.entails(always(lift_action(self.next()))),
         spec.entails(always(lift_state(Self::pending_req_of_key_is_unique_with_unique_id(controller_id, key)))),

diff --git a/src/v2/kubernetes_cluster/spec/api_server/state_machine.rs b/src/v2/kubernetes_cluster/spec/api_server/state_machine.rs
@@ -298,8 +298,6 @@ pub open spec fn handle_create_request(installed_types: InstalledTypes, req: Cre
             // Creation succeeds.
             (APIServerState {
                 resources: s.resources.insert(created_obj.object_ref(), created_obj),
-                // The object just gets created so it is not stable yet: built-in controller might update it
-                stable_resources: s.stable_resources.remove(created_obj.object_ref()),
                 uid_counter: s.uid_counter + 1,
                 resource_version_counter: s.resource_version_counter + 1,
                 ..s
@@ -506,8 +504,6 @@ pub open spec fn handle_update_request(installed_types: InstalledTypes, req: Upd
                     // or has at least one finalizer.
                     (APIServerState {
                         resources: s.resources.insert(req.key(), updated_obj_with_new_rv),
-                        // The object just gets updated so it is not stable yet: built-in controller might update it
-                        stable_resources: s.stable_resources.remove(req.key()),
                         resource_version_counter: s.resource_version_counter + 1, // Advance the rv counter
                         ..s
                     }, UpdateResponse{res: Ok(updated_obj_with_new_rv)})
@@ -686,8 +682,7 @@ pub open spec fn handle_request(installed_types: InstalledTypes) -> APIServerAct
 pub open spec fn api_server(installed_types: InstalledTypes) -> APIServerStateMachine {
     StateMachine {
         init: |s: APIServerState| {
-            &&& s.resources == Map::<ObjectRef, DynamicObjectView>::empty()
-            &&& s.stable_resources == Set::<ObjectRef>::empty()
+            s.resources == Map::<ObjectRef, DynamicObjectView>::empty()
         },
         actions: set![handle_request(installed_types)],
         step_to_action: |step: APIServerStep| {

diff --git a/src/v2/kubernetes_cluster/spec/api_server/types.rs b/src/v2/kubernetes_cluster/spec/api_server/types.rs
@@ -15,7 +15,6 @@ pub struct APIServerState {
     pub resources: StoredState,
     pub uid_counter: Uid,
     pub resource_version_counter: ResourceVersion,
-    pub stable_resources: Set<ObjectRef>,
 }
 
 pub type InstalledTypes = Map<StringView, InstalledType>;