kings-crown/FVELER_Isabelle huggingface dataset:
theory Move_C

lemma valid_cap_cte_at':
  "\<lbrakk>isCNodeCap cap; valid_cap' cap s'\<rbrakk>
   \<Longrightarrow> cte_at' (capCNodePtr cap + 2^cteSizeBits * (addr && mask (capCNodeBits cap))) s'" apply (clarsimp simp: isCap_simps valid_cap'_def) apply (rule real_cte_at') apply (erule spec) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isCNodeCap cap; valid_cap' cap s'\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (capCNodePtr cap + 2 ^ cteSizeBits * (addr && mask (capCNodeBits cap))) s' proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 v3. \<lbrakk>cap = capability.CNodeCap v0 v1 v2 v3; capAligned (capability.CNodeCap v0 v1 v2 v3); 0 < v1; v1 + v3 \<le> word_bits; v2 && mask v3 = v2; \<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask v1)) s'\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (v0 + 2 ^ cteSizeBits * (addr && mask v1)) s' proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 v3. \<lbrakk>cap = capability.CNodeCap v0 v1 v2 v3; capAligned (capability.CNodeCap v0 v1 v2 v3); 0 < v1; v1 + v3 \<le> word_bits; v2 && mask v3 = v2; \<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask v1)) s'\<rbrakk> \<Longrightarrow> real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask v1)) s' proof (prove)
goal:
No subgoals!
theory Move_C

lemma cd_wp[wp]:
  "\<lbrace>\<lambda>s. P (ksCurDomain s) s\<rbrace> curDomain \<lbrace>P\<rbrace>" by (unfold curDomain_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s) s\<rbrace> curDomain \<lbrace>P\<rbrace>
theory Move_C

lemma empty_fail_getEndpoint:
  "empty_fail (getEndpoint ep)" unfolding getEndpoint_def by (auto intro: empty_fail_getObject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getEndpoint ep) proof (prove)
goal (1 subgoal):
 1. empty_fail (getObject ep)
theory Move_C

lemma ko_at_valid_ep':
  "\<lbrakk>ko_at' ep p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_ep' ep s" apply (erule obj_atE') apply (erule (1) valid_objsE') apply (simp add: projectKOs valid_obj'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ep p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_ep' ep s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>valid_objs' s; ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; obj = ep; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> valid_ep' ep s proof (prove)
goal (1 subgoal):
 1. \<And>ko obj. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); fst (projectKO ko s) = {(obj, s)}; obj = ep; ps_clear p (objBitsKO ko) s; valid_obj' ko s\<rbrakk> \<Longrightarrow> valid_ep' ep s proof (prove)
goal:
No subgoals!
theory Move_C

lemma cap_case_EndpointCap_NotificationCap:
  "(case cap of EndpointCap v0 v1 v2 v3 v4 v5 \<Rightarrow> f v0 v1 v2 v3 v4 v5
              | NotificationCap v0 v1 v2 v3  \<Rightarrow> g v0 v1 v2 v3
              | _ \<Rightarrow> h)
   = (if isEndpointCap cap
      then f (capEPPtr cap) (capEPBadge cap) (capEPCanSend cap) (capEPCanReceive cap)
             (capEPCanGrant cap) (capEPCanGrantReply cap)
      else if isNotificationCap cap
           then g (capNtfnPtr cap)  (capNtfnBadge cap) (capNtfnCanSend cap) (capNtfnCanReceive cap)
           else h)" by (simp add: isCap_simps
         split: capability.split split del: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.NotificationCap v0 v1 v2 v3 \<Rightarrow> g v0 v1 v2 v3 | capability.EndpointCap v0 v1 v2 v3 v4 v5 \<Rightarrow> f v0 v1 v2 v3 v4 v5 | _ \<Rightarrow> h) = (if isEndpointCap cap then f (capEPPtr cap) (capEPBadge cap) (capEPCanSend cap) (capEPCanReceive cap) (capEPCanGrant cap) (capEPCanGrantReply cap) else if isNotificationCap cap then g (capNtfnPtr cap) (capNtfnBadge cap) (capNtfnCanSend cap) (capNtfnCanReceive cap) else h)
theory Move_C

lemma asUser_obj_at':
  "\<lbrace> K(t\<noteq>t') and obj_at' P t' \<rbrace> asUser t f \<lbrace> \<lambda>_.  obj_at' (P::Structures_H.tcb \<Rightarrow> bool) t' \<rbrace>" including no_pre apply (simp add: asUser_def) apply wpsimp apply (case_tac "t=t'"; clarsimp) apply (rule hoare_drop_imps) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (t \<noteq> t') and obj_at' P t'\<rbrace> asUser t f \<lbrace>\<lambda>_. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (t \<noteq> t') and obj_at' P t'\<rbrace> asUser t f \<lbrace>\<lambda>_. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. t \<noteq> t') and obj_at' P t'\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
(a, uc') <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) t;
return a
od \<lbrace>\<lambda>_. obj_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. t \<noteq> t') and obj_at' P t'\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>uc s. \<forall>x\<in>fst (f uc). \<forall>xa xb. x = (xa, xb) \<longrightarrow> obj_at' (\<lambda>obj. (t = t' \<longrightarrow> P (tcbArch_update (\<lambda>_. atcbContextSet xb (tcbArch obj)) obj)) \<and> (t \<noteq> t' \<longrightarrow> P obj)) t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>uc s. (\<exists>a b. (a, b) \<in> fst (f uc)) \<longrightarrow> obj_at' P t' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>obj_at' P t'\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Move_C

lemma update_ep_map_to_ctes:
  fixes P :: "endpoint \<Rightarrow> bool"
  assumes at: "obj_at' P p s"
  shows     "map_to_ctes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = map_to_ctes (ksPSpace s)" using at by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI
    simp: projectKOs projectKO_opts_defs split: kernel_object.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_ctes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = ctes_of s proof (prove)
using this:
obj_at' P p s

goal (1 subgoal):
 1. map_to_ctes ((ksPSpace s)(p \<mapsto> KOEndpoint ko)) = ctes_of s
theory Move_C

lemma multiple_add_less_nat:
  "\<lbrakk> a < (c :: nat); x dvd a; x dvd c; b < x \<rbrakk>
   \<Longrightarrow> a + b < c" apply (subgoal_tac "b < c - a") apply simp apply (erule order_less_le_trans) apply (rule dvd_imp_le) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < c; x dvd a; x dvd c; b < x\<rbrakk> \<Longrightarrow> a + b < c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a < c; x dvd a; x dvd c; b < x; b < c - a\<rbrakk> \<Longrightarrow> a + b < c
 2. \<lbrakk>a < c; x dvd a; x dvd c; b < x\<rbrakk> \<Longrightarrow> b < c - a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < c; x dvd a; x dvd c; b < x\<rbrakk> \<Longrightarrow> b < c - a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < c; x dvd a; x dvd c\<rbrakk> \<Longrightarrow> x \<le> c - a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a < c; x dvd a; x dvd c\<rbrakk> \<Longrightarrow> x dvd c - a
 2. \<lbrakk>a < c; x dvd a; x dvd c\<rbrakk> \<Longrightarrow> 0 < c - a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < c; x dvd a; x dvd c\<rbrakk> \<Longrightarrow> 0 < c - a proof (prove)
goal:
No subgoals!
theory ArchMove_C

lemma ps_clear_is_aligned_ctes_None:
  assumes "ps_clear p tcbBlockSizeBits s"
      and "is_aligned p tcbBlockSizeBits"
  shows "ksPSpace s (p + 2*2^cteSizeBits) = None"
    and "ksPSpace s (p + 3*2^cteSizeBits) = None"
    and "ksPSpace s (p + 4*2^cteSizeBits) = None" by (auto intro: assms ps_clear_is_aligned_ksPSpace_None
            simp: objBits_defs mask_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksPSpace s (p + 2 * 2 ^ cteSizeBits) = None &&& ksPSpace s (p + 3 * 2 ^ cteSizeBits) = None &&& ksPSpace s (p + 4 * 2 ^ cteSizeBits) = None
theory ArchMove_C

lemma Arch_switchToThread_obj_at_pre:
  "\<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace>
   Arch.switchToThread t
   \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace>" apply (simp add: ARM_H.switchToThread_def) apply (wp doMachineOp_obj_at setVMRoot_obj_at hoare_drop_imps|wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (Not \<circ> tcbQueued) t\<rbrace> do y <- ARM_H.setVMRoot t;
doMachineOp ARM.clearExMonitor
od \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchMove_C

lemma asid_pool_at'_ko:
  "asid_pool_at' p s \<Longrightarrow> \<exists>pool. ko_at' (ASIDPool pool) p s" apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def projectKOs) apply (case_tac ko, auto) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object, auto)[1] apply (rename_tac asidpool) apply (case_tac asidpool, auto)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_pool_at' p s \<Longrightarrow> \<exists>pool. ko_at' (asidpool.ASIDPool pool) p s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>ksPSpace s p = Some ko; is_aligned p (objBitsKO ko); koTypeOf ko = ArchT ASIDPoolT; ps_clear p (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<exists>pool. ko = KOArch (KOASIDPool (asidpool.ASIDPool pool)) \<and> is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) \<and> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s proof (prove)
goal (1 subgoal):
 1. \<And>x8. \<lbrakk>ksPSpace s p = Some (KOArch x8); is_aligned p (objBitsKO (KOArch x8)); archTypeOf x8 = ASIDPoolT; ps_clear p (objBitsKO (KOArch x8)) s\<rbrakk> \<Longrightarrow> \<exists>pool. x8 = KOASIDPool (asidpool.ASIDPool pool) \<and> is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) \<and> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s proof (prove)
goal (1 subgoal):
 1. \<And>arch_kernel_object. \<lbrakk>ksPSpace s p = Some (KOArch arch_kernel_object); is_aligned p (objBitsKO (KOArch arch_kernel_object)); archTypeOf arch_kernel_object = ASIDPoolT; ps_clear p (objBitsKO (KOArch arch_kernel_object)) s\<rbrakk> \<Longrightarrow> \<exists>pool. arch_kernel_object = KOASIDPool (asidpool.ASIDPool pool) \<and> is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) \<and> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s proof (prove)
goal (1 subgoal):
 1. \<And>x1. \<lbrakk>ksPSpace s p = Some (KOArch (KOASIDPool x1)); is_aligned p (objBitsKO (KOArch (KOASIDPool x1))); ps_clear p (objBitsKO (KOArch (KOASIDPool x1))) s\<rbrakk> \<Longrightarrow> \<exists>pool. x1 = asidpool.ASIDPool pool \<and> is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) \<and> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s proof (prove)
goal (1 subgoal):
 1. \<And>asidpool. \<lbrakk>ksPSpace s p = Some (KOArch (KOASIDPool asidpool)); is_aligned p (objBitsKO (KOArch (KOASIDPool asidpool))); ps_clear p (objBitsKO (KOArch (KOASIDPool asidpool))) s\<rbrakk> \<Longrightarrow> \<exists>pool. asidpool = asidpool.ASIDPool pool \<and> is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) \<and> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s proof (prove)
goal:
No subgoals!
theory ArchMove_C

lemma empty_fail_findPDForASID[iff]:
  "empty_fail (findPDForASID asid)" unfolding findPDForASID_def checkPDAt_def by (wpsimp wp: empty_fail_getObject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (findPDForASID asid) proof (prove)
goal (1 subgoal):
 1. empty_fail (doE haskell_assertE (0 < asid) [];
haskell_assertE (asid \<le> snd asidRange) [];
asidTable <- withoutFailure $ gets (armKSASIDTable \<circ> ksArchState);
poolPtr <- returnOk (asidTable (asidHighBitsOf asid));
pool <- liftME (inv asidpool.ASIDPool) $ case poolPtr of None \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> withoutFailure $ getObject ptr;
pd <- returnOk (pool (asid && mask asidLowBits));
case pd of None \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> doE haskell_assertE (ptr \<noteq> 0) [];
withoutFailure $ stateAssert (page_directory_at' ptr) [];
returnOk ptr
odE
odE)
theory ArchMove_C

lemma empty_fail_findPDForASIDAssert[iff]:
  "empty_fail (findPDForASIDAssert asid)" unfolding findPDForASIDAssert_def checkPDAt_def checkPDUniqueToASID_def checkPDASIDMapMembership_def by (wpsimp wp: empty_fail_getObject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (findPDForASIDAssert asid) proof (prove)
goal (1 subgoal):
 1. empty_fail (do pd <- findPDForASID asid `~catchFailure~` const (haskell_fail []);
haskell_assert (pd && mask pdBits = 0) [];
stateAssert (page_directory_at' pd) [];
stateAssert (\<lambda>s. pd \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` (- set [asid]))) [];
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
swp haskell_assert [] $ case asidMap asid of None \<Rightarrow> True | Some (x, pd') \<Rightarrow> pd = pd';
return pd
od)
theory ArchMove_C

lemma mab_gt_2 [simp]:
  "2 \<le> msg_align_bits" by (simp add: msg_align_bits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 \<le> msg_align_bits
theory ArchMove_C

lemma vaddr_segment_nonsense6:
  "is_aligned (p :: word32) pdBits \<Longrightarrow>
   (p + (vaddr >> 20 << 2) && ~~ mask pdBits) = p" apply (rule is_aligned_add_helper[THEN conjunct2]) apply (erule is_aligned_weaken, simp) apply (simp add: pdBits_def pdeBits_def) apply (rule shiftl_less_t2n[where m=14 and n=2 and 'a=machine_word_len, simplified]) apply (rule shiftr_less_t2n'[where m=12 and n=20 and 'a=machine_word_len, simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned p pdBits \<Longrightarrow> p + (vaddr >> 20 << 2) && ~~ mask pdBits = p proof (prove)
goal (2 subgoals):
 1. is_aligned p pdBits \<Longrightarrow> is_aligned p pdBits
 2. is_aligned p pdBits \<Longrightarrow> vaddr >> 20 << 2 < 2 ^ pdBits proof (prove)
goal (1 subgoal):
 1. is_aligned p pdBits \<Longrightarrow> vaddr >> 20 << 2 < 2 ^ pdBits proof (prove)
goal (1 subgoal):
 1. is_aligned p 14 \<Longrightarrow> vaddr >> 20 << 2 < 0x4000 proof (prove)
goal (1 subgoal):
 1. is_aligned p 14 \<Longrightarrow> vaddr >> 20 < 0x1000 proof (prove)
goal:
No subgoals!
theory ArchMove_C

lemma valid_eq_wf_asid_pool'[simp]:
  "valid_asid_pool' pool = (\<lambda>s. wf_asid_pool' pool)" by (case_tac pool) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_pool' pool = (\<lambda>s. wf_asid_pool' pool)
theory ArchMove_C

lemma length_msgRegisters[simplified size_msgRegisters_def]:
  "length ARM_H.msgRegisters = size_msgRegisters" by (simp add: size_msgRegisters_pre_def ARM_H.msgRegisters_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length TCB_H.msgRegisters = size_msgRegisters
theory ArchMove_C

lemma empty_fail_loadWordUser[intro!, simp]:
  "empty_fail (loadWordUser x)" by (fastforce simp: loadWordUser_def ef_loadWord ef_dmo')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (loadWordUser x)
theory ArchMove_C

lemma empty_fail_getMRs[iff]:
  "empty_fail (getMRs t buf mi)" by (auto simp add: getMRs_def split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getMRs t buf mi)
theory ArchMove_C

lemma empty_fail_getReceiveSlots:
  "empty_fail (getReceiveSlots r rbuf)" proof - note
    empty_fail_resolveAddressBits[wp]
    empty_fail_rethrowFailure[wp]
    empty_fail_rethrowFailure[wp] show ?thesis unfolding getReceiveSlots_def loadCapTransfer_def lookupCap_def lookupCapAndSlot_def by (wpsimp simp: emptyOnFailure_def unifyFailure_def lookupSlotForThread_def
                   capTransferFromWords_def getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
                   lookupSlotForCNodeOp_def lookupErrorOnFailure_def rangeCheck_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getReceiveSlots r rbuf) proof (state)
goal (1 subgoal):
 1. empty_fail (getReceiveSlots r rbuf) proof (state)
this:
empty_fail (CSpace_H.resolveAddressBits ?cap ?cptr ?bits)
empty_fail ?f \<Longrightarrow> empty_fail (rethrowFailure ?fn ?f)
empty_fail ?f \<Longrightarrow> empty_fail (rethrowFailure ?fn ?f)

goal (1 subgoal):
 1. empty_fail (getReceiveSlots r rbuf) proof (prove)
goal (1 subgoal):
 1. empty_fail (getReceiveSlots r rbuf) proof (prove)
goal (1 subgoal):
 1. empty_fail (case rbuf of None \<Rightarrow> return [] | Some buffer \<Rightarrow> do ct <- do intSize <- return (fromIntegral wordSize);
offset <- return (msgMaxLength + msgMaxExtraCaps + 2);
capTransferFromWords (buffer + PPtr (offset * intSize))
od;
emptyOnFailure $ doE cptr <- returnOk (ctReceiveRoot ct);
cnode <- unifyFailure $ liftME fst $ doE slot <- lookupSlotForThread r cptr;
cap <- withoutFailure $ getSlotCap slot;
returnOk (cap, slot)
odE;
slot <- unifyFailure $ lookupTargetSlot cnode (ctReceiveIndex ct) (ctReceiveDepth ct);
cte <- withoutFailure $ getCTE slot;
unlessE (isNullCap $ cteCap cte) $ throw ();
returnOk [slot]
odE
od) proof (state)
this:
empty_fail (getReceiveSlots r rbuf)

goal:
No subgoals!
theory ArchMove_C

lemma user_getreg_rv:
  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>" apply (simp add: asUser_def split_def) apply (wp threadGet_wp) apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb) r)) t\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (getRegister r uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb) r)) t s \<Longrightarrow> \<forall>tcb. ko_at' tcb t s \<longrightarrow> (\<forall>x\<in>fst (getRegister r ((atcbContextGet \<circ> tcbArch) tcb)). P (fst x)) proof (prove)
goal:
No subgoals!
theory ArchMove_C

lemma addrFromPPtr_mask[simplified ARM.pageBitsForSize_simps]:
  "n \<le> pageBitsForSize ARMSuperSection
   \<Longrightarrow> addrFromPPtr ptr && mask n = ptr && mask n" apply (simp add: addrFromPPtr_def) apply (prop_tac "pptrBaseOffset AND mask n = 0") apply (rule mask_zero[OF is_aligned_weaken[OF pptrBaseOffset_aligned]], simp) apply (simp flip: mask_eqs(8)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> pageBitsForSize ARMSuperSection \<Longrightarrow> addrFromPPtr ptr && mask n = ptr && mask n proof (prove)
goal (1 subgoal):
 1. n \<le> 24 \<Longrightarrow> ptr - pptrBaseOffset && mask n = ptr && mask n proof (prove)
goal (2 subgoals):
 1. n \<le> 24 \<Longrightarrow> pptrBaseOffset && mask n = 0
 2. \<lbrakk>n \<le> 24; pptrBaseOffset && mask n = 0\<rbrakk> \<Longrightarrow> ptr - pptrBaseOffset && mask n = ptr && mask n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> 24; pptrBaseOffset && mask n = 0\<rbrakk> \<Longrightarrow> ptr - pptrBaseOffset && mask n = ptr && mask n proof (prove)
goal:
No subgoals!
theory ArchMove_C

lemma addrFromPPtr_mask_5:
  "addrFromPPtr ptr && mask 5 = ptr && mask 5" by (rule addrFromPPtr_mask[where n=5, simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. addrFromPPtr ptr && mask 5 = ptr && mask 5
theory Boolean_C

lemma true_and_1[simp]:
  "true && 1 = true"
  "signed true && 1 = signed true"
  "unsigned true && 1 = unsigned true" by (simp add: true_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. true && 1 = true &&& SCAST(32 signed \<rightarrow> 'a) true && 1 = SCAST(32 signed \<rightarrow> 'a) true &&& UCAST(32 signed \<rightarrow> 'b) true && 1 = UCAST(32 signed \<rightarrow> 'b) true
theory Boolean_C

lemma to_bool_true[simp]:
  "to_bool true"
  "to_bool (signed true)"
  "to_bool (unsigned true)" by (simp add: to_bool_def true_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bool true &&& to_bool (SCAST(32 signed \<rightarrow> 'a) true) &&& to_bool (UCAST(32 signed \<rightarrow> 'b) true)
theory Boolean_C

lemma true_eq_from_bool[simp]:
  "(true = from_bool P) = P"
  "(signed true = from_bool P) = P"
  "(unsigned true = from_bool P) = P" by (simp add: from_bool_def split: bool.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (true = from_bool P) = P &&& (SCAST(32 signed \<rightarrow> 'a) true = from_bool P) = P &&& (UCAST(32 signed \<rightarrow> 'b) true = from_bool P) = P
theory Boolean_C

lemma to_bool_false[simp]:
  "\<not> to_bool false"
  "\<not> to_bool (signed false)"
  "\<not> to_bool (unsigned false)" by (simp add: to_bool_def false_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> to_bool false &&& \<not> to_bool (SCAST(32 signed \<rightarrow> 'a) false) &&& \<not> to_bool (UCAST(32 signed \<rightarrow> 'b) false)
theory Boolean_C

lemma false_equals_simps[simp]:
  "false = 0 \<longleftrightarrow> True"
  "signed false = 0 \<longleftrightarrow> True"
  "unsigned false = 0 \<longleftrightarrow> True"
  "false = 1 \<longleftrightarrow> False"
  "signed false = 1 \<longleftrightarrow> False"
  "unsigned false = 1 \<longleftrightarrow> False" by (simp add: false_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((false = 0) = True &&& (signed false = (0::'a)) = True &&& (unsigned false = (0::'b)) = True) &&& (false = 1) = False &&& (signed false = (1::'c)) = False &&& (unsigned false = (1::'d)) = False
theory Boolean_C

lemma false_eq_from_bool[simp]:
  "(false = from_bool P) = (\<not> P)"
  "(signed false = from_bool P) = (\<not> P)"
  "(unsigned false = from_bool P) = (\<not> P)" by (simp add: from_bool_def split: bool.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (false = from_bool P) = (\<not> P) &&& (SCAST(32 signed \<rightarrow> 'a) false = from_bool P) = (\<not> P) &&& (UCAST(32 signed \<rightarrow> 'b) false = from_bool P) = (\<not> P)
theory Boolean_C

lemma from_bool_vals[simp]:
  "from_bool True = signed true"
  "from_bool False = signed false" by (simp add: from_bool_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. from_bool True = SCAST(32 signed \<rightarrow> 'a) true &&& from_bool False = SCAST(32 signed \<rightarrow> 'b) false
theory Boolean_C

lemma true_neq_false[simp]:
  "true \<noteq> false"
  "signed true \<noteq> signed false"
  "unsigned true \<noteq> unsigned false" by (simp add: true_def false_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. true \<noteq> false &&& signed true \<noteq> signed false &&& unsigned true \<noteq> unsigned false
theory Boolean_C

lemma to_bool_bf_mask1[simp]:
  "to_bool_bf (mask (Suc 0))" by (simp add: mask_def to_bool_bf_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bool_bf (mask (Suc 0))
theory Boolean_C

lemma to_bool_bf_0[simp]:
  "\<not>to_bool_bf 0" by (simp add: to_bool_bf_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> to_bool_bf 0
theory Boolean_C

lemma to_bool_bf_1[simp]:
  "to_bool_bf 1" by (simp add: to_bool_bf_def mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bool_bf 1
theory Boolean_C

lemma to_bool_bf_false[simp]:
  "\<not>to_bool_bf false" by (simp add: false_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> to_bool_bf false
theory Boolean_C

lemma to_bool_bf_true[simp]:
  "to_bool_bf true" by (simp add: true_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. to_bool_bf true