Theory TypHeapSimple
chapter ‹IO phase: In/Out Parameters›
section ‹Heap Typing for Split Heap›
theory TypHeapSimple
imports
"AutoCorres_Base"
begin
section ‹Valid root footprint›
lemma c_null_guard_size_of_limit:
"c_null_guard (p::'a::c_type ptr) ⟹ size_td (typ_uinfo_t (TYPE('a))) < 2 ^ len_of TYPE(addr_bitsize) "
unfolding c_null_guard_def size_of_def
by (metis (no_types, opaque_lifting) add.commute add_diff_cancel_left' add_lessD1
cancel_comm_monoid_add_class.diff_cancel first_in_intvl nat_less_le nat_neq_iff
not_add_less1 typ_uinfo_size unat_lt2p unsigned_eq_0_iff zero_not_in_intvl_no_overflow)
lemma root_ptr_valid_legacy_def: "root_ptr_valid d p ⟷
valid_root_footprint d (ptr_val (p::'a ptr)) (typ_uinfo_t TYPE('a)) ∧
valid_simple_footprint d (ptr_val (p::'a::c_type ptr)) (typ_uinfo_t TYPE('a)) ∧
d, c_guard ⊨⇩t p"
using c_null_guard_size_of_limit [of p]
by (auto simp add: root_ptr_valid_def c_guard_def addr_card_len_of_conv
h_t_valid_def valid_root_footprint_valid_footprint intro!: valid_root_footprint_valid_simple_footprint)
definition
simple_lift :: "heap_raw_state ⇒ ('a::c_type) ptr ⇒ 'a option"
where
"simple_lift s p = (
if (root_ptr_valid (hrs_htd s) p) then
(Some (h_val (hrs_mem s) p))
else
None)"
lemma simple_lift_root_ptr_valid:
"simple_lift s p = Some x ⟹ root_ptr_valid (hrs_htd s) p"
apply (clarsimp simp: simple_lift_def split: if_split_asm)
done
lemma simple_lift_h_t_valid:
"simple_lift s p = Some x ⟹ (hrs_htd s), c_guard ⊨⇩t p"
apply (clarsimp simp: simple_lift_def root_ptr_valid_legacy_def split: if_split_asm)
done
lemma :
"simple_lift s (p::'a::c_type ptr) = Some x ⟹ valid_root_footprint (hrs_htd s) (ptr_val p) (typ_uinfo_t (TYPE('a)))"
apply (clarsimp simp: simple_lift_def root_ptr_valid_def split: if_split_asm)
done
lemma simple_lift_c_guard:
assumes lift: "simple_lift s p = Some x"
shows "c_guard p"
using simple_lift_h_t_valid [OF lift]
by (simp add: h_t_valid_def)
lemma root_ptr_valid_heap_update_other:
assumes val_p: "root_ptr_valid d (p::'a::mem_type ptr)"
and val_q: "root_ptr_valid d (q::'b::c_type ptr)"
and neq: "ptr_val p ≠ ptr_val q"
shows "h_val (heap_update p v h) q = h_val h q"
apply (clarsimp simp: h_val_def heap_update_def)
apply (subst heap_list_update_disjoint_same)
apply simp
apply (rule root_ptr_valid_neq_disjoint [OF val_p val_q neq])
apply simp
done
lemma root_ptr_valid_heap_update_other_typ:
assumes val_p: "root_ptr_valid d (p::'a::mem_type ptr)"
and val_q: "root_ptr_valid d (q::'b::c_type ptr)"
and neq: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b)"
shows "h_val (heap_update p v h) q = h_val h q"
apply (clarsimp simp: h_val_def heap_update_def)
apply (subst heap_list_update_disjoint_same)
apply simp
apply (rule root_ptr_valid_type_neq_disjoint [OF val_p val_q neq])
apply simp
done
lemma simple_lift_heap_update:
"⟦ root_ptr_valid (hrs_htd h) p ⟧ ⟹
simple_lift (hrs_mem_update (heap_update p v) h)
= (simple_lift h)(p := Some (v::'a::mem_type))"
apply (rule ext)
apply (clarsimp simp: simple_lift_def hrs_mem_update h_val_heap_update)
apply (fastforce simp: root_ptr_valid_heap_update_other)
done
lemma simple_lift_heap_update_other:
"⟦ root_ptr_valid (hrs_htd d) (p::'b::mem_type ptr);
typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b) ⟧ ⟹
simple_lift (hrs_mem_update (heap_update p v) d) = ((simple_lift d)::'a::c_type typ_heap)"
apply (rule ext)+
apply (clarsimp simp: simple_lift_def h_val_heap_update hrs_mem_update)
apply (auto intro: root_ptr_valid_heap_update_other_typ)
done
lemma h_val_simple_lift:
"simple_lift h p = Some v ⟹ h_val (hrs_mem h) p = v"
apply (clarsimp simp: simple_lift_def split: if_split_asm)
done
lemma the_simple_lift_h_val_conv:
"root_ptr_valid (hrs_htd h) p ⟹ the (simple_lift h p) = h_val (hrs_mem h) p"
apply (clarsimp simp: simple_lift_def split: if_split_asm)
done
lemma slift_clift_Some_same:
assumes slift: "simple_lift s p = Some x"
assumes clift: "clift s p = Some y"
shows "x = y"
using h_val_simple_lift [OF slift] h_val_clift' [OF clift]
by simp
lemma simple_lift_Some_clift_Some:
assumes slift: "simple_lift s p = Some x"
shows "clift s p = Some x"
using simple_lift_h_t_valid [OF slift] h_t_valid_clift_Some_iff slift_clift_Some_same [OF slift]
by (cases s) auto
lemma h_val_field_simple_lift:
"⟦ simple_lift h (pa :: 'a ptr) = Some (v::'a::mem_type);
field_ti TYPE('a) f = Some t;
export_uinfo (the (field_ti TYPE('a) f)) = export_uinfo (typ_info_t TYPE('b :: mem_type)) ⟧ ⟹
h_val (hrs_mem h) (Ptr &(pa→f) :: 'b :: mem_type ptr) = from_bytes (access_ti⇩0 (the (field_ti TYPE('a) f)) v)"
apply (clarsimp simp: simple_lift_def split: if_split_asm)
apply (clarsimp simp: h_val_field_from_bytes)
done
lemma simple_lift_heap_update':
"simple_lift h p = Some v' ⟹
simple_lift (hrs_mem_update (heap_update (p::('a::{mem_type}) ptr) v) h)
= (simple_lift h)(p := Some v)"
apply (rule simple_lift_heap_update)
apply (erule simple_lift_root_ptr_valid)
done
lemma simple_lift_hrs_mem_update_None [simp]:
"(simple_lift (hrs_mem_update a hp) x = None) = (simple_lift hp x = None)"
apply (clarsimp simp: simple_lift_def)
done
lemma simple_lift_hrs_mem_update_Some: " (∃z. simple_lift (hrs_mem_update upd h) x = Some z)
⟷ (∃z. simple_lift h x = Some z)"
apply (cases "simple_lift h x")
apply simp
apply (cases "simple_lift (hrs_mem_update upd h) x")
apply (auto)
done
lemma clift_hrs_mem_update_None [simp]:
"(clift (hrs_mem_update a hp) x = None) = (clift hp x = None)"
using h_t_valid_clift_Some_iff
apply (cases hp)
apply (clarsimp simp add: hrs_mem_update)
apply (metis hrs_htd_def hrs_htd_mem_update lift_t_if option.distinct(1) prod.collapse)+
done
lemma clift_hrs_mem_update_Some:
"(∃z. clift (hrs_mem_update a hp) x = Some z) = (∃z. clift hp x = Some z)"
apply (cases "clift hp x")
apply simp
apply (cases "clift (hrs_mem_update a hp) x")
apply (auto)
done
lemma simple_lift_data_eq:
"⟦ h_val (hrs_mem h) p = h_val (hrs_mem h') p';
root_ptr_valid (hrs_htd h) p = root_ptr_valid (hrs_htd h') p' ⟧ ⟹
simple_lift h p = simple_lift h' p'"
apply (clarsimp simp: simple_lift_def)
done
lemma h_val_heap_update_disjoint:
"⟦ {ptr_val p ..+ size_of TYPE('a::c_type)}
∩ {ptr_val q ..+ size_of TYPE('b::mem_type)} = {} ⟧ ⟹
h_val (heap_update (q :: 'b ptr) r h) (p :: 'a ptr) = h_val h p"
apply (clarsimp simp: h_val_def)
apply (clarsimp simp: heap_update_def)
apply (subst heap_list_update_disjoint_same)
apply clarsimp
apply blast
apply clarsimp
done
lemma update_ti_t_valid_size:
"size_of TYPE('b) = size_td t ⟹
update_ti_t t (to_bytes_p (val::'b::mem_type)) obj = update_ti t (to_bytes_p val) obj"
apply (clarsimp simp: update_ti_t_def to_bytes_p_def)
done
lemma h_val_field_from_bytes':
"⟦ field_ti TYPE('a::{mem_type}) f = Some t;
export_uinfo t = export_uinfo (typ_info_t TYPE('b::{mem_type})) ⟧ ⟹
h_val h (Ptr &(pa→f) :: 'b ptr) = from_bytes (access_ti⇩0 t (h_val h pa))"
apply (insert h_val_field_from_bytes[where f=f and pa=pa and t=t and h="(h,x)"
and 'a='a and 'b='b for x])
apply (clarsimp simp: hrs_mem_def)
done
lemma h_val_field_from_root:
fixes p::"'a:: mem_type ptr"
assumes fl:
"field_lookup (typ_info_t TYPE('a::{mem_type})) f 0 =
Some (adjust_ti (typ_info_t TYPE('b::mem_type)) fld fld_update, n)"
assumes fg_cons: "fg_cons fld (fld_update)"
shows "h_val h (PTR('b) &(p→f)) = fld (h_val h p)"
proof -
from fl
have fl: "field_ti TYPE('a) f = Some (adjust_ti (typ_info_t TYPE('b::mem_type)) fld fld_update)"
using field_lookup_field_ti by blast
have exp: "export_uinfo (adjust_ti (typ_info_t TYPE('b)) fld fld_update) =
export_uinfo (typ_info_t TYPE('b))"
using fg_cons
by simp
from h_val_field_from_bytes' [OF fl exp]
show ?thesis
by simp
qed
lemma simple_lift_super_field_update_lookup:
fixes dummy :: "'b :: mem_type"
assumes "field_lookup (typ_info_t TYPE('b::mem_type)) f 0 = Some (s,n)"
and "typ_uinfo_t TYPE('a) = export_uinfo s"
and "simple_lift h p = Some v'"
shows "(super_field_update_t (Ptr (&(p→f))) (v::'a::mem_type) ((simple_lift h)::'b ptr ⇒ 'b option)) =
((simple_lift h)(p ↦ field_update (field_desc s) (to_bytes_p v) v'))"
proof -
from assms have [simp]: "unat (of_nat n :: addr) = n"
apply (subst unat_of_nat)
apply (subst mod_less)
apply (drule td_set_field_lookupD)+
apply (drule td_set_offset_size)+
apply (subst len_of_addr_card)
apply (subst (asm) size_of_def [symmetric, where t="TYPE('b)"])+
apply (subgoal_tac "size_of TYPE('b) < addr_card")
apply arith
apply simp
apply simp
done
from assms show ?thesis
supply unsigned_of_nat [simp del]
apply (clarsimp simp: super_field_update_t_def)
apply (rule ext)
apply (clarsimp simp: field_lvalue_def split: option.splits)
apply (safe, simp_all)
apply (frule_tac v=v and v'=v' in update_field_update)
apply (clarsimp simp: field_of_t_def field_of_def typ_uinfo_t_def)
apply (frule_tac m=0 in field_names_SomeD2)
apply simp
apply clarsimp
apply (simp add: field_typ_def field_typ_untyped_def)
apply (frule field_lookup_export_uinfo_Some)
apply (frule_tac s=k in field_lookup_export_uinfo_Some)
apply simp
apply (drule (1) field_lookup_inject)
apply (subst typ_uinfo_t_def [symmetric, where t="TYPE('b)"])
apply simp
apply simp
apply (drule field_of_t_mem)+
apply (cases h)
apply (clarsimp simp: simple_lift_def split: if_split_asm)
apply (drule (1) root_ptr_valid_neq_disjoint)
apply simp
apply fast
apply (clarsimp simp: field_of_t_def field_of_def)
apply (subst (asm) td_set_field_lookup)
apply simp
apply simp
apply (frule field_lookup_export_uinfo_Some)
apply (simp add: typ_uinfo_t_def)
apply (clarsimp simp: field_of_t_def field_of_def)
apply (subst (asm) td_set_field_lookup)
apply simp
apply simp
apply (frule field_lookup_export_uinfo_Some)
apply (simp add: typ_uinfo_t_def)
done
qed
lemma field_offset_addr_card:
"∃x. field_lookup (typ_info_t TYPE('a::mem_type)) f 0 = Some x
⟹ field_offset TYPE('a) f < addr_card"
apply (clarsimp simp: field_offset_def field_offset_untyped_def typ_uinfo_t_def)
apply (subst field_lookup_export_uinfo_Some)
apply assumption
apply (frule td_set_field_lookupD)
apply (drule td_set_offset_size)
apply (insert max_size [where ?'a="'a"])
apply (clarsimp simp: size_of_def)
done
lemma unat_of_nat_field_offset:
"∃x. field_lookup (typ_info_t TYPE('a::mem_type)) f 0 = Some x ⟹
unat (of_nat (field_offset TYPE('a) f) :: addr) = field_offset TYPE('a) f"
apply (subst word_unat.Abs_inverse)
apply (clarsimp simp: unats_def)
apply (insert field_offset_addr_card [where f=f and ?'a="'a"])[1]
apply (fastforce simp: addr_card)
apply simp
done
lemma field_of_t_field_lookup:
assumes a: "field_lookup (typ_info_t TYPE('a::mem_type)) f 0 = Some (s, n)"
assumes b: "export_uinfo s = typ_uinfo_t TYPE('b::mem_type)"
assumes n: "n = field_offset TYPE('a) f"
shows "field_of_t (Ptr &(ptr→f) :: ('b ptr)) (ptr :: 'a ptr)"
supply unsigned_of_nat [simp del]
apply (clarsimp simp del: field_lookup_offset_eq
simp: field_of_t_def field_of_def)
apply (subst td_set_field_lookup)
apply (rule wf_desc_typ_tag)
apply (rule exI [where x=f])
using a[simplified n] b
apply (clarsimp simp: typ_uinfo_t_def)
apply (subst field_lookup_export_uinfo_Some)
apply assumption
apply (clarsimp simp del: field_lookup_offset_eq
simp: field_lvalue_def unat_of_nat_field_offset)
done
lemma simple_lift_field_update':
fixes val :: "'b :: mem_type" and ptr :: "'a :: mem_type ptr"
assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 =
Some (adjust_ti (typ_info_t TYPE('b)) xf xfu, n)"
and xf_xfu: "fg_cons xf xfu"
and cl: "simple_lift hp ptr = Some z"
shows "(simple_lift (hrs_mem_update (heap_update (Ptr &(ptr→f)) val) hp)) =
(simple_lift hp)(ptr ↦ xfu val z)"
(is "?LHS = ?RHS")
proof (rule ext)
fix p
have eui: "typ_uinfo_t TYPE('b) =
export_uinfo (adjust_ti (typ_info_t TYPE('b)) xf xfu)"
using xf_xfu
apply (subst export_tag_adjust_ti2 [OF _ wf_lf wf_desc])
apply (simp add: fg_cons_def )
apply (rule meta_eq_to_obj_eq [OF typ_uinfo_t_def])
done
have n_is_field_offset: "n = field_offset TYPE('a) f"
apply (insert field_lookup_offset_eq [OF fl])
apply (clarsimp)
done
have equal_case: "?LHS ptr = ?RHS ptr"
supply unsigned_of_nat [simp del]
apply (insert cl)
apply (clarsimp simp: simple_lift_def split: if_split_asm)
apply (clarsimp simp: hrs_mem_update)
apply (subst h_val_super_update_bs)
apply (rule field_of_t_field_lookup [OF fl])
apply (clarsimp simp: eui)
apply (clarsimp simp: n_is_field_offset)
apply clarsimp
apply (unfold from_bytes_def)
apply (subst fi_fu_consistentD [where f=f and s="adjust_ti (typ_info_t TYPE('b)) xf xfu"])
apply (clarsimp simp: fl)
apply (clarsimp simp: n_is_field_offset field_lvalue_def)
apply (metis unat_of_nat_field_offset fl)
apply clarsimp
apply (clarsimp simp: size_of_def)
apply (clarsimp simp: size_of_def)
apply clarsimp
apply (subst update_ti_s_from_bytes)
apply clarsimp
apply (subst update_ti_t_adjust_ti)
apply (rule xf_xfu)
apply (subst update_ti_s_from_bytes)
apply clarsimp
apply clarsimp
apply (clarsimp simp: h_val_def)
done
show "?LHS p = ?RHS p"
apply (cases "p = ptr")
apply (erule ssubst)
apply (rule equal_case)
apply (insert cl)
apply (clarsimp simp: simple_lift_def hrs_mem_update split: if_split_asm)
apply (rule h_val_heap_update_disjoint)
apply (insert field_tag_sub [OF fl, where p=ptr])
apply (clarsimp simp: size_of_def)
apply (clarsimp simp: root_ptr_valid_legacy_def)
apply (frule (1) valid_simple_footprint_neq_disjoint, fastforce)
apply clarsimp
apply blast
done
qed
lemma simple_lift_field_update:
fixes val :: "'b :: mem_type" and ptr :: "'a :: mem_type ptr"
assumes fl: "field_ti TYPE('a) f =
Some (adjust_ti (typ_info_t TYPE('b)) xf (xfu o (λx _. x)))"
and xf_xfu: "fg_cons xf (xfu o (λx _. x))"
and cl: "simple_lift hp ptr = Some z"
shows "(simple_lift (hrs_mem_update (heap_update (Ptr &(ptr→f)) val) hp)) =
(simple_lift hp)(ptr ↦ xfu (λ_. val) z)"
(is "?LHS = ?RHS")
apply (insert fl [unfolded field_ti_def])
apply (clarsimp split: option.splits)
apply (subst simple_lift_field_update' [where xf=xf and xfu="xfu o (λx _. x)" and z=z])
apply (clarsimp simp: o_def split: option.splits)
apply (rule refl)
apply (rule xf_xfu)
apply (rule cl)
apply clarsimp
done
lemma simple_heap_diff_types_impl_diff_ptrs:
"⟦ root_ptr_valid h (p::('a::c_type) ptr);
root_ptr_valid h (q::('b::c_type) ptr);
typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b) ⟧ ⟹
ptr_val p ≠ ptr_val q"
apply (clarsimp simp: root_ptr_valid_legacy_def)
apply (clarsimp simp: valid_simple_footprint_def)
done
lemma h_val_update_regions_disjoint:
"⟦ { ptr_val p ..+ size_of TYPE('a) } ∩ { ptr_val x ..+ size_of TYPE('b)} = {} ⟧ ⟹
h_val (heap_update p (v::('a::mem_type)) h) x = h_val h (x::('b::c_type) ptr)"
apply (clarsimp simp: heap_update_def)
apply (clarsimp simp: h_val_def)
apply (subst heap_list_update_disjoint_same)
apply clarsimp
apply clarsimp
done
lemma h_val_heap_update_padding_disjoint:
fixes p::"'a::mem_type ptr"
fixes q::"'b::c_type ptr"
shows "⟦ ptr_span p ∩ ptr_span q = {}; length bs = size_of TYPE('a) ⟧ ⟹
h_val (heap_update_padding p v bs h) q = h_val h q"
apply (clarsimp simp: heap_update_padding_def)
apply (clarsimp simp: h_val_def)
apply (subst heap_list_update_disjoint_same)
apply clarsimp
apply clarsimp
done
lemma simple_lift_field_update_t:
fixes val :: "'b :: mem_type" and ptr :: "'a :: mem_type ptr"
assumes fl: "field_ti TYPE('a) f = Some t"
and diff: "typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('c :: c_type)"
and eu: "export_uinfo t = export_uinfo (typ_info_t TYPE('b))"
and cl: "simple_lift hp ptr = Some z"
shows "((simple_lift (hrs_mem_update (heap_update (Ptr &(ptr→f)) val) hp)) :: 'c ptr ⇒ 'c option) =
simple_lift hp"
apply (rule ext)
subgoal for x
apply (cases "simple_lift hp x")
apply clarsimp
apply (cases "ptr_val x = ptr_val ptr")
apply clarsimp
apply (clarsimp simp: simple_lift_def hrs_mem_update split: if_split_asm)
apply (cut_tac simple_lift_root_ptr_valid [OF cl])
apply (drule (1) simple_heap_diff_types_impl_diff_ptrs [OF _ _ diff])
apply simp
apply (clarsimp simp: simple_lift_def hrs_mem_update split: if_split_asm)
apply (rule field_ti_field_lookupE [OF fl])
apply (frule_tac p=ptr in field_tag_sub)
apply (clarsimp simp: h_val_def heap_update_def)
apply (subst heap_list_update_disjoint_same)
apply clarsimp
apply (cut_tac simple_lift_root_ptr_valid [OF cl])
apply (drule (2) root_ptr_valid_neq_disjoint)
apply (clarsimp simp: export_size_of [unfolded typ_uinfo_t_def, OF eu])
apply blast
apply simp
done
done
lemma simple_lift_heap_update_other':
"⟦ simple_lift h (p::'b::mem_type ptr) = Some v';
typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b) ⟧ ⟹
simple_lift (hrs_mem_update (heap_update p v) h) = ((simple_lift h)::'a::c_type typ_heap)"
apply (rule simple_lift_heap_update_other)
apply (erule simple_lift_root_ptr_valid)
apply simp
done
lemma simple_lift_heap_update_bytes_in_other:
"⟦ simple_lift h (p::'b::mem_type ptr) = Some v';
typ_uinfo_t TYPE('b) ≠ typ_uinfo_t TYPE('c);
{ ptr_val q ..+ size_of TYPE('a)} ⊆ {ptr_val p ..+ size_of TYPE('b) } ⟧ ⟹
simple_lift (hrs_mem_update (heap_update (q::'a::mem_type ptr) v) h) = ((simple_lift h)::'c::mem_type typ_heap)"
apply (rule ext)
apply (clarsimp simp: simple_lift_def split: if_split_asm)
apply (drule (1) root_ptr_valid_type_neq_disjoint, simp)
apply (clarsimp simp: hrs_mem_update)
apply (rule h_val_heap_update_disjoint)
apply blast
done
lemma typ_name_neq:
"typ_name (export_uinfo (typ_info_t TYPE('a::c_type)))
≠ typ_name (export_uinfo (typ_info_t TYPE('b::c_type)))
⟹ typ_uinfo_t TYPE('a) ≠ typ_uinfo_t TYPE('b)"
apply (metis typ_uinfo_t_def)
done
lemma of_nat_mod_div_decomp:
"of_nat k
= of_nat (k div size_of TYPE('b)) * of_nat (size_of TYPE('b::mem_type)) +
of_nat (k mod size_of TYPE('b))"
by (metis mod_div_decomp of_nat_add of_nat_mult)
lemma c_guard_array_c_guard:
"⟦ ⋀x. x < CARD('a) ⟹ c_guard (ptr_coerce p +⇩p int x :: 'b ptr) ⟧ ⟹ c_guard ( p :: ('b :: mem_type, 'a :: finite) array ptr)"
apply atomize
apply (clarsimp simp: c_guard_def)
apply (rule conjI)
apply (drule_tac x=0 in spec)
apply (clarsimp simp: ptr_aligned_def align_of_def align_td_array)
apply (simp add: c_null_guard_def)
apply (clarsimp simp: intvl_def)
apply (drule_tac x="k div size_of TYPE('b)" in spec)
apply (erule impE)
apply (metis (full_types) less_nat_zero_code mult_is_0 neq0_conv td_gal_lt)
apply clarsimp
apply (drule_tac x="k mod size_of TYPE('b)" in spec)
apply (clarsimp simp: CTypesDefs.ptr_add_def)
apply (subst (asm) add.assoc)
apply (subst (asm) of_nat_mod_div_decomp [symmetric])
apply clarsimp
done
lemma heap_list_update_list':
"⟦ n + x ≤ length v; length v < addr_card; q = (p + of_nat x) ⟧ ⟹
heap_list (heap_update_list p v h) n q = take n (drop x v)"
by (metis heap_list_update_list)
lemma outside_intvl_range:
"p ∉ {a ..+ b} ⟹ p < a ∨ p ≥ a + of_nat b"
apply (clarsimp simp: intvl_def not_le not_less)
apply (drule_tac x="unat (p-a)" in spec)
apply clarsimp
apply (metis add_diff_cancel2 le_less_linear le_unat_uoi
mpl_lem not_add_less2 unat_mono word_less_minus_mono_left)
done
lemma root_ptr_valid_intersect_array:
"⟦ ∀j < n. root_ptr_valid htd (p +⇩p int j);
root_ptr_valid htd (q :: ('a :: c_type) ptr) ⟧
⟹ (∃m < n. q = (p +⇩p int m))
∨ ({ptr_val p ..+ size_of TYPE ('a) * n} ∩ {ptr_val q ..+ size_of TYPE ('a :: c_type)} = {})"
apply (induct n)
apply clarsimp
subgoal for n
apply atomize
apply simp
apply (cases "n = 0")
apply clarsimp
apply (metis root_ptr_valid_neq_disjoint ptr_val_inj)
apply (erule disjE)
apply (metis less_Suc_eq)
apply (cases "q = p +⇩p int n")
apply force
apply (frule_tac x=n in spec)
apply (erule impE, simp)
apply (drule (1) root_ptr_valid_neq_disjoint)
apply simp
apply (simp add: CTypesDefs.ptr_add_def)
apply (rule disjI2)
apply (cut_tac a=" of_nat n * of_nat (size_of TYPE('a))"
and p="ptr_val p" and n="n * size_of TYPE('a) + size_of TYPE('a)" in intvl_split)
apply clarsimp
apply (clarsimp simp: field_simps Int_Un_distrib2)
apply (metis IntI emptyE intvl_empty intvl_inter intvl_self neq0_conv)
done
done
lemmas simple_lift_simps =
typ_name_neq
simple_lift_c_guard
h_val_simple_lift
simple_lift_heap_update
simple_lift_heap_update_other
c_guard_field
h_val_field_simple_lift
simple_lift_field_update
simple_lift_field_update_t
c_guard_array_field
lemmas typ_simple_heap_simps = simple_lift_simps
lemma :
assumes valid_p: "valid_footprint d (ptr_val (p::'a::mem_type ptr)) (typ_uinfo_t TYPE('a))"
assumes valid_q: "valid_footprint d (ptr_val (q::'b::mem_type ptr)) (typ_uinfo_t TYPE('b))"
assumes overlap: "ptr_span p ∩ ptr_span q ≠ {}"
shows "TYPE('a) ≤⇩τ TYPE('b) ∨ TYPE('b) ≤⇩τ TYPE('a)"
proof (cases "typ_uinfo_t (TYPE('a)) = typ_uinfo_t (TYPE('b))")
case True
thus ?thesis by (simp add: sub_typ_def)
next
case False
note not_eq = False
show ?thesis
proof (cases "TYPE('a) ⊥⇩τ TYPE('b)")
case False
thus ?thesis by (simp add: tag_disj_typ_def tag_disj_def sub_typ_def)
next
case True
note disj_types = True
with disj_types not_eq have ne_le_b_a: "¬ typ_uinfo_t (TYPE('b)) < typ_uinfo_t (TYPE('a))"
apply (simp add: tag_disj_typ_def tag_disj_def)
by (meson le_less)
have not_field_of_p_q: "¬ field_of (ptr_val p - ptr_val q) (typ_uinfo_t (TYPE('a))) (typ_uinfo_t (TYPE('b)))"
apply (rule ccontr, simp)
apply (drule field_of_sub)
using disj_types
apply (simp add: tag_disj_typ_def tag_disj_def)
done
from valid_footprint_neq_disjoint [OF valid_p valid_q ne_le_b_a not_field_of_p_q]
have "ptr_span p ∩ ptr_span q = {}"
by (simp add: size_of_def)
with overlap show ?thesis by auto
qed
qed
lemma :
assumes valid_p: "valid_root_footprint d (ptr_val (p::'a:: mem_type ptr)) (typ_uinfo_t (TYPE('a)))"
assumes valid_q: "valid_footprint d (ptr_val (q::'b::mem_type ptr)) (typ_uinfo_t (TYPE('b)))"
assumes overlap: "ptr_span p ∩ ptr_span q ≠ {}"
shows "TYPE('b) ≤⇩τ TYPE('a)"
proof -
from overlap [simplified size_of_def, folded typ_uinfo_t_def]
have " {ptr_val p..+size_td (typ_uinfo_t TYPE('a))} ∩ {ptr_val q..+size_td (typ_uinfo_t TYPE('b))} ≠ {}"
by simp
from valid_root_footprint_overlap_sub_typ [OF valid_p valid_q this]
have "typ_uinfo_t TYPE('b) ≤ typ_uinfo_t TYPE('a)".
thus ?thesis
by (simp add: sub_typ_def)
qed
lemma :
assumes valid_root_x: "valid_root_footprint d x t"
assumes valid_y: "valid_footprint d y s"
assumes overlap: "{x ..+ size_td t} ∩ {y ..+ size_td s} ≠ {}"
shows "y ∈ {x ..+ size_td t}"
using valid_root_x overlap valid_y
apply (clarsimp simp add: valid_root_footprint_def valid_footprint_def Let_def typ_tag_le_def)
by (metis (no_types, opaque_lifting) intvl_inter intvl_inter_le le_less_trans less_irrefl overlap
valid_footprint_sub2 valid_root_footprint_overlap_sub_typ valid_root_footprint_valid_footprint valid_root_x valid_y zero_le)
lemma :
assumes valid_x: "valid_footprint d x t"
assumes field: "field_of off s t"
shows "{x + off ..+ size_td s} ⊆ {x ..+ size_td t}"
proof -
from field have "(s, unat off) ∈ td_set t 0"
by (simp add: field_of_def)
from td_set_offset_size [OF this] have "size_td s + unat off ≤ size_td t".
thus ?thesis
by (simp add: intvl_sub_offset)
qed
lemma :
assumes valid_root_x: "valid_root_footprint d x t"
assumes valid_y: "valid_footprint d y s"
assumes y: "y ∈ {x ..+ size_td t}"
shows "field_of (y - x) s t"
proof -
from y have "{x ..+ size_td t} ∩ {y ..+ size_td s} ≠ {}"
by (meson disjoint_iff intvl_self valid_footprint_def valid_y)
from valid_root_footprint_overlap_sub_typ [OF valid_root_x valid_y this]
have "s ≤ t" .
with y show ?thesis
by (meson le_less_trans less_irrefl valid_footprint_sub valid_root_footprint_valid_footprint valid_root_x valid_y)
qed
lemma :
assumes valid_root_x: "valid_root_footprint d x t"
assumes valid_y: "valid_footprint d y s"
assumes overlap: "{x ..+ size_td t} ∩ {y ..+ size_td s} ≠ {}"
shows "{y ..+ size_td s} ⊆ {x ..+ size_td t}"
proof -
from valid_root_footprint_overlap_contained [OF valid_root_x valid_y overlap]
have "y ∈ {x..+size_td t}" .
from valid_root_footprint_overlap_field_of [OF valid_root_x valid_y this]
have "field_of (y - x) s t" .
from valid_footprint_field_of_contained [OF valid_root_footprint_valid_footprint [OF valid_root_x] this]
have "{x + (y - x)..+size_td s} ⊆ {x..+size_td t}" .
then show ?thesis
by auto
qed
lemma :
assumes valid_p: "valid_footprint d p s"
assumes valid_q: "valid_footprint d q t"
assumes sub: "¬ t < s"
shows "{p..+size_td s} ∩ {q..+size_td t} = {} ∨ field_of (p - q) (s) (t)"
using valid_footprint_neq_disjoint valid_p valid_q sub by blast
lemma :
assumes valid_p: "valid_root_footprint d (ptr_val (p::'a:: mem_type ptr)) (typ_uinfo_t (TYPE('a)))"
assumes valid_q: "valid_footprint d (ptr_val (q::'b::mem_type ptr)) (typ_uinfo_t (TYPE('b)))"
assumes dist_type: "typ_uinfo_t (TYPE('a)) ≠ typ_uinfo_t (TYPE('b))"
assumes nested_case: "⋀f. f ∈ set (field_names_u (typ_uinfo_t (TYPE('a))) (typ_uinfo_t (TYPE('b)))) ⟹
field_lookup (typ_uinfo_t TYPE('a)) f 0 = Some (typ_uinfo_t TYPE('b), unat (ptr_val q - ptr_val p)) ⟹
field_of_t (PTR('b) &(p→f)) p ⟹
ptr_val q = &(p→f) ⟹
ptr_span q ⊆ ptr_span p ⟹ P"
assumes disj_case: "ptr_span p ∩ ptr_span q = {} ⟹ P"
shows P
proof (cases "ptr_span p ∩ ptr_span q = {}")
case True thus ?thesis by (rule disj_case)
next
case False
from valid_root_footprint_valid_footprint_overlap_case [OF valid_p valid_q False]
have le_b_a: "typ_uinfo_t TYPE('b) ≤ typ_uinfo_t TYPE('a)" by (simp add: sub_typ_def)
from sub_typ_field_names_u_nonempty [OF this]
obtain f where "f ∈ set (field_names_u (typ_uinfo_t (TYPE('a))) (typ_uinfo_t (TYPE('b))))"
by fastforce
from False have "{ptr_val p..+size_td (typ_uinfo_t TYPE('a))} ∩ {ptr_val q..+size_td (typ_uinfo_t TYPE('b))} ≠ {}"
by (simp add: size_of_def)
from valid_root_footprint_overlap_contained' [OF valid_p valid_q this]
have "{ptr_val q..+size_td (typ_uinfo_t TYPE('b))} ⊆ {ptr_val p..+size_td (typ_uinfo_t TYPE('a))}" .
hence "ptr_val q ∈ {ptr_val p..+size_td (typ_uinfo_t TYPE('a))}"
by (simp add: size_of_tag subsetD)
from valid_root_footprint_overlap_field_of [OF valid_p valid_q this]
have "field_of (ptr_val q - ptr_val p) (typ_uinfo_t TYPE('b)) (typ_uinfo_t TYPE('a)) " .
from field_of_lookup_info [OF this, of p]
obtain f where
"f ∈ set (field_names_u (typ_uinfo_t (TYPE('a))) (typ_uinfo_t (TYPE('b))))"
"field_lookup (typ_uinfo_t TYPE('a)) f 0 =
Some (typ_uinfo_t TYPE('b), unat (ptr_val q - ptr_val p))"
"field_of_t (PTR('b) &(p→f)) p"
"ptr_val q = &(p→f)"
"ptr_span q ⊆ ptr_span p"
by (auto simp add: size_of_def)
from nested_case [OF this]
show ?thesis .
qed
lemma cvalid_field_pres:
assumes lookup: "field_lookup (typ_uinfo_t TYPE('a::mem_type)) f 0 = Some (typ_uinfo_t TYPE('b::mem_type), n)"
assumes valid: "d,c_guard ⊨⇩t (p::'a:: mem_type ptr) "
shows "d, c_guard ⊨⇩t PTR('b) &(p→f)"
using field_lookup_export_uinfo_Some_rev [OF lookup [simplified typ_uinfo_t_def]]
apply (clarsimp)
apply (rule h_t_valid_mono [rule_format, OF _ _ c_guard_mono valid])
apply (auto simp add: typ_uinfo_t_def)
done
lemma cvalid_field_pres':
assumes ptr_val_eq: "ptr_val q = &(p→f)"
assumes lookup: "field_lookup (typ_uinfo_t TYPE('a::mem_type)) f 0 = Some (typ_uinfo_t TYPE('b::mem_type), n)"
assumes valid: "d,c_guard ⊨⇩t (p::'a:: mem_type ptr)"
shows "d, c_guard ⊨⇩t (q::'b ptr)"
proof -
from ptr_val_eq have "q = PTR('b) (&(p→f))"
by (cases q) (auto simp add: ptr_val_def)
with cvalid_field_pres [OF lookup valid]
show ?thesis
by simp
qed
lemma cvalid_field_pres'':
assumes ptr_val_eq: "ptr_val q = &(p→f)"
assumes lookup: "field_lookup (typ_info_t TYPE('a::mem_type)) f 0 = Some (s, n)"
assumes match: "export_uinfo s = typ_uinfo_t TYPE('b::mem_type)"
assumes valid: "d,c_guard ⊨⇩t (p::'a:: mem_type ptr)"
shows "d, c_guard ⊨⇩t (q::'b ptr)"
proof -
from cvalid_field_pres' [OF ptr_val_eq _ valid] lookup match
show ?thesis
by (simp add: UMM.field_lookup_typ_uinfo_t_Some)
qed
lemma cvalid_field_pres''':
assumes lookup: "field_lookup (typ_info_t TYPE('a::mem_type)) f 0 = Some (t, n)"
assumes match: "export_uinfo t = typ_uinfo_t TYPE('b::mem_type)"
assumes valid: "d,c_guard ⊨⇩t (p::'a:: mem_type ptr) "
shows "d, c_guard ⊨⇩t PTR('b) &(p→f)"
using lookup match valid
using c_guard_mono h_t_valid_mono by blast
lemma the_clift_eq_h_val_eq:
assumes h_val_eq: "hrs_htd hp ⊨⇩t p ⟹ h_val (hrs_mem (hrs_mem_update a hp)) p = h_val (hrs_mem hp) p"
shows "the (clift (hrs_mem_update a hp) p) = the (clift hp p)"
proof (cases "clift hp p")
case None
with clift_hrs_mem_update_None show ?thesis by metis
next
case (Some v)
with clift_hrs_mem_update_None obtain v' where "clift (hrs_mem_update a hp) p = Some v'"
by (cases "clift (hrs_mem_update a hp) p") auto
with Some h_val_clift' h_val_eq [OF h_t_valid_clift [OF Some]]
show ?thesis by metis
qed
lemma field_lvalue_same_conv: "&(p::'a:: c_type ptr→f) = &(q::'a:: c_type ptr→f) ⟹ p = q"
by (simp add: field_lvalue_def)
lemma ptr_val_field_convD: "ptr_val p = &(q→f) ⟹ p = Ptr &(q→f)"
by (cases p) auto
lemma ptr_val_field_conv: "ptr_val p = &(q→f) ⟷ p = Ptr &(q→f)"
by (cases p) auto
lemma ptr_val_array_index_convD:
"ptr_val p = ptr_val (array_ptr_index q False j) ⟹ p = array_ptr_index q False j"
by (cases p) auto
lemma ptr_val_conv': "ptr_coerce p = Ptr q ⟷ ptr_val p = q"
by (cases p) simp
lemma ptr_val_conv: "p = q ⟷ ptr_val p = ptr_val q"
by auto
lemma ptr_val_neq_conv: "p ≠ q ⟷ ptr_val p ≠ ptr_val q"
by auto
lemma the_simple_lift_strong_eqI:
fixes p::"'a::mem_type ptr"
fixes q::"'b::mem_type ptr"
assumes eq: "⋀x1 x2. root_ptr_valid (hrs_htd s) q ⟹
simple_lift s q = Some x1 ⟹
(simple_lift (hrs_mem_update (heap_update p v) s) q) = Some x2 ⟹
x1 = x2"
shows "the (simple_lift
(hrs_mem_update (heap_update p v) s) q) =
the (simple_lift s q)"
proof (cases "root_ptr_valid (hrs_htd s) q")
case True
with eq show ?thesis by (fastforce simp add: simple_lift_def)
next
case False
hence "simple_lift s q = None"
by (simp add: simple_lift_def)
with simple_lift_hrs_mem_update_None
show ?thesis by metis
qed
lemma the_simple_lift_hval_eqI:
fixes p::"'a::mem_type ptr"
fixes q::"'b::mem_type ptr"
assumes eq: "root_ptr_valid (hrs_htd s) q ⟹
(h_val ((heap_update p v) (hrs_mem s)) q) = h_val (hrs_mem s) q "
shows "the (simple_lift
(hrs_mem_update (heap_update p v) s) q) =
the (simple_lift s q)"
apply (rule the_simple_lift_strong_eqI)
apply (drule h_val_simple_lift)
apply (drule h_val_simple_lift)
apply (auto simp add: hrs_mem_update eq)
done
lemma h_t_valid_hrs_mem_update_pres: "hrs_htd s,g ⊨⇩t q ⟹
hrs_htd ((hrs_mem_update (heap_update p v) s)), g⊨⇩t q"
by (cases s) (auto simp add: hrs_htd_def hrs_mem_update_def)
lemma field_the_clift_hval_eqI:
fixes p::"'a::mem_type ptr"
fixes q::"'b::mem_type ptr"
assumes eq: "hrs_htd s, c_guard ⊨⇩t q ⟹
f (h_val ((heap_update p v) (hrs_mem s)) q) = f (h_val (hrs_mem s) q) "
shows "f (the (clift
(hrs_mem_update (heap_update p v) s) q)) =
f (the (clift s q))"
proof (cases "(clift s q)")
case None
then show ?thesis using clift_hrs_mem_update_None by metis
next
case (Some x)
from h_t_valid_clift [OF this] have valid: "hrs_htd s ⊨⇩t q" .
hence "hrs_htd ((hrs_mem_update (heap_update p v) s))⊨⇩t q"
by (rule h_t_valid_hrs_mem_update_pres)
with h_t_valid_clift_Some_iff
obtain y where y: "clift (hrs_mem_update (heap_update p v) s) q = Some y"
by blast
from h_val_clift' [OF Some] h_val_clift' [OF this] eq [OF valid]
show ?thesis by (auto simp add: Some y hrs_mem_update)
qed
lemma the_clift_hval_eqI:
fixes p::"'a::mem_type ptr"
fixes q::"'b::mem_type ptr"
assumes eq: "hrs_htd s, c_guard ⊨⇩t q ⟹
(h_val ((heap_update p v) (hrs_mem s)) q) = (h_val (hrs_mem s) q) "
shows "the (clift
(hrs_mem_update (heap_update p v) s) q) =
(the (clift s q))"
apply (rule field_the_clift_hval_eqI)
by (rule eq)
lemma :
assumes valid_p: "valid_root_footprint d (ptr_val (p::'a:: mem_type ptr)) (typ_uinfo_t (TYPE('a)))"
assumes valid_q: "valid_footprint d (ptr_val (q::'a::mem_type ptr)) (typ_uinfo_t (TYPE('a)))"
assumes eq_case: "p = q ⟹ P"
assumes disj_case: "ptr_span p ∩ ptr_span q = {} ⟹ P"
shows P
proof (cases "ptr_span p ∩ ptr_span q = {}")
case True
then show ?thesis by (simp add: disj_case)
next
case False
from valid_root_footprint_overlap_contained [OF valid_p valid_q ] False
have "ptr_val q ∈ ptr_span p"
by (simp add: typ_uinfo_t_def size_of_def)
hence "p = q"
by (metis ptr_val_conv size_of_tag valid_footprint_neq_nmem valid_p valid_q valid_root_footprint_valid_footprint)
thus ?thesis by (simp add: eq_case)
qed
lemma :
assumes valid_root_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 "y ∈ {x ..+ size_td t} ∨ x ∈ {y ..+ size_td s}"
using valid_root_x overlap valid_y
apply (clarsimp simp add: valid_footprint_def Let_def typ_tag_le_def)
by (meson intvl_inter overlap)
lemma :
assumes valid_p: "valid_footprint d (ptr_val (p::'a:: mem_type ptr)) (typ_uinfo_t (TYPE('a)))"
assumes valid_q: "valid_footprint d (ptr_val (q::'a::mem_type ptr)) (typ_uinfo_t (TYPE('a)))"
assumes eq_case: "p = q ⟹ P"
assumes disj_case: "ptr_span p ∩ ptr_span q = {} ⟹ P"
shows P
proof (cases "ptr_span p ∩ ptr_span q = {}")
case True
then show ?thesis by (simp add: disj_case)
next
case False
from valid_footprint_overlap_contained [OF valid_p valid_q ] False
have "ptr_val q ∈ ptr_span p ∨ ptr_val p ∈ ptr_span q"
by (simp add: typ_uinfo_t_def size_of_def)
hence "p = q"
by (metis ptr_val_conv size_of_tag valid_footprint_neq_nmem valid_p valid_q )
thus ?thesis by (simp add: eq_case)
qed
theorem subfield_deref_append:
fixes "q"::"'a::mem_type ptr"
fixes "p"::"'b::mem_type ptr"
assumes base: "ptr_val p = &(q→g)"
assumes g: "g ∈ set (field_names_u (typ_uinfo_t (TYPE('a))) (typ_uinfo_t (TYPE('b))))"
assumes f: "f ∈ set (all_field_names (typ_uinfo_t (TYPE('b))))"
shows "&(p→f) = &(q→(g@f))"
proof -
have wf_a: "wf_desc (typ_info_t (TYPE('a)))" by simp
have wf_b: "wf_desc (typ_info_t (TYPE('b)))" by simp
from g have "g ∈ set (field_names (typ_info_t (TYPE('a))) (typ_uinfo_t (TYPE('b))))"
by (simp add: typ_uinfo_t_def field_names_u_field_names_export_uinfo_conv(1))
from field_names_Some2(1) [rule_format, OF wf_a this] obtain n s where
fl_g: "field_lookup (typ_info_t TYPE('a)) g 0 = Some (s, n)" and
s: "export_uinfo s = typ_uinfo_t TYPE('b)"
by blast
from fl_g have off_g: "field_offset TYPE('a) g = n"
by (simp)
from all_field_names_exists_field_names_u(1) [OF f] obtain t
where "f ∈ set (field_names_u (typ_uinfo_t TYPE('b)) t)" by blast
hence "f ∈ set (field_names (typ_info_t TYPE('b)) t)"
by (simp add: field_names_u_field_names_export_uinfo_conv(1) typ_uinfo_t_def)
from field_names_Some2(1) [rule_format, OF wf_b this] obtain t' m where
fl_f: "field_lookup (typ_info_t TYPE('b)) f 0 = Some (t', m)" and
t': "export_uinfo t' = t"
by blast
from fl_f have off_f: "field_offset TYPE('b) f = m"
by simp
from field_lookup_prefix_Some''(1) [rule_format, OF fl_g wf_a, of f]
have fl_g_f: "field_lookup (typ_info_t TYPE('a)) (g @ f) 0 = field_lookup s f n" .
from field_lookup_export_uinfo_Some [OF fl_f] t'
have "field_lookup (typ_uinfo_t TYPE('b)) f 0 = Some (t, m)"
by (simp add: typ_uinfo_t_def)
from field_lookup_offset_shift' [OF this, of n]
have "field_lookup (typ_uinfo_t TYPE('b)) f n = Some (t, m + n)"
by simp
with s have "field_lookup (export_uinfo s) f n = Some (t, m + n)"
by simp
from field_lookup_export_uinfo_Some_rev [OF this] obtain t'' where
fl_s_f: "field_lookup s f n = Some (t'', m + n)" and
t'': "t = export_uinfo t''"
by blast
from fl_g_f fl_s_f have off_g_f: "field_offset TYPE('a) (g@f) = m + n"
by (simp)
show ?thesis
using base
by (simp add: field_lvalue_def off_g off_f off_g_f)
qed
lemmas root_ptr_valid_same_type_cases = valid_root_footprint_same_type_cases [OF root_ptr_valid_valid_root_footprint h_t_valid_valid_footprint]
lemmas ptr_valid_same_type_cases = valid_footprint_same_type_cases [OF h_t_valid_valid_footprint h_t_valid_valid_footprint]
theorem root_ptr_valid_heap_update_other':
assumes val_p: "root_ptr_valid d (p::'a::mem_type ptr)"
assumes val_q: "d ⊨⇩t (q::'b::mem_type ptr)"
assumes not_subtype: "¬ TYPE('b) ≤⇩τ TYPE('a)"
shows "h_val (heap_update p v h) q = h_val h q"
apply (clarsimp simp: h_val_def heap_update_def)
apply (subst heap_list_update_disjoint_same)
apply simp
apply (rule root_ptr_valid_not_subtype_disjoint [OF val_p val_q not_subtype])
apply simp
done
theorem root_ptr_valid_heap_update_field_other:
assumes val_p: "root_ptr_valid d (p::'a::mem_type ptr)"
assumes val_q: "d ⊨⇩t (q::'b::mem_type ptr)"
assumes fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (t, n)"
assumes match: "export_uinfo t = typ_uinfo_t TYPE('c::mem_type)"
assumes not_subtype_b_c: "¬ TYPE('b) ≤⇩τ TYPE('c)"
assumes not_subtype_c_b: "¬ TYPE('c) ≤⇩τ TYPE('b)"
shows "h_val (heap_update (PTR('c) &(p→f)) v h) q = h_val h q"
proof (cases "ptr_span (PTR('c) &(p→f)) ∩ ptr_span q = {}" )
case True
then show ?thesis by (simp add: h_val_update_regions_disjoint)
next
case False
from valid_footprint_overlap_cases [OF _ _ False] val_p val_q field_lookup_typ_uinfo_t_Some [OF fl]
not_subtype_b_c not_subtype_c_b match
have False
by (smt (verit) cvalid_field_pres h_t_valid_valid_footprint root_ptr_valid_legacy_def)
thus ?thesis
by simp
qed
theorem root_ptr_valid_heap_update_field_other':
assumes val_p: "root_ptr_valid d (p::'a::mem_type ptr)"
assumes val_q: "d ⊨⇩t (q::'b::mem_type ptr)"
assumes fl: "field_lookup (typ_info_t TYPE('b)) f 0 = Some (t, n)"
assumes match: "export_uinfo t = typ_uinfo_t TYPE('c::mem_type)"
assumes not_subtype_b_a: "¬ TYPE('b) ≤⇩τ TYPE('a)"
shows "h_val (heap_update p v h) (PTR ('c) &(q→f)) = h_val h (PTR ('c) &(q→f))"
proof (cases "ptr_span p ∩ ptr_span q = {}" )
case True
from fl val_q match have subset: "ptr_span (PTR('c) &(q→f)) ⊆ ptr_span q"
by (metis export_uinfo_size field_tag_sub ptr_val.ptr_val_def size_of_tag)
show ?thesis
apply (rule h_val_update_regions_disjoint)
using True subset
by auto
next
case False
from valid_root_footprint_valid_footprint_overlap_case [OF _ _ False] val_p val_q
have "TYPE('b) ≤⇩τ TYPE('a)"
by (meson False cvalid_field_pres'' fl match ptr_val.ptr_val_def root_ptr_valid_not_subtype_disjoint)
with not_subtype_b_a have False by simp
thus ?thesis
by simp
qed
lemmas root_ptr_valid_dist_type_cases = valid_root_footprint_dist_type_cases [OF root_ptr_valid_valid_root_footprint h_t_valid_valid_footprint,
consumes 3, case_names Field Disjoint_Spans]
theorem ptr_valid_heap_update_field_disj:
assumes val_p: "d ⊨⇩t (p::'a::mem_type ptr)"
assumes val_q: "d ⊨⇩t (q::'b::mem_type ptr)"
assumes subtype: "TYPE('b) ≤⇩τ TYPE('a)"
assumes disj [rule_format] :
"∀f. f ∈ set (field_names_u (typ_uinfo_t (TYPE('a))) (typ_uinfo_t (TYPE('b)))) ⟶ q ≠ Ptr (&(p→f))"
shows "h_val (heap_update p v h) q = h_val h q"
proof (cases "ptr_span p ∩ ptr_span q = {}")
case True
then show ?thesis
by (simp add: h_val_update_regions_disjoint)
next
case False
from subtype have "typ_uinfo_t TYPE('b) ≤ typ_uinfo_t TYPE('a)" by (simp add: sub_typ_def)
from this False valid_footprint_sub_cases [OF h_t_valid_valid_footprint [OF val_q] h_t_valid_valid_footprint [OF val_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 s where
fl': "field_lookup (typ_info_t (TYPE('a))) f 0 = Some (s, unat (ptr_val q - ptr_val p))" and
s: "export_uinfo s = typ_uinfo_t TYPE('b)"
using field_lookup_uinfo_Some_rev by blast
from fl have f: "f ∈ set (field_names_u (typ_uinfo_t TYPE('a)) (typ_uinfo_t TYPE('b)))"
by (metis field_names_Some3(1) field_names_u_field_names_export_uinfo_conv(1) fl' s typ_uinfo_t_def)
from fl'
have ptr_val_q: "ptr_val q = &(p→f)"
by (simp add: field_lvalue_def)
from disj [OF f] ptr_val_q
show ?thesis
by (auto simp add: ptr_val_field_convD)
qed
lemma is_padding_tag_access_ti_eq: "is_padding_tag s ⟹ access_ti s x bs = access_ti s y bs"
by (clarsimp simp add: is_padding_tag_def padding_tag_def from_bytes_def access_ti⇩0_def padding_desc_def)
lemma is_padding_tag_access_ti⇩0: "is_padding_tag s ⟹ access_ti⇩0 s x = replicate (size_td s) 0"
by (clarsimp simp add: is_padding_tag_def padding_tag_def from_bytes_def access_ti⇩0_def padding_desc_def)
lemma is_padding_tag_from_bytes_eq: "is_padding_tag s ⟹ from_bytes (access_ti⇩0 s x) = from_bytes (access_ti⇩0 s y)"
by (simp add: from_bytes_def is_padding_tag_access_ti⇩0)
theorem ptr_valid_heap_update_field_disj':
assumes val_p: "d ⊨⇩t (p::'a::xmem_type ptr)"
assumes val_q: "d ⊨⇩t (q::'b::xmem_type ptr)"
assumes subtype: "TYPE('b) ≤⇩τ TYPE('a)"
assumes disj [rule_format] :
"∀f. f ∈ set (field_names_no_padding (typ_info_t (TYPE('a))) (export_uinfo (typ_info_t (TYPE('b))))) ⟶ q ≠ Ptr (&(p→f))"
shows "h_val (heap_update p v h) q = h_val h q"
proof (cases "ptr_span p ∩ ptr_span q = {}")
case True
then show ?thesis
by (simp add: h_val_update_regions_disjoint)
next
case False
from subtype have "typ_uinfo_t TYPE('b) ≤ typ_uinfo_t TYPE('a)" by (simp add: sub_typ_def)
from this False valid_footprint_sub_cases [OF h_t_valid_valid_footprint [OF val_q] h_t_valid_valid_footprint [OF val_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 s where
fl': "field_lookup (typ_info_t (TYPE('a))) f 0 = Some (s, unat (ptr_val q - ptr_val p))" and
s: "export_uinfo s = typ_uinfo_t TYPE('b)"
using field_lookup_uinfo_Some_rev by blast
from fl' have fl'': "field_ti (TYPE('a)) f = Some s"
by (simp add: field_ti_def)
from fl' have f: "f ∈ set (field_names (typ_info_t TYPE('a)) (typ_uinfo_t TYPE('b)))"
by (metis field_names_Some3(1) fl' s)
from fl'
have ptr_val_q: "ptr_val q = &(p→f)"
by (simp add: field_lvalue_def)
then have q: "q = PTR ('b) &(p→f)"
by (cases q) auto
show ?thesis
proof (cases "qualified_padding_field_name f")
case True
from field_lookup_qualified_padding_field_name(1) [OF fl' True]
have padding_tag_s: "is_padding_tag s"
by (simp add: wf_padding)
note h_val = h_val_field_from_bytes' [where pa=p,OF fl'' s [simplified typ_uinfo_t_def]]
show ?thesis apply (simp add: q)
apply (simp add: h_val)
apply (simp add: is_padding_tag_from_bytes_eq [OF padding_tag_s])
done
next
case False
with f fl' s have "f ∈ set (field_names_no_padding (typ_info_t (TYPE('a))) (export_uinfo (typ_info_t (TYPE('b)))))"
by (simp add: set_field_names_no_padding_all_field_names_no_padding_conv all_field_names_no_padding_def
fold_typ_uinfo_t set_field_names_all_field_names_conv)
with disj [OF this] ptr_val_q show ?thesis by (auto simp add: ptr_val_field_convD)
qed
qed
lemma is_padding_tag_update_ti_id: "is_padding_tag s ⟹ update_ti s bs v = v"
by (auto simp add: is_padding_tag_def padding_tag_def padding_desc_def)
theorem ptr_valid_heap_update_field_disj'':
assumes val_p: "d ⊨⇩t (p::'a::xmem_type ptr)"
assumes val_q: "d ⊨⇩t (q::'b::xmem_type ptr)"
assumes subtype: "TYPE('b) ≤⇩τ TYPE('a)"
assumes fl_g: "field_lookup (typ_info_t TYPE('a)) g 0 = Some (t, n)"
assumes match: "export_uinfo t = typ_uinfo_t TYPE('c::xmem_type)"
assumes disj [rule_format] :
"∀f. f ∈ set (field_names_no_padding (typ_info_t (TYPE('a))) (export_uinfo (typ_info_t (TYPE('b)))))
⟶ ptr_span (PTR('b) &(p→f)) ∩ ptr_span (PTR('c) &(p→g)) = {}"
shows "h_val (heap_update q v h) (PTR('c) &(p→g)) = h_val h (PTR('c) &(p→g))"
proof (cases "ptr_span q ∩ ptr_span (PTR('c) &(p→g)) = {}")
case True
then show ?thesis by (simp add: h_val_update_regions_disjoint)
next
case False
from subtype have st: "typ_uinfo_t TYPE('b) ≤ typ_uinfo_t TYPE('a)" by (simp add: sub_typ_def)
from fl_g match have "ptr_span (PTR('c) &(p→g)) ⊆ ptr_span p"
by (metis export_uinfo_size field_tag_sub ptr_val.ptr_val_def size_of_tag)
with False have "ptr_span q ∩ ptr_span p ≠ {}"
by auto
from this st valid_footprint_sub_cases [OF h_t_valid_valid_footprint [OF val_q] h_t_valid_valid_footprint [OF val_p]]
have field_of: "field_of (ptr_val q - ptr_val p) (typ_uinfo_t TYPE('b)) (typ_uinfo_t TYPE('a))"
by (simp add: size_of_def)
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 s where
fl': "field_lookup (typ_info_t (TYPE('a))) f 0 = Some (s, unat (ptr_val q - ptr_val p))" and
s: "export_uinfo s = typ_uinfo_t TYPE('b)"
using field_lookup_uinfo_Some_rev by blast
from fl' have fl'': "field_ti (TYPE('a)) f = Some s"
by (simp add: field_ti_def)
from fl' have f: "f ∈ set (field_names (typ_info_t TYPE('a)) (typ_uinfo_t TYPE('b)))"
by (metis field_names_Some3(1) fl' s)
from val_p have cgrd_p: "c_guard p"
by (simp add: h_t_valid_c_guard)
from fl'
have ptr_val_q: "ptr_val q = &(p→f)"
by (simp add: field_lvalue_def)
then have q: "q = PTR ('b) &(p→f)"
by (cases q) auto
show ?thesis
proof (cases "qualified_padding_field_name f")
case True
from field_lookup_qualified_padding_field_name(1) [OF fl' True]
have padding_tag_s: "is_padding_tag s"
by (simp add: wf_padding)
note h_upd = heap_update_field_root_conv''' [OF fl'' cgrd_p s]
show ?thesis
apply (simp add: q)
by (simp add: h_upd is_padding_tag_update_ti_id [OF padding_tag_s] xmem_type_class.heap_update_id)
next
case False
with f fl' s have "f ∈ set (field_names_no_padding (typ_info_t (TYPE('a))) (export_uinfo (typ_info_t (TYPE('b)))))"
by (simp add: set_field_names_no_padding_all_field_names_no_padding_conv all_field_names_no_padding_def
fold_typ_uinfo_t set_field_names_all_field_names_conv)
from disj [OF this] have "ptr_span (PTR('b) &(p→f)) ∩ ptr_span (PTR('c) &(p→g)) = {}" .
then show ?thesis
by (simp add: q h_val_update_regions_disjoint)
qed
qed
theorem ptr_valid_heap_update_field_access_ti_disj:
assumes val_p: "d ⊨⇩t (p::'a::xmem_type ptr)"
assumes val_q: "d ⊨⇩t (q::'b::xmem_type ptr)"
assumes subtype: "TYPE('b) ≤⇩τ TYPE('a)"
assumes disj [rule_format] :
"∀f. f ∈ set (field_names_u (typ_uinfo_t (TYPE('a))) (typ_uinfo_t (TYPE('b)))) ⟶
(access_ti (fst (the (field_lookup (typ_info_t TYPE('a)) f 0)))
v
(heap_list h (size_of TYPE('b)) (ptr_val q))) =
(access_ti (fst (the (field_lookup (typ_info_t TYPE('a)) f 0)))
(h_val h p)
(heap_list h (size_of TYPE('b)) (ptr_val q)))"
shows "h_val (heap_update p v h) q = h_val h q"
proof (cases "ptr_span p ∩ ptr_span q = {}")
case True
then show ?thesis
by (simp add: h_val_update_regions_disjoint)
next
case False
from subtype have "typ_uinfo_t TYPE('b) ≤ typ_uinfo_t TYPE('a)" by (simp add: sub_typ_def)
from this False valid_footprint_sub_cases [OF h_t_valid_valid_footprint [OF val_q] h_t_valid_valid_footprint [OF val_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 s where
fl': "field_lookup (typ_info_t (TYPE('a))) f 0 = Some (s, unat (ptr_val q - ptr_val p))" and
s: "export_uinfo s = typ_uinfo_t TYPE('b)"
using field_lookup_uinfo_Some_rev by blast
from fl have f: "f ∈ set (field_names_u (typ_uinfo_t TYPE('a)) (typ_uinfo_t TYPE('b)))"
by (metis field_names_Some3(1) field_names_u_field_names_export_uinfo_conv(1) fl' s typ_uinfo_t_def)
from fl'
have ptr_val_q: "ptr_val q = &(p→f)"
by (simp add: field_lvalue_def)
from field_of
have contained: "ptr_span q ⊆ ptr_span p"
by (metis (no_types, opaque_lifting)
add_diff_cancel_left' export_uinfo_size field_lvalue_def field_of_lookup_info ptr_val_q size_of_def typ_uinfo_t_def)
from disj [OF f] fl' have from_bytes_eq:
"(access_ti s v (heap_list h (size_of TYPE('b)) (ptr_val q))) =
(access_ti s (h_val h p) (heap_list h (size_of TYPE('b)) (ptr_val q)))" by simp
from ptr_val_q have q: "ptr_val q = ptr_val p + word_of_nat (unat (ptr_val q - ptr_val p))"
by (simp add: field_lvalue_def field_offset_def field_offset_untyped_def fl)
from fl' s
have sz_bound: "size_of TYPE('b) + unat (ptr_val q - ptr_val p)
≤ length (to_bytes v (heap_list h (size_of TYPE('a)) (ptr_val p)))"
by (metis export_uinfo_size field_lookup_offset_size heap_list_length len size_of_def typ_uinfo_size)
have lheap_list: "length (heap_list h (size_of TYPE('a)) (ptr_val p)) = size_of (TYPE('a))"
by simp
from s
have sz_s: "size_td s = size_of TYPE('b)"
by (simp add: export_size_of )
from val_p
have p_no_overflow: "unat (ptr_val p) + size_of TYPE('a) ≤ addr_card"
by (meson c_guard_no_wrap' h_t_valid_def)
from contained q
have q_bound: "unat (ptr_val q - ptr_val p) + size_of TYPE('b) ≤ size_of TYPE('a)"
using sz_bound by auto
from heap_list_take_drop' [OF p_no_overflow q_bound]
have take_drop_eq:
"take (size_of TYPE('b))
(drop (unat (ptr_val q - ptr_val p))
(heap_list h (size_of TYPE('a)) (ptr_val p))) =
heap_list h (size_of TYPE('b)) (ptr_val q)"
by (simp add: q [symmetric])
note acc_eq = mem_type_field_lookup_access_ti_take_drop [OF fl' lheap_list, simplified sz_s, of v, simplified take_drop_eq]
note acc_eq' = mem_type_field_lookup_access_ti_take_drop [OF fl' lheap_list, simplified sz_s, of "h_val h p", simplified take_drop_eq]
have acc_eq'':
"(access_ti (typ_info_t TYPE('a)) (h_val h p)
(heap_list h (size_of TYPE('a)) (ptr_val p))) = (heap_list h (size_of TYPE('a)) (ptr_val p))"
apply (simp add: h_val_def)
apply (simp add: to_bytes_def [symmetric])
by (simp add: to_bytes_from_bytes_id)
show ?thesis
apply (simp add: heap_update_def h_val_def)
apply (subst (1 2) q)
apply (subst heap_list_update_list [OF sz_bound])
apply simp
apply (simp add: to_bytes_def)
apply (subst acc_eq [symmetric])
apply (subst from_bytes_eq)
apply (subst acc_eq')
apply (subst acc_eq'')
apply (simp add: take_drop_eq)
done
qed
lemma access_ti_field_names_no_padding_to_field_names_u:
assumes val_p: "d ⊨⇩t (p::'a::xmem_type ptr)"
assumes val_q: "d ⊨⇩t (q::'b::xmem_type ptr)"
assumes subtype: "TYPE('b) ≤⇩τ TYPE('a)"
assumes disj [rule_format]:
"∀f. f ∈ set (field_names_no_padding (typ_info_t (TYPE('a))) (export_uinfo (typ_info_t (TYPE('b))))) ⟶
(access_ti (fst (the (field_lookup (typ_info_t TYPE('a)) f 0)))
v
(heap_list h (size_of TYPE('b)) (ptr_val q))) =
(access_ti (fst (the (field_lookup (typ_info_t TYPE('a)) f 0)))
(h_val h p)
(heap_list h (size_of TYPE('b)) (ptr_val q)))"
assumes f_in: "f ∈ set (field_names_u (typ_uinfo_t (TYPE('a))) (typ_uinfo_t (TYPE('b))))"
shows "(access_ti (fst (the (field_lookup (typ_info_t TYPE('a)) f 0)))
v
(heap_list h (size_of TYPE('b)) (ptr_val q))) =
(access_ti (fst (the (field_lookup (typ_info_t TYPE('a)) f 0)))
(h_val h p)
(heap_list h (size_of TYPE('b)) (ptr_val q)))"
proof -
from f_in
obtain n s where
fl: "field_lookup (typ_info_t TYPE('a)) f 0 = Some (s, n)" and
match: "export_uinfo s = export_uinfo (typ_info_t (TYPE('b)))"
by (smt (verit) field_names_Some2(1) fold_typ_uinfo_t set_field_names_all_field_names_conv
set_field_names_u_all_field_names_conv wf_desc)
show ?thesis
proof (cases "qualified_padding_field_name f")
case True
from field_lookup_qualified_padding_field_name(1) [OF fl True]
have padding_tag_s: "is_padding_tag s"
by (simp add: wf_padding)
show ?thesis by (simp add: fl is_padding_tag_access_ti_eq [OF padding_tag_s])
next
case False
with fl match field_lookup_all_field_names(1) [OF fl]
have "f ∈ set (field_names_no_padding (typ_info_t (TYPE('a))) (export_uinfo (typ_info_t (TYPE('b)))))"
by (simp add: set_field_names_no_padding_all_field_names_no_padding_conv all_field_names_no_padding_def)
from disj [rule_format, OF this]
show ?thesis .
qed
qed
theorem ptr_valid_heap_update_field_access_ti_disj':
assumes val_p: "d ⊨⇩t (p::'a::xmem_type ptr)"
assumes val_q: "d ⊨⇩t (q::'b::xmem_type ptr)"
assumes subtype: "TYPE('b) ≤⇩τ TYPE('a)"
assumes disj :
"∀f. f ∈ set (field_names_no_padding (typ_info_t (TYPE('a))) (export_uinfo (typ_info_t (TYPE('b))))) ⟶
(access_ti (fst (the (field_lookup (typ_info_t TYPE('a)) f 0)))
v
(heap_list h (size_of TYPE('b)) (ptr_val q))) =
(access_ti (fst (the (field_lookup (typ_info_t TYPE('a)) f 0)))
(h_val h p)
(heap_list h (size_of TYPE('b)) (ptr_val q)))"
shows "h_val (heap_update p v h) q = h_val h q"
apply (rule ptr_valid_heap_update_field_access_ti_disj [OF val_p val_q subtype])
apply clarify
apply (rule access_ti_field_names_no_padding_to_field_names_u [OF val_p val_q subtype disj])
apply assumption
done
theorem ptr_valid_heap_update_subtype_field_access_ti_disj:
assumes val_p: "d ⊨⇩t (p::'a::xmem_type ptr)"
assumes val_q: "d ⊨⇩t (q::'b::xmem_type ptr)"
assumes subtype_b_a: "TYPE('b) ≤⇩τ TYPE('a)"
assumes fl_g: "field_lookup (typ_uinfo_t TYPE('b)) g 0 = Some (typ_uinfo_t TYPE('c::xmem_type), n)"
assumes disj [rule_format] :
"∀f. f ∈ set (field_names_u (typ_uinfo_t (TYPE('a))) (typ_uinfo_t (TYPE('b)))) ⟶
(access_ti (fst (the (field_lookup (typ_info_t TYPE('a)) f 0)))
v
(heap_list h (size_of TYPE('b)) (ptr_val q))) =
(access_ti (fst (the (field_lookup (typ_info_t TYPE('a)) f 0)))
(h_val h p)
(heap_list h (size_of TYPE('b)) (ptr_val q)))"
shows "h_val (heap_update p v h) (PTR('c) (&(q→g))) = h_val h (PTR('c) (&(q→g)))"
proof (cases "ptr_span p ∩ ptr_span q = {}")
case True
from fl_g have "ptr_span (PTR('c) (&(q→g))) ⊆ ptr_span q"
by (metis export_uinfo_size field_lookup_uinfo_Some_rev field_tag_sub ptr_val.ptr_val_def size_of_tag)
with True have "ptr_span p ∩ ptr_span (PTR('c) (&(q→g))) = {}" by blast
then show ?thesis
by (simp add: h_val_update_regions_disjoint)
next
case False
from subtype_b_a have "typ_uinfo_t TYPE('b) ≤ typ_uinfo_t TYPE('a)" by (simp add: sub_typ_def)
from this False valid_footprint_sub_cases [OF h_t_valid_valid_footprint [OF val_q] h_t_valid_valid_footprint [OF val_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 s where
fl': "field_lookup (typ_info_t (TYPE('a))) f 0 = Some (s, unat (ptr_val q - ptr_val p))" and
s: "export_uinfo s = typ_uinfo_t TYPE('b)"
using field_lookup_uinfo_Some_rev by blast
from fl have f: "f ∈ set (field_names_u (typ_uinfo_t TYPE('a)) (typ_uinfo_t TYPE('b)))"
by (metis field_names_Some3(1) field_names_u_field_names_export_uinfo_conv(1) fl' s typ_uinfo_t_def)
from fl'
have ptr_val_q: "ptr_val q = &(p→f)"
by (simp add: field_lvalue_def)
from field_of
have contained: "ptr_span q ⊆ ptr_span p"
by (metis (no_types, opaque_lifting)
add_diff_cancel_left' export_uinfo_size field_lvalue_def field_of_lookup_info ptr_val_q size_of_def typ_uinfo_t_def)
from fl_g have contained': "ptr_span (PTR('c) (&(q→g))) ⊆ ptr_span q"
by (metis export_uinfo_size field_lookup_uinfo_Some_rev field_tag_sub ptr_val.ptr_val_def size_of_tag)
from disj [OF f] fl' have from_bytes_eq:
"(access_ti s v (heap_list h (size_of TYPE('b)) (ptr_val q))) =
(access_ti s (h_val h p) (heap_list h (size_of TYPE('b)) (ptr_val q)))" by simp
from ptr_val_q have q: "ptr_val q = ptr_val p + word_of_nat (unat (ptr_val q - ptr_val p))"
by (simp add: field_lvalue_def field_offset_def field_offset_untyped_def fl)
from fl_g have q_g: "&(q→g) = ptr_val q + word_of_nat n"
by (simp add: field_lvalue_def field_offset_def field_offset_untyped_def)
with q have q_g': "&(q→g) = ptr_val p + word_of_nat (unat (ptr_val q - ptr_val p) + n)"
by simp
from fl' s
have sz_bound: "size_of TYPE('b) + unat (ptr_val q - ptr_val p)
≤ length (to_bytes v (heap_list h (size_of TYPE('a)) (ptr_val p)))"
by (metis export_uinfo_size field_lookup_offset_size heap_list_length len size_of_def