Invariant transfer lemma

Signed-off-by: Xudong Sun <[email protected]>

src/v2/kubernetes_cluster/proof/mod.rs

@@ -11,6 +11,7 @@ pub mod network_liveness;
 pub mod objects_in_reconcile;
 pub mod objects_in_store;
 pub mod req_resp;
+pub mod retentive_cluster;
 pub mod stability;
 pub mod transition_validation;
 pub mod wf1_helpers;

src/v2/kubernetes_cluster/proof/retentive_cluster.rs

@@ -0,0 +1,95 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+#![allow(unused_imports)]
+use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::kubernetes_cluster::spec::{cluster_state_machine::*, retentive_cluster::*};
+use crate::temporal_logic::{defs::*, rules::*};
+use vstd::prelude::*;
+
+verus! {
+
+impl RetentiveCluster {
+
+pub proof fn transfer_invariant_to_cluster(self, inv: StatePred<ClusterState>)
+    requires
+        forall |h| #[trigger] self.init()(h) ==> inv(h.current),
+        forall |h: ClusterHistory, h_prime: ClusterHistory| inv(h.current) && #[trigger] self.next()(h, h_prime) ==> inv(h_prime.current),
+    ensures
+        forall |s| #[trigger] self.to_cluster().init()(s) ==> inv(s),
+        forall |s, s_prime| inv(s) && #[trigger] self.to_cluster().next()(s, s_prime) ==> inv(s_prime),
+{
+    assert forall |s| #[trigger] self.to_cluster().init()(s) implies inv(s) by {
+        let h = ClusterHistory {
+            current: s,
+            past: Seq::<ClusterState>::empty(),
+        };
+        self.reverse_refinement_init(s, h);
+    }
+    assert forall |s, s_prime| inv(s) && #[trigger] self.to_cluster().next()(s, s_prime) implies inv(s_prime) by {
+        let h = ClusterHistory {
+            current: s,
+            past: arbitrary(),
+        };
+        let h_prime = ClusterHistory {
+            current: s_prime,
+            past: h.past.push(s),
+        };
+        self.reverse_refinement_next(s, s_prime, h, h_prime);
+    }
+}
+
+pub proof fn transfer_invariant_from_cluster(self, inv: StatePred<ClusterState>)
+    requires
+        forall |s| #[trigger] self.to_cluster().init()(s) ==> inv(s),
+        forall |s, s_prime| inv(s) && #[trigger] self.to_cluster().next()(s, s_prime) ==> inv(s_prime),
+    ensures
+        forall |h| #[trigger] self.init()(h) ==> inv(h.current),
+        forall |h: ClusterHistory, h_prime: ClusterHistory| inv(h.current) && #[trigger] self.next()(h, h_prime) ==> inv(h_prime.current),
+
+{
+    assert forall |h| #[trigger] self.init()(h) implies inv(h.current) by {
+        self.refinement_init(h);
+    }
+    assert forall |h: ClusterHistory, h_prime: ClusterHistory| inv(h.current) && #[trigger] self.next()(h, h_prime) implies inv(h_prime.current) by {
+        self.refinement_next(h, h_prime);
+    }
+}
+
+pub proof fn refinement_init(self, h: ClusterHistory)
+    requires
+        self.init()(h),
+    ensures
+        self.to_cluster().init()(h.current),
+{}
+
+pub proof fn refinement_next(self, h: ClusterHistory, h_prime: ClusterHistory)
+    requires
+        self.next()(h, h_prime),
+    ensures
+        self.to_cluster().next()(h.current, h_prime.current),
+{}
+
+pub proof fn reverse_refinement_init(self, s: ClusterState, h: ClusterHistory)
+    requires
+        self.to_cluster().init()(s),
+        h.current == s,
+        h.past == Seq::<ClusterState>::empty(),
+    ensures
+        self.init()(h),
+{}
+
+pub proof fn reverse_refinement_next(self, s: ClusterState, s_prime: ClusterState, h: ClusterHistory, h_prime: ClusterHistory)
+    requires
+        self.to_cluster().next()(s, s_prime),
+        h.current == s,
+        h_prime.current == s_prime,
+        h_prime.past == h.past.push(s),
+    ensures
+        self.next()(h, h_prime),
+{}
+
+}
+
+
+
+}

src/v2/kubernetes_cluster/spec/mod.rs

@@ -9,3 +9,4 @@ pub mod install_helpers;
 pub mod message;
 pub mod network;
 pub mod pod_monkey;
+pub mod retentive_cluster;

src/v2/kubernetes_cluster/spec/retentive_cluster.rs

@@ -0,0 +1,49 @@
+// Copyright 2022 VMware, Inc.
+// SPDX-License-Identifier: MIT
+#![allow(unused_imports)]
+use crate::kubernetes_api_objects::error::*;
+use crate::kubernetes_api_objects::spec::prelude::*;
+use crate::kubernetes_cluster::spec::{
+    api_server::types::InstalledTypes, cluster_state_machine::*,
+};
+use crate::state_machine::{action::*, state_machine::*};
+use crate::temporal_logic::defs::*;
+use vstd::{multiset::*, prelude::*};
+
+verus! {
+
+pub struct ClusterHistory {
+    pub current: ClusterState,
+    pub past: Seq<ClusterState>,
+}
+
+pub struct RetentiveCluster {
+    pub installed_types: InstalledTypes,
+    pub controller_models: Map<int, ControllerModel>,
+}
+
+impl RetentiveCluster {
+    pub open spec fn init(self) -> StatePred<ClusterHistory> {
+        |h: ClusterHistory| {
+            &&& self.to_cluster().init()(h.current)
+            &&& h.past == Seq::<ClusterState>::empty()
+        }
+    }
+
+    pub open spec fn next(self) -> ActionPred<ClusterHistory> {
+        |h: ClusterHistory, h_prime: ClusterHistory| {
+            &&& self.to_cluster().next()(h.current, h_prime.current)
+            &&& h_prime.past == h.past.push(h.current)
+        }
+    }
+
+    #[verifier(inline)]
+    pub open spec fn to_cluster(self) -> Cluster {
+        Cluster {
+            installed_types: self.installed_types,
+            controller_models: self.controller_models,
+        }
+    }
+}
+
+}