Use option_view whenever needed (#555)

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

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

@@ -5,6 +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::{string_map::StringMap, string_view::*};
 use vstd::prelude::*;
 use vstd::seq_lib::*;
@@ -89,7 +90,7 @@ pub fn reconcile_error(state: &VReplicaSetReconcileState) -> (res: bool)
 
 pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<VoidEResp>>, state: VReplicaSetReconcileState) -> (res: (VReplicaSetReconcileState, Option<Request<VoidEReq>>))
     requires [email protected]_formed(),
-    ensures (res.0@, opt_request_to_view(&res.1)) == model_reconciler::reconcile_core(v_replica_set@, opt_response_to_view(&resp_o), state@),
+    ensures (res.0@, option_view(res.1)) == model_reconciler::reconcile_core(v_replica_set@, option_view(resp_o), state@),
 {
     let namespace = v_replica_set.metadata().namespace().unwrap();
     match &state.reconcile_step {

src/v2/reconciler/exec/io.rs

@@ -131,20 +131,6 @@ impl <T: View> View for Request<T> {
     }
 }
 
-pub open spec fn opt_response_to_view<T: View>(resp: &Option<Response<T>>) -> Option<ResponseView<T::V>> {
-    match resp {
-        Some(resp) => Some(resp@),
-        None => None,
-    }
-}
-
-pub open spec fn opt_request_to_view<T: View>(request: &Option<Request<T>>) -> Option<RequestView<T::V>> {
-    match request {
-        Some(req) => Some(req@),
-        None => None,
-    }
-}
-
 #[macro_export]
 macro_rules! is_some_k_get_resp {
     ($r:expr) => {