Delete useless spec

Signed-off-by: Wenjie Ma <[email protected]>
anvil-verifier · Aug 25, 2023 · 741cd2a · 741cd2a
1 parent b4c5bf2
commit 741cd2a
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 54 deletions.
diff --git a/src/controller_examples/rabbitmq_controller/proof/common.rs b/src/controller_examples/rabbitmq_controller/proof/common.rs
@@ -394,12 +394,4 @@ pub open spec fn sts_get_response_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> b
         )
 }
 
-pub open spec fn ok_sts_get_response_msg(key: ObjectRef) -> FnSpec(RMQMessage) -> bool {
-    |msg: RMQMessage|
-        msg.src.is_KubernetesAPI()
-        && msg.content.is_get_response()
-        && msg.content.get_get_response().res.is_Ok()
-        && msg.content.get_get_response().res.get_Ok_0().object_ref() == make_stateful_set_key(key)
-}
-
 }
diff --git a/src/controller_examples/rabbitmq_controller/proof/safety.rs b/src/controller_examples/rabbitmq_controller/proof/safety.rs
@@ -208,58 +208,33 @@ proof fn lemma_always_triggering_cr_has_no_larger_replicas_than_scheduled_cr_and
         lift_state(scheduled_cr_has_no_larger_replicas_than_current_cr(rabbitmq))
     );
     assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
-        s_leq_both_to_s_prime_leq_scheduled_cr(rabbitmq, s, s_prime);
-        s_leq_both_to_s_prime_leq_current_cr(rabbitmq, s, s_prime);
+        let key = rabbitmq.object_ref();
+        if s_prime.reconcile_state_contains(rabbitmq.object_ref()) && s_prime.resource_key_exists(rabbitmq.object_ref())
+        && s_prime.resource_obj_of(rabbitmq.object_ref()).metadata.uid.get_Some_0() == s_prime.triggering_cr_of(rabbitmq.object_ref()).metadata.uid.get_Some_0() {
+            let step = choose |step| RMQCluster::next_step(s, s_prime, step);
+            if step.is_KubernetesAPIStep() {
+                assert(s.reconcile_state_contains(key) && s.triggering_cr_of(key) == s_prime.triggering_cr_of(key));
+                if !s.resource_key_exists(key) {
+                    assert(s_prime.resource_obj_of(key).metadata.uid == Some(s.kubernetes_api_state.uid_counter));
+                    assert(s_prime.resource_obj_of(rabbitmq.object_ref()).metadata.uid.get_Some_0() != s_prime.triggering_cr_of(rabbitmq.object_ref()).metadata.uid.get_Some_0());
+                } else if s.resource_obj_of(key) != s_prime.resource_obj_of(key) {
+                    assert(RabbitmqClusterView::from_dynamic_object(s.resource_obj_of(key)).is_Ok());
+                    assert(RabbitmqClusterView::from_dynamic_object(s_prime.resource_obj_of(key)).is_Ok());
+                    assert(replicas_of_rabbitmq(s.resource_obj_of(key)) <= replicas_of_rabbitmq(s_prime.resource_obj_of(key)));
+                }
+            } else if step.is_ControllerStep() {
+                assert(s.resource_key_exists(key) && s.resource_obj_of(key) == s_prime.resource_obj_of(key));
+                if !s.reconcile_state_contains(key) || s.triggering_cr_of(key) != s_prime.triggering_cr_of(key) {
+                    assert(s_prime.triggering_cr_of(rabbitmq.object_ref()).spec.replicas == s.reconcile_scheduled_obj_of(rabbitmq.object_ref()).spec.replicas);
+                }
+            }
+        }
     }
     init_invariant(spec, RMQCluster::init(), next, inv);
     always_weaken(spec, inv, triggering_cr_has_no_larger_replicas_than_current_cr(rabbitmq));
     always_weaken(spec, inv, triggering_cr_has_no_larger_replicas_than_scheduled_cr(rabbitmq));
 }
 
-proof fn s_leq_both_to_s_prime_leq_scheduled_cr(rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster)
-    requires
-        RMQCluster::next()(s, s_prime),
-        triggering_cr_has_no_larger_replicas_than_current_cr(rabbitmq)(s),
-        triggering_cr_has_no_larger_replicas_than_scheduled_cr(rabbitmq)(s),
-        RMQCluster::each_object_in_etcd_is_well_formed()(s),
-    ensures
-        triggering_cr_has_no_larger_replicas_than_scheduled_cr(rabbitmq)(s_prime),
-{}
-
-proof fn s_leq_both_to_s_prime_leq_current_cr(rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster)
-    requires
-        RMQCluster::next()(s, s_prime),
-        scheduled_cr_has_no_larger_replicas_than_current_cr(rabbitmq)(s),
-        triggering_cr_has_no_larger_replicas_than_current_cr(rabbitmq)(s),
-        triggering_cr_has_no_larger_replicas_than_scheduled_cr(rabbitmq)(s),
-        RMQCluster::each_object_in_etcd_is_well_formed()(s),
-        RMQCluster::triggering_cr_has_lower_uid_than_uid_counter()(s),
-    ensures
-        triggering_cr_has_no_larger_replicas_than_current_cr(rabbitmq)(s_prime),
-{
-    let key = rabbitmq.object_ref();
-    if s_prime.reconcile_state_contains(rabbitmq.object_ref()) && s_prime.resource_key_exists(rabbitmq.object_ref())
-    && s_prime.resource_obj_of(rabbitmq.object_ref()).metadata.uid.get_Some_0() == s_prime.triggering_cr_of(rabbitmq.object_ref()).metadata.uid.get_Some_0() {
-        let step = choose |step| RMQCluster::next_step(s, s_prime, step);
-        if step.is_KubernetesAPIStep() {
-            assert(s.reconcile_state_contains(key) && s.triggering_cr_of(key) == s_prime.triggering_cr_of(key));
-            if !s.resource_key_exists(key) {
-                assert(s_prime.resource_obj_of(key).metadata.uid == Some(s.kubernetes_api_state.uid_counter));
-                assert(s_prime.resource_obj_of(rabbitmq.object_ref()).metadata.uid.get_Some_0() != s_prime.triggering_cr_of(rabbitmq.object_ref()).metadata.uid.get_Some_0());
-            } else if s.resource_obj_of(key) != s_prime.resource_obj_of(key) {
-                assert(RabbitmqClusterView::from_dynamic_object(s.resource_obj_of(key)).is_Ok());
-                assert(RabbitmqClusterView::from_dynamic_object(s_prime.resource_obj_of(key)).is_Ok());
-                assert(replicas_of_rabbitmq(s.resource_obj_of(key)) <= replicas_of_rabbitmq(s_prime.resource_obj_of(key)));
-            }
-        } else if step.is_ControllerStep() {
-            assert(s.resource_key_exists(key) && s.resource_obj_of(key) == s_prime.resource_obj_of(key));
-            if !s.reconcile_state_contains(key) || s.triggering_cr_of(key) != s_prime.triggering_cr_of(key) {
-                assert(s_prime.triggering_cr_of(rabbitmq.object_ref()).spec.replicas == s.reconcile_scheduled_obj_of(rabbitmq.object_ref()).spec.replicas);
-            }
-        }
-    }
-}
-
 spec fn response_at_after_get_stateful_set_step_is_sts_get_response(rabbitmq: RabbitmqClusterView) -> StatePred<RMQCluster> {
     let key = rabbitmq.object_ref();
     |s: RMQCluster| {