theory Ipc_C

lemma ntfn_set_active_ccorres:
  "ccorres dc xfdc (invs' and ko_at' ntfn ntfnptr
                          and (\<lambda>_. \<not> isWaitingNtfn (ntfnObj ntfn)))
     (UNIV \<inter> {s. ntfnPtr_' s = Ptr ntfnptr} \<inter> {s. badge_' s = badge}) hs
     (setNotification ntfnptr
          (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn))
     (Call ntfn_set_active_'proc)" apply (rule ccorres_gen_asm) apply (cinit lift: ntfnPtr_' badge_') apply (simp only: setNotification_def) apply (rule_tac P="ko_at' ntfn ntfnptr and invs'"
            in ccorres_from_vcg[where P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (rule cmap_relation_ko_atE [OF cmap_relation_ntfn], assumption+) apply (clarsimp simp: typ_heap_simps) apply (rule bexI[OF _ setObject_eq], simp_all) apply (clarsimp simp: typ_heap_simps' rf_sr_def cstate_relation_def Let_def
                          cpspace_relation_def update_ntfn_map_tos
                          carch_state_relation_def cmachine_state_relation_def) apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) apply (simp add: cnotification_relation_def Let_def NtfnState_Active_def
                      isWaitingNtfn_def mask_def
               split: Structures_H.ntfn.split_asm) apply (simp add: objBits_simps')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and ko_at' ntfn ntfnptr and (\<lambda>_. \<not> isWaitingNtfn (ntfnObj ntfn))) (UNIV \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>) hs (setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn)) (Call ntfn_set_active_'proc) proof (prove)
goal (1 subgoal):
 1. \<not> isWaitingNtfn (ntfnObj ntfn) \<Longrightarrow> ccorres dc xfdc (invs' and ko_at' ntfn ntfnptr) (UNIV \<inter> \<lbrace>\<acute>ntfnPtr = ntfn_Ptr ntfnptr\<rbrace> \<inter> \<lbrace>\<acute>badge = badge\<rbrace>) hs (setNotification ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn)) (Call ntfn_set_active_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>badgea ntfnPtr. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); badgea = badge; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q110 badgea ntfnPtr) (?Q'110 badgea ntfnPtr) (SKIP # hs) (setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn)) (CALL notification_ptr_set_state_'proc(ntfnPtr,SCAST(32 signed \<rightarrow> 32) NtfnState_Active);;
CALL notification_ptr_set_ntfnMsgIdentifier_'proc(ntfnPtr,UCAST(32 \<rightarrow> 32) badgea))
 2. \<And>badgea ntfnPtr s s'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); badgea = badge; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and ko_at' ntfn ntfnptr) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q110 badgea ntfnPtr s \<and> s' \<in> ?Q'110 badgea ntfnPtr proof (prove)
goal (2 subgoals):
 1. \<And>badgea ntfnPtr. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); badgea = badge; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q110 badge (ntfn_Ptr ntfnptr)) (?Q'110 badge (ntfn_Ptr ntfnptr)) (SKIP # hs) (setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn)) (CALL notification_ptr_set_state_'proc(ntfn_Ptr ntfnptr,SCAST(32 signed \<rightarrow> 32) NtfnState_Active);;
CALL notification_ptr_set_ntfnMsgIdentifier_'proc(ntfn_Ptr ntfnptr,UCAST(32 \<rightarrow> 32) badge))
 2. \<And>badgea ntfnPtr s s'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); badgea = badge; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and ko_at' ntfn ntfnptr) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q110 badgea ntfnPtr s \<and> s' \<in> ?Q'110 badgea ntfnPtr proof (prove)
goal (2 subgoals):
 1. \<And>badgea ntfnPtr. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); badgea = badge; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (ko_at' ntfn ntfnptr and invs') \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} CALL notification_ptr_set_state_'proc(ntfn_Ptr ntfnptr,SCAST(32 signed \<rightarrow> 32) NtfnState_Active);;
CALL notification_ptr_set_ntfnMsgIdentifier_'proc(ntfn_Ptr ntfnptr,UCAST(32 \<rightarrow> 32) badge) {s. \<exists>(rv, \<sigma>')\<in>fst (setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>badgea ntfnPtr s s'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); badgea = badge; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and ko_at' ntfn ntfnptr) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (ko_at' ntfn ntfnptr and invs') s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>badgea ntfnPtr \<sigma>. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); badgea = badge; ntfnPtr = ntfn_Ptr ntfnptr\<rbrakk> \<Longrightarrow> {s. (ko_at' ntfn ntfnptr and invs') \<sigma> \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. s \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> (\<forall>t. (\<exists>notification. notification_lift notification = notification_lift (the (cslift s (ntfn_Ptr ntfnptr)))\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals s))) \<longrightarrow> t \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> (\<forall>ta. (\<exists>notification. notification_lift notification = notification_lift (the (cslift t (ntfn_Ptr ntfnptr)))\<lparr>ntfnMsgIdentifier_CL := UCAST(32 \<rightarrow> 32) badge && mask 32\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals t))) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn) \<sigma>). (\<sigma>', s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>) \<in> rf_sr \<and> dc rv (xfdc (s\<lparr>globals := globals s\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>)))))}
 2. \<And>badgea ntfnPtr s s'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); badgea = badge; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and ko_at' ntfn ntfnptr) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (ko_at' ntfn ntfnptr and invs') s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> (\<forall>t. (\<exists>notification. notification_lift notification = notification_lift (the (cslift x (ntfn_Ptr ntfnptr)))\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))) \<longrightarrow> t \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> (\<forall>ta. (\<exists>notification. notification_lift notification = notification_lift (the (cslift t (ntfn_Ptr ntfnptr)))\<lparr>ntfnMsgIdentifier_CL := badge\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals t))) \<longrightarrow> (\<exists>xa\<in>fst (setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>) \<in> rf_sr)))
 2. \<And>badgea ntfnPtr s s'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); badgea = badge; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and ko_at' ntfn ntfnptr) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (ko_at' ntfn ntfnptr and invs') s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x ko'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> (\<forall>t. (\<exists>notification. notification_lift notification = notification_lift (the (cslift x (ntfn_Ptr ntfnptr)))\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))) \<longrightarrow> t \<Turnstile>\<^sub>c ntfn_Ptr ntfnptr \<and> (\<forall>ta. (\<exists>notification. notification_lift notification = notification_lift (the (cslift t (ntfn_Ptr ntfnptr)))\<lparr>ntfnMsgIdentifier_CL := badge\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals t))) \<longrightarrow> (\<exists>xa\<in>fst (setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>) \<in> rf_sr)))
 2. \<And>badgea ntfnPtr s s'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); badgea = badge; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and ko_at' ntfn ntfnptr) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (ko_at' ntfn ntfnptr and invs') s \<and> s' \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x ko' t notification ta notificationa. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (setObject ntfnptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>badgea ntfnPtr s s'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); badgea = badge; ntfnPtr = ntfn_Ptr ntfnptr; (s, s') \<in> rf_sr; (invs' and ko_at' ntfn ntfnptr) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (ko_at' ntfn ntfnptr and invs') s \<and> s' \<in> UNIV proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x ko' t notification ta notificationa. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksPSpace := (ksPSpace \<sigma>)(ntfnptr \<mapsto> KONotification (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn))\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>\<sigma> x ko' t notification ta notificationa v. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 3. \<And>\<sigma> x ko' t notification ta notificationa v v'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rbrakk> \<Longrightarrow> objBits v = objBits v' proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x ko' t notification ta notificationa. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cmap_relation (map_to_ntfns ((ksPSpace \<sigma>)(ntfnptr \<mapsto> KONotification (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn)))) ((cslift x)(ntfn_Ptr ntfnptr \<mapsto> notificationa)) ntfn_Ptr (cnotification_relation (cslift x))
 2. \<And>\<sigma> x ko' t notification ta notificationa v. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 3. \<And>\<sigma> x ko' t notification ta notificationa v v'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rbrakk> \<Longrightarrow> objBits v = objBits v' proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> x ko' t notification ta notificationa. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cnotification_relation (cslift x) (ntfnObj_update (\<lambda>_. Structures_H.ntfn.ActiveNtfn badge) ntfn) notificationa
 2. \<And>\<sigma> x ko' t notification ta notificationa. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cslift x|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub> = cslift x|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub>
 3. \<And>\<sigma> x ko' t notification ta notificationa v. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 4. \<And>\<sigma> x ko' t notification ta notificationa v v'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rbrakk> \<Longrightarrow> objBits v = objBits v' proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma> x ko' t notification ta notificationa. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x))); cmap_relation (ctes_of \<sigma>) (cslift x) cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace \<sigma>)) (cslift x) tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace \<sigma>)) (cslift x) ep_Ptr (cendpoint_relation (cslift x)); cmap_relation (map_to_ntfns (ksPSpace \<sigma>)) (cslift x) ntfn_Ptr (cnotification_relation (cslift x)); cmap_relation (map_to_pdes (ksPSpace \<sigma>)) (cslift x) pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace \<sigma>)) (cslift x) pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace \<sigma>)) (cslift x) ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>))) (cslift x) PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace \<sigma>)) (c_h_t_valid x) pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace \<sigma>)) (c_h_t_valid x) pt_Ptr; cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (globals x)); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> cslift x|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub> = cslift x|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub>
 2. \<And>\<sigma> x ko' t notification ta notificationa v. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rbrakk> \<Longrightarrow> 1 < 2 ^ objBits v
 3. \<And>\<sigma> x ko' t notification ta notificationa v v'. \<lbrakk>\<not> isWaitingNtfn (ntfnObj ntfn); ko_at' ntfn ntfnptr \<sigma>; invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; cslift x (ntfn_Ptr ntfnptr) = Some ko'; cnotification_relation (cslift x) ntfn ko'; notification_lift notification = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)); notification_lift notificationa = notification_lift ko'\<lparr>notification_CL.state_CL := SCAST(32 signed \<rightarrow> 32) NtfnState_Active && mask 2, ntfnMsgIdentifier_CL := badge\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notificationa) (hrs_mem_update (heap_update (ntfn_Ptr ntfnptr) notification) (t_hrs_' (globals x)))\<rbrakk> \<Longrightarrow> objBits v = objBits v' proof (prove)
goal:
No subgoals!