kings-crown/FVELER_Isabelle huggingface dataset:
theory IsolatedThreadAction

lemma isolate_thread_actions_tcbs_at:
  assumes f: "\<And>x. \<lbrace>tcb_at' (idx x)\<rbrace> f \<lbrace>\<lambda>rv. tcb_at' (idx x)\<rbrace>" shows
  "\<lbrace>\<lambda>s. \<forall>x. tcb_at' (idx x) s\<rbrace>
       isolate_thread_actions idx f f' f'' \<lbrace>\<lambda>p s. \<forall>x. tcb_at' (idx x) s\<rbrace>" apply (simp add: isolate_thread_actions_def split_def) apply wp apply clarsimp apply (simp add: obj_at_partial_overwrite_If use_valid[OF _ f]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. tcb_at' (idx x) s\<rbrace> isolate_thread_actions idx f f' f'' \<lbrace>\<lambda>p s. \<forall>x. tcb_at' (idx x) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. tcb_at' (idx x) s\<rbrace> do s <- gets (ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)));
tcbs <- gets (\<lambda>s. get_tcb_state_regs \<circ> ksPSpace s \<circ> idx);
sa <- getSchedulerAction;
p <- select_f (f s);
y <- modify (\<lambda>s. ksPSpace_update (partial_overwrite idx (f' tcbs)) (snd p\<lparr>ksSchedulerAction := f'' sa\<rparr>));
return (fst p)
od \<lbrace>\<lambda>p s. \<forall>x. tcb_at' (idx x) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>x. tcb_at' (idx x) s \<Longrightarrow> \<forall>x\<in>fst (f ((ksSchedulerAction_update (\<lambda>_. ResumeCurrentThread) \<circ> ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined))) s)). \<forall>xa. tcb_at' (idx xa) (ksPSpace_update (partial_overwrite idx (f' (get_tcb_state_regs \<circ> ksPSpace s \<circ> idx))) (snd x\<lparr>ksSchedulerAction := f'' (ksSchedulerAction s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>\<forall>x. tcb_at' (idx x) s; (a, b) \<in> fst (f (ksPSpace_update (partial_overwrite idx (\<lambda>y. undefined)) s\<lparr>ksSchedulerAction := ResumeCurrentThread\<rparr>))\<rbrakk> \<Longrightarrow> tcb_at' (idx x) (ksPSpace_update (partial_overwrite idx (f' (\<lambda>a. get_tcb_state_regs (ksPSpace s (idx a))))) (b\<lparr>ksSchedulerAction := f'' (ksSchedulerAction s)\<rparr>)) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma tcb_at_KOTCB_upd:
  "tcb_at' (idx x) s \<Longrightarrow>
   tcb_at' p (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB tcb)) s)
        = tcb_at' p s" apply (clarsimp simp: obj_at'_def projectKOs objBits_simps
                 split: if_split) apply (fastforce simp add: ps_clear_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at' (idx x) s \<Longrightarrow> tcb_at' p (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB tcb)) s) = tcb_at' p s proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s (idx x) = Some (KOTCB obj); is_aligned (idx x) tcbBlockSizeBits; ps_clear (idx x) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (p = idx x \<longrightarrow> ps_clear (idx x) tcbBlockSizeBits (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB tcb)) s)) \<and> (p \<noteq> idx x \<longrightarrow> (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj) \<and> ps_clear p (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) (ksPSpace_update (\<lambda>ps. ps(idx x \<mapsto> KOTCB tcb)) s)) = (\<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj) \<and> ps_clear p (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s)) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma setSchedulerAction_isolate:
  "inj idx \<Longrightarrow>
   monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s)
        (setSchedulerAction sa)
        (isolate_thread_actions idx (return ()) id (\<lambda>_. sa))" apply (clarsimp simp: monadic_rewrite_def liftM_def bind_assoc
                        isolate_thread_actions_def select_f_returns
                        exec_gets getSchedulerAction_def o_def
                        ksPSpace_update_partial_id setSchedulerAction_def) apply (simp add: simpler_modify_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj idx \<Longrightarrow> monadic_rewrite False True (\<lambda>s. \<forall>x. tcb_at' (idx x) s) (setSchedulerAction sa) (isolate_thread_actions idx (return ()) id (\<lambda>_. sa)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>inj idx; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> modify (ksSchedulerAction_update (\<lambda>_. sa)) s = modify (\<lambda>sb. s\<lparr>ksSchedulerAction := sa\<rparr>) s proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma updateMDB_isolatable:
  "thread_actions_isolatable idx (updateMDB slot f)" apply (simp add: updateMDB_def thread_actions_isolatable_return
            split: if_split) apply (intro impI thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
               getCTE_isolatable setCTE_isolatable,
           (wp | simp)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (updateMDB slot f) proof (prove)
goal (1 subgoal):
 1. slot \<noteq> 0 \<longrightarrow> thread_actions_isolatable idx (do cte <- getCTE slot;
setCTE slot (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od) proof (prove)
goal:
No subgoals!
theory IsolatedThreadAction

lemma emptySlot_isolatable:
  "thread_actions_isolatable idx (emptySlot slot NullCap)" apply (simp add: emptySlot_def updateCap_def case_Null_If Retype_H.postCapDeletion_def
             cong: if_cong) apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
               clearUntypedFreeIndex_isolatable
               thread_actions_isolatable_if
               getCTE_isolatable setCTE_isolatable
               thread_actions_isolatable_return
               updateMDB_isolatable,
           (wp | simp)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (emptySlot slot capability.NullCap) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (do y <- clearUntypedFreeIndex slot;
newCTE <- getCTE slot;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- do cte <- getCTE slot;
setCTE slot (cteCap_update (\<lambda>_. capability.NullCap) cte)
od;
updateMDB slot (const nullMDBNode)
od
od) proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma replyFromKernel_success_empty:
  "replyFromKernel thread (0, []) = replyFromKernel_success_empty thread" unfolding replyFromKernel_def replyFromKernel_success_empty_def by (simp add: setMRs_Nil submonad_asUser.fn_stateAssert)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replyFromKernel thread (0, []) = replyFromKernel_success_empty thread proof (prove)
goal (1 subgoal):
 1. (case (0, []) of (resultLabel, resultData) \<Rightarrow> do destIPCBuffer <- lookupIPCBuffer True thread;
asUser thread $ setRegister Notification_H.badgeRegister 0;
len <- setMRs thread destIPCBuffer resultData;
return (Types_H.message_info.MI len 0 0 resultLabel) >>= setMessageInfo thread
od) = do lookupIPCBuffer True thread;
asUser thread $ setRegister Notification_H.badgeRegister 0;
setMessageInfo thread $ Types_H.message_info.MI 0 0 0 0
od
theory Ipc_C

lemma asUser_ntfn_at[wp]:
  "\<lbrace>ko_at' (ntfn :: Structures_H.notification) p\<rbrace>
    asUser tptr f \<lbrace>\<lambda>_. ko_at' ntfn p\<rbrace>" apply (simp add: asUser_def split_def) apply (wp threadSet_obj_at'_nontcb hoare_drop_imps | simp | rule subset_refl)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at' ntfn p\<rbrace> asUser tptr f \<lbrace>\<lambda>_. ko_at' ntfn p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at' ntfn p\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) tptr;
p <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) tptr;
return (fst p)
od \<lbrace>\<lambda>_. ko_at' ntfn p\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma registers_less_maxlength:
  "length msgRegisters < msgMaxLength" by (simp add: msgRegisters_unfold msgMaxLength_unfold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length TCB_H.msgRegisters < msgMaxLength
theory Ipc_C

lemma asUser_comm:
  assumes neq: "a \<noteq> b"
  assumes efa: "empty_fail fa" and efb: "empty_fail fb"
  shows
  "\<And>ra rb. do
     ra \<leftarrow> asUser a fa;
     rb \<leftarrow> asUser b fb;
     c ra rb
   od = do
     rb \<leftarrow> asUser b fb;
     ra \<leftarrow> asUser a fa;
     c ra rb
   od" apply (rule submonad_comm' [OF submonad_asUser submonad_asUser]) apply (clarsimp simp: neq asUser_replace_def Let_def fun_upd_twist [OF neq]) apply (clarsimp simp: neq asUser_replace_def Let_def obj_at'_real_def
                           ko_wp_at'_def ps_clear_upd_None ps_clear_upd
                    split: option.split kernel_object.split) apply (clarsimp simp: neq[symmetric] asUser_replace_def Let_def
                          obj_at'_real_def ko_wp_at'_def ps_clear_upd_None
                          ps_clear_upd
                   split: option.split kernel_object.split) apply (rule efa efb)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ra rb. do ra <- asUser a fa;
asUser b fb >>= c ra
od = do rb <- asUser b fb;
ra <- asUser a fa;
c ra rb
od proof (prove)
goal (5 subgoals):
 1. \<And>ra rb s raa x'. asUser_replace a raa (asUser_replace b x' s) = asUser_replace b x' (asUser_replace a raa s)
 2. \<And>ra rb s raa. tcb_at' a (asUser_replace b raa s) = tcb_at' a s
 3. \<And>ra rb s raa. tcb_at' b (asUser_replace a raa s) = tcb_at' b s
 4. \<And>ra rb. empty_fail fa
 5. \<And>ra rb. empty_fail fb proof (prove)
goal (4 subgoals):
 1. \<And>ra rb s raa. tcb_at' a (asUser_replace b raa s) = tcb_at' a s
 2. \<And>ra rb s raa. tcb_at' b (asUser_replace a raa s) = tcb_at' b s
 3. \<And>ra rb. empty_fail fa
 4. \<And>ra rb. empty_fail fb proof (prove)
goal (3 subgoals):
 1. \<And>ra rb s raa. tcb_at' b (asUser_replace a raa s) = tcb_at' b s
 2. \<And>ra rb. empty_fail fa
 3. \<And>ra rb. empty_fail fb proof (prove)
goal (2 subgoals):
 1. \<And>ra rb. empty_fail fa
 2. \<And>ra rb. empty_fail fb proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma empty_fail_getSanitiseRegisterInfo[wp, simp]:
  "empty_fail (getSanitiseRegisterInfo t)" by (wpsimp simp: getSanitiseRegisterInfo_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (local.getSanitiseRegisterInfo t)
theory Ipc_C

lemma asUser_getRegister_getSanitiseRegisterInfo_comm:
  "do
     ra \<leftarrow> asUser a (getRegister r);
     rb \<leftarrow> getSanitiseRegisterInfo b;
     c ra rb
   od = do
     rb \<leftarrow> getSanitiseRegisterInfo b;
     ra \<leftarrow> asUser a (getRegister r);
     c ra rb
   od" by (rule bind_inv_inv_comm; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do ra <- asUser a (getRegister r);
local.getSanitiseRegisterInfo b >>= c ra
od = do rb <- local.getSanitiseRegisterInfo b;
ra <- asUser a (getRegister r);
c ra rb
od
theory Ipc_C

lemma asUser_mapMloadWordUser_getSanitiseRegisterInfo_comm:
  "do
     ra \<leftarrow> mapM loadWordUser xs;
     rb \<leftarrow> getSanitiseRegisterInfo b;
     c ra rb
   od = do
     rb \<leftarrow> getSanitiseRegisterInfo b;
     ra \<leftarrow> mapM loadWordUser xs;
     c ra rb
   od" by (rule bind_inv_inv_comm, auto; wp mapM_wp')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do ra <- mapM loadWordUser xs;
local.getSanitiseRegisterInfo b >>= c ra
od = do rb <- local.getSanitiseRegisterInfo b;
ra <- mapM loadWordUser xs;
c ra rb
od
theory Ipc_C

lemma asUser_getRegister_discarded:
  "(asUser t (getRegister r)) >>= (\<lambda>_. n) =
   stateAssert (tcb_at' t) [] >>= (\<lambda>_. n)" apply (rule ext) apply (clarsimp simp: submonad_asUser.fn_is_sm submonad_fn_def
                        submonad_asUser.args assert_def select_f_def
                        gets_def get_def modify_def put_def
                        getRegister_def bind_def split_def
                        return_def fail_def stateAssert_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- asUser t (getRegister r);
n
od = do _ <- stateAssert (tcb_at' t) [];
n
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do _ <- asUser t (getRegister r);
n
od) x = (do _ <- stateAssert (tcb_at' t) [];
n
od) x proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma loadWordUser_submonad_fn:
  "loadWordUser p = submonad_fn ksMachineState (ksMachineState_update \<circ> K)
                                (pointerInUserData p) (loadWord p)" by (simp add: loadWordUser_def submonad_doMachineOp.fn_is_sm submonad_fn_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. loadWordUser p = submonad_fn ksMachineState (ksMachineState_update \<circ> K) (pointerInUserData p) (loadWord p)
theory Ipc_C

lemma ccap_relation_ep_helpers:
  "\<lbrakk> ccap_relation cap cap'; cap_get_tag cap' = scast cap_endpoint_cap \<rbrakk>
        \<Longrightarrow> capCanSend_CL (cap_endpoint_cap_lift cap') = from_bool (capEPCanSend cap)
          \<and> capCanReceive_CL (cap_endpoint_cap_lift cap') = from_bool (capEPCanReceive cap)
          \<and> capEPPtr_CL (cap_endpoint_cap_lift cap') = capEPPtr cap
          \<and> capEPBadge_CL (cap_endpoint_cap_lift cap') = capEPBadge cap
          \<and> capCanGrant_CL (cap_endpoint_cap_lift cap') = from_bool (capEPCanGrant cap)
          \<and> capCanGrantReply_CL (cap_endpoint_cap_lift cap') = from_bool (capEPCanGrantReply cap)" by (clarsimp simp: cap_lift_endpoint_cap cap_to_H_simps
                     cap_endpoint_cap_lift_def word_size
              elim!: ccap_relationE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap\<rbrakk> \<Longrightarrow> capCanSend_CL (cap_endpoint_cap_lift cap') = from_bool (capEPCanSend cap) \<and> capCanReceive_CL (cap_endpoint_cap_lift cap') = from_bool (capEPCanReceive cap) \<and> capEPPtr_CL (cap_endpoint_cap_lift cap') = capEPPtr cap \<and> capEPBadge_CL (cap_endpoint_cap_lift cap') = capEPBadge cap \<and> capCanGrant_CL (cap_endpoint_cap_lift cap') = from_bool (capEPCanGrant cap) \<and> capCanGrantReply_CL (cap_endpoint_cap_lift cap') = from_bool (capEPCanGrantReply cap)
theory Ipc_C

lemma ccap_relation_reply_helpers:
  "\<lbrakk> ccap_relation cap cap'; cap_get_tag cap' = scast cap_reply_cap \<rbrakk>
        \<Longrightarrow> capReplyCanGrant_CL (cap_reply_cap_lift cap') = from_bool (capReplyCanGrant cap)
          \<and> capReplyMaster_CL (cap_reply_cap_lift cap') = from_bool (capReplyMaster cap)
          \<and> cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap')
              = ptr_val (tcb_ptr_to_ctcb_ptr (capTCBPtr cap))" by (clarsimp simp: cap_lift_reply_cap cap_to_H_simps
                     cap_reply_cap_lift_def word_size
              elim!: ccap_relationE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap cap'; cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_reply_cap\<rbrakk> \<Longrightarrow> capReplyCanGrant_CL (cap_reply_cap_lift cap') = from_bool (capReplyCanGrant cap) \<and> capReplyMaster_CL (cap_reply_cap_lift cap') = from_bool (capReplyMaster cap) \<and> cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap') = ptr_val (tcb_ptr_to_ctcb_ptr (capTCBPtr cap))
theory Ipc_C

lemma loadWordUser_discarded:
  "loadWordUser p >>= (\<lambda>_. n) =
   stateAssert (pointerInUserData p and K (p && mask 2 = 0)) [] >>= (\<lambda>_. n)" apply (rule ext) apply (clarsimp simp: loadWordUser_def loadWord_def bind_def assert_def
                        stateAssert_def split_def return_def fail_def
                        doMachineOp_def gets_def get_def select_f_def
                        modify_def put_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- loadWordUser p;
n
od = do _ <- stateAssert (pointerInUserData p and K (p && mask 2 = 0)) [];
n
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do _ <- loadWordUser p;
n
od) x = (do _ <- stateAssert (pointerInUserData p and K (p && mask 2 = 0)) [];
n
od) x proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma getSanitiseRegisterInfo_lookupIPCBuffer_comm:
  "do
     a \<leftarrow> lookupIPCBuffer x y;
     t \<leftarrow> getSanitiseRegisterInfo r;
     c a t
   od = do
     t \<leftarrow> getSanitiseRegisterInfo r;
     a \<leftarrow> lookupIPCBuffer x y;
     c a t
  od" by (rule bind_inv_inv_comm; wp?; auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do a <- lookupIPCBuffer x y;
TCB_H.getSanitiseRegisterInfo r >>= c a
od = do t <- TCB_H.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer x y;
c a t
od
theory Ipc_C

lemma getSanitiseRegisterInfo_moreMapM_comm:
  "do
     a \<leftarrow>
       case sb of None \<Rightarrow> return []
       | Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser;
     t \<leftarrow> getSanitiseRegisterInfo r;
     c a t
   od = do
     t \<leftarrow> getSanitiseRegisterInfo r;
     a \<leftarrow>
       case sb of None \<Rightarrow> return []
       | Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser;
     c a t
  od" apply (rule bind_inv_inv_comm) apply (rule hoare_pre, wpc; (wp mapM_wp')?) apply simp apply wp apply (auto split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do a <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser;
TCB_H.getSanitiseRegisterInfo r >>= c a
od = do t <- TCB_H.getSanitiseRegisterInfo r;
a <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser;
c a t
od proof (prove)
goal (4 subgoals):
 1. \<And>P. \<lbrace>P\<rbrace> case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>P. \<lbrace>P\<rbrace> TCB_H.getSanitiseRegisterInfo r \<lbrace>\<lambda>_. P\<rbrace>
 3. empty_fail (case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser)
 4. empty_fail (TCB_H.getSanitiseRegisterInfo r) proof (prove)
goal (4 subgoals):
 1. \<And>P s. P s \<Longrightarrow> (sb = None \<longrightarrow> P s) \<and> (\<forall>x. sb = Some x \<longrightarrow> P s)
 2. \<And>P. \<lbrace>P\<rbrace> TCB_H.getSanitiseRegisterInfo r \<lbrace>\<lambda>_. P\<rbrace>
 3. empty_fail (case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser)
 4. empty_fail (TCB_H.getSanitiseRegisterInfo r) proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>P\<rbrace> TCB_H.getSanitiseRegisterInfo r \<lbrace>\<lambda>_. P\<rbrace>
 2. empty_fail (case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser)
 3. empty_fail (TCB_H.getSanitiseRegisterInfo r) proof (prove)
goal (2 subgoals):
 1. empty_fail (case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (xs bufferPtr) >>= mapM loadWordUser)
 2. empty_fail (TCB_H.getSanitiseRegisterInfo r) proof (prove)
goal:
No subgoals!
theory Ipc_C

lemma no_fail_getSanitiseRegisterInfo[wp, simp]:
  "no_fail (tcb_at' r) (getSanitiseRegisterInfo r)" apply (simp add: getSanitiseRegisterInfo_def) by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at' r) (local.getSanitiseRegisterInfo r) proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at' r) (return False)
theory Ipc_C

lemma asUser_mapMloadWordUser_threadGet_comm:
  "do
     ra \<leftarrow> mapM loadWordUser xs;
     rb \<leftarrow> threadGet fb b;
     c ra rb
   od = do
     rb \<leftarrow> threadGet fb b;
     ra \<leftarrow> mapM loadWordUser xs;
     c ra rb
   od" by (rule bind_inv_inv_comm, auto; wp mapM_wp')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do ra <- mapM loadWordUser xs;
threadGet fb b >>= c ra
od = do rb <- threadGet fb b;
ra <- mapM loadWordUser xs;
c ra rb
od
theory Ipc_C

lemma messageInfoFromWord_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call messageInfoFromWord_'proc {t. seL4_MessageInfo_lift (ret__struct_seL4_MessageInfo_C_' t) =
            \<lparr>label_CL = (w_' s >> 12) && 0xFFFFF, capsUnwrapped_CL = (w_' s >> 9) && 7,
                 extraCaps_CL = (w_' s >> 7) && 3, length_CL = let v = w_' s && 0x7F in if v > msgMaxLength then msgMaxLength else v\<rparr>}" apply vcg apply (simp add: seL4_MessageInfo_lift_def Let_def msgMaxLength_def mask_def word_sle_def
                   word_sless_def seL4_MsgMaxLength_def
         split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call messageInfoFromWord_'proc \<lbrace>seL4_MessageInfo_lift \<acute>ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = (\<^bsup>s\<^esup>w >> 12) && 0xFFFFF, capsUnwrapped_CL = (\<^bsup>s\<^esup>w >> 9) && 7, extraCaps_CL = (\<^bsup>s\<^esup>w >> 7) && 3, length_CL = let v = \<^bsup>s\<^esup>w && 0x7F in if msgMaxLength < v then msgMaxLength else v\<rparr>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>w. \<forall>v. 0 <s 1 \<and> 0 \<le>s 0 \<and> (\<forall>ret__unsigned. ret__unsigned = length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (UCAST(32 \<rightarrow> 32) w)) v)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength < UCAST(32 \<rightarrow> 32) (length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (UCAST(32 \<rightarrow> 32) w)) v))) \<longrightarrow> (\<forall>ret__struct_seL4_MessageInfo_C. seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = seL4_MessageInfo_lift (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (UCAST(32 \<rightarrow> 32) w)) v)\<lparr>length_CL := SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength && mask 7\<rparr> \<longrightarrow> seL4_MessageInfo_lift (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (UCAST(32 \<rightarrow> 32) w)) v)\<lparr>length_CL := SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength && mask 7\<rparr> = \<lparr>label_CL = (w >> 12) && 0xFFFFF, capsUnwrapped_CL = (w >> 9) && 7, extraCaps_CL = (w >> 7) && 3, length_CL = let v = w && 0x7F in if msgMaxLength < v then msgMaxLength else v\<rparr>)) \<and> (\<not> SCAST(32 signed \<rightarrow> 32) seL4_MsgMaxLength < UCAST(32 \<rightarrow> 32) (length_CL (seL4_MessageInfo_lift (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (UCAST(32 \<rightarrow> 32) w)) v))) \<longrightarrow> seL4_MessageInfo_lift (seL4_MessageInfo_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (UCAST(32 \<rightarrow> 32) w)) v) = \<lparr>label_CL = (w >> 12) && 0xFFFFF, capsUnwrapped_CL = (w >> 9) && 7, extraCaps_CL = (w >> 7) && 3, length_CL = let v = w && 0x7F in if msgMaxLength < v then msgMaxLength else v\<rparr>)) proof (prove)
goal:
No subgoals!