theory Fastpath_C

lemma cap_reply_cap_ptr_new_np_updateCap_ccorres:
  "ccorres dc xfdc
        (cte_at' ptr and tcb_at' thread)
        (UNIV \<inter> {s. cap_ptr_' s = cap_Ptr &(cte_Ptr ptr \<rightarrow> [''cap_C''])}
              \<inter> {s. capTCBPtr___unsigned_long_' s = ptr_val (tcb_ptr_to_ctcb_ptr thread)}
              \<inter> {s. capReplyMaster___unsigned_long_' s = from_bool m}
              \<inter> {s. capReplyCanGrant___unsigned_long_' s = from_bool canGrant}) []
     (updateCap ptr (ReplyCap thread m canGrant))
     (Call cap_reply_cap_ptr_new_np_'proc)" apply (rule ccorres_from_vcg, rule allI) apply (rule conseqPre, vcg) apply (clarsimp simp: cte_wp_at_ctes_of word_sle_def) apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+) apply (clarsimp simp: updateCap_def split_def typ_heap_simps'
                        word_sless_def word_sle_def) apply (erule(1) getCTE_setCTE_rf_sr, simp_all add: typ_heap_simps') apply (clarsimp simp: ccte_relation_eq_ccap_relation
                        ccap_relation_def c_valid_cap_def) apply (frule is_aligned_tcb_ptr_to_ctcb_ptr) apply (rule ssubst[OF cap_lift_reply_cap]) apply (simp add: cap_get_tag_def cap_reply_cap_def ctcb_size_bits_def
                    mask_def word_ao_dist
                    limited_and_simps
                    limited_and_simps1[OF lshift_limited_and, OF limited_and_from_bool]) apply (simp add: cap_to_H_simps word_ao_dist cl_valid_cap_def ctcb_size_bits_def
                   limited_and_simps cap_reply_cap_def
                   limited_and_simps1[OF lshift_limited_and, OF limited_and_from_bool]
                   shiftr_over_or_dist word_bw_assocs mask_def shiftl_shiftr3 word_size) apply (cases m ; clarsimp simp: true_def) apply (cases canGrant ; clarsimp simp: true_def false_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (cte_wp_at' (\<lambda>_. True) ptr and tcb_at' thread) (UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>capTCBPtr___unsigned_long = ptr_val (tcb_ptr_to_ctcb_ptr thread)\<rbrace> \<inter> \<lbrace>\<acute>capReplyMaster___unsigned_long = from_bool m\<rbrace> \<inter> \<lbrace>\<acute>capReplyCanGrant___unsigned_long = from_bool canGrant\<rbrace>) [] (updateCap ptr (capability.ReplyCap thread m canGrant)) (Call cap_reply_cap_ptr_new_np_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> {s. (cte_wp_at' (\<lambda>_. True) ptr and tcb_at' thread) \<sigma> \<and> s \<in> UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>capTCBPtr___unsigned_long = ptr_val (tcb_ptr_to_ctcb_ptr thread)\<rbrace> \<inter> \<lbrace>\<acute>capReplyMaster___unsigned_long = from_bool m\<rbrace> \<inter> \<lbrace>\<acute>capReplyCanGrant___unsigned_long = from_bool canGrant\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} Call cap_reply_cap_ptr_new_np_'proc {s. \<exists>(rv, \<sigma>')\<in>fst (updateCap ptr (capability.ReplyCap thread m canGrant) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. (cte_wp_at' (\<lambda>_. True) ptr and tcb_at' thread) \<sigma> \<and> s \<in> UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>capTCBPtr___unsigned_long = ptr_val (tcb_ptr_to_ctcb_ptr thread)\<rbrace> \<inter> \<lbrace>\<acute>capReplyMaster___unsigned_long = from_bool m\<rbrace> \<inter> \<lbrace>\<acute>capReplyCanGrant___unsigned_long = from_bool canGrant\<rbrace> \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. 0 <s 2 \<and> 0 \<le>s 0 \<and> s \<Turnstile>\<^sub>c cap_ptr_' s \<and> 0 \<le>s 5 \<and> 5 <s 0x20 \<and> 0 \<le>s 4 \<and> 4 <s 0x20 \<and> (\<exists>(rv, \<sigma>')\<in>fst (updateCap ptr (capability.ReplyCap thread m canGrant) \<sigma>). (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' s\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[2]) &(cap_ptr_' s\<rightarrow>[''words_C'']))) (unat 0) (UCAST(32 \<rightarrow> 32) (((capTCBPtr___unsigned_long_' s || (capReplyMaster___unsigned_long_' s << unat 4)) || (capReplyCanGrant___unsigned_long_' s << unat 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)))))) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' s\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[2]) &(cap_ptr_' s\<rightarrow>[''words_C'']))) (unat 0) (UCAST(32 \<rightarrow> 32) (((capTCBPtr___unsigned_long_' s || (capReplyMaster___unsigned_long_' s << unat 4)) || (capReplyCanGrant___unsigned_long_' s << unat 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)))))) s)))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte. \<lbrakk>ctes_of \<sigma> ptr = Some cte; tcb_at' thread \<sigma>; cap_ptr_' x = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']); capTCBPtr___unsigned_long_' x = ptr_val (tcb_ptr_to_ctcb_ptr thread); capReplyMaster___unsigned_long_' x = from_bool m; capReplyCanGrant___unsigned_long_' x = from_bool canGrant; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']) \<and> (\<exists>xa\<in>fst (updateCap ptr (capability.ReplyCap thread m canGrant) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C''])\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C''])\<rightarrow>[''words_C'']))) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap))))) x) \<in> rf_sr) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte y'. \<lbrakk>ctes_of \<sigma> ptr = Some cte; tcb_at' thread \<sigma>; cap_ptr_' x = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']); capTCBPtr___unsigned_long_' x = ptr_val (tcb_ptr_to_ctcb_ptr thread); capReplyMaster___unsigned_long_' x = from_bool m; capReplyCanGrant___unsigned_long_' x = from_bool canGrant; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte; ccte_relation cte y'; cslift x (cte_Ptr ptr) = Some y'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']) \<and> (\<exists>xa\<in>fst (updateCap ptr (capability.ReplyCap thread m canGrant) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C''])\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C''])\<rightarrow>[''words_C'']))) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap))))) x) \<in> rf_sr) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte y'. \<lbrakk>tcb_at' thread \<sigma>; cap_ptr_' x = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']); capTCBPtr___unsigned_long_' x = ptr_val (tcb_ptr_to_ctcb_ptr thread); capReplyMaster___unsigned_long_' x = from_bool m; capReplyCanGrant___unsigned_long_' x = from_bool canGrant; (\<sigma>, x) \<in> rf_sr; ctes_of \<sigma> ptr = Some cte; ccte_relation cte y'; cslift x (cte_Ptr ptr) = Some y'\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst ((do cte <- getCTE ptr;
setCTE ptr (cteCap_update (\<lambda>_. capability.ReplyCap thread m canGrant) cte)
od) \<sigma>). (snd xa, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C''])\<rightarrow>[''words_C''])) (Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap))))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte y'. \<lbrakk>tcb_at' thread \<sigma>; cap_ptr_' x = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']); capTCBPtr___unsigned_long_' x = ptr_val (tcb_ptr_to_ctcb_ptr thread); capReplyMaster___unsigned_long_' x = from_bool m; capReplyCanGrant___unsigned_long_' x = from_bool canGrant; ctes_of \<sigma> ptr = Some cte; ccte_relation cte y'; cslift x (cte_Ptr ptr) = Some y'\<rbrakk> \<Longrightarrow> ccte_relation (cteCap_update (\<lambda>_. capability.ReplyCap thread m canGrant) cte) (cte_C.cap_C_update (\<lambda>_. cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')) y') proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte y'. \<lbrakk>tcb_at' thread \<sigma>; cap_ptr_' x = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']); capTCBPtr___unsigned_long_' x = ptr_val (tcb_ptr_to_ctcb_ptr thread); capReplyMaster___unsigned_long_' x = from_bool m; capReplyCanGrant___unsigned_long_' x = from_bool canGrant; ctes_of \<sigma> ptr = Some cte; cslift x (cte_Ptr ptr) = Some y'; Some (cteCap cte) = map_option cap_to_H (cap_lift (cte_C.cap_C y')); case cap_lift (cte_C.cap_C y') of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x; mdb_node_to_H (mdb_node_lift (cteMDBNode_C y')) = cteMDBNode cte\<rbrakk> \<Longrightarrow> Some (capability.ReplyCap thread m canGrant) = map_option cap_to_H (cap_lift (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y'))) \<and> (case cap_lift (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')) of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte y'. \<lbrakk>tcb_at' thread \<sigma>; cap_ptr_' x = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']); capTCBPtr___unsigned_long_' x = ptr_val (tcb_ptr_to_ctcb_ptr thread); capReplyMaster___unsigned_long_' x = from_bool m; capReplyCanGrant___unsigned_long_' x = from_bool canGrant; ctes_of \<sigma> ptr = Some cte; cslift x (cte_Ptr ptr) = Some y'; Some (cteCap cte) = map_option cap_to_H (cap_lift (cte_C.cap_C y')); case cap_lift (cte_C.cap_C y') of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x; mdb_node_to_H (mdb_node_lift (cteMDBNode_C y')) = cteMDBNode cte; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr thread)) ctcb_size_bits\<rbrakk> \<Longrightarrow> Some (capability.ReplyCap thread m canGrant) = map_option cap_to_H (cap_lift (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y'))) \<and> (case cap_lift (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')) of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x) proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma> x cte y'. \<lbrakk>tcb_at' thread \<sigma>; cap_ptr_' x = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']); capTCBPtr___unsigned_long_' x = ptr_val (tcb_ptr_to_ctcb_ptr thread); capReplyMaster___unsigned_long_' x = from_bool m; capReplyCanGrant___unsigned_long_' x = from_bool canGrant; ctes_of \<sigma> ptr = Some cte; cslift x (cte_Ptr ptr) = Some y'; Some (cteCap cte) = map_option cap_to_H (cap_lift (cte_C.cap_C y')); case cap_lift (cte_C.cap_C y') of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x; mdb_node_to_H (mdb_node_lift (cteMDBNode_C y')) = cteMDBNode cte; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr thread)) ctcb_size_bits\<rbrakk> \<Longrightarrow> cap_get_tag (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')) = SCAST(32 signed \<rightarrow> 32) cap_reply_cap
 2. \<And>\<sigma> x cte y'. \<lbrakk>tcb_at' thread \<sigma>; cap_ptr_' x = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']); capTCBPtr___unsigned_long_' x = ptr_val (tcb_ptr_to_ctcb_ptr thread); capReplyMaster___unsigned_long_' x = from_bool m; capReplyCanGrant___unsigned_long_' x = from_bool canGrant; ctes_of \<sigma> ptr = Some cte; cslift x (cte_Ptr ptr) = Some y'; Some (cteCap cte) = map_option cap_to_H (cap_lift (cte_C.cap_C y')); case cap_lift (cte_C.cap_C y') of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x; mdb_node_to_H (mdb_node_lift (cteMDBNode_C y')) = cteMDBNode cte; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr thread)) ctcb_size_bits\<rbrakk> \<Longrightarrow> Some (capability.ReplyCap thread m canGrant) = map_option cap_to_H (Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] << 0) && ~~ mask 6\<rparr>)) \<and> (case Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] << 0) && ~~ mask 6\<rparr>) of None \<Rightarrow> True | Some a \<Rightarrow> cl_valid_cap a) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte y'. \<lbrakk>tcb_at' thread \<sigma>; cap_ptr_' x = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']); capTCBPtr___unsigned_long_' x = ptr_val (tcb_ptr_to_ctcb_ptr thread); capReplyMaster___unsigned_long_' x = from_bool m; capReplyCanGrant___unsigned_long_' x = from_bool canGrant; ctes_of \<sigma> ptr = Some cte; cslift x (cte_Ptr ptr) = Some y'; Some (cteCap cte) = map_option cap_to_H (cap_lift (cte_C.cap_C y')); case cap_lift (cte_C.cap_C y') of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x; mdb_node_to_H (mdb_node_lift (cteMDBNode_C y')) = cteMDBNode cte; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr thread)) ctcb_size_bits\<rbrakk> \<Longrightarrow> Some (capability.ReplyCap thread m canGrant) = map_option cap_to_H (Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] << 0) && ~~ mask 6\<rparr>)) \<and> (case Some (Cap_reply_cap \<lparr>capReplyCanGrant_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] >> 5) && mask 1, capReplyMaster_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] >> 4) && mask 1, capTCBPtr_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C y')) 0 (((ptr_val (tcb_ptr_to_ctcb_ptr thread) || (from_bool m << 4)) || (from_bool canGrant << 5)) || SCAST(32 signed \<rightarrow> 32) cap_reply_cap)) (cte_C.cap_C y')).[0] << 0) && ~~ mask 6\<rparr>) of None \<Rightarrow> True | Some a \<Rightarrow> cl_valid_cap a) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte y'. \<lbrakk>tcb_at' thread \<sigma>; cap_ptr_' x = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']); capTCBPtr___unsigned_long_' x = ptr_val (tcb_ptr_to_ctcb_ptr thread); capReplyMaster___unsigned_long_' x = from_bool m; capReplyCanGrant___unsigned_long_' x = from_bool canGrant; ctes_of \<sigma> ptr = Some cte; cslift x (cte_Ptr ptr) = Some y'; Some (cteCap cte) = map_option cap_to_H (cap_lift (cte_C.cap_C y')); case cap_lift (cte_C.cap_C y') of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x; mdb_node_to_H (mdb_node_lift (cteMDBNode_C y')) = cteMDBNode cte; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr thread)) 8\<rbrakk> \<Longrightarrow> m = to_bool (from_bool m || (from_bool canGrant << 5 >> 4) && 1) \<and> canGrant = to_bool ((from_bool m >> Suc 0) && 1 || from_bool canGrant) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x cte y'. \<lbrakk>tcb_at' thread \<sigma>; cap_ptr_' x = cap_Ptr &(cte_Ptr ptr\<rightarrow>[''cap_C'']); capTCBPtr___unsigned_long_' x = ptr_val (tcb_ptr_to_ctcb_ptr thread); capReplyMaster___unsigned_long_' x = SCAST(32 signed \<rightarrow> 32) false; capReplyCanGrant___unsigned_long_' x = from_bool canGrant; ctes_of \<sigma> ptr = Some cte; cslift x (cte_Ptr ptr) = Some y'; Some (cteCap cte) = map_option cap_to_H (cap_lift (cte_C.cap_C y')); case cap_lift (cte_C.cap_C y') of None \<Rightarrow> True | Some x \<Rightarrow> cl_valid_cap x; mdb_node_to_H (mdb_node_lift (cteMDBNode_C y')) = cteMDBNode cte; is_aligned (ptr_val (tcb_ptr_to_ctcb_ptr thread)) 8; \<not> m\<rbrakk> \<Longrightarrow> \<not> to_bool (SCAST(32 signed \<rightarrow> 32) false || (from_bool canGrant << 5 >> 4) && 1) \<and> canGrant = to_bool ((SCAST(32 signed \<rightarrow> 32) false >> Suc 0) && 1 || from_bool canGrant) proof (prove)
goal:
No subgoals!