Skip to content

Commit

Permalink
aarch64 crefine: minimal fixups for arch-split up to InvariantUpdates_H
Browse files Browse the repository at this point in the history
Includes tcb_cte_cases tweaks, and a bit of effort to minimise Arch
spillage in Move_C.

Signed-off-by: Rafal Kolanski <[email protected]>
  • Loading branch information
Xaphiosis committed Dec 9, 2024
1 parent 375d6a5 commit e6fcea9
Show file tree
Hide file tree
Showing 6 changed files with 64 additions and 40 deletions.
1 change: 1 addition & 0 deletions proof/crefine/AARCH64/ADT_C.thy
Original file line number Diff line number Diff line change
Expand Up @@ -787,6 +787,7 @@ lemma map_to_ctes_tcb_ctes:
"ctes_of s' = ctes_of s \<Longrightarrow>
ko_at' tcb p s \<Longrightarrow> ko_at' tcb' p s' \<Longrightarrow>
\<forall>x\<in>ran tcb_cte_cases. fst x tcb' = fst x tcb"
supply raw_tcb_cte_cases_simps[simp] (* FIXME arch-split: legacy, try use tcb_cte_cases_neqs *)
apply (clarsimp simp add: ran_tcb_cte_cases)
apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKO_opt_tcb
split: kernel_object.splits)
Expand Down
18 changes: 9 additions & 9 deletions proof/crefine/AARCH64/ArchMove_C.thy
Original file line number Diff line number Diff line change
Expand Up @@ -34,15 +34,6 @@ lemma ps_clear_is_aligned_ksPSpace_None:
power_overflow)
by assumption

lemma ps_clear_is_aligned_ctes_None:
assumes "ps_clear p tcbBlockSizeBits s"
and "is_aligned p tcbBlockSizeBits"
shows "ksPSpace s (p + 2*2^cteSizeBits) = None"
and "ksPSpace s (p + 3*2^cteSizeBits) = None"
and "ksPSpace s (p + 4*2^cteSizeBits) = None"
by (auto intro: assms ps_clear_is_aligned_ksPSpace_None
simp: objBits_defs mask_def)+

lemma word_shift_by_3:
"x * 8 = (x::'a::len word) << 3"
by (simp add: shiftl_t2n)
Expand Down Expand Up @@ -89,6 +80,15 @@ lemmas unat64_eq_of_nat = unat_eq_of_nat[where 'a=64, folded word_bits_def]

context begin interpretation Arch .

lemma ps_clear_is_aligned_ctes_None:
assumes "ps_clear p tcbBlockSizeBits s"
and "is_aligned p tcbBlockSizeBits"
shows "ksPSpace s (p + 2*2^cteSizeBits) = None"
and "ksPSpace s (p + 3*2^cteSizeBits) = None"
and "ksPSpace s (p + 4*2^cteSizeBits) = None"
by (auto intro: assms ps_clear_is_aligned_ksPSpace_None
simp: objBits_defs mask_def)+

crunch archThreadGet
for inv'[wp]: P

Expand Down
2 changes: 1 addition & 1 deletion proof/crefine/AARCH64/Finalise_C.thy
Original file line number Diff line number Diff line change
Expand Up @@ -2391,7 +2391,7 @@ lemma associateVCPUTCB_ccorres:
apply vcg
apply wpsimp
apply (vcg exspec=dissociateVCPUTCB_modifies)
apply ((wpsimp wp: hoare_vcg_all_lift hoare_drop_imps
apply ((wpsimp wp: hoare_vcg_all_lift hoare_drop_imps valid_arch_tcb_lift'
| strengthen invs_valid_objs' invs_arch_state')+)[1]
apply (vcg exspec=dissociateVCPUTCB_modifies)
apply (rule_tac Q'="\<lambda>_. invs' and vcpu_at' vcpuptr and tcb_at' tptr" in hoare_post_imp)
Expand Down
4 changes: 2 additions & 2 deletions proof/crefine/AARCH64/IsolatedThreadAction.thy
Original file line number Diff line number Diff line change
Expand Up @@ -142,11 +142,11 @@ end

lemmas getObject_return_tcb
= getObject_return[OF meta_eq_to_obj_eq, OF loadObject_tcb,
unfolded objBits_simps, simplified]
unfolded gen_objBits_simps, simplified]

lemmas setObject_modify_tcb
= setObject_modify[OF _ meta_eq_to_obj_eq, OF _ updateObject_tcb,
unfolded objBits_simps, simplified]
unfolded gen_objBits_simps, simplified]

lemma partial_overwrite_fun_upd:
"inj idx \<Longrightarrow>
Expand Down
4 changes: 2 additions & 2 deletions proof/crefine/AARCH64/Recycle_C.thy
Original file line number Diff line number Diff line change
Expand Up @@ -502,10 +502,10 @@ lemma heap_to_user_data_in_user_mem'[simp]:
apply (subst is_aligned_add_helper[THEN conjunct2,where n1 = 3])
apply (erule aligned_add_aligned)
apply (simp add: is_aligned_mult_triv2[where n = 3,simplified])
apply (clarsimp simp: objBits_simps AARCH64.pageBits_def)
apply (clarsimp simp: gen_objBits_simps AARCH64.pageBits_def)
apply simp
apply (rule is_aligned_add_helper[THEN conjunct2])
apply (simp add: AARCH64.pageBits_def objBits_simps)
apply (simp add: AARCH64.pageBits_def gen_objBits_simps)
apply (rule word_less_power_trans2[where k = 3,simplified])
apply (rule less_le_trans[OF ucast_less])
apply simp+
Expand Down
75 changes: 49 additions & 26 deletions proof/crefine/Move_C.thy
Original file line number Diff line number Diff line change
Expand Up @@ -131,13 +131,11 @@ lemma length_Suc_0_conv:

lemma imp_ignore: "B \<Longrightarrow> A \<longrightarrow> B" by blast

lemma cteSizeBits_eq:
"cteSizeBits = cte_level_bits"
by (simp add: cte_level_bits_def cteSizeBits_def)
lemmas cteSizeBits_eq = cteSizeBits_cte_level_bits

lemma cteSizeBits_le_cte_level_bits[simp]:
"cteSizeBits \<le> cte_level_bits"
by (simp add: cte_level_bits_def cteSizeBits_def)
by (simp add: cteSizeBits_eq)

lemma unat_ucast_prio_mask_simp[simp]:
"unat (ucast (p::priority) && mask m :: machine_word) = unat (p && mask m)"
Expand Down Expand Up @@ -344,14 +342,29 @@ lemma word_eq_cast_unsigned:
"(x = y) = (UCAST ('a signed \<rightarrow> ('a :: len)) x = ucast y)"
by (simp add: word_eq_iff nth_ucast)

(* tcbIPCBufferSlot is last slot in TCB *)
(* FIXME arch-split: Arch is needed for wordSizeCase, proof is same on all arches *)
lemma (in Arch) cteSizeBits_2ptcbBlockSizeBits[simplified tcbIPCBufferSlot_def]:
"n \<le> tcbIPCBufferSlot \<Longrightarrow> n << cteSizeBits < 2 ^ tcbBlockSizeBits"
unfolding tcbIPCBufferSlot_def tcbBlockSizeBits_def cteSizeBits_def
apply (simp only: wordSizeCase_simp)
apply (rule shiftl_less_t2n; simp)
apply unat_arith
done

requalify_facts Arch.cteSizeBits_2ptcbBlockSizeBits

lemmas zero_less_2p_tcbBlockSizeBits = cteSizeBits_2ptcbBlockSizeBits[where n=0, simplified]

lemma ran_tcb_cte_cases:
"ran tcb_cte_cases =
{(Structures_H.tcbCTable, tcbCTable_update),
(Structures_H.tcbVTable, tcbVTable_update),
(Structures_H.tcbReply, tcbReply_update),
(Structures_H.tcbCaller, tcbCaller_update),
(tcbIPCBufferFrame, tcbIPCBufferFrame_update)}"
by (auto simp add: tcb_cte_cases_def cteSizeBits_def split: if_split_asm)
unfolding tcb_cte_cases_def
by (auto split: if_split_asm simp: tcb_cte_cases_neqs)

lemma user_data_at_ko:
"typ_at' UserDataT p s \<Longrightarrow> ko_at' UserData p s"
Expand Down Expand Up @@ -568,7 +581,7 @@ lemma threadGet_again:
(threadGet ext t >>= n) s' = n rv s'"
apply (clarsimp simp add: threadGet_def liftM_def in_monad)
apply (frule use_valid [OF _ getObject_obj_at'])
apply (simp add: objBits_simps')+
apply (simp add: gen_objBits_simps tcbBlockSizeBits_def)+ (* FIXME arch-split: tcbBlockSizeBits *)
apply (frule getObject_tcb_det)
apply (clarsimp simp: bind_def split_def)
apply (insert no_fail_getObject_tcb)
Expand Down Expand Up @@ -623,16 +636,17 @@ lemma mapM_only_length:

lemma tcb_aligned':
"tcb_at' t s \<Longrightarrow> is_aligned t tcbBlockSizeBits"
apply (drule obj_at_aligned')
apply (simp add: objBits_simps)
apply (simp add: objBits_simps)
done
by (drule obj_at_aligned'; simp add: gen_objBits_simps)

lemma cte_at_0' [dest!]:
(* identical proof on all arches *)
lemma (in Arch) cte_at_0'[dest!]:
"\<lbrakk> cte_at' 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> False"
apply (clarsimp simp: cte_wp_at_obj_cases')
by (auto simp: tcb_cte_cases_def is_aligned_def objBits_simps' dest!:tcb_aligned' split: if_split_asm)

requalify_facts Arch.cte_at_0'
lemmas [dest!] = cte_at_0'

lemma getMessageInfo_le3:
"\<lbrace>\<top>\<rbrace> getMessageInfo sender \<lbrace>\<lambda>rv s. unat (msgExtraCaps rv) \<le> 3\<rbrace>"
including no_pre
Expand Down Expand Up @@ -1119,45 +1133,54 @@ lemma updateObject_cte_tcb:
return (KOTCB (updF (\<lambda>_. ctea) tcb))
od)"
using tc unfolding tcb_cte_cases_def
apply -
apply (clarsimp simp add: updateObject_cte Let_def
tcb_cte_cases_def objBits_simps' tcbSlots shiftl_t2n
split: if_split_asm cong: if_cong)
done
by (clarsimp simp: updateObject_cte Let_def tcb_cte_cases_neqs gen_objBits_simps tcbSlots
split: if_split_asm
cong: if_cong)

lemma self_elim:
"\<And>P Q. \<lbrakk> P \<Longrightarrow> Q; P \<rbrakk> \<Longrightarrow> Q"
by blast

lemma tcb_cte_cases_in_range1:
assumes tc:"tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "x \<le> y"
proof -
note objBits_defs [simp]

from tc obtain q where yq: "y = x + q" and qv: "q < 2 ^ tcbBlockSizeBits"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
by (clarsimp simp: diff_eq_eq tcbSlot_defs
simp del: shiftl_1
elim!: self_elim
intro!: cteSizeBits_2ptcbBlockSizeBits zero_less_2p_tcbBlockSizeBits
split: if_split_asm)

have "x \<le> x + 2 ^ tcbBlockSizeBits - 1" using al
by (rule is_aligned_no_overflow)

hence "x \<le> x + q" using qv
apply simp
apply unat_arith
apply simp
done
by unat_arith

thus ?thesis using yq by simp
qed

lemma tcbBlockSizeBits_word_less_sub_le:
fixes x :: machine_word
shows "(x \<le> 2 ^ tcbBlockSizeBits - 1) = (x < 2 ^ tcbBlockSizeBits)"
unfolding tcbBlockSizeBits_def
by (subst word_less_sub_le; simp)

lemma tcb_cte_cases_in_range2:
assumes tc: "tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "y \<le> x + 2 ^ tcbBlockSizeBits - 1"
proof -
note objBits_defs [simp]

from tc obtain q where yq: "y = x + q" and qv: "q \<le> 2 ^ tcbBlockSizeBits - 1"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
by (clarsimp simp: diff_eq_eq tcbSlot_defs tcbBlockSizeBits_word_less_sub_le
simp del: shiftl_1
elim!: self_elim
intro!: cteSizeBits_2ptcbBlockSizeBits zero_less_2p_tcbBlockSizeBits
split: if_split_asm)

have "x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)" using qv
apply (rule word_plus_mono_right)
Expand Down

0 comments on commit e6fcea9

Please sign in to comment.