Skip to content

Commit

Permalink
fastpath_c: rule_tac in misaligns
Browse files Browse the repository at this point in the history
  • Loading branch information
@Xaphiosis
Xaphiosis committed Mar 25, 2024
1 parent 119f850 commit f1391d6
Showing 1 changed file with 14 additions and 14 deletions.
28 changes: 14 additions & 14 deletions proof/crefine/AARCH64/Fastpath_C.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -235,9 +235,9 @@ lemma lookup_fp_ccorres':
ccap_relation_NullCap_iff)
apply (clarsimp simp del: Collect_const)
apply (rule_tac P="valid_cap' cap and valid_objs'"
and P'="{s. ccap_relation cap (cap_' s) \<and> isCNodeCap cap}
\<inter> {s. bits_' s = 64 - of_nat bits \<and> bits \<le> 64 \<and> bits \<noteq> 0}" (* FIXME AARCH64 64 *)
in ccorres_inst)
and P'="{s. ccap_relation cap (cap_' s) \<and> isCNodeCap cap}
\<inter> {s. bits_' s = 64 - of_nat bits \<and> bits \<le> 64 \<and> bits \<noteq> 0}" (* FIXME AARCH64 64 *)
in ccorres_inst)
apply (thin_tac "isCNodeCap cap")
defer
apply vcg
Expand Down Expand Up @@ -278,7 +278,7 @@ lemma lookup_fp_ccorres':
\<and> unat (capCNodeGuardSize_CL (cap_cnode_cap_lift ccap)
+ capCNodeRadix_CL (cap_cnode_cap_lift ccap))
= capCNodeGuardSize acap + capCNodeBits acap"
in Corres_UL_C.ccorres_req)
in Corres_UL_C.ccorres_req)
apply (clarsimp simp: cap_get_tag_isCap[symmetric])
apply (clarsimp simp: cap_lift_cnode_cap cap_to_H_simps valid_cap'_def
capAligned_def cap_cnode_cap_lift_def objBits_simps
Expand All @@ -305,7 +305,7 @@ lemma lookup_fp_ccorres':
apply (rule ccorres_drop_cutMon_bind, rule ccorres_stateAssert)

apply (rule_tac P="abits < capCNodeBits acap + capCNodeGuardSize acap"
in ccorres_case_bools2)
in ccorres_case_bools2)
apply (rule ccorres_drop_cutMon)
apply csymbr+
apply (rule ccorres_symb_exec_r)
Expand Down Expand Up @@ -381,7 +381,7 @@ lemma lookup_fp_ccorres':
apply (simp add: liftE_bindE locateSlot_conv
del: Collect_const)
apply (rule_tac P="abits = capCNodeBits acap + capCNodeGuardSize acap"
in ccorres_case_bools2)
in ccorres_case_bools2)
apply (rule ccorres_drop_cutMon)
apply (simp del: Collect_const)
apply (simp add: liftE_def getSlotCap_def del: Collect_const)
Expand All @@ -402,7 +402,7 @@ lemma lookup_fp_ccorres':
apply (rule ccorres_cond_false_seq)
apply (simp del: Collect_const)
apply (rule_tac P'="{s. cap_' s = getCTE_cap}"
in ccorres_from_vcg_throws[where P=\<top>])
in ccorres_from_vcg_throws[where P=\<top>])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: word_sle_def return_def returnOk_def
isRight_def)
Expand Down Expand Up @@ -430,7 +430,7 @@ lemma lookup_fp_ccorres':
apply (rule ccorres_cutMon)
apply (simp add: cutMon_walk_if)
apply (rule_tac Q'="\<lambda>s. ret__int_' s = from_bool (isCNodeCap rv)"
in ccorres_cond_both'[where Q=\<top>])
in ccorres_cond_both'[where Q=\<top>])
apply (clarsimp simp: from_bool_0)
apply (rule ccorres_rhs_assoc)+
apply (rule_tac P="ccorres r xf Gd Gd' hs a" for r xf Gd Gd' hs a in rsubst)
Expand Down Expand Up @@ -1373,7 +1373,7 @@ lemma fastpath_enqueue_ccorres:
split: if_split)
apply (rule conjI)
apply (rule_tac S="tcb_ptr_to_ctcb_ptr ` set (ksCurThread \<sigma> # list)"
in cpspace_relation_ep_update_an_ep,
in cpspace_relation_ep_update_an_ep,
assumption+)
apply (simp add: cendpoint_relation_def Let_def EPState_Recv_def
tcb_queue_relation'_def)
Expand Down Expand Up @@ -2133,7 +2133,7 @@ proof -
and obj_at' ((=) destPrio \<circ> tcbPriority)
(hd (epQueue send_ep))
and (\<lambda>s. ksCurThread s = curThread)"
in ccorres_cross_over_guard)
in ccorres_cross_over_guard)
apply (rule_tac xf'=ret__int_' and val="from_bool (destPrio < curPrio)"
and R="obj_at' ((=) curPrio \<circ> tcbPriority) curThread
and obj_at' ((=) destPrio \<circ> tcbPriority)
Expand Down Expand Up @@ -2189,7 +2189,7 @@ proof -
apply (rule_tac val="from_bool (\<not> (capEPCanGrant (theRight luRet)
\<or> capEPCanGrantReply (theRight luRet)))"
and xf'=ret__int_' and R=\<top> and R'=UNIV
in ccorres_symb_exec_r_known_rv)
in ccorres_symb_exec_r_known_rv)
apply (clarsimp, rule conseqPre, vcg)
apply (fastforce simp: ccap_relation_ep_helpers from_bool_eq_if')
apply ceqv
Expand Down Expand Up @@ -2274,7 +2274,7 @@ proof -
rule_tac P="replySlot
= cte_Ptr (curThread
+ (tcbReplySlot << cte_level_bits))"
in ccorres_gen_asm2)
in ccorres_gen_asm2)
apply (rule ccorres_move_const_guard
ccorres_move_array_assertion_tcb_ctes
ccorres_move_c_guard_tcb_ctes)+
Expand Down Expand Up @@ -2324,7 +2324,7 @@ proof -
apply (subst aligned_add_aligned, erule tcb_aligned',
simp add: is_aligned_def, simp add: objBits_defs, simp)
apply (rule_tac x="hd (epQueue send_ep) + v" for v
in cmap_relationE1[OF cmap_relation_cte], assumption+)
in cmap_relationE1[OF cmap_relation_cte], assumption+)
apply (clarsimp simp: typ_heap_simps' updateMDB_def Let_def)
apply (subst if_not_P)
apply clarsimp
Expand All @@ -2343,7 +2343,7 @@ proof -
+ (tcbReplySlot << cte_level_bits))
and tcb_at' (hd (epQueue send_ep))
and (no_0 o ctes_of)"
in ccorres_from_vcg[where P'=UNIV])
in ccorres_from_vcg[where P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: cte_wp_at_ctes_of size_of_def
tcb_cnode_index_defs tcbCallerSlot_def
Expand Down

0 comments on commit f1391d6

Please sign in to comment.