From 3a9818b0709016723a1d74725c66d5bc47e87007 Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Mon, 16 Oct 2017 16:34:36 +1100 Subject: [PATCH] x64: crefine: added CSpace_RAB_C.thy --- proof/crefine/X64/CSpace_RAB_C.thy | 725 +++++++++++++++++++++++++++++ 1 file changed, 725 insertions(+) create mode 100644 proof/crefine/X64/CSpace_RAB_C.thy diff --git a/proof/crefine/X64/CSpace_RAB_C.thy b/proof/crefine/X64/CSpace_RAB_C.thy new file mode 100644 index 000000000..15cda3386 --- /dev/null +++ b/proof/crefine/X64/CSpace_RAB_C.thy @@ -0,0 +1,725 @@ +(* + * 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_RAB_C +imports CSpaceAcc_C "../../../lib/clib/MonadicRewrite_C" +begin + +context kernel +begin + +abbreviation + "rab_xf \ (liftxf errstate resolveAddressBits_ret_C.status_C + (\v. (resolveAddressBits_ret_C.slot_C v, bitsRemaining_C v)) + ret__struct_resolveAddressBits_ret_C_')" + +lemma rab_failure_case_ccorres: + fixes v :: "machine_word" and ist :: "cstate \ cstate" and f :: int + defines "call_part \ (call ist f (\s t. s\globals := globals t\) + (\ts s'. Basic (\s. + globals_update (current_lookup_fault_'_update + (\_. ret__struct_lookup_fault_C_' s')) s)))" + assumes spec: "\\ G' call_part {s. v \ scast EXCEPTION_NONE \ lookup_failure_rel e v (errstate s)}" + and mod: "\s. \\ {s'. (s, s') \ rf_sr} call_part {s'. (s, s') \ rf_sr}" + shows "ccorres (lookup_failure_rel \ r) rab_xf \ G' (SKIP # hs) + (throwError e) + (call_part ;; + \ret___struct_resolveAddressBits_ret_C :== + resolveAddressBits_ret_C.status_C_update (\_. v) \ret___struct_resolveAddressBits_ret_C;; + return_C ret__struct_resolveAddressBits_ret_C_'_update ret___struct_resolveAddressBits_ret_C_')" + apply (rule ccorres_rhs_assoc)+ + apply (rule ccorres_symb_exec_r [where R=\, OF _ spec]) + apply (rule ccorres_from_vcg_throws) + apply (simp add: throwError_def return_def) + apply (rule allI) + apply (rule conseqPre) + apply vcg + apply (auto simp add: exception_defs errstate_def)[1] + apply (rule conseqPre [OF mod]) + apply clarsimp + done + +lemma not_snd_bindE_I1: + "\ snd ((a >>=E b) s) \ \ snd (a s)" + unfolding bindE_def + by (erule not_snd_bindI1) + +lemma ccorres_remove_bind_returnOk_noguard: + assumes ac: "ccorres (f \ r') xf P P' (SKIP # hs) a c" + and rr: "\v s'. r' v (exvalue (xf s')) \ r (g v) (exvalue (xf s'))" + shows "ccorres (f \ r) xf P P' (SKIP # hs) (a >>=E (\v. returnOk (g v))) c" + apply (rule ccorresI') + apply clarsimp + apply (drule not_snd_bindE_I1) + apply (erule (4) ccorresE[OF ac]) + apply (clarsimp simp add: bindE_def returnOk_def NonDetMonad.lift_def bind_def return_def + split_def) + apply (rule bexI [rotated], assumption) + apply (simp add: throwError_def return_def unif_rrel_def + split: sum.splits) + apply (auto elim!: rr) + done + +declare isCNodeCap_CNodeCap[simp] + +(* MOVE *) +lemma ccorres_gen_asm_state: + assumes rl: "\s. P s \ ccorres r xf G G' hs a c" + shows "ccorres r xf (G and P) G' hs a c" +proof (rule ccorres_guard_imp2) + show "ccorres r xf (G and (\_. \s. P s)) G' hs a c" + apply (rule ccorres_gen_asm) + apply (erule exE) + apply (erule rl) + done +next + fix s s' + assume "(s, s') \ rf_sr" and "(G and P) s" and "s' \ G'" + thus "(G and (\_. \s. P s)) s \ s' \ G'" + by (clarsimp elim!: exI) +qed + +(* MOVE, generalise *) +lemma ccorres_req: + assumes rl: "\s s'. \ (s, s') \ rf_sr; Q s; Q' s' \ \ F s s'" + and cc: "\s s'. F s s' \ ccorres r xf P P' hs a c" + shows "ccorres r xf (P and Q) (P' \ Collect Q') hs a c" + apply (rule ccorresI') + apply clarsimp + apply (frule (2) rl) + apply (erule (5) ccorresE [OF cc]) + apply (clarsimp elim!: bexI [rotated]) + done + +lemma valid_cap_cte_at': + "\isCNodeCap cap; valid_cap' cap s'\ \ cte_at' (capCNodePtr cap + 0x20 * (addr && mask (capCNodeBits cap))) s'" + apply (clarsimp simp: isCap_simps valid_cap'_def) + apply (rule real_cte_at') + apply (erule spec) + done + +lemma mask_64_max_word [simp]: + shows "mask 64 = (max_word :: machine_word)" + unfolding mask_def + by (simp add: max_word_def) + +declare ucast_id [simp] +declare resolveAddressBits.simps [simp del] + +lemma if_then_1_else_0: + "((if P then 1 else 0) = (0 :: machine_word)) = (\ P)" + by (simp del: word_neq_0_conv) + +lemma if_then_0_else_1: + "((if P then 0 else 1) = (0 :: machine_word)) = (P)" + by (simp del: word_neq_0_conv) + +lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0 + +lemma rightsFromWord_wordFromRights: + "rightsFromWord (wordFromRights rghts) = rghts" + apply (cases rghts) + apply (simp add: wordFromRights_def rightsFromWord_def + split: if_split) + done + +lemma wordFromRights_inj: + "inj wordFromRights" + by (rule inj_on_inverseI, rule rightsFromWord_wordFromRights) + +lemmas wordFromRights_eq = inj_eq [OF wordFromRights_inj] + +lemma rightsFromWord_and: + "rightsFromWord (a && b) = andCapRights (rightsFromWord a) (rightsFromWord b)" + by (simp add: rightsFromWord_def andCapRights_def) + +lemma andCapRights_ac: + "andCapRights (andCapRights a b) c = andCapRights a (andCapRights b c)" + "andCapRights a b = andCapRights b a" + "andCapRights a (andCapRights b c) = andCapRights b (andCapRights a c)" + by (simp add: andCapRights_def conj_comms split: cap_rights.split)+ + +lemma wordFromRights_rightsFromWord: + "wordFromRights (rightsFromWord w) = w && mask 3" + apply (simp add: wordFromRights_def rightsFromWord_def + mask_def) + apply (auto simp: bin_nth_ops bin_nth_Bit0 bin_nth_Bit1 numeral_2_eq_2 + intro!: word_eqI) + done + + +lemma le_32_mask_eq: + " (bits::machine_word) \ 32 \ bits && mask 6 = bits " + apply (rule less_mask_eq) apply simp + apply (erule le_less_trans) apply simp +done + +(* FIXME: move, duplicated in CSpace_C *) +lemma ccorres_cases: + assumes P: " P \ ccorres_underlying sr \ r xf ar axf G G' hs a b" + assumes notP: "\P \ ccorres_underlying sr \ r xf ar axf H H' hs a b" + shows "ccorres_underlying sr \ r xf ar axf (\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 monadic_rewrite_stateAssert: + "monadic_rewrite F E P (stateAssert P xs) (return ())" + by (simp add: stateAssert_def monadic_rewrite_def exec_get) + +lemma ccorres_locateSlotCap_push: + "ccorres_underlying sr \ r xf ar axf P P' hs + (a >>=E (\x. locateSlotCap cp n >>= (\p. b p x))) c + \ (\P. \P\ a \\_. P\, - ) + \ ccorres_underlying sr \ r xf ar axf P P' hs + (locateSlotCap cp n >>= (\p. a >>=E (\x. b p x))) c" + apply (simp add: locateSlot_conv) + apply (rule ccorres_guard_imp2) + apply (rule ccorres_stateAssert) + apply (erule monadic_rewrite_ccorres_assemble) + apply (rule monadic_rewrite_bindE[OF monadic_rewrite_refl]) + apply (rule monadic_rewrite_transverse) + apply (rule monadic_rewrite_bind_head) + apply (rule monadic_rewrite_stateAssert) + apply simp + apply (rule monadic_rewrite_refl) + apply assumption + apply simp + done + +declare Kernel_C.cte_C_size[simp del] + +(* FIXME x64: redo after guard bits changes *) +lemma resolveAddressBits_ccorres [corres]: + shows "ccorres (lookup_failure_rel \ + (\(cte, bits) (cte', bits'). cte' = Ptr cte \ bits = unat bits' \ bits'\ 64)) rab_xf + (valid_pspace' and valid_cap' cap' + and K (guard' \ 64)) + ({s. ccap_relation cap' (nodeCap_' s)} \ + {s. capptr_' s = cptr'} \ {s. unat (n_bits_' s) = guard'}) [] + (resolveAddressBits cap' cptr' guard') (Call resolveAddressBits_'proc)" + (is "ccorres ?rvr rab_xf ?P ?P' [] ?rab ?rab'") +proof (cases "isCNodeCap cap'") + case False + + note Collect_const [simp del] + + show ?thesis using False + apply (cinit' lift: nodeCap_' capptr_' n_bits_') + apply csymbr+ + -- "Exception stuff" + apply (rule ccorres_split_throws) + apply (simp add: Collect_const cap_get_tag_isCap isCap_simps ccorres_cond_iffs + resolveAddressBits.simps scast_id) + apply (rule ccorres_from_vcg_throws [where P = \ and P' = UNIV]) + apply (rule allI) + apply (rule conseqPre) + apply (simp add: throwError_def return_def split) + apply vcg + apply (clarsimp simp add: exception_defs lookup_fault_lift_def) + apply (simp split: if_split) + apply (vcg strip_guards=true) + apply (clarsimp simp: cap_get_tag_isCap isCap_simps) + done +next + case True + + note word_neq_0_conv [simp del] + + from True show ?thesis + apply - + apply (cinit' simp add: whileAnno_def ucast_id) + -- "This is done here as init lift usually throws away the relationship between nodeCap_' s and nodeCap. Normally + this OK, but the induction messes with everything :(" + apply (rule ccorres_abstract [where xf' = nodeCap_']) + apply ceqv + apply (rename_tac "nodeCap") + apply (rule ccorres_abstract [where xf' = n_bits_']) + apply ceqv + apply (rename_tac "n_bits") + apply (rule ccorres_abstract [where xf' = capptr_']) + apply ceqv + apply (rename_tac "capptr") + apply (rule_tac P = "capptr = cptr' \ ccap_relation cap' nodeCap" in ccorres_gen_asm2) + apply (erule conjE) + apply (erule_tac t = capptr in ssubst) + apply csymbr+ + apply (simp add: cap_get_tag_isCap split del: if_split) + apply (thin_tac "ret__unsigned_longlong = X" for X) + apply (rule ccorres_split_throws [where P = "?P"]) + apply (rule_tac G' = "\w_rightsMask. ({s. nodeCap_' s = nodeCap} + \ {s. unat (n_bits_' s) = guard'})" + in ccorres_abstract [where xf' = w_rightsMask_']) + apply (rule ceqv_refl) + apply (rule_tac r' = "?rvr" in + ccorres_rel_imp [where xf' = rab_xf]) + defer + apply (case_tac x) + apply clarsimp + apply clarsimp + apply (rule_tac I = "{s. cap_get_tag (nodeCap_' s) = scast cap_cnode_cap}" + in HoarePartial.While [unfolded whileAnno_def, OF subset_refl]) + apply (vcg strip_guards=true) -- "takes a while" + apply clarsimp + apply simp + apply (clarsimp simp: cap_get_tag_isCap to_bool_def) + -- "Main thm" + proof (induct cap' cptr' guard' rule: resolveAddressBits.induct [case_names ind]) + case (ind cap cptr guard) + + note conj_refl = conjI [OF refl refl] + have imp_rem: "\P X. P \ P \ (P \ X = X)" by clarsimp + have imp_rem': "\P R X. P \ R \ P \ R \ (P \ R \ X = X)" by clarsimp + note conj_refl_r = conjI [OF _ refl] + + have getSlotCap_in_monad: + "\a b p rs s. ((a, b) \ fst (getSlotCap p s)) = + (option_map cteCap (ctes_of s p) = Some a + \ b = s)" + apply (simp add: getSlotCap_def return_def bind_def objBits_simps split_def) + apply rule + apply (clarsimp simp: in_getCTE_cte_wp_at' cte_wp_at_ctes_of) + apply clarsimp + apply (subgoal_tac "cte_wp_at' (op = z) p s") + apply (clarsimp simp: getCTE_def cte_wp_at'_def) + apply (simp add: cte_wp_at_ctes_of) + done + + note ih = ind.hyps[simplified, simplified in_monad + getSlotCap_in_monad locateSlot_conv stateAssert_def, simplified] + + have gsCNodes: "\s bits p x P Q. bits = capCNodeBits cap \ capCNodeBits cap < 64 \ + (case gsCNodes (s \ gsCNodes := [p \ bits ] \) p of None \ False + | Some n \ ((n = capCNodeBits cap \ Q n)) + \ (x && mask bits :: machine_word) < 2 ^ n) \ P" + by (clarsimp simp: word_size and_mask_less_size) + + have case_into_if: + "\c f g. (case c of CNodeCap _ _ _ _ \ f | _ \ g) = (if isCNodeCap c then f else g)" + by (case_tac c, simp_all add: isCap_simps) + + note [split del] = if_split + + have gbD: "\guardBits cap cap'. \ guardBits = capCNodeGuardSize_CL (cap_cnode_cap_lift cap'); + ccap_relation cap cap'; isCNodeCap cap \ + \ unat guardBits = capCNodeGuardSize cap \ capCNodeGuardSize cap < 64" + apply (simp add: cap_get_tag_isCap[symmetric]) + apply (frule(1) cap_get_tag_CNodeCap [THEN iffD1]) + apply simp + apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap) + apply (rule order_le_less_trans, rule word_le_nat_alt[THEN iffD1], + rule word_and_le1) + apply (simp add: mask_def) + done + + have cgD: "\capGuard cap cap'. \ capGuard = capCNodeGuard_CL (cap_cnode_cap_lift cap'); + ccap_relation cap cap'; isCNodeCap cap \ \ capGuard = capCNodeGuard cap" + apply (frule cap_get_tag_CNodeCap [THEN iffD1]) + apply (simp add: cap_get_tag_isCap) + apply simp + done + + have rbD: "\radixBits cap cap'. \ radixBits = capCNodeRadix_CL (cap_cnode_cap_lift cap'); + ccap_relation cap cap'; isCNodeCap cap \ + \ unat radixBits = capCNodeBits cap \ capCNodeBits cap < 64" + apply (simp add: cap_get_tag_isCap[symmetric]) + apply (frule(1) cap_get_tag_CNodeCap [THEN iffD1]) + apply simp + apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap) + apply (rule order_le_less_trans, rule word_le_nat_alt[THEN iffD1], + rule word_and_le1) + apply (simp add: mask_def) + done + + have rxgd: + "\cap cap'. \ ccap_relation cap cap'; isCNodeCap cap \ + \ unat (capCNodeRadix_CL (cap_cnode_cap_lift cap') + + capCNodeGuardSize_CL (cap_cnode_cap_lift cap')) + = unat (capCNodeRadix_CL (cap_cnode_cap_lift cap')) + + unat (capCNodeGuardSize_CL (cap_cnode_cap_lift cap'))" + apply (simp add: cap_get_tag_isCap[symmetric]) + apply (frule(1) cap_get_tag_CNodeCap [THEN iffD1]) + apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap) + apply (subst unat_plus_simple[symmetric], subst no_olen_add_nat) + apply (rule order_le_less_trans, rule add_le_mono) + apply (rule word_le_nat_alt[THEN iffD1], rule word_and_le1)+ + apply (simp add: mask_def) + done + + (* Move outside this context? *) + note cap_simps = rxgd cgD [OF refl] + rbD [OF refl, THEN conjunct1] rbD [OF refl, THEN conjunct2] + gbD [OF refl, THEN conjunct1] gbD [OF refl, THEN conjunct2] + + have cond1: "\(nb :: machine_word) guardBits capGuard. + \unat nb = guard; unat guardBits = capCNodeGuardSize cap; capGuard = capCNodeGuard cap; + guard \ 64\ + \ \s s'. + (s, s') \ rf_sr \ True \ True \ + (\ (capCNodeGuardSize cap \ guard \ + (cptr >> guard - capCNodeGuardSize cap) && + mask (capCNodeGuardSize cap) = + capCNodeGuard cap)) = + (s' \ \nb < guardBits \ + (cptr >> unat (nb - guardBits && 0x3F)) && + 2 ^ unat guardBits - 1 \ capGuard\)" + apply (subst not_le [symmetric]) + apply (clarsimp simp: mask_def unat_of_nat Collect_const_mem) + apply (cases "capCNodeGuardSize cap = 0") + apply (simp add: word_le_nat_alt) + apply (subgoal_tac "(0x3F :: machine_word) = mask 6") + apply (erule ssubst [where t = "0x3F"]) + apply (simp add: less_mask_eq word_less_nat_alt word_le_nat_alt) + apply (subst imp_cong) + apply (rule refl) + prefer 2 + apply (rule refl) + apply (subst less_mask_eq) + apply (simp add: word_less_nat_alt word_le_nat_alt unat_sub) + apply (simp add: word_less_nat_alt word_le_nat_alt unat_sub) + apply (simp add: mask_def) + done + + have cond2: "\nb (radixBits :: machine_word) (guardBits :: machine_word). + \ unat nb = guard; unat radixBits = capCNodeBits cap; capCNodeBits cap < 64; capCNodeGuardSize cap < 32; + unat guardBits = capCNodeGuardSize cap \ \ + \s s'. (s, s') \ rf_sr \ True \ True \ + (guard < capCNodeBits cap + capCNodeGuardSize cap) = (s' \ \nb < radixBits + guardBits\)" + by (simp add: Collect_const_mem word_less_nat_alt unat_word_ariths) + + have cond3: "\nb (radixBits :: machine_word) (guardBits :: machine_word). + \ unat nb = guard; unat radixBits = capCNodeBits cap; capCNodeBits cap < 64; capCNodeGuardSize cap < 32; + unat guardBits = capCNodeGuardSize cap; + \ guard < capCNodeBits cap + capCNodeGuardSize cap \ \ + \s s'. (s, s') \ rf_sr \ True \ True \ + (guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \ \nb \ radixBits + guardBits\)" + by (simp add: Collect_const_mem word_le_nat_alt unat_word_ariths) + + have cond4: + "\rva nodeCapb ret__unsigned_long. + \ ccap_relation rva nodeCapb; ret__unsigned_long = cap_get_tag nodeCapb\ + \ \s s'. (s, s') \ rf_sr \ True \ True \ (\ isCNodeCap rva) = (s' \ \ret__unsigned_long \ scast cap_cnode_cap\)" + by (simp add: cap_get_tag_isCap Collect_const_mem) + + let ?p = "(capCNodePtr cap + 0x20 * ((cptr >> guard - (capCNodeBits cap + capCNodeGuardSize cap)) && + mask (capCNodeBits cap)))" + + have n_bits_guard: "\nb :: machine_word. \ guard \ 64; unat nb = guard \ \ unat (nb && mask 6) = guard" + apply (subgoal_tac "nb \ 64") + apply (clarsimp) + apply (rule less_mask_eq) + apply (erule order_le_less_trans) + apply simp + sorry (* + apply (simp add: word_le_nat_alt) + done *) + + have mask6_eqs: + "\cap ccap. \ ccap_relation cap ccap; isCNodeCap cap \ + \ (capCNodeRadix_CL (cap_cnode_cap_lift ccap) + capCNodeGuardSize_CL (cap_cnode_cap_lift ccap)) && mask 6 + = capCNodeRadix_CL (cap_cnode_cap_lift ccap) + capCNodeGuardSize_CL (cap_cnode_cap_lift ccap)" + "\cap ccap. \ ccap_relation cap ccap; isCNodeCap cap \ + \ capCNodeRadix_CL (cap_cnode_cap_lift ccap) && mask 6 = capCNodeRadix_CL (cap_cnode_cap_lift ccap)" + "\cap ccap. \ ccap_relation cap ccap; isCNodeCap cap \ + \ capCNodeGuardSize_CL (cap_cnode_cap_lift ccap) && mask 6 = capCNodeGuardSize_CL (cap_cnode_cap_lift ccap)" + apply (frule(1) rxgd) + defer + apply (simp_all add: cap_cnode_cap_lift_def cap_get_tag_isCap[symmetric] + cap_lift_cnode_cap) + apply (rule less_mask_eq + | rule order_le_less_trans, (rule word_and_le1)+ + | simp add: mask_def)+ + apply (simp add: word_less_nat_alt) + apply (rule order_le_less_trans, rule add_le_mono) + apply (rule word_le_nat_alt[THEN iffD1], rule word_and_le1)+ + apply simp + sorry + + have gm: "\(nb :: machine_word) cap cap'. \ unat nb = guard; ccap_relation cap cap'; isCNodeCap cap \ + \ nb \ capCNodeRadix_CL (cap_cnode_cap_lift cap') + + capCNodeGuardSize_CL (cap_cnode_cap_lift cap') + \ unat (nb - + (capCNodeRadix_CL (cap_cnode_cap_lift cap') + + capCNodeGuardSize_CL (cap_cnode_cap_lift cap'))) + = guard - (capCNodeBits cap + capCNodeGuardSize cap)" + sorry (* + apply (simp add: unat_sub) + apply (subst unat_plus_simple[THEN iffD1]) + apply (subst no_olen_add_nat) + apply (simp add: cap_lift_cnode_cap cap_cnode_cap_lift_def + cap_get_tag_isCap[symmetric] mask_def) + apply (rule order_le_less_trans, rule add_le_mono) + apply (rule word_le_nat_alt[THEN iffD1], rule word_and_le1)+ + apply simp + apply (simp add: cap_simps) + done *) + + note if_cong[cong] + show ?case + using ind.prems + apply - + apply (rule iffD1 [OF ccorres_expand_while_iff]) + apply (subst resolveAddressBits.simps) + apply (unfold case_into_if) + apply (simp add: Let_def ccorres_cond_iffs split del: if_split) + apply (rule ccorres_rhs_assoc)+ + apply (cinitlift nodeCap_' n_bits_') + apply (erule_tac t = nodeCapa in ssubst) + apply (rule ccorres_guard_imp2) + apply (rule ccorres_gen_asm [where P="0 < capCNodeBits cap \ 0 < capCNodeGuardSize cap"]) + apply (rule ccorres_assertE) + apply (csymbr | rule iffD2 [OF ccorres_seq_skip])+ + apply (rule ccorres_Guard_Seq)+ + apply csymbr + -- "handle the stateAssert in locateSlotCap very carefully" + apply (simp(no_asm) only: liftE_bindE[where a="locateSlotCap a b" for a b]) + apply (rule ccorres_locateSlotCap_push[rotated]) + apply (simp add: unlessE_def) + apply (rule hoare_pre, wp, simp) + -- "Convert guardBits, radixBits and capGuard to their Haskell versions" + apply (drule (2) cgD, drule (2) rbD, drule (2) gbD) + apply (elim conjE) + apply (rule ccorres_gen_asm [where P = "guard \ 64"]) + apply (rule ccorres_split_unless_throwError_cond [OF cond1], assumption+) + apply (rule rab_failure_case_ccorres, vcg, rule conseqPre, vcg) + apply clarsimp + apply (rule ccorres_locateSlotCap_push[rotated]) + apply (rule hoare_pre, wp whenE_throwError_wp, simp) + apply (rule ccorres_split_when_throwError_cond [OF cond2], assumption+) + sorry (* + apply (rule rab_failure_case_ccorres, vcg, rule conseqPre, vcg) + apply clarsimp + apply (rule ccorres_Guard_Seq)+ + apply csymbr + apply csymbr + apply (simp only: locateSlotCap_def Let_def if_True) + apply (rule ccorres_split_nothrow) + apply (rule locateSlotCNode_ccorres[where xf="slot_'" and xfu="slot_'_update"], + simp+)[1] + apply ceqv + apply (rename_tac rv slot) + apply (erule_tac t = slot in ssubst) + apply (simp del: Collect_const) + apply (rule ccorres_if_cond_throws [OF cond3], assumption+) + apply (rule ccorres_rhs_assoc)+ + apply csymbr+ + apply (rule ccorres_return_CE, simp_all)[1] + apply (rule ccorres_Guard_Seq) + apply (rule ccorres_basic_srnoop2, simp) + apply csymbr + apply (ctac pre: ccorres_liftE_Seq) + apply (rename_tac rva nodeCapa) + apply csymbr + apply (rule ccorres_if_cond_throws2 [OF cond4], assumption+) + apply (rule ccorres_rhs_assoc)+ + apply csymbr+ + apply (rule ccorres_return_CE, simp_all)[1] + apply (frule_tac v1 = rva in iffD1 [OF isCap_simps(4)]) + apply (elim exE) + apply (rule_tac + Q = "\s. option_map cteCap (ctes_of s ?p) = Some rva" + and F = "\s s'. + (option_map cteCap (ctes_of s ?p) = Some rva + \ (ccap_relation rva (h_val (hrs_mem (t_hrs_' (globals s'))) (Ptr &(Ptr ?p :: cte_C ptr\[''cap_C'']) :: cap_C ptr))))" + in ccorres_req [where Q' = "\s'. s' \\<^sub>c (Ptr ?p :: cte_C ptr)"]) + apply (thin_tac "rva = X" for X) + apply (clarsimp simp: h_t_valid_clift_Some_iff typ_heap_simps) + apply (rule ccte_relation_ccap_relation) + apply (erule (2) rf_sr_cte_relation) + apply (elim conjE) + apply (rule_tac nodeCap1 = "nodeCapa" in ih, + (simp | rule conjI refl gsCNodes)+)[1] + apply (clarsimp simp: cte_level_bits_def field_simps isCap_simps, fast) + apply (rule refl) + apply assumption + apply assumption + apply assumption + apply vcg + apply (simp add: getSlotCap_def imp_conjR) + apply (wp getCTE_ctes_of | (wp_once hoare_drop_imps))+ + apply (clarsimp simp: Collect_const_mem if_then_simps lookup_fault_lifts cong: imp_cong conj_cong) + apply vcg + apply (vcg strip_guards=true) + apply (simp add: locateSlot_conv) + apply wp + apply vcg + apply (vcg strip_guards=true) + apply (vcg strip_guards=true) + apply (rule conjI) + -- "Haskell guard" + apply (thin_tac "unat n_bits = guard") + apply (clarsimp simp del: imp_disjL) -- "take a while" + apply (intro impI conjI allI) + apply fastforce + apply clarsimp + apply arith + apply (clarsimp simp: isCap_simps cte_level_bits_def + option.split[where P="\x. x"]) + apply (clarsimp simp: isCap_simps valid_cap_simps' cte_level_bits_def + real_cte_at') + apply (clarsimp simp: isCap_simps valid_cap'_def) + -- "C guard" + apply (frule (1) cgD [OF refl], frule (1) rbD [OF refl], frule (1) gbD [OF refl]) + apply (simp add: Collect_const_mem cap_get_tag_isCap exception_defs lookup_fault_lifts + n_bits_guard mask6_eqs word_le_nat_alt word_less_nat_alt gm) + apply (elim conjE) + apply (frule rf_sr_cte_at_valid [where p = + "cte_Ptr (capCNodePtr cap + 0x10 * ((cptr >> guard - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)))", rotated]) + apply simp + apply (erule (1) valid_cap_cte_at') + apply simp + apply (frule(2) gm) + apply (simp add: word_less_nat_alt word_le_nat_alt less_mask_eq) + apply (intro impI conjI allI, simp_all) + apply (simp add: cap_simps) + apply (frule iffD1 [OF cap_get_tag_CNodeCap]) + apply (simp add: cap_get_tag_isCap) + apply (erule ssubst [where t = cap]) + apply simp + apply (simp add: mask_def) + apply (subgoal_tac "capCNodeBits cap \ 0") + apply (clarsimp simp: linorder_not_less cap_simps) + apply (clarsimp simp: isCap_simps valid_cap'_def) + apply (clarsimp simp: linorder_not_less cap_simps) + apply (clarsimp simp: isCap_simps valid_cap'_def) + apply (clarsimp simp: linorder_not_less cap_simps) + apply (clarsimp simp: isCap_simps valid_cap'_def) + apply arith + apply (subgoal_tac "(0x1F :: machine_word) = mask 5") + apply (erule ssubst [where t = "0x1F"]) + apply (subst word_mod_2p_is_mask [symmetric]) + apply simp + apply (simp add: unat_word_ariths) + apply (simp add: mask_def) + done *) + qed +qed + +abbreviation + "lookupSlot_xf \ liftxf errstate lookupSlot_ret_C.status_C + lookupSlot_ret_C.slot_C ret__struct_lookupSlot_ret_C_'" + + +lemma rightsFromWord_spec: + shows "\s. \ \ {s} \ret__struct_seL4_CapRights_C :== PROC rightsFromWord(\w) + \seL4_CapRights_lift \ret__struct_seL4_CapRights_C = cap_rights_from_word_canon \<^bsup>s\<^esup>w \" + apply vcg + apply (simp add: seL4_CapRights_lift_def nth_shiftr mask_shift_simps nth_shiftr + cap_rights_from_word_canon_def from_bool_def word_and_1 eval_nat_numeral + word_sless_def word_sle_def) + done + + +abbreviation + "lookupSlot_rel' \ \(cte, rm) (cte', rm'). cte' = Ptr cte \ rm = cap_rights_to_H (seL4_CapRights_lift rm')" + +(* MOVE *) +lemma cap_rights_to_H_from_word_canon [simp]: + "cap_rights_to_H (cap_rights_from_word_canon wd) = rightsFromWord wd" + unfolding cap_rights_from_word_def rightsFromWord_def + apply (simp add: cap_rights_from_word_canon_def) + apply (simp add: cap_rights_to_H_def) + done + +(* MOVE *) +lemma to_bool_false [simp]: + "to_bool false = False" + unfolding to_bool_def false_def + by simp + +(* MOVE *) +lemma tcb_aligned': + "tcb_at' t s \ is_aligned t 9" + apply (drule obj_at_aligned') + apply (simp add: objBits_simps) + apply (simp add: objBits_simps) + done + +(* FIXME: FROM ArchAcc.thy *) +lemma add_mask_lower_bits: + "\ is_aligned (x :: 'a :: len word) n; \n' \ n. n' < len_of TYPE('a) \ \ p !! n' \ \ x + p && ~~mask n = x" + apply (subst word_plus_and_or_coroll) + apply (rule word_eqI) + apply (clarsimp simp: word_size is_aligned_nth) + apply (erule_tac x=na in allE)+ + apply simp + apply (rule word_eqI) + apply (clarsimp simp: word_size is_aligned_nth nth_mask word_ops_nth_size) + apply (erule_tac x=na in allE)+ + apply (case_tac "na < n") + apply simp + apply simp + done + +(* FIXME x64: fix after tcb bits change *) +lemma tcb_ptr_to_ctcb_ptr_mask [simp]: + assumes tcbat: "tcb_at' thread s" + shows "ptr_val (tcb_ptr_to_ctcb_ptr thread) && 0xFFFFFFFFFFFFF800 = thread" +proof - + have "thread + 2 ^ 10 && ~~ mask 11 = thread" + proof (rule add_mask_lower_bits) + show "is_aligned thread 11" using tcbat sorry + show "\n'\11. n' < len_of TYPE(64) \ \ ((2 :: machine_word) ^ 10) !! n'" by simp + qed + thus ?thesis + unfolding tcb_ptr_to_ctcb_ptr_def ctcb_offset_def + sorry +qed + +abbreviation + "lookupSlot_raw_xf \ + liftxf errstate lookupSlot_raw_ret_C.status_C + lookupSlot_raw_ret_C.slot_C + ret__struct_lookupSlot_raw_ret_C_'" + +definition + lookupSlot_raw_rel :: "machine_word \ cte_C ptr \ bool" +where + "lookupSlot_raw_rel \ \slot slot'. slot' = cte_Ptr slot" + +lemma lookupSlotForThread_ccorres': + "ccorres (lookup_failure_rel \ lookupSlot_raw_rel) lookupSlot_raw_xf + (valid_pspace' and tcb_at' thread) + ({s. capptr_' s = cptr} \ {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) [] + (lookupSlotForThread thread cptr) (Call lookupSlot_'proc)" + apply (cinit lift: capptr_' thread_' + simp add: getThreadCSpaceRoot_def locateSlot_conv + returnOk_liftE [symmetric] split_def) + apply (ctac pre: ccorres_liftE_Seq) + apply (ctac (no_vcg) add: resolveAddressBits_ccorres) + apply csymbr+ + apply (ctac add: ccorres_return_CE) + apply csymbr+ + apply (ctac add: ccorres_return_C_errorE) + apply wp+ + apply vcg + apply (rule conjI) + apply (clarsimp simp add: conj_comms word_size tcbSlots Kernel_C.tcbCTable_def) + apply (rule conjI) + apply fastforce + apply (erule tcb_at_cte_at') + apply (clarsimp simp add: Collect_const_mem errstate_def tcbSlots + Kernel_C.tcbCTable_def word_size lookupSlot_raw_rel_def + word_sle_def + split del: if_split) + sorry + +lemma lookupSlotForThread_ccorres[corres]: + "ccorres (lookup_failure_rel \ lookupSlot_raw_rel) lookupSlot_raw_xf + (invs' and tcb_at' thread) + (UNIV \ {s. capptr_' s = cptr} \ {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) [] + (lookupSlotForThread thread cptr) (Call lookupSlot_'proc)" + apply (rule ccorres_guard_imp2, rule lookupSlotForThread_ccorres') + apply fastforce + done + +end +end