Skip to content

Commit

Permalink
Add install helper for reconcile model
Browse files Browse the repository at this point in the history 
Signed-off-by: Xudong Sun <[email protected]>
  • Loading branch information
@marshtompsxd
marshtompsxd committed Oct 3, 2024
1 parent 8c41419 commit 07c7b7f
Show file tree
Hide file tree
Showing 12 changed files with 184 additions and 213 deletions.
59 changes: 36 additions & 23 deletions src/v2/controllers/vreplicaset_controller/exec/reconciler.rs
View file
Original file line number Diff line number Diff line change
@@ -1,48 +1,61 @@
// Copyright 2022 VMware, Inc.
// SPDX-License-Identifier: MIT
use crate::external_api::exec::*;
use crate::kubernetes_api_objects::exec::resource::ResourceWrapper;
use crate::kubernetes_api_objects::exec::{
container::*, label_selector::*, pod_template_spec::*, prelude::*, resource_requirements::*,
volume::*,
};
use crate::kubernetes_api_objects::spec::prelude::DynamicObjectView;
use crate::kubernetes_api_objects::spec::prelude::PodView;
use crate::kubernetes_api_objects::spec::resource::ResourceView;
use crate::reconciler::exec::{io::*, reconciler::*, resource_builder::*};
use crate::kubernetes_api_objects::exec::{label_selector::*, pod_template_spec::*, prelude::*};
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::*;
use crate::vreplicaset_controller::trusted::spec_types;
use crate::vreplicaset_controller::trusted::step::*;
use crate::vreplicaset_controller::trusted::{exec_types::*, step::*};
use crate::vstd_ext::{string_map::StringMap, string_view::*};
use vstd::prelude::*;
use vstd::seq_lib::*;
use vstd::string::*;

verus! {

// VReplicaSetReconcileState describes the local state with which the reconcile functions makes decisions.
pub struct VReplicaSetReconcileState {
pub reconcile_step: VReplicaSetReconcileStep,
pub filtered_pods: Option<Vec<Pod>>,
}

impl View for VReplicaSetReconcileState {
type V = model_reconciler::VReplicaSetReconcileState;

open spec fn view(&self) -> model_reconciler::VReplicaSetReconcileState {
model_reconciler::VReplicaSetReconcileState {
reconcile_step: self.reconcile_step,
filtered_pods: match self.filtered_pods {
Some(fp) => Some([email protected]_values(|p: Pod| p@)),
None => None,
},
}
}
}

pub struct VReplicaSetReconciler {}

impl Reconciler for VReplicaSetReconciler {
type R = VReplicaSet;
type T = VReplicaSetReconcileState;
type ExternalAPIType = EmptyAPIShimLayer;
type S = VReplicaSetReconcileState;
type K = VReplicaSet;
type EReq = VoidEReq;
type EResp = VoidEResp;

open spec fn well_formed(v_replica_set: &VReplicaSet) -> bool { [email protected]_formed() }
open spec fn well_formed(v_replica_set: &Self::K) -> bool {
[email protected]_formed()
}

fn reconcile_init_state() -> VReplicaSetReconcileState {
fn reconcile_init_state() -> Self::S {
reconcile_init_state()
}

fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<EmptyType>>, state: VReplicaSetReconcileState) -> (VReplicaSetReconcileState, Option<Request<EmptyType>>) {
fn reconcile_core(v_replica_set: &Self::K, resp_o: Option<Response<Self::EResp>>, state: Self::S) -> (Self::S, Option<Request<Self::EReq>>) {
reconcile_core(v_replica_set, resp_o, state)
}

fn reconcile_done(state: &VReplicaSetReconcileState) -> bool {
fn reconcile_done(state: &Self::S) -> bool {
reconcile_done(state)
}

fn reconcile_error(state: &VReplicaSetReconcileState) -> bool {
fn reconcile_error(state: &Self::S) -> bool {
reconcile_error(state)
}
}
Expand Down Expand Up @@ -74,7 +87,7 @@ pub fn reconcile_error(state: &VReplicaSetReconcileState) -> (res: bool)
}
}

pub fn reconcile_core(v_replica_set: &VReplicaSet, resp_o: Option<Response<EmptyType>>, state: VReplicaSetReconcileState) -> (res: (VReplicaSetReconcileState, Option<Request<EmptyType>>))
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@),
{
Expand Down
71 changes: 2 additions & 69 deletions src/v2/controllers/vreplicaset_controller/model/install.rs
View file
Original file line number Diff line number Diff line change
@@ -1,41 +1,13 @@
// Copyright 2022 VMware, Inc.
// SPDX-License-Identifier: MIT
use crate::external_api::spec::EmptyTypeView;
use crate::kubernetes_api_objects::{error::*, spec::prelude::*};
use crate::kubernetes_cluster::spec::{
api_server::types::InstalledType,
cluster::ControllerModel,
controller::types::{ReconcileModel, RequestContent, ResponseContent},
install_helpers::*,
};
use crate::reconciler::spec::io::{RequestView, ResponseView};
use crate::reconciler::spec::reconciler::Reconciler;
use crate::kubernetes_cluster::spec::cluster::{Cluster, ControllerModel};
use crate::vreplicaset_controller::model::reconciler::*;
use crate::vreplicaset_controller::trusted::spec_types::*;
use vstd::prelude::*;

verus! {

pub open spec fn vrs_installed_type() -> InstalledType {
InstalledType {
unmarshallable_spec: |v| {
InstallTypeHelper::<VReplicaSetView>::unmarshal_spec(v)
},
unmarshallable_status: |v| {
InstallTypeHelper::<VReplicaSetView>::unmarshal_status(v)
},
valid_object: |obj| {
InstallTypeHelper::<VReplicaSetView>::valid_object(obj)
},
valid_transition: |obj, old_obj| {
InstallTypeHelper::<VReplicaSetView>::valid_transition(obj, old_obj)
},
marshalled_default_status: || {
InstallTypeHelper::<VReplicaSetView>::marshalled_default_status()
}
}
}

impl Marshallable for VReplicaSetReconcileState {
spec fn marshal(self) -> Value;

Expand All @@ -47,48 +19,9 @@ impl Marshallable for VReplicaSetReconcileState {
{}
}

impl Marshallable for EmptyTypeView {
spec fn marshal(self) -> Value;

spec fn unmarshal(v: Value) -> Result<Self, UnmarshalError>;

#[verifier(external_body)]
proof fn marshal_preserves_integrity()
ensures forall |o: Self| Self::unmarshal(#[trigger] o.marshal()).is_Ok() && o == Self::unmarshal(o.marshal()).get_Ok_0()
{}
}

pub open spec fn vrs_reconcile_model() -> ReconcileModel {
ReconcileModel {
kind: VReplicaSetView::kind(),
init: || VReplicaSetReconciler::reconcile_init_state().marshal(),
transition: |obj, resp_o, s| {
let obj_um = VReplicaSetView::unmarshal(obj).get_Ok_0();
let resp_o_um = match resp_o {
None => None,
Some(resp) => Some(match resp {
ResponseContent::KubernetesResponse(api_resp) => ResponseView::<EmptyTypeView>::KResponse(api_resp),
ResponseContent::ExternalResponse(ext_resp) => ResponseView::<EmptyTypeView>::ExternalResponse(EmptyTypeView::unmarshal(ext_resp).get_Ok_0()),
})
};
let s_um = VReplicaSetReconcileState::unmarshal(s).get_Ok_0();
let (s_prime_um, req_o_um) = VReplicaSetReconciler::reconcile_core(obj_um, resp_o_um, s_um);
(s_prime_um.marshal(), match req_o_um {
None => None,
Some(req) => Some(match req {
RequestView::<EmptyTypeView>::KRequest(api_req) => RequestContent::KubernetesRequest(api_req),
RequestView::<EmptyTypeView>::ExternalRequest(ext_req) => RequestContent::ExternalRequest(ext_req.marshal()),
})
})
},
done: |s| VReplicaSetReconciler::reconcile_done(VReplicaSetReconcileState::unmarshal(s).get_Ok_0()),
error: |s| VReplicaSetReconciler::reconcile_error(VReplicaSetReconcileState::unmarshal(s).get_Ok_0()),
}
}

pub open spec fn vrs_controller_model() -> ControllerModel {
ControllerModel {
reconcile_model: vrs_reconcile_model(),
reconcile_model: Cluster::installed_reconcile_model::<VReplicaSetReconciler>(),
external_model: None,
}
}
Expand Down
26 changes: 15 additions & 11 deletions src/v2/controllers/vreplicaset_controller/model/reconciler.rs
View file
Original file line number Diff line number Diff line change
@@ -1,33 +1,39 @@
// Copyright 2022 VMware, Inc.
// SPDX-License-Identifier: MIT
#![allow(unused_imports)]
use crate::external_api::spec::*;
use crate::kubernetes_api_objects::spec::prelude::*;
use crate::reconciler::spec::{io::*, reconciler::*};
use crate::vreplicaset_controller::trusted::{spec_types::*, step::*};
use vstd::{prelude::*, string::*};

verus! {

pub struct VReplicaSetReconciler {}

pub struct VReplicaSetReconcileState {
pub reconcile_step: VReplicaSetReconcileStep,
pub filtered_pods: Option<Seq<PodView>>,
}

impl Reconciler for VReplicaSetReconciler {
type T = VReplicaSetReconcileState;
type S = VReplicaSetReconcileState;
type K = VReplicaSetView;
type E = EmptyAPI;
type EReq = VoidEReqView;
type EResp = VoidERespView;

open spec fn reconcile_init_state() -> VReplicaSetReconcileState {
open spec fn reconcile_init_state() -> Self::S {
reconcile_init_state()
}

open spec fn reconcile_core(fb: VReplicaSetView, resp_o: Option<ResponseView<EmptyTypeView>>, state: VReplicaSetReconcileState)
-> (VReplicaSetReconcileState, Option<RequestView<EmptyTypeView>>) {
open spec fn reconcile_core(fb: Self::K, resp_o: Option<ResponseView<Self::EResp>>, state: Self::S) -> (Self::S, Option<RequestView<Self::EReq>>) {
reconcile_core(fb, resp_o, state)
}

open spec fn reconcile_done(state: VReplicaSetReconcileState) -> bool {
open spec fn reconcile_done(state: Self::S) -> bool {
reconcile_done(state)
}

open spec fn reconcile_error(state: VReplicaSetReconcileState) -> bool {
open spec fn reconcile_error(state: Self::S) -> bool {
reconcile_error(state)
}
}
Expand All @@ -53,9 +59,7 @@ pub open spec fn reconcile_error(state: VReplicaSetReconcileState) -> bool {
}
}

pub open spec fn reconcile_core(
v_replica_set: VReplicaSetView, resp_o: Option<ResponseView<EmptyTypeView>>, state: VReplicaSetReconcileState
) -> (VReplicaSetReconcileState, Option<RequestView<EmptyTypeView>>) {
pub open spec fn reconcile_core(v_replica_set: VReplicaSetView, resp_o: Option<ResponseView<VoidERespView>>, state: VReplicaSetReconcileState) -> (VReplicaSetReconcileState, Option<RequestView<VoidEReqView>>) {
let namespace = v_replica_set.metadata.namespace.unwrap();
match &state.reconcile_step {
VReplicaSetReconcileStep::Init => {
Expand Down
36 changes: 0 additions & 36 deletions src/v2/controllers/vreplicaset_controller/trusted/exec_types.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,42 +12,6 @@ use vstd::prelude::*;

verus! {

// VReplicaSetReconcileState describes the local state with which the reconcile functions makes decisions.
pub struct VReplicaSetReconcileState {
pub reconcile_step: VReplicaSetReconcileStep,
pub filtered_pods: Option<Vec<Pod>>,
}

// impl std::clone::Clone for VReplicaSetReconcileState {

// #[verifier(external_body)]
// fn clone(&self) -> (result: VReplicaSetReconcileState)
// ensures result == self
// {
// VReplicaSetReconcileState {
// reconcile_step: self.reconcile_step,
// filtered_pods: match self.filtered_pods {
// Some(fp) => Some(fp.clone()),
// None => None,
// },
// }
// }
// }

impl View for VReplicaSetReconcileState {
type V = spec_types::VReplicaSetReconcileState;

open spec fn view(&self) -> spec_types::VReplicaSetReconcileState {
spec_types::VReplicaSetReconcileState {
reconcile_step: self.reconcile_step,
filtered_pods: match self.filtered_pods {
Some(fp) => Some([email protected]_values(|p: Pod| p@)),
None => None,
},
}
}
}

#[verifier(external_body)]
pub struct VReplicaSet {
inner: deps_hack::VReplicaSet
Expand Down
9 changes: 1 addition & 8 deletions src/v2/controllers/vreplicaset_controller/trusted/spec_types.rs
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
// Copyright 2022 VMware, Inc.
// SPDX-License-Identifier: MIT
use crate::external_api::spec::{EmptyAPI, EmptyTypeView};
use crate::kubernetes_api_objects::error::*;
use crate::kubernetes_api_objects::spec::{
api_resource::*, label_selector::*, pod_template_spec::*, prelude::*,
Expand All @@ -12,13 +11,6 @@ use vstd::prelude::*;

verus! {

pub struct VReplicaSetReconciler {}

pub struct VReplicaSetReconcileState {
pub reconcile_step: VReplicaSetReconcileStep,
pub filtered_pods: Option<Seq<PodView>>,
}

pub struct VReplicaSetView {
pub metadata: ObjectMetaView,
pub spec: VReplicaSetSpecView,
Expand All @@ -28,6 +20,7 @@ pub struct VReplicaSetView {
pub type VReplicaSetStatusView = EmptyStatusView;

impl VReplicaSetView {
// TODO: well_formed should just call state_validation
pub open spec fn well_formed(self) -> bool {
&&& self.metadata.name.is_Some()
&&& self.metadata.namespace.is_Some()
Expand Down
10 changes: 0 additions & 10 deletions src/v2/kubernetes_cluster/proof/objects_in_store.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,16 +140,6 @@ pub open spec fn each_custom_object_in_etcd_is_well_formed<T: CustomResourceView
}
}

pub open spec fn type_is_installed_in_cluster<T: CustomResourceView>(self) -> bool {
let string = T::kind().get_CustomResourceKind_0();
&&& self.installed_types.contains_key(string)
&&& self.installed_types[string].unmarshallable_spec == |v: Value| InstallTypeHelper::<T>::unmarshal_spec(v)
&&& self.installed_types[string].unmarshallable_status == |v: Value| InstallTypeHelper::<T>::unmarshal_status(v)
&&& self.installed_types[string].valid_object == |obj: DynamicObjectView| InstallTypeHelper::<T>::valid_object(obj)
&&& self.installed_types[string].valid_transition == |obj, old_obj: DynamicObjectView| InstallTypeHelper::<T>::valid_transition(obj, old_obj)
&&& self.installed_types[string].marshalled_default_status == || InstallTypeHelper::<T>::marshalled_default_status()
}

pub proof fn lemma_always_each_custom_object_in_etcd_is_well_formed<T: CustomResourceView>(self, spec: TempPred<ClusterState>)
requires
spec.entails(lift_state(self.init())),
Expand Down
Loading

0 comments on commit 07c7b7f

Please sign in to comment.