simplify predicate

Signed-off-by: Cody Rivera <[email protected]>
anvil-verifier · Jan 20, 2025 · 3dc70cd · 3dc70cd
1 parent 74feb60
commit 3dc70cd
Show file tree

Hide file tree

Showing 4 changed files with 31 additions and 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
@@ -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<ClusterState> {
     |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
@@ -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
@@ -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)