(* * Copyright 2014, General Dynamics C4 Systems * * This software may be distributed and modified according to the terms of * the GNU General Public License version 2. Note that NO WARRANTY is provided. * See "LICENSE_GPLv2.txt" for details. * * @TAG(GD_GPL) *) theory CSpace_C imports CSpaceAcc_C Machine_C begin context kernel_m begin lemma maskCapRights_cap_cases: "return (maskCapRights R c) = (case c of ArchObjectCap ac \ return (Arch.maskCapRights R ac) | EndpointCap _ _ _ _ _ \ return (capEPCanGrant_update (\_. capEPCanGrant c \ capAllowGrant R) (capEPCanReceive_update (\_. capEPCanReceive c \ capAllowRead R) (capEPCanSend_update (\_. capEPCanSend c \ capAllowWrite R) c))) | NotificationCap _ _ _ _ \ return (capNtfnCanReceive_update (\_. capNtfnCanReceive c \ capAllowRead R) (capNtfnCanSend_update (\_. capNtfnCanSend c \ capAllowWrite R) c)) | _ \ return c)" apply (simp add: maskCapRights_def Let_def split del: if_split) apply (cases c; simp add: isCap_simps split del: if_split) done lemma imp_ignore: "B \ A \ B" by blast (* FIXME x64: ucast? see how it goes *) lemma wordFromVMRights_spec: "\s. \ \ {s} Call wordFromVMRights_'proc \\ret__unsigned_long = \<^bsup>s\<^esup>vm_rights\" by vcg simp? (* FIXME x64: ucast? see how it goes *) lemma vmRightsFromWord_spec: "\s. \ \ {s} Call vmRightsFromWord_'proc \\ret__unsigned_long = \<^bsup>s\<^esup>w\" by vcg simp? lemmas vmrights_defs = Kernel_C.VMReadOnly_def Kernel_C.VMKernelOnly_def Kernel_C.VMReadWrite_def lemma maskVMRights_spec: "\s. \ \ ({s} \ \ \vm_rights && mask 2 = \vm_rights \) Call maskVMRights_'proc \ vmrights_to_H \ret__unsigned_long = maskVMRights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) (cap_rights_to_H (seL4_CapRights_lift \<^bsup>s\<^esup>cap_rights_mask)) \ \ret__unsigned_long && mask 2 = \ret__unsigned_long \ \ret__unsigned_long \ 0 \" apply vcg apply clarsimp apply (rule conjI) apply ((auto simp: vmrights_to_H_def maskVMRights_def vmrights_defs cap_rights_to_H_def to_bool_def split: bool.split | simp add: mask_def | word_bitwise)+)[1] apply clarsimp apply (subgoal_tac "vm_rights = 0 \ vm_rights = 1 \ vm_rights = 2 \ vm_rights = 3") apply (auto simp: vmrights_to_H_def maskVMRights_def vmrights_defs cap_rights_to_H_def seL4_CapRights_lift_def to_bool_def mask_def split: bool.splits)[1] apply (subst(asm) mask_eq_iff_w2p) apply (simp add: word_size) apply (rule ccontr, clarsimp) apply (drule inc_le, simp, drule(1) order_le_neq_trans [OF _ not_sym])+ apply (drule inc_le, simp) done lemma frame_cap_rights [simp]: "cap_get_tag cap = scast cap_frame_cap \ cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) && mask 2 = cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap)" apply (simp add: cap_frame_cap_lift_def) by (simp add: cap_lift_def cap_tag_defs mask_def word_bw_assocs) lemma Arch_maskCapRights_ccorres [corres]: "ccorres ccap_relation ret__struct_cap_C_' \ (UNIV \ \ccap_relation (ArchObjectCap arch_cap) \cap\ \ \ccap_rights_relation R \cap_rights_mask\) [] (return (Arch.maskCapRights R arch_cap)) (Call Arch_maskCapRights_'proc)" apply (cinit' lift: cap_' cap_rights_mask_') apply csymbr apply (unfold X64_H.maskCapRights_def) apply (simp only: Let_def) apply (case_tac "cap_get_tag cap = scast cap_frame_cap") apply (clarsimp simp add: ccorres_cond_iffs cap_get_tag_isCap isCap_simps split del: if_splits) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: cap_get_tag_isCap isCap_simps) apply (clarsimp simp: return_def) apply (unfold ccap_relation_def)[1] apply (simp add: cap_frame_cap_lift [THEN iffD1]) apply (clarsimp simp: cap_to_H_def) apply (simp add: map_option_case split: option.splits) apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) apply (clarsimp simp: cap_frame_cap_lift_def) apply (clarsimp simp: ccap_rights_relation_def cap_frame_cap_lift c_valid_cap_def cl_valid_cap_def mask_eq_iff word_less_alt split: option.splits cap_CL.splits) apply (clarsimp simp: cap_frame_cap_lift_def) apply (clarsimp simp: ccap_rights_relation_def c_valid_cap_def cap_frame_cap_lift cl_valid_cap_def mask_eq_iff word_less_alt) apply (clarsimp simp add: cap_get_tag_isCap isCap_simps simp del: not_ex) apply (rule conjI, clarsimp) apply (simp add: ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp add: return_def simp del: not_ex) apply (cases arch_cap) by (fastforce simp add: cap_get_tag_isCap isCap_simps simp del: not_ex omgwtfbbq)+ lemma to_bool_mask_to_bool_bf: "to_bool (x && mask (Suc 0)) = to_bool_bf (x::machine_word)" apply (simp add: to_bool_bf_def to_bool_def) apply (rule iffI) prefer 2 apply simp apply (subgoal_tac "x && mask (Suc 0) < 2^(Suc 0)") apply simp apply (drule word_less_cases [where y=2]) apply auto[1] apply (rule and_mask_less') apply simp done lemma to_bool_cap_rights_bf: "to_bool (capAllowRead_CL (seL4_CapRights_lift R)) = to_bool_bf (capAllowRead_CL (seL4_CapRights_lift R))" "to_bool (capAllowWrite_CL (seL4_CapRights_lift R)) = to_bool_bf (capAllowWrite_CL (seL4_CapRights_lift R))" "to_bool (capAllowGrant_CL (seL4_CapRights_lift R)) = to_bool_bf (capAllowGrant_CL (seL4_CapRights_lift R))" by (subst to_bool_bf_to_bool_mask, simp add: seL4_CapRights_lift_def mask_def word_bw_assocs, simp)+ lemma to_bool_ntfn_cap_bf: "cap_lift c = Some (Cap_notification_cap cap) \ to_bool (capNtfnCanSend_CL cap) = to_bool_bf (capNtfnCanSend_CL cap) \ to_bool (capNtfnCanReceive_CL cap) = to_bool_bf (capNtfnCanReceive_CL cap)" apply (simp add:cap_lift_def Let_def split: if_split_asm) apply (subst to_bool_bf_to_bool_mask, clarsimp simp: cap_lift_thread_cap mask_def word_bw_assocs)+ apply simp done lemma to_bool_ep_cap_bf: "cap_lift c = Some (Cap_endpoint_cap cap) \ to_bool (capCanSend_CL cap) = to_bool_bf (capCanSend_CL cap) \ to_bool (capCanReceive_CL cap) = to_bool_bf (capCanReceive_CL cap) \ to_bool (capCanGrant_CL cap) = to_bool_bf (capCanGrant_CL cap)" apply (simp add:cap_lift_def Let_def split: if_split_asm) apply (subst to_bool_bf_to_bool_mask, clarsimp simp: cap_lift_thread_cap mask_def word_bw_assocs)+ apply simp done lemma isArchCap_spec: "\s. \\ {s} Call isArchCap_'proc \\ret__unsigned_long = from_bool (isArchCap_tag (cap_get_tag (cap_' s)))\" apply vcg apply (clarsimp simp: from_bool_def isArchCap_tag_def bool.split) apply (clarsimp simp: word_mod_2p_is_mask[where n=1, simplified] mask_def) apply word_bitwise done lemma maskCapRights_ccorres [corres]: "ccorres ccap_relation ret__struct_cap_C_' \ (UNIV \ \ccap_relation cap \cap\ \ \ccap_rights_relation R \cap_rights\) [] (return (RetypeDecls_H.maskCapRights R cap)) (Call maskCapRights_'proc)" apply (cinit' lift: cap_' cap_rights_') apply csymbr apply (simp add: maskCapRights_cap_cases cap_get_tag_isCap del: Collect_const) apply wpc apply (simp add: Collect_const_mem from_bool_def) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) apply (simp add: ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply clarsimp apply (simp add: cap_get_tag_isCap isCap_simps return_def) apply (simp add: Collect_const_mem from_bool_def) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) apply (simp add: ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply (clarsimp simp: return_def) apply (simp add: Collect_const_mem from_bool_def) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) apply (simp add: ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply clarsimp apply (simp add: cap_get_tag_isCap isCap_simps return_def) apply (rule imp_ignore) apply (rule imp_ignore) apply (rule imp_ignore) apply (rule imp_ignore) apply (rule imp_ignore) apply clarsimp apply (unfold ccap_relation_def)[1] apply (simp add: cap_notification_cap_lift [THEN iffD1]) apply (clarsimp simp: cap_to_H_def) apply (simp add: map_option_case split: option.splits) apply (clarsimp simp add: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) apply (simp add: cap_notification_cap_lift_def) apply (simp add: ccap_rights_relation_def cap_rights_to_H_def to_bool_ntfn_cap_bf to_bool_mask_to_bool_bf to_bool_cap_rights_bf) apply (simp add: Collect_const_mem from_bool_def) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply (clarsimp simp: cap_get_tag_isCap isCap_simps return_def) apply (simp add: Collect_const_mem from_bool_def) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply clarsimp apply (simp add: cap_get_tag_isCap isCap_simps return_def) apply (rule imp_ignore) apply (rule imp_ignore) apply (rule imp_ignore) apply (rule imp_ignore) apply (rule imp_ignore) apply (rule imp_ignore) apply (rule imp_ignore) apply (rule imp_ignore) apply clarsimp apply (unfold ccap_relation_def)[1] apply (simp add: cap_endpoint_cap_lift [THEN iffD1]) apply (clarsimp simp: cap_to_H_def) apply (simp add: map_option_case split: option.splits) apply (clarsimp simp add: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) apply (simp add: cap_endpoint_cap_lift_def) apply (simp add: ccap_rights_relation_def cap_rights_to_H_def to_bool_ep_cap_bf to_bool_mask_to_bool_bf to_bool_cap_rights_bf) apply (simp add: Collect_const_mem from_bool_def) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) apply (simp add: ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply (clarsimp simp: return_def) apply (simp add: Collect_const_mem from_bool_def) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply (clarsimp simp: cap_get_tag_isCap isCap_simps return_def) apply (simp add: Collect_const_mem from_bool_def) apply (subst bind_return [symmetric]) apply (rule ccorres_split_throws) apply ctac apply (rule_tac P=\ and P'="\\ret__struct_cap_C = ret__struct_cap_C\" in ccorres_inst) apply (rule ccorres_from_vcg_throws) apply (clarsimp simp: return_def) apply (rule conseqPre) apply vcg apply clarsimp apply wp apply vcg apply vcg apply (simp add: Collect_const_mem from_bool_def) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) apply (simp add: ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply (clarsimp simp: return_def) apply (simp add: Collect_const_mem from_bool_def) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) apply (simp add: ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply (clarsimp simp: return_def) apply (simp add: Collect_const_mem from_bool_def) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) apply (simp add: ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply clarsimp apply (simp add: cap_get_tag_isCap isCap_simps return_def) apply (simp add: Collect_const_mem from_bool_def) apply csymbr apply (simp add: cap_get_tag_isCap isCap_simps del: Collect_const) apply (simp add: ccorres_cond_iffs) apply (rule ccorres_from_vcg_throws [where P=\ and P'=UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply (clarsimp simp: return_def) apply clarsimp done abbreviation "lookupCap_xf \ liftxf errstate lookupCap_ret_C.status_C lookupCap_ret_C.cap_C ret__struct_lookupCap_ret_C_'" lemma ccorres_return_cte_cteCap [corres]: fixes ptr' :: "cstate \ cte_C ptr" assumes r1: "\s s' g. (s, s') \ rf_sr \ (s, xfu g s') \ rf_sr" and xf_xfu: "\s g. xf (xfu g s) = g s" shows "ccorres ccap_relation xf (\s. ctes_of s ptr = Some cte) {s. ptr_val (ptr' s) = ptr} hs (return (cteCap cte)) (Basic (\s. xfu (\_. h_val (hrs_mem (t_hrs_' (globals s))) (Ptr &(ptr' s \[''cap_C'']))) s))" apply (rule ccorres_return) apply (rule conseqPre) apply vcg apply (clarsimp simp: xf_xfu ccap_relation_def) apply rule apply (erule r1) apply (drule (1) rf_sr_ctes_of_clift) apply (clarsimp simp: typ_heap_simps) apply (simp add: c_valid_cte_def) done lemma ccorres_return_cte_mdbnode [corres]: fixes ptr' :: "cstate \ cte_C ptr" assumes r1: "\s s' g. (s, s') \ rf_sr \ (s, xfu g s') \ rf_sr" and xf_xfu: "\s g. xf (xfu g s) = g s" shows "ccorres cmdbnode_relation xf (\s. ctes_of s ptr = Some cte) {s. ptr_val (ptr' s) = ptr} hs (return (cteMDBNode cte)) (Basic (\s. xfu (\_. h_val (hrs_mem (t_hrs_' (globals s))) (Ptr &(ptr' s \[''cteMDBNode_C'']))) s))" apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp add: return_def xf_xfu) apply (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp: typ_heap_simps) apply (erule r1) done (* FIXME: MOVE *) lemma heap_update_field_ext: "\field_ti TYPE('a :: packed_type) f = Some t; c_guard p; export_uinfo t = export_uinfo (typ_info_t TYPE('b :: packed_type))\ \ heap_update (Ptr &(p\f) :: 'b ptr) = (\v hp. heap_update p (update_ti t (to_bytes_p v) (h_val hp p)) hp)" apply (rule ext, rule ext) apply (erule (2) heap_update_field) done lemma ccorres_updateCap [corres]: fixes ptr :: "cstate \ cte_C ptr" and val :: "cstate \ cap_C" shows "ccorres dc xfdc \ ({s. ccap_relation cap (val s)} \ {s. ptr s = Ptr dest}) hs (updateCap dest cap) (Basic (\s. globals_update (t_hrs_'_update (hrs_mem_update (heap_update (Ptr &(ptr s\[''cap_C''])) (val s)))) s))" unfolding updateCap_def apply (cinitlift ptr) apply (erule ssubst) apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_getCTE) apply (rule_tac P = "\s. ctes_of s dest = Some rva" in ccorres_from_vcg [where P' = "{s. ccap_relation cap (val s)}"]) apply (rule allI) apply (rule conseqPre) apply vcg apply clarsimp apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) apply (erule bexI [rotated]) apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp add: rf_sr_def cstate_relation_def Let_def cpspace_relation_def cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) apply (simp add:typ_heap_simps) apply (rule conjI) apply (erule (3) cpspace_cte_relation_upd_capI) apply (frule_tac f="ksPSpace" in arg_cong) apply (erule_tac t = s' in ssubst) apply simp apply (simp add: heap_to_user_data_def heap_to_device_data_def) apply (rule conjI) apply (erule (1) setCTE_tcb_case) by (auto simp: carch_state_relation_def cmachine_state_relation_def global_ioport_bitmap_heap_update_tag_disj_simps fpu_null_state_heap_update_tag_disj_simps) lemma ccorres_updateMDB_const [corres]: fixes ptr :: "cstate \ cte_C ptr" and val :: "cstate \ mdb_node_C" shows "ccorres dc xfdc (\_. dest \ 0) ({s. cmdbnode_relation m (val s)} \ {s. ptr s = Ptr dest}) hs (updateMDB dest (const m)) (Basic (\s. globals_update (t_hrs_'_update (hrs_mem_update (heap_update (Ptr &(ptr s\[''cteMDBNode_C''])) (val s)))) s))" unfolding updateMDB_def apply (cinitlift ptr) apply (erule ssubst) apply (rule ccorres_gen_asm [where G = \, simplified]) apply (simp only: Let_def) apply simp apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_getCTE) apply (rule_tac P = "\s. ctes_of s dest = Some cte" in ccorres_from_vcg [where P' = "{s. cmdbnode_relation m (val s)}"]) apply (rule allI) apply (rule conseqPre) apply vcg apply clarsimp apply (rule fst_setCTE [OF ctes_of_cte_at], assumption ) apply (erule bexI [rotated]) apply (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp add: rf_sr_def cstate_relation_def typ_heap_simps Let_def cpspace_relation_def cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) apply (rule conjI) apply (erule (3) cspace_cte_relation_upd_mdbI) apply (erule_tac t = s' in ssubst) apply (simp add: heap_to_user_data_def) apply (rule conjI) apply (erule (1) setCTE_tcb_case) by (auto simp: carch_state_relation_def cmachine_state_relation_def global_ioport_bitmap_heap_update_tag_disj_simps fpu_null_state_heap_update_tag_disj_simps) (* 64 == badgeBits *) lemma cap_lift_capNtfnBadge_mask_eq: "cap_lift cap = Some (Cap_notification_cap ec) \ capNtfnBadge_CL ec && mask 64 = capNtfnBadge_CL ec" unfolding cap_lift_def by (fastforce simp: Let_def mask_def word_bw_assocs split: if_split_asm) lemma cap_lift_capEPBadge_mask_eq: "cap_lift cap = Some (Cap_endpoint_cap ec) \ capEPBadge_CL ec && mask 64 = capEPBadge_CL ec" unfolding cap_lift_def by (fastforce simp: Let_def mask_def word_bw_assocs split: if_split_asm) lemma Arch_isCapRevocable_spec: "\s. \\ {\. s = \ \ True} Call Arch_isCapRevocable_'proc {t. \c c'. ccap_relation c (derivedCap_' s) \ ccap_relation c' (srcCap_' s) \ ret__unsigned_long_' t = from_bool (Arch.isCapRevocable c c')}" apply vcg by (auto simp: false_def from_bool_def X64_H.isCapRevocable_def cap_get_tag_isCap_unfolded_H_cap cap_tag_defs isCap_simps cap_get_tag_isCap[unfolded cap_io_port_control_cap_def, simplified] split: capability.splits arch_capability.splits bool.splits) lemmas isCapRevocable_simps[simp] = Retype_H.isCapRevocable_def[split_simps capability.split] context begin (* revokable_ccorres *) private method revokable'_hammer = solves \( simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def, rule ccorres_guard_imp, rule ccorres_return_C; clarsimp)\ lemma revokable_ccorres: "ccorres (\a c. from_bool a = c) ret__unsigned_long_' (\_. capMasterCap cap = capMasterCap parent \ is_simple_cap' cap) (UNIV \ {s. ccap_relation cap (derivedCap_' s)} \ {s. ccap_relation parent (srcCap_' s)}) hs (return (isCapRevocable cap parent)) (Call isCapRevocable_'proc)" apply (rule ccorres_gen_asm[where G=\, simplified]) apply (cinit' lift: derivedCap_' srcCap_') \ \Clear up Arch cap case\ apply csymbr apply (clarsimp simp: cap_get_tag_isCap split del: if_splits simp del: Collect_const) apply (rule ccorres_Cond_rhs_Seq) apply (rule ccorres_rhs_assoc) apply (clarsimp simp: isCap_simps) apply csymbr apply (drule spec, drule spec, drule mp, fastforce) apply ccorres_rewrite apply (drule sym, simp only:) apply (rule ccorres_return_C, clarsimp+) apply csymbr apply (rule_tac P'=UNIV and P=\ in ccorres_inst) apply (cases cap) \ \Uninteresting caps\ apply revokable'_hammer+ \ \NotificationCap\ apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def) apply (rule ccorres_guard_imp, (rule ccorres_rhs_assoc)+, csymbr, csymbr) apply (rule ccorres_return_C, clarsimp+) apply (frule_tac cap'1=srcCap in cap_get_tag_NotificationCap[THEN iffD1]) apply (clarsimp simp: cap_get_tag_isCap isCap_simps is_simple_cap'_def) apply (frule_tac cap'1=derivedCap in cap_get_tag_NotificationCap[THEN iffD1]) apply (clarsimp simp: cap_get_tag_isCap isCap_simps) apply (fastforce simp: cap_get_tag_isCap isCap_simps) \ \IRQHandlerCap\ apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def) apply (rule ccorres_guard_imp, csymbr) apply (rule ccorres_return_C, clarsimp+) apply (fastforce simp: cap_get_tag_isCap isCap_simps) \ \EndpointCap\ apply (simp add: cap_get_tag_isCap isCap_simps ccorres_cond_iffs from_bool_def true_def false_def) apply (rule ccorres_guard_imp, (rule ccorres_rhs_assoc)+, csymbr, csymbr) apply (rule ccorres_return_C, clarsimp+) apply (frule_tac cap'1=srcCap in cap_get_tag_EndpointCap[THEN iffD1]) apply (clarsimp simp: cap_get_tag_isCap isCap_simps is_simple_cap'_def) apply (frule_tac cap'1=derivedCap in cap_get_tag_EndpointCap[THEN iffD1]) apply (clarsimp simp: cap_get_tag_isCap isCap_simps) apply (fastforce simp: cap_get_tag_isCap isCap_simps) \ \Other Caps\ by (revokable'_hammer | fastforce simp: isCap_simps)+ end (* revokable_ccorres *) lemma cteInsert_ccorres_mdb_helper: "\cmdbnode_relation rva srcMDB; from_bool rvc = (newCapIsRevocable :: machine_word); srcSlot = Ptr src\ \ ccorres cmdbnode_relation newMDB_' (K (is_aligned src 3)) UNIV hs (return (mdbFirstBadged_update (\_. rvc) (mdbRevocable_update (\_. rvc) (mdbPrev_update (\_. src) rva)))) (\newMDB :== CALL mdb_node_set_mdbPrev(srcMDB, ptr_val srcSlot);; \newMDB :== CALL mdb_node_set_mdbRevocable(\newMDB, newCapIsRevocable);; \newMDB :== CALL mdb_node_set_mdbFirstBadged(\newMDB, newCapIsRevocable))" apply (rule ccorres_from_vcg) apply (rule allI) apply (rule conseqPre) apply vcg apply (clarsimp simp: return_def cmdbnode_relation_def mask_def) done lemma ccorres_updateMDB_set_mdbNext [corres]: "src=src' \ ccorres dc xfdc ((\_. src \ 0 \ is_aligned dest cteSizeBits \ canonical_address dest)) ({s. mdb_node_ptr_' s = Ptr &((Ptr src' :: cte_C ptr)\[''cteMDBNode_C''])} \ {s. v64_' s = dest}) [] (updateMDB src (mdbNext_update (\_. dest))) (Call mdb_node_ptr_set_mdbNext_'proc)" unfolding updateMDB_def apply (hypsubst) apply (rule ccorres_gen_asm [where G = \, simplified]) apply (simp only: Let_def) apply simp apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_getCTE [where P = "\cte s. ctes_of s src' = Some cte" and P'= "\_. (\\mdb_node_ptr = Ptr &((Ptr src' :: cte_C ptr)\[''cteMDBNode_C''])\ \ \\v64 = dest\)"]) apply (rule ccorres_from_spec_modifies_heap) apply (rule mdb_node_ptr_set_mdbNext_spec) apply (rule mdb_node_ptr_set_mdbNext_modifies) apply simp apply clarsimp apply (rule rf_sr_cte_at_valid) apply simp apply (erule ctes_of_cte_at) apply assumption apply clarsimp apply (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp: typ_heap_simps) apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) apply (erule bexI [rotated]) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def cte_wp_at_ctes_of heap_to_user_data_def cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"] typ_heap_simps') apply (rule conjI) apply (erule (2) cspace_cte_relation_upd_mdbI) apply (simp add: cmdbnode_relation_def) apply (intro arg_cong[where f="\f. mdbNext_update f mdb" for mdb] ext word_eqI) apply (simp add: sign_extend_bitwise_if' neg_mask_bang word_size) apply (match premises in C: "canonical_address _" and A: "is_aligned _ _" (multi) \ \match premises in H[thin]: _ (multi) \ \insert C A\\) apply (drule is_aligned_weaken[where y=2], simp add: objBits_defs) apply (case_tac "n < 2"; case_tac "n \ 47"; clarsimp simp: linorder_not_less linorder_not_le is_aligned_nth[THEN iffD1]) apply (fastforce simp: word_size dest: canonical_address_high_bits) apply (erule_tac t = s'a in ssubst) apply simp apply (rule conjI) apply (erule (1) setCTE_tcb_case) by (auto simp: carch_state_relation_def cmachine_state_relation_def global_ioport_bitmap_heap_update_tag_disj_simps fpu_null_state_heap_update_tag_disj_simps) lemma ccorres_updateMDB_set_mdbPrev [corres]: "src=src' \ ccorres dc xfdc (\_. src \ 0 \ is_aligned dest cteSizeBits) ({s. mdb_node_ptr_' s = Ptr &((Ptr src' :: cte_C ptr)\[''cteMDBNode_C''])} \ {s. v64_' s = dest}) [] (updateMDB src (mdbPrev_update (\_. dest))) (Call mdb_node_ptr_set_mdbPrev_'proc)" unfolding updateMDB_def apply (hypsubst) apply (rule ccorres_gen_asm [where G = \, simplified]) apply (simp only: Let_def) apply simp apply (rule ccorres_guard_imp2) apply (rule ccorres_pre_getCTE [where P = "\cte s. ctes_of s src' = Some cte" and P' = "\_. (\\mdb_node_ptr = Ptr &((Ptr src' :: cte_C ptr)\[''cteMDBNode_C''])\ \ \\v64 = dest\)"]) apply (rule ccorres_from_spec_modifies_heap) apply (rule mdb_node_ptr_set_mdbPrev_spec) apply (rule mdb_node_ptr_set_mdbPrev_modifies) apply simp apply clarsimp apply (rule rf_sr_cte_at_valid) apply simp apply (erule ctes_of_cte_at) apply assumption apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp: typ_heap_simps) apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) apply (erule bexI[rotated]) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def cte_wp_at_ctes_of heap_to_user_data_def cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"] typ_heap_simps') apply (rule conjI) apply (erule (2) cspace_cte_relation_upd_mdbI) apply (simp add: cmdbnode_relation_def mask_def) apply (erule_tac t = s'a in ssubst) apply (simp add: carch_state_relation_def cmachine_state_relation_def fpu_null_state_heap_update_tag_disj_simps global_ioport_bitmap_heap_update_tag_disj_simps) apply (erule (1) setCTE_tcb_case) by clarsimp lemma ccorres_updateMDB_skip: "ccorres dc xfdc (\ and (\_. n = 0)) UNIV hs (updateMDB n f) SKIP" unfolding updateMDB_def apply (rule ccorres_gen_asm) apply simp apply (rule ccorres_return) apply simp apply vcg done definition "is_simple_cap_tag (tag :: machine_word) \ tag \ scast cap_null_cap \ tag \ scast cap_irq_control_cap \ tag \ scast cap_untyped_cap \ tag \ scast cap_reply_cap \ tag \ scast cap_endpoint_cap \ tag \ scast cap_notification_cap \ tag \ scast cap_thread_cap \ tag \ scast cap_cnode_cap \ tag \ scast cap_zombie_cap \ tag \ scast cap_io_port_control_cap \ tag \ scast cap_frame_cap" (* Useful: apply (tactic {* let val _ = reset CtacImpl.trace_ceqv; val _ = reset CtacImpl.trace_ctac in all_tac end; *}) *) declare word_neq_0_conv [simp del] schematic_goal ccap_relation_tag_Master: "\ccap. \ ccap_relation cap ccap \ \ cap_get_tag ccap = case_capability ?a ?b ?c ?d ?e ?f ?g (case_arch_capability ?aa ?ab ?ac ?ad ?ae ?af ?ag ?ah ?ai) ?h ?i ?j ?k (capMasterCap cap)" by (fastforce simp: ccap_relation_def map_option_Some_eq2 Let_def cap_lift_def cap_to_H_def split: if_split_asm) lemma ccap_relation_is_derived_tag_equal: "\ is_derived' cs p cap cap'; ccap_relation cap ccap; ccap_relation cap' ccap' \ \ cap_get_tag ccap' = cap_get_tag ccap" unfolding badge_derived'_def is_derived'_def by (clarsimp simp: ccap_relation_tag_Master) lemma ccap_relation_Master_tags_eq: "\ capMasterCap cap = capMasterCap cap'; ccap_relation cap ccap; ccap_relation cap' ccap' \ \ cap_get_tag ccap' = cap_get_tag ccap" by (clarsimp simp: ccap_relation_tag_Master) lemma is_simple_cap_get_tag_relation: "ccap_relation cap ccap \ is_simple_cap_tag (cap_get_tag ccap) = is_simple_cap' cap" apply (simp add: is_simple_cap_tag_def is_simple_cap'_def cap_get_tag_isCap) apply (auto simp: isCap_simps) done lemma setUntypedCapAsFull_cte_at_wp [wp]: "\ cte_at' x \ setUntypedCapAsFull rvb cap src \ \_. cte_at' x \" apply (clarsimp simp: setUntypedCapAsFull_def) apply wp done lemma valid_cap_untyped_inv: "valid_cap' (UntypedCap d r n f) s \ n \ minUntypedSizeBits \ is_aligned (of_nat f :: machine_word) minUntypedSizeBits \ n \ maxUntypedSizeBits \ n < word_bits" apply (clarsimp simp:valid_cap'_def capAligned_def) done lemma update_freeIndex': assumes i'_align: "is_aligned (of_nat i' :: machine_word) minUntypedSizeBits" assumes sz_bound: "sz \ maxUntypedSizeBits" assumes i'_bound: "i'\ 2^sz" shows "ccorres dc xfdc (cte_wp_at' (\cte. \i. cteCap cte = capability.UntypedCap d p sz i) srcSlot) (UNIV \ \\cap_ptr = cap_Ptr &(cte_Ptr srcSlot\[''cap_C''])\ \ \\v64 = of_nat i' >> minUntypedSizeBits\) [] (updateCap srcSlot (capability.UntypedCap d p sz i')) (Call cap_untyped_cap_ptr_set_capFreeIndex_'proc)" proof - note i'_bound_concrete = order_trans[OF i'_bound power_increasing[OF sz_bound], simplified untypedBits_defs, simplified] have i'_bound_word: "(of_nat i' :: machine_word) \ 2 ^ maxUntypedSizeBits" using order_trans[OF i'_bound power_increasing[OF sz_bound], simplified] by (simp add: word_of_nat_le untypedBits_defs) show ?thesis apply (cinit lift: cap_ptr_' v64_') apply (rule ccorres_pre_getCTE) apply (rule_tac P="\s. ctes_of s srcSlot = Some rv \ (\i. cteCap rv = UntypedCap d p sz i)" in ccorres_from_vcg[where P' = UNIV]) apply (rule allI) apply (rule conseqPre) apply vcg apply (clarsimp simp: guard_simps) apply (intro conjI) apply (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp: typ_heap_simps) apply (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp: split_def) apply (simp add: hrs_htd_def typ_heap_simps) apply (rule fst_setCTE[OF ctes_of_cte_at], assumption) apply (erule bexI[rotated], clarsimp) apply (frule (1) rf_sr_ctes_of_clift) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) apply (simp add: cpspace_relation_def) apply (clarsimp simp: typ_heap_simps') apply (rule conjI) apply (erule (2) cpspace_cte_relation_upd_capI) apply (simp only: cte_lift_def split: option.splits; simp) apply (simp add: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) apply (case_tac y) apply (simp add: cap_lift_def Let_def split: if_split_asm) apply (case_tac cte', simp) apply (clarsimp simp: ccap_relation_def cap_lift_def cap_get_tag_def cap_to_H_def) apply (thin_tac _)+ apply (simp add: mask_def to_bool_and_1 nth_shiftr word_ao_dist word_bool_alg.conj.assoc) apply (rule inj_onD[OF word_unat.Abs_inj_on[where 'a=machine_word_len]], simp) apply (cut_tac i'_align i'_bound_word) apply (simp add: is_aligned_mask) apply word_bitwise subgoal by (simp add: word_size untypedBits_defs) apply (cut_tac i'_bound_concrete) subgoal by (simp add: unats_def) subgoal by (simp add: word_unat.Rep[where 'a=machine_word_len, simplified]) apply (erule_tac t = s' in ssubst) apply clarsimp apply (rule conjI) subgoal by (erule (1) setCTE_tcb_case) apply (clarsimp simp: carch_state_relation_def cmachine_state_relation_def fpu_null_state_heap_update_tag_disj_simps global_ioport_bitmap_heap_update_tag_disj_simps packed_heap_update_collapse_hrs) by (clarsimp simp: cte_wp_at_ctes_of) qed lemma update_freeIndex: "ccorres dc xfdc (valid_objs' and cte_wp_at' (\cte. \i. cteCap cte = UntypedCap d p sz i) srcSlot and (\_. is_aligned (of_nat i' :: machine_word) minUntypedSizeBits \ i' \ 2 ^ sz)) (UNIV \ \\cap_ptr = cap_Ptr &(cte_Ptr srcSlot\[''cap_C''])\ \ \\v64 = of_nat i' >> minUntypedSizeBits\) [] (updateCap srcSlot (UntypedCap d p sz i')) (Call cap_untyped_cap_ptr_set_capFreeIndex_'proc)" apply (rule ccorres_assume_pre, rule ccorres_guard_imp) apply (rule update_freeIndex'; clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte; clarsimp dest!: ctes_of_valid_cap' simp: valid_cap'_def) by auto (* FIXME: move *) lemma ccorres_cases: assumes P: " P \ ccorres r xf G G' hs a b" assumes notP: "\P \ ccorres r xf H H' hs a b" shows "ccorres r xf (\s. (P \ G s) \ (\P \ H s)) ({s. P \ s \ G'} \ {s. \P \ s \ H'}) hs a b" apply (cases P, auto simp: P notP) done lemma capBlockSize_CL_maxSize: " \ cap_get_tag c = scast cap_untyped_cap \ \ capBlockSize_CL (cap_untyped_cap_lift c) < 0x40" apply (clarsimp simp: cap_untyped_cap_lift_def) apply (clarsimp simp: cap_lift_def) apply (clarsimp simp: cap_untyped_cap_def cap_null_cap_def) apply (rule word_and_less') apply (simp add: mask_def) done lemma setUntypedCapAsFull_ccorres [corres]: notes if_split [split del] notes Collect_const [simp del] notes Collect_True [simp] Collect_False [simp] shows "ccorres dc xfdc ((cte_wp_at' (\c. (cteCap c) = srcCap) srcSlot) and valid_mdb' and pspace_aligned' and valid_objs' and (K (isUntypedCap newCap \ (minUntypedSizeBits \ capBlockSize newCap))) and (K (isUntypedCap srcCap \ (minUntypedSizeBits \ capBlockSize srcCap)))) (UNIV \ {s. ccap_relation srcCap (srcCap_' s)} \ {s. ccap_relation newCap (newCap_' s)} \ {s. srcSlot_' s = Ptr srcSlot}) [] (setUntypedCapAsFull srcCap newCap srcSlot) (Call setUntypedCapAsFull_'proc)" apply (cinit lift: srcCap_' newCap_' srcSlot_') apply (rule ccorres_if_lhs) apply (clarsimp simp: isCap_simps) apply csymbr apply csymbr apply (simp add: if_then_0_else_1 if_then_1_else_0 cap_get_tag_isCap_unfolded_H_cap) apply (rule ccorres_rhs_assoc)+ apply csymbr apply csymbr apply (simp add: cap_get_tag_isCap_unfolded_H_cap ccorres_cond_univ_iff) apply (rule ccorres_rhs_assoc)+ apply csymbr apply csymbr apply csymbr apply (frule cap_get_tag_to_H(9)) apply (simp add: cap_get_tag_isCap_unfolded_H_cap) apply (rotate_tac 1) apply (frule cap_get_tag_to_H(9)) apply (simp add: cap_get_tag_isCap_unfolded_H_cap) apply simp apply (rule ccorres_rhs_assoc)+ apply csymbr apply csymbr apply csymbr apply (simp add: ccorres_cond_univ_iff) apply csymbr+ apply (rule ccorres_move_c_guard_cte) apply (rule ccorres_Guard) apply (rule ccorres_call) apply (rule update_freeIndex [unfolded dc_def]) apply simp apply simp apply simp apply clarsimp apply (csymbr) apply (csymbr) apply (simp add: cap_get_tag_isCap) apply (rule ccorres_Cond_rhs_Seq) apply (rule ccorres_rhs_assoc)+ apply csymbr apply csymbr apply (simp add: cap_get_tag_isCap) apply (rule ccorres_Cond_rhs) apply (rule ccorres_rhs_assoc)+ apply csymbr apply csymbr apply csymbr apply (rule ccorres_cases [where P="capPtr srcCap = capPtr newCap"]) apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap split: if_split_asm) apply (rule ccorres_rhs_assoc)+ apply csymbr apply csymbr apply csymbr apply (clarsimp simp: cap_get_tag_to_H cap_get_tag_UntypedCap split: if_split_asm) apply (rule ccorres_cond_false) apply (rule ccorres_return_Skip [unfolded dc_def]) apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap split: if_split_asm) apply (rule ccorres_cond_false) apply (rule ccorres_return_Skip [unfolded dc_def]) apply (rule ccorres_return_Skip [unfolded dc_def]) apply clarsimp apply (rule ccorres_cond_false) apply (rule ccorres_return_Skip [unfolded dc_def]) apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap) apply (frule(1) cte_wp_at_valid_objs_valid_cap') apply (clarsimp simp: untypedBits_defs) apply (intro conjI impI allI) apply (erule cte_wp_at_weakenE') apply (clarsimp simp: cap_get_tag_isCap[symmetric] cap_get_tag_UntypedCap split: if_split_asm) apply clarsimp apply (drule valid_cap_untyped_inv,clarsimp simp:max_free_index_def) apply (rule is_aligned_weaken) apply (rule is_aligned_shiftl_self[unfolded shiftl_t2n,where p = 1,simplified]) apply assumption apply (clarsimp simp: max_free_index_def shiftL_nat valid_cap'_def capAligned_def) apply (simp add:power_minus_is_div unat_sub word_le_nat_alt t2p_shiftr) apply clarsimp apply (erule cte_wp_at_weakenE', simp) apply clarsimp apply (drule valid_cap_untyped_inv) apply (clarsimp simp: max_free_index_def t2p_shiftr unat_sub word_le_nat_alt word_bits_def) apply (rule word_less_imp_diff_less) apply (subst (asm) eq_commute, fastforce simp: unat_sub word_le_nat_alt) apply (rule capBlockSize_CL_maxSize) apply (clarsimp simp: cap_get_tag_UntypedCap) apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap) done lemma ccte_lift: "\(s, s') \ rf_sr; cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\ \ ctes_of s p = Some (cte_to_H (the (cte_lift cte')))" apply (clarsimp simp:rf_sr_def cstate_relation_def Let_def cpspace_relation_def) apply (drule(1) cmap_relation_cs_atD) apply simp apply (clarsimp simp:ccte_relation_def) done lemma cmdb_node_relation_mdbNext: "cmdbnode_relation n n' \ mdbNext_CL (mdb_node_lift n') = mdbNext n" by (simp add:cmdbnode_relation_def) lemma cslift_ptr_safe: "cslift x ptr = Some a \ ptr_safe ptr (hrs_htd (t_hrs_' (globals x)))" apply (rule_tac h = "fst (t_hrs_' (globals x))" in lift_t_ptr_safe[where g = c_guard]) apply (fastforce simp add:typ_heap_simps hrs_htd_def) done lemma ccorres_move_ptr_safe: "ccorres_underlying rf_sr \ r xf arrel axf A C' hs a c \ ccorres_underlying rf_sr \ r xf arrel axf (A and K (dest = cte_Ptr (ptr_val dest)) and cte_wp_at' (\_. True) (ptr_val dest)) (C' \ \True\) hs a (Guard MemorySafety \ptr_safe (dest) (hrs_htd \t_hrs) \ c)" apply (rule ccorres_guard_imp2) apply (rule ccorres_Guard) apply simp apply (clarsimp simp:cte_wp_at_ctes_of) apply (drule(1) rf_sr_ctes_of_clift) apply (case_tac dest) apply (clarsimp simp:ptr_coerce_def) apply (erule cslift_ptr_safe) done lemma ccorres_move_ptr_safe_Seq: "ccorres_underlying rf_sr \ r xf arrel axf A C' hs a (c;;d) \ ccorres_underlying rf_sr \ r xf arrel axf (A and cte_wp_at' (\_. True) (ptr_val dest) and K (dest = cte_Ptr (ptr_val dest))) (C' \ \True\) hs a (Guard MemorySafety \ptr_safe (dest) (hrs_htd \t_hrs) \ c;;d)" apply (rule ccorres_guard_imp2) apply (rule ccorres_Guard_Seq) apply simp apply (clarsimp simp:cte_wp_at_ctes_of) apply (drule(1) rf_sr_ctes_of_clift) apply clarsimp apply (erule cslift_ptr_safe) done lemmas ccorres_move_guard_ptr_safe = ccorres_move_ptr_safe_Seq ccorres_move_ptr_safe lemma cteInsert_ccorres: "ccorres dc xfdc (cte_wp_at' (\scte. capMasterCap (cteCap scte) = capMasterCap cap \ is_simple_cap' cap) src and valid_mdb' and valid_objs' and pspace_aligned' and pspace_canonical' and (valid_cap' cap)) (UNIV \ {s. destSlot_' s = Ptr dest} \ {s. srcSlot_' s = Ptr src} \ {s. ccap_relation cap (newCap_' s)}) [] (cteInsert cap src dest) (Call cteInsert_'proc)" supply ctes_of_aligned_bits[simp] apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_' simp del: return_bind simp add: Collect_const) apply (rule ccorres_move_c_guard_cte) apply (ctac pre: ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) apply (ctac pre: ccorres_pre_getCTE) apply (ctac (no_vcg) add: revokable_ccorres) apply (ctac (c_lines 3) add: cteInsert_ccorres_mdb_helper) apply (simp del: Collect_const) apply (rule ccorres_pre_getCTE ccorres_assert)+ apply (ctac add: setUntypedCapAsFull_ccorres) apply (rule ccorres_move_c_guard_cte) apply (ctac) apply (rule ccorres_move_c_guard_cte) apply ctac apply (rule ccorres_move_c_guard_cte) apply (ctac(no_vcg)) apply csymbr apply (erule_tac t = ret__unsigned_longlong in ssubst) apply (rule ccorres_cond_both [where R = \, simplified]) apply (erule mdbNext_not_zero_eq) apply csymbr apply simp apply (rule ccorres_move_c_guard_cte) apply (simp add:dc_def[symmetric]) apply (ctac ccorres:ccorres_updateMDB_set_mdbPrev) apply (simp add:dc_def[symmetric]) apply (ctac ccorres: ccorres_updateMDB_skip) apply (wp static_imp_wp)+ apply (clarsimp simp: Collect_const_mem dc_def split del: if_split) apply vcg apply (wp static_imp_wp) apply (clarsimp simp: Collect_const_mem dc_def split del: if_split) apply vcg apply (clarsimp simp:cmdb_node_relation_mdbNext) apply (wp setUntypedCapAsFull_cte_at_wp static_imp_wp) apply (clarsimp simp: Collect_const_mem dc_def split del: if_split) apply (vcg exspec=setUntypedCapAsFull_modifies) apply wp apply vcg apply wp apply wp apply vcg apply wp apply vcg apply (simp add: Collect_const_mem split del: if_split) \ \Takes a while\ apply (rule conjI) apply (clarsimp simp: conj_comms cte_wp_at_ctes_of) apply (intro conjI) apply clarsimp apply simp apply simp apply (clarsimp simp: ctes_of_canonical objBits_defs cte_level_bits_def) apply (rule conjI) apply (clarsimp simp: isUntypedCap_def split: capability.split_asm) apply (frule valid_cap_untyped_inv) apply clarsimp apply (rule conjI) apply (case_tac ctea) apply (clarsimp simp: isUntypedCap_def split: capability.splits) apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap']) apply fastforce apply clarsimp+ apply (drule valid_dlist_nextD) apply (simp add:valid_mdb'_def valid_mdb_ctes_def) apply simp apply clarsimp apply (clarsimp simp: map_comp_Some_iff cte_wp_at_ctes_of split del: if_split) apply (clarsimp simp: typ_heap_simps c_guard_clift split_def) apply (clarsimp simp: is_simple_cap_get_tag_relation ccte_relation_ccap_relation cmdb_node_relation_mdbNext[symmetric]) done (****************************************************************************) (* *) (* Lemmas dealing with updateMDB on Haskell side and IF-THEN-ELSE on C side *) (* *) (****************************************************************************) lemma updateMDB_mdbNext_set_mdbPrev: "\ slotc = Ptr slota; cmdbnode_relation mdba mdbc\ \ ccorres dc xfdc (\s. is_aligned slota cteSizeBits) UNIV hs (updateMDB (mdbNext mdba) (mdbPrev_update (\_. slota))) (IF mdbNext_CL (mdb_node_lift mdbc) \ 0 THEN Guard C_Guard \hrs_htd \t_hrs \\<^sub>t (Ptr (mdbNext_CL (mdb_node_lift mdbc)) :: cte_C ptr)\ (call (\ta. ta(| mdb_node_ptr_' := Ptr &(Ptr (mdbNext_CL (mdb_node_lift mdbc)):: cte_C ptr \[''cteMDBNode_C'']), v64_' := ptr_val slotc |)) mdb_node_ptr_set_mdbPrev_'proc (\s t. s\ globals := globals t \) (\ta s'. Basic (\a. a))) FI)" apply (rule ccorres_guard_imp2) apply (rule ccorres_cond_both[where R=\, simplified]) apply (erule mdbNext_not_zero_eq) apply (rule ccorres_updateMDB_cte_at) apply (ctac add: ccorres_updateMDB_set_mdbPrev) apply (ctac ccorres: ccorres_updateMDB_skip) apply (clarsimp simp: cmdbnode_relation_def cte_wp_at_ctes_of) done lemma updateMDB_mdbPrev_set_mdbNext: "\ slotc = Ptr slota; cmdbnode_relation mdba mdbc\ \ ccorres dc xfdc (\s. is_aligned slota cteSizeBits \ canonical_address slota) UNIV hs (updateMDB (mdbPrev mdba) (mdbNext_update (\_. slota))) (IF mdbPrev_CL (mdb_node_lift mdbc) \ 0 THEN Guard C_Guard \hrs_htd \t_hrs \\<^sub>t (Ptr (mdbPrev_CL (mdb_node_lift mdbc)):: cte_C ptr)\ (call (\ta. ta(| mdb_node_ptr_' := Ptr &(Ptr (mdbPrev_CL (mdb_node_lift mdbc)):: cte_C ptr \[''cteMDBNode_C'']), v64_' := ptr_val slotc |)) mdb_node_ptr_set_mdbNext_'proc (\s t. s\ globals := globals t \