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

Isabelle2018 arm: CRefine

This commit is contained in:
Gerwin Klein 2018-06-27 14:43:34 +02:00
parent 0a3c274054
commit a1d1b69776
11 changed files with 19 additions and 33 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/crefine/ARM/ADT_C.thy
View File

@ -355,7 +355,7 @@ definition
lemma unat_ucast_mask_pageBits_shift:
"unat (ucast (p && mask pageBits >> 2) :: 10 word) = unat ((p::word32) && mask pageBits >> 2)"
apply (simp only: unat_ucast)
apply (rule Divides.mod_less)
apply (rule Divides.mod_less, simp)
apply (rule unat_less_power)
apply (simp add: word_bits_def)
apply (rule shiftr_less_t2n)

18
proof/crefine/ARM/Arch_C.thy
View File

@ -221,7 +221,7 @@ proof -
apply (clarsimp simp: asid_low_bits_def word_le_nat_alt)
done
def ko \<equiv> "KOArch (KOASIDPool makeObject)"
define ko where "ko \<equiv> KOArch (KOASIDPool makeObject)"
have rc :"range_cover frame (objBitsKO ko) (objBitsKO ko) (Suc 0)"
by (simp add:objBits_simps ko_def archObjSize_def al range_cover_full)
@ -1805,22 +1805,6 @@ lemma createMappingEntries_valid_pde_slots'2:
apply (simp add: pdBits_def)
done
(* FIXME : move *)
lemma of_nat_ucast:
"is_down (ucast :: ('a :: len) word \<Rightarrow> ('b :: len) word)
\<Longrightarrow> (of_nat n :: 'b word) = ucast (of_nat n :: 'a word)"
apply (subst word_unat.inverse_norm)
apply (simp add: ucast_def word_of_int[symmetric]
of_nat_nat[symmetric] unat_def[symmetric])
apply (simp add: unat_of_nat)
apply (rule nat_int.Rep_eqD)
apply (simp only: zmod_int)
apply (rule mod_mod_cancel)
apply (subst zdvd_int[symmetric])
apply (rule le_imp_power_dvd)
apply (simp add: is_down_def target_size_def source_size_def word_size)
done
lemma mapM_x_storePDE_pde_mappings':
"\<lbrakk>valid_pde_slots'2 (Inr (a, b)) s; b \<noteq> []\<rbrakk> \<Longrightarrow> \<lbrace>valid_pde_mappings'\<rbrace>
mapM_x (\<lambda>b. storePDE b a) b \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>"

2
proof/crefine/ARM/Fastpath_C.thy
View File

@ -4108,7 +4108,7 @@ lemma in_getCTE_slot:
apply (drule(1) tcb_cte_cases_aligned[where cte=rv])
apply (simp add: objBits_simps' cte_level_bits_def)
apply (simp add: cte_wp_at_ctes_of)
apply (rule_tac x="undefined \<lparr> ksPSpace := empty (slot \<mapsto> KOCTE rv) \<rparr>" in exI)
apply (rule_tac x="undefined \<lparr> ksPSpace := Map.empty (slot \<mapsto> KOCTE rv) \<rparr>" in exI)
apply (simp add: map_to_ctes_def Let_def objBits_simps' cte_level_bits_def)
done

2
proof/crefine/ARM/Finalise_C.thy
View File

@ -1151,7 +1151,7 @@ lemma deleteASID_ccorres:
apply (simp add: asid_high_bits_of_def
asidLowBits_def Kernel_C.asidLowBits_def
asid_low_bits_def unat_ucast)
apply (rule sym, rule Divides.mod_less)
apply (rule sym, rule Divides.mod_less, simp)
apply (rule unat_less_power[where sz=7, simplified])
apply (simp add: word_bits_conv)
apply (rule shiftr_less_t2n[where m=7, simplified])

2
proof/crefine/ARM/Interrupt_C.thy
View File

@ -323,7 +323,7 @@ lemma invokeIRQControl_ccorres:
lemma unat_ucast_16_32:
"unat (ucast (x::(16 word))::32 signed word) = unat x"
apply (subst unat_ucast)
apply (rule Divides.mod_less)
apply (rule Divides.mod_less, simp)
apply (rule less_le_trans[OF unat_lt2p])
apply simp
done

1
proof/crefine/ARM/IpcCancel_C.thy
View File

@ -2265,6 +2265,7 @@ proof -
apply (subst uint_nat)
apply (simp add: unat_of_nat)
apply (subst Divides.mod_less)
apply simp
apply (rule order_le_less_trans[OF word_clz_max])
apply (simp add: word_size)
apply (rule iffD2 [OF le_nat_iff[symmetric]])

12
proof/crefine/ARM/Retype_C.thy
View File

@ -93,7 +93,7 @@ definition
region_is_typeless :: "word32 \<Rightarrow> nat \<Rightarrow> ('a globals_scheme, 'b) StateSpace.state_scheme \<Rightarrow> bool"
where
"region_is_typeless ptr sz s \<equiv>
\<forall>z\<in>{ptr ..+ sz}. snd (snd (t_hrs_' (globals s)) z) = empty"
\<forall>z\<in>{ptr ..+ sz}. snd (snd (t_hrs_' (globals s)) z) = Map.empty"
lemma c_guard_word8:
"c_guard (p :: word8 ptr) = (ptr_val p \<noteq> 0)"
@ -202,7 +202,7 @@ lemma const_less_word: "\<lbrakk> (a :: word32) - 1 < b; a \<noteq> b \<rbrakk>
lemma const_le_unat_word: "\<lbrakk> b < 2 ^ word_bits; of_nat b \<le> a \<rbrakk> \<Longrightarrow> b \<le> unat (a :: word32)"
apply (clarsimp simp: word_le_def uint_nat)
apply (subst (asm) unat_of_nat32)
apply (clarsimp simp: word_bits_def size)
apply (clarsimp simp: word_bits_def)
apply clarsimp
done
@ -487,11 +487,11 @@ qed
lemma h_t_valid_not_empty:
fixes p :: "'a :: c_type ptr"
shows "\<lbrakk> d,g \<Turnstile>\<^sub>t p; x \<in> {ptr_val p..+size_of TYPE('a)} \<rbrakk> \<Longrightarrow> snd (d x) \<noteq> empty"
shows "\<lbrakk> d,g \<Turnstile>\<^sub>t p; x \<in> {ptr_val p..+size_of TYPE('a)} \<rbrakk> \<Longrightarrow> snd (d x) \<noteq> Map.empty"
apply (drule intvlD)
apply (clarsimp simp: h_t_valid_def size_of_def)
apply (drule valid_footprintD)
apply (simp add: typ_uinfo_size)
apply simp
apply clarsimp
done
@ -3251,7 +3251,7 @@ lemma cnc_tcb_helper:
(is "(\<sigma>\<lparr>ksPSpace := ?ks\<rparr>, globals_update ?gs' x) \<in> rf_sr")
proof -
def ko \<equiv> "(KOCTE (makeObject :: cte))"
define ko where "ko \<equiv> (KOCTE (makeObject :: cte))"
let ?ptr = "cte_Ptr (ctcb_ptr_to_tcb_ptr p)"
let ?arr_ptr = "Ptr (ctcb_ptr_to_tcb_ptr p) :: (cte_C[5]) ptr"
let ?sp = "\<sigma>\<lparr>ksPSpace := ks\<rparr>"
@ -4226,7 +4226,7 @@ proof (intro impI allI)
apply simp
done
def big_0s \<equiv> "(replicate (2^pageBits) 0) :: word8 list"
define big_0s where "big_0s \<equiv> (replicate (2^pageBits) 0) :: word8 list"
have "length big_0s = 4096" unfolding big_0s_def
by simp (simp add: pageBits_def)

8
proof/crefine/ARM/StoreWord_C.thy
View File

@ -411,8 +411,8 @@ proof (intro allI impI)
and piud: "pointerInUserData ptr \<sigma>"
by simp_all
def offset \<equiv> "ucast ((ptr && mask pageBits) >> 2) :: 10 word"
def base \<equiv> "Ptr (ptr && ~~ mask pageBits) :: user_data_C ptr"
define offset where "offset \<equiv> ucast ((ptr && mask pageBits) >> 2) :: 10 word"
define base where "base \<equiv> Ptr (ptr && ~~ mask pageBits) :: user_data_C ptr"
from piud
obtain old_w where
@ -719,8 +719,8 @@ proof (intro allI impI)
and piud: "pointerInDeviceData ptr \<sigma>"
by simp_all
def offset \<equiv> "ucast ((ptr && mask pageBits) >> 2) :: 10 word"
def base \<equiv> "Ptr (ptr && ~~ mask pageBits) :: user_data_device_C ptr"
define offset where "offset \<equiv> ucast ((ptr && mask pageBits) >> 2) :: 10 word"
define base where "base \<equiv> Ptr (ptr && ~~ mask pageBits) :: user_data_device_C ptr"
from piud
obtain old_w where

2
proof/crefine/ARM/VSpace_C.thy
View File

@ -2689,7 +2689,7 @@ lemma updateCap_frame_mapped_addr_ccorres:
shows "ccorres dc xfdc
(cte_wp_at' (\<lambda>c. ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap))
UNIV []
(updateCap ctSlot (ArchObjectCap (capVPMappedAddress_update empty cap)))
(updateCap ctSlot (ArchObjectCap (capVPMappedAddress_update Map.empty cap)))
(CALL generic_frame_cap_ptr_set_capFMappedAddress(cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']),(scast asidInvalid),0))"
unfolding updateCap_def
apply (rule ccorres_guard_imp2)

2
proof/crefine/lib/Corres_C.thy
View File

@ -1060,7 +1060,7 @@ lemma ccorres_sequenceE_while_gen_either_way:
(body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xfrel_upd (xf s)) s)))"
(is "ccorres_underlying sr \<Gamma> (inr_rrel ?r') ?xf' arrel axf ?G ?G' hs (sequenceE xs) ?body")
proof -
def init_xs \<equiv> xs
define init_xs where "init_xs \<equiv> xs"
have rl: "xs = drop (length init_xs - length xs) init_xs" unfolding init_xs_def
by fastforce

1
spec/ROOT
View File

@ -103,6 +103,7 @@ session CKernel = CParser +
sessions
"ExecSpec"
"CLib"
"AsmRefine"
theories [condition = "SORRY_MODIFIES_PROOFS", quick_and_dirty]
"cspec/$L4V_ARCH/Kernel_C"
theories