Theory Step_vpeq

subsection ‹The view-partitioning equivalence relation›

theory Step_vpeq
  imports Step Step_invariants
begin

text ‹The view consists of
 \begin{enumerate}
 \item View of object values.
 \item View of subject-subject dynamic policy. The threads can discover the policy
       at runtime, e.g. by calling ipc() and observing success or failure.
 \item View of subject-object dynamic policy. The threads can discover the policy
       at runtime, e.g. by calling open() and observing success or failure.
 \end{enumerate}
›

definition vpeq_obj :: "partition_id_t  state_t  state_t  bool" where
  "vpeq_obj u s t   obj_id . Policy.sp_spec_subj_obj u obj_id READ  (obj s) obj_id = (obj t) obj_id"

definition vpeq_subj_subj :: "partition_id_t  state_t  state_t  bool" where
  "vpeq_subj_subj u s t 
     v . ((Policy.sp_spec_subj_subj u v  sp_impl_subj_subj s u v = sp_impl_subj_subj t u v)
            (Policy.sp_spec_subj_subj v u  sp_impl_subj_subj s v u = sp_impl_subj_subj t v u))"

definition vpeq_subj_obj :: "partition_id_t  state_t  state_t  bool" where
  "vpeq_subj_obj u s t     
    ob m p1 .
     (Policy.sp_spec_subj_obj u ob m  sp_impl_subj_obj s u ob m = sp_impl_subj_obj t u ob m) 
    (Policy.sp_spec_subj_obj p1 ob PROVIDE  (Policy.sp_spec_subj_obj u ob READ  Policy.sp_spec_subj_obj u ob WRITE) 
         sp_impl_subj_obj s p1 ob PROVIDE = sp_impl_subj_obj t p1 ob PROVIDE)"
   

definition vpeq_local :: "partition_id_t  state_t  state_t  bool" where
 "vpeq_local u s t 
     tid . (partition tid) = u  (thread s tid) = (thread t tid)"

definition "vpeq u s t 
   vpeq_obj u s t  vpeq_subj_subj u s t  vpeq_subj_obj u s t  vpeq_local u s t"

subsubsection ‹Elementary properties›

lemma vpeq_rel:
  shows vpeq_refl: "vpeq u s s"
    and vpeq_sym [sym]: "vpeq u s t  vpeq u t s"
    and vpeq_trans [trans]: " vpeq u s1 s2 ; vpeq u s2 s3   vpeq u s1 s3"
  unfolding vpeq_def vpeq_obj_def vpeq_subj_subj_def vpeq_subj_obj_def vpeq_local_def
    by auto

text ‹Auxiliary equivalence relation.›


lemma set_object_value_ign:
  assumes eq_obs: "~ Policy.sp_spec_subj_obj u x READ"
    shows "vpeq u s (set_object_value x y s)"
proof -
  from assms show ?thesis
    unfolding vpeq_def vpeq_obj_def vpeq_subj_subj_def vpeq_subj_obj_def set_object_value_def 
              vpeq_local_def
    by auto
qed

text ‹Context-switch and fetch operations are also consistent with vpeq
        and locally respect everything.›

theorem cswitch_consistency_and_respect:
  fixes u :: partition_id_t 
    and s :: state_t
    and new_current :: thread_id_t
  assumes "atomic_step_invariant s"
  shows "vpeq u s (s  current := new_current )"
proof -
  show ?thesis
    unfolding vpeq_def vpeq_obj_def vpeq_subj_subj_def vpeq_subj_obj_def vpeq_local_def
    by auto
qed



end