kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_S

lemma bisim_reflE_dc:
  "bisim (dc \<oplus> (=)) \<top> \<top> a a" apply (rule bisim_underlyingI) apply (case_tac r, fastforce+)[1] apply (case_tac r', fastforce+)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (dc \<oplus> (=)) (\<lambda>_. True) (\<lambda>_. True) a a proof (prove)
goal (2 subgoals):
 1. \<And>s s' r t. \<lbrakk>s = s'; True; True; (r, t) \<in> fst (a s)\<rbrakk> \<Longrightarrow> \<exists>(r', t')\<in>fst (a s'). (dc \<oplus> (=)) r r' \<and> t = t'
 2. \<And>s s' r' t'. \<lbrakk>s = s'; True; True; (r', t') \<in> fst (a s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (a s). (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' r' t'. \<lbrakk>s = s'; True; True; (r', t') \<in> fst (a s')\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (a s). (dc \<oplus> (=)) r r' \<and> t = t' proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma perform_invocation_bisim:
  "bisim (dc \<oplus> (=)) \<top> (\<top> and K (separate_inv c))
  (perform_invocation a b c) (Syscall_A.perform_invocation a b c)" apply (rule bisim_gen_asm_r) apply clarsimp apply (rule bisim_reflE_dc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (dc \<oplus> (=)) (\<lambda>_. True) ((\<lambda>_. True) and K (separate_inv c)) (Syscall_SA.perform_invocation a b c) (Syscall_A.perform_invocation a b c) proof (prove)
goal (1 subgoal):
 1. separate_inv c \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (\<lambda>_. True) (Syscall_SA.perform_invocation a b c) (Syscall_A.perform_invocation a b c) proof (prove)
goal (1 subgoal):
 1. \<And>ptr badge. c = InvokeNotification ptr badge \<Longrightarrow> bisim (dc \<oplus> (=)) (\<lambda>_. True) (\<lambda>_. True) (doE y <- liftE (send_signal ptr badge);
returnOk []
odE) (doE y <- liftE (send_signal ptr badge);
returnOk []
odE) proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma lcas_sep [wp]:
  "\<lbrace>separate_state and valid_objs\<rbrace> lookup_cap_and_slot t v \<lbrace>\<lambda>rv s. separate_cap (fst rv)\<rbrace>, -" apply (simp add: lookup_cap_and_slot_def split_def bind_assoc) apply (rule hoare_pre) apply (wp lsft_sep get_cap_wp'|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state and valid_objs\<rbrace> lookup_cap_and_slot t v \<lbrace>\<lambda>rv s. separate_cap (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state and valid_objs\<rbrace> doE p <- lookup_slot_for_thread t v;
cap <- liftE (get_cap (fst p));
returnOk (cap, fst p)
odE \<lbrace>\<lambda>rv s. separate_cap (fst rv)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE p <- lookup_slot_for_thread t v;
cap <- liftE (get_cap (fst p));
returnOk (cap, fst p)
odE \<lbrace>\<lambda>rv s. separate_cap (fst rv)\<rbrace>, -
 2. \<And>s. (separate_state and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma lec_separate_caps:
  "\<lbrace>separate_state and valid_objs\<rbrace> lookup_extra_caps t buffer ra \<lbrace>\<lambda>rv s. (\<forall>c\<in>set rv. separate_cap (fst c))\<rbrace>, -" unfolding lookup_extra_caps_def apply (wp mapME_set | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state and valid_objs\<rbrace> lookup_extra_caps t buffer ra \<lbrace>\<lambda>rv s. \<forall>c\<in>set rv. separate_cap (fst c)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state and valid_objs\<rbrace> (liftE $ get_extra_cptrs buffer ra) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot t cptr) \<lbrace>\<lambda>rv s. \<forall>c\<in>set rv. separate_cap (fst c)\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma rel_sum_comb_eq:
  "((=) \<oplus> (=)) = (=)" apply (rule ext, rule ext) apply (case_tac x) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (=) \<oplus> (=) = (=) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. ((=) \<oplus> (=)) x xa = (x = xa) proof (prove)
goal (2 subgoals):
 1. \<And>x xa a. x = Inl a \<Longrightarrow> ((=) \<oplus> (=)) x xa = (x = xa)
 2. \<And>x xa b. x = Inr b \<Longrightarrow> ((=) \<oplus> (=)) x xa = (x = xa) proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma separate_state_cdt [simp]:
  "separate_state (s\<lparr>cdt := x\<rparr>) = separate_state s" unfolding separate_state_def by (simp add: get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. separate_state (s\<lparr>cdt := x\<rparr>) = separate_state s proof (prove)
goal (1 subgoal):
 1. (\<forall>p. tcb_at p (s\<lparr>cdt := x\<rparr>) \<longrightarrow> separate_tcb p (caps_of_state (s\<lparr>cdt := x\<rparr>))) = (\<forall>p. tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s))
theory Syscall_S

lemma separate_state_original [simp]:
  "separate_state (s\<lparr>is_original_cap := x\<rparr>) = separate_state s" unfolding separate_state_def by (simp add: get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. separate_state (s\<lparr>is_original_cap := x\<rparr>) = separate_state s proof (prove)
goal (1 subgoal):
 1. (\<forall>p. tcb_at p (s\<lparr>is_original_cap := x\<rparr>) \<longrightarrow> separate_tcb p (caps_of_state (s\<lparr>is_original_cap := x\<rparr>))) = (\<forall>p. tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s))
theory Syscall_S

lemma separate_cap_NullCap [simp]: "separate_cap NullCap" by (simp add: separate_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. separate_cap NullCap
theory Syscall_S

lemma separate_state_pres:
  assumes rl: "(\<And>P t p. \<lbrace>\<lambda>s. P (typ_at t p s) (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at t p s) (caps_of_state s)\<rbrace>)"
  shows  "\<lbrace>separate_state\<rbrace> f \<lbrace>\<lambda>_. separate_state\<rbrace>" unfolding separate_state_def[abs_def] apply (simp add: tcb_at_typ) apply (wp hoare_vcg_all_lift rl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> f \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>p. tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. typ_at ATCB p s \<longrightarrow> separate_tcb p (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>p. typ_at ATCB p s \<longrightarrow> separate_tcb p (caps_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma separate_state_pres':
  assumes rl: "(\<And>P t p. \<lbrace>\<lambda>s. P (typ_at t p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at t p s)\<rbrace>)"
  "(\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>)"
  shows  "\<lbrace>separate_state\<rbrace> f \<lbrace>\<lambda>_. separate_state\<rbrace>" apply (rule separate_state_pres) apply (rule hoare_pre) apply (wps rl) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> f \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P t p. \<lbrace>\<lambda>s. P (typ_at t p s) (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at t p s) (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P t p. \<lbrace>?Q2 P t p\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at t p s) (caps_of_state s)\<rbrace>
 2. \<And>P t p s. P (typ_at t p s) (caps_of_state s) \<Longrightarrow> ?Q2 P t p s proof (prove)
goal (2 subgoals):
 1. \<And>P t p prev_s. \<lbrace>?P5 P t p prev_s\<rbrace> f \<lbrace>\<lambda>rv s'. P (typ_at t p prev_s) (caps_of_state prev_s)\<rbrace>
 2. \<And>P t p s. P (typ_at t p s) (caps_of_state s) \<Longrightarrow> ?P5 P t p s s proof (prove)
goal (1 subgoal):
 1. \<And>P t p s. P (typ_at t p s) (caps_of_state s) \<Longrightarrow> P (typ_at t p s) (caps_of_state s) proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma separate_state_more_update[simp]:
  "separate_state (trans_state f s) =
   separate_state s" by (simp add: separate_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. separate_state (trans_state f s) = separate_state s
theory Syscall_S

lemma cap_delete_one_sep [wp]:
  "\<lbrace>separate_state\<rbrace> cap_delete_one cptr \<lbrace>\<lambda>_. separate_state\<rbrace>" unfolding cap_delete_one_def empty_slot_def post_cap_deletion_def by (wpsimp wp: get_cap_wp' hoare_drop_imps |
      rule separate_state_pres, rule hoare_pre, (wps set_cdt_typ_at; wp), assumption)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> cap_delete_one cptr \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> do cap <- get_cap cptr;
unless (cap = NullCap) $ do final <- is_final_cap cap;
fast_finalise cap final;
cap <- get_cap cptr;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s cptr);
cdt <- gets cdt;
parent <- return $ cdt cptr;
set_cdt ((\<lambda>p. if cdt p = Some cptr then parent else cdt p)(cptr := None));
do_extended_op (empty_slot_ext cptr slot_p);
set_original cptr False;
set_cap NullCap cptr;
case NullCap of IRQHandlerCap irq \<Rightarrow> deleted_irq_handler irq | ArchObjectCap acap \<Rightarrow> arch_post_cap_deletion acap | _ \<Rightarrow> return ()
od
od
od \<lbrace>\<lambda>_. separate_state\<rbrace>
theory Syscall_S

lemma delete_caller_cap_bisim:
  "bisim (=) \<top> (tcb_at r and separate_state) (return ()) (delete_caller_cap r)" unfolding delete_caller_cap_def apply (rule bisim_guard_imp) apply (simp add: cap_delete_one_def unless_when) apply (rule bisim_caller_cap) apply (simp add: when_def) apply (rule bisim_refl') apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (tcb_at r and separate_state) (return ()) (delete_caller_cap r) proof (prove)
goal (1 subgoal):
 1. bisim (=) (\<lambda>_. True) (tcb_at r and separate_state) (return ()) (cap_delete_one (r, tcb_cnode_index 3)) proof (prove)
goal (3 subgoals):
 1. bisim (=) ?Q ?Q' (return ()) (cap_delete_one (r, tcb_cnode_index 3))
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at r and separate_state) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. bisim (=) ?Q ?Q' (return ()) (do cap <- get_cap (r, tcb_cnode_index 3);
when (cap \<noteq> NullCap) (do final <- is_final_cap cap;
y <- fast_finalise cap final;
empty_slot (r, tcb_cnode_index 3) NullCap
od)
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at r and separate_state) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. bisim (=) ?Q ?P'4 (return ()) (when (NullCap \<noteq> NullCap) (do final <- is_final_cap NullCap;
y <- fast_finalise NullCap final;
empty_slot (r, tcb_cnode_index 3) NullCap
od))
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at r and separate_state) s \<Longrightarrow> (?P'4 and tcb_at r and separate_state) s proof (prove)
goal (3 subgoals):
 1. bisim (=) ?Q ?P'4 (return ()) (return ())
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (tcb_at r and separate_state) s \<Longrightarrow> (?P'4 and tcb_at r and separate_state) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> True
 2. \<And>s. (tcb_at r and separate_state) s \<Longrightarrow> ((\<lambda>_. True) and tcb_at r and separate_state) s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma bisim_guard_imp_both:
  "\<lbrakk> bisim r P P' m m'; \<And>s. R s \<Longrightarrow> P s \<and> P' s \<rbrakk> \<Longrightarrow> bisim r \<top> R m m'" unfolding bisim_underlying_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bisim r P P' m m'; \<And>s. R s \<Longrightarrow> P s \<and> P' s\<rbrakk> \<Longrightarrow> bisim r (\<lambda>_. True) R m m' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s s'. s = s' \<and> P s \<and> P' s' \<longrightarrow> (\<forall>(ra, t)\<in>fst (m s). \<exists>(r', t')\<in>fst (m' s'). r ra r' \<and> t = t') \<and> (\<forall>(r', t')\<in>fst (m' s'). \<exists>(ra, t)\<in>fst (m s). r ra r' \<and> t = t'); \<And>s. R s \<Longrightarrow> P s \<and> P' s\<rbrakk> \<Longrightarrow> \<forall>s s'. s = s' \<and> True \<and> R s' \<longrightarrow> (\<forall>(ra, t)\<in>fst (m s). \<exists>(r', t')\<in>fst (m' s'). r ra r' \<and> t = t') \<and> (\<forall>(r', t')\<in>fst (m' s'). \<exists>(ra, t)\<in>fst (m s). r ra r' \<and> t = t')
theory Syscall_S

lemma as_user_separate_state [wp]:
  "\<lbrace>separate_state\<rbrace> as_user t f \<lbrace>\<lambda>_. separate_state\<rbrace>" by (wp separate_state_pres')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> as_user t f \<lbrace>\<lambda>_. separate_state\<rbrace>
theory Syscall_S

lemma activate_thread_separate_state [wp]:
  "\<lbrace>separate_state\<rbrace> activate_thread \<lbrace>\<lambda>_. separate_state\<rbrace>" unfolding activate_thread_def by (wp separate_state_pres' | wpc | simp add: arch_activate_idle_thread_def |  strengthen imp_consequent)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> activate_thread \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. separate_state\<rbrace>
theory Syscall_S

lemma schedule_separate_state [wp]:
  "\<lbrace>separate_state\<rbrace> schedule :: (unit,unit) s_monad \<lbrace>\<lambda>_. separate_state\<rbrace>" unfolding schedule_def switch_to_thread_def arch_switch_to_thread_def
            switch_to_idle_thread_def arch_switch_to_idle_thread_def allActiveTCBs_def by (wpsimp wp: select_inv separate_state_pres'
             simp: arch_activate_idle_thread_def |
      strengthen imp_consequent)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> schedule \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> do cur <- gets cur_thread;
threads <- do state <- get;
return {x. getActiveTCB x state \<noteq> None}
od;
thread <- select threads;
if thread = cur then return () \<sqinter> do state <- get;
assert (get_tcb thread state \<noteq> None);
do set_vm_root thread;
do_machine_op $ clearExMonitor
od;
do_extended_op (tcb_sched_action tcb_sched_dequeue thread);
modify (cur_thread_update (\<lambda>_. thread))
od else do state <- get;
assert (get_tcb thread state \<noteq> None);
do set_vm_root thread;
do_machine_op $ clearExMonitor
od;
do_extended_op (tcb_sched_action tcb_sched_dequeue thread);
modify (cur_thread_update (\<lambda>_. thread))
od
od \<sqinter> do cur <- gets cur_thread;
idl <- gets idle_thread;
if idl = cur then return () \<sqinter> do thread <- gets idle_thread;
gets idle_thread >>= set_vm_root;
modify (cur_thread_update (\<lambda>_. thread))
od else do thread <- gets idle_thread;
gets idle_thread >>= set_vm_root;
modify (cur_thread_update (\<lambda>_. thread))
od
od \<lbrace>\<lambda>_. separate_state\<rbrace>
theory Syscall_S

lemma set_message_info_sep_pres [wp]:
      "\<lbrace>\<lambda>s. P (typ_at t p s) (caps_of_state s)\<rbrace>
      set_message_info a b
      \<lbrace>\<lambda>_ s. P (typ_at t p s) (caps_of_state s)\<rbrace>" apply (rule hoare_pre) apply (wp | wpc | wps | simp )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at t p s) (caps_of_state s)\<rbrace> set_message_info a b \<lbrace>\<lambda>_ s. P (typ_at t p s) (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> set_message_info a b \<lbrace>\<lambda>_ s. P (typ_at t p s) (caps_of_state s)\<rbrace>
 2. \<And>s. P (typ_at t p s) (caps_of_state s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma dmo_separate_state [wp]:
  "\<lbrace>separate_state\<rbrace> do_machine_op f \<lbrace>\<lambda>_. separate_state\<rbrace>" by (rule separate_state_pres, rule hoare_pre, wps, wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> do_machine_op f \<lbrace>\<lambda>_. separate_state\<rbrace>
theory Syscall_S

lemma handle_interrupt_separate_state [wp]:
  "\<lbrace>separate_state\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. separate_state\<rbrace>" unfolding handle_interrupt_def apply (rule hoare_pre) apply (wp | wpc | wps | simp add: handle_reserved_irq_def arch_mask_irq_signal_def
         | strengthen imp_consequent)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> if maxIRQ < irq then do_machine_op $ do maskInterrupt True irq;
ackInterrupt irq
od else do st <- get_irq_state irq;
case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op $ ackInterrupt irq
od \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if maxIRQ < irq then do_machine_op $ do maskInterrupt True irq;
ackInterrupt irq
od else do st <- get_irq_state irq;
case st of IRQInactive \<Rightarrow> fail | IRQSignal \<Rightarrow> do slot <- get_irq_slot irq;
cap <- get_cap slot;
when (is_ntfn_cap cap \<and> AllowSend \<in> cap_rights cap) $ send_signal (obj_ref_of cap) (cap_ep_badge cap);
arch_mask_irq_signal irq
od | IRQTimer \<Rightarrow> do do_extended_op timer_tick;
do_machine_op resetTimer
od | IRQReserved \<Rightarrow> handle_reserved_irq irq;
do_machine_op $ ackInterrupt irq
od \<lbrace>\<lambda>_. separate_state\<rbrace>
 2. \<And>s. separate_state s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Syscall_S

lemma decode_invocation_separate_state [wp]:
  "\<lbrace> separate_state \<rbrace>
  Decode_SA.decode_invocation param_a param_b param_c param_d param_e param_f
  \<lbrace> \<lambda>_. separate_state \<rbrace>" unfolding decode_invocation_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> Decode_SA.decode_invocation param_a param_b param_c param_d param_e param_f \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state\<rbrace> case param_e of NotificationCap ptr badge rights \<Rightarrow> if AllowSend \<in> rights then returnOk $ InvokeNotification ptr badge else throwError $ InvalidCapability 0 | _ \<Rightarrow> throwError $ InvalidCapability 0 \<lbrace>\<lambda>_. separate_state\<rbrace>
theory Syscall_S

lemma separate_state_machine_state:
  "separate_state (s\<lparr>machine_state := ms\<rparr>) = separate_state s" unfolding separate_state_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. separate_state (s\<lparr>machine_state := ms\<rparr>) = separate_state s proof (prove)
goal (1 subgoal):
 1. (\<forall>p. tcb_at p (s\<lparr>machine_state := ms\<rparr>) \<longrightarrow> separate_tcb p (caps_of_state (s\<lparr>machine_state := ms\<rparr>))) = (\<forall>p. tcb_at p s \<longrightarrow> separate_tcb p (caps_of_state s))
theory Syscall_S

lemma call_kernel_separate_state:
  "\<lbrace>separate_state and cur_tcb and valid_objs\<rbrace> Syscall_A.call_kernel ev :: (unit,unit) s_monad \<lbrace>\<lambda>_. separate_state\<rbrace>" apply (rule hoare_pre) apply (rule bisim_valid) apply (rule call_kernel_bisim) apply (simp add: call_kernel_def) apply (wp | wpc | wps | simp | strengthen imp_consequent)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state and cur_tcb and valid_objs\<rbrace> Syscall_A.call_kernel ev \<lbrace>\<lambda>_. separate_state\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> Syscall_A.call_kernel ev \<lbrace>\<lambda>_. separate_state\<rbrace>
 2. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. bisim (=) ?P3 ?P'3 ?a3 (Syscall_A.call_kernel ev)
 2. \<lbrace>?Q3\<rbrace> ?a3 \<lbrace>\<lambda>_. separate_state\<rbrace>
 3. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> (?P3 and ?P'3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> Syscall_SA.call_kernel ev \<lbrace>\<lambda>_. separate_state\<rbrace>
 2. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ((\<lambda>_. True) and (separate_state and cur_tcb and valid_objs) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> do y <- Syscall_SA.handle_event ev <handle> (\<lambda>_. liftE (do irq <- do_machine_op (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handle_interrupt (the irq))
od));
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_. separate_state\<rbrace>
 2. \<And>s. (separate_state and cur_tcb and valid_objs) s \<Longrightarrow> ((\<lambda>_. True) and (separate_state and cur_tcb and valid_objs) and ?Q3) s proof (prove)
goal:
No subgoals!
theory TailrecPre

lemma tailrec_steps:
  "g x \<Longrightarrow> tailrec f1 f2 g x = tailrec f1 f2 g (f1 x)"
  "\<not> g x \<Longrightarrow> tailrec f1 f2 g x = f2 x" by (simp_all add: tailrec.simps cong: if_weak_cong split del: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (g x \<Longrightarrow> tailrec f1 f2 g x = tailrec f1 f2 g (f1 x)) &&& (\<not> g x \<Longrightarrow> tailrec f1 f2 g x = f2 x)
theory TailrecPre

lemma tailrec_pre_lemmata:
  "g x \<Longrightarrow> tailrec_pre f1 g p (x::'a) = (p x \<and> tailrec_pre f1 g p (f1 x))"
  "\<not> g x \<Longrightarrow> tailrec_pre f1 g p (x::'a) = p x" by (metis tailrec_pre_lemma)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (g x \<Longrightarrow> tailrec_pre f1 g p x = (p x \<and> tailrec_pre f1 g p (f1 x))) &&& (\<not> g x \<Longrightarrow> tailrec_pre f1 g p x = p x)
theory TailrecPre

theorem short_tailrec_thm:
  "\<forall>f x. short_tailrec f x = (if isLeft (fst (f x))
     then short_tailrec f (theLeft (fst (f x)))
     else theRight (fst (f x))) \<and>
   (short_tailrec_pre f x = (snd (f x)
     \<and> (isLeft (fst (f x)) \<longrightarrow> short_tailrec_pre f (theLeft (fst (f x))))))" apply (clarsimp simp add: short_tailrec_pre_def short_tailrec_def) apply (simp add: tailrec_pre_lemmata tailrec_steps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>f x. short_tailrec f x = (if isLeft (fst (f x)) then short_tailrec f (theLeft (fst (f x))) else theRight (fst (f x))) \<and> short_tailrec_pre f x = (snd (f x) \<and> (isLeft (fst (f x)) \<longrightarrow> short_tailrec_pre f (theLeft (fst (f x))))) proof (prove)
goal (1 subgoal):
 1. \<And>f x. (isLeft (fst (f x)) \<longrightarrow> tailrec (theLeft \<circ> fst \<circ> f) (theRight \<circ> fst \<circ> f) (isLeft \<circ> fst \<circ> f) x = tailrec (theLeft \<circ> fst \<circ> f) (theRight \<circ> fst \<circ> f) (isLeft \<circ> fst \<circ> f) (theLeft (fst (f x))) \<and> tailrec_pre (theLeft \<circ> fst \<circ> f) (isLeft \<circ> fst \<circ> f) (snd \<circ> f) x = (snd (f x) \<and> tailrec_pre (theLeft \<circ> fst \<circ> f) (isLeft \<circ> fst \<circ> f) (snd \<circ> f) (theLeft (fst (f x))))) \<and> (isRight (fst (f x)) \<longrightarrow> tailrec (theLeft \<circ> fst \<circ> f) (theRight \<circ> fst \<circ> f) (isLeft \<circ> fst \<circ> f) x = theRight (fst (f x)) \<and> tailrec_pre (theLeft \<circ> fst \<circ> f) (isLeft \<circ> fst \<circ> f) (snd \<circ> f) x = snd (f x)) proof (prove)
goal:
No subgoals!