Theory 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