Make it more stable

Signed-off-by: Wenjie Ma <[email protected]>
anvil-verifier · Aug 26, 2023 · 922ae12 · 922ae12
1 parent 3cac4d3
commit 922ae12
Show file tree

Hide file tree

Showing 19 changed files with 136 additions and 115 deletions.
diff --git a/src/controller_examples/fluent_controller/spec/fluentbit.rs b/src/controller_examples/fluent_controller/spec/fluentbit.rs
@@ -83,8 +83,6 @@ impl ResourceView for FluentBitView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: FluentBitSpecView) -> Value;

diff --git a/src/controller_examples/rabbitmq_controller/proof/safety/safety.rs b/src/controller_examples/rabbitmq_controller/proof/safety/safety.rs
@@ -397,14 +397,6 @@ proof fn lemma_always_replicas_of_stateful_set_create_or_update_request_msg_sati
         spec.entails(always(lift_state(replicas_of_stateful_set_create_or_update_request_msg_satisfies_order(rabbitmq)))),
 {
     let inv = replicas_of_stateful_set_create_or_update_request_msg_satisfies_order(rabbitmq);
-    let create_order = |msg: RMQMessage, s: RMQCluster| {
-        sts_create_request_msg(rabbitmq.object_ref())(msg)
-        ==> replicas_satisfies_order(msg.content.get_create_request().obj, rabbitmq)(s)
-    };
-    let update_order = |msg: RMQMessage, s: RMQCluster| {
-        sts_update_request_msg(rabbitmq.object_ref())(msg)
-        ==> replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s)
-    };
     let next = |s, s_prime| {
         &&& RMQCluster::next()(s, s_prime)
         &&& RMQCluster::each_object_in_etcd_is_well_formed()(s)
@@ -428,79 +420,138 @@ proof fn lemma_always_replicas_of_stateful_set_create_or_update_request_msg_sati
         lift_state(object_in_every_create_or_update_request_msg_only_has_valid_owner_references())
     );
     assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
-        assert forall |msg| #[trigger] s_prime.message_in_flight(msg) implies create_order(msg, s_prime) && update_order(msg, s_prime) by {
-            let step = choose |step| RMQCluster::next_step(s, s_prime, step);
-            let key = rabbitmq.object_ref();
-            let sts_key = make_stateful_set_key(key);
-            match step {
-                Step::KubernetesAPIStep(input) => {
-                    assert(s.controller_state == s_prime.controller_state);
-                    if sts_create_request_msg(key)(msg) || sts_update_request_msg(key)(msg) {
-                        assert(s.message_in_flight(msg));
-                    }
-                    if s_prime.resource_key_exists(key) {
-                        if s.resource_key_exists(key) {
-                            assert(replicas_of_rabbitmq(s.resource_obj_of(key)) <= replicas_of_rabbitmq(s_prime.resource_obj_of(key)));
-                        } else {
-                            assert(s_prime.resource_obj_of(key).metadata.uid.is_Some());
-                            assert(s_prime.resource_obj_of(key).metadata.uid.get_Some_0() == s.kubernetes_api_state.uid_counter);
-                            if sts_create_request_msg(key)(msg) {
-                                assert(s.message_in_flight(msg));
-                                let owner_refs = msg.content.get_create_request().obj.metadata.owner_references;
-                                if owner_refs.is_Some() && owner_refs.get_Some_0().len() == 1 {
-                                    assert(owner_refs.get_Some_0()[0].uid != s.kubernetes_api_state.uid_counter);
-                                    assert(owner_refs.get_Some_0()[0] != RabbitmqClusterView::from_dynamic_object(s_prime.resource_obj_of(key)).get_Ok_0().controller_owner_ref());
-                                }
-                            } else if sts_update_request_msg(key)(msg) {
-                                assert(s.message_in_flight(msg));
-                                let owner_refs = msg.content.get_update_request().obj.metadata.owner_references;
-                                if owner_refs.is_Some() && owner_refs.get_Some_0().len() == 1 {
-                                    assert(owner_refs.get_Some_0()[0].uid < s.kubernetes_api_state.uid_counter);
-                                    assert(owner_refs.get_Some_0()[0] != RabbitmqClusterView::from_dynamic_object(s_prime.resource_obj_of(key)).get_Ok_0().controller_owner_ref());
-                                }
-                            }
-                        }
-                    }
-                    assert(create_order(msg, s_prime) && update_order(msg, s_prime));
-                },
-                Step::ControllerStep(input) => {
-                    if !s.message_in_flight(msg) {
-                        StatefulSetView::spec_integrity_is_preserved_by_marshal();
-                        if sts_create_request_msg(key)(msg) {
-                            lemma_stateful_set_create_request_msg_implies_key_in_reconcile_equals(key, s, s_prime, msg, step);
-                            assert(StatefulSetView::from_dynamic_object(msg.content.get_create_request().obj).get_Ok_0().spec.get_Some_0().replicas.get_Some_0() <= s.triggering_cr_of(key).spec.replicas);
-                        } else if sts_update_request_msg(key)(msg) {
-                            lemma_stateful_set_update_request_msg_implies_key_in_reconcile_equals(key, s, s_prime, msg, step);
-                            assert(StatefulSetView::from_dynamic_object(msg.content.get_update_request().obj).get_Ok_0().spec.get_Some_0().replicas.get_Some_0() <= s.triggering_cr_of(key).spec.replicas);
-                        }
+        assert forall |msg| #[trigger] s_prime.message_in_flight(msg) implies (sts_create_request_msg(rabbitmq.object_ref())(msg)
+        ==> replicas_satisfies_order(msg.content.get_create_request().obj, rabbitmq)(s_prime)) && (sts_update_request_msg(rabbitmq.object_ref())(msg)
+        ==> replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s_prime)) by {
+            if sts_create_request_msg(rabbitmq.object_ref())(msg) {
+                replicas_of_stateful_set_create_request_msg_satisfies_order_induction(rabbitmq, s, s_prime, msg);
+            }
+            if sts_update_request_msg(rabbitmq.object_ref())(msg) {
+                replicas_of_stateful_set_update_request_msg_satisfies_order_induction(rabbitmq, s, s_prime, msg);
+            }
+        }
+    }
+    init_invariant(spec, RMQCluster::init(), next, inv);
+}
+
+proof fn replicas_of_stateful_set_create_request_msg_satisfies_order_induction(
+    rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster, msg: RMQMessage
+)
+    requires
+        RMQCluster::next()(s, s_prime),
+        RMQCluster::each_object_in_etcd_is_well_formed()(s),
+        RMQCluster::each_object_in_etcd_is_well_formed()(s_prime),
+        RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s),
+        RMQCluster::etcd_and_scheduled_and_triggering_cr_in_correct_order(rabbitmq)(s),
+        object_in_every_create_or_update_request_msg_only_has_valid_owner_references()(s),
+        replicas_of_stateful_set_create_or_update_request_msg_satisfies_order(rabbitmq)(s),
+        s_prime.message_in_flight(msg),
+        sts_create_request_msg(rabbitmq.object_ref())(msg),
+    ensures
+        replicas_satisfies_order(msg.content.get_create_request().obj, rabbitmq)(s_prime),
+{
+    let step = choose |step| RMQCluster::next_step(s, s_prime, step);
+    let key = rabbitmq.object_ref();
+    let sts_key = make_stateful_set_key(key);
+    match step {
+        Step::KubernetesAPIStep(input) => {
+            assert(s.controller_state == s_prime.controller_state);
+            assert(s.message_in_flight(msg));
+            if s_prime.resource_key_exists(key) {
+                if s.resource_key_exists(key) {
+                    assert(replicas_of_rabbitmq(s.resource_obj_of(key)) <= replicas_of_rabbitmq(s_prime.resource_obj_of(key)));
+                } else {
+                    assert(s_prime.resource_obj_of(key).metadata.uid.is_Some());
+                    assert(s_prime.resource_obj_of(key).metadata.uid.get_Some_0() == s.kubernetes_api_state.uid_counter);
+                    let owner_refs = msg.content.get_create_request().obj.metadata.owner_references;
+                    if owner_refs.is_Some() && owner_refs.get_Some_0().len() == 1 {
+                        assert(owner_refs.get_Some_0()[0].uid != s.kubernetes_api_state.uid_counter);
+                        assert(owner_refs.get_Some_0()[0] != RabbitmqClusterView::from_dynamic_object(s_prime.resource_obj_of(key)).get_Ok_0().controller_owner_ref());
                     }
-                    assert(create_order(msg, s_prime) && update_order(msg, s_prime));
-                },
-                Step::ScheduleControllerReconcileStep(input) => {
-                    assert(s.message_in_flight(msg));
-                    assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
-                    if input == key {} else {}
-                    assert(create_order(msg, s_prime) && update_order(msg, s_prime));
-                },
-                Step::RestartController() => {
-                    assert(s.message_in_flight(msg));
-                    assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
-                    assert(!s_prime.reconcile_state_contains(key));
-                    assert(!s_prime.reconcile_scheduled_for(key));
-                    assert(create_order(msg, s_prime) && update_order(msg, s_prime));
-                },
-                _ => {
-                    if sts_create_request_msg(key)(msg) || sts_update_request_msg(key)(msg) {
-                        assert(s.message_in_flight(msg));
-                        assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
-                        assert(s.controller_state == s_prime.controller_state);
+                }
+            }
+        },
+        Step::ControllerStep(input) => {
+            if !s.message_in_flight(msg) {
+                StatefulSetView::spec_integrity_is_preserved_by_marshal();
+                lemma_stateful_set_create_request_msg_implies_key_in_reconcile_equals(key, s, s_prime, msg, step);
+                assert(StatefulSetView::from_dynamic_object(msg.content.get_create_request().obj).get_Ok_0().spec.get_Some_0().replicas.get_Some_0() <= s.triggering_cr_of(key).spec.replicas);
+            }
+        },
+        Step::ScheduleControllerReconcileStep(input) => {
+            assert(s.message_in_flight(msg));
+            assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
+        },
+        Step::RestartController() => {
+            assert(s.message_in_flight(msg));
+            assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
+        },
+        _ => {
+            assert(s.message_in_flight(msg));
+            assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
+            assert(s.controller_state == s_prime.controller_state);
+        }
+    }
+}
+
+proof fn replicas_of_stateful_set_update_request_msg_satisfies_order_induction(
+    rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster, msg: RMQMessage
+)
+    requires
+        RMQCluster::next()(s, s_prime),
+        RMQCluster::each_object_in_etcd_is_well_formed()(s),
+        RMQCluster::each_object_in_etcd_is_well_formed()(s_prime),
+        RMQCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s),
+        RMQCluster::etcd_and_scheduled_and_triggering_cr_in_correct_order(rabbitmq)(s),
+        object_in_every_create_or_update_request_msg_only_has_valid_owner_references()(s),
+        replicas_of_stateful_set_create_or_update_request_msg_satisfies_order(rabbitmq)(s),
+        s_prime.message_in_flight(msg),
+        sts_update_request_msg(rabbitmq.object_ref())(msg),
+    ensures
+        replicas_satisfies_order(msg.content.get_update_request().obj, rabbitmq)(s_prime),
+{
+    let step = choose |step| RMQCluster::next_step(s, s_prime, step);
+    let key = rabbitmq.object_ref();
+    let sts_key = make_stateful_set_key(key);
+    match step {
+        Step::KubernetesAPIStep(input) => {
+            assert(s.message_in_flight(msg));
+            assert(s.controller_state == s_prime.controller_state);
+            if s_prime.resource_key_exists(key) {
+                if s.resource_key_exists(key) {
+                    assert(replicas_of_rabbitmq(s.resource_obj_of(key)) <= replicas_of_rabbitmq(s_prime.resource_obj_of(key)));
+                } else {
+                    assert(s_prime.resource_obj_of(key).metadata.uid.is_Some());
+                    assert(s_prime.resource_obj_of(key).metadata.uid.get_Some_0() == s.kubernetes_api_state.uid_counter);
+                    let owner_refs = msg.content.get_update_request().obj.metadata.owner_references;
+                    if owner_refs.is_Some() && owner_refs.get_Some_0().len() == 1 {
+                        assert(owner_refs.get_Some_0()[0].uid < s.kubernetes_api_state.uid_counter);
+                        assert(owner_refs.get_Some_0()[0] != RabbitmqClusterView::from_dynamic_object(s_prime.resource_obj_of(key)).get_Ok_0().controller_owner_ref());
                     }
-                    assert(create_order(msg, s_prime) && update_order(msg, s_prime));
                 }
             }
+        },
+        Step::ControllerStep(input) => {
+            if !s.message_in_flight(msg) {
+                StatefulSetView::spec_integrity_is_preserved_by_marshal();
+                lemma_stateful_set_update_request_msg_implies_key_in_reconcile_equals(key, s, s_prime, msg, step);
+                assert(StatefulSetView::from_dynamic_object(msg.content.get_update_request().obj).get_Ok_0().spec.get_Some_0().replicas.get_Some_0() <= s.triggering_cr_of(key).spec.replicas);
+            }
+        },
+        Step::ScheduleControllerReconcileStep(input) => {
+            assert(s.message_in_flight(msg));
+            assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
+        },
+        Step::RestartController() => {
+            assert(s.message_in_flight(msg));
+            assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
+        },
+        _ => {
+            assert(s.message_in_flight(msg));
+            assert(s.kubernetes_api_state == s_prime.kubernetes_api_state);
+            assert(s.controller_state == s_prime.controller_state);
         }
     }
-    init_invariant(spec, RMQCluster::init(), next, inv);
 }
 
 }
diff --git a/src/controller_examples/rabbitmq_controller/spec/rabbitmqcluster.rs b/src/controller_examples/rabbitmq_controller/spec/rabbitmqcluster.rs
@@ -92,8 +92,6 @@ impl ResourceView for RabbitmqClusterView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: RabbitmqClusterSpecView) -> Value;

diff --git a/src/controller_examples/simple_controller/spec/custom_resource.rs b/src/controller_examples/simple_controller/spec/custom_resource.rs
@@ -151,8 +151,6 @@ impl ResourceView for SimpleCRView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: SimpleCRSpecView) -> Value;

diff --git a/src/controller_examples/zookeeper_controller/spec/types.rs b/src/controller_examples/zookeeper_controller/spec/types.rs
@@ -74,8 +74,6 @@ impl ResourceView for ZookeeperClusterView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: ZookeeperClusterSpecView) -> Value;

diff --git a/src/kubernetes_api_objects/cluster_role.rs b/src/kubernetes_api_objects/cluster_role.rs
@@ -189,8 +189,6 @@ impl ResourceView for ClusterRoleView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: ClusterRoleSpecView) -> Value;

diff --git a/src/kubernetes_api_objects/cluster_role_binding.rs b/src/kubernetes_api_objects/cluster_role_binding.rs
@@ -209,8 +209,6 @@ impl ResourceView for ClusterRoleBindingView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: ClusterRoleBindingSpecView) -> Value;

diff --git a/src/kubernetes_api_objects/config_map.rs b/src/kubernetes_api_objects/config_map.rs
@@ -219,8 +219,6 @@ impl ResourceView for ConfigMapView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: ConfigMapSpecView) -> Value;

diff --git a/src/kubernetes_api_objects/daemon_set.rs b/src/kubernetes_api_objects/daemon_set.rs
@@ -262,8 +262,6 @@ impl ResourceView for DaemonSetView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: Option<DaemonSetSpecView>) -> Value;

diff --git a/src/kubernetes_api_objects/persistent_volume_claim.rs b/src/kubernetes_api_objects/persistent_volume_claim.rs
@@ -256,8 +256,6 @@ impl ResourceView for PersistentVolumeClaimView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: Option<PersistentVolumeClaimSpecView>) -> Value;

diff --git a/src/kubernetes_api_objects/pod.rs b/src/kubernetes_api_objects/pod.rs
@@ -1112,8 +1112,6 @@ impl ResourceView for PodView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: Option<PodSpecView>) -> Value;

diff --git a/src/kubernetes_api_objects/resource.rs b/src/kubernetes_api_objects/resource.rs
@@ -72,12 +72,6 @@ pub trait ResourceView: Sized {
                 #[trigger] Self::from_dynamic_object(d).is_Ok()
                     ==> d.metadata == Self::from_dynamic_object(d).get_Ok_0().metadata();
 
-    proof fn from_dynamic_preserves_spec()
-        ensures
-            forall |d: DynamicObjectView|
-                #[trigger] Self::from_dynamic_object(d).is_Ok()
-                    ==> Self::unmarshal_spec(d.spec).get_Ok_0() == Self::from_dynamic_object(d).get_Ok_0().spec();
-
     proof fn from_dynamic_preserves_kind()
         ensures
             forall |d: DynamicObjectView|

diff --git a/src/kubernetes_api_objects/role.rs b/src/kubernetes_api_objects/role.rs
@@ -243,8 +243,6 @@ impl ResourceView for RoleView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: RoleSpecView) -> Value;

diff --git a/src/kubernetes_api_objects/role_binding.rs b/src/kubernetes_api_objects/role_binding.rs
@@ -309,8 +309,6 @@ impl ResourceView for RoleBindingView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: RoleBindingSpecView) -> Value;

diff --git a/src/kubernetes_api_objects/secret.rs b/src/kubernetes_api_objects/secret.rs
@@ -229,8 +229,6 @@ impl ResourceView for SecretView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     open spec fn marshal_spec(s: SecretSpecView) -> Value;

diff --git a/src/kubernetes_api_objects/service.rs b/src/kubernetes_api_objects/service.rs
@@ -314,8 +314,6 @@ impl ResourceView for ServiceView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: Option<ServiceSpecView>) -> Value;

diff --git a/src/kubernetes_api_objects/service_account.rs b/src/kubernetes_api_objects/service_account.rs
@@ -180,8 +180,6 @@ impl ResourceView for ServiceAccountView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: ServiceAccountSpecView) -> Value;

diff --git a/src/kubernetes_api_objects/stateful_set.rs b/src/kubernetes_api_objects/stateful_set.rs
@@ -337,8 +337,6 @@ impl ResourceView for StatefulSetView {
 
     proof fn from_dynamic_preserves_metadata() {}
 
-    proof fn from_dynamic_preserves_spec() {}
-
     proof fn from_dynamic_preserves_kind() {}
 
     closed spec fn marshal_spec(s: Option<StatefulSetSpecView>) -> Value;