From b12c762e79fe748c777fa850fd55f88bb0666180 Mon Sep 17 00:00:00 2001
From: Xudong Sun <xudongs3@illinois.edu>
Date: Thu, 3 Oct 2024 15:15:03 -0500
Subject: [PATCH] Use `option_view` whenever needed (#555)

Signed-off-by: Xudong Sun <xudongs3@illinois.edu>
---
 .../vreplicaset_controller/exec/reconciler.rs      |  3 ++-
 src/v2/reconciler/exec/io.rs                       | 14 --------------
 2 files changed, 2 insertions(+), 15 deletions(-)

diff --git a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs b/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
index 001d181b..4788af70 100644
--- a/src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
+++ b/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 v_replica_set@.well_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 {
diff --git a/src/v2/reconciler/exec/io.rs b/src/v2/reconciler/exec/io.rs
index c96abb54..a1f32e78 100644
--- a/src/v2/reconciler/exec/io.rs
+++ b/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) => {