Remove open/closed from empty spec functions

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

src/external_api/spec.rs

@@ -18,10 +18,10 @@ pub trait ExternalAPI {
     // transition describes the complete logic of external apis, which is a spec counterpart of ExternalAPI::process.
     // This method consumes the input (which should be computed by reconcile_core) and the current state of the external
     // api and produces the response and the next state of the api.
-    open spec fn transition(input: Self::Input, resources: StoredState, state: Self::State) -> (Self::State, Self::Output);
+    spec fn transition(input: Self::Input, resources: StoredState, state: Self::State) -> (Self::State, Self::Output);
 
     // init_state gives the initial state of the external api.
-    open spec fn init_state() -> Self::State;
+    spec fn init_state() -> Self::State;
 }
 
 pub struct EmptyTypeView {}

src/kubernetes_api_objects/resource.rs

@@ -26,17 +26,17 @@ pub trait ResourceView: Sized {
 
     /// Get the metadata of the object
 
-    open spec fn metadata(self) -> ObjectMetaView;
+    spec fn metadata(self) -> ObjectMetaView;
 
     /// Get the kind of the object
 
-    open spec fn kind() -> Kind;
+    spec fn kind() -> Kind;
 
     /// Get the reference of the object,
     /// which consists of kind, name and namespace
 
     // TODO: object_ref can be implemented here if default implementation is supported by Verus
-    open spec fn object_ref(self) -> ObjectRef;
+    spec fn object_ref(self) -> ObjectRef;
 
     proof fn object_ref_is_well_formed()
         ensures
@@ -49,15 +49,15 @@ pub trait ResourceView: Sized {
 
     /// Get the spec of the object
 
-    open spec fn spec(self) -> Self::Spec;
+    spec fn spec(self) -> Self::Spec;
 
     /// Convert the object to a dynamic object
 
-    open spec fn to_dynamic_object(self) -> DynamicObjectView;
+    spec fn to_dynamic_object(self) -> DynamicObjectView;
 
     /// Convert back from a dynamic object
 
-    open spec fn from_dynamic_object(obj: DynamicObjectView) -> Result<Self, ParseDynamicObjectError>;
+    spec fn from_dynamic_object(obj: DynamicObjectView) -> Result<Self, ParseDynamicObjectError>;
 
     /// Check if the data integrity is preserved after converting to and back from dynamic object
 
@@ -78,26 +78,26 @@ pub trait ResourceView: Sized {
                 #[trigger] Self::from_dynamic_object(d).is_Ok()
                     ==> d.kind == Self::kind();
 
-    closed spec fn marshal_spec(s: Self::Spec) -> Value;
+    spec fn marshal_spec(s: Self::Spec) -> Value;
 
-    closed spec fn unmarshal_spec(v: Value) -> Result<Self::Spec, ParseDynamicObjectError>;
+    spec fn unmarshal_spec(v: Value) -> Result<Self::Spec, ParseDynamicObjectError>;
 
     proof fn spec_integrity_is_preserved_by_marshal()
         ensures
             forall |s: Self::Spec|
                 Self::unmarshal_spec(#[trigger] Self::marshal_spec(s)).is_Ok()
                 && s == Self::unmarshal_spec(Self::marshal_spec(s)).get_Ok_0();
-    
+
     proof fn from_dynamic_object_result_determined_by_unmarshal()
         ensures
             forall |obj: DynamicObjectView|
                 obj.kind == Self::kind() ==> Self::unmarshal_spec(obj.spec).is_Ok() == #[trigger] Self::from_dynamic_object(obj).is_Ok();
 
     /// This method specifies the validation rule that only checks the new object.
-    open spec fn rule(obj: Self) -> bool;
+    spec fn rule(obj: Self) -> bool;
 
     /// This method specifies the validation rule that checks the relations between the new and old object.
-    open spec fn transition_rule(new_obj: Self, old_obj: Self) -> bool;
+    spec fn transition_rule(new_obj: Self, old_obj: Self) -> bool;
 
 }
 

src/pervasive_ext/to_view.rs

@@ -6,7 +6,7 @@ verus! {
 
 pub trait ToView {
     type V;
-    open spec fn to_view(&self) -> Self::V;
+    spec fn to_view(&self) -> Self::V;
 }
 
 }

src/reconciler/spec/reconciler.rs

@@ -21,21 +21,21 @@ pub trait Reconciler<#[verifier(maybe_negative)] K: ResourceView, #[verifier(may
     // Currently the local state is hardcoded to a ReconcileState.
     // We would like to make ReconcileState more general and reconcile_init_state
     // can also be more flexible.
-    open spec fn reconcile_init_state() -> Self::T;
+    spec fn reconcile_init_state() -> Self::T;
 
     // reconcile_core describes the logic of reconcile function and is the key logic we want to verify.
     // Each reconcile_core should take the local state and a response of the previous request (if any) as input
     // and outputs the next local state and the request to send to Kubernetes API (if any).
-    open spec fn reconcile_core(cr: K, resp_o: Option<ResponseView<ExternalAPIType::Output>>, state: Self::T)
+    spec fn reconcile_core(cr: K, resp_o: Option<ResponseView<ExternalAPIType::Output>>, state: Self::T)
         -> (Self::T, Option<RequestView<ExternalAPIType::Input>>);
 
     // reconcile_done is used to tell the controller_runtime whether this reconcile round is done.
     // If it is true, controller_runtime will probably requeue the reconcile.
-    open spec fn reconcile_done(state: Self::T) -> bool;
+    spec fn reconcile_done(state: Self::T) -> bool;
 
     // reconcile_error is used to tell the controller_runtime whether this reconcile round returns with error.
     // If it is true, controller_runtime will requeue the reconcile.
-    open spec fn reconcile_error(state: Self::T) -> bool;
+    spec fn reconcile_error(state: Self::T) -> bool;
 }
 
 }