adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

backport changes to ARM proofs from X64 work in progress 

- replace ARM-specific constants and types with aliases which can be
  instantiated separately for each architecture.
- expand lib with lemmas used in X64 proofs.
- simplify some proofs.

Also-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
This commit is contained in:
Joel Beeren 2017-01-26 14:20:48 +11:00 committed by Matthew Brecknell
parent ad6bd61332
commit 3dafec7d46
86 changed files with 1157 additions and 975 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

63
.gitignore vendored
View File

@ -7,45 +7,36 @@
*.lev
*#*#
spec/cspec/c/32/
spec/cspec/c/api/
spec/cspec/c/arch/
spec/cspec/c/kernel_all.c
spec/cspec/c/kernel_all.c_pp
spec/cspec/c/parsetab.py
spec/cspec/c/plat/
spec/cspec/c/sources_list_updated
spec/cspec/c/autoconf.h
/spec/cspec/c/32/
/spec/cspec/c/64/
/spec/cspec/c/api/
/spec/cspec/c/arch/
/spec/cspec/c/kernel_all.c
/spec/cspec/c/kernel_all.c_pp
/spec/cspec/c/parsetab.py
/spec/cspec/c/plat/
/spec/cspec/c/sources_list_updated
/spec/cspec/c/autoconf.h
spec/haskell/doc/**/*.aux
spec/haskell/doc/**/*.bbl
spec/haskell/doc/**/*.blg
spec/haskell/doc/**/*.log
spec/haskell/doc/**/*.mpx
spec/haskell/doc/**/*.out
spec/haskell/doc/**/*.toc
/spec/haskell/doc/**/*.aux
/spec/haskell/doc/**/*.bbl
/spec/haskell/doc/**/*.blg
/spec/haskell/doc/**/*.log
/spec/haskell/doc/**/*.mpx
/spec/haskell/doc/**/*.out
/spec/haskell/doc/**/*.toc
**/CFunDump.txt
**/umm_types.txt
CFunDump.txt
umm_types.txt
tools/autocorres/doc/quickstart/output/
tools/autocorres/sel4.txt
tools/autocorres/tests/ROOT
tools/autocorres/tests/parse-tests/*.thy
tools/autocorres/tests/examples/trace_demo_incr.trace
/tools/autocorres/doc/quickstart/output/
/tools/autocorres/sel4.txt
/tools/autocorres/tests/ROOT
/tools/autocorres/tests/parse-tests/*.thy
/tools/autocorres/tests/examples/trace_demo_incr.trace
tools/c-parser/standalone-parser/table.ML
tools/c-parser/StrictC.grm.desc
tools/c-parser/standalone-parser/ARM/
tools/c-parser/standalone-parser/FAKE64/
tools/c-parser/tools/mllex/mllex
tools/c-parser/tools/mlyacc/mlyacc
tools/c-parser/tools/mlyacc/src/yacc.lex.sml
tools/c-parser/testfiles/ROOT
tools/c-parser/testfiles/umm_types.txt
/tools/haskell-translator/caseconvs-useful
tools/haskell-translator/caseconvs-useful
/camkes/adl-spec/camkes.ML
camkes/adl-spec/camkes.ML
internal
/internal/

8
.licenseignore
View File

@ -65,9 +65,12 @@ spec/haskell/src/SEL4/Object/CNode.lhs-boot
spec/haskell/src/SEL4/Object/Endpoint.lhs-boot
spec/haskell/src/SEL4/Object/ObjectType.lhs-boot
spec/haskell/src/SEL4/Object/TCB.lhs-boot
spec/haskell/src/SEL4/Object/IOPort/X64.lhs-boot
spec/design/version
spec/cspec/c/32/*
spec/cspec/c/64/*
spec/cspec/c/api/*
spec/cspec/c/arch/*
spec/cspec/c/kernel_all.c
@ -151,9 +154,10 @@ tools/c-parser/standalone-parser/*/tokenizer
tools/c-parser/tools/mllex/mllex
tools/c-parser/tools/mlyacc/mlyacc
tools/c-parser/tools/mlyacc/src/yacc.lex.sml
tools/c-parser/testfiles/jiraver473.minfo
tools/c-parser/testfiles/ROOT
tools/c-parser/testfiles/**/*.minfo
tools/c-parser/testfiles/**/ROOT
tools/c-parser/testfiles/umm_types.txt
tools/c-parser/testfiles/modifies_speed.c
tools/haskell-translator/caseconvs-useful
tools/haskell-translator/primrecs

3
lib/LemmaBucket.thy
View File

@ -440,4 +440,7 @@ lemma list_ran_prop:"map_of (map (\<lambda>x. (f x, g x)) xs) i = Some t \<Longr
lemma in_set_enumerate_eq2:"(a, b) \<in> set (enumerate n xs) \<Longrightarrow> (b = xs ! (a - n))"
by (simp add: in_set_enumerate_eq)
lemma subset_eq_notI: "\<lbrakk>a\<in> B;a\<notin> C\<rbrakk> \<Longrightarrow> \<not> B \<subseteq> C"
by auto
end

213
lib/NonDetMonadLemmaBucket.thy
View File

@ -2897,4 +2897,217 @@ lemma hoare_assume_preNF:
"(\<And>s. P s \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!"
by (metis validNF_alt_def)
lemma bexEI: "\<lbrakk>\<exists>x\<in>S. Q x; \<And>x. \<lbrakk>x \<in> S; Q x\<rbrakk> \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. P x" by blast
lemma monad_eq_split:
assumes "\<And>r s. Q r s \<Longrightarrow> f r s = f' r s"
"\<lbrace>P\<rbrace> g \<lbrace>\<lambda>r s. Q r s\<rbrace>"
"P s"
shows "(g >>= f) s = (g >>= f') s"
proof -
have pre: "\<And>rv s'. \<lbrakk>(rv, s') \<in> fst (g s)\<rbrakk> \<Longrightarrow> f rv s' = f' rv s'"
using assms unfolding valid_def
by (erule_tac x=s in allE) auto
show ?thesis
apply (simp add: bind_def image_def)
apply (intro conjI)
apply (rule set_eqI)
apply (clarsimp simp: Union_eq)
apply (rule iffI; elim exEI conjE; simp; elim exEI bexEI; clarsimp simp: pre)
apply (rule iffI; cases "snd (g s)"; simp; elim exEI bexEI; clarsimp simp: pre)
done
qed
lemma monad_eq_split2:
assumes eq: " g' s = g s"
assumes tail:"\<And>r s. Q r s \<Longrightarrow> f r s = f' r s"
and hoare: "\<lbrace>P\<rbrace>g\<lbrace>\<lambda>r s. Q r s\<rbrace>" "P s"
shows "(g>>=f) s = (g'>>= f') s"
proof -
have pre: "\<And>aa bb. \<lbrakk>(aa, bb) \<in> fst (g s)\<rbrakk> \<Longrightarrow> Q aa bb"
using hoare by (auto simp: valid_def)
show ?thesis
apply (simp add:bind_def eq split_def image_def)
apply (rule conjI)
apply (rule set_eqI)
apply (clarsimp simp:Union_eq)
apply (metis pre surjective_pairing tail)
apply (metis pre surjective_pairing tail)
done
qed
lemma monad_eq_split_tail:
"\<lbrakk>f = g;a s = b s\<rbrakk> \<Longrightarrow> (a >>= f) s = ((b >>= g) s)"
by (simp add:bind_def)
definition monad_commute where
"monad_commute P a b \<equiv>
(\<forall>s. (P s \<longrightarrow> ((do x\<leftarrow>a;y\<leftarrow>b; return (x, y) od) s) = ((do y\<leftarrow>b;x\<leftarrow>a; return (x, y) od) s)))"
lemma monad_eq:
"a s = b s \<Longrightarrow> (a >>= g) s = (b >>= g) s"
by (auto simp:bind_def)
lemma monad_commute_simple:
"\<lbrakk>monad_commute P a b;P s\<rbrakk> \<Longrightarrow> ((do x\<leftarrow>a;y\<leftarrow>b; g x y od) s) = ((do y\<leftarrow>b;x\<leftarrow>a; g x y od) s)"
apply (clarsimp simp:monad_commute_def)
apply (drule spec)
apply (erule(1) impE)
apply (drule_tac g = "(\<lambda>t. g (fst t) (snd t))" in monad_eq)
apply (simp add:bind_assoc)
done
lemma commute_commute:
"monad_commute P f h \<Longrightarrow> monad_commute P h f"
apply (simp (no_asm) add: monad_commute_def)
apply (clarsimp)
apply (erule monad_commute_simple[symmetric])
apply simp
done
lemma assert_commute: "monad_commute (K G) (assert G) f"
by (clarsimp simp:assert_def monad_commute_def)
lemma cond_fail_commute: "monad_commute (K (\<not>G)) (when G fail) f"
by (clarsimp simp:when_def fail_def monad_commute_def)
lemma return_commute: "monad_commute \<top> (return a) f"
by (clarsimp simp: return_def bind_def monad_commute_def)
lemma monad_commute_guard_imp:
"\<lbrakk>monad_commute P f h; \<And>s. Q s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> monad_commute Q f h"
by (clarsimp simp:monad_commute_def)
lemma monad_commute_split:
"\<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h;
\<lbrace>P'\<rbrace> h \<lbrace>\<lambda>r. Q r\<rbrace>\<rbrakk>
\<Longrightarrow> monad_commute (P and P') f (h>>=g)"
apply (simp (no_asm) add:monad_commute_def)
apply (clarsimp simp:bind_assoc)
apply (subst monad_commute_simple)
apply simp+
apply (rule_tac Q = "(\<lambda>x. Q x)" in monad_eq_split)
apply (subst monad_commute_simple[where a = f])
apply assumption
apply simp+
done
lemma monad_commute_get:
assumes hf: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. P\<rbrace>"
and hg: "\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>r. P\<rbrace>"
and eptyf: "empty_fail f" "empty_fail g"
shows "monad_commute \<top> f g"
proof -
have fsame: "\<And>a b s. (a,b) \<in> fst (f s) \<Longrightarrow> b = s"
by (drule use_valid[OF _ hf],auto)
have gsame: "\<And>a b s. (a,b) \<in> fst (g s) \<Longrightarrow> b = s"
by (drule use_valid[OF _ hg],auto)
note ef = empty_fail_not_snd[OF _ eptyf(1)]
note eg = empty_fail_not_snd[OF _ eptyf(2)]
show ?thesis
apply (simp add:monad_commute_def)
apply (clarsimp simp:bind_def split_def return_def)
apply (intro conjI)
apply (rule set_eqI)
apply (rule iffI)
apply (clarsimp simp:Union_eq dest!: singletonD)
apply (frule fsame)
apply clarsimp
apply (frule gsame)
apply (metis fst_conv snd_conv)
apply (clarsimp simp:Union_eq dest!: singletonD)
apply (frule gsame)
apply clarsimp
apply (frule fsame)
apply clarsimp
apply (metis fst_conv snd_conv)
apply (rule iffI)
apply (erule disjE)
apply (clarsimp simp:image_def)
apply (metis fsame)
apply (clarsimp simp:image_def)
apply (drule eg)
apply clarsimp
apply (rule bexI [rotated], assumption)
apply (frule gsame)
apply clarsimp
apply (erule disjE)
apply (clarsimp simp:image_def dest!:gsame)
apply (clarsimp simp:image_def)
apply (drule ef)
apply clarsimp
apply (frule fsame)
apply (erule bexI[rotated])
apply simp
done
qed
lemma mapM_x_commute:
assumes commute:
"\<And>r. monad_commute (P r) a (b r)"
and single:
"\<And>r x. \<lbrace>P r and K (f r \<noteq> f x) and P x\<rbrace> b x \<lbrace>\<lambda>v. P r \<rbrace>"
shows
"monad_commute (\<lambda>s. (distinct (map f list)) \<and> (\<forall>r\<in> set list. P r s)) a (mapM_x b list)"
apply (induct list)
apply (clarsimp simp:mapM_x_Nil return_def bind_def monad_commute_def)
apply (clarsimp simp:mapM_x_Cons)
apply (rule monad_commute_guard_imp)
apply (rule monad_commute_split)
apply assumption
apply (rule monad_commute_guard_imp[OF commute])
apply assumption
apply (wp hoare_vcg_ball_lift)
apply (rule single)
apply (clarsimp simp: image_def)
apply auto
done
lemma commute_name_pre_state:
assumes "\<And>s. P s \<Longrightarrow> monad_commute (op = s) f g"
shows "monad_commute P f g"
using assms
by (clarsimp simp:monad_commute_def)
lemma commute_rewrite:
assumes rewrite: "\<And>s. Q s \<Longrightarrow> f s = t s"
and hold : "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>x. Q\<rbrace>"
shows "monad_commute R t g \<Longrightarrow> monad_commute (P and Q and R) f g"
apply (clarsimp simp:monad_commute_def bind_def split_def return_def)
apply (drule_tac x = s in spec)
apply (clarsimp simp:rewrite[symmetric])
apply (intro conjI)
apply (rule set_eqI)
apply (rule iffI)
apply clarsimp
apply (rule bexI[rotated],assumption)
apply (subst rewrite)
apply (rule use_valid[OF _ hold])
apply simp+
apply (erule bexI[rotated],simp)
apply clarsimp
apply (rule bexI[rotated],assumption)
apply (subst rewrite[symmetric])
apply (rule use_valid[OF _ hold])
apply simp+
apply (erule bexI[rotated],simp)
apply (intro iffI)
apply clarsimp
apply (rule bexI[rotated],assumption)
apply simp
apply (subst rewrite)
apply (erule(1) use_valid[OF _ hold])
apply simp
apply (clarsimp)
apply (drule bspec,assumption)
apply clarsimp
apply (metis rewrite use_valid[OF _ hold])
done
lemma commute_grab_asm:
"(F \<Longrightarrow> monad_commute P f g) \<Longrightarrow> (monad_commute (P and (K F)) f g)"
by (clarsimp simp: monad_commute_def)
end

18
lib/Word_Lib/Word_Lemmas.thy
View File

@ -5322,6 +5322,8 @@ lemma NOT_mask_shifted_lenword:
apply (simp add: word_size nth_shiftl nth_shiftr)
by auto
(* Comparisons between different word sizes. *)
lemma eq_ucast_ucast_eq:
fixes x :: "'a::len word"
and y :: "'b::len word"
@ -5364,4 +5366,20 @@ lemma ucast_le_ucast:
apply simp
done
(* High bits w.r.t. mask operations. *)
lemma and_neg_mask_eq_iff_not_mask_le:
"w && ~~ mask n = ~~ mask n \<longleftrightarrow> ~~ mask n \<le> w"
by (metis (full_types) dual_order.antisym neg_mask_mono_le word_and_le1 word_and_le2
word_bool_alg.conj_absorb)
lemma le_mask_high_bits:
shows "w \<le> mask n \<longleftrightarrow> (\<forall> i \<in> {n ..< size w}. \<not> w !! i)"
by (auto simp: word_size and_mask_eq_iff_le_mask[symmetric] word_eq_iff)
lemma neg_mask_le_high_bits:
shows "~~ mask n \<le> w \<longleftrightarrow> (\<forall> i \<in> {n ..< size w}. w !! i)"
by (auto simp: word_size and_neg_mask_eq_iff_not_mask_le[symmetric]
word_eq_iff neg_mask_bang)
end

17
lib/Word_Lib/Word_Lemmas_64.thy
View File

@ -84,6 +84,23 @@ lemma unat_less_word_bits:
lemmas unat_mask_word64' = unat_mask[where 'a=64]
lemmas unat_mask_word64 = unat_mask_word64'[folded word_bits_def]
lemma Suc_unat_mask_div:
"Suc (unat (mask sz div word_size::word64)) = 2 ^ (min sz word_bits - 3)"
apply (case_tac "sz < word_bits")
apply (case_tac "3\<le>sz")
apply (clarsimp simp: word_size_def word_bits_def min_def mask_def)
apply (drule (2) Suc_div_unat_helper
[where 'a=64 and sz=sz and us=3, simplified, symmetric])
apply (simp add: not_le word_size_def word_bits_def)
apply (case_tac sz, simp add: unat_word_ariths)
apply (case_tac nat, simp add: unat_word_ariths
unat_mask_word64 min_def word_bits_def)
apply (case_tac nata, simp add: unat_word_ariths unat_mask_word64 word_bits_def)
apply simp
apply (simp add: unat_word_ariths
unat_mask_word64 min_def word_bits_def word_size_def)
done
lemmas word64_minus_one_le' = word_minus_one_le[where 'a=64]
lemmas word64_minus_one_le = word64_minus_one_le'[simplified]

44
lib/X64/WordSetup.thy Normal file
View File

@ -0,0 +1,44 @@
(*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*)
theory WordSetup
imports
"../Distinct_Prop"
"../Word_Lib/Word_Lemmas_64"
begin
(* Distinct_Prop lemmas that need word lemmas: *)
lemma distinct_prop_enum:
"\<lbrakk> \<And>x y. \<lbrakk> x \<le> stop; y \<le> stop; x \<noteq> y \<rbrakk> \<Longrightarrow> P x y \<rbrakk>
\<Longrightarrow> distinct_prop P [0 :: 'a :: len word .e. stop]"
apply (simp add: upto_enum_def distinct_prop_map del: upt.simps)
apply (rule distinct_prop_distinct)
apply simp
apply (simp add: less_Suc_eq_le del: upt.simps)
apply (erule_tac x="of_nat x" in meta_allE)
apply (erule_tac x="of_nat y" in meta_allE)
apply (frule_tac y=x in unat_le)
apply (frule_tac y=y in unat_le)
apply (erule word_unat.Rep_cases)+
apply (simp add: toEnum_of_nat[OF unat_lt2p]
word_le_nat_alt)
done
lemma distinct_prop_enum_step:
"\<lbrakk> \<And>x y. \<lbrakk> x \<le> stop div step; y \<le> stop div step; x \<noteq> y \<rbrakk> \<Longrightarrow> P (x * step) (y * step) \<rbrakk>
\<Longrightarrow> distinct_prop P [0, step .e. stop]"
apply (simp add: upto_enum_step_def distinct_prop_map)
apply (rule distinct_prop_enum)
apply simp
done
end

2
proof/access-control/Retype_AC.thy
View File

@ -1168,7 +1168,7 @@ lemma usable_range_disjoint:
< ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us"
apply (rule minus_one_helper,simp)
apply (rule neq_0_no_wrap)
apply (rule word32_plus_mono_right_split)
apply (rule machine_word_plus_mono_right_split)
apply (simp add:shiftl_t2n range_cover_unat[OF cover] field_simps)
apply (simp add:range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+
done

12
proof/access-control/Syscall_AC.thy
View File

@ -202,18 +202,6 @@ lemma set_thread_state_authorised[wp]:
apply (wp sts_valid_untyped_inv ct_in_state_set
hoare_vcg_ex_lift sts_obj_at_impossible
| simp)+
apply (rename_tac tcb_invocation)
apply (case_tac tcb_invocation, simp_all)
apply (wp hoare_case_option_wp sts_typ_ats set_thread_state_cte_wp_at
hoare_vcg_conj_lift static_imp_wp
| wp_once valid_case_option_post_wp
| simp)+
apply ((clarsimp split: option.splits)+)[3]
apply ((wp
| simp)+)[2]
apply (rename_tac option)
apply (case_tac option, simp_all)[1]
apply (wp set_thread_state_tcb_at sts_obj_at_impossible | simp add: authorised_tcb_inv_def)+
apply (rename_tac cnode_invocation)
apply (case_tac cnode_invocation,
simp_all add: cnode_inv_auth_derivations_def authorised_cnode_inv_def)[1]

2
proof/crefine/Arch_C.thy
View File

@ -3409,7 +3409,7 @@ proof -
show "w \<le> w + (end - start)"
using assms
apply -
apply (rule word32_plus_mono_right_split, rule c)
apply (rule machine_word_plus_mono_right_split, rule c)
apply (simp add:pbfs_less_wb')
done

6
proof/crefine/Detype_C.thy
View File

@ -1640,13 +1640,13 @@ lemma deleteObjects_ccorres':
apply (rule ccorres_assert)
apply (rule ccorres_stateAssert_fwd)
apply (subst bind_assoc[symmetric])
apply (unfold freeMemory_def word_size_def)
apply (unfold freeMemory_def)
apply (subst ksPSpace_update_ext)
apply (subgoal_tac "bits \<le> word_bits")
prefer 2
apply (clarsimp simp:cte_wp_at_ctes_of)
apply (clarsimp simp: mapM_x_storeWord_step intvl_range_conv
intvl_range_conv[where 'a=32, folded word_bits_def]
apply (clarsimp simp: mapM_x_storeWord_step[simplified word_size_bits_def]
intvl_range_conv intvl_range_conv[where 'a=32, folded word_bits_def]
doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm
bind_assoc modify_machinestate_assert_cnodes_swap
modify_modify_bind)

10
proof/drefine/KHeap_DR.thy
View File

@ -3064,11 +3064,11 @@ lemma branch_map_simp1:
apply (rule iffI)
apply (subst(asm) shiftr_bl_of)
apply simp
apply (rule_tac cref1=ref and cref'1="of_bl ref" in iffD1[OF guard_mask_shift])
apply (simp add: word_rep_drop)+
apply (rule_tac cref1=ref and cref'1="of_bl ref::word32" in iffD1[OF guard_mask_shift])
apply (simp add: word_rep_drop)
apply (subst shiftr_bl_of)
apply simp+
apply (drule_tac cref1=ref and cref'1="of_bl ref" in iffD2[OF guard_mask_shift,rotated])
apply (drule_tac cref1=ref and cref'1="of_bl ref::word32" in iffD2[OF guard_mask_shift,rotated])
apply (simp add: word_rep_drop)+
done
@ -3080,7 +3080,7 @@ lemma branch_map_simp2:
" \<lbrakk>length cref \<le> 32; 0 < nata;nata + length list < length cref; list \<le> cref\<rbrakk>
\<Longrightarrow> unat ((((of_bl cref)::word32) >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))"
apply (subgoal_tac "take nata (drop (length list) cref) \<le> drop (length list) cref")
apply (frule_tac iffD2[OF guard_mask_shift,rotated,where cref1="drop (length list) cref" and cref'1="of_bl cref"])
apply (frule_tac iffD2[OF guard_mask_shift,rotated,where cref1="drop (length list) cref" and cref'1="of_bl cref::word32"])
defer
apply clarsimp
apply (subgoal_tac "nata\<le> length cref - length list")
@ -3183,7 +3183,7 @@ lemma resolve_address_bits_terminate_corres:
opt_object_def transform_def
split: nat.splits)+)[3]
apply fastforce
apply (frule_tac cref1=ref and cref'1="of_bl ref" in iffD2[OF guard_mask_shift,rotated])
apply (frule_tac cref1=ref and cref'1="of_bl ref::word32" in iffD2[OF guard_mask_shift,rotated])
apply (simp add: word_rep_drop)+
done

2
proof/drefine/Tcb_DR.thy
View File

@ -1030,7 +1030,7 @@ lemma dcorres_tcb_update_ipc_buffer:
(\<lambda>ptr frame.
doE cap_delete (obj_id', tcb_cnode_index 4);
liftE $ thread_set (tcb_ipc_buffer_update (\<lambda>_. ptr)) obj_id';
liftE $ as_user obj_id' $ set_register TPIDRURW ptr;
liftE $ arch_tcb_set_ipc_buffer obj_id' ptr;
liftE $
case_option (return ())
(case_prod

6
proof/drefine/Untyped_DR.thy
View File

@ -257,8 +257,8 @@ lemma freeMemory_dcorres:
in use_valid)
apply (simp add: do_machine_op_def split_def)
apply wp
apply (clarsimp simp: freeMemory_def word_size_def
mapM_x_storeWord_step intvl_range_conv')
apply (clarsimp simp: freeMemory_def mapM_x_storeWord_step[simplified word_size_bits_def]
intvl_range_conv')
apply (rule conjI, fastforce)
apply clarsimp
apply (erule use_valid[where P=P and Q="%_. P" for P])
@ -947,7 +947,7 @@ lemma retype_transform_ref_subseteq_strong:
apply (simp add:unat_of_nat_m1 less_imp_le)
using cover
apply (simp add:range_cover_def word_bits_def)
apply (rule word32_plus_mono_right_split[where sz = sz])
apply (rule machine_word_plus_mono_right_split[where sz = sz])
using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::word32))"]
apply (clarsimp simp:unat_of_nat_m1)
using cover

14
proof/infoflow/Example_Valid_State.thy
View File

@ -682,7 +682,7 @@ where
lemma irq_node_offs_min:
"init_irq_node_ptr \<le> init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits)"
apply (rule_tac sz=28 in word32_plus_mono_right_split)
apply (rule_tac sz=28 in machine_word_plus_mono_right_split)
apply (simp add: unat_word_ariths mask_def shiftl_t2n s0_ptr_defs cte_level_bits_def)
apply (cut_tac x=irq and 'a=32 in ucast_less)
apply simp
@ -1300,7 +1300,7 @@ lemma pspace_distinct_s0:
apply (simp add: word_less_nat_alt)
apply (simp add: mult.commute)
apply (drule_tac y="0x10" and x="0xE0007FFF" in word_plus_mono_right)
apply (rule_tac sz=28 in word32_plus_mono_right_split)
apply (rule_tac sz=28 in machine_word_plus_mono_right_split)
apply (simp add: unat_word_ariths mask_def)
apply (cut_tac x=irqa and 'a=32 in ucast_less)
apply simp
@ -1314,14 +1314,14 @@ lemma pspace_distinct_s0:
and c="0xE0007FFF + (ucast irqa << 4)" and d="ucast irqa << 4" in word_sub_mono)
apply simp
apply simp
apply (rule_tac sz=28 in word32_plus_mono_right_split)
apply (rule_tac sz=28 in machine_word_plus_mono_right_split)
apply (simp add: unat_word_ariths mask_def shiftl_t2n)
apply (cut_tac x=irqa and 'a=32 in ucast_less)
apply simp
apply (simp add: word_less_nat_alt)
apply (simp add: word_bits_def)
apply simp
apply (rule_tac sz=28 in word32_plus_mono_right_split)
apply (rule_tac sz=28 in machine_word_plus_mono_right_split)
apply (simp add: unat_word_ariths mask_def shiftl_t2n)
apply (cut_tac x=irqa and 'a=32 in ucast_less)
apply simp
@ -1346,7 +1346,7 @@ lemma pspace_distinct_s0:
apply (simp add: word_less_nat_alt)
apply (simp add: mult.commute)
apply (drule_tac y="0x10" and x="0xE0007FFF" in word_plus_mono_right)
apply (rule_tac sz=28 in word32_plus_mono_right_split)
apply (rule_tac sz=28 in machine_word_plus_mono_right_split)
apply (simp add: unat_word_ariths mask_def)
apply (cut_tac x=irq and 'a=32 in ucast_less)
apply simp
@ -1360,14 +1360,14 @@ lemma pspace_distinct_s0:
and c="0xE0007FFF + (ucast irq << 4)" and d="ucast irq << 4" in word_sub_mono)
apply simp
apply simp
apply (rule_tac sz=28 in word32_plus_mono_right_split)
apply (rule_tac sz=28 in machine_word_plus_mono_right_split)
apply (simp add: unat_word_ariths mask_def shiftl_t2n)
apply (cut_tac x=irq and 'a=32 in ucast_less)
apply simp
apply (simp add: word_less_nat_alt)
apply (simp add: word_bits_def)
apply simp
apply (rule_tac sz=28 in word32_plus_mono_right_split)
apply (rule_tac sz=28 in machine_word_plus_mono_right_split)
apply (simp add: unat_word_ariths mask_def shiftl_t2n)
apply (cut_tac x=irq and 'a=32 in ucast_less)
apply simp

95
proof/invariant-abstract/ARM/ArchAcc_AI.thy
View File

@ -18,12 +18,6 @@ imports "../SubMonad_AI"
begin
(*FIXME: Move or remove *)
method spec for x :: "_ :: type" = (erule allE[of _ x])
method bspec for x :: "_ :: type" = (erule ballE[of _ _ x])
method prove for x :: "prop" = (rule revcut_rl[of "PROP x"])
context Arch begin global_naming ARM
@ -221,105 +215,30 @@ lemma set_asid_pool_pred_tcb_at[wp]:
apply (wpsimp wp: get_object_wp simp: pred_tcb_at_def obj_at_def)
done
lemmas word_simps =
word_size word_ops_nth_size nth_ucast nth_shiftr nth_shiftl
pd_bits_def pageBits_def
lemma mask_pd_bits_inner_beauty:
"is_aligned p 2 \<Longrightarrow>
(p && ~~ mask pd_bits) + (ucast ((ucast (p && mask pd_bits >> 2))::12 word) << 2) = (p::word32)"
apply (simp add: is_aligned_nth)
apply (subst word_plus_and_or_coroll; rule word_eqI)
subgoal
by (clarsimp simp: word_simps)
subgoal for n
apply (clarsimp simp: word_simps)
apply (rule iffI, (erule disjE;clarsimp))
subgoal by (clarsimp simp: SucSucMinus)
apply (spec n)
apply (clarsimp simp: SucSucMinus)
by arith
done
by (rule mask_split_aligned; simp add: pd_bits_def pageBits_def)
lemma more_pd_inner_beauty:
fixes x :: "12 word"
fixes p :: word32
assumes x: "x \<noteq> ucast (p && mask pd_bits >> 2)"
shows "(p && ~~ mask pd_bits) + (ucast x << 2) = p \<Longrightarrow> False"
apply (subst (asm) word_plus_and_or_coroll)
apply (clarsimp simp: word_simps bang_eq)
subgoal for n
apply (drule test_bit_size)
apply (clarsimp simp: word_simps)
by arith
apply (insert x)
apply (erule notE)
apply (rule word_eqI)
subgoal for n
apply (clarsimp simp: word_simps bang_eq)
apply (spec "n+2")
by (clarsimp simp: word_ops_nth_size word_size)
done
lemma mask_alignment_ugliness:
"\<lbrakk> x \<noteq> x + z && ~~ mask m;
is_aligned (x + z && ~~ mask m) m;
is_aligned x m;
\<forall>n \<ge> m. \<not>z !! n\<rbrakk>
\<Longrightarrow> False"
apply (erule notE)
apply (rule word_eqI)
apply (clarsimp simp: is_aligned_nth word_ops_nth_size word_size pd_bits_def pageBits_def)
apply (subst word_plus_and_or_coroll)
apply (rule word_eqI)
apply (clarsimp simp: word_size)
subgoal for \<dots> na
apply (spec na)+
by simp
by auto
by (rule mask_split_aligned_neg[OF _ _ x]; simp add: pd_bits_def pageBits_def)
lemma mask_pt_bits_inner_beauty:
"is_aligned p 2 \<Longrightarrow>
(p && ~~ mask pt_bits) + (ucast ((ucast (p && mask pt_bits >> 2))::word8) << 2) = (p::word32)"
apply (simp add: is_aligned_nth)
apply (subst word_plus_and_or_coroll; rule word_eqI)
subgoal by (clarsimp simp: word_simps)
apply (clarsimp simp: word_simps)
subgoal for n
apply (rule iffI)
apply (erule disjE;clarsimp)
subgoal by (prove "Suc (Suc (n - 2)) = n") simp+
apply clarsimp
apply (rule context_conjI)
apply (rule leI)
subgoal by clarsimp
apply (prove "Suc (Suc (n - 2)) = n") subgoal by arith
by (simp add: pt_bits_def pageBits_def)
done
by (rule mask_split_aligned; simp add: pt_bits_def pageBits_def)
lemma more_pt_inner_beauty:
fixes x :: "word8"
fixes p :: word32
assumes x: "x \<noteq> ucast (p && mask pt_bits >> 2)"
shows "(p && ~~ mask pt_bits) + (ucast x << 2) = p \<Longrightarrow> False"
apply (subst (asm) word_plus_and_or_coroll)
apply (clarsimp simp: word_size word_ops_nth_size nth_ucast
nth_shiftl bang_eq)
apply (drule test_bit_size)
apply (clarsimp simp: word_size pt_bits_def pageBits_def)
apply arith
apply (rule x[THEN notE])
apply (rule word_eqI)
subgoal for n
apply (clarsimp simp: bang_eq word_simps)
apply (spec "n+2")
apply (clarsimp simp: word_ops_nth_size word_size)
by (clarsimp simp: pt_bits_def pageBits_def)
done
by (rule mask_split_aligned_neg[OF _ _ x]; simp add: pt_bits_def pageBits_def)
lemma set_pd_aligned [wp]:
@ -511,9 +430,7 @@ lemma pde_shifting:
apply (drule (1) order_le_less_trans)
apply (drule bang_is_le)
apply (drule order_le_less_trans[where z="2 ^ 4"], assumption)
apply (drule word_power_increasing)
apply (fold_subgoals (prefix))[4]
subgoal premises using prems by simp+
apply (drule word_power_increasing; simp)
apply (spec "n' + 20")
apply (frule test_bit_size[where n = "n' + 20"])
by (simp add: word_size)

2
proof/invariant-abstract/ARM/ArchBCorres2_AI.thy
View File

@ -28,7 +28,7 @@ crunch (bcorres)bcorres[wp]: set_extra_badge,derive_cap truncate_state (ignore:
crunch (bcorres)bcorres[wp]: invoke_untyped truncate_state
(ignore: sequence_x)
crunch (bcorres)bcorres[wp]: set_mcpriority truncate_state
crunch (bcorres)bcorres[wp]: set_mcpriority,arch_tcb_set_ipc_buffer truncate_state
lemma invoke_tcb_bcorres[wp]:
fixes a

3
proof/invariant-abstract/ARM/ArchCSpacePre_AI.thy
View File

@ -201,7 +201,8 @@ lemma same_aobject_as_commute:
"same_aobject_as x y \<Longrightarrow> same_aobject_as y x"
by (cases x; cases y; clarsimp)
lemmas wellformed_cap_simps = wellformed_cap_simps[simplified wellformed_acap_def, split_simps arch_cap.split]
lemmas wellformed_cap_simps = wellformed_cap_def
[simplified wellformed_acap_def, split_simps cap.split arch_cap.split]
lemma same_master_cap_same_types:
"cap_master_cap cap = cap_master_cap cap' \<Longrightarrow>

31
proof/invariant-abstract/ARM/ArchCSpace_AI.thy
View File

@ -38,25 +38,24 @@ lemma weak_derived_valid_cap [CSpace_AI_assms]:
apply (clarsimp simp: copy_of_def split: if_split_asm)
apply (auto simp: is_cap_simps same_object_as_def wellformed_cap_simps
valid_cap_def cap_aligned_def bits_of_def
aobj_ref_cases Let_def cap_asid_def
split: cap.splits arch_cap.splits option.splits)
aobj_ref_cases Let_def cap_asid_def
split: cap.splits arch_cap.splits option.splits)
done
lemma weak_derived_tcb_cap_valid [CSpace_AI_assms]:
(* FIXME: unused *)
lemma weak_derived_tcb_cap_valid:
"\<lbrakk> tcb_cap_valid cap p s; weak_derived cap cap' \<rbrakk> \<Longrightarrow> tcb_cap_valid cap' p s"
apply (clarsimp simp add: tcb_cap_valid_def weak_derived_def
obj_at_def is_tcb
split: option.split)
apply (clarsimp simp: st_tcb_def2)
apply (erule disjE, simp_all add: copy_of_def split: if_split_asm)
apply clarsimp
apply (clarsimp simp: tcb_cap_cases_def split: if_split_asm)
apply (auto simp: is_cap_simps same_object_as_def
valid_ipc_buffer_cap_def is_nondevice_page_cap_simps
is_nondevice_page_cap_arch_def
split: cap.split_asm arch_cap.split_asm
Structures_A.thread_state.split_asm)[3]
apply clarsimp
apply (erule disjE; simp add: copy_of_def split: if_split_asm; (solves \<open>clarsimp\<close>)?)
apply (clarsimp simp: tcb_cap_cases_def split: if_split_asm)
apply (auto simp: is_cap_simps same_object_as_def
valid_ipc_buffer_cap_def is_nondevice_page_cap_simps
is_nondevice_page_cap_arch_def
split: cap.split_asm arch_cap.split_asm
thread_state.split_asm)
done
lemma copy_obj_refs [CSpace_AI_assms]:
@ -268,12 +267,12 @@ lemma cap_insert_valid_arch_caps [CSpace_AI_assms]:
prefer 2
apply (erule iffD2[OF caps_of_state_cteD'])
apply (wp set_untyped_cap_as_full_cte_wp_at hoare_vcg_all_lift hoare_vcg_imp_lift
set_untyped_cap_as_full_cte_wp_at_neg hoare_vcg_ex_lift | clarsimp)+
set_untyped_cap_as_full_cte_wp_at_neg hoare_vcg_ex_lift | clarsimp)+
apply (rule hoare_strengthen_post)
prefer 2
apply (erule iffD2[OF caps_of_state_cteD'])
apply (wp set_untyped_cap_as_full_cte_wp_at hoare_vcg_all_lift hoare_vcg_imp_lift
set_untyped_cap_as_full_cte_wp_at_neg hoare_vcg_ex_lift | clarsimp)+
set_untyped_cap_as_full_cte_wp_at_neg hoare_vcg_ex_lift | clarsimp)+
apply (wp get_cap_wp)+
apply (intro conjI allI impI disj_subst)
apply simp
@ -406,7 +405,7 @@ lemma update_cap_data_validI [CSpace_AI_assms]:
apply (simp_all add: is_cap_defs update_cap_data_def Let_def split_def)
apply (simp add: valid_cap_def cap_aligned_def)
apply (simp add: valid_cap_def cap_aligned_def)
apply (simp add: the_cnode_cap_def valid_cap_def cap_aligned_def)
apply (simp add: the_cnode_cap_def valid_cap_def cap_aligned_def word_bits_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (simp_all add: is_cap_defs arch_update_cap_data_def)
@ -523,7 +522,7 @@ lemma cap_insert_simple_arch_caps_no_ap:
end
global_interpretation CSpace_AI?: CSpace_AI_7
global_interpretation CSpace_AI?: CSpace_AI
proof goal_cases
interpret Arch .
case 1 show ?case by (unfold_locales; (fact CSpace_AI_assms)?)

3
proof/invariant-abstract/ARM/ArchDeterministic_AI.thy
View File

@ -16,7 +16,8 @@ context Arch begin global_naming ARM
named_theorems Deterministic_AI_assms
crunch valid_list[wp, Deterministic_AI_assms]: cap_swap_for_delete,set_cap,finalise_cap valid_list
crunch valid_list[wp, Deterministic_AI_assms]:
cap_swap_for_delete,set_cap,finalise_cap,arch_tcb_set_ipc_buffer valid_list
(wp: crunch_wps simp: unless_def crunch_simps)
end

17
proof/invariant-abstract/ARM/ArchDetype_AI.thy
View File

@ -40,10 +40,10 @@ lemma caps_of_state_ko[Detype_AI_asms]:
lemma mapM_x_storeWord[Detype_AI_asms]:
(* FIXME: taken from Retype_C.thy and adapted wrt. the missing intvl syntax. *)
assumes al: "is_aligned ptr 2"
shows "mapM_x (\<lambda>x. storeWord (ptr + of_nat x * 4) 0) [0..<n]
assumes al: "is_aligned ptr word_size_bits"
shows "mapM_x (\<lambda>x. storeWord (ptr + of_nat x * word_size) 0) [0..<n]
= modify (underlying_memory_update
(\<lambda>m x. if \<exists>k. x = ptr + of_nat k \<and> k < n * 4 then 0 else m x))"
(\<lambda>m x. if \<exists>k. x = ptr + of_nat k \<and> k < n * word_size then 0 else m x))"
proof (induct n)
case 0
thus ?case
@ -81,13 +81,13 @@ next
from al have "is_aligned (ptr + of_nat n' * 4) 2"
apply (rule aligned_add_aligned)
apply (rule is_aligned_mult_triv2 [where n = 2, simplified])
apply (simp add: word_bits_conv)+
apply (simp add: word_bits_conv word_size_bits_def)+
done
thus ?case
apply (simp add: mapM_x_append bind_assoc Suc.hyps mapM_x_singleton)
apply (simp add: storeWord_def assert_def is_aligned_mask modify_modify
comp_def)
comp_def word_size_def)
apply (simp only: funs_eq)
done
qed
@ -599,16 +599,17 @@ lemma delete_objects_invs[wp]:
apply (simp add: freeMemory_def word_size_def bind_assoc
empty_fail_mapM_x ef_storeWord)
apply (rule hoare_pre)
apply (rule_tac G="is_aligned ptr bits \<and> 2 \<le> bits \<and> bits \<le> word_bits"
apply (rule_tac G="is_aligned ptr bits \<and> word_size_bits \<le> bits \<and> bits \<le> word_bits"
in hoare_grab_asm)
apply (simp add: mapM_storeWord_clear_um intvl_range_conv[where 'a=32, folded word_bits_def])
apply (simp add: mapM_storeWord_clear_um[unfolded word_size_def]
intvl_range_conv[where 'a=machine_word_len, folded word_bits_def])
apply wp
apply clarsimp
apply (frule invs_untyped_children)
apply (frule detype_invariants, clarsimp+)
apply (drule invs_valid_objs)
apply (drule (1) cte_wp_valid_cap)
apply (simp add: valid_cap_def cap_aligned_def)
apply (simp add: valid_cap_def cap_aligned_def word_size_bits_def)
done
end
end

8
proof/invariant-abstract/ARM/ArchInterrupt_AI.thy
View File

@ -12,7 +12,13 @@ theory ArchInterrupt_AI
imports "../Interrupt_AI"
begin
context Arch begin
context Arch begin global_naming ARM
defs arch_irq_control_inv_valid_def:
"arch_irq_control_inv_valid irq_inv \<equiv> \<bottom>"
declare arch_irq_control_inv_valid_def [simp]
named_theorems Interrupt_AI_asms

2
proof/invariant-abstract/ARM/ArchInvariants_AI.thy
View File

@ -373,6 +373,8 @@ definition
where
"vs_lookup \<equiv> \<lambda>s. vs_lookup_trans s `` vs_asid_refs (arm_asid_table (arch_state s))"
definition "second_level_tables \<equiv> arch_state.arm_global_pts"
end
context begin interpretation Arch .

2
proof/invariant-abstract/ARM/ArchIpc_AI.thy
View File

@ -50,7 +50,7 @@ lemma update_cap_data_closedform:
the_cnode_cap_def fst_conv snd_conv fun_app_def the_arch_cap_def
arch_update_cap_data_def
cong: if_cong)
apply auto
apply (auto simp: word_bits_def)
done
lemma cap_asid_PageCap_None [simp]:

6
proof/invariant-abstract/ARM/ArchKHeap_AI.thy
View File

@ -261,13 +261,11 @@ lemma set_object_valid_kernel_mappings:
lemma valid_vs_lookup_lift:
assumes lookup: "\<And>P. \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>"
assumes cap: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>"
assumes pts: "\<And>P. \<lbrace>\<lambda>s. P (arm_global_pts (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (arm_global_pts (arch_state s))\<rbrace>"
shows "\<lbrace>valid_vs_lookup\<rbrace> f \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>"
unfolding valid_vs_lookup_def
apply (rule hoare_lift_Pf [where f=vs_lookup_pages])
apply (rule hoare_lift_Pf [where f="\<lambda>s. (caps_of_state s)"])
apply (rule hoare_lift_Pf [where f="\<lambda>s. arm_global_pts (arch_state s)"])
apply (wp lookup cap pts)+
apply (wp lookup cap)+
done
@ -402,7 +400,7 @@ lemma arch_lifts:
apply (rule aobj_at)
apply clarsimp
done
subgoal
apply (simp add: valid_arch_state_def valid_asid_table_def)
apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch])

103
proof/invariant-abstract/ARM/ArchRetype_AI.thy
View File

@ -58,14 +58,6 @@ lemma retype_region_ret_folded [Retype_AI_assms]:
declare store_pde_state_refs_of [wp]
(* FIXME: move to Machine_R.thy *)
lemma clearMemory_corres:
"corres_underlying Id False True dc \<top> (\<lambda>_. is_aligned y 2)
(clearMemory y a) (clearMemory y a)"
apply (rule corres_Id)
apply simp+
done
(* These also prove facts about copy_global_mappings *)
crunch pspace_aligned[wp]: init_arch_objects "pspace_aligned"
(ignore: clearMemory wp: crunch_wps hoare_unless_wp)
@ -150,22 +142,6 @@ lemmas init_arch_objects_valid_cap[wp] = valid_cap_typ [OF init_arch_objects_typ
lemmas init_arch_objects_cap_table[wp] = cap_table_at_lift_valid [OF init_arch_objects_typ_at]
lemma clearMemory_vms:
"valid_machine_state s \<Longrightarrow>
\<forall>x\<in>fst (clearMemory ptr bits (machine_state s)).
valid_machine_state (s\<lparr>machine_state := snd x\<rparr>)"
apply (clarsimp simp: valid_machine_state_def
disj_commute[of "in_user_frame p s" for p s])
apply (drule_tac x=p in spec, simp)
apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = 0"
in use_valid[where P=P and Q="\<lambda>_. P" for P], simp_all)
apply (simp add: clearMemory_def cleanCacheRange_PoU_def machine_op_lift_def
machine_rest_lift_def split_def)
apply (wp hoare_drop_imps | simp | wp mapM_x_wp_inv)+
apply (simp add: storeWord_def | wp)+
apply (simp add: word_rsplit_0)+
done
crunch device_state_inv[wp]: clearMemory "\<lambda>ms. P (device_state ms)"
(wp: mapM_x_wp)
@ -174,8 +150,6 @@ crunch cap_refs_respects_device_region[wp]: reserve_region cap_refs_respects_dev
crunch invs [wp]: reserve_region "invs"
crunch invs [wp]: reserve_region "invs"
crunch iflive[wp]: copy_global_mappings "if_live_then_nonz_cap"
(wp: crunch_wps)
@ -312,12 +286,8 @@ lemma store_pde_map_global_valid_arch_caps:
lemma store_pde_map_global_valid_arch_objs:
"\<lbrace>valid_arch_objs and valid_arch_state and valid_global_objs
and K (valid_pde_mappings pde)
and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)
\<in> kernel_vsrefs)
and (\<lambda>s. \<forall>p. pde_ref pde = Some p
\<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))\<rbrace>
store_pde p pde
and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs)\<rbrace>
store_pde p pde
\<lbrace>\<lambda>rv. valid_arch_objs\<rbrace>"
apply (simp add: store_pde_def)
apply (wp set_pd_arch_objs_map[where T="{}" and S="{}"])
@ -431,8 +401,6 @@ lemma copy_global_equal_kernel_mappings_restricted:
apply (drule mp)
apply (simp add: kernel_base_def pd_bits_def pageBits_def)
apply (clarsimp simp: obj_at_def)
apply (case_tac "global_pd = pd")
apply simp
apply (subst equal_kernel_mappings_specific_def)
apply (fastforce simp add: obj_at_def restrict_map_def)
apply (subst(asm) equal_kernel_mappings_specific_def)
@ -576,7 +544,7 @@ requalify_consts post_retype_invs_check
end
definition
post_retype_invs :: "apiobject_type \<Rightarrow> word32 list \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
post_retype_invs :: "apiobject_type \<Rightarrow> machine_word list \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"post_retype_invs tp refs \<equiv>
if post_retype_invs_check tp
@ -672,7 +640,7 @@ context Arch begin global_naming ARM
lemma valid_untyped_helper [Retype_AI_assms]:
assumes valid_c : "s \<turnstile> c"
and cte_at : "cte_wp_at (op = c) q s"
and tyunt: "ty \<noteq> Structures_A.apiobject_type.Untyped"
and tyunt: "ty \<noteq> Untyped"
and cover : "range_cover ptr sz (obj_bits_api ty us) n"
and range : "is_untyped_cap c \<Longrightarrow> usable_untyped_range c \<inter> {ptr..ptr + of_nat (n * 2 ^ (obj_bits_api ty us)) - 1} = {}"
and pn : "pspace_no_overlap_range_cover ptr sz s"
@ -847,18 +815,10 @@ end
context retype_region_proofs_arch begin
lemma obj_at_valid_pte:
"\<lbrakk>valid_pte pte s; \<And>P p. obj_at P p s \<Longrightarrow> obj_at P p s'\<rbrakk>
\<Longrightarrow> valid_pte pte s'"
apply (cases pte,simp_all add: valid_pte_def data_at_def)
apply (clarsimp | elim disjE)+
done
lemma obj_at_valid_pde:
"\<lbrakk>valid_pde pde s; \<And>P p. obj_at P p s \<Longrightarrow> obj_at P p s'\<rbrakk>
\<Longrightarrow> valid_pde pde s'"
apply (cases pde, simp_all add: valid_pte_def data_at_def)
apply (clarsimp | elim disjE)+
lemma valid_arch_obj_pres:
"valid_arch_obj ao s \<Longrightarrow> valid_arch_obj ao s'"
apply (cases ao; simp add: obj_at_pres)
apply (erule allEI ballEI; rename_tac t i; case_tac "t i"; fastforce simp: data_at_def obj_at_pres)+
done
end
@ -887,12 +847,7 @@ proof
have "valid_arch_obj ao s"
by (auto simp: vs_lookup' elim: valid_arch_objsD)
hence "valid_arch_obj ao s'"
apply (cases ao, simp_all add: obj_at_pres)
apply (erule allEI)
apply (erule (1) obj_at_valid_pte[OF _ obj_at_pres])
apply (erule ballEI)
apply (erule (1) obj_at_valid_pde[OF _ obj_at_pres])
done
by (rule valid_arch_obj_pres)
}
ultimately
show "valid_arch_obj ao s'" by blast
@ -908,18 +863,16 @@ end
context Arch begin global_naming ARM (*FIXME: arch_split*)
definition
valid_vs_lookup2 :: "(vs_ref list \<times> word32) set \<Rightarrow> word32 set \<Rightarrow> (cslot_ptr \<rightharpoonup> cap) \<Rightarrow> bool"
valid_vs_lookup2 :: "(vs_ref list \<times> word32) set \<Rightarrow> (cslot_ptr \<rightharpoonup> cap) \<Rightarrow> bool"
where
"valid_vs_lookup2 lookup S caps \<equiv>
"valid_vs_lookup2 lookup caps \<equiv>
\<forall>p ref. (ref, p) \<in> lookup \<longrightarrow>
ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and>
(\<exists>p' cap. caps p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)"
lemma valid_vs_lookup_def2:
"valid_vs_lookup s = valid_vs_lookup2
(vs_lookup_pages s) (set (arm_global_pts (arch_state s)))
(null_filter (caps_of_state s))"
"valid_vs_lookup s = valid_vs_lookup2 (vs_lookup_pages s) (null_filter (caps_of_state s))"
apply (simp add: valid_vs_lookup_def valid_vs_lookup2_def)
apply (intro iff_allI imp_cong[OF refl] disj_cong[OF refl]
iff_exI conj_cong[OF refl])
@ -947,12 +900,6 @@ lemma unique_table_refs_null:
done
definition
region_in_kernel_window :: "word32 set \<Rightarrow> 'z state \<Rightarrow> bool"
where
"region_in_kernel_window S \<equiv>
\<lambda>s. \<forall>x \<in> S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow"
lemma pspace_respects_device_regionI:
assumes uat: "\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage False sz))
\<Longrightarrow> obj_range ptr (ArchObj $ DataPage False sz) \<subseteq> - device_region s"
@ -1020,8 +967,18 @@ lemma default_obj_dev:
by (clarsimp simp: default_object_def default_arch_object_def
split: apiobject_type.split_asm aobject_type.split_asm)
definition
region_in_kernel_window :: "word32 set \<Rightarrow> 'z state \<Rightarrow> bool"
where
"region_in_kernel_window S \<equiv>
\<lambda>s. \<forall>x \<in> S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow"
end
context begin interpretation Arch .
requalify_consts region_in_kernel_window
end
lemma cap_range_respects_device_region_cong[cong]:
@ -1030,11 +987,6 @@ lemma cap_range_respects_device_region_cong[cong]:
by (clarsimp simp: cap_range_respects_device_region_def)
context begin interpretation Arch .
requalify_consts region_in_kernel_window
end
context retype_region_proofs_arch begin
lemmas unique_table_caps_eq
@ -1064,16 +1016,6 @@ lemma valid_arch_caps:
unique_table_refs_eq
valid_table_caps)
lemma valid_arch_obj_pres:
"valid_arch_obj ao s \<Longrightarrow> valid_arch_obj ao s'"
apply (cases ao, simp_all)
apply (simp add: obj_at_pres)
apply (erule allEI)
apply (erule (1) obj_at_valid_pte[OF _ obj_at_pres])
apply (erule ballEI)
apply (erule (1) obj_at_valid_pde[OF _ obj_at_pres])
done
lemma valid_global_objs:
"valid_global_objs s \<Longrightarrow> valid_global_objs s'"
apply (simp add: valid_global_objs_def valid_ao_at_def)
@ -1314,7 +1256,6 @@ lemma storeWord_um_eq_0:
\<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>"
by (simp add: storeWord_def word_rsplit_0 | wp)+
lemma clearMemory_um_eq_0:
"\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace>
clearMemory ptr bits

7
proof/invariant-abstract/ARM/ArchTcb_AI.thy
View File

@ -360,7 +360,7 @@ lemma update_cap_valid[Tcb_AI_asms]:
split del: if_split)
apply (simp add: badge_update_def cap_rights_update_def)
apply (simp add: badge_update_def)
apply simp
apply (simp add: word_bits_def)
apply (rename_tac arch_cap)
using valid_validate_vm_rights[simplified valid_vm_rights_def]
apply (case_tac arch_cap, simp_all add: acap_rights_update_def
@ -371,11 +371,16 @@ lemma update_cap_valid[Tcb_AI_asms]:
crunch pred_tcb_at: switch_to_thread "pred_tcb_at proj P t"
(wp: crunch_wps simp: crunch_simps)
crunch typ_at[wp]: invoke_tcb "\<lambda>s. P (typ_at T p s)"
(ignore: check_cap_at setNextPC zipWithM
wp: hoare_drop_imps mapM_x_wp' check_cap_inv
simp: crunch_simps)
end
context begin interpretation Arch .
requalify_consts is_cnode_or_valid_arch
requalify_facts invoke_tcb_typ_at
end
global_interpretation Tcb_AI?: Tcb_AI

14
proof/invariant-abstract/ARM/ArchUntyped_AI.thy
View File

@ -313,7 +313,7 @@ lemma delete_objects_rewrite[Untyped_AI_assms]:
od"
apply (clarsimp simp:delete_objects_def freeMemory_def word_size_def)
apply (subgoal_tac "is_aligned (ptr &&~~ mask sz) sz")
apply (subst mapM_storeWord_clear_um)
apply (subst mapM_storeWord_clear_um[simplified word_size_def word_size_bits_def])
apply (simp)
apply simp
apply (simp add:range_cover_def)
@ -326,7 +326,7 @@ declare store_pde_pred_tcb_at [wp]
(* nonempty_table *)
definition
nonempty_table :: "word32 set \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
nonempty_table :: "machine_word set \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
where
"nonempty_table S ko \<equiv>
(a_type ko = AArch APageTable \<or> a_type ko = AArch APageDirectory)
@ -342,7 +342,7 @@ lemma create_cap_valid_arch_caps[wp, Untyped_AI_assms]:
and valid_cap (default_cap tp oref sz dev)
and (\<lambda>(s::'state_ext::state_ext state). \<forall>r\<in>obj_refs (default_cap tp oref sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
and cte_wp_at (op = cap.NullCap) cref
and K (tp \<noteq> ArchObject ASIDPoolObj)\<rbrace>
create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>"
@ -361,7 +361,7 @@ lemma create_cap_valid_arch_caps[wp, Untyped_AI_assms]:
apply (case_tac cref, fastforce)
apply (simp add: obj_ref_none_no_asid)
apply (rule conjI)
apply (auto simp: is_cap_simps valid_cap_def
apply (auto simp: is_cap_simps valid_cap_def second_level_tables_def
obj_at_def nonempty_table_def a_type_simps)[1]
apply (clarsimp simp del: imp_disjL)
apply (case_tac "\<exists>x. x \<in> obj_refs cap")
@ -549,15 +549,15 @@ lemma mapM_copy_global_mappings_nonempty_table[wp]:
done
lemma init_arch_objects_nonempty_table[Untyped_AI_assms, wp]:
"\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s)
"\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
\<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and
K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us))\<rbrace>
init_arch_objects tp ptr bits us refs
\<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s)\<rbrace>"
\<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: init_arch_objects_def split del: if_split)
apply (rule hoare_pre)
apply (wp hoare_unless_wp | wpc | simp add: reserve_region_def)+
apply (wp hoare_unless_wp | wpc | simp add: reserve_region_def second_level_tables_def)+
apply (clarsimp simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def)
done

24
proof/invariant-abstract/ARM/ArchVSpace_AI.thy
View File

@ -116,20 +116,14 @@ lemma pd_at_asid_unique:
valid_arch_state s; asid < 2 ^ asid_bits; asid' < 2 ^ asid_bits \<rbrakk>
\<Longrightarrow> asid = asid'"
apply (clarsimp simp: vspace_at_asid_def)
apply (subgoal_tac "pd \<notin> set (arm_global_pts (arch_state s))")
apply (drule(1) valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI])+
apply (clarsimp simp: table_cap_ref_ap_eq[symmetric])
apply (clarsimp simp: table_cap_ref_def
split: cap.split_asm arch_cap.split_asm option.split_asm)
apply (drule(2) unique_table_refsD,
simp+, clarsimp simp: table_cap_ref_def,
erule(1) asid_low_high_bits)
apply simp+
apply clarsimp
apply (drule(2) vs_ref_order)
apply clarsimp
apply (drule(1) valid_global_ptsD)
apply (clarsimp simp: obj_at_def a_type_def)
apply (drule(1) valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI])+
apply (clarsimp simp: table_cap_ref_ap_eq[symmetric])
apply (clarsimp simp: table_cap_ref_def
split: cap.split_asm arch_cap.split_asm option.split_asm)
apply (drule(2) unique_table_refsD,
simp+, clarsimp simp: table_cap_ref_def,
erule(1) asid_low_high_bits)
apply simp+
done
lemma pd_at_asid_unique2:
@ -4994,7 +4988,7 @@ lemma set_asid_pool_valid_arch_caps_map:
apply (wp get_object_wp)
apply clarsimp
apply (frule obj_at_not_pt_not_in_global_pts[where p=pd], clarsimp+)
apply (simp add: a_type_def)
apply (simp add: a_type_def)
apply (frule obj_at_not_pt_not_in_global_pts[where p=ap], clarsimp+)
apply (clarsimp simp: obj_at_def valid_arch_caps_def
caps_of_state_after_update)

2
proof/invariant-abstract/BCorres_AI.thy
View File

@ -202,7 +202,7 @@ lemma throw_on_false_bcorres[wp]: "bcorres f f' \<Longrightarrow> bcorres (thro
done
context Arch begin
crunch (bcorres)bcorres[wp]: arch_finalise_cap truncate_state (simp: swp_def)
crunch (bcorres)bcorres[wp]: arch_finalise_cap truncate_state (simp: swp_def ignore: forM_x)
end
requalify_facts Arch.arch_finalise_cap_bcorres

118
proof/invariant-abstract/CSpace_AI.thy
View File

@ -39,9 +39,13 @@ requalify_facts
loadWord_inv
valid_global_refsD2
arch_derived_is_device
valid_ao_at_lift
update_cnode_cap_data_def
end
(* Proofs don't want to see these details. *)
declare update_cnode_cap_data_def [simp]
definition
capBadge_ordering :: "bool \<Rightarrow> (badge option \<times> badge option) set"
@ -106,7 +110,7 @@ lemma gets_machine_state_modify:
by (simp add: bind_def split_def simpler_gets_def simpler_modify_def)
locale CSpace_AI =
locale CSpace_AI_getActiveIRQ_wp =
fixes state_ext_t :: "'state_ext::state_ext itself"
assumes getActiveIRQ_wp[wp]:
"\<And>P :: 'state_ext state \<Rightarrow> bool.
@ -120,7 +124,7 @@ lemma OR_choiceE_weak_wp:
split: option.splits if_split_asm)
done
context CSpace_AI begin
context CSpace_AI_getActiveIRQ_wp begin
lemma preemption_point_inv:
fixes P :: "'state_ext state \<Rightarrow> bool"
@ -338,58 +342,59 @@ lemmas is_cap_defs = is_arch_cap_def is_zombie_def
lemma guard_mask_shift:
fixes cref' :: word32
fixes cref' :: "'a::len word"
assumes postfix: "to_bl cref' = xs @ cref"
shows
"(length guard \<le> length cref \<and>
(cref' >> length cref - length guard) && mask (length guard) = of_bl guard)
=
(guard \<le> cref)" (is "(_ \<and> ?l = ?r) = _ " is "(?len \<and> ?shift) = ?prefix")
(cref' >> (length cref - length guard)) && mask (length guard) = of_bl guard)
= (guard \<le> cref)" (is "(_ \<and> ?l = ?r) = _ " is "(?len \<and> ?shift) = ?prefix")
proof
let ?w_len = "len_of TYPE('a)"
from postfix
have "length (to_bl cref') = length xs + length cref" by simp
hence 32: "32 = \<dots>" by simp
hence w_len: "?w_len = \<dots>" by simp
assume "?len \<and> ?shift"
hence shift: ?shift and c_len: ?len by auto
from 32 c_len have "length guard \<le> 32" by simp
from w_len c_len have "length guard \<le> ?w_len" by simp
with shift
have "(replicate (32 - length guard) False) @ guard = to_bl ?l"
have "(replicate (?w_len - length guard) False) @ guard = to_bl ?l"
by (simp add: word_rep_drop)
also
have "\<dots> = replicate (32 - length guard) False @
drop (32 - length guard) (to_bl (cref' >> length cref - length guard))"
have "\<dots> = replicate (?w_len - length guard) False @
drop (?w_len - length guard) (to_bl (cref' >> (length cref - length guard)))"
by (simp add: bl_and_mask)
also
from c_len
have "\<dots> = replicate (32 - length guard) False @ take (length guard) cref"
by (simp add: bl_shiftr 32 word_size postfix)
have "\<dots> = replicate (?w_len - length guard) False @ take (length guard) cref"
by (simp add: bl_shiftr w_len word_size postfix)
finally
have "take (length guard) cref = guard" by simp
thus ?prefix by (simp add: take_prefix)
next
let ?w_len = "len_of TYPE('a)"
assume ?prefix
then obtain zs where cref: "cref = guard @ zs"
by (auto simp: prefix_def less_eq_list_def)
with postfix
have to_bl_c: "to_bl cref' = xs @ guard @ zs" by simp
hence "length (to_bl cref') = length \<dots>" by simp
hence 32: "32 = \<dots>" by simp
hence w_len: "?w_len = \<dots>" by simp
from cref have c_len: "length guard \<le> length cref" by simp
from cref
have "length cref - length guard = length zs" by simp
hence "to_bl ?l = replicate (32-length guard) False @
drop (32-length guard) (to_bl (cref' >> length zs))"
hence "to_bl ?l = replicate (?w_len - length guard) False @
drop (?w_len - length guard) (to_bl (cref' >> (length zs)))"
by (simp add: bl_and_mask)
also
have "drop (32-length guard) (to_bl (cref' >> length zs)) = guard"
by (simp add: bl_shiftr word_size 32 to_bl_c)
also
have "drop (?w_len - length guard) (to_bl (cref' >> (length zs))) = guard"
by (simp add: bl_shiftr word_size w_len to_bl_c)
finally
have "to_bl ?l = to_bl ?r"
by (simp add: word_rep_drop 32)
by (simp add: word_rep_drop w_len)
with c_len
show "?len \<and> ?shift" by simp
qed
@ -914,7 +919,7 @@ lemma null_no_mdb:
end
(* True if cap' is derived from cap. *)
definition
is_derived :: "cdt \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
where
@ -2722,16 +2727,6 @@ lemma weak_derived_Null:
done
locale CSpace_AI_2 = CSpace_AI state_ext_t
for state_ext_t :: "'state_ext::state_ext itself" +
assumes weak_derived_valid_cap:
"\<And>(s::'state_ext state) c c'.
\<lbrakk> s \<turnstile> c; wellformed_cap c'; weak_derived c' c\<rbrakk> \<Longrightarrow> s \<turnstile> c'"
assumes weak_derived_tcb_cap_valid:
"\<And>(s::'state_ext state) cap p cap'.
\<lbrakk> tcb_cap_valid cap p s; weak_derived cap cap' \<rbrakk> \<Longrightarrow> tcb_cap_valid cap' p s"
lemma weak_derived_refl [intro!, simp]:
"weak_derived c c"
by (simp add: weak_derived_def)
@ -3080,8 +3075,10 @@ lemma copy_of_Null2 [simp]:
by (auto simp add: copy_of_def same_object_as_def is_cap_simps)
locale CSpace_AI_3 = CSpace_AI_2 state_ext_t
for state_ext_t :: "'state_ext::state_ext itself" +
locale CSpace_AI_weak_derived =
fixes state_ext_t :: "'state_ext::state_ext itself"
assumes weak_derived_valid_cap:
"\<And>(s:: 'state_ext state) c c'. \<lbrakk> s \<turnstile> c; wellformed_cap c'; weak_derived c' c\<rbrakk> \<Longrightarrow> s \<turnstile> c'"
assumes copy_obj_refs:
"\<And>cap cap'. copy_of cap cap' \<Longrightarrow> obj_refs cap' = obj_refs cap"
assumes weak_derived_cap_class[simp]:
@ -3099,7 +3096,7 @@ lemma weak_derived_untyped_range:
split: if_split_asm cap.splits)
context CSpace_AI_3 begin
context CSpace_AI_weak_derived begin
lemma weak_derived_cap_range:
"\<And>dcap cap. weak_derived dcap cap \<Longrightarrow> cap_range dcap = cap_range cap"
@ -3110,7 +3107,7 @@ end
locale mdb_move_abs_gen
= mdb_move_abs src dest m s' s m'' m'
+ CSpace_AI_3 state_ext_t
+ CSpace_AI_weak_derived state_ext_t
for state_ext_t :: "'state_ext::state_ext itself"
and src dest m
and s' :: "'state_ext state"
@ -3199,12 +3196,12 @@ lemma weak_derived_untyped2:
lemma weak_derived_Null_eq [simp]:
"(weak_derived cap.NullCap cap) = (cap = cap.NullCap)"
"(weak_derived NullCap cap) = (cap = NullCap)"
by (auto simp: weak_derived_def)
lemma weak_derived_eq_Null [simp]:
"(weak_derived cap cap.NullCap) = (cap = cap.NullCap)"
"(weak_derived cap NullCap) = (cap = NullCap)"
by (auto simp: weak_derived_def)
@ -3216,12 +3213,12 @@ lemma weak_derived_is_untyped:
lemma weak_derived_irq [simp]:
"weak_derived cap.IRQControlCap cap = (cap = cap.IRQControlCap)"
"weak_derived IRQControlCap cap = (cap = IRQControlCap)"
by (auto simp add: weak_derived_def copy_of_def same_object_as_def
split: cap.splits)
lemmas (in CSpace_AI_3) weak_derived_ranges =
lemmas (in CSpace_AI_weak_derived) weak_derived_ranges =
weak_derived_is_untyped
weak_derived_untyped_range
weak_derived_obj_refs
@ -3249,7 +3246,7 @@ lemma weak_derived_Reply:
split: if_split_asm cap.split_asm)
lemmas (in CSpace_AI_3) weak_derived_replies =
lemmas (in CSpace_AI_weak_derived) weak_derived_replies =
weak_derived_is_reply
weak_derived_is_reply_master
weak_derived_obj_ref_of
@ -3355,7 +3352,7 @@ end
declare is_master_reply_cap_NullCap [simp]
context CSpace_AI_3 begin
context CSpace_AI_weak_derived begin
lemma mdb_move_abs_gen:
"\<And>src dest m (s::'state_ext state).
@ -3556,8 +3553,8 @@ lemma set_free_index_valid_pspace:
apply (clarsimp simp: is_nondevice_page_cap_simps)
done
locale CSpace_AI_4 = CSpace_AI_3 state_ext_t
for state_ext_t :: "'state_ext::state_ext itself" +
locale CSpace_AI_set_free_index_invs =
fixes state_ext_t :: "'state_ext::state_ext itself"
assumes set_free_index_invs_known_cap:
"\<And>cap idx.
\<lbrace>\<lambda>s::'state_ext state. (free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2^cap_bits cap)
@ -3565,7 +3562,7 @@ locale CSpace_AI_4 = CSpace_AI_3 state_ext_t
set_cap (free_index_update (\<lambda>_. idx) cap) cref
\<lbrace>\<lambda>rv s'. invs s'\<rbrace>"
lemma (in CSpace_AI_4) set_free_index_invs:
lemma (in CSpace_AI_set_free_index_invs) set_free_index_invs:
"\<lbrace>\<lambda>s::'state_ext state. (free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2^cap_bits cap) \<and>
invs s \<and> cte_wp_at (\<lambda>cp. \<exists>ptr sz dev idx' idx''. idx' \<le> idx
\<and> cp = UntypedCap dev ptr sz idx' \<and> cap = UntypedCap dev ptr sz idx'') cref s\<rbrace>
@ -3875,8 +3872,8 @@ lemma unique_table_refs_upd_eqD:
done
locale CSpace_AI_5 = CSpace_AI_4 state_ext_t
for state_ext_t :: "'state_ext::state_ext itself" +
locale CSpace_AI_set_untyped_cap_as_full =
fixes state_ext_t :: "'state_ext::state_ext itself"
assumes set_untyped_cap_as_full_valid_arch_caps:
"\<And>src_cap src cap.
\<lbrace>valid_arch_caps and cte_wp_at (op = src_cap) src\<rbrace>
@ -3943,8 +3940,8 @@ lemma derived_cap_master_cap_eq: "is_derived m n b c \<Longrightarrow> cap_maste
by (clarsimp simp:is_derived_def split:if_splits)
locale CSpace_AI_6 = CSpace_AI_5 state_ext_t
for state_ext_t :: "'state_ext::state_ext itself" +
locale CSpace_AI_cap_insert =
fixes state_ext_t :: "'state_ext::state_ext itself"
assumes cap_insert_valid_arch_caps:
"\<And>src cap dest.
\<lbrace>valid_arch_caps and (\<lambda>s::'state_ext state. cte_wp_at (is_derived (cdt s) src cap) src s)\<rbrace>
@ -4100,7 +4097,7 @@ lemma valid_irq_states_exst_update[simp]:
by(auto simp: valid_irq_states_def)
context CSpace_AI_6 begin
context CSpace_AI_cap_insert begin
interpretation cap_insert_crunches .
@ -4231,7 +4228,12 @@ lemma cap_swap_valid_objs:
done
locale CSpace_AI_7 = CSpace_AI_6 state_ext_t
locale CSpace_AI
= CSpace_AI_getActiveIRQ_wp state_ext_t
+ CSpace_AI_weak_derived state_ext_t
+ CSpace_AI_set_free_index_invs state_ext_t
+ CSpace_AI_set_untyped_cap_as_full state_ext_t
+ CSpace_AI_cap_insert state_ext_t
for state_ext_t :: "'state_ext::state_ext itself" +
assumes mask_cap_valid[simp]:
"\<And>(s::'state_ext state) c R. s \<turnstile> c \<Longrightarrow> s \<turnstile> mask_cap R c"
@ -4582,7 +4584,7 @@ lemma appropriate_cte_cap_def2:
\<or> (\<forall> irq. cte_cap \<noteq> IRQHandlerCap irq))"
by (clarsimp simp: appropriate_cte_cap_def cap_irqs_def cap_irq_opt_def split: cap.split)
context CSpace_AI_7 begin
context CSpace_AI begin
lemma setup_reply_master_ifunsafe[wp]:
"\<And>t.
@ -4654,10 +4656,8 @@ crunch empty_table_at[wp]: setup_reply_master "obj_at (empty_table S) p"
(ignore: set_cap wp: set_cap_obj_at_impossible crunch_wps
simp: if_apply_def2 empty_table_caps_of)
lemmas setup_reply_master_valid_ao_at[wp]
= ARM.valid_ao_at_lift [OF setup_reply_master_typ_at setup_reply_master_arch_ko_at]
= valid_ao_at_lift [OF setup_reply_master_typ_at setup_reply_master_arch_ko_at]
crunch v_ker_map[wp]: setup_reply_master "valid_kernel_mappings"
@ -4686,7 +4686,7 @@ lemma setup_reply_master_cap_refs_respects_device_region[wp]:
apply (auto simp: cte_wp_at_caps_of_state)
done
context CSpace_AI_7 begin
context CSpace_AI begin
crunch cap_refs_in_kernel_window[wp]: setup_reply_master "cap_refs_in_kernel_window"
end
@ -4718,7 +4718,7 @@ lemma setup_reply_master_vms[wp]:
crunch valid_irq_states[wp]: setup_reply_master "valid_irq_states"
context CSpace_AI_7 begin
context CSpace_AI begin
lemma setup_reply_master_invs[wp]:
"\<And>t.
@ -4750,7 +4750,7 @@ definition
is_untyped_cap parent \<and> descendants_of p m = {})"
context CSpace_AI_7 begin
context CSpace_AI begin
lemma safe_parent_cap_range:
"\<And> m p cap pcap. safe_parent_for m p cap pcap \<Longrightarrow> cap_range cap \<subseteq> cap_range pcap"
@ -4784,7 +4784,7 @@ lemma safe_parent_is_parent:
done
context CSpace_AI_7 begin
context CSpace_AI begin
lemma safe_parent_ut_descendants:
"\<And>m p cap pcap.
@ -4922,7 +4922,7 @@ lemma (in mdb_insert_abs) reply_mdb_simple:
by (simp add: reply_caps_mdb_simple reply_masters_mdb_simple)
context CSpace_AI_7 begin
context CSpace_AI begin
lemma cap_insert_simple_mdb:
fixes dest src cap

4
proof/invariant-abstract/DetSchedSchedule_AI.thy
View File

@ -1665,6 +1665,9 @@ lemma set_mcpriority_valid_sched[wp]:
crunch simple_sched_action[wp]: set_priority,set_mcpriority simple_sched_action
context begin interpretation Arch . (*FIXME: arch_split*)
crunch valid_sched[wp]: arch_tcb_set_ipc_buffer valid_sched
lemma tc_valid_sched[wp]:
"\<lbrace>valid_sched and simple_sched_action\<rbrace>
invoke_tcb (ThreadControl a sl b mcp pr e f g)
@ -1675,6 +1678,7 @@ lemma tc_valid_sched[wp]:
apply (wp check_cap_inv thread_set_not_state_valid_sched hoare_vcg_all_lift gts_wp static_imp_wp
| wpc | simp add: option_update_thread_def)+
done
end
lemma set_scheduler_action_swt_weak_valid_sched:

2
proof/invariant-abstract/Deterministic_AI.thy
View File

@ -3895,6 +3895,8 @@ locale Deterministic_AI_1 =
"\<And>param_a param_b. \<lbrace>valid_list\<rbrace> finalise_cap param_a param_b \<lbrace>\<lambda>_. valid_list\<rbrace>"
assumes get_cap_valid_list[wp]:
"\<And>param_a. \<lbrace>valid_list\<rbrace> get_cap param_a \<lbrace>\<lambda>_. valid_list\<rbrace>"
assumes arch_tcb_set_ipc_buffer_valid_list[wp]:
"\<And>t ptr. \<lbrace>valid_list\<rbrace> arch_tcb_set_ipc_buffer t ptr \<lbrace>\<lambda>_. valid_list\<rbrace>"
context Deterministic_AI_1 begin

139
proof/invariant-abstract/Detype_AI.thy
View File

@ -23,10 +23,10 @@ locale Detype_AI =
cap_range cap = {} \<or>
(\<forall>ptr \<in> cap_range cap. \<exists>ko. kheap s ptr = Some ko)"
assumes mapM_x_storeWord:
"\<And>ptr. is_aligned ptr 2
\<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + of_nat x * 4) 0) [0..<n]
"\<And>ptr. is_aligned ptr word_size_bits
\<Longrightarrow> mapM_x (\<lambda>x. storeWord (ptr + of_nat x * word_size) 0) [0..<n]
= modify (underlying_memory_update
(\<lambda>m x. if \<exists>k. x = ptr + of_nat k \<and> k < n * 4 then 0 else m x))"
(\<lambda>m x. if \<exists>k. x = ptr + of_nat k \<and> k < n * word_size then 0 else m x))"
assumes empty_fail_freeMemory:
"empty_fail (freeMemory ptr bits)"
@ -73,7 +73,7 @@ lemma state_refs_of_detype:
definition
obj_reply_refs :: "cap \<Rightarrow> word32 set"
obj_reply_refs :: "cap \<Rightarrow> machine_word set"
where
"obj_reply_refs cap \<equiv> obj_refs cap \<union>
(case cap of cap.ReplyCap t m \<Rightarrow> {t} | _ \<Rightarrow> {})"
@ -897,15 +897,14 @@ lemma of_nat_le_pow:
apply simp
done
(* FIXME: move, fix underlying -1 problem *)
lemma maxword_32_conv: "(x::32 word) + 0xFFFFFFFF = x - 1" by simp
lemma maxword_len_conv': "(x::machine_word) + max_word = x - 1" by (simp add: max_word_def)
(* FIXME: copied from Retype_C and slightly adapted. *)
lemma (in Detype_AI) mapM_x_storeWord_step:
assumes al: "is_aligned ptr sz"
and sz2: "2 \<le> sz"
and sz2: "word_size_bits \<le> sz"
and sz: "sz <= word_bits"
shows "mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + 4 .e. ptr + 2 ^ sz - 1] =
shows "mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1] =
modify (underlying_memory_update
(\<lambda>m x. if x \<in> {x. \<exists>k. x = ptr + of_nat k \<and> k < 2 ^ sz} then 0 else m x))"
using al sz
@ -913,21 +912,20 @@ lemma (in Detype_AI) mapM_x_storeWord_step:
apply (subst if_not_P)
apply (subst not_less)
apply (erule is_aligned_no_overflow)
apply (simp add: mapM_x_map comp_def upto_enum_word maxword_32_conv del: upt.simps)
apply (simp add:Suc_unat_mask_div[simplified mask_2pm1 word_size_def] min_def)
apply (simp add: mapM_x_map comp_def upto_enum_word maxword_len_conv' del: upt.simps)
apply (simp add: Suc_unat_mask_div_obfuscated[simplified mask_2pm1] min_def)
apply (subst mapM_x_storeWord)
apply (erule is_aligned_weaken [OF _ sz2])
apply (rule arg_cong)
apply (subgoal_tac "2^2 = (4::nat)")
apply (cut_tac power_add[symmetric,of "2::nat" "sz - 2" 2])
apply (simp only: le_add_diff_inverse2[OF sz2])
apply simp
apply (subgoal_tac "2^word_size_bits = (word_size :: nat)")
apply (cut_tac power_add[symmetric,of "2::nat" "sz - word_size_bits" word_size_bits])
apply (simp only: le_add_diff_inverse2[OF sz2])
apply (simp add: word_size_size_bits_nat)
done
lemma (in Detype_AI) mapM_storeWord_clear_um:
"is_aligned p n \<Longrightarrow> 2\<le>n \<Longrightarrow> n<=word_bits \<Longrightarrow>
do_machine_op (mapM_x (\<lambda>p. storeWord p 0) [p, p + 4 .e. p + 2 ^ n - 1]) =
"is_aligned p n \<Longrightarrow> word_size_bits\<le>n \<Longrightarrow> n<=word_bits \<Longrightarrow>
do_machine_op (mapM_x (\<lambda>p. storeWord p 0) [p, p + word_size .e. p + 2 ^ n - 1]) =
modify (clear_um {x. \<exists>k. x = p + of_nat k \<and> k < 2 ^ n})"
apply (simp add: mapM_x_storeWord_step)
apply (rule ext)
@ -1000,7 +998,7 @@ lemma dom_known_length:
lemma of_bl_length2:
"length xs < word_bits - cte_level_bits \<Longrightarrow> of_bl xs * 16 < (2 :: word32) ^ (length xs + 4)"
"length xs < word_bits - cte_level_bits \<Longrightarrow> of_bl xs * 16 < (2 :: machine_word) ^ (length xs + 4)"
apply (simp add: power_add)
apply (rule word_mult_less_mono1)
apply (rule of_bl_length, simp add: word_bits_def)
@ -1122,9 +1120,9 @@ lemma refl_spec[simp]:
by clarsimp
lemma pre_helper:
"\<And>base x n. \<lbrakk> is_aligned (base :: word32) (n + 4); n + 4 < word_bits \<rbrakk>
\<Longrightarrow> base + (x && mask n) * 16 \<in> {base .. base + 2 ^ (n + 4) - 1}"
apply (subgoal_tac "(x && mask n) * 0x10 < 2 ^ (n + 4)")
"\<And>base x n. \<lbrakk> is_aligned (base :: machine_word) (n + (a::nat)); n + a < word_bits \<rbrakk>
\<Longrightarrow> base + (x && mask n) * 2^a \<in> {base .. base + 2 ^ (n + a) - 1}"
apply (subgoal_tac "(x && mask n) * bit(a) < 2 ^ (n + a)")
apply simp
apply (rule context_conjI)
apply (erule(1) is_aligned_no_wrap')
@ -1136,13 +1134,14 @@ lemma pre_helper:
apply (simp add: power_add)
apply (rule word_mult_less_mono1)
apply (rule and_mask_less_size, simp add: word_size word_bits_def)
apply simp
apply (simp add: p2_gt_0 word_bits_def)
apply (simp add: word_bits_def)
apply (drule power_strict_increasing[where a="2 :: nat"], simp_all)
apply (simp add: power_add[where a="2::nat"])
done
lemma pre_helper2:
"\<And>base x n. \<lbrakk> is_aligned (base :: word32) n; n < word_bits; 2 \<le> n; x < 2 ^ (n - 2) \<rbrakk>
"\<And>base x n. \<lbrakk> is_aligned (base :: machine_word) n; n < word_bits; 2 \<le> n; x < 2 ^ (n - 2) \<rbrakk>
\<Longrightarrow> base + x * 4 \<in> {base .. base + 2 ^ n - 1}"
apply (subgoal_tac "x * 4 < 2 ^ n")
apply simp
@ -1166,20 +1165,11 @@ lemma pre_helper2:
lemmas ucast_ucast_mask_8 = ucast_ucast_mask[where 'a=8, simplified, symmetric]
lemma subset_eq_notI: "\<lbrakk>a\<in> B;a\<notin> C\<rbrakk> \<Longrightarrow> \<not> B \<subseteq> C" by auto
lemma pspace_no_overlap_obj_range:
"\<lbrakk> pspace_no_overlap S s; kheap s p = Some obj \<rbrakk>
\<Longrightarrow> obj_range p obj \<inter> S = {}"
by (auto simp add: pspace_no_overlap_def obj_range_def field_simps)
lemma commute_grab_asm:
"(F \<Longrightarrow> monad_commute P f g) \<Longrightarrow> (monad_commute (P and (K F)) f g)"
by (clarsimp simp: monad_commute_def)
(* FIXME: generalised version of Arch_AI.range_cover_full *)
lemma range_cover_full:
"\<lbrakk>is_aligned (ptr :: 'a :: len word) sz;sz < len_of TYPE('a)\<rbrakk> \<Longrightarrow> range_cover ptr sz sz (Suc 0)"
@ -1192,68 +1182,6 @@ lemma range_cover_plus_us:
apply simp+
done
lemma commute_name_pre_state:
assumes "\<And>s. P s \<Longrightarrow> monad_commute (op = s) f g"
shows "monad_commute P f g"
using assms
by (clarsimp simp:monad_commute_def)
lemma commute_rewrite:
assumes rewrite: "\<And>s. Q s \<Longrightarrow> f s = t s"
and hold : "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>x. Q\<rbrace>"
shows "monad_commute R t g \<Longrightarrow> monad_commute (P and Q and R) f g"
apply (clarsimp simp:monad_commute_def bind_def split_def return_def)
apply (drule_tac x = s in spec)
apply (clarsimp simp:rewrite[symmetric])
apply (intro conjI)
apply (rule set_eqI)
apply (rule iffI)
apply clarsimp
apply (rule bexI[rotated],assumption)
apply (subst rewrite)
apply (rule use_valid[OF _ hold])
apply simp+
apply (erule bexI[rotated],simp)
apply clarsimp
apply (rule bexI[rotated],assumption)
apply (subst rewrite[symmetric])
apply (rule use_valid[OF _ hold])
apply simp+
apply (erule bexI[rotated],simp)
apply (intro iffI)
apply clarsimp
apply (rule bexI[rotated],assumption)
apply simp
apply (subst rewrite)
apply (erule(1) use_valid[OF _ hold])
apply simp
apply (clarsimp)
apply (drule bspec,assumption)
apply clarsimp
apply (metis rewrite use_valid[OF _ hold])
done
lemma mapM_x_commute:
assumes commute:
"\<And>r. monad_commute (P r) a (b r)"
and single:
"\<And>r x. \<lbrace>P r and K (f r \<noteq> f x) and P x\<rbrace> b x \<lbrace>\<lambda>v. P r \<rbrace>"
shows
"monad_commute (\<lambda>s. (distinct (map f list)) \<and> (\<forall>r\<in> set list. P r s)) a (mapM_x b list)"
apply (induct list)
apply (clarsimp simp:mapM_x_Nil return_def bind_def monad_commute_def)
apply (clarsimp simp:mapM_x_Cons)
apply (rule monad_commute_guard_imp)
apply (rule monad_commute_split)
apply assumption
apply (rule monad_commute_guard_imp[OF commute])
apply assumption
apply (wp hoare_vcg_ball_lift)
apply (rule single)
apply (clarsimp simp: image_def)
apply auto
done
lemma mask_sub: "n \<le> m \<Longrightarrow> mask m - mask n = mask m && ~~ mask n"
apply (simp add: field_simps)
apply (subst word_plus_and_or_coroll)
@ -1333,29 +1261,6 @@ lemma range_cover_tail_mask:
done
lemma monad_eq_split2:
assumes eq: " g' s = g s"
assumes tail:"\<And>r s. Q r s \<Longrightarrow> f r s = f' r s"
and hoare: "\<lbrace>P\<rbrace>g\<lbrace>\<lambda>r s. Q r s\<rbrace>" "P s"
shows "(g>>=f) s = (g'>>= f') s"
proof -
have pre: "\<And>aa bb. \<lbrakk>(aa, bb) \<in> fst (g s)\<rbrakk> \<Longrightarrow> Q aa bb"
using hoare by (auto simp: valid_def)
show ?thesis
apply (simp add:bind_def eq split_def image_def)
apply (rule conjI)
apply (rule set_eqI)
apply (clarsimp simp:Union_eq)
apply (metis pre surjective_pairing tail)
apply (metis pre surjective_pairing tail)
done
qed
lemma monad_eq_split_tail:
"\<lbrakk>f = g;a s = b s\<rbrakk> \<Longrightarrow> (a >>= f) s = ((b >>= g) s)"
by (simp add:bind_def)
lemma shift_distinct_helper:
"\<lbrakk> (x :: 'a :: len word) < bnd; y < bnd; x \<noteq> y; x << n = y << n; n < len_of TYPE('a);
bnd - 1 \<le> 2 ^ ((len_of TYPE('a)) - n) - 1 \<rbrakk>

2
proof/invariant-abstract/Finalise_AI.thy
View File

@ -984,7 +984,7 @@ crunch tcb_at[wp]: unbind_notification "tcb_at t"
locale Finalise_AI_3 = Finalise_AI_2 a b
for a :: "('a :: state_ext) itself"
and b :: "('b :: state_ext) itself" +
fixes replaceable_or_arch_update :: "'a state \<Rightarrow> 32 word \<times> bool list \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
fixes replaceable_or_arch_update :: "'a state \<Rightarrow> machine_word \<times> bool list \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool"
fixes c :: "'c itself"
assumes finalise_cap_invs:
"\<And> cap slot x.

14
proof/invariant-abstract/Interrupt_AI.thy
View File

@ -39,17 +39,20 @@ where
\<and> cte_wp_at (interrupt_derived cap) cte_ptr s
\<and> s \<turnstile> cap \<and> is_ntfn_cap cap)"
consts
arch_irq_control_inv_valid :: "arch_irq_control_invocation \<Rightarrow> ('a :: state_ext) state \<Rightarrow> bool"
primrec
irq_control_inv_valid :: "irq_control_invocation \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
irq_control_inv_valid :: "irq_control_invocation \<Rightarrow> 'a::state_ext state \<Rightarrow> bool"
where
"irq_control_inv_valid (Invocations_A.ArchIRQControl ivk) = \<bottom>"
"irq_control_inv_valid (Invocations_A.ArchIRQControl ivk) = (arch_irq_control_inv_valid ivk)"
| "irq_control_inv_valid (Invocations_A.IRQControl irq ptr ptr') =
(cte_wp_at (op = cap.NullCap) ptr and
cte_wp_at (op = cap.IRQControlCap) ptr'
and ex_cte_cap_wp_to is_cnode_cap ptr and real_cte_at ptr
and K (irq \<le> maxIRQ))"
locale Interrupt_AI =
fixes state_ext_type1 :: "('a :: state_ext) itself"
assumes decode_irq_control_invocation_inv[wp]:
@ -108,7 +111,12 @@ locale Interrupt_AI =
"\<And> f irq. empty_fail (maskInterrupt f irq)"
assumes handle_interrupt_invs [wp]:
"\<And> irq. \<lbrace>invs :: 'a state \<Rightarrow> bool\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. invs\<rbrace>"
assumes sts_arch_irq_control_inv_valid [wp]:
"\<And>i t st.
\<lbrace>arch_irq_control_inv_valid i :: 'a state \<Rightarrow> bool\<rbrace>
set_thread_state t st
\<lbrace>\<lambda>rv. arch_irq_control_inv_valid i\<rbrace>"
crunch inv[wp]: decode_irq_handler_invocation "P"
(simp: crunch_simps)

12
proof/invariant-abstract/Invariants_AI.thy
View File

@ -216,7 +216,7 @@ where
subsection "Valid caps and objects"
primrec
untyped_range :: "cap \<Rightarrow> word32 set"
untyped_range :: "cap \<Rightarrow> machine_word set"
where
"untyped_range (cap.UntypedCap dev p n f) = {p..p + (1 << n) - 1}"
| "untyped_range (cap.NullCap) = {}"
@ -231,10 +231,10 @@ where
| "untyped_range (cap.Zombie r b n) = {}"
| "untyped_range (cap.ArchObjectCap cap) = {}"
primrec
usable_untyped_range :: "cap \<Rightarrow> word32 set"
primrec (nonexhaustive)
usable_untyped_range :: "cap \<Rightarrow> machine_word set"
where
"usable_untyped_range (cap.UntypedCap _ p n f) =
"usable_untyped_range (UntypedCap _ p n f) =
(if f < 2^n then {p+of_nat f .. p + 2 ^ n - 1} else {})"
definition
@ -300,7 +300,7 @@ where
case c of
UntypedCap dev p sz idx \<Rightarrow> sz \<ge> 4
| NotificationCap r badge rights \<Rightarrow> AllowGrant \<notin> rights
| CNodeCap r bits guard \<Rightarrow> bits \<noteq> 0 \<and> length guard \<le> 32
| CNodeCap r bits guard \<Rightarrow> bits \<noteq> 0 \<and> length guard \<le> word_bits
| IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ
| Zombie r b n \<Rightarrow> (case b of None \<Rightarrow> n \<le> 5
| Some b \<Rightarrow> n \<le> 2 ^ b \<and> b \<noteq> 0)
@ -336,7 +336,7 @@ where
| NotificationCap r badge rights \<Rightarrow>
ntfn_at r s \<and> AllowGrant \<notin> rights
| CNodeCap r bits guard \<Rightarrow>
cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> 32
cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits
| ThreadCap r \<Rightarrow> tcb_at r s
| DomainCap \<Rightarrow> True
| ReplyCap r m \<Rightarrow> tcb_at r s

2
proof/invariant-abstract/IpcCancel_AI.thy
View File

@ -811,7 +811,7 @@ lemma suspend_unlive:
done
definition bound_refs_of_tcb :: "'a state \<Rightarrow> 32 word \<Rightarrow> (32 word \<times> reftype) set"
definition bound_refs_of_tcb :: "'a state \<Rightarrow> machine_word \<Rightarrow> (machine_word \<times> reftype) set"
where
"bound_refs_of_tcb s t \<equiv> case kheap s t of
Some (TCB tcb) \<Rightarrow> tcb_bound_refs (tcb_bound_notification tcb)

61
proof/invariant-abstract/LevityCatch_AI.thy
View File

@ -19,6 +19,12 @@ requalify_facts
end
(*FIXME: Move or remove *)
method spec for x :: "_ :: type" = (erule allE[of _ x])
method bspec for x :: "_ :: type" = (erule ballE[of _ _ x])
method prove for x :: "prop" = (rule revcut_rl[of "PROP x"])
lemmas aobj_ref_arch_cap_simps[simp] = aobj_ref_arch_cap
lemma detype_arch_state :
@ -81,7 +87,58 @@ lemma select_ext_wp[wp]:"\<lbrace>\<lambda>s. a s \<in> S \<longrightarrow> Q (a
(* FIXME: move *)
lemmas mapM_UNIV_wp = mapM_wp[where S="UNIV", simplified]
(* FIXME: move *)
lemma bexEI: "\<lbrakk>\<exists>x\<in>S. Q x; \<And>x. \<lbrakk>x \<in> S; Q x\<rbrakk> \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. P x" by blast
lemmas word_simps =
word_size word_ops_nth_size nth_ucast nth_shiftr nth_shiftl
lemma mask_split_aligned:
assumes len: "m \<le> a + len_of TYPE('a)"
assumes align: "is_aligned p a"
shows "(p && ~~ mask m) + (ucast ((ucast (p && mask m >> a))::'a::len word) << a) = p"
apply (insert align[simplified is_aligned_nth])
apply (subst word_plus_and_or_coroll; rule word_eqI; clarsimp simp: word_simps)
apply (rule iffI)
apply (erule disjE; clarsimp)
apply (case_tac "n < m"; case_tac "n < a")
using len by auto
lemma mask_split_aligned_neg:
fixes x :: "'a::len word"
fixes p :: "'b::len word"
assumes len: "a + len_of TYPE('a) \<le> len_of TYPE('b)"
"m = a + len_of TYPE('a)"
assumes x: "x \<noteq> ucast (p && mask m >> a)"
shows "(p && ~~ mask m) + (ucast x << a) = p \<Longrightarrow> False"
apply (subst (asm) word_plus_and_or_coroll)
apply (clarsimp simp: word_simps bang_eq)
subgoal for n
apply (drule test_bit_size)
apply (clarsimp simp: word_simps)
using len by arith
apply (insert x)
apply (erule notE)
apply (rule word_eqI)
subgoal for n
using len
apply (clarsimp simp: word_simps bang_eq)
apply (spec "n + a")
by (clarsimp simp: word_ops_nth_size word_size)
done
lemma mask_alignment_ugliness:
"\<lbrakk> x \<noteq> x + z && ~~ mask m;
is_aligned (x + z && ~~ mask m) m;
is_aligned x m;
\<forall>n \<ge> m. \<not>z !! n\<rbrakk>
\<Longrightarrow> False"
apply (erule notE)
apply (rule word_eqI)
apply (clarsimp simp: is_aligned_nth word_ops_nth_size word_size)
apply (subst word_plus_and_or_coroll)
apply (rule word_eqI)
apply (clarsimp simp: word_size)
subgoal for \<dots> na
apply (spec na)+
by simp
by auto
end

167
proof/invariant-abstract/Retype_AI.thy
View File

@ -43,32 +43,12 @@ lemma upto_enum_inc_1:
apply (subgoal_tac "unat (1 +a) = 1 + unat a")
apply simp
apply (subst unat_plus_simple[THEN iffD1])
apply (rule word_plus_mono_right2[where b = "2^32 - 2"])
apply (rule word_plus_mono_right2[where b = "2^word_bits - 2"])
apply (simp add:word_bits_def minus_one_norm)+
apply unat_arith
apply simp
done
(* FIXME: move *)
lemma monad_eq_split:
assumes "\<And>r s. Q r s \<Longrightarrow> f r s = f' r s"
"\<lbrace>P\<rbrace> g \<lbrace>\<lambda>r s. Q r s\<rbrace>"
"P s"
shows "(g >>= f) s = (g >>= f') s"
proof -
have pre: "\<And>rv s'. \<lbrakk>(rv, s') \<in> fst (g s)\<rbrakk> \<Longrightarrow> f rv s' = f' rv s'"
using assms unfolding valid_def
by (erule_tac x=s in allE) auto
show ?thesis
apply (simp add: bind_def image_def)
apply (intro conjI)
apply (rule set_eqI)
apply (clarsimp simp: Union_eq)
apply (rule iffI; elim exEI conjE; simp; elim exEI bexEI; clarsimp simp: pre)
apply (rule iffI; cases "snd (g s)"; simp; elim exEI bexEI; clarsimp simp: pre)
done
qed
lemma unat_of_nat_minus_1:
"\<lbrakk>n < 2^len_of TYPE('a);n\<noteq> 0\<rbrakk> \<Longrightarrow> (unat (((of_nat n):: 'a :: len word) - 1)) = n - 1"
apply (subst unat_minus_one)
@ -78,119 +58,6 @@ lemma unat_of_nat_minus_1:
apply (simp add:unat_of_nat word_bits_def)
done
definition monad_commute where
"monad_commute P a b \<equiv>
(\<forall>s. (P s \<longrightarrow> ((do x\<leftarrow>a;y\<leftarrow>b; return (x, y) od) s) = ((do y\<leftarrow>b;x\<leftarrow>a; return (x, y) od) s)))"
lemma monad_eq:
"a s = b s \<Longrightarrow> (a >>= g) s = (b >>= g) s"
by (auto simp:bind_def)
lemma monad_commute_simple:
"\<lbrakk>monad_commute P a b;P s\<rbrakk> \<Longrightarrow> ((do x\<leftarrow>a;y\<leftarrow>b; g x y od) s) = ((do y\<leftarrow>b;x\<leftarrow>a; g x y od) s)"
apply (clarsimp simp:monad_commute_def)
apply (drule spec)
apply (erule(1) impE)
apply (drule_tac g = "(\<lambda>t. g (fst t) (snd t))" in monad_eq)
apply (simp add:bind_assoc)
done
lemma commute_commute:
"monad_commute P f h \<Longrightarrow> monad_commute P h f"
apply (simp (no_asm) add: monad_commute_def)
apply (clarsimp)
apply (erule monad_commute_simple[symmetric])
apply simp
done
lemma assert_commute: "monad_commute (K G) (assert G) f"
by (clarsimp simp:assert_def monad_commute_def)
lemma cond_fail_commute: "monad_commute (K (\<not>G)) (when G fail) f"
by (clarsimp simp:when_def fail_def monad_commute_def)
lemma return_commute: "monad_commute \<top> (return a) f"
by (clarsimp simp: return_def bind_def monad_commute_def)
lemma monad_commute_guard_imp:
"\<lbrakk>monad_commute P f h; \<And>s. Q s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> monad_commute Q f h"
by (clarsimp simp:monad_commute_def)
lemma monad_commute_split:
"\<lbrakk>\<And>r. monad_commute (Q r) f (g r); monad_commute P f h;
\<lbrace>P'\<rbrace> h \<lbrace>\<lambda>r. Q r\<rbrace>\<rbrakk>
\<Longrightarrow> monad_commute (P and P') f (h>>=g)"
apply (simp (no_asm) add:monad_commute_def)
apply (clarsimp simp:bind_assoc)
apply (subst monad_commute_simple)
apply simp+
apply (rule_tac Q = "(\<lambda>x. Q x)" in monad_eq_split)
apply (subst monad_commute_simple[where a = f])
apply assumption
apply simp+
done
lemma monad_commute_get:
assumes hf: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. P\<rbrace>"
and hg: "\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>r. P\<rbrace>"
and eptyf: "empty_fail f" "empty_fail g"
shows "monad_commute \<top> f g"
proof -
have fsame: "\<And>a b s. (a,b) \<in> fst (f s) \<Longrightarrow> b = s"
by (drule use_valid[OF _ hf],auto)
have gsame: "\<And>a b s. (a,b) \<in> fst (g s) \<Longrightarrow> b = s"
by (drule use_valid[OF _ hg],auto)
note ef = empty_fail_not_snd[OF _ eptyf(1)]
note eg = empty_fail_not_snd[OF _ eptyf(2)]
show ?thesis
apply (simp add:monad_commute_def)
apply (clarsimp simp:bind_def split_def return_def)
apply (intro conjI)
apply (rule set_eqI)
apply (rule iffI)
apply (clarsimp simp:Union_eq dest!: singletonD)
apply (frule fsame)
apply clarsimp
apply (frule gsame)
apply (metis fst_conv snd_conv)
apply (clarsimp simp:Union_eq dest!: singletonD)
apply (frule gsame)
apply clarsimp
apply (frule fsame)
apply clarsimp
apply (metis fst_conv snd_conv)
apply (rule iffI)
apply (erule disjE)
apply (clarsimp simp:image_def)
apply (metis fsame)
apply (clarsimp simp:image_def)
apply (drule eg)
apply clarsimp
apply (rule bexI [rotated], assumption)
apply (frule gsame)
apply clarsimp
apply (erule disjE)
apply (clarsimp simp:image_def dest!:gsame)
apply (clarsimp simp:image_def)
apply (drule ef)
apply clarsimp
apply (frule fsame)
apply (erule bexI[rotated])
apply simp
done
qed
lemma range_to_bl':
"\<lbrakk> is_aligned (ptr :: 'a :: len word) bits; bits < len_of TYPE('a) \<rbrakk> \<Longrightarrow>
{ptr .. ptr + (2 ^ bits) - 1} = {x. take (len_of TYPE('a) - bits) (to_bl x)
@ -507,7 +374,7 @@ lemma word_plus_mono_right_split:
apply (auto simp:unat_plus_if_size word_size word_bits_def not_less)
done
lemmas word32_plus_mono_right_split = word_plus_mono_right_split[where 'a=32, folded word_bits_def]
lemmas machine_word_plus_mono_right_split = word_plus_mono_right_split[where 'a=machine_word_len, folded word_bits_def]
(* range_cover locale:
@ -846,7 +713,7 @@ proof -
proof (rule base_member_set)
from vp show "is_aligned x (obj_bits ko)" using ps'
by (auto elim!: valid_pspaceE pspace_alignedE)
show "obj_bits ko < len_of TYPE(32)"
show "obj_bits ko < len_of TYPE(machine_word_len)"
by (rule valid_pspace_obj_sizes [OF _ ranI, unfolded word_bits_def]) fact+
qed
@ -1213,7 +1080,7 @@ lemma retype_region_global_refs_disjoint:
apply (rule subsetI, simp only: mask_in_range[symmetric])
apply (clarsimp simp: ptr_add_def)
apply (intro conjI)
apply (rule word32_plus_mono_right_split[where sz = sz])
apply (rule machine_word_plus_mono_right_split[where sz = sz])
apply (erule(1) range_cover.range_cover_compare)
apply (simp add:range_cover_def word_bits_def)
apply (subst p_assoc_help)
@ -1290,7 +1157,7 @@ crunch cap_refs_in_kernel_window[wp]: do_machine_op "cap_refs_in_kernel_window"
locale Retype_AI_post_retype_invs =
fixes state_ext_t :: "'state_ext::state_ext itself"
and post_retype_invs_check :: "apiobject_type \<Rightarrow> bool"
and post_retype_invs :: "apiobject_type \<Rightarrow> word32 list \<Rightarrow> 'state_ext state \<Rightarrow> bool"
and post_retype_invs :: "apiobject_type \<Rightarrow> machine_word list \<Rightarrow> 'state_ext state \<Rightarrow> bool"
assumes post_retype_invs_def':
"post_retype_invs tp refs \<equiv>
if post_retype_invs_check tp
@ -1324,13 +1191,13 @@ lemma honestly_16_10:
definition
caps_no_overlap :: "word32 \<Rightarrow> nat \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
caps_no_overlap :: "machine_word \<Rightarrow> nat \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
where
"caps_no_overlap ptr sz s \<equiv> \<forall>cap \<in> ran (caps_of_state s).
untyped_range cap \<inter> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
\<longrightarrow> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untyped_range cap"
definition caps_overlap_reserved :: "word32 set \<Rightarrow> ('z::state_ext) state \<Rightarrow> bool"
definition caps_overlap_reserved :: "machine_word set \<Rightarrow> ('z::state_ext) state \<Rightarrow> bool"
where
"caps_overlap_reserved S (s :: ('z::state_ext) state) \<equiv> \<forall>cap \<in> ran (caps_of_state s).
(is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {})"
@ -1672,11 +1539,11 @@ lemma retype_addrs_obj_range_subset_strong:
and not_0:"n\<noteq> 0"
and tyunt:"ty\<noteq> Untyped"
note n_less = range_cover.range_cover_n_less[OF cover]
have unat_of_nat_m1: "unat (of_nat n - (1::word32)) < n"
have unat_of_nat_m1: "unat (of_nat n - (1::machine_word)) < n"
using not_0 n_less
by (simp add:unat_of_nat_minus_1)
have decomp:"of_nat n * 2 ^ obj_bits_api ty us = of_nat (n - 1) * 2 ^ (obj_bits (default_object ty dev us))
+ (2 :: word32) ^ obj_bits (default_object ty dev us)"
+ (2 :: machine_word) ^ obj_bits (default_object ty dev us)"
apply (simp add:distrib_right[where b = "1::'a::len word",simplified,symmetric])
using not_0 n_less
apply (simp add: unat_of_nat_minus_1 obj_bits_api_def3 tyunt cong: obj_bits_cong)
@ -1706,8 +1573,8 @@ lemma retype_addrs_obj_range_subset_strong:
apply (simp add:unat_of_nat_m1 less_imp_le)
using cover
apply (simp add:range_cover_def word_bits_def)
apply (rule word32_plus_mono_right_split[where sz = sz])
using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::word32))"]
apply (rule machine_word_plus_mono_right_split[where sz = sz])
using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::machine_word))"]
apply (clarsimp simp:unat_of_nat_m1)
using cover
apply (simp add:range_cover_def word_bits_def)
@ -1800,7 +1667,7 @@ lemma usable_range_subseteq:
lemma usable_range_emptyD:
"\<lbrakk>cap_aligned cap;is_untyped_cap cap ;usable_untyped_range cap = {}\<rbrakk> \<Longrightarrow> 2 ^ cap_bits cap \<le> free_index_of cap"
apply (clarsimp simp:is_cap_simps not_le free_index_of_def cap_aligned_def split:if_splits)
apply (drule(1) of_nat_less_pow_32)
apply (drule(1) of_nat_power [where 'a=machine_word_len, folded word_bits_def])
apply (drule word_plus_mono_right[OF _ is_aligned_no_overflow[unfolded p_assoc_help],rotated])
apply simp
apply (simp add:p_assoc_help)
@ -2224,7 +2091,7 @@ lemma p_in_obj_range:
apply (drule valid_obj_sizes, erule ranI)
apply (simp add: obj_range_def add_diff_eq[symmetric])
apply (erule is_aligned_no_wrap')
apply (erule word_power_less_1[where 'a=32, folded word_bits_def])
apply (erule word_power_less_1[where 'a=machine_word_len, folded word_bits_def])
done
lemma p_in_obj_range_internal:
@ -2288,8 +2155,8 @@ locale retype_region_proofs_invs
+ Retype_AI_post_retype_invs "TYPE('state_ext)" post_retype_invs_check post_retype_invs
for s :: "'state_ext :: state_ext state"
and ty us ptr sz n ps s' dev post_retype_invs_check
and post_retype_invs :: "apiobject_type \<Rightarrow> word32 list \<Rightarrow> 'state_ext state \<Rightarrow> bool" +
fixes region_in_kernel_window :: "word32 set \<Rightarrow> 'state_ext state \<Rightarrow> bool"
and post_retype_invs :: "apiobject_type \<Rightarrow> machine_word list \<Rightarrow> 'state_ext state \<Rightarrow> bool" +
fixes region_in_kernel_window :: "machine_word set \<Rightarrow> 'state_ext state \<Rightarrow> bool"
assumes valid_global_refs: "valid_global_refs s \<Longrightarrow> valid_global_refs s'"
assumes valid_arch_state: "valid_arch_state s \<Longrightarrow> valid_arch_state s'"
assumes valid_arch_objs': "valid_arch_objs s \<Longrightarrow> valid_arch_objs s'"
@ -2342,11 +2209,11 @@ locale Retype_AI
+ Retype_AI_dmo_eq_kernel_restricted state_ext_t machine_op_t
for state_ext_t :: "'state_ext::state_ext itself"
and post_retype_invs_check
and post_retype_invs :: "apiobject_type \<Rightarrow> word32 list \<Rightarrow> 'state_ext state \<Rightarrow> bool"
and post_retype_invs :: "apiobject_type \<Rightarrow> machine_word list \<Rightarrow> 'state_ext state \<Rightarrow> bool"
and no_gs_types
and machine_op_t :: "'machine_op_t itself" +
fixes state_ext'_t :: "'state_ext'::state_ext itself"
fixes region_in_kernel_window :: "word32 set \<Rightarrow> 'state_ext state \<Rightarrow> bool"
fixes region_in_kernel_window :: "machine_word set \<Rightarrow> 'state_ext state \<Rightarrow> bool"
assumes invs_post_retype_invs:
"\<And>(s::'state_ext state) ty refs. invs s \<Longrightarrow> post_retype_invs ty refs s"
assumes equal_kernel_mappings_trans_state[simp]:

37
proof/invariant-abstract/Syscall_AI.thy
View File

@ -522,29 +522,22 @@ lemma sts_mcpriority_tcb_at_ct[wp]:
apply clarsimp
done
lemma sts_tcb_inv_wf [wp]:
"\<lbrace>tcb_inv_wf i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. tcb_inv_wf i\<rbrace>"
apply (case_tac i)
apply (wp set_thread_state_valid_cap hoare_vcg_all_lift hoare_vcg_const_imp_lift
| simp add: tcb_at_typ split: option.split
| safe
| wp sts_obj_at_impossible)+
done
lemma sts_valid_inv[wp]:
"\<lbrace>valid_invocation i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_invocation i\<rbrace>"
apply (case_tac i, simp_all add: ntfn_at_typ ep_at_typ
sts_valid_untyped_inv sts_valid_arch_inv)
apply (wp | simp)+
apply (rename_tac tcb_invocation)
apply (case_tac tcb_invocation,
(wp set_thread_state_valid_cap hoare_vcg_all_lift hoare_vcg_const_imp_lift|
simp add: tcb_at_typ split: option.split|
safe |
wp sts_obj_at_impossible )+)
apply (rename_tac cnode_invocation)
apply (case_tac cnode_invocation, simp_all)[1]
apply (case_tac cnode_invocation,
(wp set_thread_state_valid_cap sts_nasty_bit hoare_vcg_const_imp_lift
| simp)+)
apply (rename_tac irq_control_invocation)
apply (case_tac irq_control_invocation; wpsimp)
apply (rename_tac irq_handler_invocation)
apply (case_tac irq_handler_invocation;
wpsimp wp: ex_cte_cap_to_pres hoare_vcg_ex_lift set_thread_state_valid_cap)
done
by (cases i; wpsimp simp: sts_valid_untyped_inv sts_valid_arch_inv;
rename_tac i'; case_tac i'; simp;
wpsimp wp: set_thread_state_valid_cap sts_nasty_bit
hoare_vcg_const_imp_lift hoare_vcg_ex_lift)
lemma sts_Restart_stay_simple:
@ -766,7 +759,7 @@ proof (induct param rule: resolve_address_bits'.induct)
apply (elim conjE exE disjE)
apply ((clarsimp simp: whenE_def bindE_def bind_def lift_def liftE_def
throwError_def returnOk_def return_def valid_fault_def
valid_cap_def2 wellformed_cap_def
valid_cap_def2 wellformed_cap_def word_bits_def
split: if_split_asm cap.splits)+)[4]
apply (split if_split_asm)
apply (clarsimp simp: whenE_def bindE_def bind_def lift_def liftE_def

8
proof/invariant-abstract/Tcb_AI.thy
View File

@ -590,7 +590,6 @@ lemma out_no_cap_to_trivial:
apply (wpsimp wp: hoare_vcg_const_Ball_lift out_cte_wp_at_trivialT)
done
(* FIXME: eliminate *)
lemmas thread_set_no_cap_to_trivial = thread_set_no_cap_obj_ref_trivial
@ -865,11 +864,6 @@ lemma (in Tcb_AI) tcbinv_invs:
apply clarsimp
done
crunch typ_at[wp]: invoke_tcb "\<lambda>s. P (typ_at T p s)"
(ignore: check_cap_at setNextPC zipWithM
wp: hoare_drop_imps mapM_x_wp' check_cap_inv
simp: crunch_simps)
lemma inj_ucast: "\<lbrakk> uc = ucast; is_up uc \<rbrakk> \<Longrightarrow> inj uc"
apply simp
apply (rule inj_on_inverseI)
@ -1015,7 +1009,7 @@ where
primrec
thread_control_target :: "tcb_invocation \<Rightarrow> word32"
thread_control_target :: "tcb_invocation \<Rightarrow> machine_word"
where
"thread_control_target (tcb_invocation.ThreadControl a b c d e f g h) = a"

160
proof/invariant-abstract/Untyped_AI.thy
View File

@ -19,6 +19,8 @@ context begin interpretation Arch .
requalify_consts
region_in_kernel_window
arch_default_cap
second_level_tables
end
primrec
@ -61,7 +63,7 @@ locale Untyped_AI_of_bl_nat_to_cref =
lemma cnode_cap_bits_range:
"\<lbrakk> cte_wp_at P p s; invs s \<rbrakk> \<Longrightarrow>
(\<exists>c. P c \<and> (is_cnode_cap c \<longrightarrow>
(\<lambda>n. n > 0 \<and> n < 28 \<and> is_aligned (obj_ref_of c) (n + 4)) (bits_of c)))"
(\<lambda>n. n > 0 \<and> n < (word_bits - 4) \<and> is_aligned (obj_ref_of c) (n + 4)) (bits_of c)))"
apply (frule invs_valid_objs)
apply (drule(1) cte_wp_at_valid_objs_valid_cap)
apply clarsimp
@ -283,7 +285,7 @@ locale Untyped_AI_arch =
"\<And>ptr sz s x6 us n dev. \<lbrakk>pspace_no_overlap_range_cover ptr sz (s::'state_ext state) \<and> x6 \<noteq> ASIDPoolObj \<and> range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \<and> ptr \<noteq> 0(*; tp = ArchObject x6*)\<rbrakk>
\<Longrightarrow> \<forall>y\<in>{0..<n}. s
\<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x6) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0..<n])
(kheap s)\<rparr> \<turnstile> ArchObjectCap (ARM_A.arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)"
(kheap s)\<rparr> \<turnstile> ArchObjectCap (arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)"
assumes init_arch_objects_descendants_range[wp]:
"\<And>x cref ty ptr n us y. \<lbrace>\<lambda>(s::'state_ext state). descendants_range x cref s \<rbrace> init_arch_objects ty ptr n us y
@ -373,20 +375,23 @@ qed
lemma range_cover_stuff:
"\<lbrakk>0 < n;n \<le> unat ((2::word32) ^ sz - of_nat rv >> bits);
notes unat_power_lower_machine = unat_power_lower[where 'a=machine_word_len]
notes unat_of_nat_machine = unat_of_nat_eq[where 'a=machine_word_len]
shows
"\<lbrakk>0 < n;n \<le> unat ((2::machine_word) ^ sz - of_nat rv >> bits);
rv \<le> 2^ sz; sz < word_bits; is_aligned w sz\<rbrakk> \<Longrightarrow>
rv \<le> unat (alignUp (w + of_nat rv) bits - w) \<and>
(alignUp (w + of_nat rv) bits) && ~~ mask sz = w \<and>
range_cover (alignUp (w + ((of_nat rv)::word32)) bits) sz bits n"
range_cover (alignUp (w + ((of_nat rv)::machine_word)) bits) sz bits n"
apply (clarsimp simp: range_cover_def)
proof (intro conjI)
assume not_0 : "0<n"
assume bound : "n \<le> unat ((2::word32) ^ sz - of_nat rv >> bits)" "rv\<le> 2^sz"
assume bound : "n \<le> unat ((2::machine_word) ^ sz - of_nat rv >> bits)" "rv\<le> 2^sz"
"sz < word_bits"
assume al: "is_aligned w sz"
have space: "(2::word32) ^ sz - of_nat rv \<le> 2^ sz"
have space: "(2::machine_word) ^ sz - of_nat rv \<le> 2^ sz"
apply (rule word_sub_le[OF word_of_nat_le])
apply (clarsimp simp: bound unat_power_lower32)
apply (clarsimp simp: bound unat_power_lower_machine)
done
show cmp: "bits \<le> sz"
using not_0 bound
@ -396,7 +401,7 @@ lemma range_cover_stuff:
apply (drule le_trans)
apply (rule word_le_nat_alt[THEN iffD1])
apply (rule le_shiftr[OF space])
apply (subgoal_tac "(2::word32)^sz >> bits = 0")
apply (subgoal_tac "(2::machine_word)^sz >> bits = 0")
apply simp
apply (rule and_mask_eq_iff_shiftr_0[THEN iffD1])
apply (simp add: and_mask_eq_iff_le_mask)
@ -404,18 +409,18 @@ lemma range_cover_stuff:
apply (simp add: word_bits_def mask_def power_overflow)
apply (subst le_mask_iff_lt_2n[THEN iffD1])
apply (simp add: word_bits_def)
apply (simp add: word_less_nat_alt[THEN iffD2] unat_power_lower32)
apply (simp add: word_less_nat_alt[THEN iffD2] unat_power_lower_machine)
done
have shiftr_t2n[simp]:"(2::word32)^sz >> bits = 2^ (sz - bits)"
have shiftr_t2n[simp]:"(2::machine_word)^sz >> bits = 2^ (sz - bits)"
using bound cmp
apply (case_tac "sz = 0",simp)
apply (subgoal_tac "(1::word32) << sz >> bits = 2^ (sz -bits)")
apply (subgoal_tac "(1::machine_word) << sz >> bits = 2^ (sz -bits)")
apply simp
apply (subst shiftl_shiftr1)
apply (simp add: word_size word_bits_def shiftl_t2n word_1_and_bl)+
done
have cmp2[simp]: "alignUp (of_nat rv) bits < (2 :: word32) ^ sz"
have cmp2[simp]: "alignUp (of_nat rv) bits < (2 :: machine_word) ^ sz"
using bound cmp not_0
apply -
apply (case_tac "rv = 0")
@ -423,7 +428,7 @@ lemma range_cover_stuff:
apply (clarsimp simp: alignUp_def2)
apply (subst mask_eq_x_eq_0[THEN iffD1])
apply (simp add: and_mask_eq_iff_le_mask mask_def)
apply (simp add: p2_gt_0[where 'a=32, folded word_bits_def])
apply (simp add: p2_gt_0[where 'a=machine_word_len, folded word_bits_def])
apply (simp add: alignUp_def3)
apply (subgoal_tac "1 \<le> unat (2 ^ sz - of_nat rv >> bits)")
prefer 2
@ -433,7 +438,7 @@ lemma range_cover_stuff:
apply (simp add: shiftr_div_2n')
apply (simp add: td_gal[symmetric])
apply (subst (asm) unat_sub)
apply (simp add: word_of_nat_le unat_power_lower32)
apply (simp add: word_of_nat_le unat_power_lower_machine)
apply (simp add: le_diff_conv2 word_of_nat_le unat_le_helper word_less_nat_alt)
apply (rule le_less_trans[OF unat_plus_gt])
apply (rule less_le_trans[where y = "2^bits + unat (of_nat rv)"])
@ -448,7 +453,7 @@ lemma range_cover_stuff:
apply simp
done
show "n + unat (alignUp (w + ((of_nat rv)::word32)) bits && mask sz >> bits) \<le> 2 ^ (sz - bits)"
show "n + unat (alignUp (w + ((of_nat rv)::machine_word)) bits && mask sz >> bits) \<le> 2 ^ (sz - bits)"
using not_0 bound cmp
apply -
apply (erule le_trans[OF add_le_mono])
@ -493,37 +498,42 @@ lemma range_cover_stuff:
apply (case_tac "rv = 0")
apply simp
apply (rule le_trans[OF _ word_le_nat_alt[THEN iffD1,OF alignUp_ge]])
apply (subst unat_of_nat32)
apply (erule le_less_trans)
apply simp
apply (simp_all add: word_bits_def)[2]
apply (subst unat_of_nat_machine)
apply (erule le_less_trans)
apply (rule power_strict_increasing)
apply (simp_all add: word_bits_def)[4]
apply (rule alignUp_is_aligned_nz[where x = "2^sz"])
apply (rule is_aligned_weaken[OF is_aligned_triv2])
apply (simp_all add: word_bits_def)[2]
apply (subst word_of_nat_le)
apply (subst unat_power_lower32)
apply simp+
apply (erule of_nat_neq_0)
apply (erule le_less_trans)
apply (subst word_bits_def[symmetric])
apply simp
done
apply (rule is_aligned_weaken[OF is_aligned_triv2])
apply (simp_all add: word_bits_def)[2]
apply (subst word_of_nat_le)
apply (subst unat_power_lower_machine)
apply (simp add: word_bits_def)+
apply (erule of_nat_neq_0)
apply (erule le_less_trans)
apply (rule power_strict_increasing)
apply (simp add: word_bits_def)+
done
show "alignUp (w + of_nat rv) bits && ~~ mask sz = w"
using bound not_0 cmp al
apply (clarsimp simp: alignUp_plus[OF is_aligned_weaken]
mask_out_add_aligned[symmetric])
apply (clarsimp simp: and_not_mask)
apply (subgoal_tac "alignUp ((of_nat rv)::word32) bits >> sz = 0")
apply (subgoal_tac "alignUp ((of_nat rv)::machine_word) bits >> sz = 0")
apply simp
apply (simp add: le_mask_iff[symmetric] mask_def)
done
show "sz < 32" by (simp add: bound(3)[unfolded word_bits_def, simplified])
qed
qed (simp add: word_bits_def)
context Arch begin
(*FIXME: generify proof that uses this *)
lemmas range_cover_stuff_arch = range_cover_stuff[unfolded word_bits_def, simplified]
end
lemma cte_wp_at_range_cover:
"\<lbrakk>bits < word_bits; rv\<le> 2^ sz; invs s;
cte_wp_at (op = (cap.UntypedCap dev w sz idx)) p s;
0 < n; n \<le> unat ((2::word32) ^ sz - of_nat rv >> bits)\<rbrakk>
0 < n; n \<le> unat ((2::machine_word) ^ sz - of_nat rv >> bits)\<rbrakk>
\<Longrightarrow> range_cover (alignUp (w + of_nat rv) bits) sz bits n"
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (frule(1) caps_of_state_valid)
@ -535,7 +545,7 @@ lemma cte_wp_at_range_cover:
lemma le_mask_le_2p:
"\<lbrakk>idx \<le> unat ((ptr::word32) && mask sz);sz < word_bits\<rbrakk> \<Longrightarrow> idx < 2^ sz"
"\<lbrakk>idx \<le> unat ((ptr::machine_word) && mask sz);sz < word_bits\<rbrakk> \<Longrightarrow> idx < 2^ sz"
apply (erule le_less_trans)
apply (rule unat_less_helper)
apply simp
@ -666,18 +676,18 @@ lemma cases_imp_eq:
by blast
lemma inj_16:
"\<lbrakk> of_nat x * 16 = of_nat y * (16 :: word32);
"\<lbrakk> of_nat x * 16 = of_nat y * (16 :: machine_word);
x < bnd; y < bnd; bnd \<le> 2 ^ (word_bits - 4) \<rbrakk>
\<Longrightarrow> of_nat x = (of_nat y :: word32)"
\<Longrightarrow> of_nat x = (of_nat y :: machine_word)"
apply (fold shiftl_t2n [where n=4, simplified, simplified mult.commute])
apply (simp only: word_bl.Rep_inject[symmetric]
bl_shiftl)
apply (drule(1) order_less_le_trans)+
apply (drule of_nat_mono_maybe[rotated, where 'a=32])
apply (drule of_nat_mono_maybe[rotated, where 'a=machine_word_len])
apply (rule power_strict_increasing)
apply (simp add: word_bits_def)
apply simp
apply (drule of_nat_mono_maybe[rotated, where 'a=32])
apply (drule of_nat_mono_maybe[rotated, where 'a=machine_word_len])
apply (rule power_strict_increasing)
apply (simp add: word_bits_def)
apply simp
@ -689,12 +699,15 @@ lemma inj_16:
lemma of_nat_shiftR:
"a < 2 ^ word_bits \<Longrightarrow>
unat (of_nat (shiftR a b)::word32) = unat ((of_nat a :: word32) >> b)"
unat (of_nat (shiftR a b)::machine_word) = unat ((of_nat a :: machine_word) >> b)"
apply (subst shiftr_div_2n')
apply (clarsimp simp: shiftR_nat)
apply (subst unat_of_nat32)
apply (subst unat_of_nat_eq[where 'a=machine_word_len])
apply (simp only: word_bits_def)
apply (erule le_less_trans[OF div_le_dividend])
apply (simp add: unat_of_nat32)
apply (subst unat_of_nat_eq[where 'a=machine_word_len])
apply (simp only: word_bits_def)
apply simp
done
@ -1437,17 +1450,17 @@ lemma of_nat_shift_distinct_helper:
done
lemmas of_nat_shift_distinct_helper32 = of_nat_shift_distinct_helper[where 'a=32, folded word_bits_def]
lemmas of_nat_shift_distinct_helper_machine = of_nat_shift_distinct_helper[where 'a=machine_word_len, folded word_bits_def]
lemma ptr_add_distinct_helper:
"\<lbrakk> ptr_add (p :: word32) (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x \<noteq> y;
"\<lbrakk> ptr_add (p :: machine_word) (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x \<noteq> y;
x < bnd; y < bnd; n < word_bits;
bnd \<le> 2 ^ (word_bits - n) \<rbrakk>
\<Longrightarrow> P"
apply (clarsimp simp: ptr_add_def word_unat_power[symmetric]
shiftl_t2n[symmetric, simplified mult.commute])
apply (erule(5) of_nat_shift_distinct_helper32)
apply (erule(5) of_nat_shift_distinct_helper_machine)
done
@ -1608,12 +1621,12 @@ lemma retype_region_distinct_sets:
apply (clarsimp simp: retype_addrs_def distinct_prop_map)
apply (rule distinct_prop_distinct)
apply simp
apply (subgoal_tac "of_nat y * (2::word32) ^ obj_bits_api tp us \<noteq> of_nat x * 2 ^ obj_bits_api tp us")
apply (subgoal_tac "of_nat y * (2::machine_word) ^ obj_bits_api tp us \<noteq> of_nat x * 2 ^ obj_bits_api tp us")
apply (case_tac tp) defer
apply (simp add:cap_range_def ptr_add_def)+
apply (clarsimp simp: ptr_add_def word_unat_power[symmetric]
shiftl_t2n[simplified mult.commute, symmetric])
apply (erule(2) of_nat_shift_distinct_helper[where 'a=32 and n = "obj_bits_api tp us"])
apply (erule(2) of_nat_shift_distinct_helper[where 'a=machine_word_len and n = "obj_bits_api tp us"])
apply simp
apply (simp add:range_cover_def)
apply (erule range_cover.range_cover_n_le)
@ -2035,10 +2048,10 @@ lemma op_equal: "(\<lambda>x. x = c) = (op = c)" by (rule ext) auto
lemma mask_out_eq_0:
"\<lbrakk>idx < 2^ sz;sz<word_bits\<rbrakk> \<Longrightarrow> ((of_nat idx)::word32) && ~~ mask sz = 0"
"\<lbrakk>idx < 2^ sz;sz<word_bits\<rbrakk> \<Longrightarrow> ((of_nat idx)::machine_word) && ~~ mask sz = 0"
apply (clarsimp simp: mask_out_sub_mask)
apply (subst less_mask_eq[symmetric])
apply (erule(1) of_nat_less_pow_32)
apply (erule(1) of_nat_power[where 'a=machine_word_len, folded word_bits_def])
apply simp
done
@ -2063,7 +2076,7 @@ lemma is_aligned_neg_mask_eq':
(* FIXME: move *)
lemma neg_mask_mask_unat:
"sz < word_bits \<Longrightarrow>
unat ((ptr::word32) && ~~ mask sz) + unat (ptr && mask sz) = unat ptr"
unat ((ptr::machine_word) && ~~ mask sz) + unat (ptr && mask sz) = unat ptr"
apply (subst unat_plus_simple[THEN iffD1,symmetric])
apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask[OF le_refl]])
apply (rule and_mask_less')
@ -2293,7 +2306,7 @@ proof -
apply -
apply (erule disjE)
apply (erule cte_wp_at_caps_descendants_range_inI[OF _ _ _ range_cover.sz(1)
[where 'a=32, folded word_bits_def]])
[where 'a=machine_word_len, folded word_bits_def]])
apply (simp add:cte_wp_at_caps_of_state desc_range)+
done
thus "descendants_range_in usable_range cref s"
@ -2313,7 +2326,7 @@ lemma ps_no_overlap[simp]: "\<not> reset \<longrightarrow> pspace_no_overlap_ran
using misc cte_wp_at cover idx_cases
apply clarsimp
apply (erule cte_wp_at_pspace_no_overlapI[OF _ _ _
range_cover.sz(1)[where 'a=32, folded word_bits_def]])
range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]])
apply (simp add: cte_wp_at_caps_of_state)
apply simp+
done
@ -2323,7 +2336,7 @@ lemma caps_no_overlap[simp]: "caps_no_overlap ptr sz s"
apply -
apply (erule disjE)
apply (erule cte_wp_at_caps_no_overlapI[OF _ _ _ range_cover.sz(1)
[where 'a=32, folded word_bits_def]])
[where 'a=machine_word_len, folded word_bits_def]])
apply (simp add:cte_wp_at_caps_of_state)+
apply (erule descendants_range_caps_no_overlapI)
apply (simp add:cte_wp_at_caps_of_state desc_range)+
@ -2388,14 +2401,14 @@ lemma usable_range_disjoint:
{ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {}"
proof -
have idx_compare''[simp]:
"unat ((ptr && mask sz) + (of_nat (length slots) * (2::word32) ^ obj_bits_api tp us)) < 2 ^ sz
"unat ((ptr && mask sz) + (of_nat (length slots) * (2::machine_word) ^ obj_bits_api tp us)) < 2 ^ sz
\<Longrightarrow> ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1
< ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us"
apply (rule minus_one_helper,simp)
apply (rule neq_0_no_wrap)
apply (rule word32_plus_mono_right_split)
apply (rule machine_word_plus_mono_right_split)
apply (simp add:shiftl_t2n range_cover_unat[OF cover] field_simps)
apply (simp add:range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+
apply (simp add:range_cover.sz[where 'a=machine_word_len, folded word_bits_def, OF cover])+
done
show ?thesis
apply (clarsimp simp:mask_out_sub_mask blah)
@ -2499,14 +2512,14 @@ lemma valid_untyped_cap_inc:
apply simp
apply (erule disjoint_subset[rotated])
apply (frule(1) le_mask_le_2p[OF _
range_cover.sz(1)[where 'a=32, folded word_bits_def]])
range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]])
apply clarsimp
apply (rule word_plus_mono_right)
apply (rule word_of_nat_le)
apply (simp add: unat_of_nat32 range_cover_unat field_simps)
apply (simp add: unat_of_nat_eq[where 'a=machine_word_len] range_cover_unat field_simps)
apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask[OF le_refl]])
apply (simp add: word_less_nat_alt
unat_power_lower[where 'a=32, folded word_bits_def])
unat_power_lower[where 'a=machine_word_len, folded word_bits_def])
apply (simp add: range_cover_unat range_cover.unat_of_nat_shift shiftl_t2n field_simps)
apply (subst add.commute)
apply (simp add: range_cover.range_cover_compare_bound)
@ -3081,16 +3094,15 @@ lemma create_cap_irq_handlers[wp]:
crunch valid_arch_objs[wp]: create_cap "valid_arch_objs"
(simp: crunch_simps)
locale Untyped_AI_nonempty_table =
fixes state_ext_t :: "('state_ext::state_ext) itself"
fixes nonempty_table :: "word32 set \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
fixes nonempty_table :: "machine_word set \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool"
assumes create_cap_valid_arch_caps[wp]:
"\<And>tp oref sz dev cref p.\<lbrace>valid_arch_caps
and valid_cap (default_cap tp oref sz dev)
and (\<lambda>(s::'state_ext state). \<forall>r\<in>obj_refs (default_cap tp oref sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
and cte_wp_at (op = cap.NullCap) cref
and K (tp \<noteq> ArchObject ASIDPoolObj)\<rbrace>
create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>"
@ -3102,11 +3114,11 @@ locale Untyped_AI_nonempty_table =
assumes nonempty_table_caps_of:
"\<And>S ko. nonempty_table S ko \<Longrightarrow> caps_of ko = {}"
assumes init_arch_objects_nonempty_table:
"\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
"\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
\<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and
K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us))\<rbrace>
init_arch_objects tp ptr bits us refs
\<lbrace>\<lambda>rv. \<lambda>s :: 'state_ext state. \<not> (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)\<rbrace>"
\<lbrace>\<lambda>rv. \<lambda>s :: 'state_ext state. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>"
crunch valid_global_objs[wp]: create_cap "valid_global_objs"
(simp: crunch_simps)
@ -3182,7 +3194,7 @@ lemma (in Untyped_AI_nonempty_table) create_cap_invs[wp]:
and real_cte_at cref
and (\<lambda>(s::'state_ext state). \<forall>r\<in>obj_refs (default_cap tp oref sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
and K (p \<noteq> cref \<and> tp \<noteq> ArchObject ASIDPoolObj)\<rbrace>
create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (rule hoare_pre)
@ -3213,9 +3225,9 @@ lemma create_cap_no_cap[wp]:
unfolding create_cap_def cte_wp_at_caps_of_state by wpsimp
lemma (in Untyped_AI_nonempty_table) create_cap_nonempty_tables[wp]:
"\<lbrace>\<lambda>s. P (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) p s)\<rbrace>
"\<lbrace>\<lambda>s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>
create_cap tp sz p' dev (cref, oref)
\<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) p s)\<rbrace>"
\<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>"
apply (rule hoare_pre)
apply (rule hoare_use_eq [where f=arch_state, OF create_cap_arch_state])
apply (simp add: create_cap_def set_cdt_def)
@ -3265,7 +3277,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs_inv:
real_cte_at (fst tup) s)
\<and> (\<forall>tup \<in> set ((cref,oref)#list). \<forall>r \<in> obj_refs (default_cap tp (snd tup) sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> Structures_A.obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
\<and> distinct (p # (map fst ((cref,oref)#list)))
\<and> tp \<noteq> ArchObject ASIDPoolObj) \<rbrace>
create_cap tp sz p dev (cref,oref)
@ -3290,7 +3302,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs_inv:
real_cte_at (fst tup) s)
\<and> (\<forall>tup \<in> set list. \<forall>r \<in> obj_refs (default_cap tp (snd tup) sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> Structures_A.obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
\<and> distinct (p # (map fst list))
\<and> tp \<noteq> ArchObject ASIDPoolObj) \<rbrace>"
apply (rule hoare_pre)
@ -3342,7 +3354,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs:
real_cte_at (fst tup) s)
\<and> (\<forall>tup \<in> set (zip crefs orefs). \<forall>r \<in> obj_refs (default_cap tp (snd tup) sz dev).
(\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> Structures_A.obj_refs cap) p' s)
\<and> \<not> obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)
\<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
\<and> distinct (p # (map fst (zip crefs orefs)))
\<and> tp \<noteq> ArchObject ASIDPoolObj)
and K (set orefs \<subseteq> set (retype_addrs ptr tp (length slots) us))\<rbrace>
@ -3441,7 +3453,7 @@ lemma retype_region_refs_distinct[wp]:
| drule subsetD [OF obj_refs_default_cap]
less_two_pow_divD)+
apply (simp add: range_cover_def word_bits_def)
apply (erule range_cover.range_cover_n_le[where 'a=32, folded word_bits_def])
apply (erule range_cover.range_cover_n_le[where 'a=machine_word_len, folded word_bits_def])
done
@ -3496,9 +3508,9 @@ lemma do_machine_op_obj_at_arch_state[wp]:
by (clarsimp simp: do_machine_op_def split_def | wp)+
lemma (in Untyped_AI_nonempty_table) retype_nonempty_table[wp]:
"\<lbrace>\<lambda>(s::('state_ext::state_ext) state). \<not> (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)\<rbrace>
"\<lbrace>\<lambda>(s::('state_ext::state_ext) state). \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>
retype_region ptr sz us tp dev
\<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)\<rbrace>"
\<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>"
apply (simp add: retype_region_def split del: if_split)
apply (rule hoare_pre)
apply (wp|simp del: fun_upd_apply)+
@ -3528,9 +3540,9 @@ lemma invs_cap_refs_in_kernel_window[elim!]:
by (simp add: invs_def valid_state_def)
lemma (in Untyped_AI_nonempty_table) set_cap_nonempty_tables[wp]:
"\<lbrace>\<lambda>s. P (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) p s)\<rbrace>
"\<lbrace>\<lambda>s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>
set_cap cap cref
\<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) p s)\<rbrace>"
\<lbrace>\<lambda>rv s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\<rbrace>"
apply (rule hoare_pre)
apply (rule hoare_use_eq [where f=arch_state, OF set_cap_arch])
apply (wp set_cap_obj_at_impossible)

2
proof/refine/ADT_H.thy
View File

@ -346,7 +346,7 @@ lemma cap_relation_imp_CapabilityMap:
apply (rule set_eqI, clarsimp)
apply (case_tac "x", simp_all)
apply (rule set_eqI, clarsimp)
apply (case_tac "x", simp_all)
apply (case_tac "x", simp_all add: word_bits_def)
apply (simp add: uint_of_bl_is_bl_to_bin bl_bin_bl[simplified])
apply (simp add: zbits_map_def split: option.splits)
apply (rename_tac arch_cap)

12
proof/refine/Detype_R.thy
View File

@ -846,16 +846,16 @@ lemma valid_cap_ctes_pre:
| _ \<Rightarrow> True"
apply (drule valid_capAligned)
apply (simp split: capability.split zombie_type.split arch_capability.split, safe)
apply (clarsimp simp add: capRange_def capAligned_def objBits_simps pre_helper field_simps
simp del: atLeastAtMost_iff)
using pre_helper[where a=4]
apply (clarsimp simp add: capRange_def capAligned_def objBits_simps field_simps)
apply (clarsimp simp add: capRange_def capAligned_def
simp del: atLeastAtMost_iff capBits.simps)
apply (rule pre_helper2, simp_all)[1]
apply (clarsimp simp add: capRange_def capAligned_def
simp del: atLeastAtMost_iff capBits.simps)
apply (rule pre_helper2, simp_all)[1]
apply (clarsimp simp add: capRange_def capAligned_def objBits_simps pre_helper field_simps
simp del: atLeastAtMost_iff)
using pre_helper[where a=4]
apply (clarsimp simp add: capRange_def capAligned_def objBits_simps field_simps)
done
lemma replycap_argument:
@ -1643,8 +1643,8 @@ proof -
apply (clarsimp simp add: deleteObjects_def2)
apply (simp add: freeMemory_def bind_assoc doMachineOp_bind ef_storeWord)
apply (simp add: bind_assoc[where f="\<lambda>_. modify f" for f, symmetric])
apply (simp add: word_size_def mapM_x_storeWord_step doMachineOp_modify
modify_modify)
apply (simp add: mapM_x_storeWord_step[simplified word_size_bits_def]
doMachineOp_modify modify_modify)
apply (simp add: bind_assoc intvl_range_conv'[where 'a=32, folded word_bits_def] mask_def field_simps)
apply (wp)
apply (simp cong: if_cong)

2
proof/refine/Include.thy
View File

@ -12,7 +12,7 @@ theory Include
imports
"../../spec/abstract/Syscall_A"
"../../spec/design/API_H"
"../../spec/design/$L4V_ARCH/Intermediate_H"
"../../spec/design/$L4V_ARCH/ArchIntermediate_H"
begin
no_notation bind_drop (infixl ">>" 60)

6
proof/refine/Retype_R.thy
View File

@ -836,7 +836,7 @@ lemma new_cap_addrs_subset:
dest!: less_two_pow_divD)
apply (intro conjI)
apply (insert range_cover)
apply (rule word32_plus_mono_right_split[OF range_cover.range_cover_compare])
apply (rule machine_word_plus_mono_right_split[OF range_cover.range_cover_compare])
apply assumption
apply simp
apply (simp add:range_cover_def word_bits_def)
@ -3216,7 +3216,7 @@ lemma obj_range'_subset_strong:
apply (simp add:unat_of_nat_m1 less_imp_le)
using cover
apply (simp add:range_cover_def word_bits_def)
apply (rule word32_plus_mono_right_split[where sz = sz])
apply (rule machine_word_plus_mono_right_split[where sz = sz])
using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::word32))"]
apply (clarsimp simp:unat_of_nat_m1)
using cover
@ -3646,7 +3646,7 @@ proof -
apply unat_arith
using upbound
apply (simp add:word_bits_def)
apply (rule word32_plus_mono_right_split[where sz = sz])
apply (rule machine_word_plus_mono_right_split[where sz = sz])
apply (rule less_le_trans[rotated -1])
apply (rule range_cover.range_cover_compare_bound[OF cover'])
apply (simp add: unat_minus_one[OF not_0'])

2
proof/refine/Syscall_R.thy
View File

@ -202,7 +202,7 @@ lemma decode_invocation_corres:
apply (rule corres_guard_imp)
apply (rule_tac F="length list \<le> 32" in corres_gen_asm)
apply (rule dec_cnode_inv_corres, simp+)
apply (simp add: valid_cap_def)
apply (simp add: valid_cap_def word_bits_def)
apply simp
-- "ThreadCap"
apply (simp add: isCap_defs Let_def CanModify_def

15
proof/refine/Untyped_R.thy
View File

@ -3253,7 +3253,7 @@ lemma createNewCaps_range_helper2:
apply (fastforce simp:range_cover_def)
apply simp
apply (rule range_subsetI)
apply (rule word32_plus_mono_right_split[OF range_cover.range_cover_compare])
apply (rule machine_word_plus_mono_right_split[OF range_cover.range_cover_compare])
apply (assumption)+
apply (simp add:range_cover_def word_bits_def)
apply (frule range_cover_cell_subset)
@ -4477,7 +4477,7 @@ lemma caps_no_overlap'[simp]: "caps_no_overlap'' ptr sz s"
< ptr + of_nat (length slots) * 2 ^ APIType_capBits tp us"
apply (rule minus_one_helper,simp)
apply (rule neq_0_no_wrap)
apply (rule word32_plus_mono_right_split)
apply (rule machine_word_plus_mono_right_split)
apply (simp add: shiftl_t2n range_cover_unat[OF cover] field_simps)
apply (simp add: range_cover.sz(1)
[where 'a=32, folded word_bits_def, OF cover])+
@ -5273,11 +5273,8 @@ let ?ui' = "Invocations_H.untyped_invocation.Retype (cte_map cref) reset
using cover
apply (clarsimp simp:delete_objects_def freeMemory_def word_size_def)
apply (subgoal_tac "is_aligned (ptr &&~~ mask sz) sz")
apply (subst mapM_storeWord_clear_um)
apply (simp)
apply simp
apply (simp add:range_cover_def word_bits_def)
apply clarsimp
apply (subst mapM_storeWord_clear_um[simplified word_size_def word_size_bits_def];
clarsimp simp: range_cover_def word_bits_def)
apply (rule is_aligned_neg_mask)
apply simp
done
@ -5351,7 +5348,7 @@ let ?ui' = "Invocations_H.untyped_invocation.Retype (cte_map cref) reset
< ptr + of_nat (length slots) * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us"
apply (rule minus_one_helper,simp)
apply (rule neq_0_no_wrap)
apply (rule word32_plus_mono_right_split)
apply (rule machine_word_plus_mono_right_split)
apply (simp add:shiftl_t2n range_cover_unat[OF cover] field_simps)
apply (simp add:range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+
done
@ -5366,7 +5363,7 @@ let ?ui' = "Invocations_H.untyped_invocation.Retype (cte_map cref) reset
apply (rule minus_one_helper,simp)
apply (simp add:is_aligned_neg_mask_eq'[symmetric])
apply (rule neq_0_no_wrap)
apply (rule word32_plus_mono_right_split[where sz = sz])
apply (rule machine_word_plus_mono_right_split[where sz = sz])
apply (simp add:is_aligned_mask)+
apply (simp add:range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+
done

2
spec/ROOT
View File

@ -67,7 +67,7 @@ session ExecSpec = Word_Lib +
options [document = false]
theories
"design/API_H"
"design/$L4V_ARCH/Intermediate_H"
"design/$L4V_ARCH/ArchIntermediate_H"
(*

19
spec/abstract/ARM/ArchCSpace_A.thy
View File

@ -18,8 +18,27 @@ theory ArchCSpace_A
imports
ArchVSpace_A
begin
context Arch begin global_naming ARM_A
definition cnode_guard_size_bits :: "nat"
where
cnode_guard_size_bits_def [simp]: "cnode_guard_size_bits \<equiv> 5"
definition cnode_padding_bits :: "nat"
where
cnode_padding_bits_def [simp]: "cnode_padding_bits \<equiv> 3"
text {* On a user request to modify a cnode capability, extract new guard bits and guard. *}
definition
update_cnode_cap_data :: "data \<Rightarrow> nat \<times> data" where
"update_cnode_cap_data w \<equiv>
let
guard_bits = 18;
guard_size' = unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits);
guard'' = (w >> (cnode_padding_bits + cnode_guard_size_bits)) && mask guard_bits
in (guard_size', guard'')"
text {* For some purposes capabilities to physical objects are treated
differently to others. *}
definition

29
spec/abstract/ARM/ArchTcb_A.thy Normal file
View File

@ -0,0 +1,29 @@
(*
* 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)
*)
(*
Arch-specific functions for the abstract model of CSpace.
*)
chapter "Architecture-specific TCB functions"
theory ArchTcb_A
imports "../KHeap_A"
begin
context Arch begin global_naming ARM_A
definition
arch_tcb_set_ipc_buffer :: "machine_word \<Rightarrow> vspace_ref \<Rightarrow> (unit, 'a::state_ext) s_monad"
where
"arch_tcb_set_ipc_buffer target ptr \<equiv> as_user target $ set_register TPIDRURW ptr"
end
end

6
spec/abstract/ARM/Arch_Structs_A.thy
View File

@ -260,7 +260,13 @@ where
| DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz
| ASIDPool f \<Rightarrow> AASIDPool)"
text {* For implementation reasons the badge word has differing amounts of bits *}
definition
badge_bits :: nat where
badge_bits_def [simp]: "badge_bits \<equiv> 28"
end
section "Arch-specific tcb"

14
spec/abstract/CSpace_A.thy
View File

@ -32,11 +32,13 @@ requalify_consts
arch_is_physical
arch_same_region_as
same_aobject_as
msg_max_length
cap_transfer_data_size
msg_max_extra_caps
msg_align_bits
update_cnode_cap_data
cnode_padding_bits
cnode_guard_size_bits
end
@ -96,7 +98,7 @@ where
"max_free_index_update cap \<equiv> cap \<lparr> free_index:= max_free_index (untyped_sz_bits cap) \<rparr>"
definition
set_untyped_cap_as_full :: "cap \<Rightarrow> cap \<Rightarrow> obj_ref \<times> bool list\<Rightarrow> (unit,'z::state_ext) s_monad"
set_untyped_cap_as_full :: "cap \<Rightarrow> cap \<Rightarrow> obj_ref \<times> bool list \<Rightarrow> (unit,'z::state_ext) s_monad"
where
"set_untyped_cap_as_full src_cap new_cap src_slot \<equiv>
if (is_untyped_cap src_cap \<and> is_untyped_cap new_cap
@ -136,11 +138,7 @@ definition
else if is_cnode_cap cap then
let
(oref, bits, guard) = the_cnode_cap cap;
rights_bits = 3;
guard_bits = 18;
guard_size_bits = 5;
guard_size' = unat ((w >> rights_bits) && mask guard_size_bits);
guard'' = (w >> (rights_bits + guard_size_bits)) && mask guard_bits;
(guard_size', guard'') = update_cnode_cap_data w;
guard' = drop (size guard'' - guard_size') (to_bl guard'')
in
if guard_size' + bits > word_bits
@ -856,6 +854,6 @@ definition
section "Cap classification used to define invariants"
datatype capclass =
PhysicalClass | ReplyClass "obj_ref" | IRQClass | ASIDMasterClass | NullClass | DomainClass
PhysicalClass | ReplyClass "obj_ref" | IRQClass | ASIDMasterClass | NullClass | DomainClass | IOPortClass
end

8
spec/abstract/Structures_A.thy
View File

@ -41,6 +41,7 @@ requalify_consts
asid_high_bits
asid_low_bits
arch_is_frame_type
badge_bits
default_arch_tcb
arch_tcb_context_get
arch_tcb_context_set
@ -227,13 +228,6 @@ definition
| ArchObjectCap acap \<Rightarrow> ArchObjectCap (acap_rights_update cr' acap)
| _ \<Rightarrow> cap"
text {* For implementation reasons not all bits of the badge word can be used. *}
definition
badge_bits :: nat where
"badge_bits \<equiv> 28"
declare badge_bits_def [simp]
definition
badge_update :: "badge \<Rightarrow> cap \<Rightarrow> cap" where
"badge_update data cap \<equiv>

9
spec/abstract/Tcb_A.thy
View File

@ -15,13 +15,14 @@ The TCB and thread related specifications.
chapter "Threads and TCBs"
theory Tcb_A
imports TcbAcc_A Schedule_A
imports TcbAcc_A Schedule_A "$L4V_ARCH/ArchTcb_A"
begin
context begin interpretation Arch .
requalify_consts
arch_activate_idle_thread
arch_tcb_set_ipc_buffer
end
@ -177,7 +178,7 @@ where
| Some (ptr, frame) \<Rightarrow> doE
cap_delete (target, tcb_cnode_index 4);
liftE $ thread_set (\<lambda>t. t \<lparr> tcb_ipc_buffer := ptr \<rparr>) target;
liftE $ as_user target $ set_register ARM.TPIDRURW ptr;
liftE $ arch_tcb_set_ipc_buffer target ptr;
liftE $ case frame of None \<Rightarrow> return ()
| Some (new_cap, src_slot) \<Rightarrow>
check_cap_at new_cap src_slot
@ -240,6 +241,10 @@ where
return []
od)"
context Arch begin
declare arch_tcb_set_ipc_buffer_def [simp]
end
definition
set_domain :: "obj_ref \<Rightarrow> domain \<Rightarrow> unit det_ext_monad" where
"set_domain tptr new_dom \<equiv> do

68
spec/design/ARM/ArchIntermediate_H.thy Normal file
View File

@ -0,0 +1,68 @@
(*
* 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)
*)
chapter "Intermediate"
theory ArchIntermediate_H
imports "../Intermediate_H"
begin
context Arch begin
context begin
private abbreviation (input)
"createNewPageCaps regionBase numObjects dev gSize pSize \<equiv>
let Data = (if dev then KOUserDataDevice else KOUserData) in
(do addrs \<leftarrow> createObjects regionBase numObjects Data gSize;
modify (\<lambda>ks. ks \<lparr> gsUserPages := (\<lambda> addr.
if addr `~elem~` map fromPPtr addrs then Just pSize
else gsUserPages ks addr)\<rparr>);
return $ map (\<lambda>n. PageCap dev (PPtr (fromPPtr n)) VMReadWrite pSize Nothing) addrs
od)"
private abbreviation (input)
"createNewTableCaps regionBase numObjects tableBits objectProto cap initialiseMappings \<equiv> (do
tableSize \<leftarrow> return (tableBits - objBits objectProto);
addrs \<leftarrow> createObjects regionBase numObjects (injectKO objectProto) tableSize;
pts \<leftarrow> return (map (PPtr \<circ> fromPPtr) addrs);
initialiseMappings pts;
return $ map (\<lambda>pt. cap pt Nothing) pts
od)"
defs Arch_createNewCaps_def:
"Arch_createNewCaps t regionBase numObjects userSize dev \<equiv>
let pointerCast = PPtr \<circ> fromPPtr
in (case t of
APIObjectType apiObject \<Rightarrow> haskell_fail []
| SmallPageObject \<Rightarrow>
createNewPageCaps regionBase numObjects dev 0 ARMSmallPage
| LargePageObject \<Rightarrow>
createNewPageCaps regionBase numObjects dev 4 ARMLargePage
| SectionObject \<Rightarrow>
createNewPageCaps regionBase numObjects dev 8 ARMSection
| SuperSectionObject \<Rightarrow>
createNewPageCaps regionBase numObjects dev 12 ARMSuperSection
| PageTableObject \<Rightarrow>
createNewTableCaps regionBase numObjects ptBits (makeObject::pte) PageTableCap
(\<lambda>pts. return ())
| PageDirectoryObject \<Rightarrow>
createNewTableCaps regionBase numObjects pdBits (makeObject::pde) PageDirectoryCap
(\<lambda>pds. do objSize \<leftarrow> return (((1::nat) `~shiftL~` pdBits));
mapM_x copyGlobalMappings pds;
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x
(x + (fromIntegral objSize) - 1)
(addrFromPPtr x)) pds
od)
)"
end
end
end

31
spec/design/ArchInterrupt_H.thy
View File

@ -1,31 +0,0 @@
(*
* 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 ArchInterrupt_H
imports RetypeDecls_H
begin
definition
decodeIRQControlInvocation :: "machine_word \<Rightarrow> machine_word list \<Rightarrow> machine_word \<Rightarrow> capability list \<Rightarrow> ( syscall_error , ArchRetypeDecls_H.irqcontrol_invocation ) kernel_f"
where
"decodeIRQControlInvocation arg1 arg2 arg3 arg4 \<equiv> throw IllegalOperation"
definition
invokeIRQControl :: "ArchRetypeDecls_H.irqcontrol_invocation \<Rightarrow> unit kernel_p"
where
"invokeIRQControl arg1 \<equiv> haskell_fail []"
definition
checkIRQ :: "machine_word \<Rightarrow> ( syscall_error , unit ) kernel_f"
where
"checkIRQ irq\<equiv> rangeCheck irq (fromEnum minIRQ) (fromEnum maxIRQ)"
end

84
spec/design/ARM/Intermediate_H.thy → spec/design/Intermediate_H.thy
View File

@ -11,12 +11,14 @@
chapter "Intermediate"
theory Intermediate_H
imports "../API_H"
imports "API_H"
begin
context begin interpretation Arch .
requalify_consts
clearMemory
end
(*
* Intermediate function bodies that were once in the Haskell spec, but are
* now no longer.
@ -44,95 +46,37 @@ createNewCaps :: "object_type \<Rightarrow> machine_word \<Rightarrow> nat \<Rig
consts
Arch_createNewCaps :: "object_type \<Rightarrow> machine_word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> arch_capability list kernel"
thm injectKO_defs
defs insertNewCaps_def:
"insertNewCaps newType srcSlot destSlots regionBase magnitudeBits dev \<equiv> (do
caps \<leftarrow> createNewCaps newType regionBase (length destSlots) magnitudeBits dev ;
caps \<leftarrow> createNewCaps newType regionBase (length destSlots) magnitudeBits dev;
zipWithM_x (insertNewCap srcSlot) destSlots caps
od)"
defs (in Arch) Arch_createNewCaps_def:
"Arch_createNewCaps t regionBase numObjects arg4 dev \<equiv>
let pointerCast = PPtr \<circ> fromPPtr;
Data = (if dev then KOUserDataDevice else KOUserData)
in (case t of
APIObjectType v5 \<Rightarrow>
haskell_fail []
| SmallPageObject \<Rightarrow> (do
addrs \<leftarrow> createObjects regionBase numObjects Data 0;
modify (\<lambda> ks. ks \<lparr> gsUserPages := (\<lambda> addr.
if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage
else gsUserPages ks addr)\<rparr>);
return $ map (\<lambda> n. PageCap dev (pointerCast n) VMReadWrite
ARMSmallPage Nothing) addrs
od)
| LargePageObject \<Rightarrow> (do
addrs \<leftarrow> createObjects regionBase numObjects Data 4;
modify (\<lambda> ks. ks \<lparr> gsUserPages := (\<lambda> addr.
if addr `~elem~` map fromPPtr addrs then Just ARMLargePage
else gsUserPages ks addr)\<rparr>);
return $ map (\<lambda> n. PageCap dev (pointerCast n) VMReadWrite
ARMLargePage Nothing) addrs
od)
| SectionObject \<Rightarrow> (do
addrs \<leftarrow> createObjects regionBase numObjects Data 8;
modify (\<lambda> ks. ks \<lparr> gsUserPages := (\<lambda> addr.
if addr `~elem~` map fromPPtr addrs then Just ARMSection
else gsUserPages ks addr)\<rparr>);
return $ map (\<lambda> n. PageCap dev (pointerCast n) VMReadWrite
ARMSection Nothing) addrs
od)
| SuperSectionObject \<Rightarrow> (do
addrs \<leftarrow> createObjects regionBase numObjects Data 12;
modify (\<lambda> ks. ks \<lparr> gsUserPages := (\<lambda> addr.
if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection
else gsUserPages ks addr)\<rparr>);
return $ map (\<lambda> n. PageCap dev (pointerCast n) VMReadWrite
ARMSuperSection Nothing) addrs
od)
| PageTableObject \<Rightarrow> (do
ptSize \<leftarrow> return ( ptBits - objBits (makeObject ::pte));
addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject ::pte)) ptSize;
objSize \<leftarrow> return (((1::nat) `~shiftL~` ptBits));
pts \<leftarrow> return ( map pointerCast addrs);
return $ map (\<lambda> pt. PageTableCap pt Nothing) pts
od)
| PageDirectoryObject \<Rightarrow> (do
pdSize \<leftarrow> return ( pdBits - objBits (makeObject ::pde));
addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject ::pde)) pdSize;
objSize \<leftarrow> return ( ((1::nat) `~shiftL~` pdBits));
pds \<leftarrow> return ( map pointerCast addrs);
mapM_x copyGlobalMappings pds;
doMachineOp $ mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + (fromIntegral objSize) - 1)
(addrFromPPtr x)) pds;
return $ map (\<lambda> pd. PageDirectoryCap pd Nothing) pds
od)
)"
od)"
defs createNewCaps_def:
"createNewCaps t regionBase numObjects userSize dev \<equiv>
(case toAPIType t of
Some TCBObject \<Rightarrow> (do
Some TCBObject \<Rightarrow> (do
addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject ::tcb)) 0;
curdom \<leftarrow> curDomain;
mapM_x (\<lambda>tptr. threadSet (tcbDomain_update (\<lambda>_. curdom)) tptr) addrs;
return $ map (\<lambda> addr. ThreadCap addr) addrs
od)
| Some EndpointObject \<Rightarrow> (do
| Some EndpointObject \<Rightarrow> (do
addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject ::endpoint)) 0;
return $ map (\<lambda> addr. EndpointCap addr 0 True True True) addrs
od)
| Some NotificationObject \<Rightarrow> (do
od)
| Some NotificationObject \<Rightarrow> (do
addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject ::notification)) 0;
return $ map (\<lambda> addr. NotificationCap addr 0 True True) addrs
od)
| Some ArchTypes_H.CapTableObject \<Rightarrow> (do
od)
| Some ArchTypes_H.CapTableObject \<Rightarrow> (do
addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject ::cte)) userSize;
modify (\<lambda> ks. ks \<lparr> gsCNodes := (\<lambda> addr.
if addr `~elem~` map fromPPtr addrs then Just userSize
else gsCNodes ks addr)\<rparr>);
return $ map (\<lambda> addr. CNodeCap addr userSize 0 0) addrs
od)
od)
| Some ArchTypes_H.Untyped \<Rightarrow>
return $ map
(\<lambda> n. UntypedCap dev (regionBase + n * 2 ^ (fromIntegral userSize)) userSize 0)
@ -140,7 +84,7 @@ defs createNewCaps_def:
| None \<Rightarrow> (do
archCaps \<leftarrow> Arch_createNewCaps t regionBase numObjects userSize dev;
return $ map ArchObjectCap archCaps
od)
od)
)"
defs createObjects_def:

7
spec/design/m-skel/ARM/MachineTypes.thy
View File

@ -29,8 +29,15 @@ section "Types"
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM decls_only
(*<*)
section "Machine Words"
type_synonym machine_word_len = 32
definition
word_size_bits :: "'a :: numeral"
where
"word_size_bits \<equiv> 2"
end
context begin interpretation Arch .

40
spec/haskell/SEL4.cabal
View File

@ -21,13 +21,17 @@ Flag FFI
description: Include the C language bindings
default: True
Flag ArchArm
description: Include ARM modules and platforms (else x64)
default: True
Library
exposed-modules: SEL4
SEL4.Machine.Target
-- Newer mtl's cause old APIs to be deprecated, which fails -Werror.
-- base-4.8 (ghc 7.10) exports conflicting name Prelude.Word.
build-depends: mtl==2.1.3.1, base==4.7.*, array, containers, transformers
if flag(FFI)
-- FFIBindings currently relies on POSIX signal handlers. This could
-- be fixed.
@ -36,6 +40,9 @@ Library
include-dirs: include
install-includes: sel4model.h gic.h
dist/build/Simulation/FFIBindings_stub.h
else
build-depends: unix
include-dirs: include
other-modules: SEL4.API
SEL4.API.Syscall
@ -75,13 +82,15 @@ Library
Data.BinaryTree
Data.Helpers
SEL4.Machine.Hardware.GICInterface
SEL4.Machine.Hardware.MCTInterface
SEL4.Machine.Hardware.MPTimerInterface
if flag(ArchArm)
other-modules:
SEL4.Machine.Hardware.ARM.KZM
SEL4.Machine.Hardware.ARM.Exynos4210
SEL4.Machine.Hardware.ARM.Sabre
SEL4.Machine.Hardware.ARM.Callbacks
SEL4.Machine.Hardware.GICInterface
SEL4.Machine.Hardware.MCTInterface
SEL4.Machine.Hardware.MPTimerInterface
SEL4.API.Types.ARM
SEL4.API.InvocationLabels.ARM
@ -98,7 +107,28 @@ Library
SEL4.Model.StateData.ARM
SEL4.Machine.RegisterSet.ARM
SEL4.Machine.Hardware.ARM
else
-- FIXME: should be a flag also, or some other way to conditionally compile
-- Setup.hs hooks can handle this, but do we want to do that?
other-modules:
SEL4.API.Types.X64
SEL4.API.InvocationLabels.X64
SEL4.API.Invocation.X64
SEL4.Kernel.VSpace.X64
SEL4.Kernel.Thread.X64
SEL4.Object.ObjectType.X64
SEL4.Object.Structures.X64
SEL4.Object.Interrupt.X64
SEL4.Object.Instances.X64
SEL4.Object.IOPort.X64
SEL4.Object.TCB.X64
SEL4.Model.StateData.X64
SEL4.Machine.RegisterSet.X64
SEL4.Machine.Hardware.X64
SEL4.Machine.Hardware.X64.PC99
hs-source-dirs: src
ghc-prof-options: -auto-all -prof -fprof-auto

5
spec/haskell/src/SEL4/API/Invocation.lhs
View File

@ -126,11 +126,14 @@ The following data type defines the parameters expected for invocations of Untyp
The following data type defines the set of possible invocations for interrupt controller capabilities.
%FIXME IssueIRQHandler is not really handled on x64, instead it has two arch-specific ones
> data IRQControlInvocation
> = ArchIRQControl { archIRQControl :: Arch.IRQControlInvocation }
> | IssueIRQHandler {
> issueHandlerIRQ :: IRQ,
> issueHandlerSlot, issueHandlerControllerSlot :: PPtr CTE }
> issueHandlerSlot,
> issueHandlerControllerSlot :: PPtr CTE }
> deriving Show
\subsubsection{IRQ Handler Invocations}

2
spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs
View File

@ -26,7 +26,7 @@ This module contains the architecture-specific thread switch code for the ARM.
\end{impdetails}
The ARM thread switch function invalidates all caches and the TLB, and writes the IPC buffer pointer to the first word of the globals page.
The ARM thread switch function invalidates all caches and the TLB.
> switchToThread :: PPtr TCB -> Kernel ()
> switchToThread tcb = do

2
spec/haskell/src/SEL4/Object/Interrupt.lhs
View File

@ -107,6 +107,8 @@ An IRQ handler capability allows a thread possessing it to set an endpoint which
> toBool :: Word -> Bool
> toBool w = w /= 0
%FIXME x64 naming: this should be called perform, not invoke, same for CNode
> invokeIRQHandler :: IRQHandlerInvocation -> Kernel ()
> invokeIRQHandler (AckIRQ irq) =
> doMachineOp $ maskInterrupt False irq

7
spec/machine/ARM/MachineTypes.thy
View File

@ -59,8 +59,15 @@ sanitiseRegister :: "register \<Rightarrow> machine_word \<Rightarrow> machine_w
(*<*)
section "Machine Words"
type_synonym machine_word_len = 32
definition
word_size_bits :: "'a :: numeral"
where
"word_size_bits \<equiv> 2"
end
context begin interpretation Arch .

12
spec/machine/MachineExports.thy
View File

@ -45,8 +45,20 @@ requalify_consts
resetTimer
maxIRQ
minIRQ
word_size_bits
clearMemory
(* HERE IS THE PLACE FOR GENERIC WORD LEMMAS FOR ALL ARCHITECTURES *)
lemma Suc_unat_mask_div_obfuscated:
"Suc (unat (mask sz div (word_size::machine_word))) = 2 ^ (min sz word_bits - word_size_bits)"
unfolding word_size_bits_def
by (rule Suc_unat_mask_div)
lemma word_size_size_bits_nat:
"2^word_size_bits = (word_size :: nat)"
by (simp add: word_size_bits_def word_size_def)
end
end

13
tools/c-parser/.gitignore vendored
View File

@ -2,3 +2,16 @@
*.minfo
umm_types.txt
globalmakevars.local
/StrictC.grm.desc
/standalone-parser/table.ML
/standalone-parser/ARM/
/standalone-parser/X64/
/tools/mllex/mllex
/tools/mlyacc/mlyacc
/tools/mlyacc/src/yacc.lex.sml
/testfiles/**/ROOT
/testfiles/modifies_speed.c

12
tools/c-parser/IsaMakefile
View File

@ -42,12 +42,12 @@ $(HEAPS): .FORCE
# We dynamically generate a ROOT file containing all the test files, and
# then build it using Isabelle.
#
cparser_test: testfiles/ROOT .FORCE
$(ISABELLE_TOOL) build -d ../.. -d testfiles -b -v CParserTest
testfiles/ROOT: testfiles testfiles/*.c testfiles/*.thy ../../misc/scripts/gen_isabelle_root.py
python ../../misc/scripts/gen_isabelle_root.py -i testfiles -o testfiles/ROOT -s CParserTest -b CParser
all_tests.thy: testfiles testfiles/*.c ../../misc/scripts/gen_isabelle_root.py
python ../../misc/scripts/gen_isabelle_root.py -T -o $@ -b CParser -i testfiles
cparser_test: testfiles/$(L4V_ARCH)/ROOT .FORCE
$(ISABELLE_TOOL) build -d ../.. -d testfiles/$(L4V_ARCH) -b -v CParserTest
testfiles/$(L4V_ARCH)/ROOT: testfiles testfiles/*.c testfiles/*.thy ../../misc/scripts/gen_isabelle_root.py
python ../../misc/scripts/gen_isabelle_root.py -i testfiles -i testfiles/$(L4V_ARCH) -o testfiles/$(L4V_ARCH)/ROOT -s CParserTest -b CParser
all_tests_$(L4V_ARCH).thy: testfiles testfiles/*.c ../../misc/scripts/gen_isabelle_root.py
python ../../misc/scripts/gen_isabelle_root.py -T -o $@ -b CParser -i testfiles -i testfiles/$(L4V_ARCH)
GRAMMAR_PRODUCTS = l4c.lex.sml l4c.grm.sml l4c.grm.sig

26
tools/c-parser/standalone-parser/Makefile
View File

@ -20,16 +20,16 @@ ifndef STP_INCLUDED
STP_INCLUDED=true
ARM_DIR=$(STP_PFX)/ARM
F64_DIR=$(STP_PFX)/FAKE64
ARCH_DIRS=$(ARM_DIR) $(F64_DIR)
X64_DIR=$(STP_PFX)/X64
ARCH_DIRS=$(ARM_DIR) $(X64_DIR)
STPARSER_ARM=$(ARM_DIR)/c-parser
STPARSER_F64=$(F64_DIR)/c-parser
STPARSERS=$(STPARSER_ARM) $(STPARSER_F64)
STPARSER_X64=$(X64_DIR)/c-parser
STPARSERS=$(STPARSER_ARM) $(STPARSER_X64)
TOKENIZER_ARM=$(ARM_DIR)/tokenizer
TOKENIZER_F64=$(F64_DIR)/tokenizer
TOKENIZERS=$(TOKENIZER_ARM) $(TOKENIZER_F64)
TOKENIZER_X64=$(X64_DIR)/tokenizer
TOKENIZERS=$(TOKENIZER_ARM) $(TOKENIZER_X64)
.PHONY: all cparser_tools stp_all standalone-cparser standalone-tokenizer
@ -55,26 +55,26 @@ ifeq ($(SML_COMPILER),mlton)
#
ARM_MLB_PATH := -mlb-path-var 'L4V_ARCH ARM'
F64_MLB_PATH := -mlb-path-var 'L4V_ARCH FAKE64'
X64_MLB_PATH := -mlb-path-var 'L4V_ARCH X64'
PARSER_DEPS_ARM := $(shell mlton $(ARM_MLB_PATH) -stop f $(STP_PFX)/c-parser.mlb)
PARSER_DEPS_F64 := $(shell mlton $(F64_MLB_PATH) -stop f $(STP_PFX)/c-parser.mlb)
PARSER_DEPS_X64 := $(shell mlton $(X64_MLB_PATH) -stop f $(STP_PFX)/c-parser.mlb)
TOKENIZER_DEPS_ARM := $(shell mlton $(ARM_MLB_PATH) -stop f $(STP_PFX)/tokenizer.mlb)
TOKENIZER_DEPS_F64 := $(shell mlton $(F64_MLB_PATH) -stop f $(STP_PFX)/tokenizer.mlb)
TOKENIZER_DEPS_X64 := $(shell mlton $(X64_MLB_PATH) -stop f $(STP_PFX)/tokenizer.mlb)
$(STPARSER_ARM): $(PARSER_DEPS_ARM) | $(ARM_DIR)
mlton $(ARM_MLB_PATH) -output $@ $<
$(STPARSER_F64): $(PARSER_DEPS_F64) | $(F64_DIR)
mlton $(F64_MLB_PATH) -output $@ $<
$(STPARSER_X64): $(PARSER_DEPS_X64) | $(X64_DIR)
mlton $(X64_MLB_PATH) -output $@ $<
$(TOKENIZER_ARM): $(TOKENIZER_DEPS_ARM) | $(ARM_DIR)
mlton $(ARM_MLB_PATH) -output $@ $<
$(TOKENIZER_F64): $(TOKENIZER_DEPS_F64) | $(F64_DIR)
mlton $(F64_MLB_PATH) -output $@ $<
$(TOKENIZER_X64): $(TOKENIZER_DEPS_X64) | $(X64_DIR)
mlton $(X64_MLB_PATH) -output $@ $<
else ifeq ($(SML_COMPILER),poly)

0
tools/c-parser/testfiles/asm_stmt.c → tools/c-parser/testfiles/ARM/asm_stmt.c
View File

2
tools/c-parser/testfiles/asm_stmt.thy → tools/c-parser/testfiles/ARM/asm_stmt.thy
View File

@ -10,7 +10,7 @@
theory asm_stmt
imports "../CTranslation"
imports "../../CTranslation"
begin

24
tools/c-parser/testfiles/ARM/imports/MachineWords.thy Normal file
View File

@ -0,0 +1,24 @@
(*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*)
theory MachineWords
imports "../../../CTranslation"
begin
type_synonym machine_word_len = "32"
type_synonym machine_word = "machine_word_len word"
abbreviation "machine_word_bytes \<equiv> 4 :: nat"
lemma of_nat_machine_word_bytes[simp]: "of_nat machine_word_bytes = 4"
by simp
end

24
tools/c-parser/testfiles/X64/imports/MachineWords.thy Normal file
View File

@ -0,0 +1,24 @@
(*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
* See "LICENSE_BSD2.txt" for details.
*
* @TAG(NICTA_BSD)
*)
theory MachineWords
imports "../../../CTranslation"
begin
type_synonym machine_word_len = "64"
type_synonym machine_word = "machine_word_len word"
abbreviation "machine_word_bytes \<equiv> 8 :: nat"
lemma of_nat_machine_word_bytes[simp]: "of_nat machine_word_bytes = 8"
by simp
end

22
tools/c-parser/testfiles/factorial.c
View File

@ -11,24 +11,24 @@
/** FNSPEC alloc_spec:
"\<forall>\<sigma> k. \<Gamma> \<turnstile>
\<lbrace>\<sigma>. (free_pool k)\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__ptr_to_unsigned :== PROC alloc()
\<acute>ret__ptr_to_unsigned_long :== PROC alloc()
\<lbrace> ((\<lambda>p s. if k > 0 then (\<turnstile>\<^sub>s p \<and>\<^sup>* \<turnstile>\<^sub>s (p +\<^sub>p 1) \<and>\<^sup>*
free_pool (k - 1)) s else (free_pool k) s \<and> p = NULL) \<acute>ret__ptr_to_unsigned)\<^bsup>sep\<^esup> \<rbrace>"
free_pool (k - 1)) s else (free_pool k) s \<and> p = NULL) \<acute>ret__ptr_to_unsigned_long)\<^bsup>sep\<^esup> \<rbrace>"
*/
unsigned int *alloc(void)
unsigned long *alloc(void)
{
/* Stub */
}
/** FNSPEC free_spec:
"\<forall>\<sigma> k. \<Gamma> \<turnstile>
\<lbrace>\<sigma>. (sep_cut' (ptr_val \<acute>p) (2 * size_of TYPE(word32)) \<and>\<^sup>* free_pool k)\<^bsup>sep\<^esup> \<rbrace>
\<lbrace>\<sigma>. (sep_cut' (ptr_val \<acute>p) (2 * size_of TYPE(machine_word)) \<and>\<^sup>* free_pool k)\<^bsup>sep\<^esup> \<rbrace>
PROC free(\<acute>p)
\<lbrace> (free_pool (k + 1))\<^bsup>sep\<^esup> \<rbrace>"
*/
void free(unsigned int *p)
void free(unsigned long *p)
{
/* Stub */
}
@ -36,14 +36,14 @@ void free(unsigned int *p)
/** FNSPEC factorial_spec:
"\<forall>\<sigma> k. \<Gamma> \<turnstile>
\<lbrace>\<sigma>. (free_pool k)\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__ptr_to_unsigned :== PROC factorial(\<acute>n)
\<lbrace> if \<acute>ret__ptr_to_unsigned \<noteq> NULL then (sep_fac_list \<^bsup>\<sigma>\<^esup>n \<acute>ret__ptr_to_unsigned \<and>\<^sup>*
\<acute>ret__ptr_to_unsigned_long :== PROC factorial(\<acute>n)
\<lbrace> if \<acute>ret__ptr_to_unsigned_long \<noteq> NULL then (sep_fac_list \<^bsup>\<sigma>\<^esup>n \<acute>ret__ptr_to_unsigned_long \<and>\<^sup>*
free_pool (k - (unat \<^bsup>\<sigma>\<^esup>n + 1)))\<^bsup>sep\<^esup> \<and> (unat \<^bsup>\<sigma>\<^esup>n + 1) \<le> k else (free_pool k)\<^bsup>sep\<^esup> \<rbrace>"
*/
unsigned int *factorial(unsigned int n)
unsigned long *factorial(unsigned long n)
{
unsigned int *p, *q;
unsigned long *p, *q;
if (n == 0) {
p = alloc();
@ -69,7 +69,7 @@ unsigned int *factorial(unsigned int n)
/** INV: "\<lbrace> \<exists>xs. (sep_list xs \<acute>q \<and>\<^sup>* free_pool (k - length xs))\<^bsup>sep\<^esup> \<and>
length xs \<le> k \<rbrace>" */
{
unsigned int *k = (unsigned int *)*(q + 1);
unsigned long *k = (unsigned long *)*(q + 1);
free(q);
q = k;
@ -79,7 +79,7 @@ unsigned int *factorial(unsigned int n)
}
*p = n * *q;
*(p + 1) = (unsigned int)q;
*(p + 1) = (unsigned long)q;
return p;
}

68
tools/c-parser/testfiles/factorial.thy
View File

@ -1,5 +1,5 @@
(*
* Copyright 2014, NICTA
* Copyright 201machine_word_bytes, NICTA
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
@ -9,7 +9,7 @@
*)
theory factorial
imports "../CTranslation"
imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
begin
declare hrs_simps [simp add]
@ -18,7 +18,7 @@ declare sep_conj_ac [simp add]
consts free_pool :: "nat \<Rightarrow> heap_assert"
primrec
fac :: "nat \<Rightarrow> word32"
fac :: "nat \<Rightarrow> machine_word"
where
"fac 0 = 1"
| "fac (Suc n) = of_nat (Suc n) * fac n"
@ -40,7 +40,7 @@ lemma fac_unfold:
done
primrec
fac_list :: "nat \<Rightarrow> word32 list"
fac_list :: "nat \<Rightarrow> machine_word list"
where
"fac_list 0 = [1]"
| "fac_list (Suc n) = fac (Suc n) # fac_list n"
@ -58,7 +58,7 @@ lemma fac_list_unfold:
done
primrec
sep_list :: "word32 list \<Rightarrow> word32 ptr \<Rightarrow> heap_assert"
sep_list :: "machine_word list \<Rightarrow> machine_word ptr \<Rightarrow> heap_assert"
where
"sep_list [] p = (\<lambda>s. p=NULL \<and> \<box> s)"
| "sep_list (x#xs) p = (\<lambda>s. \<exists>j. ((p \<mapsto> x) \<and>\<^sup>* (p +\<^sub>p 1) \<mapsto> j \<and>\<^sup>*
@ -69,7 +69,7 @@ lemma sep_list_NULL [simp]:
by (case_tac xs) auto
definition
sep_fac_list :: "word32 \<Rightarrow> word32 ptr \<Rightarrow> heap_assert"
sep_fac_list :: "machine_word \<Rightarrow> machine_word ptr \<Rightarrow> heap_assert"
where
"sep_fac_list n p \<equiv> sep_list (fac_list (unat n)) p"
@ -103,7 +103,7 @@ install_C_file memsafe "factorial.c"
thm factorial_global_addresses.factorial_body_def
lemma (in factorial_global_addresses) mem_safe_alloc:
"mem_safe (\<acute>ret__ptr_to_unsigned :== PROC alloc()) \<Gamma>"
"mem_safe (\<acute>ret__ptr_to_unsigned_long :== PROC alloc()) \<Gamma>"
apply(insert alloc_impl)
apply(unfold alloc_body_def)
apply(subst mem_safe_restrict)
@ -113,10 +113,10 @@ lemma (in factorial_global_addresses) mem_safe_alloc:
done
lemma (in factorial_global_addresses) sep_frame_alloc:
"\<lbrakk> \<forall>\<sigma>. \<Gamma> \<turnstile> \<lbrace>\<sigma>. (P (f \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace> \<acute>ret__ptr_to_unsigned :== PROC alloc() \<lbrace> (Q (g \<sigma> \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>;
"\<lbrakk> \<forall>\<sigma>. \<Gamma> \<turnstile> \<lbrace>\<sigma>. (P (f \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace> \<acute>ret__ptr_to_unsigned_long :== PROC alloc() \<lbrace> (Q (g \<sigma> \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>;
htd_ind f; htd_ind g; \<forall>s. htd_ind (g s) \<rbrakk> \<Longrightarrow>
\<forall>\<sigma>. \<Gamma> \<turnstile> \<lbrace>\<sigma>. (P (f \<acute>(\<lambda>x. x)) \<and>\<^sup>* R (h \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__ptr_to_unsigned :== PROC alloc()
\<acute>ret__ptr_to_unsigned_long :== PROC alloc()
\<lbrace> (Q (g \<sigma> \<acute>(\<lambda>x. x)) \<and>\<^sup>* R (h \<sigma>))\<^bsup>sep\<^esup> \<rbrace>"
unfolding sep_app_def
by (rule sep_frame, auto intro!: mem_safe_alloc)
@ -124,9 +124,9 @@ lemma (in factorial_global_addresses) sep_frame_alloc:
lemma (in alloc_spec) alloc_spec':
shows "\<forall>\<sigma> k R f. factorial_global_addresses.\<Gamma> \<turnstile>
\<lbrace>\<sigma>. ((\<lambda>x. free_pool k) ((\<lambda>x. undefined) \<acute>(\<lambda>x. x)) \<and>\<^sup>* R (f \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__ptr_to_unsigned :== PROC alloc()
\<acute>ret__ptr_to_unsigned_long :== PROC alloc()
\<lbrace> ((\<lambda>p s. if k > 0 then (\<turnstile>\<^sub>s p \<and>\<^sup>* \<turnstile>\<^sub>s (p +\<^sub>p 1) \<and>\<^sup>*
free_pool (k - 1)) s else (free_pool k) s \<and> p = NULL) \<acute>ret__ptr_to_unsigned
free_pool (k - 1)) s else (free_pool k) s \<and> p = NULL) \<acute>ret__ptr_to_unsigned_long
\<and>\<^sup>* R (f \<sigma>))\<^bsup>sep\<^esup> \<rbrace>"
apply clarify
apply(insert alloc_spec)
@ -159,7 +159,7 @@ lemma (in factorial_global_addresses) sep_frame_free:
lemma (in free_spec) free_spec':
shows "\<forall>\<sigma> k R f. factorial_global_addresses.\<Gamma> \<turnstile>
\<lbrace>\<sigma>. ((\<lambda>p. sep_cut' (ptr_val p) (2 * size_of TYPE(word32)) \<and>\<^sup>* free_pool k) \<acute>p \<and>\<^sup>* R (f \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>
\<lbrace>\<sigma>. ((\<lambda>p. sep_cut' (ptr_val p) (2 * size_of TYPE(machine_word)) \<and>\<^sup>* free_pool k) \<acute>p \<and>\<^sup>* R (f \<acute>(\<lambda>x. x)))\<^bsup>sep\<^esup> \<rbrace>
PROC free(\<acute>p)
\<lbrace> ((\<lambda>x. free_pool (k + 1)) ((\<lambda>x. ()) \<acute>(\<lambda>x. x)) \<and>\<^sup>* R (f \<sigma>))\<^bsup>sep\<^esup> \<rbrace>"
apply clarify
@ -171,28 +171,28 @@ lemma (in free_spec) free_spec':
done
lemma double_word_sep_cut':
"(p \<mapsto> x \<and>\<^sup>* (p +\<^sub>p 1) \<mapsto> y) s \<Longrightarrow> sep_cut' (ptr_val (p::word32 ptr)) 8 s"
"(p \<mapsto> x \<and>\<^sup>* (p +\<^sub>p 1) \<mapsto> y) s \<Longrightarrow> sep_cut' (ptr_val (p::machine_word ptr)) (2*machine_word_bytes) s"
apply(clarsimp simp: sep_conj_def sep_cut'_def dest!: sep_map_dom)
apply(subgoal_tac "{ptr_val p..+4} \<subseteq> {ptr_val p..+8}")
apply(subgoal_tac "{ptr_val p+4..+4} \<subseteq> {ptr_val p..+8}")
apply(subgoal_tac "{ptr_val p..+machine_word_bytes} \<subseteq> {ptr_val p..+(2*machine_word_bytes)}")
apply(subgoal_tac "{ptr_val p+(of_nat machine_word_bytes)..+machine_word_bytes} \<subseteq> {ptr_val p..+(2*machine_word_bytes)}")
apply rule
apply fast
apply (fastforce simp: ptr_add_def)
apply clarsimp
apply(drule intvlD)
apply clarsimp
apply(case_tac "k < 4")
apply(case_tac "k < machine_word_bytes")
apply(erule intvlI)
apply(erule notE)
apply(clarsimp simp: intvl_def)
apply(rule_tac x="k - 4" in exI)
apply(rule_tac x="k - machine_word_bytes" in exI)
apply rule
apply(simp only: unat_simps)
apply(subst mod_less)
apply(simp add: addr_card)
apply simp
apply (simp add: ptr_add_def addr_card)
apply simp
apply(clarsimp simp: intvl_def)
apply(rule_tac x="4+k" in exI)
apply(rule_tac x="machine_word_bytes+k" in exI)
apply simp
apply(rule intvl_start_le)
apply simp
@ -209,11 +209,9 @@ lemma (in specs) factorial_spec:
prefer 2
apply (simp add: whileAnno_def factorial_invs_body_def)
apply(subst factorial_invs_body_def)
apply (simp only: ucast_id)
apply(unfold sep_app_def)
apply (vcg exspec=alloc_spec' exspec=free_spec')
apply (fold lift_def)
apply(clarsimp simp: sep_app_def)
apply (rule conjI)
apply clarsimp
@ -224,12 +222,12 @@ lemma (in specs) factorial_spec:
apply (rule conjI)
apply clarsimp
apply clarsimp
apply (rename_tac a b ret__ptr_to_unsigned)
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned \<and>\<^sup>* sep_true) (lift_state (a,b))")
apply (rename_tac a b ret__ptr_to_unsigned_long)
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned_long \<and>\<^sup>* sep_true) (lift_state (a,b))")
prefer 2
apply(drule sep_conj_sep_true_right)
apply simp
apply(subgoal_tac "(\<turnstile>\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \<and>\<^sup>* sep_true) (lift_state (a,b))")
apply(subgoal_tac "(\<turnstile>\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \<and>\<^sup>* sep_true) (lift_state (a,b))")
prefer 2
apply(drule sep_conj_sep_true_left)
apply simp
@ -258,18 +256,18 @@ lemma (in specs) factorial_spec:
apply(rule_tac x="fac_list (unat (n - 1))" in exI)
apply clarsimp
apply clarsimp
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned \<and>\<^sup>* sep_true) (lift_state (ab,bb))")
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned_long \<and>\<^sup>* sep_true) (lift_state (ab,bb))")
prefer 2
apply(erule (1) sep_conj_impl)
apply simp
apply(subgoal_tac "(\<turnstile>\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \<and>\<^sup>* sep_true) (lift_state (ab,bb))")
apply(subgoal_tac "(\<turnstile>\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \<and>\<^sup>* sep_true) (lift_state (ab,bb))")
prefer 2
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned \<and>\<^sup>*
\<turnstile>\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \<and>\<^sup>*
sep_fac_list (n - 1) ret__ptr_to_unsigneda \<and>\<^sup>*
apply(subgoal_tac "(\<turnstile>\<^sub>s ret__ptr_to_unsigned_long \<and>\<^sup>*
\<turnstile>\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \<and>\<^sup>*
sep_fac_list (n - 1) ret__ptr_to_unsigned_longa \<and>\<^sup>*
free_pool (k - Suc (unat n))) =
(\<turnstile>\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \<and>\<^sup>* (\<turnstile>\<^sub>s ret__ptr_to_unsigned \<and>\<^sup>*
sep_fac_list (n - 1) ret__ptr_to_unsigneda \<and>\<^sup>*
(\<turnstile>\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \<and>\<^sup>* (\<turnstile>\<^sub>s ret__ptr_to_unsigned_long \<and>\<^sup>*
sep_fac_list (n - 1) ret__ptr_to_unsigned_longa \<and>\<^sup>*
free_pool (k - Suc (unat n))))")
prefer 2
apply simp
@ -282,7 +280,7 @@ lemma (in specs) factorial_spec:
apply clarsimp
apply (rule conjI, unat_arith)
apply sep_exists_tac
apply(rule_tac x="ptr_val ret__ptr_to_unsigneda" in exI)
apply(rule_tac x="ptr_val ret__ptr_to_unsigned_longa" in exI)
apply clarsimp
apply(subst fac_unfold)
apply unat_arith
@ -317,7 +315,7 @@ lemma (in specs) factorial_spec:
apply(subst (asm) sep_conj_assoc [symmetric])+
apply(erule sep_conj_impl)
apply simp
apply(erule double_word_sep_cut')
apply(erule double_word_sep_cut'[simplified])
apply assumption
apply simp
apply clarsimp
@ -330,7 +328,7 @@ lemma (in specs) factorial_spec:
declare hrs_simps [simp del]
lemma (in factorial_global_addresses) mem_safe_factorial:
shows "mem_safe (\<acute>ret__ptr_to_unsigned :== PROC factorial(\<acute>n)) \<Gamma>"
shows "mem_safe (\<acute>ret__ptr_to_unsigned_long :== PROC factorial(\<acute>n)) \<Gamma>"
apply(subst mem_safe_restrict)
apply(rule intra_mem_safe)
apply (insert factorial_impl free_impl alloc_impl)

4
tools/c-parser/testfiles/kmalloc.thy
View File

@ -9,14 +9,14 @@
*)
theory kmalloc
imports "../CTranslation"
imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
begin
(* no proof here, just testing the parser *)
consts
KMC :: word32
ptr_retyps :: "nat \<Rightarrow> word32 \<Rightarrow> heap_typ_desc \<Rightarrow> heap_typ_desc"
ptr_retyps :: "nat \<Rightarrow> machine_word \<Rightarrow> heap_typ_desc \<Rightarrow> heap_typ_desc"
install_C_file "kmalloc.c"

8
tools/c-parser/testfiles/list_reverse.c
View File

@ -8,16 +8,16 @@
* @TAG(NICTA_BSD)
*/
typedef unsigned int word_t;
typedef unsigned long word_t;
/** FNSPEC reverse_spec:
"\<Gamma> \<turnstile>
\<lbrace> (list zs \<acute>i)\<^bsup>sep\<^esup> \<rbrace>
\<acute>ret__int :== PROC reverse(\<acute>i)
\<lbrace> (list (rev zs) (Ptr (scast \<acute>ret__int)))\<^bsup>sep\<^esup> \<rbrace>"
\<acute>ret__long :== PROC reverse(\<acute>i)
\<lbrace> (list (rev zs) (Ptr (scast \<acute>ret__long)))\<^bsup>sep\<^esup> \<rbrace>"
*/
int reverse(word_t *i)
long reverse(word_t *i)
{
word_t j = 0;

4
tools/c-parser/testfiles/list_reverse.thy
View File

@ -9,7 +9,7 @@
*)
theory list_reverse
imports "../CTranslation"
imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
begin
declare hrs_simps [simp add]
@ -17,7 +17,7 @@ declare exists_left [simp add]
declare sep_conj_ac [simp add]
primrec
list :: "word32 list \<Rightarrow> word32 ptr \<Rightarrow> heap_state \<Rightarrow> bool"
list :: "machine_word list \<Rightarrow> machine_word ptr \<Rightarrow> heap_state \<Rightarrow> bool"
where
"list [] i = (\<lambda>s. i=NULL \<and> \<box> s)"
| "list (x#xs) i = (\<lambda>s. i=Ptr x \<and> x\<noteq>0 \<and> (\<exists>j. ((i \<mapsto> j) \<and>\<^sup>* list xs (Ptr j)) s))"

6
tools/c-parser/testfiles/list_reverse_norm.c
View File

@ -8,13 +8,13 @@
* @TAG(NICTA_BSD)
*/
typedef unsigned int word_t;
typedef unsigned long word_t;
/** FNSPEC reverse_spec:
"\<Gamma> \<turnstile>
\<lbrace> list (lift_t_c \<zeta>) zs \<acute>i \<rbrace>
\<acute>ret__unsigned :== PROC reverse(\<acute>i)
\<lbrace> list (lift_t_c \<zeta>) (rev zs) (Ptr \<acute>ret__unsigned) \<rbrace>"
\<acute>ret__unsigned_long :== PROC reverse(\<acute>i)
\<lbrace> list (lift_t_c \<zeta>) (rev zs) (Ptr \<acute>ret__unsigned_long) \<rbrace>"
*/

6
tools/c-parser/testfiles/list_reverse_norm.thy
View File

@ -9,14 +9,14 @@
*)
theory list_reverse_norm
imports "../CTranslation"
imports "../CTranslation" "$L4V_ARCH/imports/MachineWords"
begin
declare sep_conj_ac [simp add]
declare hrs_simps [simp add]
primrec
list :: "word32 typ_heap \<Rightarrow> word32 list \<Rightarrow> word32 ptr \<Rightarrow> bool"
list :: "machine_word typ_heap \<Rightarrow> machine_word list \<Rightarrow> machine_word ptr \<Rightarrow> bool"
where
"list h [] i = (i = Ptr 0)"
@ -63,7 +63,7 @@ lemma in_list_Some:
lemma in_list_valid [simp]:
"\<lbrakk> list (lift_t_c (h,d)) xs p; ptr_val q \<in> set xs \<rbrakk>
\<Longrightarrow> d \<Turnstile>\<^sub>t (q::word32 ptr)"
\<Longrightarrow> d \<Turnstile>\<^sub>t (q::machine_word ptr)"
by (auto dest: in_list_Some simp: lift_t_if split: if_split_asm)
lemma list_restrict:

0
tools/c-parser/umm_heap/FAKE64/Addr_Type.thy → tools/c-parser/umm_heap/X64/Addr_Type.thy
View File

4
tools/c-parser/umm_heap/FAKE64/TargetNumbers.ML → tools/c-parser/umm_heap/X64/TargetNumbers.ML
View File

@ -26,10 +26,10 @@ val boolWidth = fromInt 8
val charWidth = 8
val shortWidth = 16
val intWidth = 32
val longWidth = 32
val longWidth = 64
val llongWidth = 64
val ptrWidth : int = 64
val ptr_t = BaseCTypes.LongLong
val ptr_t = BaseCTypes.Long
val CHAR_BIT : int = 8
fun umax width = exp(2, width) - 1

0
tools/c-parser/umm_heap/FAKE64/Word_Mem_Encoding.thy → tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy
View File

57
tools/haskell-translator/caseconvs
View File

@ -896,6 +896,11 @@ case \x of (cap@PageCap { capVPIsDevice = isDevice }) -> (cap@PageTableCap { cap
in ->5
else undefined
case \x of ArchObjectCap (frame@PageCap {capVPIsDevice = False}) -> _ -> ---> let cap = \x in
if isPageCap cap \<and> \<not> capVPIsDevice cap
then ->1
else ->2
case \x of (srcIndex:srcDepth:args, srcRootCap:_) | label < 4 -> (_, _) | label == 4 -> (_, _) | label == 5 -> (_, _) | label == 6 -> (_, _) | label == 7 -> (pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, pivotRootCap:srcRootCap:_) | label == 8 -> (_, _) | label > 8 -> _ -> ---> let (\v0\, \v1\) = \x in
case (if label < 4 then 1
else if label = 4 then 2
@ -1468,7 +1473,7 @@ case \x of (cap@PageCap {}) -> _ -> ---> let cap = \x in
then ->1
else ->2
case \x of (ArchInvocationLabel X64PDPTMap, vaddr':attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PageDirectoryMap, _, _) -> (ArchInvocationLabel X64PageDirectoryUnmap, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in
case \x of (ArchInvocationLabel X64PDPTMap, vaddr':attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PDPTMap, _, _) -> (ArchInvocationLabel X64PDPTUnmap, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in
case (label, args, extraCaps) of
(ArchInvocationLabel X64PDPTMap, vaddr'#attr#_, (vspaceCap,_)#_) => ->1
| (ArchInvocationLabel X64PageDirectoryMap, _, _) => ->2
@ -1568,6 +1573,20 @@ case \x of (ArchInvocationLabel X64PageMap, vaddr:rightsMask:attr:_, (vspaceCap,
| (ArchInvocationLabel X64PageGetAddress, _, _) => ->7
| _ => ->8
case \x of (ArchInvocationLabel X64IOPageTableMap, ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64IOPageTableMap, _, _) -> (ArchInvocationLabel X64IOPageTableUnmap, _, _) -> _ -> ---> let (ilabel, args, extraCaps) = \x in
case (ilabel, args, extraCaps) of
(ArchInvocationLabel X64IOPageTableMap, ioaddr#_, (iospaceCap,_)#_) => ->1
| (ArchInvocationLabel X64IOPageTableMap, _, _) => ->2
| (ArchInvocationLabel X64IOPageTableUnmap, _, _) => ->3
| _ => ->4
case \x of (ArchInvocationLabel X64PageMapIO, rw:ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64PageMapIO, _, _) -> (ArchInvocationLabel X64PageUnmap, _, _) -> _ -> ---> let (ilabel, args, extraCaps) = \x in
case (ilabel, args, extraCaps) of
(ArchInvocationLabel X64PageMapIO, rw:ioaddr#_, (iospaceCap,_)#_) => ->1
| (ArchInvocationLabel X64PageMapIO, _, _) => ->2
| (ArchInvocationLabel X64PageUnmap, _, _) => ->3
| _ => ->4
case \x of cap@(PDPointerTableCap {}) -> _ -> ---> let cap = \x in
if isPDPointerTableCap cap
then ->1
@ -1607,13 +1626,41 @@ case \x of cap@(PageCap {}) -> cap@(PDPointerTableCap {}) -> cap@(PageDirectoryC
then ->8
else ->9
case \x of (ArchInvocationLabel X64PDPTMap, vaddr':attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PDPTMap, _, _) -> (ArchInvocationLabel X64PDPTUnmap, _, _) -> _ -> ---X>
case \x of ArchObjectCap (frame@PageCap {capVPIsDevice = False}) -> _ -> ---X>
case \x of cap@(IOPageTableCap {}) -> _ -> ---> let cap = \x in
if isIOPageTableCap
then ->1
else ->2
case \x of (cap@UntypedCap {}) -> _ -> ---> let cap = \x in
if isUntypedCap cap
then ->1
else ->2
case \x of cap@(PageCap {}) -> _ -> ---> let cap = \x in
if isPageCap cap
then ->1
else ->2
case \x of (PageMap asid cap ctSlot entries) -> (PageRemap entries) -> (PageUnmap cap ctSlot) -> (PageIOMap cap cptr vtdpte slot) -> (PageIOUnmap (ArchObjectCap cap@PageCap {}) ctSlot) -> (PageIOUnmap _ _) -> (PageGetAddr ptr) -> ---> let \v0\ = \x in
case \v0\ of
PageMap asid cap ct ctSlot entries => ->1
| PageRemap entries => ->2
| PageUnmap cap ctSlot => ->3
| PageIOMap cap cptr ctdpte slot => ->4
| PageIOUnmap (ArchObjectCap cap) ctSlot =>
if isPageCap cap
then ->5
else ->6
| PageIOUnmap _ _ => ->6
| PageGetAddr ptr => ->7
case \x of UntypedCap {} | capBlockSize untyped == objBits pool -> _ -> ---> let \v0\ = \x in
if isUntypedCap \v0\ \<and> capBlockSize \v0\ == objBits pool
then ->1
else ->2
case \x of (cap@IOPageTableCap {}) -> _ -> ---> let cap = \x in
if isIOPageTableCap cap
then ->1
else ->2

2
tools/haskell-translator/make_spec.sh
View File

@ -74,7 +74,7 @@ then
(cd $L4CAP && git status --short) >> $SPEC/version
fi
ARCHES=("ARM")
ARCHES=("ARM" "X64")
NAMES=`cd $SKEL; ls *.thy`

1
tools/tests.xml
View File

@ -23,6 +23,7 @@
<sequence cwd="c-parser">
<test name="CParser">../../isabelle/bin/isabelle env make -f IsaMakefile CParser</test>
<test name="CParserTest" cpu-timeout="7200">../../isabelle/bin/isabelle env make -f IsaMakefile cparser_test</test>
<test name="CParserTestX64" cpu-timeout="7200">L4V_ARCH=X64 ../../isabelle/bin/isabelle env make -f IsaMakefile cparser_test</test>
<test name="CParserTools">../../isabelle/bin/isabelle env make -f IsaMakefile cparser_tools</test>
</sequence>