From 3dc70cd85c039e74292e964ee6fccfb6013fc42d Mon Sep 17 00:00:00 2001 From: Cody Rivera Date: Mon, 20 Jan 2025 12:14:43 -0600 Subject: [PATCH] simplify predicate Signed-off-by: Cody Rivera --- .../proof/helper_invariants/predicate.rs | 6 +-- .../proof/helper_invariants/proof.rs | 4 +- .../proof/liveness/api_actions.rs | 4 +- .../proof/liveness/resource_match.rs | 48 +++++++++---------- 4 files changed, 31 insertions(+), 31 deletions(-) diff --git a/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/predicate.rs b/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/predicate.rs index ad103209..f24b376a 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/predicate.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/predicate.rs @@ -3,7 +3,7 @@ #![allow(unused_imports)] use crate::kubernetes_api_objects::spec::prelude::*; use crate::kubernetes_cluster::spec::{ - api_server::state_machine::*, + api_server::{state_machine::*, types::InstalledTypes}, cluster::*, message::* }; @@ -110,7 +110,7 @@ pub open spec fn no_pending_create_or_delete_request_not_from_controller_on_pods } pub open spec fn every_create_matching_pod_request_implies_at_after_create_pod_step( - vrs: VReplicaSetView, cluster: Cluster, controller_id: int, + vrs: VReplicaSetView, installed_types: InstalledTypes, controller_id: int, ) -> StatePred { |s: ClusterState| { forall |msg: Message| #![trigger msg.dst.is_APIServer(), msg.content.is_APIRequest()] { @@ -133,7 +133,7 @@ pub open spec fn every_create_matching_pod_request_implies_at_after_create_pod_s ..req.obj.metadata }, spec: req.obj.spec, - status: marshalled_default_status(req.obj.kind, cluster.installed_types), // Overwrite the status with the default one + status: marshalled_default_status(req.obj.kind, installed_types), // Overwrite the status with the default one }; &&& s.in_flight().contains(msg) &&& msg.src.is_Controller() diff --git a/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/proof.rs b/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/proof.rs index 9ee893d0..0ec39c4d 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/proof.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/helper_invariants/proof.rs @@ -491,7 +491,7 @@ pub proof fn lemma_eventually_always_every_create_matching_pod_request_implies_a spec.entails(always(lift_state(Cluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata(controller_id)))), forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id) ==> spec.entails(always(lift_state(#[trigger] vrs_not_interfered_by(other_id)))), - ensures spec.entails(true_pred().leads_to(always(lift_state(every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id))))), + ensures spec.entails(true_pred().leads_to(always(lift_state(every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id))))), { let key = vrs.object_ref(); let requirements = |msg: Message, s: ClusterState| { @@ -670,7 +670,7 @@ pub proof fn lemma_eventually_always_every_create_matching_pod_request_implies_a cluster.lemma_true_leads_to_always_every_in_flight_req_msg_satisfies(spec, requirements); temp_pred_equality( - lift_state(every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)), + lift_state(every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)), lift_state(Cluster::every_in_flight_req_msg_satisfies(requirements)) ); } diff --git a/src/v2/controllers/vreplicaset_controller/proof/liveness/api_actions.rs b/src/v2/controllers/vreplicaset_controller/proof/liveness/api_actions.rs index aa14de08..54991ca1 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/liveness/api_actions.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/liveness/api_actions.rs @@ -33,7 +33,7 @@ pub proof fn lemma_api_request_outside_create_or_delete_loop_maintains_matching_ helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)(s), helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s), helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s), - helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)(s), + helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)(s), helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)(s), forall |diff: nat| !(#[trigger] at_vrs_step_with_vrs(vrs, controller_id, VReplicaSetRecStepView::AfterCreatePod(diff))(s)), forall |diff: nat| !(#[trigger] at_vrs_step_with_vrs(vrs, controller_id, VReplicaSetRecStepView::AfterDeletePod(diff))(s)), @@ -102,7 +102,7 @@ pub proof fn lemma_api_request_not_made_by_vrs_maintains_matching_pods( helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)(s), helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s), helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s), - helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)(s), + helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)(s), helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)(s), forall |other_id| cluster.controller_models.remove(controller_id).contains_key(other_id) ==> #[trigger] vrs_not_interfered_by(other_id)(s) diff --git a/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs b/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs index 42d7bd7e..d6c8748b 100644 --- a/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs +++ b/src/v2/controllers/vreplicaset_controller/proof/liveness/resource_match.rs @@ -48,7 +48,7 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req( spec.entails(always(lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), spec.entails(always(lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)))), - spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)))), + spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)))), spec.entails(always(lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)))), ensures spec.entails( @@ -94,7 +94,7 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req( &&& helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)(s) &&& helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s) &&& helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s) - &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)(s) + &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)(s) &&& helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)(s) }; helper_lemmas::vrs_non_interference_property_equivalent_to_lifted_vrs_non_interference_property( @@ -119,7 +119,7 @@ pub proof fn lemma_from_init_step_to_send_list_pods_req( lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)), lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()), lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)), - lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)), + lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)), lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)) ); @@ -175,7 +175,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( spec.entails(always(lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), spec.entails(always(lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)))), - spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)))), + spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)))), spec.entails(always(lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)))) ensures spec.entails( @@ -222,7 +222,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( &&& helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)(s) &&& helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s) &&& helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s) - &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)(s) + &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)(s) &&& helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)(s) }; helper_lemmas::vrs_non_interference_property_equivalent_to_lifted_vrs_non_interference_property( @@ -248,7 +248,7 @@ pub proof fn lemma_from_after_send_list_pods_req_to_receive_list_pods_resp( lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)), lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()), lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)), - lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)), + lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)), lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)) ); @@ -493,7 +493,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_req( spec.entails(always(lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), spec.entails(always(lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)))), - spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)))), + spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)))), spec.entails(always(lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)))), diff < 0, ensures @@ -543,7 +543,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_req( &&& helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)(s) &&& helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s) &&& helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s) - &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)(s) + &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)(s) &&& helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)(s) }; helper_lemmas::vrs_non_interference_property_equivalent_to_lifted_vrs_non_interference_property( @@ -571,7 +571,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_create_pod_req( lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)), lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()), lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)), - lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)), + lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)), lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)) ); @@ -633,7 +633,7 @@ pub proof fn lemma_from_after_send_create_pod_req_to_receive_ok_resp( spec.entails(always(lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()))), spec.entails(always(lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), - spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)))), + spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)))), spec.entails(always(lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)))), spec.entails(always(lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)))), @@ -683,7 +683,7 @@ pub proof fn lemma_from_after_send_create_pod_req_to_receive_ok_resp( &&& helper_invariants::no_pending_update_or_update_status_request_on_pods()(s) &&& helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)(s) &&& helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s) - &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)(s) + &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)(s) &&& helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)(s) &&& helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s) }; @@ -710,7 +710,7 @@ pub proof fn lemma_from_after_send_create_pod_req_to_receive_ok_resp( lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()), lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)), lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()), - lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)), + lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)), lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)), lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)) ); @@ -854,7 +854,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_create_pod_req( spec.entails(always(lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), spec.entails(always(lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)))), - spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)))), + spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)))), spec.entails(always(lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)))), diff < 0, @@ -906,7 +906,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_create_pod_req( &&& helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)(s) &&& helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s) &&& helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s) - &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)(s) + &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)(s) &&& helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)(s) }; helper_lemmas::vrs_non_interference_property_equivalent_to_lifted_vrs_non_interference_property( @@ -934,7 +934,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_create_pod_req( lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)), lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()), lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)), - lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)), + lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)), lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)) ); @@ -999,7 +999,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_delete_pod_req( spec.entails(always(lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), spec.entails(always(lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)))), - spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)))), + spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)))), spec.entails(always(lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)))), diff > 0, ensures @@ -1049,7 +1049,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_delete_pod_req( &&& helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)(s) &&& helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s) &&& helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s) - &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)(s) + &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)(s) &&& helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)(s) }; helper_lemmas::vrs_non_interference_property_equivalent_to_lifted_vrs_non_interference_property( @@ -1077,7 +1077,7 @@ pub proof fn lemma_from_after_receive_list_pods_resp_to_send_delete_pod_req( lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)), lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()), lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)), - lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)), + lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)), lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)) ); @@ -1151,7 +1151,7 @@ pub proof fn lemma_from_after_send_delete_pod_req_to_receive_ok_resp( spec.entails(always(lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), spec.entails(always(lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)))), - spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)))), + spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)))), spec.entails(always(lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)))), diff > 0, @@ -1200,7 +1200,7 @@ pub proof fn lemma_from_after_send_delete_pod_req_to_receive_ok_resp( &&& helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)(s) &&& helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s) &&& helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s) - &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)(s) + &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)(s) &&& helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)(s) }; helper_lemmas::vrs_non_interference_property_equivalent_to_lifted_vrs_non_interference_property( @@ -1226,7 +1226,7 @@ pub proof fn lemma_from_after_send_delete_pod_req_to_receive_ok_resp( lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)), lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()), lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)), - lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)), + lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)), lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)) ); @@ -1318,7 +1318,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_delete_pod_req( spec.entails(always(lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)))), spec.entails(always(lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()))), spec.entails(always(lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)))), - spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)))), + spec.entails(always(lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)))), spec.entails(always(lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)))), spec.entails(always(lift_state(helper_invariants::at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_entries(vrs, controller_id)))), @@ -1372,7 +1372,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_delete_pod_req( &&& helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)(s) &&& helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()(s) &&& helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)(s) - &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)(s) + &&& helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)(s) &&& helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)(s) &&& helper_invariants::at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_entries(vrs, controller_id)(s) }; @@ -1401,7 +1401,7 @@ pub proof fn lemma_from_after_receive_ok_resp_to_send_delete_pod_req( lift_state(helper_invariants::no_pending_update_or_update_status_request_on_pods()), lift_state(helper_invariants::garbage_collector_does_not_delete_vrs_pods(vrs)), lift_state(helper_invariants::no_pending_create_or_delete_request_not_from_controller_on_pods()), - lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster, controller_id)), + lift_state(helper_invariants::every_create_matching_pod_request_implies_at_after_create_pod_step(vrs, cluster.installed_types, controller_id)), lift_state(helper_invariants::every_delete_matching_pod_request_implies_at_after_delete_pod_step(vrs, controller_id)), lift_state(helper_invariants::every_delete_request_from_vrs_has_rv_precondition_that_is_less_than_rv_counter(vrs, controller_id)), lift_state(helper_invariants::at_after_delete_pod_step_implies_filtered_pods_in_matching_pod_entries(vrs, controller_id))