Use option_vec_view (anvil-verifier#559)

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

src/kubernetes_api_objects/exec/daemon_set.rs

@@ -28,9 +28,14 @@ pub struct DaemonSet {
     inner: deps_hack::k8s_openapi::api::apps::v1::DaemonSet,
 }
 
-impl DaemonSet {
-    pub spec fn view(&self) -> DaemonSetView;
 
+impl View for DaemonSet {
+    type V = DaemonSetView;
+
+    spec fn view(&self) -> DaemonSetView;
+}
+
+impl DaemonSet {
     #[verifier(external_body)]
     pub fn default() -> (daemon_set: DaemonSet)
         ensures daemon_set@ == DaemonSetView::default(),

src/kubernetes_api_objects/exec/persistent_volume_claim.rs

@@ -25,9 +25,13 @@ pub struct PersistentVolumeClaim {
     inner: deps_hack::k8s_openapi::api::core::v1::PersistentVolumeClaim,
 }
 
-impl PersistentVolumeClaim {
-    pub spec fn view(&self) -> PersistentVolumeClaimView;
+impl View for PersistentVolumeClaim {
+    type V = PersistentVolumeClaimView;
+
+    spec fn view(&self) -> PersistentVolumeClaimView;
+}
 
+impl PersistentVolumeClaim {
     #[verifier(external_body)]
     pub fn eq(&self, other: &Self) -> (b: bool)
         ensures b == (self.view() == other.view())

src/kubernetes_api_objects/exec/pod.rs

@@ -30,9 +30,13 @@ pub struct Pod {
     inner: deps_hack::k8s_openapi::api::core::v1::Pod,
 }
 
-impl Pod {
-    pub spec fn view(&self) -> PodView;
+impl View for Pod {
+    type V = PodView;
+
+    spec fn view(&self) -> PodView;
+}
 
+impl Pod {
     #[verifier(external_body)]
     pub fn default() -> (pod: Pod)
         ensures pod@ == PodView::default(),

src/v2/controllers/vreplicaset_controller/exec/reconciler.rs

@@ -5,7 +5,7 @@ use crate::kubernetes_api_objects::spec::prelude::*;
 use crate::reconciler::exec::{io::*, reconciler::*};
 use crate::vreplicaset_controller::model::reconciler as model_reconciler;
 use crate::vreplicaset_controller::trusted::{exec_types::*, step::*};
-use crate::vstd_ext::option_lib::option_view;
+use crate::vstd_ext::option_lib::*;
 use crate::vstd_ext::{string_map::StringMap, string_view::*};
 use vstd::prelude::*;
 use vstd::seq_lib::*;
@@ -276,7 +276,7 @@ pub fn make_owner_references(v_replica_set: &VReplicaSet) -> (owner_references:
 // TODO: This function can be replaced by a map.
 // Revisit it if Verus supports Vec.map.
 fn objects_to_pods(objs: Vec<DynamicObject>) -> (pods_or_none: Option<Vec<Pod>>)
-    ensures opt_podvec_to_view(&pods_or_none) == model_reconciler::objects_to_pods(objs@.map_values(|o: DynamicObject| o@))
+    ensures option_vec_view(pods_or_none) == model_reconciler::objects_to_pods(objs@.map_values(|o: DynamicObject| o@))
 {
     let mut pods = Vec::new();
     let mut idx = 0;
@@ -375,13 +375,6 @@ proof fn lemma_filter_contains_implies_contains<A>(s: Seq<A>, pred: spec_fn(A) -
     }
 }
 
-pub open spec fn opt_podvec_to_view(vec_or_none: &Option<Vec<Pod>>) -> Option<Seq<PodView>> {
-    match vec_or_none {
-        Some(vec) => Some(vec@.map_values(|p: Pod| p@)),
-        None => None,
-    }
-}
-
 // TODO: This function can be replaced by a map.
 // Revisit it if Verus supports Vec.map.
 fn filter_pods(pods: Vec<Pod>, v_replica_set: &VReplicaSet) -> (filtered_pods: Vec<Pod>)

src/vstd_ext/option_lib.rs

@@ -5,9 +5,16 @@ use vstd::prelude::*;
 
 verus! {
 
-pub open spec fn option_view<T: View>(t: Option<T>) -> Option<T::V> {
-    match t {
-        Some(v) => Some(v@),
+pub open spec fn option_view<T: View>(o: Option<T>) -> Option<T::V> {
+    match o {
+        Some(t) => Some(t@),
+        None => None,
+    }
+}
+
+pub open spec fn option_vec_view<T: View>(o: Option<Vec<T>>) -> Option<Seq<T::V>> {
+    match o {
+        Some(vec) => Some(vec@.map_values(|t: T| t@)),
         None => None,
     }
 }