Theory AutoCorres2.Split_Heap
chapter "HL phase: Heap Lifting / Split Heap"
theory Split_Heap
imports
TypHeapSimple
begin
ML_file "ac_names.ML"
definition array_fields :: "nat ⇒ qualified_field_name list" where
"array_fields n = map (λn. [replicate n CHR ''1'']) [0..<n]"
lemma Nil_nmem_array_fields[simp]: "[] ∉ set (array_fields n)"
by (auto simp add: array_fields_def)
lemma distinct_prop_disj_fn_array_fields[simp]: "distinct_prop disj_fn (array_fields n)"
by (simp add: array_fields_def distinct_prop_iff_nth)
lemma field_lookup_field_ti':
"field_lookup (typ_info_t TYPE('a :: c_type)) f 0 = Some (a, b) ⟹ field_ti TYPE('a) f = Some a"
unfolding field_ti_def by simp
lemma field_lookup_append_add:
"wf_desc t ⟹
field_lookup t (f @ g) n =
Option.bind (field_lookup t f n) (λ(t', m).
Option.bind (field_lookup t' g 0) (λ(t'', m'). Some (t'', m + m')))"
by (subst field_lookup_append_eq)
(auto simp: field_lookup_offset intro: field_lookup_offset_None[THEN iffD2]
split: bind_split)
lemma nth_array_fields: "i < n ⟹ array_fields n ! i = [replicate i CHR ''1'']"
by (simp add: array_fields_def)
lemma array_fields_Suc: "array_fields (Suc n) = array_fields n @ [[replicate n CHR ''1'']]"
by (simp add: array_fields_def)
lemma find_append: "find P (xs @ ys) = (case find P xs of None ⇒ find P ys | Some x => Some x)"
by (induct xs) auto
lemma length_array_fields: "length (array_fields n) = n"
by (simp add: array_fields_def)
lemma set_array_fields: "set (array_fields n) = (⋃i<n. {[replicate i CHR ''1'']})"
by (induct n) (auto simp add: array_fields_def)
lemma find_array_fields_Some:
"find P (array_fields n) = Some y ⟷
(∃i < n. y = [replicate i CHR ''1''] ∧ P y ∧ (∀j<i. ¬ P ([replicate j CHR ''1''])))"
proof (induct n arbitrary: y)
case 0
then show ?case
by (simp add: array_fields_def)
next
case (Suc n)
show ?case
proof (cases "find P (array_fields n)")
case None
then show ?thesis
apply (simp add: array_fields_Suc find_append )
using less_Suc_eq
by (auto dest!: findNoneD simp add: set_array_fields)
next
case (Some a)
then show ?thesis
apply (simp add: array_fields_Suc find_append )
apply (simp add: Suc.hyps)
by (metis less_Suc_eq linorder_neqE_nat)
qed
qed
lemma Bex_intvl_conv: "(∃x ∈ {0..<n::nat}. P x) ⟷ (∃i. i < n ∧ P i)"
by auto
lemma Bex_union_conv: "(∃x ∈ A ∪ B. P x) ⟷ ((∃x ∈ A. P x) ∨ (∃x ∈ B. P x))"
by auto
lemma ex_intvl_conj_distribR: " ((∃x∈{0..<n}. P x) ∧ Q) ⟷ (∃x∈{0..<n}. P x ∧ Q)"
by blast
lemma ex_less_conj_distribR: "((∃i<n::nat. P i) ∧ Q) ⟷ (∃i<n. P i ∧ Q)"
by blast
lemma map_filter_map_Some_conv:
assumes all_Some: "⋀x. x ∈ set xs ⟹ f x = Some (g x)"
shows "List.map_filter f xs = map g xs"
using all_Some
apply (induct xs)
apply (auto simp add: List.map_filter_def)
done
lemma map_filter_map_compose:
"List.map_filter f (map g xs) = List.map_filter (f o g) xs"
by (induct xs) (auto simp add: List.map_filter_def)
lemma map_filter_fun_eq_conv:
assumes all_same: "⋀x. x ∈ set xs ⟹ f x = g x"
shows "List.map_filter f xs = List.map_filter g xs"
using all_same
apply (induct xs)
apply (auto simp add: List.map_filter_def)
done
lemma map_filter_empty[simp]: "List.map_filter Map.empty xs = []"
by (simp add: List.map_filter_def)
lemma map_filter_Some[simp]: "List.map_filter (λx. Some (f x)) xs = map f xs"
by (simp add: List.map_filter_def)
lemma list_all_field_lookup[simp]:
"CARD('n) = m ⟹
list_all
(λf. ∃a b. field_lookup (typ_uinfo_t TYPE('a::c_type['n::finite])) f 0 = Some (a, b))
(map (λn. [replicate n CHR ''1'']) [0..<m])"
using field_lookup_array[where 'b='n and 'a='a]
apply (simp add: list_all_iff atLeast0LessThan typ_uinfo_t_def flip: All_less_Ball)
using field_lookup_export_uinfo_Some by blast
lemma ptr_span_with_stack_byte_type_subset_field[simp]:
"∀a∈ptr_span (p::'a::mem_type ptr). root_ptr_valid h (PTR(stack_byte) a) ⟹
∃u. field_ti TYPE('a::mem_type) f = Some u ∧ size_td u = sz ⟹
(∀a∈{&(p→f)..+sz}. root_ptr_valid h (PTR(stack_byte) a)) ⟷ True"
by (auto simp: dest!: mem_type_class.field_tag_sub field_tiD)
lemma (in pointer_lense) pointer_lense_field_lvalue:
assumes f: "field_ti TYPE('c::mem_type) f = Some u"
and u: "size_td u = size_of TYPE('a)"
shows "pointer_lense (λh (p::'c ptr). r h (PTR('a) &(p→f))) (λp. w (PTR('a) &(p→f)))"
apply unfold_locales
apply (simp_all add: read_write_same write_same)
apply (subst write_other_commute)
subgoal for p q
using field_tag_sub[OF field_tiD, OF f, of p]
using field_tag_sub[OF field_tiD, OF f, of q]
apply (simp add: u)
apply (rule disjnt_subset1, erule disjnt_subset2)
by auto
apply simp
done
lemma exists_nat_numeral: "∃x::nat. x < numeral k"
apply (rule exI[where x=0])
apply (rule Num.rel_simps)
done
lemma fun_upd_eq_cases: "f(p:=x) = g ⟷ (g p = x ∧ (∀q. p≠q ⟶ f q = g q))"
by (auto simp add: fun_upd_def)
lemma fun_upd_apply_eq_cases: "(f(p:=x)) q = g q ⟷ ((p = q ⟶ g q = x) ∧ (p ≠ q ⟶ f q = g q))"
by (auto simp add: fun_upd_def)
lemma comp_fun_upd_same_fuse:
"(λf. f(p := x)) o (λf. f(p := y)) = (λf. f(p:=x))"
by auto
lemma comp_fun_upd_other_commute:
"p ≠ q ⟹ (λf. f(q := y)) o (λf. f(p := x)) = (λf. f(p := x)) o (λf. f(q := y))"
by (auto simp add: comp_def fun_upd_def fun_eq_iff)
lemma map_td_compose:
fixes t::"('a, 'b) typ_desc"
and st::"('a, 'b) typ_struct"
and ts::"('a, 'b) typ_tuple list"
and x::"('a, 'b) typ_tuple"
shows
"map_td f1 g1 (map_td f2 g2 t) = map_td (λn algn. f1 n algn o f2 n algn) (g1 o g2) t" and
"map_td_struct f1 g1 (map_td_struct f2 g2 st) = map_td_struct (λn algn. f1 n algn o f2 n algn) (g1 o g2) st" and
"map_td_list f1 g1 (map_td_list f2 g2 ts) = map_td_list (λn algn. f1 n algn o f2 n algn) (g1 o g2) ts" and
"map_td_tuple f1 g1 (map_td_tuple f2 g2 x) = map_td_tuple (λn algn. f1 n algn o f2 n algn) (g1 o g2) x"
proof (induct t and st and ts and x)
case (TypDesc nat typ_struct list)
then show ?case by auto
next
case (TypScalar nat1 nat2 a)
then show ?case by auto
next
case (TypAggregate list)
then show ?case by auto
next
case Nil_typ_desc
then show ?case by auto
next
case (Cons_typ_desc dt_tuple list)
then show ?case by auto
next
case (DTuple_typ_desc typ_desc list b)
then show ?case by auto
qed
lemma (in mem_type) distinct_all_field_names:
"distinct (all_field_names (typ_info_t TYPE('a)))"
using distinct_all_field_names wf_desc by blast
lemma field_lookup_same_type_disjoint:
"⟦field_lookup t f m = Some (d,n);
field_lookup t f' m = Some (d',n'); f ≠ f'; export_uinfo d = export_uinfo d';
wf_desc t; size_td t < addr_card⟧ ⟹
{(of_nat n)::addr..+size_td (d::('a,'b) typ_info)} ∩ {of_nat n'..+size_td d'} = {}" and
"⟦field_lookup_struct st f m = Some (d,n);
field_lookup_struct st f' m = Some (d',n'); f ≠ f'; export_uinfo d = export_uinfo d';
wf_desc_struct st; size_td_struct st < addr_card ⟧ ⟹
{(of_nat n)::addr..+size_td (d::('a,'b) typ_info)} ∩ {of_nat n'..+size_td d'} = {}" and
"⟦field_lookup_list ts f m = Some (d,n);
field_lookup_list ts f' m = Some (d',n'); f ≠ f'; export_uinfo d = export_uinfo d';
wf_desc_list ts; size_td_list ts < addr_card⟧ ⟹
{(of_nat n)::addr..+size_td (d::('a,'b) typ_info)} ∩ {of_nat n'..+size_td d'} = {}" and
"⟦field_lookup_tuple x f m = Some (d,n) ;
field_lookup_tuple x f' m = Some (d',n'); f ≠ f'; export_uinfo d = export_uinfo d';
wf_desc_tuple x; size_td_tuple x < addr_card⟧ ⟹
{(of_nat n)::addr..+size_td (d::('a,'b) typ_info)} ∩ {of_nat n'..+size_td d'} = {}"
proof (induct t and st and ts and x arbitrary: f m d n f' m d' n' and f m d n f' m d' n' and
f m d n f' m d' n' and f m d n f' m d' n')
case (TypDesc algn st nm)
then show ?case
by (metis field_lookup.simps field_lookup_export_uinfo_Some field_lookup_same_type_empty(1)
size_td.simps wf_desc.simps)
next
case (TypScalar n algn x)
then show ?case by auto
next
case (TypAggregate ts)
then show ?case by simp
next
case Nil_typ_desc
then show ?case by simp
next
case (Cons_typ_desc x xs)
from Cons_typ_desc.prems obtain
f: "field_lookup_list (x # xs) f m = Some (d, n)" and
f': "field_lookup_list (x # xs) f' m = Some (d', n')" and
neq_f_f': "f ≠ f'" and
eq_d_d': "export_uinfo d = export_uinfo d'" and
sz: "size_td_tuple x + size_td_list xs < addr_card" and
wf_x: "wf_desc_tuple x" and
distinct: "dt_snd x ∉ dt_snd ` set xs" and
wf_xs: "wf_desc_list xs" by clarsimp
from sz have sz_xs: "size_td_list xs < addr_card" by auto
from sz have sz_x: "size_td_tuple x < addr_card" by auto
show ?case
proof (cases "field_lookup_tuple x f m")
case None
note f_None = this
from f None have f_xs: "field_lookup_list xs f (m + size_td (dt_fst x)) = Some (d, n)" by simp
from td_set_list_field_lookup_listD [OF f_xs] have "(d, n) ∈ td_set_list xs (m + size_td (dt_fst x))" .
from td_set_list_intvl_sub [OF this]
have contained_f: "{word_of_nat n..+size_td d} ⊆ {word_of_nat (m + size_td (dt_fst x))..+size_td_list xs}" .
show ?thesis
proof (cases "field_lookup_tuple x f' m")
case None
from f' None have f'_xs: "field_lookup_list xs f' (m + size_td (dt_fst x)) = Some (d', n')" by simp
from Cons_typ_desc.hyps(2) [OF f_xs f'_xs neq_f_f' eq_d_d' wf_xs sz_xs]
show ?thesis .
next
case (Some _)
with f' have f'_x: "field_lookup_tuple x f' m = Some (d', n')" by simp
from td_set_tuple_field_lookup_tupleD [OF f'_x] have "(d', n') ∈ td_set_tuple x m" .
from td_set_tuple_intvl_sub [OF this]
have "{word_of_nat n'..+size_td d'} ⊆ {word_of_nat m..+size_td_tuple x}" .
with contained_f sz show ?thesis
by (smt (verit, ccfv_SIG) disj_subset init_intvl_disj of_nat_add size_td_tuple_dt_fst)
qed
next
case (Some _)
from f Some have f_x: "field_lookup_tuple x f m = Some (d, n)" by simp
from td_set_tuple_field_lookup_tupleD [OF f_x] have "(d, n) ∈ td_set_tuple x m" .
from td_set_tuple_intvl_sub [OF this]
have contained_f: "{word_of_nat n..+size_td d} ⊆ {word_of_nat m..+size_td_tuple x}" .
show ?thesis
proof (cases "field_lookup_tuple x f' m")
case None
from f' None have f'_xs: "field_lookup_list xs f' (m + size_td (dt_fst x)) = Some (d', n')" by simp
from td_set_list_field_lookup_listD [OF f'_xs]
have "(d', n') ∈ td_set_list xs (m + size_td (dt_fst x))" .
from td_set_list_intvl_sub [OF this]
have "{word_of_nat n'..+size_td d'} ⊆ {word_of_nat (m + size_td (dt_fst x))..+size_td_list xs}" .
with contained_f sz show ?thesis
by (smt (verit, ccfv_threshold) Int_commute disjoint_subset init_intvl_disj
of_nat_add size_td_tuple_dt_fst)
next
case (Some _)
with f' have f'_x: "field_lookup_tuple x f' m = Some (d', n')" by simp
from Cons_typ_desc.hyps(1) [OF f_x f'_x neq_f_f' eq_d_d' wf_x sz_x]
show ?thesis .
qed
qed
next
case (DTuple_typ_desc typ_desc list b)
then show ?case
by (metis fl5 list.expand option.simps(3) size_td_tuple.simps wf_desc_tuple.simps)
qed
lemma field_lookup_same_type_u_disjoint:
"⟦field_lookup t f m = Some (d,n);
field_lookup t f' m = Some (d,n'); f ≠ f';
wf_desc t; size_td t < addr_card⟧ ⟹
{(of_nat n)::addr..+size_td d} ∩ {of_nat n'..+size_td d} = {}" and
"⟦field_lookup_struct st f m = Some (d,n);
field_lookup_struct st f' m = Some (d,n'); f ≠ f';
wf_desc_struct st; size_td_struct st < addr_card ⟧ ⟹
{(of_nat n)::addr..+size_td d} ∩ {of_nat n'..+size_td d} = {}" and
"⟦field_lookup_list ts f m = Some (d,n);
field_lookup_list ts f' m = Some (d,n'); f ≠ f';
wf_desc_list ts; size_td_list ts < addr_card⟧ ⟹
{(of_nat n)::addr..+size_td d} ∩ {of_nat n'..+size_td d} = {}" and
"⟦field_lookup_tuple x f m = Some (d,n) ;
field_lookup_tuple x f' m = Some (d,n'); f ≠ f';
wf_desc_tuple x; size_td_tuple x < addr_card⟧ ⟹
{(of_nat n)::addr..+size_td d} ∩ {of_nat n'..+size_td d} = {}"
proof (induct t and st and ts and x arbitrary: f m d n f' m n' and f m d n f' m n' and
f m d n f' m n' and f m d n f' m n')
case (TypDesc algn st nm)
then show ?case
by (metis field_lookup.simps field_lookup_same_type_empty(1)
size_td.simps wf_desc.simps)
next
case (TypScalar n algn x)
then show ?case by auto
next
case (TypAggregate ts)
then show ?case by simp
next
case Nil_typ_desc
then show ?case by simp
next
case (Cons_typ_desc x xs)
from Cons_typ_desc.prems obtain
f: "field_lookup_list (x # xs) f m = Some (d, n)" and
f': "field_lookup_list (x # xs) f' m = Some (d, n')" and
neq_f_f': "f ≠ f'" and
sz: "size_td_tuple x + size_td_list xs < addr_card" and
wf_x: "wf_desc_tuple x" and
distinct: "dt_snd x ∉ dt_snd ` set xs" and
wf_xs: "wf_desc_list xs" by clarsimp
from sz have sz_xs: "size_td_list xs < addr_card" by auto
from sz have sz_x: "size_td_tuple x < addr_card" by auto
show ?case
proof (cases "field_lookup_tuple x f m")
case None
note f_None = this
from f None have f_xs: "field_lookup_list xs f (m + size_td (dt_fst x)) = Some (d, n)" by simp
from td_set_list_field_lookup_listD [OF f_xs] have "(d, n) ∈ td_set_list xs (m + size_td (dt_fst x))" .
from td_set_list_intvl_sub [OF this]
have contained_f: "{word_of_nat n..+size_td d} ⊆ {word_of_nat (m + size_td (dt_fst x))..+size_td_list xs}" .
show ?thesis
proof (cases "field_lookup_tuple x f' m")
case None
from f' None have f'_xs: "field_lookup_list xs f' (m + size_td (dt_fst x)) = Some (d, n')" by simp
from Cons_typ_desc.hyps(2) [OF f_xs f'_xs neq_f_f' wf_xs sz_xs]
show ?thesis .
next
case (Some _)
with f' have f'_x: "field_lookup_tuple x f' m = Some (d, n')" by simp
from td_set_tuple_field_lookup_tupleD [OF f'_x] have "(d, n') ∈ td_set_tuple x m" .
from td_set_tuple_intvl_sub [OF this]
have "{word_of_nat n'..+size_td d} ⊆ {word_of_nat m..+size_td_tuple x}" .
with contained_f sz show ?thesis
by (smt (verit, ccfv_SIG) disj_subset init_intvl_disj of_nat_add size_td_tuple_dt_fst)
qed
next
case (Some _)
from f Some have f_x: "field_lookup_tuple x f m = Some (d, n)" by simp
from td_set_tuple_field_lookup_tupleD [OF f_x] have "(d, n) ∈ td_set_tuple x m" .
from td_set_tuple_intvl_sub [OF this]
have contained_f: "{word_of_nat n..+size_td d} ⊆ {word_of_nat m..+size_td_tuple x}" .
show ?thesis
proof (cases "field_lookup_tuple x f' m")
case None
from f' None have f'_xs: "field_lookup_list xs f' (m + size_td (dt_fst x)) = Some (d, n')" by simp
from td_set_list_field_lookup_listD [OF f'_xs]
have "(d, n') ∈ td_set_list xs (m + size_td (dt_fst x))" .
from td_set_list_intvl_sub [OF this]
have "{word_of_nat n'..+size_td d} ⊆ {word_of_nat (m + size_td (dt_fst x))..+size_td_list xs}" .
with contained_f sz show ?thesis
by (smt (verit, ccfv_threshold) Int_commute disjoint_subset init_intvl_disj
of_nat_add size_td_tuple_dt_fst)
next
case (Some _)
with f' have f'_x: "field_lookup_tuple x f' m = Some (d, n')" by simp
from Cons_typ_desc.hyps(1) [OF f_x f'_x neq_f_f' wf_x sz_x]
show ?thesis .
qed
qed
next
case (DTuple_typ_desc typ_desc list b)
then show ?case
by (metis fl5 list.expand option.simps(3) size_td_tuple.simps wf_desc_tuple.simps)
qed
lemma td_set_list_intvl_sub_nat:
"(d,n) ∈ td_set_list t m ⟹ {n..< n +size_td d} ⊆ {m..< m +size_td_list t}"
apply(frule td_set_list_offset_le)
apply(drule td_set_list_offset_size_m)
apply auto
done
lemma td_set_tuple_intvl_sub_nat:
"(d,n) ∈ td_set_tuple t m ⟹ {n..<n+size_td d} ⊆ {m..<m+size_td_tuple t}"
apply(frule td_set_tuple_offset_le)
apply(drule td_set_tuple_offset_size_m)
apply auto
done
lemma field_lookup_same_type_u_disjoint_nat:
"⟦field_lookup t f m = Some (d,n);
field_lookup t f' m = Some (d,n'); f ≠ f';
wf_desc t⟧ ⟹
{n..<n + size_td d} ∩ {n'..<n' + size_td d} = {}" and
"⟦field_lookup_struct st f m = Some (d,n);
field_lookup_struct st f' m = Some (d,n'); f ≠ f';
wf_desc_struct st ⟧ ⟹
{n..< n + size_td d} ∩ {n'..< n' + size_td d} = {}" and
"⟦field_lookup_list ts f m = Some (d,n);
field_lookup_list ts f' m = Some (d,n'); f ≠ f';
wf_desc_list ts⟧ ⟹
{n..<n + size_td d} ∩ {n'..<n' + size_td d} = {}" and
"⟦field_lookup_tuple x f m = Some (d,n) ;
field_lookup_tuple x f' m = Some (d,n'); f ≠ f';
wf_desc_tuple x⟧ ⟹
{n..<n + size_td d} ∩ {n'..<n' +size_td d} = {}"
proof (induct t and st and ts and x arbitrary: f m d n f' m n' and f m d n f' m n' and
f m d n f' m n' and f m d n f' m n')
case (TypDesc algn st nm)
then show ?case
by (metis field_lookup.simps field_lookup_same_type_empty(1)
wf_desc.simps)
next
case (TypScalar n algn x)
then show ?case by auto
next
case (TypAggregate ts)
then show ?case by auto
next
case Nil_typ_desc
then show ?case by simp
next
case (Cons_typ_desc x xs)
from Cons_typ_desc.prems obtain
f: "field_lookup_list (x # xs) f m = Some (d, n)" and
f': "field_lookup_list (x # xs) f' m = Some (d, n')" and
neq_f_f': "f ≠ f'" and
wf_x: "wf_desc_tuple x" and
distinct: "dt_snd x ∉ dt_snd ` set xs" and
wf_xs: "wf_desc_list xs" by clarsimp
show ?case
proof (cases "field_lookup_tuple x f m")
case None
note f_None = this
from f None have f_xs: "field_lookup_list xs f (m + size_td (dt_fst x)) = Some (d, n)" by simp
from td_set_list_field_lookup_listD [OF f_xs] have "(d, n) ∈ td_set_list xs (m + size_td (dt_fst x))" .
from td_set_list_intvl_sub_nat [OF this]
have contained_f: "{n..<n+size_td d} ⊆ {(m + size_td (dt_fst x))..<(m + size_td (dt_fst x)) +size_td_list xs}" .
show ?thesis
proof (cases "field_lookup_tuple x f' m")
case None
from f' None have f'_xs: "field_lookup_list xs f' (m + size_td (dt_fst x)) = Some (d, n')" by simp
from Cons_typ_desc.hyps(2) [OF f_xs f'_xs neq_f_f' wf_xs ]
show ?thesis .
next
case (Some _)
with f' have f'_x: "field_lookup_tuple x f' m = Some (d, n')" by simp
from td_set_tuple_field_lookup_tupleD [OF f'_x] have "(d, n') ∈ td_set_tuple x m" .
from td_set_tuple_intvl_sub_nat[OF this]
have "{n'..<n'+size_td d} ⊆ {m..<m+size_td_tuple x}" .
with contained_f show ?thesis
by (smt (verit, best) disj_inter_swap disj_subset ivl_disj_int_two(3) size_td_tuple_dt_fst)
qed
next
case (Some _)
from f Some have f_x: "field_lookup_tuple x f m = Some (d, n)" by simp
from td_set_tuple_field_lookup_tupleD [OF f_x] have "(d, n) ∈ td_set_tuple x m" .
from td_set_tuple_intvl_sub_nat [OF this]
have contained_f: "{n..<n+size_td d} ⊆ {m..<m+size_td_tuple x}" .
show ?thesis
proof (cases "field_lookup_tuple x f' m")
case None
from f' None have f'_xs: "field_lookup_list xs f' (m + size_td (dt_fst x)) = Some (d, n')" by simp
from td_set_list_field_lookup_listD [OF f'_xs]
have "(d, n') ∈ td_set_list xs (m + size_td (dt_fst x))" .
from td_set_list_intvl_sub_nat [OF this]
have "{n'..<n'+size_td d} ⊆ {(m + size_td (dt_fst x))..<(m + size_td (dt_fst x))+size_td_list xs}" .
with contained_f show ?thesis
by (metis Int_commute disjoint_subset ivl_disj_int_two(3) size_td_tuple_dt_fst)
next
case (Some _)
with f' have f'_x: "field_lookup_tuple x f' m = Some (d, n')" by simp
from Cons_typ_desc.hyps(1) [OF f_x f'_x neq_f_f' wf_x ]
show ?thesis .
qed
qed
next
case (DTuple_typ_desc typ_desc list b)
then show ?case
by (metis fl5 list.expand option.simps(3) wf_desc_tuple.simps)
qed
lemma (in mem_type) field_lookup_same_type_disjoint:
assumes f: "field_lookup (typ_info_t TYPE('a)) f m = Some (t, n) "
assumes f': "field_lookup (typ_info_t TYPE('a)) f' m = Some (t', n')"
assumes neq: "f ≠ f'"
assumes same: "export_uinfo t = export_uinfo t'"
shows "{(of_nat n)::addr..+size_td t} ∩ {of_nat n'..+size_td t'} = {}"
proof -
have "size_td (typ_info_t TYPE('a)) < addr_card"
by (simp add: size_of_fold)
from field_lookup_same_type_disjoint(1) [OF f f' neq same wf_desc this]
show ?thesis
by simp
qed
lemma (in mem_type) field_lookup_same_type_ptr_span_disjoint:
fixes p::"'a ptr"
assumes f: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n) "
assumes f': "field_lookup (typ_info_t TYPE('a)) f' 0 = Some (t', n')"
assumes neq: "f ≠ f'"
assumes t: "export_uinfo t = typ_uinfo_t (TYPE('b::c_type))"
assumes t': "export_uinfo t' = typ_uinfo_t (TYPE('b::c_type))"
shows "ptr_span (PTR('b) &(p→f)) ∩ ptr_span (PTR('b) &(p→f')) = {}"
proof -
from t t' have "export_uinfo t = export_uinfo t'" by simp
from field_lookup_same_type_disjoint [OF f f' neq this]
have "{word_of_nat n::addr..+size_td t} ∩ {word_of_nat n'..+size_td t'} = {}" .
moreover
from t have "size_td t = size_of TYPE('b)"
by (simp add: export_size_of)
moreover
from t' have "size_td t' = size_of TYPE('b)"
by (simp add: export_size_of)
ultimately
show ?thesis
using f f'
by (simp add: field_lvalue_def intvl_disj_offset)
qed
lemma sub_type_valid_field_lvalue_overlap:
fixes p::"'a::mem_type ptr"
fixes q::"'b::mem_type ptr"
assumes subtype: "TYPE('b) ≤⇩τ TYPE('a)"
assumes valid_p: "d ⊨⇩t p"
assumes overlap: "ptr_span p ∩ ptr_span q ≠ {}"
shows "d ⊨⇩t q ⟷
(∃f t n. field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n) ∧
export_uinfo t = typ_uinfo_t TYPE('b) ∧
q = PTR('b) (&(p→f)))"
proof
assume valid_q: "d ⊨⇩t q"
show "∃f t n. field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n) ∧
export_uinfo t = typ_uinfo_t TYPE('b) ∧ q = PTR('b) (&(p→f))"
proof -
from subtype have "typ_uinfo_t TYPE('b) ≤ typ_uinfo_t TYPE('a)" by (simp add: sub_typ_def)
from this overlap valid_footprint_sub_cases [OF h_t_valid_valid_footprint [OF valid_q] h_t_valid_valid_footprint [OF valid_p]]
have field_of: "field_of (ptr_val q - ptr_val p) (typ_uinfo_t TYPE('b)) (typ_uinfo_t TYPE('a))"
apply (simp add: size_of_def)
by (metis Int_commute le_less_trans less_irrefl)
then obtain f where
fl: "field_lookup (typ_uinfo_t (TYPE('a))) f 0 = Some (typ_uinfo_t TYPE('b), unat (ptr_val q - ptr_val p))"
using field_of_lookup_info by blast
then obtain t where
fl': "field_lookup (typ_info_t (TYPE('a))) f 0 = Some (t, unat (ptr_val q - ptr_val p))" and
t: "export_uinfo t = typ_uinfo_t TYPE('b)"
using field_lookup_uinfo_Some_rev by blast
from fl'
have ptr_val_q: "ptr_val q = &(p→f)"
by (simp add: field_lvalue_def)
with fl' t show ?thesis
by (metis Ptr_ptr_val)
qed
next
assume "∃f t n.
field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n) ∧ export_uinfo t = typ_uinfo_t TYPE('b) ∧
q = PTR('b) &(p→f)"
then show "d ⊨⇩t q"
using valid_p
using c_guard_mono h_t_valid_mono by blast
qed
lemma field_lookup_intvl_contained_left:
fixes p::"'a::mem_type ptr"
assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, k)"
assumes n: "n = size_td t"
assumes m: "m = size_of TYPE('a)"
shows "{&(p→f)..+n} ∩ {ptr_val p..+m} ≠ {}"
proof -
from field_tag_sub [OF fl] have "{&(p→f)..+size_td t} ⊆ ptr_span p" .
moreover from fl have "0 < size_td t"
by (simp add: field_lookup_wf_size_desc_gt)
ultimately show ?thesis using n m
by (simp add: intvl_non_zero_non_empty le_iff_inf)
qed
lemma field_lookup_intvl_contained_right:
fixes p::"'a::mem_type ptr"
assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, k)"
assumes n: "n = size_td t"
assumes m: "m = size_of TYPE('a)"
shows " {ptr_val p..+m} ∩ {&(p→f)..+n} ≠ {}"
using field_lookup_intvl_contained_left [OF fl n m] by blast
lemma field_overlap_right:
fixes p::"'a::mem_type ptr"
assumes field_lookup: "field_lookup (typ_info_t TYPE('a)) path 0 = Some (t, n)"
assumes match: "export_uinfo t = typ_uinfo_t TYPE('f)"
shows "(ptr_span p) ∩ ptr_span (PTR('f::c_type) &(p→path)) ≠ {}"
using field_lookup match
by (simp add: export_size_of field_lookup_intvl_contained_right)
locale nested_field' =
fixes t :: "'a::mem_type xtyp_info"
fixes path :: "string list"
fixes sel :: "'a::mem_type ⇒ 'f::mem_type"
fixes upd :: "'f ⇒ 'a ⇒ 'a"
assumes field_ti: "field_ti TYPE('a) path = Some t"
assumes field_typ_match: "export_uinfo t = typ_uinfo_t TYPE('f)"
assumes sel_def: "sel ≡ from_bytes o access_ti⇩0 t"
assumes upd_def: "upd ≡ update_ti t o to_bytes_p"
begin
lemma sub_typ: "TYPE('f) ≤⇩τ TYPE('a)"
using field_ti field_typ_match
using field_ti_sub_typ sub_typ_def by blast
lemma h_val_field:
shows "h_val h (PTR('f) &(p→path)) = sel (h_val h p)"
using TypHeap.h_val_field_from_bytes' field_ti field_typ_match sel_def typ_uinfo_t_def
by fastforce
lemma clift_field_update:
assumes typed: "hrs_htd h ⊨⇩t p"
shows "clift (hrs_mem_update (heap_update (PTR('f) &(p→path)) x) h) =
(clift h)(p↦ upd x (h_val (hrs_mem h) p))"
proof -
from h_t_valid_clift_Some_iff typed obtain v where clift: "clift h p = Some v" by blast
from h_val_clift' [OF this]
have v: "v = h_val (hrs_mem h) p" by simp
from clift_field_update [OF field_ti _ clift [simplified v], where val=x,OF field_typ_match [simplified typ_uinfo_t_def]]
show ?thesis
by (simp add: upd_def export_size_of field_typ_match update_ti_t_def)
qed
lemma clift_field_update_padding:
assumes typed: "hrs_htd h ⊨⇩t p"
assumes lbs: "length bs = size_of TYPE('f)"
shows "clift (hrs_mem_update (heap_update_padding (PTR('f) &(p→path)) x bs) h) =
(clift h)(p↦ upd x (h_val (hrs_mem h) p))"
proof -
from h_t_valid_clift_Some_iff typed obtain v where clift: "clift h p = Some v" by blast
from h_val_clift' [OF this]
have v: "v = h_val (hrs_mem h) p" by simp
from clift_field_update_padding [OF field_ti _ clift [simplified v] lbs, where val=x,OF field_typ_match [simplified typ_uinfo_t_def]]
show ?thesis
by (simp add: upd_def export_size_of field_typ_match update_ti_t_def)
qed
lemma h_val_field_lvalue_update: "d ⊨⇩t p ⟹ d ⊨⇩t q ⟹
h_val (heap_update (PTR('f) &(p→path)) x h) q = ((h_val h)(p := upd x (h_val h p))) q"
by (smt (verit, best) c_type_class.lift_def clift_Some_eq_valid h_val_clift'
hrs_htd_def hrs_mem_def hrs_mem_update lift_heap_update lift_t_heap_update
nested_field'.clift_field_update nested_field'_axioms prod.sel(1) prod.sel(2))
lemma h_val_field_lvalue_update_padding: "d ⊨⇩t p ⟹ d ⊨⇩t q ⟹ length bs = size_of TYPE('f) ⟹
h_val (heap_update_padding (PTR('f) &(p→path)) x bs h) q = ((h_val h)(p := upd x (h_val h p))) q"
by (smt (verit, ccfv_threshold) clift_Some_eq_valid fst_conv h_val_clift hrs_htd_def
hrs_htd_mem_update hrs_mem_def hrs_mem_update clift_field_update_padding
clift_field_update h_val_field_lvalue_update prod.collapse snd_conv)
end
lemma align_addr_card:
assumes wf_size_desc: "wf_size_desc t"
assumes max_size: "size_td t < addr_card"
assumes align_size_of: "2 ^ align_td t dvd size_td t"
shows "2 ^ align_td t dvd addr_card"
proof -
from wf_size_desc have sz_nzero: "0 < size_td t"
by (simp add: wf_size_desc_gt(1))
with align_size_of max_size
have align_bound: "align_td t < addr_bitsize"
by (metis addr_card linorder_not_le nat_dvd_not_less power_le_dvd)
then have bound: "2 ^ align_td t < addr_card"
by (metis addr_card one_less_numeral_iff power_strict_increasing semiring_norm(76))
from bound align_bound
show ?thesis
apply (clarsimp simp: dvd_def)
apply (rule exI[where x="2^(len_of TYPE(addr_bitsize) - align_td t)"])
apply clarsimp
apply(simp add: addr_card flip: power_add)
done
qed
lemma ptr_aligned_u_field_lookup:
assumes wf_size_desc: "wf_size_desc t"
assumes wf_align: "wf_align t"
assumes align_field: "align_field t"
assumes max_size: "size_td t < addr_card"
assumes align_size_of: "2 ^ align_td t dvd size_td t"
assumes align_size_of_u: "2 ^ align_td u dvd size_td u"
assumes fl: "field_lookup t path 0 = Some (u, n)"
assumes ptr_aligned_u: "ptr_aligned_u t a"
shows "ptr_aligned_u u (a + of_nat n)"
proof -
from wf_size_desc fl have wf_size_desc_u: "wf_size_desc u"
using field_lookup_wf_size_desc_pres(1) by blast
from fl have u_n_bound: "size_td u + n ≤ size_td t"
by (simp add: field_lookup_offset_size')
with max_size have n_bound: "n < addr_card"
by simp
from u_n_bound max_size have sz_u: "size_td u < addr_card"
by simp
from align_td_field_lookup(1) [OF wf_align fl] have align_u_t: "align_td u ≤ align_td t" .
from align_field fl
have "2 ^ (align_td u) dvd n" by (simp add: align_field_def)
moreover
from ptr_aligned_u have "2 ^ align_td t dvd unat a" by (simp add: ptr_aligned_u_def)
ultimately have "2 ^ align_td u dvd unat (a + word_of_nat n)"
apply -
apply(subst unat_word_ariths)
apply(rule dvd_mod)
apply(rule dvd_add)
subgoal
using align_u_t
using power_le_dvd by blast
subgoal
apply(subst unat_of_nat)
apply(subst Euclidean_Rings.mod_less)
apply(subst len_of_addr_card)
apply (rule n_bound)
apply assumption
done
subgoal
apply(subst len_of_addr_card)
apply (rule align_addr_card)
apply (rule wf_size_desc_u)
apply (rule sz_u)
apply (rule align_size_of_u)
done
done
then show ?thesis
by (simp add: ptr_aligned_u_def)
qed
lemma c_guard_u_field_looup:
assumes wf_size_desc: "wf_size_desc t"
assumes wf_align: "wf_align t"
assumes align_field: "align_field t"
assumes max_size: "size_td t < addr_card"
assumes align_size_of: "2 ^ align_td t dvd size_td t"
assumes align_size_of_u: "2 ^ align_td u dvd size_td u"
assumes fl: "field_lookup t path 0 = Some (u, n)"
assumes c_guard_u: "c_guard_u t a"
shows "c_guard_u u (a + of_nat n)"
proof -
from wf_size_desc have sz_t: "0 < size_td t"
using wf_size_desc_gt(1) by blast
from wf_size_desc fl have sz_u: "0 < size_td u"
by (simp add: field_lookup_wf_size_desc_gt)
show ?thesis
using fl c_guard_u
apply (clarsimp simp add: c_guard_u_def)
apply safe
subgoal by (rule ptr_aligned_u_field_lookup [OF wf_size_desc wf_align align_field max_size align_size_of align_size_of_u fl])
subgoal by (meson c_null_guard_u_def field_lookup_offset_size' intvl_le subsetD)
done
qed
lemma cvalid_u_field_lookup:
assumes wf_size_desc: "wf_size_desc t"
assumes wf_align: "wf_align t"
assumes align_field: "align_field t"
assumes max_size: "size_td t < addr_card"
assumes align_size_of: "2 ^ align_td t dvd size_td t"
assumes align_size_of_u: "2 ^ align_td u dvd size_td u"
assumes fl: "field_lookup t path 0 = Some (u, n)"
assumes cvalid_u: "cvalid_u t d a"
shows "cvalid_u u d (a + of_nat n)"
proof -
from wf_size_desc have sz_t: "0 < size_td t"
using wf_size_desc_gt(1) by blast
from wf_size_desc fl have sz_u: "0 < size_td u"
by (simp add: field_lookup_wf_size_desc_gt)
from fl have u_n_bound: "size_td u + n ≤ size_td t"
by (simp add: field_lookup_offset_size')
with max_size have n_bound: "n < addr_card"
by simp
from u_n_bound max_size have sz_u_addr_card: "size_td u < addr_card"
by simp
note c_guard = c_guard_u_field_looup [OF wf_size_desc wf_align align_field max_size align_size_of align_size_of_u fl]
from cvalid_u
show ?thesis
apply(clarsimp simp: cvalid_u_def valid_footprint_def Let_def sz_t sz_u c_guard)
subgoal for y
apply(drule_tac x="n+y" in spec)
apply (erule impE)
subgoal using u_n_bound by simp
subgoal
by (metis (mono_tags, lifting) ab_semigroup_add_class.add_ac(1)
fl map_list_map_trans of_nat_add td_set_field_lookupD typ_slice_td_set)
done
done
qed
locale mem_type_u =
fixes t::typ_uinfo
assumes wf_desc: "wf_desc t"
assumes wf_size_desc: "wf_size_desc t"
assumes wf_align: "wf_align t"
assumes align_field: "align_field t"
assumes max_size: "size_td t < addr_card"
assumes align_size: "2 ^ align_td t dvd size_td t"
begin
lemmas ptr_aligned_u_field_lookup = ptr_aligned_u_field_lookup [OF wf_size_desc wf_align align_field max_size align_size]
lemmas c_guard_u_field_looup = c_guard_u_field_looup [OF wf_size_desc wf_align align_field max_size align_size]
lemmas cvalid_u_field_lookup = cvalid_u_field_lookup [OF wf_size_desc wf_align align_field max_size align_size]
end
lemma wf_size_desc_export_uinfo:
fixes t::"('a, 'b) typ_info"
and st::"('a, 'b) typ_info_struct"
and ts::"('a, 'b) typ_info_tuple list"
and x::"('a, 'b) typ_info_tuple"
shows
"wf_size_desc t ⟹ wf_size_desc (export_uinfo t)" and
"wf_size_desc_struct st ⟹ wf_size_desc_struct ( map_td_struct field_norm (λ_. ()) st)" and
"wf_size_desc_list ts ⟹ wf_size_desc_list ( map_td_list field_norm (λ_. ()) ts)" and
"wf_size_desc_tuple x ⟹ wf_size_desc_tuple ( map_td_tuple field_norm (λ_. ()) x)"
proof (induct t and st and ts and x)
case (TypDesc nat typ_struct list)
then show ?case by auto
next
case (TypScalar nat1 nat2 a)
then show ?case by auto
next
case (TypAggregate list)
then show ?case by auto
next
case Nil_typ_desc
then show ?case by auto
next
case (Cons_typ_desc dt_tuple list)
then show ?case by auto
next
case (DTuple_typ_desc typ_desc list b)
then show ?case by (auto simp add: export_uinfo_def)
qed
context mem_type
begin
lemma typ_uinfo_t_mem_type[simp]: "mem_type_u (typ_uinfo_t(TYPE('a)))"
apply (simp only: typ_uinfo_t_def)
apply (unfold_locales)
apply (simp add: typ_uinfo_t_def wf_desc_export_uinfo_pres(1))
apply (simp add:wf_size_desc_export_uinfo)
apply (metis export_uinfo_typdesc_simp local.wf_align typ_desc.exhaust wf_align_map_td(1))
using local.align_field local.align_field_uinfo local.typ_uinfo_t_def apply fastforce
apply (simp add: size_of_fold)
using align_size_of
apply (simp add: size_of_def align_of_def)
done
sublocale u: mem_type_u "typ_uinfo_t(TYPE('a))"
by (rule typ_uinfo_t_mem_type)
end
lemma field_names_u_composeI:
assumes wf_t: "wf_desc t"
assumes path1: "path1 ∈ set (field_names_u t u)"
assumes path2: "path2 ∈ set (field_names_u u v)"
shows "path1 @ path2 ∈ set (field_names_u t v)"
proof -
from path1 wf_t obtain n where fl1: "field_lookup t path1 0 = Some (u, n)"
using field_names_u_filter_all_field_names_conv(1) by fastforce
with wf_t have wf_u: "wf_desc u"
using field_lookup_wf_desc_pres(1) by blast
from path2 wf_u obtain m where "field_lookup u path2 0 = Some (v, m)"
using field_names_u_filter_all_field_names_conv(1) by fastforce
hence fl2: "field_lookup u path2 n = Some (v, n + m)"
by (simp add: field_lookup_offset)
from field_lookup_prefix_Some''(1)[rule_format, OF fl1 wf_t, of path2] fl2
have "field_lookup t (path1 @ path2) 0 = Some (v, n + m)" by simp
then
show ?thesis
by (simp add: field_lookup_all_field_names(1) field_names_u_filter_all_field_names_conv(1) wf_t)
qed
lemma field_names_u_composeD:
assumes wf_t: "wf_desc t"
assumes append: "path1 @ path2 ∈ set (field_names_u t v)"
shows "∃u. path1 ∈ set (field_names_u t u) ∧ path2 ∈ set (field_names_u u v)"
proof -
from append wf_t obtain n where fl1: "field_lookup t (path1 @ path2) 0 = Some (v, n)"
using field_names_u_filter_all_field_names_conv(1) by fastforce
from fl1
obtain u m where
path1: "field_lookup t path1 0 = Some (u, m)" and path2: "field_lookup u path2 m = Some (v, n)"
using field_lookup_append_Some wf_t by blast
thus ?thesis
by (smt (verit, ccfv_threshold) all_field_names_exists_field_names_u(1)
field_lookup_all_field_names(1) field_names_u_composeI field_names_u_filter_all_field_names_conv(1)
local.fl1 mem_Collect_eq option.inject prod.inject set_filter wf_t)
qed
lemma field_names_u_field_offset_untyped_append:
assumes "wf_desc root"
assumes path1: "path1 ∈ set (field_names_u root outer)"
assumes path2: "path2 ∈ set (field_names_u outer inner)"
shows "field_offset_untyped root (path1 @ path2) = field_offset_untyped root path1 + field_offset_untyped outer path2"
by (smt (verit, ccfv_threshold) assms(1) field_lookup_offset field_lookup_prefix_Some''(1)
field_lookup_wf_desc_pres(1) field_names_u_filter_all_field_names_conv(1) field_offset_untyped_def
mem_Collect_eq option.sel path1 path2 prod.sel(2) set_filter)
lemma root_ptr_valid_u_cases:
assumes "root_ptr_valid_u t1 d a1"
assumes "root_ptr_valid_u t2 d a2"
shows "(t1 = t2 ∧ a1 = a2) ∨ ({a1 ..+ size_td t1} ∩ {a2 ..+ size_td t2} = {})"
apply (rule valid_root_footprints_cases )
using assms
by (auto simp add: root_ptr_valid_u_def )
lemma field_offset_untyped_empty[simp]: "field_offset_untyped t [] = 0"
by (simp add: field_offset_untyped_def)
lemma field_names_u_refl[simp]: "field_names_u t t = [[]]"
by (cases t) auto
lemma field_names_u_size_td_bounds:
assumes wf_t: "wf_desc t"
assumes path: "path ∈ set (field_names_u t u)"
shows "field_offset_untyped t path + size_td u ≤ size_td t"
proof -
from wf_t path obtain n where fl: "field_lookup t path 0 = Some (u, n)"
using field_names_u_filter_all_field_names_conv(1) by auto
hence n: "field_offset_untyped t path = n"
by (simp add: field_offset_untyped_def)
from field_lookup_offset_size' [OF fl] n
show ?thesis by simp
qed
lemma field_lookup_path_cases:
assumes fl1: "field_lookup t path 0 = Some (u, n)"
shows "(t = u ∧ path = []) ∨ ((t ≠ u) ∧ path ≠ [])"
using field_lookup_same_type_empty(1) local.fl1 by blast
lemma field_lookup_cycle_cases:
assumes fl1: "field_lookup t path1 0 = Some (u, n1)"
assumes fl2: "field_lookup u path2 0 = Some (v, n2)"
shows "(t = v ∧ u = v ∧ path1 = [] ∧ path2 = [] ∧ n1 = 0 ∧ n2 = 0) ∨
(t ≠ v)"
using field_lookup_path_cases [OF fl1] field_lookup_path_cases [OF fl2] fl1 fl2
by (metis add.right_neutral diff_add_0 nat_less_le ordered_cancel_comm_monoid_diff_class.add_diff_inverse
td_set_field_lookupD td_set_size_lte'(1))
lemma field_lookup_refl_iff: "field_lookup t p n = Some (t, m) ⟷ p = [] ∧ n = m"
proof
assume fl: "field_lookup t p n = Some (t, m)"
note CTypes.field_lookup_offset2[OF this]
from field_lookup_cycle_cases[OF this this] fl show "p = [] ∧ n = m"
by auto
qed auto
lemma :
assumes valid_root_x: "valid_root_footprint d x t"
assumes valid_y: "valid_footprint d y s"
assumes contained: "{y ..+ size_td s} ⊆ {x ..+ size_td t}"
shows "s ≤ t"
proof -
from valid_y have "0 < size_td s" by (simp add: valid_footprint_def Let_def)
hence "{y ..+ size_td s} ≠ {}"
by (simp add: intvl_non_zero_non_empty)
with contained have "{x ..+ size_td t} ∩ {y ..+ size_td s} ≠ {}" by blast
from valid_root_footprint_overlap_sub_typ [OF valid_root_x valid_y this]
show ?thesis.
qed
lemma c_null_guard_u_no_overlow: "c_null_guard_u t a ⟹ unat a + size_td t ≤ addr_card"
unfolding c_null_guard_u_def addr_card_def
using zero_not_in_intvl_no_overflow
by (metis card_word)
lemma c_null_guard_u_size_td_limit: "c_null_guard_u t a ⟹ size_td t < addr_card"
unfolding c_null_guard_u_def addr_card_def
by (metis (no_types, lifting) Abs_fnat_hom_0 add_diff_cancel_right' add_leE cancel_comm_monoid_add_class.diff_cancel
card_word first_in_intvl linorder_not_less nat_less_le unat_eq_of_nat zero_less_card_finite zero_not_in_intvl_no_overflow)
lemma c_null_guard_u_intvl_nat_conv:
assumes c_null_guard: "c_null_guard_u t a"
shows "{a ..+ size_td t} = {x. (unat a ≤ unat x ∧ unat x < (unat a + size_td t))}"
using intvl_no_overflow_nat_conv [OF c_null_guard_u_no_overlow [OF c_null_guard]] by simp
lemma :
assumes valid_x: "valid_footprint d x t"
assumes valid_y: "valid_footprint d y s"
assumes overlap: "{x ..+ size_td t} ∩ {y ..+ size_td s} ≠ {}"
shows "s ≤ t ∨ t ≤ s"
by (meson field_of_sub order_less_imp_le overlap
valid_footprint_neq_disjoint valid_x valid_y)
lemma [consumes 3, case_names eq less1 less2]:
assumes valid_x: "valid_footprint d x t"
assumes valid_y: "valid_footprint d y s"
assumes overlap: "{x ..+ size_td t} ∩ {y ..+ size_td s} ≠ {}"
assumes eq: "s = t ⟹ P"
assumes less_s_t: "s < t ⟹ P"
assumes less_t_s: "t < s ⟹ P"
shows P
using valid_footprint_overlap_sub_typ [OF valid_x valid_y overlap] eq less_s_t less_t_s
by fastforce
lemma :
assumes valid_x: "valid_footprint d x t"
assumes valid_y: "valid_footprint d y s"
assumes contained: "{x ..+ size_td t} ⊆ {y ..+ size_td s}"
shows "s ≤ t ∨ t ≤ s"
by (metis intvl_non_zero_non_empty le_iff_inf contained valid_footprint_def
valid_footprint_overlap_sub_typ valid_x valid_y)
lemma :
assumes valid_x: "valid_footprint d x t"
assumes valid_y: "valid_footprint d y s"
assumes contained: "{x ..+ size_td t} ⊆ {y ..+ size_td s}"
assumes eq: "s = t ⟹ P"
assumes less_s_t: "s < t ⟹ P"
assumes less_t_s: "t < s ⟹ P"
shows P
using valid_footprint_contained_sub_typ [OF valid_x valid_y contained] eq less_s_t less_t_s
by fastforce
lemma all_field_names_field_lookup':
fixes t::"('a, 'b) typ_desc"
and st::"('a, 'b) typ_struct"
and ts::"('a, 'b) typ_tuple list"
and x::"('a, 'b) typ_tuple"
shows
"wf_desc t ⟹ f ∈ set (all_field_names t) ⟹ ∃u n. field_lookup t f 0 = Some (u, n)" and
"wf_desc_struct st ⟹ f ∈ set (all_field_names_struct st) ⟹ ∃u n. field_lookup_struct st f 0 = Some (u, n)" and
"wf_desc_list ts ⟹ f ∈ set (all_field_names_list ts) ⟹ ∃u n. field_lookup_list ts f 0 = Some (u, n)" and
"wf_desc_tuple x ⟹ f ∈ set (all_field_names_tuple x) ⟹ ∃u n. field_lookup_tuple x f 0 = Some (u, n)"
proof (induct t and st and ts and x arbitrary: f and f and f and f)
case (TypDesc nat typ_struct list)
then show ?case by auto
next
case (TypScalar nat1 nat2 a)
then show ?case by auto
next
case (TypAggregate list)
then show ?case by auto
next
case Nil_typ_desc
then show ?case by auto
next
case (Cons_typ_desc dt_tuple list)
then show ?case apply (cases dt_tuple)
apply (clarsimp split: option.splits simp add: all_field_names_list_conv)
by (metis field_lookup_list_offset_None not_Some_eq_tuple)
next
case (DTuple_typ_desc typ_desc list b)
then show ?case by auto
qed
lemma : "valid_footprint d a t ⟹ a ∈ {a ..+ size_td t}"
by (simp add: valid_footprint_def Let_def intvl_self)
lemma field_lookup_Some_field_names_u:
fixes t :: "typ_uinfo" and
st :: "typ_uinfo_struct" and
ts :: "typ_uinfo_tuple list" and
x :: "typ_uinfo_tuple"
shows
"field_lookup t f n = Some (s, m) ⟹ f ∈ set (field_names_u t s)"
"field_lookup_struct st f n = Some (s, m) ⟹ f ∈ set (field_names_struct_u st s)"
"field_lookup_list ts f n = Some (s, m) ⟹ f ∈ set (field_names_list_u ts s)"
"field_lookup_tuple x f n = Some (s, m) ⟹ f ∈ set (field_names_tuple_u x s)"
proof (induct t and st and ts and x arbitrary: f n m and f n m and f n m and f n m)
case (TypDesc nat typ_struct list)
then show ?case
apply clarsimp
by (metis TypDesc.prems field_lookup_same_type_empty(1))
next
case (TypScalar nat1 nat2 a)
then show ?case by auto
next
case (TypAggregate list)
then show ?case by auto
next
case Nil_typ_desc
then show ?case by auto
next
case (Cons_typ_desc dt_tuple list)
then show ?case
by (auto split: option.splits)
next
case (DTuple_typ_desc typ_desc list b)
then show ?case apply clarsimp
by (metis imageI list.exhaust_sel option.distinct(1))
qed
lemma field_lookup_non_prefix_disj':
assumes wf: "mem_type_u t"
assumes f: "field_lookup t f 0 = Some (tf, n)"
assumes g: "field_lookup t g 0 = Some (tg, m)"
assumes f_g: "disj_fn f g"
shows "disjnt {(of_nat n::addr) ..+ size_td tf} {of_nat m ..+ size_td tg}"
using mem_type_u.max_size[OF wf] f_g
using field_lookup_offset_size'[OF f]
using field_lookup_offset_size'[OF g]
using field_lookup_non_prefix_disj[OF wf[THEN mem_type_u.wf_desc] f g]
unfolding intvl_eq_of_nat_Ico_add
apply (subst disjnt_of_nat)
unfolding len_of_addr_card
by (auto simp add: disjnt_def disj_fn_def less_eq_list_def)
lemma sub_typ_stack_byte_u:
"t ≤ typ_uinfo_t (TYPE(stack_byte)) ⟹ t = typ_uinfo_t TYPE(stack_byte)"
by (simp add: sub_typ_def typ_uinfo_t_def typ_info_stack_byte typ_tag_le_def)
lemma root_ptr_valid_not_subtype_disjoint_u:
"⟦ root_ptr_valid d (p::'a::mem_type ptr);
cvalid_u t d q;
¬ t ≤ typ_uinfo_t TYPE('a) ⟧ ⟹
ptr_span p ∩ {q ..+ size_td t} = {}"
by (metis cvalid_u_def root_ptr_valid_valid_root_footprint size_of_fold
typ_uinfo_size valid_root_footprint_overlap_sub_typ)
lemma stack_allocs_disjoint_u:
assumes stack_alloc: "(p, d') ∈ stack_allocs n 𝒮 (TYPE('a::mem_type)) d"
assumes no_stack: "t ≠ typ_uinfo_t (TYPE(stack_byte))"
assumes typed: "cvalid_u t d q"
shows "{ptr_val p ..+ n * size_of TYPE('a)} ∩ {q ..+ size_td t} = {}"
proof -
from stack_alloc obtain
"typ_uinfo_t (TYPE('a)) ≠ typ_uinfo_t (TYPE(stack_byte))" and
stack_bytes: "∀a ∈ {ptr_val p ..+ n * size_of TYPE('a)}. root_ptr_valid d (PTR (stack_byte) a)"
by (cases rule: stack_allocs_cases) auto
from no_stack have no_sub_typ: "¬ t ≤ typ_uinfo_t (TYPE(stack_byte))" by (metis sub_typ_stack_byte_u)
{
fix a
assume a: "a ∈ {ptr_val p ..+ n * size_of TYPE('a)}"
have "a ∉ {q ..+ size_td t}"
proof -
from stack_bytes [rule_format, OF a] have "root_ptr_valid d (PTR (stack_byte) a)" .
from root_ptr_valid_not_subtype_disjoint_u [OF this typed no_sub_typ ] show ?thesis
by (simp add: disjoint_iff first_in_intvl)
qed
}
then show "{ptr_val p ..+ n * size_of TYPE('a)} ∩ {q ..+ size_td t} = {}"
by auto
qed
lemma fold_ptr_retyp_disjoint_u:
fixes p::"'a::mem_type ptr"
shows "⟦ cvalid_u t d q; {ptr_val p..+ n * size_of TYPE('a)} ∩ {q ..+ size_td t} = {} ⟧ ⟹
cvalid_u t (fold (λi. ptr_retyp (p +⇩p int i)) [0..<n] d) q"
apply(clarsimp simp: cvalid_u_def)
apply(erule fold_ptr_retyp_valid_footprint_disjoint)
apply(fastforce simp: size_of_def)
done
lemma fold_ptr_force_type_disjoint_u:
fixes p::"'a::mem_type ptr"
shows "⟦ cvalid_u t d q; {ptr_val p..+ n * size_of TYPE('a)} ∩ {q ..+ size_td t} = {} ⟧ ⟹
cvalid_u t (fold (λi. ptr_force_type (p +⇩p int i)) [0..<n] d) q"
apply(clarsimp simp: cvalid_u_def)
apply(erule fold_ptr_force_type_valid_footprint_disjoint)
apply(fastforce simp: size_of_def)
done
lemma fold_ptr_retyp_disjoint2_u:
fixes p::"'a::mem_type ptr"
assumes no_overflow: "0 ∉ {ptr_val p..+ n * size_of TYPE('a)}"
shows "⟦cvalid_u t (fold (λi. ptr_retyp (p +⇩p int i)) [0..<n] d) q;
{ptr_val p..+ n * size_of TYPE('a)} ∩ {q ..+ size_td t}= {} ⟧
⟹ cvalid_u t d q"
apply(clarsimp simp: cvalid_u_def)
apply(erule fold_ptr_retyp_valid_footprint_disjoint2 [OF no_overflow])
apply(simp add: size_of_def)
apply fast
done
lemma fold_ptr_force_type_disjoint2_u:
fixes p::"'a::mem_type ptr"
assumes no_overflow: "0 ∉ {ptr_val p..+ n * size_of TYPE('a)}"
shows "⟦cvalid_u t (fold (λi. ptr_force_type (p +⇩p int i)) [0..<n] d) q;
{ptr_val p..+ n * size_of TYPE('a)} ∩ {q ..+ size_td t}= {} ⟧
⟹ cvalid_u t d q"
apply(clarsimp simp: cvalid_u_def)
apply(erule fold_ptr_force_type_valid_footprint_disjoint2 [OF no_overflow])
apply(simp add: size_of_def)
apply fast
done
lemma fold_ptr_retyp_disjoint_iff_u:
fixes p::"'a::mem_type ptr"
assumes no_overflow: "0 ∉ {ptr_val p..+ n * size_of TYPE('a)}"
shows "{ptr_val p..+ n * size_of TYPE('a)} ∩ {q ..+ size_td t} = {}
⟹ cvalid_u t (fold (λi. ptr_retyp (p +⇩p int i)) [0..<n] d) q = cvalid_u t d q"
apply standard
apply (erule (1) fold_ptr_retyp_disjoint2_u [OF no_overflow])
apply (erule (1) fold_ptr_retyp_disjoint_u)
done
lemma fold_ptr_force_type_disjoint_iff_u:
fixes p::"'a::mem_type ptr"
assumes no_overflow: "0 ∉ {ptr_val p..+ n * size_of TYPE('a)}"
shows "{ptr_val p..+ n * size_of TYPE('a)} ∩ {q ..+ size_td t} = {}
⟹ cvalid_u t (fold (λi. ptr_force_type (p +⇩p int i)) [0..<n] d) q = cvalid_u t d q"
apply standard
apply (erule (1) fold_ptr_force_type_disjoint2_u [OF no_overflow])
apply (erule (1) fold_ptr_force_type_disjoint_u)
done
lemma stack_allocs_preserves_typing_u:
assumes stack_alloc: "(p, d') ∈ stack_allocs n 𝒮 (TYPE('a::mem_type)) d"
assumes no_stack: "t ≠ typ_uinfo_t (TYPE(stack_byte))"
assumes typed: "cvalid_u t d q"
shows "cvalid_u t d' q"
proof -
from stack_alloc obtain
d': "d' = fold (λi. ptr_force_type (p +⇩p int i)) [0..<n] d" and
no_overflow: "0 ∉ {ptr_val p ..+ n * size_of TYPE('a)}"
by (cases rule: stack_allocs_cases) auto
from stack_allocs_disjoint_u [OF stack_alloc no_stack typed]
have "{ptr_val p..+n * size_of TYPE('a)} ∩ {q..+size_td t} = {}" .
from fold_ptr_force_type_disjoint_iff_u [OF no_overflow this, where d=d ] typed show ?thesis
by (simp add: d')
qed
lemma stack_allocs_root_ptr_valid_u_new_cases:
assumes stack_alloc: "(p, d') ∈ stack_allocs n 𝒮 (TYPE('a::mem_type)) d"
assumes valid: "root_ptr_valid_u t d' q"
shows "(∃i<n. q = ptr_val (p +⇩p int i) ∧ t = typ_uinfo_t (TYPE('a))) ∨ root_ptr_valid_u t d q"
proof (cases "{ptr_val p ..+ n * size_of TYPE('a)} ∩ {q ..+ size_td t} = {}")
case True
with stack_alloc valid show ?thesis
by (smt (verit) disjoint_iff fold_ptr_force_type_other intvlI root_ptr_valid_u_def
stack_allocs_cases valid_root_footprint_def)
next
case False
with stack_alloc array_to_index_span stack_alloc valid show ?thesis
by (smt (verit, ccfv_SIG) disjoint_iff root_ptr_valid_root_ptr_valid_u_conv
root_ptr_valid_u_cases size_of_tag stack_allocs_root_ptr_valid_same_type_cases)
qed
lemma cvalid_u_c_guard_u:
"cvalid_u t d a ⟹ c_guard_u t a"
by (simp add: cvalid_u_def)
lemma stack_allocs_preserves_root_ptr_valid_u:
assumes stack_alloc: "(p, d') ∈ stack_allocs n 𝒮 (TYPE('a::mem_type)) d"
assumes no_stack: "t ≠ typ_uinfo_t (TYPE(stack_byte))"
assumes typed: "root_ptr_valid_u t d q"
shows "root_ptr_valid_u t d' q"
proof -
from stack_alloc obtain
d': "d' = fold (λi. ptr_force_type (p +⇩p int i)) [0..<n] d" and
no_overflow: "0 ∉ {ptr_val p ..+ n * size_of TYPE('a)}"
by (cases rule: stack_allocs_cases) auto
from typed have typed_q: "cvalid_u t d q"
by (simp add: root_ptr_valid_u_cvalid_u)
from stack_allocs_disjoint_u [OF stack_alloc no_stack this]
have disj: "{ptr_val p..+n * size_of TYPE('a)} ∩ {q..+size_td t} = {}" .
from stack_allocs_preserves_typing_u [OF stack_alloc no_stack typed_q]
have typed': "cvalid_u t d' q " .
hence valid_fp: "valid_footprint d' q t"
by (simp add: cvalid_u_def)
show ?thesis
apply (simp add: root_ptr_valid_u_def valid_root_footprint_valid_footprint_dom_conv valid_fp
cvalid_u_c_guard_u [OF typed'])
apply (simp add: d')
using disj fold_ptr_force_type_other
by (smt (verit) d' disjoint_iff intvlI root_ptr_valid_u_def stack_alloc
stack_allocs_cases typed valid_root_footprint_dom_typing)
qed
lemma stack_allocs_root_ptr_valid_u_other:
assumes stack_alloc: "(p, d') ∈ stack_allocs n 𝒮 (TYPE('a::mem_type)) d"
assumes valid_d: "root_ptr_valid_u t d q"
assumes non_stack: "t ≠ typ_uinfo_t (TYPE(stack_byte))"
shows "root_ptr_valid_u t d' q"
proof (cases "root_ptr_valid_u t d' q")
case True
then show ?thesis by simp
next
case False
from stack_alloc
show ?thesis
apply (rule stack_allocs_cases)
using False valid_d non_stack
using stack_alloc stack_allocs_preserves_root_ptr_valid_u by blast
qed
lemma stack_allocs_root_ptr_valid_u_same:
assumes stack_alloc: "(p, d') ∈ stack_allocs n 𝒮 (TYPE('a::mem_type)) d"
assumes i: "i < n"
assumes addr_eq: "q = ptr_val (p +⇩p int i)"
assumes match: "t = typ_uinfo_t (TYPE('a))"
shows "root_ptr_valid_u t d' q"
proof (cases "root_ptr_valid_u t d' q")
case True
then show ?thesis by simp
next
case False
from stack_alloc have "root_ptr_valid d' (p +⇩p int i)"
apply (rule stack_allocs_cases)
using i
by auto
with addr_eq match show ?thesis
apply (clarsimp simp add: root_ptr_valid_def root_ptr_valid_u_def)
apply (simp add: c_guard_def c_guard_u_def c_null_guard_def c_null_guard_u_def
ptr_aligned_def ptr_aligned_u_def)
apply (auto simp add: align_of_def align_td_uinfo[symmetric] size_of_def )
done
qed
lemma stack_allocs_root_ptr_valid_u_cases:
assumes stack_alloc: "(p, d') ∈ stack_allocs n 𝒮 (TYPE('a::mem_type)) d"
assumes non_stack_byte: "t ≠ typ_uinfo_t (TYPE(stack_byte))"
shows "root_ptr_valid_u t d' q ⟷
(∃i<n. q = ptr_val (p +⇩p int i) ∧ t = typ_uinfo_t (TYPE('a))) ∨
root_ptr_valid_u t d q
"
using stack_alloc non_stack_byte
stack_allocs_root_ptr_valid_u_new_cases stack_allocs_root_ptr_valid_u_other
stack_allocs_root_ptr_valid_u_same
by metis
lemma stack_releases_root_ptr_valid_u1:
fixes p::"'a::mem_type ptr"
assumes non_stack_p: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes non_stack_q: "t ≠ typ_uinfo_t TYPE(stack_byte)"
assumes root_q: "root_ptr_valid_u t (stack_releases n p d) q"
shows "{ptr_val p ..+ n * size_of TYPE('a::mem_type)} ∩ {q ..+ size_td t} = {} ∧ root_ptr_valid_u t d q"
apply (rule context_conjI)
subgoal
using assms
by (smt (verit, best) cvalid_u_def disjoint_iff in_ptr_span_itself ptr_val.ptr_val_def
root_ptr_valid_u_cvalid_u size_of_tag stack_releases_valid_root_footprint sub_typ_stack_byte_u
valid_root_footprint_overlap_sub_typ)
subgoal
using assms
by (smt (verit, best) disjoint_iff intvlI root_ptr_valid_u_def stack_releases_other valid_root_footprint_def)
done
lemma stack_releases_root_ptr_valid_u2:
fixes p::"'a::mem_type ptr"
assumes disj: "{ptr_val p ..+ n * size_of TYPE('a::mem_type)} ∩ {q ..+ size_td t} = {}"
assumes valid_q: "root_ptr_valid_u t d q"
shows "root_ptr_valid_u t (stack_releases n p d) q"
using assms
by (simp add: intvlI orthD2 root_ptr_valid_u_def stack_releases_other valid_root_footprint_def)
lemma stack_release_root_ptr_valid_u2:
fixes p::"'a::mem_type ptr"
assumes disj: "ptr_span p ∩ {q ..+ size_td t} = {}"
assumes valid_q: "root_ptr_valid_u t d q"
shows "root_ptr_valid_u t (stack_release p d) q"
using assms
by (smt (verit, best) disjoint_iff intvlI root_ptr_valid_u_def stack_release_other valid_root_footprint_def)
lemma stack_releases_root_ptr_valid_u_cases:
fixes p::"'a::mem_type ptr"
assumes non_stack_p: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes non_stack_q: "t ≠ typ_uinfo_t TYPE(stack_byte)"
shows "root_ptr_valid_u t (stack_releases n p d) q ⟷
{ptr_val p ..+ n * size_of TYPE('a::mem_type)} ∩ {q ..+ size_td t} = {} ∧ root_ptr_valid_u t d q"
using assms stack_releases_root_ptr_valid_u1 stack_releases_root_ptr_valid_u2 by blast
lemma :
assumes wf: "wf_desc t"
assumes wf_size: "wf_size_desc t"
assumes f: "field_lookup t path 0 = Some (s, n)"
assumes footprint_t: "valid_footprint d a t"
assumes root_s: "valid_root_footprint d (a + of_nat n) s"
shows "(t = s ∧ path = [])"
proof (cases "path")
case Nil
with f have "t = s"
by simp
with Nil show ?thesis by simp
next
case (Cons fld path')
from f have neq: "t ≠ s"
using field_lookup_same_type_empty(1) local.Cons by blast
from f have s_t: "s ≤ t"
using td_set_field_lookupD typ_tag_le_def by blast
from neq s_t have "¬ t ≤ s"
using sub_tag_antisym by blast
with valid_root_footprint_overlap_sub_typ [OF root_s footprint_t]
have "{a + word_of_nat n..+size_td s} ∩ {a..+size_td t} = {}"
by blast
moreover
from f have td_set: "(s,n) ∈ td_set t 0"
using local.wf td_set_field_lookup by blast
from td_set_offset_size [OF td_set] have "{a + word_of_nat n..+size_td s} ⊆ {a..+size_td t}"
by (simp add: intvl_le)
moreover
from field_lookup_wf_size_desc_gt [OF f wf_size] have "0 < size_td s" .
hence "{a + word_of_nat n..+size_td s} ≠ {}"
by (simp add: intvl_non_zero_non_empty)
ultimately have False
by blast
then show ?thesis by simp
qed
corollary root_ptr_valid_u_is_root:
assumes wf: "wf_desc t"
assumes wf_size: "wf_size_desc t"
assumes f: "field_lookup t path 0 = Some (s, n)"
assumes cvalid_u_t: "cvalid_u t d a"
assumes root_s: "root_ptr_valid_u s d (a + of_nat n)"
shows "(t = s ∧ path = [])"
proof -
from cvalid_u_t have footprint_t: "valid_footprint d a t" by (simp add: cvalid_u_def)
from root_s have "valid_root_footprint d (a + of_nat n) s" by (simp add: root_ptr_valid_u_def)
from valid_root_footprint_is_root [OF wf wf_size f footprint_t this] show ?thesis .
qed
lemma :
assumes wf: "wf_desc t"
assumes wf_size_desc: "wf_size_desc t"
assumes valid_t: "valid_footprint d a t"
assumes fl: "field_lookup t path1 0 = Some (s, n)"
shows "valid_footprint d (a + word_of_nat n) s"
using valid_t fl wf_size_desc
apply (clarsimp simp add: valid_footprint_def Let_def, intro conjI)
subgoal using field_lookup_wf_size_desc_gt by blast
subgoal by (smt (verit, ccfv_SIG) Abs_fnat_hom_add add.commute add_less_mono1 field_lookup_offset_size'
group_cancel.add2 map_list_map_trans order_less_le_trans td_set_field_lookupD typ_slice_td_set)
done
lemma in_set_mapD:"x ∈ set (map f xs) ⟹ ∃y ∈ set xs. x = f y "
by (induct xs) auto
lemma findSomeI: "x ∈ set xs ⟹ P x ⟹ ∃x. find P xs = Some x"
by (induct xs) auto
lemma find_in_set_inj_distinct:
"inj_on P (set (map fst xs)) ⟹ (x, v) ∈ set xs ⟹ P x ⟹ distinct (map fst xs) ⟹
find (λ(x, _). P x) xs = Some (x, v)"
by (induct xs) (auto simp add: injD rev_image_eqI)
definition "inj_on_true P A = (∀x y. x ∈ A ⟶ y ∈ A ⟶ P x ⟶ P y ⟶ x = y)"
lemma "inj_on P A ⟹ inj_on_true P A"
by (auto simp add: inj_on_def inj_on_true_def)
lemma inj_on_trueD: "inj_on_true P A ⟹ x ∈ A ⟹ y ∈ A ⟹ P x ⟹ P y ⟹ x = y"
by (simp add: inj_on_true_def)
lemma inj_on_trueI: "(⋀x y. x ∈ A ⟹ y ∈ A ⟹ P x ⟹ P y ⟹ x = y) ⟹ inj_on_true P A"
by (simp add: inj_on_true_def)
lemma inj_on_true_mono: "A ⊆ B ⟹ inj_on_true P B ⟹ inj_on_true P A"
by (auto simp add: inj_on_true_def)
lemma find_in_set_inj_on_true_distinct:
"inj_on_true P (set (map fst xs)) ⟹ (x, v) ∈ set xs ⟹ P x ⟹ distinct (map fst xs) ⟹
find (λ(x, _). P x) xs = Some (x, v)"
apply (induct xs)
apply simp
apply simp
by (smt (verit, best) case_prod_beta' fst_conv image_iff inj_on_true_def insertCI)
lemma find_in_set_inj_on_true_distinct':
"inj_on_true P (set xs) ⟹ x ∈ set xs ⟹ P x ⟹ distinct xs ⟹
find (λx. P x) xs = Some x"
apply (induct xs)
apply simp
apply simp
by (metis inj_on_true_def insertCI)
lemma typ_tag_le_size_le: "t < (u::typ_uinfo) ⟹ size t < size u"
using td_set_size_lte
by (metis typ_tag_le_def typ_tag_lt_def)
lemma c_null_guard_intvl_nat_conv:
fixes p::"'a::mem_type ptr"
assumes c_null_guard: "c_null_guard p"
shows "ptr_span p = {x. (unat (ptr_val p) ≤ unat x ∧ unat x < (unat (ptr_val p) + size_of TYPE('a)))}"
proof -
from c_null_guard
have "c_null_guard_u (typ_uinfo_t TYPE('a)) (ptr_val p)"
by (simp add: c_null_guard_c_null_guard_u_conv)
from c_null_guard_u_intvl_nat_conv [OF this]
show ?thesis
by (simp add: size_of_def)
qed
lemma c_null_guard_ptr_add:
fixes p::"'a::mem_type ptr"
assumes bound: "unat (ptr_val p) + Suc n * size_of TYPE('a) ≤ addr_card"
assumes not_null: "ptr_val p ≠ 0"
assumes le: "i ≤ n"
shows "c_null_guard (p +⇩p int i)"
proof -
from bound le have bound1: "unat (ptr_val p) + i * size_of TYPE('a) ≤ addr_card"
by (meson add_le_mono dual_order.eq_iff dual_order.trans le_SucI mult_le_cancel2)
from bound le have bound2: "unat (ptr_val p) + i * size_of TYPE('a) + size_of TYPE('a) ≤ addr_card"
by (smt (verit, ccfv_SIG) bound1 less_le_mult mult_strict_right_mono not_less_eq_eq of_nat_add of_nat_le_iff of_nat_mult)
show ?thesis
apply (clarsimp simp add: ptr_add_def c_null_guard_def intvl_def)
using bound1 bound2 not_null
by (smt (verit, del_insts) Abs_fnat_hom_add Abs_fnat_hom_mult add_eq_0_iff_both_eq_0 add_mono_thms_linordered_field(4) eq_imp_le le_Suc_ex len_of_addr_card trans_less_add1 unat_of_nat_len unsigned_0 word_unat.Rep_inverse')
qed
lemma ptr_add_disjoint_index:
fixes p::"'a::mem_type ptr"
assumes bound: "unat (ptr_val p) + Suc n * size_of TYPE('a) ≤ addr_card"
assumes le: "i < n"
assumes n: "c_null_guard (p +⇩p int n)"
assumes i: "c_null_guard (p +⇩p int i)"
shows "ptr_span (p +⇩p int n) ∩ ptr_span (p +⇩p int i) = {}"
proof -
from bound le have bound_i: "unat (ptr_val p) + Suc i * size_of TYPE('a) ≤ addr_card"
by (smt (verit, best) Suc_less_SucD add_le_cancel_left dual_order.strict_iff_not le_trans mult_less_cancel2 nat_le_linear)
from bound have bound1: "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card" by simp
from bound have bound2: "unat (ptr_val p) + n * size_of TYPE('a) + size_of TYPE('a) ≤ addr_card"
by simp
from bound_i have bound_i1: "unat (ptr_val p) + i * size_of TYPE('a) ≤ addr_card" by simp
from bound_i have bound_i2: "unat (ptr_val p) + i * size_of TYPE('a) + size_of TYPE('a) ≤ addr_card"
by simp
show ?thesis
apply (simp add: c_null_guard_intvl_nat_conv n i)
using le bound n i bound1 bound2 bound_i1 bound_i2
by (auto simp add: ptr_add_def)
(smt (verit) len_of_addr_card less_le_mult mult_strict_right_mono of_nat_add of_nat_inverse of_nat_le_iff of_nat_less_iff of_nat_mult word_unat.Rep_inverse)
qed
lemma ptr_add_disjoint_last:
fixes p::"'a::mem_type ptr"
assumes bound: "unat (ptr_val p) + Suc n * size_of TYPE('a) ≤ addr_card"
assumes not_null: "ptr_val p ≠ 0"
shows "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span (p +⇩p int n) = {}"
proof -
{
fix i assume i_bound: "i<n"
have "ptr_span (p +⇩p int i) ∩ ptr_span (p +⇩p int n) = {}"
proof -
from c_null_guard_ptr_add [OF bound not_null] i_bound obtain
"c_null_guard (p +⇩p int n)" and "c_null_guard (p +⇩p int i)" by auto
from ptr_add_disjoint_index [OF bound i_bound this]
show ?thesis by blast
qed
}
then show ?thesis
by (auto simp add: array_index_span_conv)
qed
lemma h_val_fold:
fixes p::"'a::mem_type ptr"
assumes bound: "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card"
assumes not_null: "ptr_val p ≠ 0"
assumes i_bound: "i < n"
shows"h_val ((fold (λi. heap_update (p +⇩p int i) v) [0..<n]) h) (p +⇩p int i) = v"
using bound i_bound
proof (induct n arbitrary: h i)
case 0
then show ?case by simp
next
case (Suc n)
from Suc.prems obtain i_bound: "i < Suc n" and bound: "unat (ptr_val p) + Suc n * size_of TYPE('a) ≤ addr_card" by blast
hence bound': "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card" by simp
show ?case
proof (cases "i = n")
case True
show ?thesis by (simp add: True)
next
case False
with i_bound have i_bound': "i < n" by simp
note hyp = Suc.hyps [OF bound' i_bound']
from c_null_guard_ptr_add [OF bound not_null, of n]
have null_guard_n: "c_null_guard (p +⇩p int n)" by simp
from c_null_guard_ptr_add [OF bound not_null, of i] i_bound'
have null_guard_i: "c_null_guard (p +⇩p int i)" by simp
from ptr_add_disjoint_index [OF bound i_bound' null_guard_n null_guard_i]
have disj: "ptr_span (p +⇩p int n) ∩ ptr_span (p +⇩p int i) = {}" .
show ?thesis
by (simp add: h_val_update_regions_disjoint [OF disj] hyp)
qed
qed
lemma h_val_fold_disjoint:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes disj: "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span q = {}"
shows "h_val (fold (λi. heap_update (p +⇩p int i) (v i)) [0..<n] h) q =
h_val h q"
using disj
proof (induct n arbitrary: h)
case 0
then show ?case by simp
next
case (Suc n)
from Suc.prems have disj: "{ptr_val p..+Suc n * size_of TYPE('a)} ∩ ptr_span q = {}" .
from disj have disj': "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span q = {}"
by (smt (verit, best) first_in_intvl intvlD intvlI intvl_inter le_add2 mult_Suc order_less_le_trans orthD2 sz_nzero)
have "ptr_span (p +⇩p int n) ⊆{ptr_val p..+Suc n * size_of TYPE('a)}"
by (metis (no_types, lifting) CTypesDefs.ptr_add_def intvl_le mult_Suc nat_le_linear
of_int_of_nat_eq of_nat_mult ptr_val.simps)
with disj have disj_n: "ptr_span (p +⇩p int n) ∩ ptr_span q = {}"
using intvl_le by fastforce
note hyp = Suc.hyps [OF disj']
show ?case by (simp add: h_val_update_regions_disjoint [OF disj_n] hyp)
qed
lemma h_val_fold_zero_disjoint:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes disj: "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span q = {}"
shows "h_val (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n] h) q =
h_val h q"
using disj
by (rule h_val_fold_disjoint)
lemma fold_heap_update_commute:
fixes p::"'a:: mem_type ptr"
fixes q::"'b:: mem_type ptr"
assumes disjoint: "{ptr_val p ..+ n * size_of TYPE('a)} ∩ ptr_span q = {} "
shows "fold (λi. heap_update (p +⇩p int i) (v i)) [0..<n] (heap_update q x h) =
(heap_update q x) (fold (λi. heap_update (p +⇩p int i) (v i)) [0..<n] h)"
using disjoint
proof (induct n arbitrary: h)
case 0
then show ?case by simp
next
case (Suc n)
from Suc.prems have disj: "{ptr_val p..+Suc n * size_of TYPE('a)} ∩ ptr_span q = {}" .
from disj have disj': "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span q = {}"
by (smt (verit, best) first_in_intvl intvlD intvlI intvl_inter le_add2 mult_Suc order_less_le_trans orthD2 sz_nzero)
have "ptr_span (p +⇩p int n) ⊆{ptr_val p..+Suc n * size_of TYPE('a)}"
by (metis (no_types, lifting) CTypesDefs.ptr_add_def intvl_le mult_Suc nat_le_linear
of_int_of_nat_eq of_nat_mult ptr_val.simps)
with disj have disj_n: "ptr_span (p +⇩p int n) ∩ ptr_span q = {}"
using intvl_le by fastforce
note hyp = Suc.hyps [OF disj']
note commute = heap_update_commute [OF disj_n, simplified]
show ?case apply simp
by (simp add: hyp commute)
qed
lemma fold_heap_update_padding_commute:
fixes p::"'a:: mem_type ptr"
fixes q::"'b:: mem_type ptr"
assumes disjoint: "{ptr_val p ..+ n * size_of TYPE('a)} ∩ ptr_span q = {} "
assumes lbs: "⋀i. i < n ⟹ length (bs i) = size_of TYPE('a)"
assumes lbs': "length bs' = size_of TYPE('b)"
shows "fold (λi. heap_update_padding (p +⇩p int i) (v i) (bs i)) [0..<n] (heap_update_padding q x bs' h) =
(heap_update_padding q x bs') (fold (λi. heap_update_padding (p +⇩p int i) (v i) (bs i)) [0..<n] h)"
using disjoint lbs
proof (induct n arbitrary: h bs)
case 0
then show ?case by simp
next
case (Suc n)
from Suc.prems obtain disj: "{ptr_val p..+Suc n * size_of TYPE('a)} ∩ ptr_span q = {}" and
lbs_n: "⋀i. i < n ⟹ length (bs i) = size_of TYPE('a)" and lbs_n': "length (bs n) = size_of TYPE('a)"
by auto
from disj have disj': "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span q = {}"
by (smt (verit, best) first_in_intvl intvlD intvlI intvl_inter le_add2 mult_Suc order_less_le_trans orthD2 sz_nzero)
have "ptr_span (p +⇩p int n) ⊆{ptr_val p..+Suc n * size_of TYPE('a)}"
by (metis (no_types, lifting) CTypesDefs.ptr_add_def intvl_le mult_Suc nat_le_linear
of_int_of_nat_eq of_nat_mult ptr_val.simps)
with disj have disj_n: "ptr_span (p +⇩p int n) ∩ ptr_span q = {}"
using intvl_le by fastforce
note hyp = Suc.hyps [OF disj' lbs_n]
note commute = heap_update_padding_commute [OF disj_n lbs_n' lbs', simplified]
show ?case
apply simp
apply (simp add: hyp commute )
done
qed
lemma fold_heap_update_padding_heap_update_commute:
fixes p::"'a:: mem_type ptr"
fixes q::"'b:: mem_type ptr"
assumes disjoint: "{ptr_val p ..+ n * size_of TYPE('a)} ∩ ptr_span q = {} "
assumes lbs: "⋀i. i < n ⟹ length (bs i) = size_of TYPE('a)"
shows "fold (λi. heap_update_padding (p +⇩p int i) (v i) (bs i)) [0..<n] (heap_update q x h) =
(heap_update q x) (fold (λi. heap_update_padding (p +⇩p int i) (v i) (bs i)) [0..<n] h)"
using disjoint lbs
proof (induct n arbitrary: h bs)
case 0
then show ?case by simp
next
case (Suc n)
from Suc.prems obtain disj: "{ptr_val p..+Suc n * size_of TYPE('a)} ∩ ptr_span q = {}" and
lbs_n: "⋀i. i < n ⟹ length (bs i) = size_of TYPE('a)" and lbs_n': "length (bs n) = size_of TYPE('a)"
by auto
from disj have disj': "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span q = {}"
by (smt (verit, best) first_in_intvl intvlD intvlI intvl_inter le_add2 mult_Suc order_less_le_trans orthD2 sz_nzero)
have "ptr_span (p +⇩p int n) ⊆{ptr_val p..+Suc n * size_of TYPE('a)}"
by (metis (no_types, lifting) CTypesDefs.ptr_add_def intvl_le mult_Suc nat_le_linear
of_int_of_nat_eq of_nat_mult ptr_val.simps)
with disj have disj_n: "ptr_span (p +⇩p int n) ∩ ptr_span q = {}"
using intvl_le by fastforce
note hyp = Suc.hyps [OF disj' lbs_n]
note commute = heap_update_padding_heap_update_commute [OF disj_n lbs_n' , simplified]
show ?case
apply simp
apply (simp add: hyp commute )
done
qed
lemma fold_heap_update_collapse:
fixes p::"'a::xmem_type ptr"
assumes bound: "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card"
assumes not_null: "ptr_val p ≠ 0"
shows "fold (λi. heap_update (p +⇩p int i) (v i)) [0..<n]
((fold (λi. heap_update (p +⇩p int i) (w i)) [0..<n]) h) =
fold (λi. heap_update (p +⇩p int i) (v i)) [0..<n] h"
using bound
proof (induct n arbitrary: h)
case 0
then show ?case by simp
next
case (Suc n)
from Suc.prems obtain bound: "unat (ptr_val p) + Suc n * size_of TYPE('a) ≤ addr_card" by blast
hence bound': "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card" by simp
from ptr_add_disjoint_last [OF bound not_null]
have disj: "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span (p +⇩p int n) = {}" .
show ?case
apply simp
apply (subst (2) Suc.hyps [OF bound', symmetric])
apply (subst fold_heap_update_commute [OF disj])
apply (simp add: heap_update_collapse)
done
qed
lemma fold_heap_update_padding_collapse:
fixes p::"'a::xmem_type ptr"
assumes bound: "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card"
assumes not_null: "ptr_val p ≠ 0"
assumes lbs: "⋀i. i < n ⟹ length (bs i) = size_of TYPE('a)"
assumes lbs': "⋀i. i < n ⟹ length (bs' i) = size_of TYPE('a)"
shows "fold (λi. heap_update_padding (p +⇩p int i) (v i) (bs i)) [0..<n]
((fold (λi. heap_update_padding (p +⇩p int i) (w i) (bs' i)) [0..<n]) h) =
fold (λi. heap_update_padding (p +⇩p int i) (v i) (bs i)) [0..<n] h"
using bound lbs lbs'
proof (induct n arbitrary: h bs bs')
case 0
then show ?case by simp
next
case (Suc n)
from Suc.prems obtain
bound: "unat (ptr_val p) + Suc n * size_of TYPE('a) ≤ addr_card" and
lbs_n: "⋀i. i < n ⟹ length (bs i) = size_of TYPE('a)" and
lbs'_n: "⋀i. i < n ⟹ length (bs' i) = size_of TYPE('a)" and
lbs'_n': "length (bs' n) = size_of TYPE('a)" and
lbs_n': "length (bs n) = size_of TYPE('a)"
by auto
hence bound': "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card" by simp
from ptr_add_disjoint_last [OF bound not_null]
have disj: "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span (p +⇩p int n) = {}" .
show ?case
apply simp
apply (subst (2) Suc.hyps [OF bound' lbs_n lbs'_n, symmetric])
apply (assumption)
apply assumption
apply (subst fold_heap_update_padding_commute [OF disj lbs_n lbs'_n'])
apply (assumption)
apply (simp add: heap_update_padding_collapse [OF lbs_n' lbs'_n'])
done
qed
lemma fold_heap_update_padding_heap_update_collapse:
fixes p::"'a::xmem_type ptr"
assumes bound: "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card"
assumes not_null: "ptr_val p ≠ 0"
assumes lbs: "⋀i. i < n ⟹ length (bs i) = size_of TYPE('a)"
shows "fold (λi. heap_update_padding (p +⇩p int i) (v i) (bs i)) [0..<n]
((fold (λi. heap_update (p +⇩p int i) (w i) ) [0..<n]) h) =
fold (λi. heap_update_padding (p +⇩p int i) (v i) (bs i)) [0..<n] h"
using bound lbs
proof (induct n arbitrary: h bs )
case 0
then show ?case by simp
next
case (Suc n)
from Suc.prems obtain
bound: "unat (ptr_val p) + Suc n * size_of TYPE('a) ≤ addr_card" and
lbs_n: "⋀i. i < n ⟹ length (bs i) = size_of TYPE('a)" and
lbs_n': "length (bs n) = size_of TYPE('a)"
by auto
hence bound': "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card" by simp
from ptr_add_disjoint_last [OF bound not_null]
have disj: "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span (p +⇩p int n) = {}" .
show ?case
apply simp
apply (subst (2) Suc.hyps [OF bound' lbs_n , symmetric])
apply (assumption)
apply (subst fold_heap_update_padding_heap_update_commute [OF disj lbs_n ])
apply (assumption)
thm heap_update_padding_heap_update_collapse
apply (simp add: heap_update_padding_heap_update_collapse [OF lbs_n'])
done
qed
section "Open Types"
named_theorems 𝒯_def and
ptr_valid_definition and fold_ptr_valid and ptr_valid and ptr_valid_u_recursion and
addressable_ptr_valid_field and plift_simps and stack_the_default_plift and
plift_heap_update_padding_heap_update_conv and
plift_heap_update_list_stack_byte
lemma list_ex_array_fields[simp]:
"list_ex P (array_fields m) ⟷ (∃n<m. P [replicate n CHR ''1''])"
by (simp add: array_fields_def list_ex_iff Bex_def)
lemma list_all_field_lookup_array_fields[simp]:
"CARD('n) = m ⟹
list_all
(λf. ∃a b. field_lookup (typ_uinfo_t TYPE('a::c_type['n::finite])) f 0 = Some (a, b))
(array_fields m)"
by (simp add: array_fields_def)
lemma list_ex_subst_def:
"c ≡ xs ⟹ list_ex P c = list_ex P xs"
by simp
lemma ex_field_lookup_append:
"wf_desc t ⟹
field_lookup t p1 n1 = Some (u, m1) ⟹
field_lookup u p2 n2 = Some (v, m2) ⟹
∃m. field_lookup t (p1 @ p2) n3 = Some (v, m)"
by (metis field_lookup_offset_shift' field_lookup_prefix_Some')
named_theorems addressable_field_exec
locale open_types =
fixes 𝒯:: "(typ_uinfo * qualified_field_name list) list"
assumes mem_type_u: "⋀t fs. (t, fs) ∈ set 𝒯 ⟹ mem_type_u t"
assumes wf_𝒯':
"list_all (λ(t, fs).
[] ∉ set fs ∧
list_all (λf. field_lookup t f 0 ≠ None) fs ∧
distinct_prop disj_fn fs) 𝒯"
assumes distinct_𝒯: "distinct (map fst 𝒯)"
begin
inductive addressable_field :: "typ_uinfo ⇒ qualified_field_name ⇒ typ_uinfo ⇒ bool" where
addressable_field_refl[intro!, simp]: "⋀t. addressable_field t [] t"
| addressable_field_step: "⋀t fs p p' u v n.
map_of 𝒯 t = Some fs ⟹ p ∈ set fs ⟹ field_lookup t p 0 = Some (u, n) ⟹
addressable_field u p' v ⟹ addressable_field t (p @ p') v"
inductive ptr_valid_u :: "typ_uinfo ⇒ heap_typ_desc ⇒ addr ⇒ bool" for t d where
"⋀r p a. root_ptr_valid_u r d a ⟹ addressable_field r p t ⟹
ptr_valid_u t d (a + of_nat (field_offset_untyped r p))"
definition ptr_valid :: "heap_typ_desc ⇒ 'a::mem_type ptr ⇒ bool" where
[ptr_valid_definition]:
"ptr_valid d p ≡ ptr_valid_u (typ_uinfo_t TYPE('a)) d (ptr_val p)"
lemma addressable_field_single:
"map_of 𝒯 t = Some fs ⟹ p ∈ set fs ⟹ field_lookup t p 0 = Some (v, n) ⟹
addressable_field t p v"
using addressable_field_step[of t fs p v n "[]"] by auto
lemma addressable_field_append:
assumes *: "addressable_field t p1 u" "addressable_field u p2 v"
shows "addressable_field t (p1 @ p2) v"
proof (use * in ‹induction arbitrary: p2 v›)
case *: (addressable_field_step t fs p p' u v n w p1)
show ?case
unfolding append_assoc
apply (rule addressable_field_step[OF *(1,2,3)])
apply (rule *)+
done
qed simp
lemma addressable_field_rev_induct[consumes 1, case_names refl step]:
assumes *: "addressable_field t p u"
assumes 1: "⋀t. P t [] t"
assumes 2: "⋀t p' u fs f v n.
addressable_field t p' u ⟹ map_of 𝒯 u = Some fs ⟹ f ∈ set fs ⟹
field_lookup u f 0 = Some (v, n) ⟹ P t p' u ⟹ P t (p' @ f) v"
shows "P t p u"
proof -
have "addressable_field t p1 u ⟹ P t p1 u ⟹ P t (p1 @ p2) v"
if *: "addressable_field u p2 v" for t p1 u p2 v
proof (use * in ‹induction arbitrary: t p1›)
case *: (addressable_field_step t fs f q u v n w)
show ?case
unfolding append_assoc[symmetric]
by (intro "*.IH" 2[OF "*.prems"(1) "*"(1,2,3)] *)
(intro addressable_field_append[OF "*.prems"(1)]
addressable_field_single[OF *(1,2,3)])
qed simp
from this[OF * addressable_field_refl 1] show ?thesis by simp
qed
lemma addressable_field_rev_cases[consumes 1, case_names refl step]:
assumes *: "addressable_field t p u"
assumes 1: "t = u ⟹ p = [] ⟹ P"
assumes 2: "⋀p' fs f v n.
addressable_field t p' v ⟹ map_of 𝒯 v = Some fs ⟹ f ∈ set fs ⟹
field_lookup v f 0 = Some (u, n) ⟹ p = p' @ f ⟹ P"
shows P
using *
by (induction t==t p==p u==u rule: addressable_field_rev_induct)
(use 1 2 in auto)
lemma wf_𝒯: "map_of 𝒯 t = Some fs ⟹ list_all (λf. field_lookup t f 0 ≠ None) fs"
using wf_𝒯' by (auto simp: list_all_iff dest!: map_of_SomeD)
lemma 𝒯_not_nil: "map_of 𝒯 t = Some fs ⟹ [] ∉ set fs"
using wf_𝒯' by (auto simp: list_all_iff dest!: map_of_SomeD)
lemma addressable_field_refl_iff[simp]:
"addressable_field t [] u ⟷ t = u"
by (subst addressable_field.simps) (auto simp add: 𝒯_not_nil cong: HOL.conj_cong)
lemma addressable_field_domain:
"addressable_field t p u ⟹ t ∈ fst ` set 𝒯 ∨ (t = u ∧ p = [])"
apply (subst (asm) addressable_field.simps)
by (auto simp: image_iff split_paired_Ball dest!: map_of_SomeD) blast+
lemma addressable_fieldD_mem_type_u:
"addressable_field t p u ⟹ mem_type_u t ∨ (t = u ∧ p = [])"
by (auto dest!: addressable_field_domain mem_type_u)
lemma addressable_fieldD_field_lookup:
assumes p: "addressable_field t p u" shows "∃n. field_lookup t p 0 = Some (u, n)"
by (use p in induction)
(auto intro: ex_field_lookup_append mem_type_u mem_type_u.wf_desc dest: map_of_SomeD)
lemma addressable_field_same_iff[simp]:
"addressable_field t p t ⟷ p = []"
using addressable_fieldD_field_lookup[of t p t] field_lookup_same_type_empty(1)[of t p 0 t]
by auto
lemma addressable_fieldD_field_lookup':
"addressable_field t p u ⟹ field_lookup t p 0 = Some (u, field_offset_untyped t p)"
using addressable_fieldD_field_lookup[of t p u] by (auto simp add: field_offset_untyped_def)
lemma addressable_fieldD_field_ti:
assumes p: "addressable_field (typ_uinfo_t TYPE('a::c_type)) p t"
shows "∃u. field_ti TYPE('a) p = Some u ∧ export_uinfo u = t"
using field_lookup_uinfo_Some_rev[OF addressable_fieldD_field_lookup'[OF p]]
by (clarsimp simp: field_ti_def simp del: field_lookup_offset_untyped_eq)
lemma addressable_fieldD_field_names:
"addressable_field t p u ⟹ p ∈ set (field_names_u t u)"
by (auto dest: addressable_fieldD_field_lookup intro: field_lookup_Some_field_names_u(1))
lemma mem_type_u_addressable_field:
assumes *: "addressable_field t fs u"
shows "mem_type_u u ⟹ mem_type_u t"
by (use * in induction) (auto intro: mem_type_u dest!: map_of_SomeD)
lemma wf_desc_addressable_field:
assumes *: "addressable_field t fs u"
shows "wf_desc t ⟹ wf_desc u"
using addressable_fieldD_field_lookup'[OF *] by (auto intro: field_lookup_wf_desc_pres)
lemma wf_size_desc_addressable_field:
assumes *: "addressable_field t fs u"
shows "wf_size_desc t ⟹ wf_size_desc u"
using addressable_fieldD_field_lookup'[OF *] by (auto intro: field_lookup_wf_size_desc_pres)
lemma field_offset_append_of_addressable_field:
assumes p: "addressable_field t p u" and q: "addressable_field u q v"
shows "field_offset_untyped t (p @ q) = field_offset_untyped t p + field_offset_untyped u q"
proof -
have "p = [] ∧ q = [] ∨ mem_type_u t"
using addressable_fieldD_mem_type_u[OF p] addressable_fieldD_mem_type_u[OF q] by auto
then show ?thesis
proof (elim disjE conjE)
assume "mem_type_u t" then show ?thesis
by (intro field_names_u_field_offset_untyped_append[OF mem_type_u.wf_desc
addressable_fieldD_field_names[OF p] addressable_fieldD_field_names[OF q]])
qed simp
qed
lemma intvl_subset_of_addressable_field:
assumes p: "addressable_field t p u"
shows "{a + of_nat (field_offset_untyped t p) ..+ size_td u} ⊆ {a ..+ size_td t}"
using addressable_fieldD_field_lookup[OF p]
using intvl_subset_of_field_lookup[of t p u "field_offset_untyped t p" a]
by (auto simp: field_offset_untyped_def)
lemma root_ptr_valid_u_ptr_valid_u:
assumes a: "root_ptr_valid_u t d a" shows "ptr_valid_u t d a"
using ptr_valid_u.intros[OF a addressable_field_refl] by simp
lemma root_ptr_valid_ptr_valid: "root_ptr_valid d p ⟹ ptr_valid d p"
unfolding root_ptr_valid_root_ptr_valid_u_conv ptr_valid_def
by (rule root_ptr_valid_u_ptr_valid_u)
lemma fold_ptr_valid'[fold_ptr_valid]:
"ptr_valid_u (typ_uinfo_t TYPE('a::mem_type)) d x = ptr_valid d (PTR('a) x)"
by (simp add: ptr_valid_def)
lemma ptr_valid_u_trans:
assumes *: "ptr_valid_u t d a"
shows "addressable_field t p u ⟹ ptr_valid_u u d (a + of_nat (field_offset_untyped t p))"
proof (use * in induction)
case (1 r q a)
have eq:
"a + word_of_nat (field_offset_untyped r q) + word_of_nat (field_offset_untyped t p) =
a + word_of_nat (field_offset_untyped r (q @ p))"
using field_offset_append_of_addressable_field[OF 1(2,3)] by simp
show ?case unfolding eq
by (intro ptr_valid_u.intros 1 addressable_field_append[OF 1(2,3)])
qed
lemma ptr_valid_u_step:
assumes *: "map_of 𝒯 t = Some F" "f ∈ set F" "field_lookup t f 0 = Some (u, n)"
and a: "ptr_valid_u t d a"
shows "ptr_valid_u u d (a + of_nat (field_offset_untyped t f))"
by (rule ptr_valid_u_trans[OF a]) (rule addressable_field_single[OF *])
lemma ptr_valid_u_recursion'[ptr_valid_u_recursion]:
"ptr_valid_u t d a ⟷
root_ptr_valid_u t d a ∨
list_ex (λ(u, fs). list_ex (λf. ∃a' n. field_lookup u f 0 = Some (t, n) ∧
ptr_valid_u u d a' ∧ a = a' + of_nat (field_offset_untyped u f)) fs) 𝒯"
proof -
have
"root_ptr_valid_u t d
(a + word_of_nat (field_offset_untyped r p)) ∨
(∃x∈set 𝒯. case x of (u, fs) ⇒ ∃f∈set fs.
(∃n. field_lookup u f 0 = Some (t, n)) ∧
(∃a'. ptr_valid_u u d a' ∧
a + word_of_nat (field_offset_untyped r p) =
a' + word_of_nat (field_offset_untyped u f)))"
if p: "addressable_field r p t" and r: "root_ptr_valid_u r d a"
for a r p
proof (use p in ‹cases rule: addressable_field_rev_cases›)
case refl with r show ?thesis by simp
next
case *: (step p' fs p'' u m)
then have **: "(u, fs) ∈ set 𝒯"
by (auto simp: map_of_SomeD)
have "mem_type_u u"
using mem_type_u[of u fs] *(2) by (auto dest: map_of_SomeD)
with * have mem_r: "mem_type_u r"
by (auto dest: mem_type_u_addressable_field)
have u_t: "addressable_field u p'' t"
using *(2,3,4) by (rule addressable_field_single)
show ?thesis
apply (intro disjI2 bexI[of _ "(u, fs)"] **)
apply simp
apply (intro conjI bexI[of _ p''] * exI[of _ "a + of_nat (field_offset_untyped r p')"])
subgoal using *(4) by (rule exI)
subgoal using r *(1) by (rule ptr_valid_u.intros)
apply (simp add: field_offset_append_of_addressable_field[OF *(1) u_t] ‹p = p' @ p''›)
done
qed
moreover have
"ptr_valid_u t d
(a' + word_of_nat (field_offset_untyped r p) + word_of_nat (field_offset_untyped u f))"
if 1: "(u, fs) ∈ set 𝒯" and 2: "f ∈ set fs" "field_lookup u f 0 = Some (t, n)"
and r: "root_ptr_valid_u r d a'" "addressable_field r p u"
for u fs f n r p a'
proof -
have 1: "map_of 𝒯 u = Some fs"
using 1 by (simp add: map_of_eq_Some_iff[OF distinct_𝒯])
show ?thesis
using ptr_valid_u.intros[OF r] addressable_field_single[OF 1 2]
by (rule ptr_valid_u_trans)
qed
ultimately show ?thesis
by (auto simp: list_ex_iff del: disjCI
elim!: ptr_valid_u.cases intro: root_ptr_valid_u_ptr_valid_u)
qed
lemma 𝒯_distinct: "map_of 𝒯 t = Some fs ⟹ distinct_prop disj_fn fs"
using wf_𝒯' by (auto simp: list_all_iff dest!: map_of_SomeD)
lemma addressable_field_unique:
assumes t: "addressable_field r p t" shows "addressable_field r p t' ⟹ t = t'"
proof (use t in induction)
case 1: (addressable_field_step t fs p p' u v n)
from ‹addressable_field t (p @ p') t'› show ?case
proof cases
case 2: (addressable_field_step fs' q q' w m)
with 1 have "map_of 𝒯 t = Some fs" "p ∈ set fs" "q ∈ set fs" by auto
with 1 𝒯_distinct[of t fs] have "p = q ∨ disj_fn p q"
using pairwise_set_of_distinct_prop[of disj_fn, OF disj_fn_comm, of fs]
by (auto simp: pairwise_def)
with ‹p @ p' = q @ q'› have [simp]: "q = p ∧ q' = p'"
by (auto simp: disj_fn_def less_eq_list_def prefix_def append_eq_append_conv2)
with 1(3) 2(4) have "u = w"
by simp
with 1(5) ‹addressable_field w q' t'› show ?thesis
by simp
qed (use 1 in simp)
qed simp
lemma addressable_fields_split:
assumes r: "addressable_field r p t" "addressable_field r (p @ p') u"
shows "addressable_field t p' u"
proof (use r in induction)
case 1: (addressable_field_step t fs p0 p1 u v n)
from 1(6, 1-5) show ?case
proof cases
case 2: (addressable_field_step fs' q q' t' m)
with 1 have "map_of 𝒯 t = Some fs" "p0 ∈ set fs" "q ∈ set fs" by auto
with 1 𝒯_distinct[of t fs] have "p0 = q ∨ disj_fn p0 q"
using pairwise_set_of_distinct_prop[of disj_fn, OF disj_fn_comm, of fs]
by (auto simp: pairwise_def)
with 2(1) have "p0 = q ∧ p1 @ p' = q'"
by (auto simp: disj_fn_def less_eq_list_def prefix_def append_eq_append_conv2)
with 1 2 show ?thesis
by simp
qed simp
qed simp
lemma addressable_field_antisymm:
"addressable_field t p u ⟹ addressable_field u q t ⟹ u = t"
using addressable_field_append[of t p u q t] by simp
lemma addressable_field_sub_typ: "addressable_field t path u ⟹ u ≤ t"
using addressable_fieldD_field_lookup[of t path u] typ_tag_le_def
by (blast dest: td_set_field_lookupD)
lemma sub_typ_of_field_lookup:
"field_lookup (typ_uinfo_t TYPE('a)) p 0 = Some (typ_uinfo_t TYPE('b), n) ⟹
TYPE('b::mem_type) ≤⇩τ TYPE('a::mem_type)"
apply (clarsimp simp add: sub_typ_def)
apply (rule field_of_sub[of "of_nat n"])
using field_lookup_offset_size'[of "typ_uinfo_t TYPE('a)" p]
mem_type_class.u.max_size[where 'a='a]
by (auto simp add: field_of_def field_offset_def field_offset_untyped_def addr_card_len_of_conv
intro!: td_set_field_lookupD[of _ p] unat_of_nat_eq[symmetric])
lemma addressable_fields_imp_sub_typ:
"addressable_field (typ_uinfo_t TYPE('a)) p (typ_uinfo_t TYPE('b)) ⟹
TYPE('b::mem_type) ≤⇩τ TYPE('a::mem_type)"
by (simp add: addressable_field_sub_typ sub_typ_def)
lemma ptr_valid_u_cases:
assumes t: "mem_type_u t"
assumes t_a: "ptr_valid_u t d a"
assumes u_b: "ptr_valid_u u d b"
shows "disjnt {a..+size_td t} {b..+size_td u} ∨
(t = u ∧ a = b) ∨
(∃p. addressable_field t p u ∧ t ≠ u ∧ b = a + word_of_nat (field_offset_untyped t p)) ∨
(∃p. addressable_field u p t ∧ t ≠ u ∧ a = b + word_of_nat (field_offset_untyped u p))"
(is "?disj ∨ ?addr")
proof (rule disjCI2)
assume a_b: "¬ ?disj"
from t_a obtain r f0 x where x0: "root_ptr_valid_u r d x"
and a: "a = x + of_nat (field_offset_untyped r f0)"
and r_t: "addressable_field r f0 t"
by (auto elim!: ptr_valid_u.cases)
from u_b obtain r' f1 x' where x1: "root_ptr_valid_u r' d x'"
and b: "b = x' + of_nat (field_offset_untyped r' f1)"
and r_u: "addressable_field r' f1 u"
by (auto elim!: ptr_valid_u.cases)
from a_b have "¬ disjnt {x ..+ size_td r} {x' ..+ size_td r'}"
using intvl_subset_of_addressable_field[OF r_t, of x]
using intvl_subset_of_addressable_field[OF r_u, of x']
by (auto intro: disjnt_subset1 disjnt_subset2 simp: a b)
with root_ptr_valid_u_cases[OF x0 x1] have [simp]: "r' = r" "x' = x"
by (auto simp: disjnt_def)
have r: "mem_type_u r"
using r_t t by (rule mem_type_u_addressable_field)
then have wf_r: "wf_desc r"
by (rule mem_type_u.wf_desc)
have "¬ disjnt
{(word_of_nat (field_offset_untyped r f0)::addr)..+size_td t}
{word_of_nat (field_offset_untyped r f1)..+size_td u}"
using a_b by (simp add: a b)
with field_lookup_non_prefix_disj'[OF r
addressable_fieldD_field_lookup'[OF r_t]
addressable_fieldD_field_lookup'[of r f1 u]] r_u
obtain f' where "f0 = f1 @ f' ∨ f1 = f0 @ f'"
by (auto simp: disj_fn_def less_eq_list_def prefix_def)
then show ?addr
proof (elim disjE)
assume "f0 = f1 @ f'"
with r_t r_u addressable_fields_split[of r f1 u f' t]
show ?thesis
by (cases "u = t") (auto simp add: a b field_offset_append_of_addressable_field)
next
assume "f1 = f0 @ f'"
with r_t r_u addressable_fields_split[of r f0 t f' u]
show ?thesis
by (cases "u = t") (auto simp add: a b field_offset_append_of_addressable_field)
qed
qed
lemma ptr_valid_cases':
fixes p :: "'a::mem_type ptr"
fixes q :: "'b::mem_type ptr"
assumes p: "ptr_valid d p"
assumes q: "ptr_valid d q"
shows "disjnt (ptr_span p) (ptr_span q) ∨
(typ_uinfo_t TYPE('a) = typ_uinfo_t TYPE('b) ∧ ptr_val p = ptr_val q) ∨
(∃f. addressable_field (typ_uinfo_t TYPE('a)) f (typ_uinfo_t TYPE('b)) ∧
typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b) ∧
q = PTR('b) &(p → f)) ∨
(∃f. addressable_field (typ_uinfo_t TYPE('b)) f (typ_uinfo_t TYPE('a)) ∧
typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b) ∧
p = PTR('a) &(q → f))"
using ptr_valid_u_cases[OF _ p[unfolded ptr_valid_def] q[unfolded ptr_valid_def]]
by (simp add: size_of_def ptr_val_conv field_lvalue_def field_offset_def)
lemma ptr_valid_u_cases_weak:
assumes "mem_type_u t"
assumes "ptr_valid_u t d a"
assumes "ptr_valid_u u d b"
shows "disjnt {a..+size_td t} {b..+size_td u} ∨
(∃p. addressable_field t p u ∧ b = a + word_of_nat (field_offset_untyped t p)) ∨
(∃p. addressable_field u p t ∧ a = b + word_of_nat (field_offset_untyped u p))"
using ptr_valid_u_cases[OF assms] by (cases "t = u") auto
lemma ptr_valid_cases_weak:
fixes p :: "'a::mem_type ptr"
fixes q :: "'b::mem_type ptr"
assumes p: "ptr_valid d p"
assumes q: "ptr_valid d q"
shows "disjnt (ptr_span p) (ptr_span q) ∨
(∃f. addressable_field (typ_uinfo_t TYPE('a)) f (typ_uinfo_t TYPE('b)) ∧
q = PTR('b) &(p → f)) ∨
(∃f. addressable_field (typ_uinfo_t TYPE('b)) f (typ_uinfo_t TYPE('a)) ∧
p = PTR('a) &(q → f))"
using ptr_valid_cases'[OF assms]
by (cases "typ_uinfo_t TYPE('a) = typ_uinfo_t TYPE('b)")
(auto simp: ptr_val_conv field_lvalue_def)
lemma ptr_valid_u_cvalid_u:
assumes t: "mem_type_u t"
assumes ptr_valid: "ptr_valid_u t d a"
shows "cvalid_u t d a"
using ptr_valid
proof
fix r fs a' assume r_t: "addressable_field r fs t"
and a_eq: "a = a' + word_of_nat (field_offset_untyped r fs)"
and a': "root_ptr_valid_u r d a'"
have r: "mem_type_u r"
using mem_type_u_addressable_field[OF r_t t] .
have align_t: "2 ^ align_td t dvd size_td t"
using t by (rule mem_type_u.align_size)
show "cvalid_u t d a" unfolding a_eq
using r align_t addressable_fieldD_field_lookup'[OF r_t] root_ptr_valid_u_cvalid_u[OF a']
by (rule mem_type_u.cvalid_u_field_lookup)
qed
lemma ptr_valid_h_t_valid: "ptr_valid d p ⟹ d ⊨⇩t (p::'a::mem_type ptr)"
unfolding ptr_valid_def cvalid_cvalid_u_conv
by (rule ptr_valid_u_cvalid_u) simp_all
sublocale ptr_valid?: wf_ptr_valid ptr_valid
by unfold_locales (rule ptr_valid_h_t_valid)
lemma h_val_heap_update' [plift_simps]:
fixes p::"'a::mem_type ptr"
fixes q::"'a::mem_type ptr"
assumes ptr_valid_p: "ptr_valid d p"
assumes ptr_valid_q: "ptr_valid d q"
shows "h_val (heap_update p v h) q = ((h_val h)(p:=v)) q"
by (metis c_type_class.lift_def lift_heap_update ptr_valid_h_t_valid ptr_valid_p ptr_valid_q)
lemma h_val_heap_update_padding' [plift_simps]:
fixes p::"'a::mem_type ptr"
fixes q::"'a::mem_type ptr"
assumes ptr_valid_p: "ptr_valid d p"
assumes ptr_valid_q: "ptr_valid d q"
assumes lbs: "length bs = size_of TYPE('a)"
shows "h_val (heap_update_padding p v bs h) q = ((h_val h)(p:=v)) q"
by (smt (verit, best) fun_upd_apply_eq_cases h_val_heap_update_padding
h_val_heap_update_padding_disjoint lbs local.ptr_valid_h_t_valid ptr_valid_p ptr_valid_q
ptr_valid_same_type_cases)
lemmas ptr_valid_plift_Some_hval [plift_simps]
theorem disjoint_type_plift:
fixes p::"'a::mem_type ptr"
assumes unrelated1: "¬ TYPE('a) ≤⇩τ TYPE('b::mem_type)"
assumes unrelated2: "¬ TYPE('b) ≤⇩τ TYPE('a)"
assumes ptr_valid_p: "ptr_valid (hrs_htd h) p"
shows "plift ((hrs_mem_update (heap_update p v) h)) = (plift h::'b ptr ⇒ 'b option)"
proof -
from unrelated1 unrelated2 have disj: "typ_uinfo_t TYPE('a) ⊥⇩t typ_uinfo_t TYPE('b)"
using tag_disj_def unfolding sub_typ_def by blast
from ptr_valid_p have "hrs_htd h ⊨⇩t p"
by (simp add: ptr_valid_h_t_valid)
from clift_heap_update_same [OF this disj]
have "clift (hrs_mem_update (heap_update p v) h) = (clift h::'b ptr ⇒ 'b option) "
by simp
then show ?thesis
apply -
apply (rule ext)
by (metis hrs_htd_mem_update plift_None plift_clift_conv)
qed
theorem disjoint_type_update_h_val:
fixes p::"'a::mem_type ptr"
fixes q::"'b::mem_type ptr"
assumes unrelated1: "¬ TYPE('a) ≤⇩τ TYPE('b)"
assumes unrelated2: "¬ TYPE('b) ≤⇩τ TYPE('a)"
assumes typed_p: "hrs_htd h ⊨⇩t p"
assumes typed_q: "hrs_htd h ⊨⇩t q"
shows "h_val (hrs_mem (hrs_mem_update (heap_update p v) h)) q = h_val (hrs_mem h) q"
proof -
from unrelated1 unrelated2 have disj: "typ_uinfo_t TYPE('a) ⊥⇩t typ_uinfo_t TYPE('b)"
using tag_disj_def unfolding sub_typ_def by blast
from clift_heap_update_same [OF typed_p disj]
have "clift (hrs_mem_update (heap_update p v) h) q = clift h q"
by simp
with typed_p typed_q
show ?thesis
by (metis clift_Some_eq_valid h_val_clift hrs_mem_def prod.collapse)
qed
lemma intvl_Suc_0: "{x ..+ Suc 0} = {x}"
by (auto simp: intvl_def)
lemma ptr_span_subset_of_addressable_field:
fixes q:: "'a::mem_type ptr"
shows "addressable_field t p (typ_uinfo_t TYPE('a)) ⟹
ptr_val q = x + word_of_nat (field_offset_untyped t p) ⟹
ptr_span q ⊆ {x..+size_td t}"
using intvl_subset_of_addressable_field[of t p "typ_uinfo_t TYPE('a)" x]
by (simp flip: size_of_tag)
lemma addressable_field_wf_descD:
assumes path: "addressable_field t path u"
shows "t = u ∨ (wf_desc t ∧ wf_desc u)"
using addressable_fieldD_mem_type_u[OF path] wf_desc_addressable_field[OF path]
by (blast intro: mem_type_u.wf_desc)
lemma addressable_field_wf_size_descD:
assumes path: "addressable_field t path u"
shows "t = u ∨ (wf_size_desc t ∧ wf_size_desc u)"
using addressable_fieldD_mem_type_u[OF path] wf_size_desc_addressable_field[OF path]
by (blast intro: mem_type_u.wf_size_desc)
lemma root_ptr_valid_u_ptr_valid_u_cases:
fixes p q :: addr
assumes root_valid_p: "root_ptr_valid_u t d p"
assumes valid_q: "ptr_valid_u s d q"
shows "{p ..+ size_td t} ∩ {q ..+ size_td s} = {} ∨
(∃path. addressable_field t path s ∧ q = p + of_nat (field_offset_untyped t path))"
proof (cases "{p ..+ size_td t} ∩ {q ..+ size_td s} = {}")
case True
then show ?thesis by simp
next
case False
from valid_q
obtain root path x where
path: "addressable_field root path s" and
root_ptr_valid_u: "root_ptr_valid_u root d x" and
q: "q = x + word_of_nat (field_offset_untyped root path)"
by (clarsimp simp add: ptr_valid_def elim!: ptr_valid_u.cases)
then have contained: "{q ..+ size_td s} ⊆ {x..+size_td root}"
using intvl_subset_of_addressable_field[OF path] by (simp add: size_of_def)
from root_valid_p have root_ptr_valid_u_p: "root_ptr_valid_u t d p"
by (simp add: root_ptr_valid_root_ptr_valid_u_conv)
from root_ptr_valid_u_cases [OF root_ptr_valid_u_p root_ptr_valid_u] False contained
obtain "t = root" "p = x"
by (metis (no_types, lifting) disj_subset preorder_class.dual_order.refl)
with path q False show ?thesis
by auto
qed
lemma root_ptr_valid_u_ptr_valid_cases:
fixes p :: addr and q :: "'b::mem_type ptr"
assumes root_valid_p: "root_ptr_valid_u t d p"
assumes valid_q: "ptr_valid d q"
shows "{p ..+ size_td t} ∩ ptr_span q = {} ∨
(∃path. addressable_field t path (typ_uinfo_t TYPE('b)) ∧
ptr_val q = p + of_nat (field_offset_untyped t path))"
using root_ptr_valid_u_ptr_valid_u_cases[OF root_valid_p valid_q[unfolded ptr_valid_def]]
by (simp add: size_of_def)
lemma root_ptr_valid_ptr_valid_cases:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes root_valid_p: "root_ptr_valid d p"
assumes valid_q: "ptr_valid d q"
shows "ptr_span p ∩ ptr_span q = {} ∨
(∃path. addressable_field (typ_uinfo_t TYPE('a)) path (typ_uinfo_t TYPE('b)) ∧
q = PTR ('b) &(p→path))"
using root_ptr_valid_u_ptr_valid_cases[OF
root_valid_p[unfolded root_ptr_valid_root_ptr_valid_u_conv] valid_q]
by (simp add: size_of_def field_lvalue_def ptr_val_conv field_offset_def)
lemma stack_allocs_ptr_valid_cases1:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes alloc: "(p, d') ∈ stack_allocs n 𝒮 TYPE('a) d"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes valid_q: "ptr_valid d' q"
shows "((∃i path. i < n ∧
addressable_field (typ_uinfo_t TYPE('a)) path (typ_uinfo_t TYPE('b)) ∧
q = PTR ('b) &((p +⇩p int i)→path)) ∧ ¬ ptr_valid d q) ∨
(ptr_valid d q ∧ {ptr_val p ..+ n * size_of TYPE('a)} ∩ ptr_span q = {})"
proof -
from valid_q
obtain root path x where
path: "addressable_field root path (typ_uinfo_t TYPE('b))" and
root_ptr_valid_u: "root_ptr_valid_u root d' x" and
q: "ptr_val q = x + word_of_nat (field_offset_untyped root path)"
by (clarsimp simp add: ptr_valid_def elim!: ptr_valid_u.cases)
from path q_not_stack_byte have root_not_stack_byte: "root ≠ typ_uinfo_t TYPE(stack_byte)"
using addressable_field_sub_typ sub_typ_stack_byte_u by blast
from stack_allocs_root_ptr_valid_u_cases [OF alloc root_not_stack_byte] root_ptr_valid_u
consider i where "i<n" "x = ptr_val (p +⇩p int i)" "root = typ_uinfo_t TYPE('a)"
| "root_ptr_valid_u root d x" by auto
then show ?thesis
proof cases
case 1
have "ptr_span q ⊆ ptr_span (p +⇩p int i)"
using ptr_span_subset_of_addressable_field[OF path q] by (simp add: size_of_def 1)
also have "… ⊆ {ptr_val p..+n * size_of TYPE('a)}"
using alloc 1(1) by (rule stack_allocs_contained)
finally have "ptr_val q ∈ {ptr_val p..+n * size_of TYPE('a)}"
using mem_type_self by auto
then have root_q: "root_ptr_valid d (PTR_COERCE('b → stack_byte) q)"
using stack_allocs_cases[OF alloc] by (auto simp add: q 1 simp flip: Ptr_ptr_coerce)
have False if q': "ptr_valid d q"
using root_ptr_valid_ptr_valid_cases[OF root_q q'] q_not_stack_byte
by (auto simp add: intvl_Suc_0 dest!: addressable_field_sub_typ sub_typ_stack_byte_u)
then have "¬ ptr_valid d q" by auto
with 1 path show ?thesis
by (auto simp: ptr_val_conv q field_lvalue_def field_offset_def
intro!: exI[of _ i] exI[of _ path])
next
case 2
then have "ptr_valid d q"
by (auto simp add: ptr_valid_def q intro!: ptr_valid_u.intros path)
with stack_allocs_disjoint [OF alloc q_not_stack_byte ptr_valid_h_t_valid, of q]
show ?thesis by simp
qed
qed
lemma stack_allocs_ptr_valid_cases1' [consumes 3, case_names addressable_field disjoint]:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes alloc: "(p, d') ∈ stack_allocs n 𝒮 TYPE('a) d"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes valid_q: "ptr_valid d' q"
assumes addressable_field: "⋀i path. i < n ⟹
addressable_field (typ_uinfo_t TYPE('a)) path (typ_uinfo_t TYPE('b)) ⟹
q = PTR ('b) &((p +⇩p int i)→path) ⟹ ¬ ptr_valid d q ⟹ P"
assumes disjoint: "ptr_valid d q ⟹ {ptr_val p ..+ n * size_of TYPE('a)} ∩ ptr_span q = {} ⟹ P"
shows "P"
using stack_allocs_ptr_valid_cases1 [OF alloc q_not_stack_byte valid_q] addressable_field disjoint by blast
lemma stack_allocs_ptr_valid_cases2:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes alloc: "(p, d') ∈ stack_allocs n 𝒮 TYPE('a) d"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes valid_q: "ptr_valid d q"
shows "ptr_valid d' q"
proof -
from valid_q
obtain root path x where
path: "addressable_field root path (typ_uinfo_t TYPE('b))" and
root_ptr_valid_u: "root_ptr_valid_u root d x" and
x: "ptr_val q = x + word_of_nat (field_offset_untyped root path)"
by (clarsimp simp add: ptr_valid_def ptr_valid_u.simps)
from path q_not_stack_byte have root_not_stack_byte: "root ≠ typ_uinfo_t TYPE(stack_byte)"
using addressable_field_sub_typ sub_typ_stack_byte_u by blast
from stack_allocs_root_ptr_valid_u_other [OF alloc root_ptr_valid_u root_not_stack_byte]
have "root_ptr_valid_u root d' x" .
with path x
show "ptr_valid d' q"
using ptr_valid_def ptr_valid_u.simps by blast
qed
lemma stack_allocs_ptr_valid_cases3:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes alloc: "(p, d') ∈ stack_allocs n 𝒮 TYPE('a) d"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes i: "i < n"
assumes path: "addressable_field (typ_uinfo_t TYPE('a)) path (typ_uinfo_t TYPE('b))"
assumes q: "q = PTR ('b) &((p +⇩p int i)→path)"
shows "ptr_valid d' q"
apply (simp add: q ptr_valid_def field_lvalue_def field_offset_def)
apply (intro ptr_valid_u.intros[OF _ path])
apply (subst stack_allocs_root_ptr_valid_u_cases[OF alloc stack_allocs_no_stack_byte[OF alloc]])
apply (auto intro: i)
done
theorem stack_allocs_ptr_valid_cases:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes alloc: "(p, d') ∈ stack_allocs n 𝒮 TYPE('a) d"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
shows "ptr_valid d' q ⟷
(((∃i path. i < n ∧ addressable_field (typ_uinfo_t TYPE('a)) path (typ_uinfo_t TYPE('b)) ∧
q = PTR ('b) &((p +⇩p int i)→path)) ∧ ¬ ptr_valid d q) ∨
(ptr_valid d q ∧ {ptr_val p ..+ n * size_of TYPE('a)} ∩ ptr_span q = {}))"
using stack_allocs_ptr_valid_cases1 [OF alloc q_not_stack_byte]
stack_allocs_ptr_valid_cases2 [OF alloc q_not_stack_byte]
stack_allocs_ptr_valid_cases3 [OF alloc q_not_stack_byte]
by blast
lemma stack_releases_ptr_valid_cases1:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes p_not_stack_byte: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes valid_q: "ptr_valid (stack_releases n p d) q"
shows "{ptr_val p ..+ n * size_of TYPE('a::mem_type)} ∩ ptr_span q = {} ∧
ptr_valid d q"
proof -
from valid_q
obtain root path x where
path: "addressable_field root path (typ_uinfo_t TYPE('b))" and
root_ptr_valid_u: "root_ptr_valid_u root (stack_releases n p d) x" and
x: "ptr_val q = x + word_of_nat (field_offset_untyped root path)"
by (clarsimp simp add: ptr_valid_def ptr_valid_u.simps)
from path q_not_stack_byte have root_not_stack_byte: "root ≠ typ_uinfo_t TYPE(stack_byte)"
using addressable_field_sub_typ sub_typ_stack_byte_u by blast
from stack_releases_root_ptr_valid_u_cases [OF p_not_stack_byte root_not_stack_byte, of n p d x ] root_ptr_valid_u
obtain root_cases:
"{ptr_val p..+n * size_of TYPE('a)} ∩ {x..+size_td root} = {}"
"root_ptr_valid_u root d x" by auto
moreover
have "ptr_span q ⊆ {x..+size_td root}"
using path x by (rule ptr_span_subset_of_addressable_field)
moreover
from root_cases(2) path x have "ptr_valid d q"
using ptr_valid_def ptr_valid_u.simps by blast
ultimately
show ?thesis by blast
qed
lemma stack_releases_ptr_valid_cases2:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes p_not_stack_byte: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes root_p: "⋀i. i < n ⟹ root_ptr_valid d (p +⇩p int i)"
assumes disj: "{ptr_val p ..+ n * size_of TYPE('a::mem_type)} ∩ ptr_span q = {}"
assumes valid_q: "ptr_valid d q"
shows "ptr_valid (stack_releases n p d) q"
proof -
from valid_q
obtain root path x where
path: "addressable_field root path (typ_uinfo_t TYPE('b))" and
root_ptr_valid_u: "root_ptr_valid_u root d x" and
x: "ptr_val q = x + word_of_nat (field_offset_untyped root path)"
by (clarsimp simp add: ptr_valid_def ptr_valid_u.simps)
from path q_not_stack_byte have root_not_stack_byte: "root ≠ typ_uinfo_t TYPE(stack_byte)"
using addressable_field_sub_typ sub_typ_stack_byte_u by blast
have contained: "ptr_span q ⊆ {x..+size_td root}"
using path x by (rule ptr_span_subset_of_addressable_field)
have "{ptr_val p..+n * size_of TYPE('a)} ∩ {x..+size_td root} = {}"
proof (rule ccontr)
assume "{ptr_val p..+n * size_of TYPE('a)} ∩ {x..+size_td root} ≠ {}"
then obtain i where i: "i < n" and overlap: "ptr_span (p +⇩p int i) ∩ {x..+size_td root} ≠ {}"
by (meson array_to_index_span disjoint_iff)
from root_p [OF i] have "root_ptr_valid_u (typ_uinfo_t TYPE('a)) d (ptr_val (p +⇩p int i))"
by (simp add: root_ptr_valid_root_ptr_valid_u_conv)
from root_ptr_valid_u_cases [OF root_ptr_valid_u this] overlap
obtain "root = typ_uinfo_t TYPE('a)" "x = ptr_val (p +⇩p int i)"
by (simp add: inf_commute size_of_tag)
then have "ptr_span (p +⇩p int i) = {x..+size_td root}"
by (simp add: size_of_def)
with contained have "ptr_span q ⊆ ptr_span (p +⇩p int i)" by simp
with disj i show False
apply (simp add: array_index_span_conv)
by (smt (verit, ccfv_SIG) UN_I disjoint_iff mem_type_self ord_class.lessThan_iff subsetD)
qed
with stack_releases_root_ptr_valid_u_cases [OF p_not_stack_byte root_not_stack_byte] root_ptr_valid_u
have "root_ptr_valid_u root (stack_releases n p d) x" by auto
with path x
show "ptr_valid (stack_releases n p d) q"
using ptr_valid_def ptr_valid_u.simps by blast
qed
lemma stack_releases_ptr_valid_cases3:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes p_not_stack_byte: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes root_p: "⋀i. i < n ⟹ root_ptr_valid d (p +⇩p int i)"
assumes valid_q: "ptr_valid d q"
assumes invalid_q: "¬ ptr_valid (stack_releases n p d) q"
shows "∃path i.
addressable_field (typ_uinfo_t TYPE('a)) path (typ_uinfo_t TYPE('b)) ∧ i < n ∧
q = PTR('b) &(p +⇩p int i→path)"
proof -
from valid_q invalid_q stack_releases_ptr_valid_cases2 [OF p_not_stack_byte q_not_stack_byte root_p _ valid_q, of n ]
have "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span q ≠ {} " by auto
then obtain i where i_bound: "i < n" and overlap: "ptr_span (p +⇩p int i) ∩ ptr_span q ≠ {}"
by (auto simp add: array_index_span_conv )
from root_ptr_valid_ptr_valid_cases [OF root_p [OF i_bound] valid_q, simplified overlap, simplified] i_bound
show ?thesis by blast
qed
lemma stack_releases_ptr_valid_cases:
fixes p:: "'a::mem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes p_not_stack_byte: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes root_p: "⋀i. i < n ⟹ root_ptr_valid d (p +⇩p int i)"
shows "ptr_valid (stack_releases n p d) q ⟷
ptr_valid d q ∧ {ptr_val p ..+ n * size_of TYPE('a::mem_type)} ∩ ptr_span q = {}"
using stack_releases_ptr_valid_cases1 [OF p_not_stack_byte q_not_stack_byte]
stack_releases_ptr_valid_cases2 [OF p_not_stack_byte q_not_stack_byte root_p] by blast
lemma ptr_valid_same_type_neq_no_overlap_conv:
fixes p:: "'a::mem_type ptr"
fixes q:: "'a::mem_type ptr"
assumes valid_p: "ptr_valid d p"
assumes valid_q: "ptr_valid d q"
shows "p ≠ q ⟷ ptr_span p ∩ ptr_span q = {}"
using cvalid_same_type_neq_disjoint assms ptr_valid_h_t_valid
by blast
theorem stack_allocs_the_default_plift [stack_the_default_plift]:
fixes p:: "'a::xmem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes alloc: "(p, d') ∈ stack_allocs n 𝒮 TYPE('a) (hrs_htd h)"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
shows "the_default c_type_class.zero
(plift (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) (hrs_htd_update (λ_. d') h)) q) =
the_default c_type_class.zero (plift h q)"
proof (cases "ptr_valid d' q")
case True
from alloc q_not_stack_byte True
show ?thesis
proof (cases rule: stack_allocs_ptr_valid_cases1')
case (addressable_field i path)
from addressable_field obtain
i: "i < n" and
path: "addressable_field (typ_uinfo_t TYPE('a)) path (typ_uinfo_t TYPE('b))" and
q: "q = PTR('b) &(p +⇩p int i→path)" and
invalid: "¬ ptr_valid (hrs_htd h) q"
by blast
from invalid have "(plift h q) = None"
by (simp add: plift_None)
moreover
from stack_allocs_cases [OF alloc]
obtain bound: "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card" and not_null: "ptr_val p ≠ 0"
by (metis Ptr_ptr_val c_guard_NULL_simp)
from path obtain m where
"field_lookup (typ_uinfo_t TYPE('a)) path 0 = Some ((typ_uinfo_t TYPE('b)), m)"
by (auto dest: addressable_fieldD_field_lookup)
then obtain t where fl: "field_lookup (typ_info_t TYPE('a)) path 0 = Some (t, m)" and
match: "export_uinfo t = typ_uinfo_t TYPE('b)"
using field_lookup_uinfo_Some_rev by blast
from fl have field_ti: "field_ti TYPE('a) path = Some t"
using field_lookup_field_ti by blast
from field_lookup_zero [OF fl match] have from_bytes_zero: "from_bytes (access_ti⇩0 t c_type_class.zero) = (c_type_class.zero::'b)" .
note h_val_field = h_val_field_from_bytes' [OF field_ti match [simplified typ_uinfo_t_def]]
from h_val_fold [OF bound not_null i]
have h_val_zero:
"h_val (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n] (hrs_mem h)) (p +⇩p int i) = c_type_class.zero" .
have path_zero:
"h_val (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n] (hrs_mem h)) (PTR('b) &(p +⇩p int i→path)) = c_type_class.zero"
by (simp add: h_val_field h_val_zero from_bytes_zero)
from True i path q
have "(plift (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) (hrs_htd_update (λ_. d') h)) q) = Some c_type_class.zero"
apply -
apply (subst ptr_valid_plift_Some_hval)
apply (simp add: hrs_htd_update)
apply (simp add: path_zero hrs_mem_update)
done
ultimately
show ?thesis by simp
next
case disjoint
then obtain valid_q: "ptr_valid (hrs_htd h) q" and
disj: "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span q = {}" by blast
from valid_q have "(plift h q) = Some (h_val (hrs_mem h) q)"
by (simp add: ptr_valid_plift_Some_hval valid_q)
moreover
have h_val_eq:
"h_val (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n] (hrs_mem h)) q =
h_val (hrs_mem h) q" by (simp add: h_val_fold_zero_disjoint [OF disj])
from True have valid_q':
"ptr_valid (hrs_htd ((hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n])
(hrs_htd_update (λ_. d') h)))) q"
by (simp add: hrs_htd_update)
have "plift (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n])
(hrs_htd_update (λ_. d') h)) q = Some (h_val (hrs_mem h) q)"
using True by (simp add: ptr_valid_plift_Some_hval [OF valid_q'] hrs_mem_update h_val_eq)
ultimately
show ?thesis
by simp
qed
next
case False
from False
have invalid: "¬ ptr_valid (hrs_htd h) q"
using alloc q_not_stack_byte stack_allocs_ptr_valid_cases2 by blast
then
have "plift (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) (hrs_htd_update (λ_. d') h)) q = None"
using plift_None
by (metis (no_types, lifting) False hrs_htd_mem_update hrs_htd_update)
moreover
have "(plift h q) = None"
using invalid by (simp add: plift_None)
ultimately show ?thesis by simp
qed
theorem stack_releases_the_default_plift [stack_the_default_plift]:
fixes p:: "'a::xmem_type ptr"
fixes q:: "'b::mem_type ptr"
assumes roots: "⋀i. i < n ⟹ root_ptr_valid (hrs_htd h) (p +⇩p int i)"
assumes p_not_stack_byte: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
shows "the_default c_type_class.zero
(plift
(hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) h)
q) =
the_default c_type_class.zero (plift (hrs_htd_update (stack_releases n p) h) q)"
proof (cases "ptr_valid (stack_releases n p (hrs_htd h)) q")
case True
from stack_releases_ptr_valid_cases1 [OF p_not_stack_byte q_not_stack_byte True]
obtain disjoint: "{ptr_val p..+n * size_of TYPE('a)} ∩ ptr_span q = {}" and
valid_q: "ptr_valid (hrs_htd h) q" by blast
from True valid_q have "plift (hrs_htd_update (stack_releases n p) h) q = Some (h_val (hrs_mem h) q)"
using ptr_valid_plift_Some_hval
by (metis hrs_htd_update hrs_mem_htd_update)
moreover
from h_val_fold_zero_disjoint [OF disjoint]
have "h_val (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n] (hrs_mem h)) q = h_val (hrs_mem h) q" .
with valid_q
have "(plift (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) h) q) = Some (h_val (hrs_mem h) q)"
by (simp add: hrs_mem_update ptr_valid_plift_Some_hval)
ultimately show ?thesis by simp
next
case False
from False
have eq1: "plift (hrs_htd_update (stack_releases n p) h) q = None"
by (simp add: plift_None hrs_htd_update)
show ?thesis
proof (cases "ptr_valid (hrs_htd h) q")
case True
show ?thesis
proof (cases n)
case 0
then show ?thesis
using False True by (auto simp add: stack_releases_def)
next
case (Suc n')
from roots [of 0] Suc
have not_null: "ptr_val p ≠ 0"
by (metis CTypesDefs.ptr_add_def Ptr_ptr_val Zero_not_Suc add.right_neutral
bot_nat_0.not_eq_extremum mem_type_self mult_zero_left of_int_0 root_ptr_valid_range_not_NULL roots semiring_1_class.of_nat_0)
from roots Suc
have bound: "unat (ptr_val p) + n * size_of TYPE('a) ≤ addr_card"
by (metis array_to_index_span len_of_addr_card root_ptr_valid_range_not_NULL zero_not_in_intvl_no_overflow)
from stack_releases_ptr_valid_cases3 [OF p_not_stack_byte q_not_stack_byte roots True False]
obtain path i where
path: "addressable_field (typ_uinfo_t TYPE('a)) path (typ_uinfo_t TYPE('b))" and
q: "q = PTR('b) &(p +⇩p int i→path)" and
i_bound: "i < n"
by blast
from path obtain m where
"field_lookup (typ_uinfo_t TYPE('a)) path 0 = Some ((typ_uinfo_t TYPE('b)), m)"
by (auto dest: addressable_fieldD_field_lookup)
then obtain t where fl: "field_lookup (typ_info_t TYPE('a)) path 0 = Some (t, m)" and
match: "export_uinfo t = typ_uinfo_t TYPE('b)"
using field_lookup_uinfo_Some_rev by blast
from fl have field_ti: "field_ti TYPE('a) path = Some t"
using field_lookup_field_ti by blast
from field_lookup_zero [OF fl match] have from_bytes_zero: "from_bytes (access_ti⇩0 t c_type_class.zero) = (c_type_class.zero::'b)" .
note h_val_field = h_val_field_from_bytes' [OF field_ti match [simplified typ_uinfo_t_def]]
from h_val_fold [OF bound not_null i_bound]
have h_val_zero:
"h_val (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n] (hrs_mem h)) (p +⇩p int i) = c_type_class.zero" .
have path_zero:
"h_val (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n] (hrs_mem h)) (PTR('b) &(p +⇩p int i→path)) = c_type_class.zero"
by (simp add: h_val_field h_val_zero from_bytes_zero)
from True i_bound path q
have "plift (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) h) q = Some c_type_class.zero"
apply -
apply (subst ptr_valid_plift_Some_hval)
apply (simp add: hrs_htd_update)
apply (simp add: path_zero hrs_mem_update)
done
then show ?thesis by (simp add: eq1)
qed
next
case False
from False
have "plift (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) h) q = None"
using plift_None
by (metis False hrs_htd_mem_update )
with eq1 show ?thesis by simp
qed
qed
lemma h_val_heap_update_padding_heap_update_conv:
fixes p::"'a::mem_type ptr"
fixes q::"'b::mem_type ptr"
assumes valid_p: "ptr_valid d p"
assumes valid_q: "ptr_valid d q"
assumes lbs: "length bs = size_of TYPE('a)"
shows "h_val ((heap_update_padding p v bs h)) q = h_val (heap_update p v h) q"
using ptr_valid_cases_weak[OF valid_p valid_q]
proof (elim disjE exE conjE)
assume "disjnt (ptr_span p) (ptr_span q)" then show ?thesis
by (simp add: h_val_heap_update_padding_disjoint h_val_update_regions_disjoint lbs disjnt_def)
next
fix f assume f: "addressable_field (typ_uinfo_t TYPE('a)) f (typ_uinfo_t TYPE('b))"
and q: "q = PTR('b) &(p→f)"
from addressable_fieldD_field_ti[OF f]
obtain t where t: "field_ti TYPE('a) f = Some t" "export_uinfo t = typ_uinfo_t TYPE('b)"
by auto
let ?s = "from_bytes o access_ti⇩0 t :: 'a ⇒ 'b"
interpret f: nested_field' t f ?s "update_ti t o to_bytes_p"
using t by unfold_locales simp_all
show ?thesis unfolding q using lbs
by (subst (1 2) f.h_val_field) (simp add: h_val_heap_update_padding)
next
fix f assume f: "addressable_field (typ_uinfo_t TYPE('b)) f (typ_uinfo_t TYPE('a))"
and p: "p = PTR('a) &(q→f)"
from addressable_fieldD_field_ti[OF f]
obtain t where t: "field_ti TYPE('b) f = Some t" "export_uinfo t = typ_uinfo_t TYPE('a)"
by auto
let ?s = "from_bytes o access_ti⇩0 t :: 'b ⇒ 'a"
interpret f: nested_field' t f ?s "update_ti t o to_bytes_p"
using t by unfold_locales simp_all
note q = ptr_valid_h_t_valid[OF valid_q]
show ?thesis unfolding p
apply (subst f.h_val_field_lvalue_update_padding[OF q q lbs])
apply (subst f.h_val_field_lvalue_update[OF q q])
apply simp
done
qed
lemma plift_heap_update_padding_heap_update_conv:
fixes p::"'a::mem_type ptr"
fixes q::"'b::mem_type ptr"
assumes valid_p: "ptr_valid (hrs_htd h) p"
assumes lbs: "length bs = size_of TYPE('a)"
shows "plift (hrs_mem_update (heap_update_padding p v bs) h) q = plift (hrs_mem_update (heap_update p v) h) q"
using h_val_heap_update_padding_heap_update_conv
by (metis hrs_htd_mem_update hrs_mem_update lbs valid_p wf_ptr_valid.plift_None
wf_ptr_valid.ptr_valid_plift_Some_hval wf_ptr_valid_axioms)
theorem plift_heap_update_padding_heap_update_pointless_conv [plift_heap_update_padding_heap_update_conv]:
fixes p::"'a::mem_type ptr"
assumes valid_p: "ptr_valid (hrs_htd h) p"
assumes lbs: "length bs = size_of TYPE('a)"
shows "plift (hrs_mem_update (heap_update_padding p v bs) h) = plift (hrs_mem_update (heap_update p v) h)"
apply (rule ext)
using plift_heap_update_padding_heap_update_conv assms
by blast
lemma ptr_valid_stack_byte_disjoint:
fixes q::"'a::{mem_type, stack_type} ptr"
fixes p::"stack_byte ptr"
assumes "root_ptr_valid h p"
assumes "ptr_valid h q"
shows "ptr_span p ∩ ptr_span q = {}"
using assms local.ptr_valid_h_t_valid no_stack_byte root_ptr_valid_not_subtype_disjoint sub_typ_stack_byte
by blast
lemma h_val_heap_update_list_stack_byte:
fixes q::"'a::{mem_type, stack_type} ptr"
assumes valid_p: "root_ptr_valid d (p::stack_byte ptr)"
assumes valid_q: "ptr_valid d q"
assumes lbs: "length bs = size_of TYPE(stack_byte)"
shows "h_val (heap_update_list (ptr_val p) bs h) q = h_val h q"
using ptr_valid_stack_byte_disjoint [OF valid_p valid_q] lbs
by (simp add: h_val_def heap_list_update_disjoint_same)
lemma h_val_heap_update_list_stack_byte':
fixes q::"'a::{mem_type, stack_type} ptr"
fixes p::"stack_byte ptr"
assumes valid_p: "⋀i. i < length bs ⟹ root_ptr_valid d (p +⇩p int i)"
assumes valid_q: "ptr_valid d q"
shows "h_val (heap_update_list (ptr_val p) bs h) q = h_val h q"
using valid_p
proof (induct bs arbitrary: p h)
case Nil
then show ?case by simp
next
case (Cons b bs)
from Cons.prems Cons.prems [of 0] obtain
valid_bs: "⋀i. i < Suc (length bs) ⟹ root_ptr_valid d (p +⇩p int i)" and
valid_p: "root_ptr_valid d p" by auto
from valid_bs have valid_bs': "⋀i. i < length bs ⟹ root_ptr_valid d ((p +⇩p 1) +⇩p int i)"
apply (clarsimp simp add: ptr_add_def)
by (metis Ex_less_Suc group_cancel.add1 less_trans_Suc of_nat_Suc)
have "length [b] = size_of TYPE(stack_byte)" by auto
note b_eq = h_val_heap_update_list_stack_byte [OF valid_p valid_q this]
have val_eq: "ptr_val (p +⇩p 1) = ptr_val p + 1"
by (auto simp add: ptr_add_def)
note hyp = Cons.hyps [OF valid_bs', simplified val_eq]
show ?case
apply (simp add: hyp)
using b_eq
apply (auto simp add: fun_upd_def)
done
qed
lemma plift_heap_update_list_stack_byte:
fixes q::"'a::{mem_type, stack_type} ptr"
fixes p::"stack_byte ptr"
assumes valid_p: "⋀i. i < length bs ⟹ root_ptr_valid (hrs_htd h) (p +⇩p int i)"
shows "plift (hrs_mem_update (heap_update_list (ptr_val p) bs) h) q = plift h q"
using h_val_heap_update_list_stack_byte'
by (metis hrs_htd_mem_update hrs_mem_update valid_p wf_ptr_valid.plift_None
wf_ptr_valid.ptr_valid_plift_Some_hval wf_ptr_valid_axioms)
lemma plift_heap_update_list_stack_byte_pointless[plift_heap_update_list_stack_byte]:
fixes p::"stack_byte ptr"
assumes valid_p: "⋀i. i < length bs ⟹ root_ptr_valid (hrs_htd h) (p +⇩p int i)"
shows "plift (hrs_mem_update (heap_update_list (ptr_val p) bs) h) =
(plift h::'a::{mem_type, stack_type} ptr ⇒ 'a option)"
using assms plift_heap_update_list_stack_byte by blast
lemma plift_eq_plift:
"hrs_htd h = hrs_htd h' ⟹
(⋀p::'a ptr. ptr_valid (hrs_htd h') p ⟹
h_val (hrs_mem h) p = h_val (hrs_mem h') p) ⟹
(plift h::'a::mem_type ptr ⇒ 'a option) = plift h'"
apply (rule ext)
apply (cases h; cases h')
apply (simp add: plift_def lift_t_if h_t_valid_def root_ptr_valid_def hrs_htd_def
hrs_mem_def)
done
definition addressable_fields :: "'a::mem_type itself ⇒ (field_name list × 'a xtyp_info) list" where
"addressable_fields TYPE('a) = (case map_of 𝒯 (typ_uinfo_t TYPE('a)) of
None ⇒ []
| Some fs ⇒ map (λf. (f, the (field_ti TYPE('a) f))) fs)"
abbreviation merge_addressable_fields :: "'a::mem_type ⇒ 'a ⇒ 'a" where
"merge_addressable_fields ≡ merge_ti_list (map snd (addressable_fields TYPE('a)))"
definition read_dedicated_heap :: "heap_raw_state ⇒ 'a::mem_type typ_heap_g" where
"read_dedicated_heap h p = merge_addressable_fields ZERO('a) (the_default ZERO('a) (plift h p))"
definition write_dedicated_heap :: "'a::mem_type ptr ⇒ 'a ⇒ heap_raw_state ⇒ heap_raw_state" where
"write_dedicated_heap p v = hrs_mem_update (heap_upd p (λold. merge_addressable_fields old v))"
lemma mem_addressable_fields:
assumes F: "map_of 𝒯 (typ_uinfo_t TYPE('a::mem_type)) = Some F"
shows "f ∈ set F ⟹ field_ti TYPE('a) f = Some u ⟹ (f, u) ∈ set (addressable_fields TYPE('a))"
using wf_𝒯[of "typ_uinfo_t TYPE('a)"]
by (force simp add: addressable_fields_def F image_iff list_all_iff field_ti_def)
lemma mem_snd_addressable_fields:
assumes F: "map_of 𝒯 (typ_uinfo_t TYPE('a::mem_type)) = Some F" "f ∈ set F"
"field_ti TYPE('a) f = Some u"
shows "u ∈ snd ` set (addressable_fields TYPE('a))"
using mem_addressable_fields[OF assms] by (force simp: image_iff)
lemma list_all_field_ti_addressable_fields:
"list_all (λ(f, u). field_ti TYPE('a) f = Some u) (addressable_fields TYPE('a::mem_type))"
apply (clarsimp simp add: addressable_fields_def split: option.splits)
subgoal premises prems
using prems[THEN wf_𝒯]
unfolding list.pred_map
by (rule list.pred_mono_strong)
(auto simp: list_all_iff field_ti_def typ_uinfo_t_def
dest!: field_lookup_export_uinfo_Some_rev field_lookup_field_ti')
done
lemma distinct_disj_fn_addressable_fields:
"distinct_prop disj_fn (map fst (addressable_fields TYPE('a::mem_type)))"
using wf_𝒯'
by (auto simp: list_all_iff addressable_fields_def comp_def dest!: map_of_SomeD split: option.splits)
lemma list_all_field_ti_snd_addressable_fields:
"list_all (λu. ∃f. field_ti TYPE('a) f = Some u) (map snd (addressable_fields TYPE('a::mem_type)))"
unfolding list.pred_map
using list_all_field_ti_addressable_fields
by (rule list.pred_mono_strong) auto
sublocale merge_addressable_fields: is_scene "merge_addressable_fields :: 'a::xmem_type ⇒ 'a ⇒ 'a"
using list_all_field_ti_snd_addressable_fields by (rule is_scene_merge_ti_list)
lemma ptr_valid_u_cases_same_type:
assumes t: "mem_type_u t" and a: "ptr_valid_u t d a" and b: "ptr_valid_u t d b"
shows "a = b ∨ disjnt {a..+size_td t} {b..+size_td t}"
using ptr_valid_u_cases_weak[OF t a b] by auto
lemma read_dedicated_heap_heap_update_list_stack_byte_pointless[simp]:
fixes p::"stack_byte ptr"
assumes valid_p: "⋀i. i < length bs ⟹ root_ptr_valid (hrs_htd h) (p +⇩p int i)"
shows "read_dedicated_heap (hrs_mem_update (heap_update_list (ptr_val p) bs) h) =
(read_dedicated_heap h::'a::{mem_type, stack_type} ptr ⇒ 'a)"
unfolding read_dedicated_heap_def
by (simp add: plift_heap_update_list_stack_byte_pointless[OF valid_p])
lemma read_dedicated_heap_write_dedicated_heap_ne[simp]:
fixes p :: "'a::xmem_type ptr" and q :: "'b::xmem_type ptr"
assumes ne: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b)"
assumes p: "ptr_valid (hrs_htd h) p"
shows "read_dedicated_heap (write_dedicated_heap p x h) q = read_dedicated_heap h q"
proof cases
let ?A = "typ_uinfo_t TYPE('a)" and ?B = "typ_uinfo_t TYPE('b)"
assume q: "ptr_valid (hrs_htd h) q"
from ptr_valid_cases_weak[OF p q]
show ?thesis
proof (elim disjE exE conjE)
assume "disjnt (ptr_span p) (ptr_span q)" with p q show ?thesis
by (simp add: read_dedicated_heap_def write_dedicated_heap_def disjnt_def
hrs_mem_update_heap_upd plift_disjoint_region)
next
fix f' assume f'_n: "addressable_field ?A f' ?B" and q_eq: "q = PTR('b) &(p→f')"
obtain F f1 f2 u where f'_eq: "f' = f1 @ f2"
and F: "f1 ∈ set F" "map_of 𝒯 ?A = Some F"
and f_u: "field_ti TYPE('a) f1 = Some u"
and "addressable_field (export_uinfo u) f2 ?B"
using f'_n ne by (cases rule: addressable_field.cases) (auto simp: field_ti_def dest!: field_lookup_uinfo_Some_rev)
obtain v n where v: "export_uinfo v = ?B"
and f_fs: "field_lookup (typ_info_t TYPE('a)) (f1 @ f2) 0 = Some (v, n)"
using addressable_fieldD_field_lookup[OF f'_n] unfolding f'_eq
by (auto dest: field_lookup_uinfo_Some_rev)
obtain m where u_v: "field_lookup u f2 0 = Some (v, m)"
using f_fs f_u
apply (subst (asm) field_lookup_append_eq)
apply (auto simp add: f_u field_ti_def split: option.splits
dest: CTypes.field_lookup_offset2)
done
have p': "hrs_htd h ⊨⇩t p"
using p by (rule ptr_valid_h_t_valid)
have u_mem: "u ∈ snd ` set (addressable_fields TYPE('a))"
using F(2,1) f_u(1) by (rule mem_snd_addressable_fields)
have f1u_mem: "(f1, u) ∈ set (addressable_fields TYPE('a))"
using F(2,1) f_u(1) by (rule mem_addressable_fields)
have sz: "size_of TYPE('b) = size_td v"
using v unfolding export_uinfo_size[symmetric] by (simp add: size_of_def)
have "length bs = size_of TYPE('b) ⟹
access_ti v (merge_addressable_fields y x) bs = access_ti v y bs" for y bs
by (intro access_ti_merge_ti_list[OF list_all_field_ti_addressable_fields
distinct_disj_fn_addressable_fields f1u_mem u_v])
(simp add: sz)
then show ?thesis using q unfolding f'_eq q_eq
apply (simp add: read_dedicated_heap_def write_dedicated_heap_def ptr_valid_plift_Some_hval
hrs_mem_update)
apply (simp add: heap_upd_def
ptr_valid_heap_update_subtype_field_access_ti_indep[OF p' p' f_fs v])
done
next
fix f' n assume f'_n: "addressable_field ?B f' ?A" and p_eq: "p = PTR('a) &(q → f')"
from f'_n ne obtain F f0 f1 t0 n where *: "map_of 𝒯 ?B = Some F" "f0 ∈ set F" "f' = f0 @ f1"
and f0: "field_lookup ?B f0 0 = Some (t0, n)" and f1: "addressable_field t0 f1 ?A"
by cases auto
from addressable_fieldD_field_ti[OF f'_n]
obtain tA where f'_u: "field_ti TYPE('b) f' = Some tA" and tA: "export_uinfo tA = ?A"
by auto
have [simp]: "size_td tA = size_of TYPE('a)"
unfolding export_uinfo_size[symmetric] tA by (simp add: size_of_def)
from f0[unfolded typ_uinfo_t_def, THEN field_lookup_export_uinfo_Some_rev]
obtain t0' where f0_t0': "field_ti TYPE('b) f0 = Some t0'" and t0: "t0 = export_uinfo t0'"
by (auto simp: field_ti_def typ_uinfo_t_def
split: option.splits)
obtain tA' n where t0'_f1: "field_lookup t0' f1 0 = Some (tA', n)"
using addressable_fieldD_field_lookup'[OF f1, unfolded t0,
THEN field_lookup_export_uinfo_Some_rev]
by auto
with field_ti_append_field_lookup[OF f0_t0' t0'_f1] f'_u
have f0'_f1: "field_lookup t0' f1 0 = Some (tA, n)"
by (simp add: *)
note q' = ptr_valid.ptr_valid_h_t_valid[OF q]
have f0t'_mem: "(f0, t0') ∈ set (addressable_fields TYPE('b))"
using *(1,2) f0_t0' by (rule mem_addressable_fields)
from q f'_n merge_ti_list_update_ti[OF
list_all_field_ti_addressable_fields f0t'_mem distinct_disj_fn_addressable_fields]
merge_ti_list_update_ti[OF
list_all_field_ti_addressable_fields f0t'_mem distinct_disj_fn_addressable_fields f0'_f1]
show ?thesis unfolding p_eq
by (simp add: read_dedicated_heap_def write_dedicated_heap_def hrs_mem_update heap_upd_def
ptr_valid_plift_Some_hval h_val_field_update[OF f'_u tA q' q']
update_ti_t_def)
qed
qed (simp add: read_dedicated_heap_def write_dedicated_heap_def plift_None)
lemma read_dedicated_heap_write_dedicated_heap[simp]:
"ptr_valid (hrs_htd h) (p::'a::xmem_type ptr) ⟹
read_dedicated_heap (write_dedicated_heap p x h) =
upd_fun p (λold. merge_addressable_fields old x) (read_dedicated_heap h)"
by (simp add: fun_eq_iff the_plift_hval_fun_upd_eqI read_dedicated_heap_def[abs_def] upd_fun_def
write_dedicated_heap_def hrs_mem_update_heap_upd fun_upd_def)
lemma hrs_mem_update_heap_update:
fixes p :: "'a::xmem_type ptr"
shows "hrs_mem_update (heap_update p x) h =
fold (λ(f, u). hrs_mem_update (heap_upd_list (size_td u) &(p→f) (access_ti u x)))
(addressable_fields TYPE('a))
(write_dedicated_heap p x h)"
proof -
show ?thesis
apply (subst heap_update_eq_fold_subfields[OF list_all_field_ti_addressable_fields,
where y="h_val (hrs_mem h) p"])
unfolding hrs_mem_update_comp'[symmetric] write_dedicated_heap_def hrs_mem_update_heap_upd
apply (subst fold_functor[of hrs_mem_update])
apply (simp add: hrs_mem_update_def)
apply (simp add: hrs_mem_update_def fun_eq_iff)
apply (simp add: split_beta')
done
qed
lemma hrs_mem_update_heap_update':
fixes p :: "'a::xmem_type ptr"
shows "hrs_mem_update (heap_update p x) =
fold (λ(f, u). hrs_mem_update (heap_upd_list (size_td u) &(p→f) (access_ti u x)))
(addressable_fields TYPE('a)) ∘
write_dedicated_heap p x"
apply (rule ext)
unfolding comp_apply
apply (rule hrs_mem_update_heap_update)
done
lemma hrs_htd_write_dedicated_heap[simp]:
"hrs_htd (write_dedicated_heap p x h) = hrs_htd h"
by (simp add: write_dedicated_heap_def)
lemma partial_pointer_lense_merge_addressable_fields:
fixes r :: "'h ⇒ 'a::xmem_type ptr ⇒ 'a"
assumes "lense r w"
shows
"partial_pointer_lense (λx y. merge_addressable_fields y x)
(λh p x . merge_addressable_fields x (r h p)) (λp x. w (upd_fun p (λold. merge_addressable_fields old x)))"
proof -
interpret lense r w by fact
show ?thesis
apply unfold_locales
apply (simp_all add: upd_fun.upd_same upd_same)
subgoal by (simp add: comp_def)
subgoal for p q x y h
by (simp add: upd_fun_commute disj_ptr_span_ptr_neq disjnt_def Int_commute)
done
qed
lemma pointer_lense_of_partials_cover:
fixes rs :: "('h ⇒ 'a::xmem_type ptr ⇒ 'a ⇒ 'a) list"
assumes g_u: "lense g u"
assumes *:
"length ms = length rs" "length ms = length ws"
"list_all (λ(m, r, w). partial_pointer_lense m r w) (zip ms (zip rs ws))"
and **:
"⋀a b c. distinct_prop (λm1 m2. m1 a (m2 b c) = m2 b (m1 a c)) ms"
"⋀p a q b h. distinct_prop (λw1 w2. p = q ∨ disjnt (ptr_span p) (ptr_span q) ⟶
w1 p a (w2 q b h) = w2 q b (w1 p a h)) ((λp x. u (upd_fun p (λold. merge_addressable_fields old x))) # ws)"
assumes ms_cover: "⋀a b. fold (λm. m a) ms b = merge_addressable_fields a b"
assumes R: "⋀h p. R h p = fold (λr. r h p) rs (g h p)"
assumes W: "⋀p f h. W p f h =
fold (λw. w p (f (R h p))) ws (u (upd_fun p (λold. merge_addressable_fields old (f (R h p)))) h)"
shows "pointer_lense R W"
apply (rule pointer_lense_of_partials[where
ms="(λa b. merge_addressable_fields b a) # ms" and
rs = "(λh p x. merge_addressable_fields x (g h p)) # rs" and
ws = "(λp x. u (upd_fun p (λold. merge_addressable_fields old x)))#ws"])
subgoal by (simp add: *(1))
subgoal by (simp add: *(2))
subgoal
apply (rule list_all_zip_zip_cons)
apply (rule partial_pointer_lense_merge_addressable_fields[OF g_u])
apply (rule *)
done
subgoal for a b c
proof -
have scenes_ms: "list_all is_scene ms"
using * by (simp add: list_all_length partial_pointer_lense_def)
have dis_ms: "distinct_prop disjnt_scene ms"
using **(1) by (simp add: disjnt_scene_def[abs_def] distinct_prop_distrib_all)
have comm_ms: "pairwise comm_scene (set ms)"
apply (rule pairwise_set_of_distinct_prop)
apply (simp add: comm_scene_comm)
apply (use dis_ms in ‹auto simp: distinct_prop_iff_nth›)
done
have ms_y: "list_all (λm. disjnt_scene m y ∨ m = y) ms" if y: "y ∈ set ms" for y
using in_set_conv_decomp[THEN iffD1, OF y] dis_ms
by (auto simp: distinct_prop_append list_all_iff disjnt_scene_comm)
show ?thesis
apply (simp add: **)
apply (simp flip: ms_cover)
apply (intro ballI)
apply (rule fold_disjnt_scene[OF scenes_ms comm_ms ms_y])
apply auto
done
qed
subgoal by (rule **)
subgoal by (simp add: ms_cover)
subgoal for h p
proof -
interpret fold: partial_pointer_lense
"λa. fold (λm. m a) ms" "λh p. fold (λr. r h p) rs" "λp x. fold (λw. w p x) ws"
apply (rule partial_pointer_lense_fold[OF *])
subgoal using **(1) by auto
subgoal using **(2) by auto
done
show "R h p = fold (λr. r h p) ((λh p x. merge_addressable_fields x (g h p)) # rs) x"
using fold.r_m by (simp add: R flip: ms_cover)
qed
subgoal by (simp add: W)
done
lemma cover_read_dedicated_heap[simp]:
"merge_addressable_fields (read_dedicated_heap h p) = merge_addressable_fields ZERO('a::xmem_type)"
by (simp add: fun_eq_iff read_dedicated_heap_def)
lemma read_dedicated_heap_fun_upd_cover_zero_eq_upd_fun[simp]:
"((read_dedicated_heap h)(p := merge_addressable_fields ZERO('a::xmem_type) x)) q =
upd_fun p (λold. merge_addressable_fields old x) (read_dedicated_heap h) q"
by (simp add: upd_fun_def fun_upd_def fun_eq_iff)
theorem stack_allocs_read_dedicated_heap [stack_the_default_plift]:
fixes p:: "'a::xmem_type ptr"
assumes alloc: "(p, d') ∈ stack_allocs n 𝒮 TYPE('a) (hrs_htd h)"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b::xmem_type) ≠ typ_uinfo_t TYPE(stack_byte)"
shows "read_dedicated_heap (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) (hrs_htd_update (λ_. d') h)) =
(read_dedicated_heap h :: 'b ptr ⇒ _)"
apply (rule ext)
unfolding read_dedicated_heap_def stack_allocs_the_default_plift[OF assms] ..
theorem stack_releases_read_dedicated_heap [stack_the_default_plift]:
fixes p:: "'a::xmem_type ptr"
assumes roots: "⋀i. i < n ⟹ root_ptr_valid (hrs_htd h) (p +⇩p int i)"
assumes p_not_stack_byte: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE(stack_byte)"
assumes q_not_stack_byte: "typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE(stack_byte)"
shows "read_dedicated_heap (hrs_mem_update (fold (λi. heap_update (p +⇩p int i) c_type_class.zero) [0..<n]) h) =
(read_dedicated_heap (hrs_htd_update (stack_releases n p) h) :: 'b::xmem_type ptr ⇒ _)"
unfolding read_dedicated_heap_def stack_releases_the_default_plift[OF assms, of n, simplified] ..
lemma ptr_valid_addressable_field_field_lvalue[addressable_field_exec]:
fixes p::"'a::mem_type ptr"
assumes "ptr_valid h p"
assumes "addressable_field (typ_uinfo_t (TYPE('a))) fs (typ_uinfo_t (TYPE('b::mem_type)))"
shows "ptr_valid h (PTR('b) (&(p→fs)))"
using assms
by (metis field_lvalue_def field_offset_def local.fold_ptr_valid'
local.open_types_axioms local.ptr_valid_u_trans open_types.ptr_valid_def)
lemma addressable_field_exec[addressable_field_exec]:
shows
"addressable_field t ps v =
(case ps of
[] => t = v
| _ ⇒ (∃fs p. map_of 𝒯 t = Some fs ∧
List.find (λp. ∃u n. field_lookup t p 0 = Some (u, n) ∧ p @ drop (length p) ps = ps ∧
addressable_field u (drop (length p) ps) v) fs = Some p))"
proof (cases ps)
case Nil
then show ?thesis by simp
next
case (Cons f ps')
show ?thesis
proof (cases "map_of 𝒯 t")
case None
then show ?thesis
apply (simp add: Cons)
by (metis list.simps(2) local.addressable_field.cases option.simps(3))
next
case (Some fs)
show ?thesis
proof (cases "∃p. List.find (λp. ∃u n. field_lookup t p 0 = Some (u, n) ∧
p @ drop (length p) ps = ps ∧
addressable_field u (drop (length p) ps) v) fs = Some p")
case True
then obtain p where
find: "List.find (λp. ∃u n. field_lookup t p 0 = Some (u, n) ∧
p @ drop (length p) ps = ps ∧
addressable_field u (drop (length p) ps) v) fs = Some p"
by auto
then obtain u n where
p: "p ∈ set fs" and
ps: "p @ drop (length p) ps = ps" and
u: "field_lookup t p 0 = Some (u, n)" and
addr: "addressable_field u (drop (length p) ps) v"
using findSomeD
by (smt (verit, best))
from addressable_field_step [OF Some p u addr]
have addr': "addressable_field t (p @ drop (length p) ps) v" .
from addressable_fieldD_field_lookup [OF addr] obtain m
where v: "field_lookup u (drop (length p) ps) 0 = Some (v, m)"
by blast
from addressable_fieldD_field_lookup [OF addr'] obtain k where
"field_lookup t (p @ drop (length p) ps) 0 = Some (v, k)"
by blast
have ps_eq: "(p @ drop (length p) (f # ps')) = ps"
using ps
by (simp add: Cons ps)
show ?thesis
using find addr'
by (simp add: Cons Some ps_eq)
next
case False
with Some show ?thesis
apply (simp add: Cons)
apply (force simp add: find_None_iff elim: addressable_field.cases)
done
qed
qed
qed
local_setup ‹
let
fun unfold_ss ctxt = ctxt addsimps
Named_Theorems.get ctxt @{named_theorems "𝒯_def"} @
@{thms
list_ex_iff
fun_upd_other
field_lookup_typ_uinfo_t_Some
fold_typ_uinfo_t
exists_nat_numeral}
in
Cached_Theory_Simproc.declare_init_thy_simpset @{named_theorems "𝒯_def"} unfold_ss
end
›
simproc_setup 𝒯 (‹map_of 𝒯 (typ_uinfo_t TYPE('a::mem_type))› | ‹map fst 𝒯› | ‹set 𝒯›) = ‹
let
exception Abort;
fun cache_simproc augment ctxt =
let val umm_ctxt = Cached_Theory_Simproc.put_time_warp_simpset' @{named_theorems "𝒯_def"} ctxt
in Cached_Theory_Simproc.gen_simproc (umm_ctxt, Cached_Theory_Simproc.recert, Cached_Theory_Simproc.add_cache) augment end
in
fn phi => fn ctxt => fn ct =>
let
val check =
Match_Cterm.switch [
(@{cterm_morph_match "map_of 𝒯 (typ_uinfo_t ?T)"} phi) #> (fn {T, ...} =>
if UMM_Proofs.is_ctype (Thm.term_of T) then () else raise Abort)
, fn _ => ()];
val _ = check ct
val _ = Utils.verbose_msg 3 ctxt (fn _ =>
"𝒯 invoked: " ^ Syntax.string_of_term ctxt (Thm.term_of ct))
in
cache_simproc (K single) ctxt ct
end handle Match => NONE | Abort => NONE
end
›
end
lemma fold_field_lvalue:
"x + word_of_nat (field_offset_untyped (typ_uinfo_t TYPE('a::c_type)) f) = &(PTR('a) x→f)"
by (simp add: field_lvalue_def field_offset_def)
lemma field_lvalue_same_root_ptr_conv:
"&(p::'a:: c_type ptr→f) = &(q::'a:: c_type ptr→f) ⟷ p = q"
by (auto simp add: field_lvalue_same_conv)
lemma ptr_exhaust_eq: fixes p::"'a::c_type ptr" shows "PTR('a) (ptr_val p) = p"
by (cases p) simp
lemma fold_exists_ptr: "(∃x. P (PTR('a::c_type) x)) ⟷ (∃q. P q)"
by (metis ptr.exhaust)
subsection ‹Syntax ‹PTR_VALID('a)››
context open_types
begin
text ‹We want to provide syntax that makes the type of \<^const>‹ptr_valid› visible on the term level for
interpretations of the @{locale open_types}.
This is a bit tricky as Isabelle does not (yet) provide local syntax and local print / parse translations.
We implement it by a combination of theory level syntax and translations and a local
declarations for the interpretations.
›
end
syntax
"_ptr_valid" :: "type ⇒ logic" (‹(‹indent=1 notation=‹mixfix PTR_VALID››PTR'_VALID/(1'(_')))›)
ML ‹
structure Ptr_Valid_Translation =
struct
val show_ptr_valid = Attrib.setup_config_bool @{binding show_ptr_valid} (K true)
val ptr_validN = @{const_name open_types.ptr_valid} |> Long_Name.base_name
val local_ptr_validN = Long_Name.qualify Long_Name.localN ptr_validN
type options = {ptr_valid:term, ptr_valid_name: string} option
fun ptr_valid_term NONE ctxt = Syntax.read_term ctxt local_ptr_validN
| ptr_valid_term (SOME {ptr_valid, ...}) _ = ptr_valid
fun instantiate_ptr_valid opt ctxt typ =
let
val \<^Const_>‹open_types.ptr_valid _ for T› = ptr_valid_term opt ctxt
in
\<^Const>‹open_types.ptr_valid typ for T›
end
fun const_name check ctxt s =
let
val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s
val res = check (Proof_Context.consts_of ctxt, c)
handle TYPE (msg, _, _) => error (msg ^ Position.here ⌂);
in
res
end
fun const_syntax (SOME {ptr_valid_name, ...}) ctxt =
const_name (fn (_, c) => Lexicon.mark_const c) ctxt ptr_valid_name
| const_syntax NONE ctxt =
Lexicon.mark_const local_ptr_validN
fun gen_ptr_valid_tr' ptr_valid ctxt T ts = if Config.get ctxt show_ptr_valid then
let
val ptr_valid' as \<^Const_>‹open_types.ptr_valid typ for _› =
Syntax.read_term ctxt ptr_validN
val [_, \<^Type>‹ptr typ›] = T |> binder_types
val head = Syntax.const \<^syntax_const>‹_ptr_valid› $ Syntax_Phases.term_of_typ ctxt typ
in
Term.betapplys (head, ts)
end
handle Bind => raise Match
else raise Match
fun add_ptr_valid_print_translation (opt:options) thy =
let
val ctxt = Proof_Context.init_global thy
val const_syntax = const_syntax opt ctxt
val ptr_valid = instantiate_ptr_valid opt
in
thy |> Sign.typed_print_translation [(const_syntax, gen_ptr_valid_tr' ptr_valid)]
end
end›
parse_translation ‹
let
fun ptr_valid_tr ctxt [t] =
let
val \<^Const_>‹open_types.ptr_valid _ for T › =
Syntax.read_term ctxt Ptr_Valid_Translation.ptr_validN
val typ = Syntax_Phases.decode_typ t
in
\<^Const>‹open_types.ptr_valid typ› $ T
end
handle Bind => error ("PTR_VALID: no instance of ptr_valid in context ")
in
[(\<^syntax_const>‹_ptr_valid›, ptr_valid_tr)]
end›
setup ‹Ptr_Valid_Translation.add_ptr_valid_print_translation NONE›
text ‹This theory level setup actually provides the local syntax when working within
a locale like @{locale open_types}. The ‹print_translation› is
triggered on constant (abbreviation) ‹local.ptr_valid››
context open_types
begin
term "PTR_VALID(32 word)"
declaration ‹fn phi => fn context =>
let
val ptr_valid = Morphism.term phi \<^term>‹ptr_valid›
val ptr_valid_name = Morphism.binding phi (Binding.make (Ptr_Valid_Translation.ptr_validN, ⌂))
|> Binding.name_of
val opt = SOME {ptr_valid = ptr_valid, ptr_valid_name = ptr_valid_name}
in
context |> Context.mapping (Ptr_Valid_Translation.add_ptr_valid_print_translation opt) I
end›
text ‹This declaration provides the setup for global interpretations. The print translation
is triggered on constant (abbreviation) ‹<instance-name>.ptr_valid› introduced by the
iterpretation.
Keep in mind, that when printing a term on the internal @{term "open_types.ptr_valid 𝒯"} first
the notations / abbreviatons are applied. These introduce the syntactic constant \<^term>‹ptr_valid›
on which the translation then triggers.
›
end
subsection ‹Syntax ‹IS_VALID('a)››
context open_types
begin
text ‹Building on top of ‹PTR_VALID› we provide syntax that also takes the ‹heap_typing› of
lifted globals into accound: ‹IS_VALID(32 word) s p› is translated to \<^term>‹ptr_valid (heap_typing s) p›
Note that \<^term>‹heap_typing› is a field of the lifted globals record that is defined later.
›
end
syntax
"_is_valid" :: "type ⇒ logic ⇒ logic"
(‹(‹indent=1 notation=‹mixfix IS_VALID››IS'_VALID/(1'(_'))) _› [0, 1000] 1000)
parse_translation ‹
let
fun is_valid_tr ctxt [t, s] =
let
val \<^Const_>‹open_types.ptr_valid _ for T › =
Syntax.read_term ctxt Ptr_Valid_Translation.ptr_validN
val typ = Syntax_Phases.decode_typ t
in ( \<^Const>‹open_types.ptr_valid typ› $ T) $ ((Const (AC_Names.heap_typingN, dummyT)) $ s) end
handle Bind => error ("IS_VALID: no instance of ptr_valid in context ")
in
[(\<^syntax_const>‹_is_valid›, is_valid_tr)]
end
›
print_translation ‹
let
val show_is_valid = Attrib.setup_config_bool @{binding show_is_valid} (K true)
fun is_valid_tr' ctxt (typ::Const (marked_heap_typing_name, heap_typingT)$s::ts) =
if Config.get ctxt show_is_valid then
let
val heap_typing_name = \<^try>‹Lexicon.unmark_const marked_heap_typing_name
catch _ => raise Match›
val _ = if Long_Name.base_name heap_typing_name = AC_Names.heap_typingN then () else raise Match
in
Term.betapplys (Syntax.const \<^syntax_const>‹_is_valid› $ typ $ s, ts)
end
else raise Match
in
[(\<^syntax_const>‹_ptr_valid›, is_valid_tr')]
end
›
end