|
|
|
|
Impressum Shadow_DOM.thy
Sprache: Isabelle
|
|
(***********************************************************************************
* Copyright (c) 2016-2020 The University of Sheffield, UK
* 2019-2020 University of Exeter, UK
*
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are met:
*
* * Redistributions of source code must retain the above copyright notice, this
* list of conditions and the following disclaimer.
*
* * Redistributions in binary form must reproduce the above copyright notice,
* this list of conditions and the following disclaimer in the documentation
* and/or other materials provided with the distribution.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
* IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
* DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
* FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
* SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
* CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
* OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
* SPDX-License-Identifier: BSD-2-Clause
***********************************************************************************)
section‹The Shadow DOM›
theory Shadow_DOM
imports
"monads/ShadowRootMonad"
Core_DOM.Core_DOM
begin
abbreviation "safe_shadow_root_element_types ≡ {''article'', ''aside'', ''blockquote'', ''body'',
''div'', ''footer'', ''h1'', ''h2'', ''h3'', ''h4'', ''h5'', ''h6'', ''header'', ''main'',
''nav'', ''p'', ''section'', ''span''}"
subsection ‹Function Definitions›
subsubsection ‹get\_child\_nodes›
locale l_get_child_nodesShadow_DOM_defs =
CD: l_get_child_nodesCore_DOM_defs
begin
definition get_child_nodesshadow_root_ptr :: "(_) shadow_root_ptr ==> unit
==> (_, (_) node_ptr list) dom_prog" where
"get_child_nodesshadow_root_ptr shadow_root_ptr _ = get_M shadow_root_ptr RShadowRoot.child_nodes"
definition a_get_child_nodes_tups :: "(((_) object_ptr ==> bool) × ((_) object_ptr ==> unit
==> (_, (_) node_ptr list) dom_prog)) list" where
"a_get_child_nodes_tups ≡ [(is_shadow_root_ptrobject_ptr, get_child_nodesshadow_root_ptr ∘ the ∘ cast)]"
definition a_get_child_nodes :: "(_) object_ptr ==> (_, (_) node_ptr list) dom_prog" where
"a_get_child_nodes ptr = invoke (CD.a_get_child_nodes_tups @ a_get_child_nodes_tups) ptr ()"
definition a_get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set" where
"a_get_child_nodes_locs ptr ≡
(if is_shadow_root_ptr_kind ptr
then {preserved (get_M (the (cast ptr)) RShadowRoot.child_nodes)} else {}) ∪
CD.a_get_child_nodes_locs ptr"
definition first_child :: "(_) object_ptr ==> (_, (_) node_ptr option) dom_prog"
where
"first_child ptr = do {
children ← a_get_child_nodes ptr;
return (case children of [] ==> None | child#_ ==> Some child)}"
end
global_interpretation l_get_child_nodesShadow_DOM_defs defines
get_child_nodes = l_get_child_nodesShadow_DOM_defs.a_get_child_nodes and
get_child_nodes_locs = l_get_child_nodesShadow_DOM_defs.a_get_child_nodes_locs
.
locale l_get_child_nodesShadow_DOM =
l_type_wf type_wf +
l_known_ptr known_ptr +
l_get_child_nodesShadow_DOM_defs +
l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
CD: l_get_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM
get_child_nodes_locsCore_DOM
for type_wf :: "(_) heap ==> bool"
and known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool"
and get_child_nodes :: "(_) object_ptr ==> (_, (_) node_ptr list) dom_prog"
and get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_child_nodesCore_DOM :: "(_) object_ptr ==> (_, (_) node_ptr list) dom_prog"
and get_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set" +
assumes known_ptr_impl: "known_ptr = ShadowRootClass.known_ptr"
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes get_child_nodes_impl: "get_child_nodes = a_get_child_nodes"
assumes get_child_nodes_locs_impl: "get_child_nodes_locs = a_get_child_nodes_locs"
begin
lemmas get_child_nodes_def = get_child_nodes_impl[unfolded a_get_child_nodes_def get_child_nodes_def]
lemmas get_child_nodes_locs_def = get_child_nodes_locs_impl[unfolded a_get_child_nodes_locs_def
get_child_nodes_locs_def, folded CD.get_child_nodes_locs_impl]
lemma get_child_nodes_ok:
assumes "known_ptr ptr"
assumes "type_wf h"
assumes "ptr |∈| object_ptr_kinds h"
shows "h ⊨ ok (get_child_nodes ptr)"
using assms[unfolded known_ptr_impl type_wf_impl]
apply(auto simp add: get_child_nodes_def)[1]
apply(split CD.get_child_nodes_splits, rule conjI)+
using ShadowRootClass.type_wfDocument CD.get_child_nodes_ok CD.known_ptr_impl CD.type_wf_impl
apply blast
apply(auto simp add: CD.known_ptr_impl a_get_child_nodes_tups_def get_child_nodesshadow_root_ptr_def
get_MShadowRoot_ok
dest!: known_ptr_new_shadow_root_ptr intro!: bind_is_OK_I2)[1]
by (metis is_shadow_root_ptr_kind_none l_get_MShadowRoot_lemmas.get_MShadowRoot_ok
l_get_MShadowRoot_lemmas_axioms option.case_eq_if shadow_root_ptr_casts_commute3
shadow_root_ptr_kinds_commutes)
lemma get_child_nodes_ptr_in_heap:
assumes "h ⊨ get_child_nodes ptr →r children"
shows "ptr |∈| object_ptr_kinds h"
using assms
by(auto simp add: get_child_nodes_def invoke_ptr_in_heap dest: is_OK_returns_result_I)
lemma get_child_nodes_pure [simp]:
"pure (get_child_nodes ptr) h"
unfolding get_child_nodes_def a_get_child_nodes_tups_def
proof(split CD.get_child_nodes_splits, rule conjI; clarify)
assume "known_ptrCore_DOM ptr"
then show "pure (get_child_nodesCore_DOM ptr) h"
by simp
next
assume "¬ known_ptrCore_DOM ptr"
then show "pure (invoke [(is_shadow_root_ptrobject_ptr,
get_child_nodesshadow_root_ptr ∘ the ∘ castobject_ptr2shadow_root_ptr)]
ptr ()) h"
by(auto simp add: get_child_nodesshadow_root_ptr_def intro: bind_pure_I split: invoke_splits)
qed
lemma get_child_nodes_reads: "reads (get_child_nodes_locs ptr) (get_child_nodes ptr) h h'"
apply (simp add: get_child_nodes_def a_get_child_nodes_tups_def get_child_nodes_locs_def
CD.get_child_nodes_locs_def)
apply(split CD.get_child_nodes_splits, rule conjI)+
apply(auto intro!: reads_subset[OF CD.get_child_nodes_reads[unfolded CD.get_child_nodes_locs_def]]
split: if_splits)[1]
apply(split invoke_splits, rule conjI)+
apply(auto)[1]
apply(auto simp add: get_child_nodesshadow_root_ptr_def
intro: reads_subset[OF reads_singleton] reads_subset[OF check_in_heap_reads]
intro!: reads_bind_pure reads_subset[OF return_reads] split: option.splits)[1]
done
end
interpretation i_get_child_nodes?: l_get_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
DocumentClass.known_ptr get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by(simp add: l_get_child_nodesShadow_DOM_def l_get_child_nodesShadow_DOM_axioms_def instances)
declare l_get_child_nodesShadow_DOM_axioms [instances]
lemma get_child_nodes_is_l_get_child_nodes [instances]: "l_get_child_nodes type_wf known_ptr
get_child_nodes get_child_nodes_locs"
apply(auto simp add: l_get_child_nodes_def instances)[1]
using get_child_nodes_reads get_child_nodes_ok get_child_nodes_ptr_in_heap get_child_nodes_pure
by blast+
paragraph ‹new\_document›
locale l_new_document_get_child_nodesShadow_DOM =
CD: l_new_document_get_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM
get_child_nodes_locsCore_DOM
+ l_get_child_nodesShadow_DOM type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM get_child_nodes
get_child_nodes_locs get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
for type_wf :: "(_) heap ==> bool"
and known_ptr :: "(_) object_ptr ==> bool"
and get_child_nodes :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool"
and get_child_nodesCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_child_nodes_new_document:
"ptr' ≠ cast new_document_ptr ==> h ⊨ new_document →r new_document_ptr
==> h ⊨ new_document →h h' ==> r ∈ get_child_nodes_locs ptr' ==> r h h'"
apply(auto simp add: get_child_nodes_locs_def)[1]
using CD.get_child_nodes_new_document
apply (metis document_ptr_casts_commute3 empty_iff is_document_ptr_kind_none
new_document_get_MShadowRoot option.case_eq_if shadow_root_ptr_casts_commute3
singletonD)
by (simp add: CD.get_child_nodes_new_document)
lemma new_document_no_child_nodes:
"h ⊨ new_document →r new_document_ptr ==> h ⊨ new_document →h h'
==> h' ⊨ get_child_nodes (cast new_document_ptr) →r []"
apply(auto simp add: get_child_nodes_def)[1]
apply(split CD.get_child_nodes_splits, rule conjI)+
using CD.new_document_no_child_nodes apply auto[1]
by(auto simp add: DocumentClass.a_known_ptr_def CD.known_ptr_impl known_ptr_def
dest!: new_document_is_document_ptr)
end
interpretation i_new_document_get_child_nodes?:
l_new_document_get_child_nodesShadow_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
DocumentClass.type_wf DocumentClass.known_ptr Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by(unfold_locales)
declare l_new_document_get_child_nodesCore_DOM_axioms[instances]
lemma new_document_get_child_nodes_is_l_new_document_get_child_nodes [instances]:
"l_new_document_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
using new_document_is_l_new_document get_child_nodes_is_l_get_child_nodes
apply(simp add: l_new_document_get_child_nodes_def l_new_document_get_child_nodes_axioms_def)
using get_child_nodes_new_document new_document_no_child_nodes
by fast
paragraph ‹new\_shadow\_root›
locale l_new_shadow_root_get_child_nodesShadow_DOM =
l_get_child_nodesShadow_DOM type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM get_child_nodes
get_child_nodes_locs get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
for type_wf :: "(_) heap ==> bool"
and known_ptr :: "(_) object_ptr ==> bool"
and get_child_nodes :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool"
and get_child_nodesCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_child_nodes_new_shadow_root:
"ptr' ≠ cast new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →r new_shadow_root_ptr
==> h ⊨ newShadowRoot_M →h h' ==> r ∈ get_child_nodes_locs ptr' ==> r h h'"
apply(auto simp add: get_child_nodes_locs_def)[1]
apply (metis document_ptr_casts_commute3 insert_absorb insert_not_empty is_document_ptr_kind_none
new_shadow_root_get_MShadowRoot option.case_eq_if shadow_root_ptr_casts_commute3 singletonD)
apply(auto simp add: CD.get_child_nodes_locs_def)[1]
using new_shadow_root_get_MObject apply blast
apply (metis empty_iff insertE new_shadow_root_get_MElement)
apply (metis empty_iff new_shadow_root_get_MDocument singletonD)
done
lemma new_shadow_root_no_child_nodes:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →h h'
==> h' ⊨ get_child_nodes (cast new_shadow_root_ptr) →r []"
apply(auto simp add: get_child_nodes_def )[1]
apply(split CD.get_child_nodes_splits, rule conjI)+
apply(auto simp add: CD.get_child_nodes_def CD.a_get_child_nodes_tups_def)[1]
apply(split invoke_splits, rule conjI)+
using NodeClass.a_known_ptr_def known_ptr_not_character_data_ptr known_ptr_not_document_ptr
known_ptr_not_element_ptr local.CD.known_ptr_impl apply blast
apply(auto simp add: is_document_ptr_def split: option.splits document_ptr.splits)[1]
apply(auto simp add: is_character_data_ptr_def split: option.splits document_ptr.splits)[1]
apply(auto simp add: is_element_ptr_def split: option.splits document_ptr.splits)[1]
apply(auto simp add: a_get_child_nodes_tups_def)[1]
apply(split invoke_splits, rule conjI)+
apply(auto simp add: is_shadow_root_ptr_def split: shadow_root_ptr.splits
dest!: newShadowRoot_M_is_shadow_root_ptr)[1]
apply(auto intro!: bind_pure_returns_result_I)[1]
apply(drule(1) newShadowRoot_M_ptr_in_heap)
apply(auto simp add: shadow_root_ptr_kinds_def document_ptr_kinds_def)[1]
apply (metis check_in_heap_ptr_in_heap is_OK_returns_result_E old.unit.exhaust)
using new_shadow_root_children
by (simp add: new_shadow_root_children get_child_nodesshadow_root_ptr_def)
end
interpretation i_new_shadow_root_get_child_nodes?:
l_new_shadow_root_get_child_nodesShadow_DOM type_wf known_ptr get_child_nodes get_child_nodes_locs
DocumentClass.type_wf DocumentClass.known_ptr Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by(unfold_locales)
declare l_new_shadow_root_get_child_nodesShadow_DOM_def[instances]
locale l_new_shadow_root_get_child_nodes = l_get_child_nodes +
assumes get_child_nodes_new_shadow_root:
"ptr' ≠ cast new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →r new_shadow_root_ptr
==> h ⊨ newShadowRoot_M →h h' ==> r ∈ get_child_nodes_locs ptr' ==> r h h'"
assumes new_shadow_root_no_child_nodes:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →h h'
==> h' ⊨ get_child_nodes (cast new_shadow_root_ptr) →r []"
lemma new_shadow_root_get_child_nodes_is_l_new_shadow_root_get_child_nodes [instances]:
"l_new_shadow_root_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
apply(simp add: l_new_shadow_root_get_child_nodes_def l_new_shadow_root_get_child_nodes_axioms_def
instances)
using get_child_nodes_new_shadow_root new_shadow_root_no_child_nodes
by fast
paragraph ‹new\_element›
locale l_new_element_get_child_nodesShadow_DOM =
l_get_child_nodesShadow_DOM +
l_new_element_get_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM
get_child_nodes_locsCore_DOM
begin
lemma get_child_nodes_new_element:
"ptr' ≠ cast new_element_ptr ==> h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> r ∈ get_child_nodes_locs ptr' ==> r h h'"
by (auto simp add: get_child_nodes_locs_def CD.get_child_nodes_locs_def new_element_get_MObject
new_element_get_MElement new_element_get_MDocument new_element_get_MShadowRoot
split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E
intro: is_element_ptr_kind_obtains)
lemma new_element_no_child_nodes:
"h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> h' ⊨ get_child_nodes (cast new_element_ptr) →r []"
apply(auto simp add: get_child_nodes_def a_get_child_nodes_tups_def
split: prod.splits elim!: bind_returns_result_E bind_returns_heap_E)[1]
apply(split CD.get_child_nodes_splits, rule conjI)+
using local.new_element_no_child_nodes apply auto[1]
apply(auto simp add: invoke_def)[1]
apply(auto simp add: new_element_ptr_in_heap get_child_nodeselement_ptr_def check_in_heap_def
new_element_child_nodes intro!: bind_pure_returns_result_I
intro: new_element_is_element_ptr elim!: new_element_ptr_in_heap)[1]
proof -
assume " h ⊨ new_element →r new_element_ptr"
assume "h ⊨ new_element →h h'"
assume "¬ known_ptrCore_DOM (castelement_ptr2object_ptr new_element_ptr)"
moreover
have "known_ptr (cast new_element_ptr)"
using new_element_is_element_ptr ‹h ⊨ new_element →r new_element_ptr›
by(auto simp add: known_ptr_impl ShadowRootClass.a_known_ptr_def DocumentClass.a_known_ptr_def
CharacterDataClass.a_known_ptr_def ElementClass.a_known_ptr_def)
ultimately show "False"
by(simp add: known_ptr_impl CD.known_ptr_impl ShadowRootClass.a_known_ptr_def
is_document_ptr_kind_none)
qed
end
interpretation i_new_element_get_child_nodes?:
l_new_element_get_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
DocumentClass.known_ptr get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by(unfold_locales)
declare l_new_element_get_child_nodesShadow_DOM_axioms[instances]
lemma new_element_get_child_nodes_is_l_new_element_get_child_nodes [instances]:
"l_new_element_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs"
using new_element_is_l_new_element get_child_nodes_is_l_get_child_nodes
apply(auto simp add: l_new_element_get_child_nodes_def l_new_element_get_child_nodes_axioms_def)[1]
using get_child_nodes_new_element new_element_no_child_nodes
by fast+
subsubsection ‹delete\_shadow\_root›
locale l_delete_shadow_root_get_child_nodesShadow_DOM =
l_get_child_nodesShadow_DOM
begin
lemma get_child_nodes_delete_shadow_root:
"ptr' ≠ cast shadow_root_ptr ==> h ⊨ deleteShadowRoot_M shadow_root_ptr →h h' ==>
r ∈ get_child_nodes_locs ptr' ==> r h h'"
by(auto simp add: get_child_nodes_locs_def CD.get_child_nodes_locs_def
delete_shadow_root_get_MObject delete_shadow_root_get_MShadowRoot
delete_shadow_root_get_MDocument delete_shadow_root_get_MElement
split: if_splits option.splits
intro: is_shadow_root_ptr_kind_obtains)
end
locale l_delete_shadow_root_get_child_nodes = l_get_child_nodes_defs +
assumes get_child_nodes_delete_shadow_root:
"ptr' ≠ cast shadow_root_ptr ==> h ⊨ deleteShadowRoot_M shadow_root_ptr →h h' ==>
r ∈ get_child_nodes_locs ptr' ==> r h h'"
interpretation l_delete_shadow_root_get_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
DocumentClass.known_ptr get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by(auto simp add: l_delete_shadow_root_get_child_nodesShadow_DOM_def instances)
lemma l_delete_shadow_root_get_child_nodes_get_child_nodes_locs [instances]: "l_delete_shadow_root_get_child_nodes get_child_nodes_locs"
apply(auto simp add: l_delete_shadow_root_get_child_nodes_def)[1]
using get_child_nodes_delete_shadow_root apply fast
done
subsubsection ‹set\_child\_nodes›
locale l_set_child_nodesShadow_DOM_defs =
CD: l_set_child_nodesCore_DOM_defs
begin
definition set_child_nodesshadow_root_ptr :: "(_) shadow_root_ptr ==> (_) node_ptr list
==> (_, unit) dom_prog" where
"set_child_nodesshadow_root_ptr shadow_root_ptr = put_M shadow_root_ptr RShadowRoot.child_nodes_update"
definition a_set_child_nodes_tups :: "(((_) object_ptr ==> bool) × ((_) object_ptr ==> (_) node_ptr list
==> (_, unit) dom_prog)) list" where
"a_set_child_nodes_tups ≡ [(is_shadow_root_ptrobject_ptr, set_child_nodesshadow_root_ptr ∘ the ∘ cast)]"
definition a_set_child_nodes :: "(_) object_ptr ==> (_) node_ptr list ==> (_, unit) dom_prog" where
"a_set_child_nodes ptr children = invoke (CD.a_set_child_nodes_tups @ a_set_child_nodes_tups)
ptr children"
definition a_set_child_nodes_locs :: "(_) object_ptr ==> (_, unit) dom_prog set"
where
"a_set_child_nodes_locs ptr ≡
(if is_shadow_root_ptr_kind ptr
then all_args (put_M (the (cast ptr)) RShadowRoot.child_nodes_update)
else {}) ∪ CD.a_set_child_nodes_locs ptr"
end
global_interpretation l_set_child_nodesShadow_DOM_defs defines
set_child_nodes = l_set_child_nodesShadow_DOM_defs.a_set_child_nodes and
set_child_nodes_locs = l_set_child_nodesShadow_DOM_defs.a_set_child_nodes_locs
.
locale l_set_child_nodesShadow_DOM =
l_type_wf type_wf +
l_known_ptr known_ptr +
l_set_child_nodesShadow_DOM_defs +
l_set_child_nodes_defs set_child_nodes set_child_nodes_locs +
CD: l_set_child_nodesCore_DOM type_wfCore_DOM known_ptrCore_DOM set_child_nodesCore_DOM
set_child_nodes_locsCore_DOM
for type_wf :: "(_) heap ==> bool"
and known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool"
and set_child_nodes :: "(_) object_ptr ==> (_) node_ptr list ==> (_, unit) dom_prog"
and set_child_nodes_locs :: "(_) object_ptr ==> (_, unit) dom_prog set"
and set_child_nodesCore_DOM :: "(_) object_ptr ==> (_) node_ptr list ==> (_, unit) dom_prog"
and set_child_nodes_locsCore_DOM :: "(_) object_ptr ==> (_, unit) dom_prog set" +
assumes known_ptr_impl: "known_ptr = ShadowRootClass.known_ptr"
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes set_child_nodes_impl: "set_child_nodes = a_set_child_nodes"
assumes set_child_nodes_locs_impl: "set_child_nodes_locs = a_set_child_nodes_locs"
begin
lemmas set_child_nodes_def = set_child_nodes_impl[unfolded a_set_child_nodes_def set_child_nodes_def]
lemmas set_child_nodes_locs_def = set_child_nodes_locs_impl[unfolded a_set_child_nodes_locs_def
set_child_nodes_locs_def, folded CD.set_child_nodes_locs_impl]
lemma set_child_nodes_writes: "writes (set_child_nodes_locs ptr) (set_child_nodes ptr children) h h'"
apply (simp add: set_child_nodes_def a_set_child_nodes_tups_def set_child_nodes_locs_def)
apply(split CD.set_child_nodes_splits, rule conjI)+
apply (simp add: CD.set_child_nodes_writes writes_union_right_I)
apply(split invoke_splits, rule conjI)+
apply(auto simp add: a_set_child_nodes_def)[1]
apply(auto simp add: set_child_nodesshadow_root_ptr_def
intro!: writes_bind_pure
intro: writes_union_right_I writes_union_left_I
split: list.splits)[1]
by (simp add: is_shadow_root_ptr_kind_none)
lemma set_child_nodes_pointers_preserved:
assumes "w ∈ set_child_nodes_locs object_ptr"
assumes "h ⊨ w →h h'"
shows "object_ptr_kinds h = object_ptr_kinds h'"
using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: all_args_def set_child_nodes_locs_def CD.set_child_nodes_locs_def
split: if_splits)
lemma set_child_nodes_types_preserved:
assumes "w ∈ set_child_nodes_locs object_ptr"
assumes "h ⊨ w →h h'"
shows "type_wf h = type_wf h'"
using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: all_args_def type_wf_impl a_set_child_nodes_tups_def set_child_nodes_locs_def
CD.set_child_nodes_locs_def
split: if_splits option.splits)
end
interpretation
i_set_child_nodes?: l_set_child_nodesShadow_DOM type_wf known_ptr DocumentClass.type_wf
DocumentClass.known_ptr set_child_nodes set_child_nodes_locs Core_DOM_Functions.set_child_nodes
Core_DOM_Functions.set_child_nodes_locs
apply(unfold_locales)
by (auto simp add: set_child_nodes_def set_child_nodes_locs_def)
declare l_set_child_nodesShadow_DOM_axioms[instances]
lemma set_child_nodes_is_l_set_child_nodes [instances]: "l_set_child_nodes type_wf set_child_nodes
set_child_nodes_locs"
using instances Shadow_DOM.i_set_child_nodes.set_child_nodes_pointers_preserved Shadow_DOM.i_set_child_nodes.set_child_nodes_writes i_set_child_nodes.set_child_nodes_types_preserved
unfolding l_set_child_nodes_def
by blast
paragraph ‹get\_child\_nodes›
locale l_set_child_nodes_get_child_nodesShadow_DOM =
l_get_child_nodesShadow_DOM
type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM get_child_nodes get_child_nodes_locs
get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
+ l_set_child_nodesShadow_DOM
type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM set_child_nodes set_child_nodes_locs
set_child_nodesCore_DOM set_child_nodes_locsCore_DOM
+ CD: l_set_child_nodes_get_child_nodesCore_DOM
type_wfCore_DOM known_ptrCore_DOM get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
set_child_nodesCore_DOM set_child_nodes_locsCore_DOM
for type_wf :: "(_) heap ==> bool"
and known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool"
and get_child_nodes :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_child_nodesCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and set_child_nodes :: "(_) object_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_child_nodes_locs :: "(_) object_ptr ==> ((_) heap, exception, unit) prog set"
and set_child_nodesCore_DOM :: "(_) object_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, unit) prog set"
begin
lemma set_child_nodes_get_child_nodes:
assumes "known_ptr ptr"
assumes "type_wf h"
assumes "h ⊨ set_child_nodes ptr children →h h'"
shows "h' ⊨ get_child_nodes ptr →r children"
proof -
have "h ⊨ check_in_heap ptr →r ()"
using assms set_child_nodes_def invoke_ptr_in_heap
by (metis (full_types) check_in_heap_ptr_in_heap is_OK_returns_heap_I is_OK_returns_result_E
old.unit.exhaust)
then have ptr_in_h: "ptr |∈| object_ptr_kinds h"
by (simp add: check_in_heap_ptr_in_heap is_OK_returns_result_I)
have "type_wf h'"
apply(unfold type_wf_impl)
apply(rule subst[where P=id, OF type_wf_preserved[OF set_child_nodes_writes assms(3),
unfolded all_args_def], simplified])
by(auto simp add: all_args_def assms(2)[unfolded type_wf_impl] set_child_nodes_locs_def
CD.set_child_nodes_locs_def
split: if_splits)
have "h' ⊨ check_in_heap ptr →r ()"
using check_in_heap_reads set_child_nodes_writes assms(3) ‹h ⊨ check_in_heap ptr →r ()›
apply(rule reads_writes_separate_forwards)
apply(auto simp add: all_args_def set_child_nodes_locs_def CD.set_child_nodes_locs_def)[1]
done
then have "ptr |∈| object_ptr_kinds h'"
using check_in_heap_ptr_in_heap by blast
with assms ptr_in_h ‹type_wf h'› show ?thesis
apply(auto simp add: type_wf_impl known_ptr_impl get_child_nodes_def a_get_child_nodes_tups_def
set_child_nodes_def a_set_child_nodes_tups_def
del: bind_pure_returns_result_I2
intro!: bind_pure_returns_result_I2)[1]
apply(split CD.get_child_nodes_splits, (rule conjI impI)+)+
apply(split CD.set_child_nodes_splits)+
apply(auto simp add: CD.set_child_nodes_get_child_nodes type_wf_impl CD.type_wf_impl
dest: ShadowRootClass.type_wfDocument)[1]
apply(auto simp add: CD.set_child_nodes_get_child_nodes type_wf_impl CD.type_wf_impl
dest: ShadowRootClass.type_wfDocument)[1]
apply(split CD.set_child_nodes_splits)+
by(auto simp add: known_ptr_impl CD.known_ptr_impl set_child_nodesshadow_root_ptr_def
get_child_nodesshadow_root_ptr_def CD.type_wf_impl ShadowRootClass.type_wfDocument
dest: known_ptr_new_shadow_root_ptr)[2]
qed
lemma set_child_nodes_get_child_nodes_different_pointers:
assumes "ptr ≠ ptr'"
assumes "w ∈ set_child_nodes_locs ptr"
assumes "h ⊨ w →h h'"
assumes "r ∈ get_child_nodes_locs ptr'"
shows "r h h'"
using assms
apply(auto simp add: set_child_nodes_locs_def CD.set_child_nodes_locs_def
get_child_nodes_locs_def CD.get_child_nodes_locs_def)[1]
by(auto simp add: all_args_def
elim!: is_document_ptr_kind_obtains is_shadow_root_ptr_kind_obtains
is_element_ptr_kind_obtains
split: if_splits option.splits)
end
interpretation
i_set_child_nodes_get_child_nodes?: l_set_child_nodes_get_child_nodesShadow_DOM type_wf known_ptr
DocumentClass.type_wf DocumentClass.known_ptr get_child_nodes get_child_nodes_locs
Core_DOM_Functions.get_child_nodes Core_DOM_Functions.get_child_nodes_locs set_child_nodes
set_child_nodes_locs Core_DOM_Functions.set_child_nodes Core_DOM_Functions.set_child_nodes_locs
using instances
by(auto simp add: l_set_child_nodes_get_child_nodesShadow_DOM_def )
declare l_set_child_nodes_get_child_nodesShadow_DOM_axioms[instances]
lemma set_child_nodes_get_child_nodes_is_l_set_child_nodes_get_child_nodes [instances]:
"l_set_child_nodes_get_child_nodes type_wf known_ptr get_child_nodes get_child_nodes_locs
set_child_nodes set_child_nodes_locs"
apply(auto simp add: instances l_set_child_nodes_get_child_nodes_def
l_set_child_nodes_get_child_nodes_axioms_def)[1]
using set_child_nodes_get_child_nodes apply fast
using set_child_nodes_get_child_nodes_different_pointers apply fast
done
subsubsection ‹set\_tag\_type›
locale l_set_tag_nameShadow_DOM =
CD: l_set_tag_nameCore_DOM type_wfCore_DOM set_tag_name set_tag_name_locs +
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and set_tag_name :: "(_) element_ptr ==> tag_name ==> (_, unit) dom_prog"
and set_tag_name_locs :: "(_) element_ptr ==> (_, unit) dom_prog set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
begin
lemmas set_tag_name_def = CD.set_tag_name_impl[unfolded CD.a_set_tag_name_def set_tag_name_def]
lemmas set_tag_name_locs_def = CD.set_tag_name_locs_impl[unfolded CD.a_set_tag_name_locs_def
set_tag_name_locs_def]
lemma set_tag_name_ok:
"type_wf h ==> element_ptr |∈| element_ptr_kinds h ==> h ⊨ ok (set_tag_name element_ptr tag)"
apply(unfold type_wf_impl)
unfolding set_tag_name_impl[unfolded a_set_tag_name_def] using get_MElement_ok put_MElement_ok
using CD.set_tag_name_ok CD.type_wf_impl ShadowRootClass.type_wfDocument by blast
lemma set_tag_name_writes:
"writes (set_tag_name_locs element_ptr) (set_tag_name element_ptr tag) h h'"
using CD.set_tag_name_writes .
lemma set_tag_name_pointers_preserved:
assumes "w ∈ set_tag_name_locs element_ptr"
assumes "h ⊨ w →h h'"
shows "object_ptr_kinds h = object_ptr_kinds h'"
using assms
by(simp add: CD.set_tag_name_pointers_preserved)
lemma set_tag_name_typess_preserved:
assumes "w ∈ set_tag_name_locs element_ptr"
assumes "h ⊨ w →h h'"
shows "type_wf h = type_wf h'"
apply(unfold type_wf_impl)
apply(rule type_wf_preserved[OF writes_singleton2 assms(2)])
using assms(1) set_tag_name_locs_def
by(auto simp add: all_args_def set_tag_name_locs_def
split: if_splits)
end
interpretation i_set_tag_name?: l_set_tag_nameShadow_DOM type_wf DocumentClass.type_wf set_tag_name
set_tag_name_locs
by(auto simp add: l_set_tag_nameShadow_DOM_def l_set_tag_nameShadow_DOM_axioms_def instances)
declare l_set_tag_nameShadow_DOM_axioms [instances]
lemma set_tag_name_is_l_set_tag_name [instances]:
"l_set_tag_name type_wf set_tag_name set_tag_name_locs"
apply(auto simp add: l_set_tag_name_def)[1]
using set_tag_name_writes apply fast
using set_tag_name_ok apply fast
using set_tag_name_pointers_preserved apply (fast, fast)
using set_tag_name_typess_preserved apply (fast, fast)
done
paragraph ‹get\_child\_nodes›
locale l_set_tag_name_get_child_nodesShadow_DOM =
l_set_tag_nameShadow_DOM +
l_get_child_nodesShadow_DOM +
CD: l_set_tag_name_get_child_nodesCore_DOM type_wfCore_DOM set_tag_name set_tag_name_locs
known_ptrCore_DOM get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
begin
lemma set_tag_name_get_child_nodes:
"∀w ∈ set_tag_name_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
apply(auto simp add: get_child_nodes_locs_def)[1]
apply(auto simp add: set_tag_name_locs_def all_args_def)[1]
using CD.set_tag_name_get_child_nodes apply(blast)
using CD.set_tag_name_get_child_nodes apply(blast)
done
end
interpretation
i_set_tag_name_get_child_nodes?: l_set_tag_name_get_child_nodesShadow_DOM type_wf
DocumentClass.type_wf set_tag_name set_tag_name_locs known_ptr DocumentClass.known_ptr
get_child_nodes get_child_nodes_locs Core_DOM_Functions.get_child_nodes
Core_DOM_Functions.get_child_nodes_locs
by unfold_locales
declare l_set_tag_name_get_child_nodesShadow_DOM_axioms[instances]
lemma set_tag_name_get_child_nodes_is_l_set_tag_name_get_child_nodes [instances]:
"l_set_tag_name_get_child_nodes type_wf set_tag_name set_tag_name_locs known_ptr get_child_nodes
get_child_nodes_locs"
using set_tag_name_is_l_set_tag_name get_child_nodes_is_l_get_child_nodes
apply(simp add: l_set_tag_name_get_child_nodes_def
l_set_tag_name_get_child_nodes_axioms_def)
using set_tag_name_get_child_nodes
by fast
subsubsection ‹get\_shadow\_root›
locale l_get_shadow_rootShadow_DOM_defs
begin
definition a_get_shadow_root :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
where
"a_get_shadow_root element_ptr = get_M element_ptr shadow_root_opt"
definition a_get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
where
"a_get_shadow_root_locs element_ptr ≡ {preserved (get_M element_ptr shadow_root_opt)}"
end
global_interpretation l_get_shadow_rootShadow_DOM_defs
defines get_shadow_root = a_get_shadow_root
and get_shadow_root_locs = a_get_shadow_root_locs
.
locale l_get_shadow_root_defs =
fixes get_shadow_root :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
fixes get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
locale l_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM_defs +
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs +
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes get_shadow_root_impl: "get_shadow_root = a_get_shadow_root"
assumes get_shadow_root_locs_impl: "get_shadow_root_locs = a_get_shadow_root_locs"
begin
lemmas get_shadow_root_def = get_shadow_root_impl[unfolded get_shadow_root_def a_get_shadow_root_def]
lemmas get_shadow_root_locs_def = get_shadow_root_locs_impl[unfolded get_shadow_root_locs_def
a_get_shadow_root_locs_def]
lemma get_shadow_root_ok:
"type_wf h ==> element_ptr |∈| element_ptr_kinds h ==> h ⊨ ok (get_shadow_root element_ptr)"
unfolding get_shadow_root_def type_wf_impl
using ShadowRootMonad.get_MElement_ok by blast
lemma get_shadow_root_pure [simp]: "pure (get_shadow_root element_ptr) h"
unfolding get_shadow_root_def by simp
lemma get_shadow_root_ptr_in_heap:
assumes "h ⊨ get_shadow_root element_ptr →r children"
shows "element_ptr |∈| element_ptr_kinds h"
using assms
by(auto simp add: get_shadow_root_def get_MElement_ptr_in_heap dest: is_OK_returns_result_I)
lemma get_shadow_root_reads:
"reads (get_shadow_root_locs element_ptr) (get_shadow_root element_ptr) h h'"
by(simp add: get_shadow_root_def get_shadow_root_locs_def reads_bind_pure
reads_insert_writes_set_right)
end
interpretation i_get_shadow_root?: l_get_shadow_rootShadow_DOM type_wf get_shadow_root
get_shadow_root_locs
using instances
by (auto simp add: l_get_shadow_rootShadow_DOM_def)
declare l_get_shadow_rootShadow_DOM_axioms [instances]
locale l_get_shadow_root = l_type_wf + l_get_shadow_root_defs +
assumes get_shadow_root_reads:
"reads (get_shadow_root_locs element_ptr) (get_shadow_root element_ptr) h h'"
assumes get_shadow_root_ok:
"type_wf h ==> element_ptr |∈| element_ptr_kinds h ==> h ⊨ ok (get_shadow_root element_ptr)"
assumes get_shadow_root_ptr_in_heap:
"h ⊨ ok (get_shadow_root element_ptr) ==> element_ptr |∈| element_ptr_kinds h"
assumes get_shadow_root_pure [simp]:
"pure (get_shadow_root element_ptr) h"
lemma get_shadow_root_is_l_get_shadow_root [instances]:
"l_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
using instances
unfolding l_get_shadow_root_def
by (metis (no_types, lifting) ElementClass.l_type_wfElement_axioms get_shadow_root_ok get_shadow_root_pure get_shadow_root_reads l_get_MElement_lemmas.get_MElement_ptr_in_heap l_get_MElement_lemmas.intro l_get_shadow_rootShadow_DOM.get_shadow_root_def)
paragraph ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodes_get_shadow_rootShadow_DOM =
l_set_disconnected_nodesCore_DOM type_wfCore_DOM set_disconnected_nodes set_disconnected_nodes_locs +
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and set_disconnected_nodes
:: "(_) document_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap, exception, unit) prog set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma set_disconnected_nodes_get_shadow_root:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
by(auto simp add: set_disconnected_nodes_locs_def get_shadow_root_locs_def all_args_def)
end
locale l_set_disconnected_nodes_get_shadow_root =
l_set_disconnected_nodes_defs +
l_get_shadow_root_defs +
assumes set_disconnected_nodes_get_shadow_root:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
interpretation
i_set_disconnected_nodes_get_shadow_root?: l_set_disconnected_nodes_get_shadow_rootShadow_DOM
type_wf DocumentClass.type_wf set_disconnected_nodes set_disconnected_nodes_locs get_shadow_root
get_shadow_root_locs
by(auto simp add: l_set_disconnected_nodes_get_shadow_rootShadow_DOM_def instances)
declare l_set_disconnected_nodes_get_shadow_rootShadow_DOM_axioms[instances]
lemma set_disconnected_nodes_get_shadow_root_is_l_set_disconnected_nodes_get_shadow_root [instances]:
"l_set_disconnected_nodes_get_shadow_root set_disconnected_nodes_locs get_shadow_root_locs"
apply(auto simp add: l_set_disconnected_nodes_get_shadow_root_def)[1]
using set_disconnected_nodes_get_shadow_root apply fast
done
paragraph ‹set\_tag\_type›
locale l_set_tag_name_get_shadow_rootCore_DOM =
l_set_tag_nameShadow_DOM +
l_get_shadow_rootShadow_DOM
begin
lemma set_tag_name_get_shadow_root:
"∀w ∈ set_tag_name_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
by(auto simp add: set_tag_name_locs_def
get_shadow_root_locs_def all_args_def
intro: element_put_get_preserved[where setter=tag_name_update and getter=shadow_root_opt])
end
locale l_set_tag_name_get_shadow_root = l_set_tag_name + l_get_shadow_root +
assumes set_tag_name_get_shadow_root:
"∀w ∈ set_tag_name_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
interpretation
i_set_tag_name_get_shadow_root?: l_set_tag_name_get_shadow_rootCore_DOM type_wf DocumentClass.type_wf
set_tag_name set_tag_name_locs
get_shadow_root get_shadow_root_locs
apply(auto simp add: l_set_tag_name_get_shadow_rootCore_DOM_def instances)[1]
using l_set_tag_nameShadow_DOM_axioms
by unfold_locales
declare l_set_tag_name_get_shadow_rootCore_DOM_axioms[instances]
lemma set_tag_name_get_shadow_root_is_l_set_tag_name_get_shadow_root [instances]:
"l_set_tag_name_get_shadow_root type_wf set_tag_name set_tag_name_locs get_shadow_root
get_shadow_root_locs"
using set_tag_name_is_l_set_tag_name get_shadow_root_is_l_get_shadow_root
apply(simp add: l_set_tag_name_get_shadow_root_def l_set_tag_name_get_shadow_root_axioms_def)
using set_tag_name_get_shadow_root
by fast
paragraph ‹set\_child\_nodes›
locale l_set_child_nodes_get_shadow_rootShadow_DOM =
l_set_child_nodesShadow_DOM type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM set_child_nodes
set_child_nodes_locs set_child_nodesCore_DOM set_child_nodes_locsCore_DOM +
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool"
and set_child_nodes :: "(_) object_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_child_nodes_locs :: "(_) object_ptr ==> ((_) heap, exception, unit) prog set"
and set_child_nodesCore_DOM :: "(_) object_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, unit) prog set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma set_child_nodes_get_shadow_root: "∀w ∈ set_child_nodes_locs ptr. (h ⊨ w →h h' ⟶
(∀r ∈ get_shadow_root_locs ptr'. r h h'))"
apply(auto simp add: set_child_nodes_locs_def get_shadow_root_locs_def CD.set_child_nodes_locs_def
all_args_def)[1]
by(auto intro!: element_put_get_preserved[where getter=shadow_root_opt and
setter=RElement.child_nodes_update])
end
locale l_set_child_nodes_get_shadow_root = l_set_child_nodes_defs + l_get_shadow_root_defs +
assumes set_child_nodes_get_shadow_root:
"∀w ∈ set_child_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
interpretation
i_set_child_nodes_get_shadow_root?: l_set_child_nodes_get_shadow_rootShadow_DOM type_wf known_ptr
DocumentClass.type_wf DocumentClass.known_ptr set_child_nodes set_child_nodes_locs
Core_DOM_Functions.set_child_nodes Core_DOM_Functions.set_child_nodes_locs get_shadow_root
get_shadow_root_locs
by(auto simp add: l_set_child_nodes_get_shadow_rootShadow_DOM_def instances)
declare l_set_child_nodes_get_shadow_rootShadow_DOM_axioms[instances]
lemma set_child_nodes_get_shadow_root_is_l_set_child_nodes_get_shadow_root [instances]:
"l_set_child_nodes_get_shadow_root set_child_nodes_locs get_shadow_root_locs"
apply(auto simp add: l_set_child_nodes_get_shadow_root_def)[1]
using set_child_nodes_get_shadow_root apply fast
done
paragraph ‹delete\_shadow\_root›
locale l_delete_shadow_root_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM
begin
lemma get_shadow_root_delete_shadow_root: "h ⊨ deleteShadowRoot_M shadow_root_ptr →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
by(auto simp add: get_shadow_root_locs_def delete_shadow_root_get_MElement)
end
locale l_delete_shadow_root_get_shadow_root = l_get_shadow_root_defs +
assumes get_shadow_root_delete_shadow_root: "h ⊨ deleteShadowRoot_M shadow_root_ptr →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
interpretation l_delete_shadow_root_get_shadow_rootShadow_DOM type_wf get_shadow_root
get_shadow_root_locs
by(auto simp add: l_delete_shadow_root_get_shadow_rootShadow_DOM_def instances)
lemma l_delete_shadow_root_get_shadow_root_get_shadow_root_locs [instances]: "l_delete_shadow_root_get_shadow_root get_shadow_root_locs"
apply(auto simp add: l_delete_shadow_root_get_shadow_root_def)[1]
using get_shadow_root_delete_shadow_root apply fast
done
paragraph ‹new\_character\_data›
locale l_new_character_data_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_shadow_root_new_character_data:
"h ⊨ new_character_data →r new_character_data_ptr ==> h ⊨ new_character_data →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
by (auto simp add: get_shadow_root_locs_def new_character_data_get_MObject
new_character_data_get_MElement
split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E
intro: is_element_ptr_kind_obtains)
end
locale l_new_character_data_get_shadow_root = l_new_character_data + l_get_shadow_root +
assumes get_shadow_root_new_character_data:
"h ⊨ new_character_data →r new_character_data_ptr
==> h ⊨ new_character_data →h h' ==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
interpretation i_new_character_data_get_shadow_root?:
l_new_character_data_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
by(unfold_locales)
declare l_new_character_data_get_shadow_rootShadow_DOM_axioms [instances]
lemma new_character_data_get_shadow_root_is_l_new_character_data_get_shadow_root [instances]:
"l_new_character_data_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
using new_character_data_is_l_new_character_data get_shadow_root_is_l_get_shadow_root
apply(auto simp add: l_new_character_data_get_shadow_root_def
l_new_character_data_get_shadow_root_axioms_def instances)[1]
using get_shadow_root_new_character_data
by fast
paragraph ‹new\_document›
locale l_new_document_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_shadow_root_new_document:
"h ⊨ new_document →r new_document_ptr ==> h ⊨ new_document →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
by (auto simp add: get_shadow_root_locs_def new_document_get_MObject new_document_get_MElement
split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
end
locale l_new_document_get_shadow_root = l_new_document + l_get_shadow_root +
assumes get_shadow_root_new_document:
"h ⊨ new_document →r new_document_ptr
==> h ⊨ new_document →h h' ==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
interpretation i_new_document_get_shadow_root?:
l_new_document_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
by(unfold_locales)
declare l_new_document_get_shadow_rootShadow_DOM_axioms [instances]
lemma new_document_get_shadow_root_is_l_new_document_get_shadow_root [instances]:
"l_new_document_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
using new_document_is_l_new_document get_shadow_root_is_l_get_shadow_root
apply(auto simp add: l_new_document_get_shadow_root_def l_new_document_get_shadow_root_axioms_def
instances)[1]
using get_shadow_root_new_document
by fast
paragraph ‹new\_element›
locale l_new_element_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_shadow_root_new_element:
"ptr' ≠ new_element_ptr ==> h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
by (auto simp add: get_shadow_root_locs_def new_element_get_MObject new_element_get_MElement
new_element_get_MDocument split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
lemma new_element_no_shadow_root:
"h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> h' ⊨ get_shadow_root new_element_ptr →r None"
by(simp add: get_shadow_root_def new_element_shadow_root_opt)
end
locale l_new_element_get_shadow_root = l_new_element + l_get_shadow_root +
assumes get_shadow_root_new_element:
"ptr' ≠ new_element_ptr ==> h ⊨ new_element →r new_element_ptr
==> h ⊨ new_element →h h' ==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
assumes new_element_no_shadow_root:
"h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> h' ⊨ get_shadow_root new_element_ptr →r None"
interpretation i_new_element_get_shadow_root?:
l_new_element_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
by(unfold_locales)
declare l_new_element_get_shadow_rootShadow_DOM_axioms [instances]
lemma new_element_get_shadow_root_is_l_new_element_get_shadow_root [instances]:
"l_new_element_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
using new_element_is_l_new_element get_shadow_root_is_l_get_shadow_root
apply(auto simp add: l_new_element_get_shadow_root_def l_new_element_get_shadow_root_axioms_def
instances)[1]
using get_shadow_root_new_element new_element_no_shadow_root
by fast+
paragraph ‹new\_shadow\_root›
locale l_new_shadow_root_get_shadow_rootShadow_DOM =
l_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
for type_wf :: "(_) heap ==> bool"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_shadow_root_new_shadow_root:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →h h'
==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
by (auto simp add: get_shadow_root_locs_def new_shadow_root_get_MObject new_shadow_root_get_MElement
split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
end
locale l_new_shadow_root_get_shadow_root = l_get_shadow_root +
assumes get_shadow_root_new_shadow_root:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr
==> h ⊨ newShadowRoot_M →h h' ==> r ∈ get_shadow_root_locs ptr' ==> r h h'"
interpretation i_new_shadow_root_get_shadow_root?:
l_new_shadow_root_get_shadow_rootShadow_DOM type_wf get_shadow_root get_shadow_root_locs
by(unfold_locales)
declare l_new_shadow_root_get_shadow_rootShadow_DOM_axioms [instances]
lemma new_shadow_root_get_shadow_root_is_l_new_shadow_root_get_shadow_root [instances]:
"l_new_shadow_root_get_shadow_root type_wf get_shadow_root get_shadow_root_locs"
using get_shadow_root_is_l_get_shadow_root
apply(auto simp add: l_new_shadow_root_get_shadow_root_def
l_new_shadow_root_get_shadow_root_axioms_def instances)[1]
using get_shadow_root_new_shadow_root
by fast
subsubsection ‹set\_shadow\_root›
locale l_set_shadow_rootShadow_DOM_defs
begin
definition a_set_shadow_root :: "(_) element_ptr ==> (_) shadow_root_ptr option ==> (_, unit) dom_prog"
where
"a_set_shadow_root element_ptr = put_M element_ptr shadow_root_opt_update"
definition a_set_shadow_root_locs :: "(_) element_ptr ==> ((_, unit) dom_prog) set"
where
"a_set_shadow_root_locs element_ptr ≡ all_args (put_M element_ptr shadow_root_opt_update)"
end
global_interpretation l_set_shadow_rootShadow_DOM_defs
defines set_shadow_root = a_set_shadow_root
and set_shadow_root_locs = a_set_shadow_root_locs
.
locale l_set_shadow_root_defs =
fixes set_shadow_root :: "(_) element_ptr ==> (_) shadow_root_ptr option ==> (_, unit) dom_prog"
fixes set_shadow_root_locs :: "(_) element_ptr ==> (_, unit) dom_prog set"
locale l_set_shadow_rootShadow_DOM =
l_type_wf type_wf +
l_set_shadow_root_defs set_shadow_root set_shadow_root_locs +
l_set_shadow_rootShadow_DOM_defs
for type_wf :: "(_) heap ==> bool"
and set_shadow_root :: "(_) element_ptr ==> (_) shadow_root_ptr option ==> (_, unit) dom_prog"
and set_shadow_root_locs :: "(_) element_ptr ==> (_, unit) dom_prog set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes set_shadow_root_impl: "set_shadow_root = a_set_shadow_root"
assumes set_shadow_root_locs_impl: "set_shadow_root_locs = a_set_shadow_root_locs"
begin
lemmas set_shadow_root_def = set_shadow_root_impl[unfolded set_shadow_root_def
a_set_shadow_root_def]
lemmas set_shadow_root_locs_def = set_shadow_root_locs_impl[unfolded set_shadow_root_locs_def
a_set_shadow_root_locs_def]
lemma set_shadow_root_ok: "type_wf h ==> element_ptr |∈| element_ptr_kinds h ==>
h ⊨ ok (set_shadow_root element_ptr tag)"
apply(unfold type_wf_impl)
unfolding set_shadow_root_def using get_MElement_ok put_MElement_ok
by (simp add: ShadowRootMonad.put_MElement_ok)
lemma set_shadow_root_ptr_in_heap:
"h ⊨ ok (set_shadow_root element_ptr shadow_root) ==> element_ptr |∈| element_ptr_kinds h"
by(simp add: set_shadow_root_def ElementMonad.put_M_ptr_in_heap)
lemma set_shadow_root_writes:
"writes (set_shadow_root_locs element_ptr) (set_shadow_root element_ptr tag) h h'"
by(auto simp add: set_shadow_root_def set_shadow_root_locs_def intro: writes_bind_pure)
lemma set_shadow_root_pointers_preserved:
assumes "w ∈ set_shadow_root_locs element_ptr"
assumes "h ⊨ w →h h'"
shows "object_ptr_kinds h = object_ptr_kinds h'"
using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: all_args_def set_shadow_root_locs_def split: if_splits)
lemma set_shadow_root_types_preserved:
assumes "w ∈ set_shadow_root_locs element_ptr"
assumes "h ⊨ w →h h'"
shows "type_wf h = type_wf h'"
apply(unfold type_wf_impl)
using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: all_args_def set_shadow_root_locs_def split: if_splits)
end
interpretation i_set_shadow_root?: l_set_shadow_rootShadow_DOM type_wf set_shadow_root
set_shadow_root_locs
by (auto simp add: l_set_shadow_rootShadow_DOM_def instances)
declare l_set_shadow_rootShadow_DOM_axioms [instances]
locale l_set_shadow_root = l_type_wf +l_set_shadow_root_defs +
assumes set_shadow_root_writes:
"writes (set_shadow_root_locs element_ptr) (set_shadow_root element_ptr disc_nodes) h h'"
assumes set_shadow_root_ok:
"type_wf h ==> element_ptr |∈| element_ptr_kinds h ==>
h ⊨ ok (set_shadow_root element_ptr shadow_root)"
assumes set_shadow_root_ptr_in_heap:
"h ⊨ ok (set_shadow_root element_ptr shadow_root) ==> element_ptr |∈| element_ptr_kinds h"
assumes set_shadow_root_pointers_preserved:
"w ∈ set_shadow_root_locs element_ptr ==> h ⊨ w →h h' ==>
object_ptr_kinds h = object_ptr_kinds h'"
assumes set_shadow_root_types_preserved:
"w ∈ set_shadow_root_locs element_ptr ==> h ⊨ w →h h' ==> type_wf h = type_wf h'"
lemma set_shadow_root_is_l_set_shadow_root [instances]:
"l_set_shadow_root type_wf set_shadow_root set_shadow_root_locs"
apply(auto simp add: l_set_shadow_root_def instances)[1]
using set_shadow_root_writes apply blast
using set_shadow_root_ok apply (blast)
using set_shadow_root_ptr_in_heap apply blast
using set_shadow_root_pointers_preserved apply(blast, blast)
using set_shadow_root_types_preserved apply(blast, blast)
done
paragraph ‹get\_shadow\_root›
locale l_set_shadow_root_get_shadow_rootShadow_DOM =
l_set_shadow_rootShadow_DOM +
l_get_shadow_rootShadow_DOM
begin
lemma set_shadow_root_get_shadow_root:
"type_wf h ==> h ⊨ set_shadow_root ptr shadow_root_ptr_opt →h h' ==>
h' ⊨ get_shadow_root ptr →r shadow_root_ptr_opt"
by(auto simp add: set_shadow_root_def get_shadow_root_def)
lemma set_shadow_root_get_shadow_root_different_pointers: "ptr ≠ ptr' ==>
∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
by(auto simp add: set_shadow_root_locs_def get_shadow_root_locs_def all_args_def)
end
interpretation i_set_shadow_root_get_shadow_root?: l_set_shadow_root_get_shadow_rootShadow_DOM type_wf
set_shadow_root set_shadow_root_locs get_shadow_root get_shadow_root_locs
apply(auto simp add: l_set_shadow_root_get_shadow_rootShadow_DOM_def instances)[1]
by(unfold_locales)
declare l_set_shadow_root_get_shadow_rootShadow_DOM_axioms[instances]
locale l_set_shadow_root_get_shadow_root =
l_type_wf +
l_set_shadow_root_defs +
l_get_shadow_root_defs +
assumes set_shadow_root_get_shadow_root:
"type_wf h ==> h ⊨ set_shadow_root ptr shadow_root_ptr_opt →h h' ==>
h' ⊨ get_shadow_root ptr →r shadow_root_ptr_opt"
assumes set_shadow_root_get_shadow_root_different_pointers:
"ptr ≠ ptr' ==> w ∈ set_shadow_root_locs ptr ==> h ⊨ w →h h' ==>
r ∈ get_shadow_root_locs ptr' ==> r h h'"
lemma set_shadow_root_get_shadow_root_is_l_set_shadow_root_get_shadow_root [instances]:
"l_set_shadow_root_get_shadow_root type_wf set_shadow_root set_shadow_root_locs get_shadow_root
get_shadow_root_locs"
apply(auto simp add: l_set_shadow_root_get_shadow_root_def instances)[1]
using set_shadow_root_get_shadow_root apply fast
using set_shadow_root_get_shadow_root_different_pointers apply fast
done
subsubsection ‹set\_mode›
locale l_set_modeShadow_DOM_defs
begin
definition a_set_mode :: "(_) shadow_root_ptr ==> shadow_root_mode ==> (_, unit) dom_prog"
where
"a_set_mode shadow_root_ptr = put_M shadow_root_ptr mode_update"
definition a_set_mode_locs :: "(_) shadow_root_ptr ==> ((_, unit) dom_prog) set"
where
"a_set_mode_locs shadow_root_ptr ≡ all_args (put_M shadow_root_ptr mode_update)"
end
global_interpretation l_set_modeShadow_DOM_defs
defines set_mode = a_set_mode
and set_mode_locs = a_set_mode_locs
.
locale l_set_mode_defs =
fixes set_mode :: "(_) shadow_root_ptr ==> shadow_root_mode ==> (_, unit) dom_prog"
fixes set_mode_locs :: "(_) shadow_root_ptr ==> (_, unit) dom_prog set"
locale l_set_modeShadow_DOM =
l_type_wf type_wf +
l_set_mode_defs set_mode set_mode_locs +
l_set_modeShadow_DOM_defs
for type_wf :: "(_) heap ==> bool"
and set_mode :: "(_) shadow_root_ptr ==> shadow_root_mode ==> (_, unit) dom_prog"
and set_mode_locs :: "(_) shadow_root_ptr ==> (_, unit) dom_prog set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes set_mode_impl: "set_mode = a_set_mode"
assumes set_mode_locs_impl: "set_mode_locs = a_set_mode_locs"
begin
lemmas set_mode_def = set_mode_impl[unfolded set_mode_def a_set_mode_def]
lemmas set_mode_locs_def = set_mode_locs_impl[unfolded set_mode_locs_def a_set_mode_locs_def]
lemma set_mode_ok:
"type_wf h ==> shadow_root_ptr |∈| shadow_root_ptr_kinds h ==>
h ⊨ ok (set_mode shadow_root_ptr shadow_root_mode)"
apply(unfold type_wf_impl)
unfolding set_mode_def using get_MShadowRoot_ok put_MShadowRoot_ok
by (simp add: ShadowRootMonad.put_MShadowRoot_ok)
lemma set_mode_ptr_in_heap:
"h ⊨ ok (set_mode shadow_root_ptr shadow_root_mode) ==>
shadow_root_ptr |∈| shadow_root_ptr_kinds h"
by(simp add: set_mode_def put_M_ptr_in_heap)
lemma set_mode_writes:
"writes (set_mode_locs shadow_root_ptr) (set_mode shadow_root_ptr shadow_root_mode) h h'"
by(auto simp add: set_mode_def set_mode_locs_def intro: writes_bind_pure)
lemma set_mode_pointers_preserved:
assumes "w ∈ set_mode_locs element_ptr"
assumes "h ⊨ w →h h'"
shows "object_ptr_kinds h = object_ptr_kinds h'"
using assms(1) object_ptr_kinds_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: all_args_def set_mode_locs_def split: if_splits)
lemma set_mode_types_preserved:
assumes "w ∈ set_mode_locs element_ptr"
assumes "h ⊨ w →h h'"
shows "type_wf h = type_wf h'"
apply(unfold type_wf_impl)
using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
by(auto simp add: all_args_def set_mode_locs_def split: if_splits)
end
interpretation i_set_mode?: l_set_modeShadow_DOM type_wf set_mode set_mode_locs
by (auto simp add: l_set_modeShadow_DOM_def instances)
declare l_set_modeShadow_DOM_axioms [instances]
locale l_set_mode = l_type_wf +l_set_mode_defs +
assumes set_mode_writes:
"writes (set_mode_locs shadow_root_ptr) (set_mode shadow_root_ptr shadow_root_mode) h h'"
assumes set_mode_ok:
"type_wf h ==> shadow_root_ptr |∈| shadow_root_ptr_kinds h ==>
h ⊨ ok (set_mode shadow_root_ptr shadow_root_mode)"
assumes set_mode_ptr_in_heap:
"h ⊨ ok (set_mode shadow_root_ptr shadow_root_mode) ==>
shadow_root_ptr |∈| shadow_root_ptr_kinds h"
assumes set_mode_pointers_preserved:
"w ∈ set_mode_locs shadow_root_ptr ==>
h ⊨ w →h h' ==> object_ptr_kinds h = object_ptr_kinds h'"
assumes set_mode_types_preserved:
"w ∈ set_mode_locs shadow_root_ptr ==> h ⊨ w →h h' ==> type_wf h = type_wf h'"
lemma set_mode_is_l_set_mode [instances]: "l_set_mode type_wf set_mode set_mode_locs"
apply(auto simp add: l_set_mode_def instances)[1]
using set_mode_writes apply blast
using set_mode_ok apply (blast)
using set_mode_ptr_in_heap apply blast
using set_mode_pointers_preserved apply(blast, blast)
using set_mode_types_preserved apply(blast, blast)
done
paragraph ‹get\_child\_nodes›
locale l_set_shadow_root_get_child_nodesShadow_DOM =
l_get_child_nodesShadow_DOM +
l_set_shadow_rootShadow_DOM
begin
lemma set_shadow_root_get_child_nodes:
"∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
by(auto simp add: get_child_nodes_locs_def set_shadow_root_locs_def CD.get_child_nodes_locs_def
all_args_def
intro: element_put_get_preserved[where setter=shadow_root_opt_update])
end
interpretation i_set_shadow_root_get_child_nodes?: l_set_shadow_root_get_child_nodesShadow_DOM type_wf
known_ptr DocumentClass.type_wf DocumentClass.known_ptr get_child_nodes get_child_nodes_locs
Core_DOM_Functions.get_child_nodes Core_DOM_Functions.get_child_nodes_locs set_shadow_root
set_shadow_root_locs
by(unfold_locales)
declare l_set_shadow_root_get_child_nodesShadow_DOM_axioms[instances]
locale l_set_shadow_root_get_child_nodes = l_set_shadow_root + l_get_child_nodes +
assumes set_shadow_root_get_child_nodes:
"∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
lemma set_shadow_root_get_child_nodes_is_l_set_shadow_root_get_child_nodes [instances]:
"l_set_shadow_root_get_child_nodes type_wf set_shadow_root set_shadow_root_locs known_ptr
get_child_nodes get_child_nodes_locs"
apply(auto simp add: l_set_shadow_root_get_child_nodes_def
l_set_shadow_root_get_child_nodes_axioms_def instances)[1]
using set_shadow_root_get_child_nodes apply blast
done
paragraph ‹get\_shadow\_root›
locale l_set_mode_get_shadow_rootShadow_DOM =
l_set_modeShadow_DOM +
l_get_shadow_rootShadow_DOM
begin
lemma set_mode_get_shadow_root:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
by(auto simp add: set_mode_locs_def get_shadow_root_locs_def all_args_def)
end
interpretation
i_set_mode_get_shadow_root?: l_set_mode_get_shadow_rootShadow_DOM type_wf
set_mode set_mode_locs get_shadow_root
get_shadow_root_locs
by unfold_locales
declare l_set_mode_get_shadow_rootShadow_DOM_axioms[instances]
locale l_set_mode_get_shadow_root = l_set_mode + l_get_shadow_root +
assumes set_mode_get_shadow_root:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
lemma set_mode_get_shadow_root_is_l_set_mode_get_shadow_root [instances]:
"l_set_mode_get_shadow_root type_wf set_mode set_mode_locs get_shadow_root
get_shadow_root_locs"
using set_mode_is_l_set_mode get_shadow_root_is_l_get_shadow_root
apply(simp add: l_set_mode_get_shadow_root_def
l_set_mode_get_shadow_root_axioms_def)
using set_mode_get_shadow_root
by fast
paragraph ‹get\_child\_nodes›
locale l_set_mode_get_child_nodesShadow_DOM =
l_set_modeShadow_DOM +
l_get_child_nodesShadow_DOM
begin
lemma set_mode_get_child_nodes:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
by(auto simp add: get_child_nodes_locs_def CD.get_child_nodes_locs_def set_mode_locs_def
all_args_def)[1]
end
interpretation i_set_mode_get_child_nodes?: l_set_mode_get_child_nodesShadow_DOM type_wf set_mode
set_mode_locs known_ptr DocumentClass.type_wf DocumentClass.known_ptr get_child_nodes
get_child_nodes_locs Core_DOM_Functions.get_child_nodes Core_DOM_Functions.get_child_nodes_locs
by unfold_locales
declare l_set_mode_get_child_nodesShadow_DOM_axioms[instances]
locale l_set_mode_get_child_nodes = l_set_mode + l_get_child_nodes +
assumes set_mode_get_child_nodes:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
lemma set_mode_get_child_nodes_is_l_set_mode_get_child_nodes [instances]:
"l_set_mode_get_child_nodes type_wf set_mode set_mode_locs known_ptr get_child_nodes
get_child_nodes_locs"
using set_mode_is_l_set_mode get_child_nodes_is_l_get_child_nodes
apply(simp add: l_set_mode_get_child_nodes_def
l_set_mode_get_child_nodes_axioms_def)
using set_mode_get_child_nodes
by fast
subsubsection ‹get\_host›
locale l_get_hostShadow_DOM_defs =
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs
for get_shadow_root
:: "(_::linorder) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
definition a_get_host :: "(_) shadow_root_ptr ==> (_, (_) element_ptr) dom_prog" where
"a_get_host shadow_root_ptr = do {
host_ptrs ← element_ptr_kinds_M ⤜ filter_M (λelement_ptr. do {
shadow_root_opt ← get_shadow_root element_ptr;
return (shadow_root_opt = Some shadow_root_ptr)
});
(case host_ptrs of host_ptr#[] ==> return host_ptr | _ ==> error HierarchyRequestError)
}"
definition "a_get_host_locs ≡ (∪element_ptr. (get_shadow_root_locs element_ptr)) ∪
(∪ptr. {preserved (get_MObject ptr RObject.nothing)})"
end
global_interpretation l_get_hostShadow_DOM_defs get_shadow_root get_shadow_root_locs
defines get_host = "a_get_host"
and get_host_locs = "a_get_host_locs"
.
locale l_get_host_defs =
fixes get_host :: "(_) shadow_root_ptr ==> (_, (_) element_ptr) dom_prog"
fixes get_host_locs :: "((_) heap ==> (_) heap ==> bool) set"
locale l_get_hostShadow_DOM =
l_get_hostShadow_DOM_defs +
l_get_host_defs +
l_get_shadow_root +
assumes get_host_impl: "get_host = a_get_host"
assumes get_host_locs_impl: "get_host_locs = a_get_host_locs"
begin
lemmas get_host_def = get_host_impl[unfolded a_get_host_def]
lemmas get_host_locs_def = get_host_locs_impl[unfolded a_get_host_locs_def]
lemma get_host_pure [simp]: "pure (get_host element_ptr) h"
by(auto simp add: get_host_def intro!: bind_pure_I filter_M_pure_I split: list.splits)
lemma get_host_reads: "reads get_host_locs (get_host element_ptr) h h'"
using get_shadow_root_reads[unfolded reads_def]
by(auto simp add: get_host_def get_host_locs_def
intro!: reads_bind_pure reads_subset[OF check_in_heap_reads] reads_subset[OF error_reads]
reads_subset[OF get_shadow_root_reads] reads_subset[OF return_reads]
reads_subset[OF element_ptr_kinds_M_reads] filter_M_reads filter_M_pure_I
bind_pure_I
split: list.splits)
end
locale l_get_host = l_get_host_defs +
assumes get_host_pure [simp]: "pure (get_host element_ptr) h"
assumes get_host_reads: "reads get_host_locs (get_host node_ptr) h h'"
interpretation i_get_host?: l_get_hostShadow_DOM get_shadow_root get_shadow_root_locs get_host
get_host_locs type_wf
using instances
by (simp add: l_get_hostShadow_DOM_def l_get_hostShadow_DOM_axioms_def get_host_def get_host_locs_def)
declare l_get_hostShadow_DOM_axioms [instances]
lemma get_host_is_l_get_host [instances]: "l_get_host get_host get_host_locs"
apply(auto simp add: l_get_host_def)[1]
using get_host_reads apply fast
done
subsubsection ‹get\_mode›
locale l_get_modeShadow_DOM_defs
begin
definition a_get_mode :: "(_) shadow_root_ptr ==> (_, shadow_root_mode) dom_prog"
where
"a_get_mode shadow_root_ptr = get_M shadow_root_ptr mode"
definition a_get_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
where
"a_get_mode_locs shadow_root_ptr ≡ {preserved (get_M shadow_root_ptr mode)}"
end
global_interpretation l_get_modeShadow_DOM_defs
defines get_mode = a_get_mode
and get_mode_locs = a_get_mode_locs
.
locale l_get_mode_defs =
fixes get_mode :: "(_) shadow_root_ptr ==> (_, shadow_root_mode) dom_prog"
fixes get_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
locale l_get_modeShadow_DOM =
l_get_modeShadow_DOM_defs +
l_get_mode_defs get_mode get_mode_locs +
l_type_wf type_wf
for get_mode :: "(_) shadow_root_ptr ==> ((_) heap, exception, shadow_root_mode) prog"
and get_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and type_wf :: "(_) heap ==> bool" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes get_mode_impl: "get_mode = a_get_mode"
assumes get_mode_locs_impl: "get_mode_locs = a_get_mode_locs"
begin
lemmas get_mode_def = get_mode_impl[unfolded get_mode_def a_get_mode_def]
lemmas get_mode_locs_def = get_mode_locs_impl[unfolded get_mode_locs_def a_get_mode_locs_def]
lemma get_mode_ok: "type_wf h ==> shadow_root_ptr |∈| shadow_root_ptr_kinds h ==>
h ⊨ ok (get_mode shadow_root_ptr)"
unfolding get_mode_def type_wf_impl
using ShadowRootMonad.get_MShadowRoot_ok by blast
lemma get_mode_pure [simp]: "pure (get_mode element_ptr) h"
unfolding get_mode_def by simp
lemma get_mode_ptr_in_heap:
assumes "h ⊨ get_mode shadow_root_ptr →r children"
shows "shadow_root_ptr |∈| shadow_root_ptr_kinds h"
using assms
by(auto simp add: get_mode_def get_MShadowRoot_ptr_in_heap dest: is_OK_returns_result_I)
lemma get_mode_reads: "reads (get_mode_locs element_ptr) (get_mode element_ptr) h h'"
by(simp add: get_mode_def get_mode_locs_def reads_bind_pure reads_insert_writes_set_right)
end
interpretation i_get_mode?: l_get_modeShadow_DOM get_mode get_mode_locs type_wf
using instances
by (auto simp add: l_get_modeShadow_DOM_def)
declare l_get_modeShadow_DOM_axioms [instances]
locale l_get_mode = l_type_wf + l_get_mode_defs +
assumes get_mode_reads: "reads (get_mode_locs shadow_root_ptr) (get_mode shadow_root_ptr) h h'"
assumes get_mode_ok:
"type_wf h ==> shadow_root_ptr |∈| shadow_root_ptr_kinds h ==> h ⊨ ok (get_mode shadow_root_ptr)"
assumes get_mode_ptr_in_heap:
"h ⊨ ok (get_mode shadow_root_ptr) ==> shadow_root_ptr |∈| shadow_root_ptr_kinds h"
assumes get_mode_pure [simp]: "pure (get_mode shadow_root_ptr) h"
lemma get_mode_is_l_get_mode [instances]: "l_get_mode type_wf get_mode get_mode_locs"
apply(auto simp add: l_get_mode_def instances)[1]
using get_mode_reads apply blast
using get_mode_ok apply blast
using get_mode_ptr_in_heap apply blast
done
subsubsection ‹get\_shadow\_root\_safe›
locale l_get_shadow_root_safeShadow_DOM_defs =
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs +
l_get_mode_defs get_mode get_mode_locs
for get_shadow_root :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_mode :: "(_) shadow_root_ptr ==> (_, shadow_root_mode) dom_prog"
and get_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
definition a_get_shadow_root_safe :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
where
"a_get_shadow_root_safe element_ptr = do {
shadow_root_ptr_opt ← get_shadow_root element_ptr;
(case shadow_root_ptr_opt of
Some shadow_root_ptr ==> do {
mode ← get_mode shadow_root_ptr;
(if mode = Open then
return (Some shadow_root_ptr)
else
return None
)
} | None ==> return None)
}"
definition a_get_shadow_root_safe_locs
:: "(_) element_ptr ==> (_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set" where
"a_get_shadow_root_safe_locs element_ptr shadow_root_ptr ≡
(get_shadow_root_locs element_ptr) ∪ (get_mode_locs shadow_root_ptr)"
end
global_interpretation l_get_shadow_root_safeShadow_DOM_defs get_shadow_root get_shadow_root_locs
get_mode get_mode_locs
defines get_shadow_root_safe = a_get_shadow_root_safe
and get_shadow_root_safe_locs = a_get_shadow_root_safe_locs
.
locale l_get_shadow_root_safe_defs =
fixes get_shadow_root_safe :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
fixes get_shadow_root_safe_locs ::
"(_) element_ptr ==> (_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
locale l_get_shadow_root_safeShadow_DOM =
l_get_shadow_root_safeShadow_DOM_defs get_shadow_root get_shadow_root_locs get_mode get_mode_locs +
l_get_shadow_root_safe_defs get_shadow_root_safe get_shadow_root_safe_locs +
l_get_shadow_root type_wf get_shadow_root get_shadow_root_locs +
l_get_mode type_wf get_mode get_mode_locs +
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and get_shadow_root_safe ::
"(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_safe_locs ::
"(_) element_ptr ==> (_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_shadow_root :: "(_) element_ptr ==> (_, (_) shadow_root_ptr option) dom_prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_mode :: "(_) shadow_root_ptr ==> (_, shadow_root_mode) dom_prog"
and get_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
assumes get_shadow_root_safe_impl: "get_shadow_root_safe = a_get_shadow_root_safe"
assumes get_shadow_root_safe_locs_impl: "get_shadow_root_safe_locs = a_get_shadow_root_safe_locs"
begin
lemmas get_shadow_root_safe_def =
get_shadow_root_safe_impl[unfolded get_shadow_root_safe_def a_get_shadow_root_safe_def]
lemmas get_shadow_root_safe_locs_def =
get_shadow_root_safe_locs_impl[unfolded get_shadow_root_safe_locs_def a_get_shadow_root_safe_locs_def]
lemma get_shadow_root_safe_pure [simp]: "pure (get_shadow_root_safe element_ptr) h"
by (auto simp add: get_shadow_root_safe_def bind_pure_I option.case_eq_if)
end
interpretation i_get_shadow_root_safe?: l_get_shadow_root_safeShadow_DOM type_wf get_shadow_root_safe
get_shadow_root_safe_locs get_shadow_root get_shadow_root_locs get_mode get_mode_locs
using instances
by (auto simp add: l_get_shadow_root_safeShadow_DOM_def l_get_shadow_root_safeShadow_DOM_axioms_def
get_shadow_root_safe_def get_shadow_root_safe_locs_def)
declare l_get_shadow_root_safeShadow_DOM_axioms [instances]
locale l_get_shadow_root_safe = l_get_shadow_root_safe_defs +
assumes get_shadow_root_safe_pure [simp]: "pure (get_shadow_root_safe element_ptr) h"
lemma get_shadow_root_safe_is_l_get_shadow_root_safe [instances]:
"l_get_shadow_root_safe get_shadow_root_safe"
using instances
apply(auto simp add: l_get_shadow_root_safe_def)[1]
done
subsubsection ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodesShadow_DOM =
CD: l_set_disconnected_nodesCore_DOM type_wfCore_DOM set_disconnected_nodes set_disconnected_nodes_locs +
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and set_disconnected_nodes ::
"(_) document_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap, exception, unit) prog set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
begin
lemma set_disconnected_nodes_ok:
"type_wf h ==> document_ptr |∈| document_ptr_kinds h ==>
h ⊨ ok (set_disconnected_nodes document_ptr node_ptrs)"
using CD.set_disconnected_nodes_ok CD.type_wf_impl ShadowRootClass.type_wf_defs local.type_wf_impl
by blast
lemma set_disconnected_nodes_typess_preserved:
assumes "w ∈ set_disconnected_nodes_locs object_ptr"
assumes "h ⊨ w →h h'"
shows "type_wf h = type_wf h'"
using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
apply(unfold type_wf_impl)
by(auto simp add: all_args_def CD.set_disconnected_nodes_locs_def split: if_splits)
end
interpretation i_set_disconnected_nodes?: l_set_disconnected_nodesShadow_DOM type_wf
DocumentClass.type_wf set_disconnected_nodes set_disconnected_nodes_locs
by(auto simp add: l_set_disconnected_nodesShadow_DOM_def
l_set_disconnected_nodesShadow_DOM_axioms_def instances)
declare l_set_disconnected_nodesShadow_DOM_axioms [instances]
lemma set_disconnected_nodes_is_l_set_disconnected_nodes [instances]:
"l_set_disconnected_nodes type_wf set_disconnected_nodes set_disconnected_nodes_locs"
apply(auto simp add: l_set_disconnected_nodes_def)[1]
apply (simp add: i_set_disconnected_nodes.set_disconnected_nodes_writes)
using set_disconnected_nodes_ok apply blast
apply (simp add: i_set_disconnected_nodes.set_disconnected_nodes_ptr_in_heap)
using i_set_disconnected_nodes.set_disconnected_nodes_pointers_preserved apply (blast, blast)
using set_disconnected_nodes_typess_preserved apply(blast, blast)
done
paragraph ‹get\_child\_nodes›
locale l_set_disconnected_nodes_get_child_nodesShadow_DOM =
l_set_disconnected_nodesCore_DOM type_wfCore_DOM set_disconnected_nodes set_disconnected_nodes_locs +
l_get_child_nodesShadow_DOM type_wf known_ptr type_wfCore_DOM known_ptrCore_DOM get_child_nodes
get_child_nodes_locs get_child_nodesCore_DOM get_child_nodes_locsCore_DOM
for type_wf :: "(_) heap ==> bool"
and set_disconnected_nodes :: "(_) document_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit)
prog"
and set_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap, exception, unit) prog set"
and known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool"
and get_child_nodes :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_child_nodesCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locsCore_DOM :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma set_disconnected_nodes_get_child_nodes:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_child_nodes_locs ptr'. r h h'))"
by(auto simp add: set_disconnected_nodes_locs_def get_child_nodes_locs_def
CD.get_child_nodes_locs_def all_args_def)
end
interpretation i_set_disconnected_nodes_get_child_nodes?:
l_set_disconnected_nodes_get_child_nodesShadow_DOM type_wf set_disconnected_nodes
set_disconnected_nodes_locs known_ptr DocumentClass.type_wf DocumentClass.known_ptr get_child_nodes
get_child_nodes_locs Core_DOM_Functions.get_child_nodes Core_DOM_Functions.get_child_nodes_locs
by(auto simp add: l_set_disconnected_nodes_get_child_nodesShadow_DOM_def instances)
declare l_set_disconnected_nodes_get_child_nodesShadow_DOM_axioms[instances]
lemma set_disconnected_nodes_get_child_nodes_is_l_set_disconnected_nodes_get_child_nodes [instances]:
"l_set_disconnected_nodes_get_child_nodes set_disconnected_nodes_locs get_child_nodes_locs"
apply(auto simp add: l_set_disconnected_nodes_get_child_nodes_def)[1]
using set_disconnected_nodes_get_child_nodes apply fast
done
paragraph ‹get\_host›
locale l_set_disconnected_nodes_get_hostShadow_DOM =
l_set_disconnected_nodesShadow_DOM +
l_get_shadow_rootShadow_DOM +
l_get_hostShadow_DOM
begin
lemma set_disconnected_nodes_get_host:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_host_locs. r h h'))"
by(auto simp add: CD.set_disconnected_nodes_locs_def get_shadow_root_locs_def get_host_locs_def all_args_def)
end
interpretation i_set_disconnected_nodes_get_host?: l_set_disconnected_nodes_get_hostShadow_DOM type_wf
DocumentClass.type_wf set_disconnected_nodes set_disconnected_nodes_locs get_shadow_root
get_shadow_root_locs get_host get_host_locs
by(auto simp add: l_set_disconnected_nodes_get_hostShadow_DOM_def instances)
declare l_set_disconnected_nodes_get_hostShadow_DOM_axioms [instances]
locale l_set_disconnected_nodes_get_host = l_set_disconnected_nodes_defs + l_get_host_defs +
assumes set_disconnected_nodes_get_host:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_host_locs. r h h'))"
lemma set_disconnected_nodes_get_host_is_l_set_disconnected_nodes_get_host [instances]:
"l_set_disconnected_nodes_get_host set_disconnected_nodes_locs get_host_locs"
apply(auto simp add: l_set_disconnected_nodes_get_host_def instances)[1]
using set_disconnected_nodes_get_host
by fast
subsubsection ‹get\_tag\_name›
locale l_get_tag_nameShadow_DOM =
CD: l_get_tag_nameCore_DOM type_wfCore_DOM get_tag_name get_tag_name_locs +
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and get_tag_name :: "(_) element_ptr ==> (_, tag_name) dom_prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
begin
lemma get_tag_name_ok:
"type_wf h ==> element_ptr |∈| element_ptr_kinds h ==> h ⊨ ok (get_tag_name element_ptr)"
apply(unfold type_wf_impl get_tag_name_impl[unfolded a_get_tag_name_def])
using CD.get_tag_name_ok CD.type_wf_impl ShadowRootClass.type_wfDocument
by blast
end
interpretation i_get_tag_name?: l_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name
get_tag_name_locs
by(auto simp add: l_get_tag_nameShadow_DOM_def l_get_tag_nameShadow_DOM_axioms_def instances)
declare l_get_tag_nameShadow_DOM_axioms [instances]
lemma get_tag_name_is_l_get_tag_name [instances]: "l_get_tag_name type_wf get_tag_name
get_tag_name_locs"
apply(auto simp add: l_get_tag_name_def)[1]
using get_tag_name_reads apply fast
using get_tag_name_ok apply fast
done
paragraph ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodes_get_tag_nameShadow_DOM =
l_set_disconnected_nodesShadow_DOM +
l_get_tag_nameShadow_DOM
begin
lemma set_disconnected_nodes_get_tag_name:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
by(auto simp add: CD.set_disconnected_nodes_locs_def CD.get_tag_name_locs_def all_args_def)
end
interpretation i_set_disconnected_nodes_get_tag_name?: l_set_disconnected_nodes_get_tag_nameShadow_DOM
type_wf DocumentClass.type_wf set_disconnected_nodes set_disconnected_nodes_locs get_tag_name
get_tag_name_locs
by(auto simp add: l_set_disconnected_nodes_get_tag_nameShadow_DOM_def instances)
declare l_set_disconnected_nodes_get_tag_nameShadow_DOM_axioms [instances]
lemma set_disconnected_nodes_get_tag_name_is_l_set_disconnected_nodes_get_tag_name [instances]:
"l_set_disconnected_nodes_get_tag_name type_wf set_disconnected_nodes set_disconnected_nodes_locs
get_tag_name get_tag_name_locs"
apply(auto simp add: l_set_disconnected_nodes_get_tag_name_def
l_set_disconnected_nodes_get_tag_name_axioms_def instances)[1]
using set_disconnected_nodes_get_tag_name
by fast
paragraph ‹set\_child\_nodes›
locale l_set_child_nodes_get_tag_nameShadow_DOM =
l_set_child_nodesShadow_DOM +
l_get_tag_nameShadow_DOM
begin
lemma set_child_nodes_get_tag_name:
"∀w ∈ set_child_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
by(auto simp add: CD.set_child_nodes_locs_def set_child_nodes_locs_def CD.get_tag_name_locs_def
all_args_def
intro: element_put_get_preserved[where getter=tag_name and
setter=RElement.child_nodes_update])
end
interpretation i_set_child_nodes_get_tag_name?: l_set_child_nodes_get_tag_nameShadow_DOM type_wf
known_ptr DocumentClass.type_wf DocumentClass.known_ptr set_child_nodes set_child_nodes_locs
Core_DOM_Functions.set_child_nodes Core_DOM_Functions.set_child_nodes_locs get_tag_name
get_tag_name_locs
by(auto simp add: l_set_child_nodes_get_tag_nameShadow_DOM_def instances)
declare l_set_child_nodes_get_tag_nameShadow_DOM_axioms [instances]
lemma set_child_nodes_get_tag_name_is_l_set_child_nodes_get_tag_name [instances]:
"l_set_child_nodes_get_tag_name type_wf set_child_nodes set_child_nodes_locs get_tag_name
get_tag_name_locs"
apply(auto simp add: l_set_child_nodes_get_tag_name_def l_set_child_nodes_get_tag_name_axioms_def
instances)[1]
using set_child_nodes_get_tag_name
by fast
paragraph ‹delete\_shadow\_root›
locale l_delete_shadow_root_get_tag_nameShadow_DOM =
l_get_tag_nameShadow_DOM
begin
lemma get_tag_name_delete_shadow_root: "h ⊨ deleteShadowRoot_M shadow_root_ptr →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
by(auto simp add: CD.get_tag_name_locs_def delete_shadow_root_get_MElement)
end
locale l_delete_shadow_root_get_tag_name = l_get_tag_name_defs +
assumes get_tag_name_delete_shadow_root: "h ⊨ deleteShadowRoot_M shadow_root_ptr →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
interpretation l_delete_shadow_root_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name
get_tag_name_locs
by(auto simp add: l_delete_shadow_root_get_tag_nameShadow_DOM_def instances)
lemma l_delete_shadow_root_get_tag_name_get_tag_name_locs [instances]: "l_delete_shadow_root_get_tag_name get_tag_name_locs"
apply(auto simp add: l_delete_shadow_root_get_tag_name_def)[1]
using get_tag_name_delete_shadow_root apply fast
done
paragraph ‹set\_shadow\_root›
locale l_set_shadow_root_get_tag_nameShadow_DOM =
l_set_shadow_rootShadow_DOM +
l_get_tag_nameShadow_DOM
begin
lemma set_shadow_root_get_tag_name:
"∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
by(auto simp add: set_shadow_root_locs_def CD.get_tag_name_locs_def all_args_def
element_put_get_preserved[where setter=shadow_root_opt_update])
end
interpretation i_set_shadow_root_get_tag_name?: l_set_shadow_root_get_tag_nameShadow_DOM type_wf
set_shadow_root set_shadow_root_locs DocumentClass.type_wf get_tag_name get_tag_name_locs
apply(auto simp add: l_set_shadow_root_get_tag_nameShadow_DOM_def instances)[1]
by(unfold_locales)
declare l_set_shadow_root_get_tag_nameShadow_DOM_axioms[instances]
locale l_set_shadow_root_get_tag_name = l_set_shadow_root_defs + l_get_tag_name_defs +
assumes set_shadow_root_get_tag_name:
"∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
lemma set_shadow_root_get_tag_name_is_l_set_shadow_root_get_tag_name [instances]:
"l_set_shadow_root_get_tag_name set_shadow_root_locs get_tag_name_locs"
using set_shadow_root_is_l_set_shadow_root get_tag_name_is_l_get_tag_name
apply(simp add: l_set_shadow_root_get_tag_name_def )
using set_shadow_root_get_tag_name
by fast
paragraph ‹new\_element›
locale l_new_element_get_tag_nameShadow_DOM =
l_get_tag_nameShadow_DOM type_wf type_wfCore_DOM get_tag_name get_tag_name_locs
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and get_tag_name :: "(_) element_ptr ==> (_, tag_name) dom_prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_tag_name_new_element:
"ptr' ≠ new_element_ptr ==> h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
by (auto simp add: CD.get_tag_name_locs_def new_element_get_MObject new_element_get_MElement
new_element_get_MDocument split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
lemma new_element_empty_tag_name:
"h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> h' ⊨ get_tag_name new_element_ptr →r ''''"
by(simp add: CD.get_tag_name_def new_element_tag_name)
end
locale l_new_element_get_tag_name = l_new_element + l_get_tag_name +
assumes get_tag_name_new_element:
"ptr' ≠ new_element_ptr ==> h ⊨ new_element →r new_element_ptr
==> h ⊨ new_element →h h' ==> r ∈ get_tag_name_locs ptr' ==> r h h'"
assumes new_element_empty_tag_name:
"h ⊨ new_element →r new_element_ptr ==> h ⊨ new_element →h h'
==> h' ⊨ get_tag_name new_element_ptr →r ''''"
interpretation i_new_element_get_tag_name?:
l_new_element_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name get_tag_name_locs
by(auto simp add: l_new_element_get_tag_nameShadow_DOM_def instances)
declare l_new_element_get_tag_nameShadow_DOM_axioms [instances]
lemma new_element_get_tag_name_is_l_new_element_get_tag_name [instances]:
"l_new_element_get_tag_name type_wf get_tag_name get_tag_name_locs"
using new_element_is_l_new_element get_tag_name_is_l_get_tag_name
apply(auto simp add: l_new_element_get_tag_name_def l_new_element_get_tag_name_axioms_def
instances)[1]
using get_tag_name_new_element new_element_empty_tag_name
by fast+
paragraph ‹get\_shadow\_root›
locale l_set_mode_get_tag_nameShadow_DOM =
l_set_modeShadow_DOM +
l_get_tag_nameShadow_DOM
begin
lemma set_mode_get_tag_name:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
by(auto simp add: set_mode_locs_def CD.get_tag_name_locs_def all_args_def)
end
interpretation
i_set_mode_get_tag_name?: l_set_mode_get_tag_nameShadow_DOM type_wf
set_mode set_mode_locs DocumentClass.type_wf get_tag_name
get_tag_name_locs
by unfold_locales
declare l_set_mode_get_tag_nameShadow_DOM_axioms[instances]
locale l_set_mode_get_tag_name = l_set_mode + l_get_tag_name +
assumes set_mode_get_tag_name:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
lemma set_mode_get_tag_name_is_l_set_mode_get_tag_name [instances]:
"l_set_mode_get_tag_name type_wf set_mode set_mode_locs get_tag_name
get_tag_name_locs"
using set_mode_is_l_set_mode get_tag_name_is_l_get_tag_name
apply(simp add: l_set_mode_get_tag_name_def
l_set_mode_get_tag_name_axioms_def)
using set_mode_get_tag_name
by fast
paragraph ‹new\_document›
locale l_new_document_get_tag_nameShadow_DOM =
l_get_tag_nameShadow_DOM type_wf type_wfCore_DOM get_tag_name get_tag_name_locs
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and get_tag_name :: "(_) element_ptr ==> ((_) heap, exception, tag_name) prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_tag_name_new_document:
"h ⊨ new_document →r new_document_ptr ==> h ⊨ new_document →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
by(auto simp add: CD.get_tag_name_locs_def new_document_get_MElement)
end
locale l_new_document_get_tag_name = l_get_tag_name_defs +
assumes get_tag_name_new_document:
"h ⊨ new_document →r new_document_ptr ==> h ⊨ new_document →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
interpretation i_new_document_get_tag_name?:
l_new_document_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name
get_tag_name_locs
by unfold_locales
declare l_new_document_get_tag_nameShadow_DOM_def[instances]
lemma new_document_get_tag_name_is_l_new_document_get_tag_name [instances]:
"l_new_document_get_tag_name get_tag_name_locs"
unfolding l_new_document_get_tag_name_def
unfolding get_tag_name_locs_def
using new_document_get_MElement by blast
paragraph ‹new\_shadow\_root›
locale l_new_shadow_root_get_tag_nameShadow_DOM =
l_get_tag_nameShadow_DOM
begin
lemma get_tag_name_new_shadow_root:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
by (auto simp add: CD.get_tag_name_locs_def new_shadow_root_get_MObject new_shadow_root_get_MElement
split: prod.splits if_splits option.splits
elim!: bind_returns_result_E bind_returns_heap_E intro: is_element_ptr_kind_obtains)
end
locale l_new_shadow_root_get_tag_name = l_get_tag_name +
assumes get_tag_name_new_shadow_root:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr
==> h ⊨ newShadowRoot_M →h h' ==> r ∈ get_tag_name_locs ptr' ==> r h h'"
interpretation i_new_shadow_root_get_tag_name?:
l_new_shadow_root_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name get_tag_name_locs
by(unfold_locales)
declare l_new_shadow_root_get_tag_nameShadow_DOM_axioms [instances]
lemma new_shadow_root_get_tag_name_is_l_new_shadow_root_get_tag_name [instances]:
"l_new_shadow_root_get_tag_name type_wf get_tag_name get_tag_name_locs"
using get_tag_name_is_l_get_tag_name
apply(auto simp add: l_new_shadow_root_get_tag_name_def l_new_shadow_root_get_tag_name_axioms_def
instances)[1]
using get_tag_name_new_shadow_root
by fast
paragraph ‹new\_character\_data›
locale l_new_character_data_get_tag_nameShadow_DOM =
l_get_tag_nameShadow_DOM type_wf type_wfCore_DOM get_tag_name get_tag_name_locs
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and get_tag_name :: "(_) element_ptr ==> ((_) heap, exception, tag_name) prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_tag_name_new_character_data:
"h ⊨ new_character_data →r new_character_data_ptr ==> h ⊨ new_character_data →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
by(auto simp add: CD.get_tag_name_locs_def new_character_data_get_MElement)
end
locale l_new_character_data_get_tag_name = l_get_tag_name_defs +
assumes get_tag_name_new_character_data:
"h ⊨ new_character_data →r new_character_data_ptr ==> h ⊨ new_character_data →h h'
==> r ∈ get_tag_name_locs ptr' ==> r h h'"
interpretation i_new_character_data_get_tag_name?:
l_new_character_data_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name
get_tag_name_locs
by unfold_locales
declare l_new_character_data_get_tag_nameShadow_DOM_def[instances]
lemma new_character_data_get_tag_name_is_l_new_character_data_get_tag_name [instances]:
"l_new_character_data_get_tag_name get_tag_name_locs"
unfolding l_new_character_data_get_tag_name_def
unfolding get_tag_name_locs_def
using new_character_data_get_MElement by blast
paragraph ‹get\_tag\_type›
locale l_set_tag_name_get_tag_nameShadow_DOM = l_get_tag_nameShadow_DOM
+ l_set_tag_nameShadow_DOM
begin
lemma set_tag_name_get_tag_name:
assumes "h ⊨ CD.a_set_tag_name element_ptr tag →h h'"
shows "h' ⊨ CD.a_get_tag_name element_ptr →r tag"
using assms
by(auto simp add: CD.a_get_tag_name_def CD.a_set_tag_name_def)
lemma set_tag_name_get_tag_name_different_pointers:
assumes "ptr ≠ ptr'"
assumes "w ∈ CD.a_set_tag_name_locs ptr"
assumes "h ⊨ w →h h'"
assumes "r ∈ CD.a_get_tag_name_locs ptr'"
shows "r h h'"
using assms
by(auto simp add: all_args_def CD.a_set_tag_name_locs_def CD.a_get_tag_name_locs_def
split: if_splits option.splits )
end
interpretation i_set_tag_name_get_tag_name?:
l_set_tag_name_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf get_tag_name
get_tag_name_locs set_tag_name set_tag_name_locs
by unfold_locales
declare l_set_tag_name_get_tag_nameShadow_DOM_axioms[instances]
lemma set_tag_name_get_tag_name_is_l_set_tag_name_get_tag_name [instances]:
"l_set_tag_name_get_tag_name type_wf get_tag_name get_tag_name_locs
set_tag_name set_tag_name_locs"
using set_tag_name_is_l_set_tag_name get_tag_name_is_l_get_tag_name
apply(simp add: l_set_tag_name_get_tag_name_def
l_set_tag_name_get_tag_name_axioms_def)
using set_tag_name_get_tag_name
set_tag_name_get_tag_name_different_pointers
by fast+
subsubsection ‹attach\_shadow\_root›
locale l_attach_shadow_rootShadow_DOM_defs =
l_set_shadow_root_defs set_shadow_root set_shadow_root_locs +
l_set_mode_defs set_mode set_mode_locs +
l_get_tag_name_defs get_tag_name get_tag_name_locs +
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs
for set_shadow_root ::
"(_) element_ptr ==> (_) shadow_root_ptr option ==> ((_) heap, exception, unit) prog"
and set_shadow_root_locs :: "(_) element_ptr ==> ((_) heap, exception, unit) prog set"
and set_mode :: "(_) shadow_root_ptr ==> shadow_root_mode ==> ((_) heap, exception, unit) prog"
and set_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap, exception, unit) prog set"
and get_tag_name :: "(_) element_ptr ==> (_, char list) dom_prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
definition a_attach_shadow_root ::
"(_) element_ptr ==> shadow_root_mode ==> (_, (_) shadow_root_ptr) dom_prog"
where
"a_attach_shadow_root element_ptr shadow_root_mode = do {
tag ← get_tag_name element_ptr;
(if tag ∉ safe_shadow_root_element_types then error NotSupportedError else return ());
prev_shadow_root ← get_shadow_root element_ptr;
(if prev_shadow_root ≠ None then error NotSupportedError else return ());
new_shadow_root_ptr ← newShadowRoot_M;
set_mode new_shadow_root_ptr shadow_root_mode;
set_shadow_root element_ptr (Some new_shadow_root_ptr);
return new_shadow_root_ptr
}"
end
locale l_attach_shadow_root_defs =
fixes attach_shadow_root ::
"(_) element_ptr ==> shadow_root_mode ==> (_, (_) shadow_root_ptr) dom_prog"
global_interpretation l_attach_shadow_rootShadow_DOM_defs set_shadow_root set_shadow_root_locs
set_mode set_mode_locs get_tag_name get_tag_name_locs get_shadow_root get_shadow_root_locs
defines attach_shadow_root = a_attach_shadow_root
.
locale l_attach_shadow_rootShadow_DOM =
l_attach_shadow_rootShadow_DOM_defs set_shadow_root set_shadow_root_locs set_mode set_mode_locs
get_tag_name get_tag_name_locs get_shadow_root get_shadow_root_locs +
l_attach_shadow_root_defs attach_shadow_root +
l_set_shadow_rootShadow_DOM type_wf set_shadow_root set_shadow_root_locs +
l_set_mode type_wf set_mode set_mode_locs +
l_get_tag_name type_wf get_tag_name get_tag_name_locs +
l_get_shadow_root type_wf get_shadow_root get_shadow_root_locs +
l_known_ptr known_ptr
for known_ptr :: "(_) object_ptr ==> bool"
and set_shadow_root ::
"(_) element_ptr ==> (_) shadow_root_ptr option ==> ((_) heap, exception, unit) prog"
and set_shadow_root_locs :: "(_) element_ptr ==> ((_) heap, exception, unit) prog set"
and set_mode :: "(_) shadow_root_ptr ==> shadow_root_mode ==> ((_) heap, exception, unit) prog"
and set_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap, exception, unit) prog set"
and attach_shadow_root ::
"(_) element_ptr ==> shadow_root_mode ==> ((_) heap, exception, (_) shadow_root_ptr) prog"
and type_wf :: "(_) heap ==> bool"
and get_tag_name :: "(_) element_ptr ==> (_, char list) dom_prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set" +
assumes known_ptr_impl: "known_ptr = a_known_ptr"
assumes attach_shadow_root_impl: "attach_shadow_root = a_attach_shadow_root"
begin
lemmas attach_shadow_root_def = a_attach_shadow_root_def[folded attach_shadow_root_impl]
lemma attach_shadow_root_element_ptr_in_heap:
assumes "h ⊨ ok (attach_shadow_root element_ptr shadow_root_mode)"
shows "element_ptr |∈| element_ptr_kinds h"
proof -
obtain h' where "h ⊨ attach_shadow_root element_ptr shadow_root_mode →h h'"
using assms by auto
then
obtain h2 h3 new_shadow_root_ptr where
h2: "h ⊨ newShadowRoot_M →h h2" and
new_shadow_root_ptr: "h ⊨ newShadowRoot_M →r new_shadow_root_ptr" and
h3: "h2 ⊨ set_mode new_shadow_root_ptr shadow_root_mode →h h3" and
"h3 ⊨ set_shadow_root element_ptr (Some new_shadow_root_ptr) →h h'"
by(auto simp add: attach_shadow_root_def
elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_tag_name_pure, rotated]
bind_returns_heap_E2[rotated, OF get_shadow_root_pure, rotated] split: if_splits)
then have "element_ptr |∈| element_ptr_kinds h3"
using set_shadow_root_ptr_in_heap by blast
moreover
have "object_ptr_kinds h2 = object_ptr_kinds h |∪| {|cast new_shadow_root_ptr|}"
using h2 newShadowRoot_M_new_ptr new_shadow_root_ptr by auto
moreover
have "object_ptr_kinds h2 = object_ptr_kinds h3"
apply(rule writes_small_big[where P="λh h'. object_ptr_kinds h = object_ptr_kinds h'",
OF set_mode_writes h3])
using set_mode_pointers_preserved
apply blast
by (auto simp add: reflp_def transp_def)
ultimately
show ?thesis
by(auto simp add: element_ptr_kinds_def node_ptr_kinds_def)
qed
lemma create_shadow_root_known_ptr:
assumes "h ⊨ attach_shadow_root element_ptr shadow_root_mode →r new_shadow_root_ptr"
shows "known_ptr (castshadow_root_ptr2object_ptr new_shadow_root_ptr)"
using assms
by(auto simp add: attach_shadow_root_def known_ptr_impl ShadowRootClass.a_known_ptr_def
newShadowRoot_M_def newShadowRoot_def Let_def
elim!: bind_returns_result_E)
end
locale l_attach_shadow_root = l_attach_shadow_root_defs
interpretation
i_attach_shadow_root?: l_attach_shadow_rootShadow_DOM known_ptr set_shadow_root set_shadow_root_locs
set_mode set_mode_locs attach_shadow_root type_wf get_tag_name get_tag_name_locs get_shadow_root
get_shadow_root_locs
by(auto simp add: l_attach_shadow_rootShadow_DOM_def l_attach_shadow_rootShadow_DOM_axioms_def
attach_shadow_root_def instances)
declare l_attach_shadow_rootShadow_DOM_axioms [instances]
subsubsection ‹get\_parent›
global_interpretation l_get_parentCore_DOM_defs get_child_nodes get_child_nodes_locs
defines get_parent = "l_get_parentCore_DOM_defs.a_get_parent get_child_nodes"
and get_parent_locs = "l_get_parentCore_DOM_defs.a_get_parent_locs get_child_nodes_locs"
.
interpretation i_get_parent?: l_get_parentCore_DOM known_ptr type_wf get_child_nodes
get_child_nodes_locs known_ptrs get_parent get_parent_locs
by(simp add: l_get_parentCore_DOM_def l_get_parentCore_DOM_axioms_def get_parent_def
get_parent_locs_def instances)
declare l_get_parentCore_DOM_axioms [instances]
lemma get_parent_is_l_get_parent [instances]: "l_get_parent type_wf known_ptr known_ptrs get_parent
get_parent_locs get_child_nodes get_child_nodes_locs"
apply(simp add: l_get_parent_def l_get_parent_axioms_def instances)
using get_parent_reads get_parent_ok get_parent_ptr_in_heap get_parent_pure
get_parent_parent_in_heap get_parent_child_dual get_parent_reads_pointers
by blast
paragraph ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodes_get_parentShadow_DOM =
l_set_disconnected_nodes_get_child_nodes
+ l_set_disconnected_nodesShadow_DOM
+ l_get_parentCore_DOM
begin
lemma set_disconnected_nodes_get_parent [simp]:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_parent_locs. r h h'))"
by(auto simp add: get_parent_locs_def CD.set_disconnected_nodes_locs_def all_args_def)
end
interpretation i_set_disconnected_nodes_get_parent?: l_set_disconnected_nodes_get_parentShadow_DOM
set_disconnected_nodes set_disconnected_nodes_locs get_child_nodes get_child_nodes_locs type_wf
DocumentClass.type_wf known_ptr known_ptrs get_parent get_parent_locs
by (simp add: l_set_disconnected_nodes_get_parentShadow_DOM_def instances)
declare l_set_disconnected_nodes_get_parentCore_DOM_axioms[instances]
lemma set_disconnected_nodes_get_parent_is_l_set_disconnected_nodes_get_parent [instances]:
"l_set_disconnected_nodes_get_parent set_disconnected_nodes_locs get_parent_locs"
by(simp add: l_set_disconnected_nodes_get_parent_def)
subsubsection ‹get\_root\_node›
global_interpretation l_get_root_nodeCore_DOM_defs get_parent get_parent_locs
defines get_root_node = "l_get_root_nodeCore_DOM_defs.a_get_root_node get_parent"
and get_root_node_locs = "l_get_root_nodeCore_DOM_defs.a_get_root_node_locs get_parent_locs"
and get_ancestors = "l_get_root_nodeCore_DOM_defs.a_get_ancestors get_parent"
and get_ancestors_locs = "l_get_root_nodeCore_DOM_defs.a_get_ancestors_locs get_parent_locs"
.
declare a_get_ancestors.simps [code]
interpretation i_get_root_node?: l_get_root_nodeCore_DOM type_wf known_ptr known_ptrs get_parent
get_parent_locs get_child_nodes get_child_nodes_locs get_ancestors get_ancestors_locs
get_root_node get_root_node_locs
by(simp add: l_get_root_nodeCore_DOM_def l_get_root_nodeCore_DOM_axioms_def get_root_node_def
get_root_node_locs_def get_ancestors_def get_ancestors_locs_def instances)
declare l_get_root_nodeCore_DOM_axioms [instances]
lemma get_ancestors_is_l_get_ancestors [instances]: "l_get_ancestors get_ancestors"
apply(auto simp add: l_get_ancestors_def)[1]
using get_ancestors_ptr_in_heap apply fast
using get_ancestors_ptr apply fast
done
lemma get_root_node_is_l_get_root_node [instances]: "l_get_root_node get_root_node get_parent"
by (simp add: l_get_root_node_def Shadow_DOM.i_get_root_node.get_root_node_no_parent)
subsubsection ‹get\_root\_node\_si›
locale l_get_root_node_siShadow_DOM_defs =
l_get_parent_defs get_parent get_parent_locs +
l_get_host_defs get_host get_host_locs
for get_parent :: "(_) node_ptr ==> ((_) heap, exception, (_::linorder) object_ptr option) prog"
and get_parent_locs :: "((_) heap ==> (_) heap ==> bool) set"
and get_host :: "(_) shadow_root_ptr ==> ((_) heap, exception, (_) element_ptr) prog"
and get_host_locs :: "((_) heap ==> (_) heap ==> bool) set"
begin
partial_function (dom_prog) a_get_ancestors_si ::
"(_::linorder) object_ptr ==> (_, (_) object_ptr list) dom_prog"
where
"a_get_ancestors_si ptr = do {
check_in_heap ptr;
java.lang.NullPointerException: Cannot invoke "java.lang.CharSequence.toString()" because "replacement" is null
Some node_ptr ==> do {
parent_ptr_opt ← get_parent node_ptr;
(case parent_ptr_opt of
Some parent_ptr ==> a_get_ancestors_si parent_ptr
| None ==> return [])
}
| None ==> (case cast ptr of
Some shadow_root_ptr ==> do {
host ← get_host shadow_root_ptr;
a_get_ancestors_si (cast host)
} |
None ==> return []));
return (ptr # ancestors)
}"
definition "a_get_ancestors_si_locs = get_parent_locs ∪ get_host_locs"
definition a_get_root_node_si :: "(_) object_ptr ==> (_, (_) object_ptr) dom_prog"
where
"a_get_root_node_si ptr = do {
ancestors ← a_get_ancestors_si ptr;
return (last ancestors)
}"
definition "a_get_root_node_si_locs = a_get_ancestors_si_locs"
end
locale l_get_ancestors_si_defs =
fixes get_ancestors_si :: "(_::linorder) object_ptr ==> (_, (_) object_ptr list) dom_prog"
fixes get_ancestors_si_locs :: "((_) heap ==> (_) heap ==> bool) set"
locale l_get_root_node_si_defs =
fixes get_root_node_si :: "(_) object_ptr ==> (_, (_) object_ptr) dom_prog"
fixes get_root_node_si_locs :: "((_) heap ==> (_) heap ==> bool) set"
locale l_get_root_node_siShadow_DOM =
l_get_parent +
l_get_host +
l_get_root_node_siShadow_DOM_defs +
l_get_ancestors_si_defs +
l_get_root_node_si_defs +
assumes get_ancestors_si_impl: "get_ancestors_si = a_get_ancestors_si"
assumes get_ancestors_si_locs_impl: "get_ancestors_si_locs = a_get_ancestors_si_locs"
assumes get_root_node_si_impl: "get_root_node_si = a_get_root_node_si"
assumes get_root_node_si_locs_impl: "get_root_node_si_locs = a_get_root_node_si_locs"
begin
lemmas get_ancestors_si_def = a_get_ancestors_si.simps[folded get_ancestors_si_impl]
lemmas get_ancestors_si_locs_def = a_get_ancestors_si_locs_def[folded get_ancestors_si_locs_impl]
lemmas get_root_node_si_def =
a_get_root_node_si_def[folded get_root_node_si_impl get_ancestors_si_impl]
lemmas get_root_node_si_locs_def =
a_get_root_node_si_locs_def[folded get_root_node_si_locs_impl get_ancestors_si_locs_impl]
lemma get_ancestors_si_pure [simp]:
"pure (get_ancestors_si ptr) h"
proof -
have "∀ptr h h' x. h ⊨ get_ancestors_si ptr →r x ⟶ h ⊨ get_ancestors_si ptr →h h' ⟶ h = h'"
proof (induct rule: a_get_ancestors_si.fixp_induct[folded get_ancestors_si_impl])
case 1
then show ?case
by(rule admissible_dom_prog)
next
case 2
then show ?case
by simp
next
case (3 f)
then show ?case
using get_parent_pure get_host_pure
apply(auto simp add: pure_returns_heap_eq pure_def
split: option.splits
elim!: bind_returns_heap_E bind_returns_result_E
dest!: pure_returns_heap_eq[rotated, OF check_in_heap_pure])[1]
apply (meson option.simps(3) returns_result_eq)
apply(metis get_parent_pure pure_returns_heap_eq)
apply(metis get_host_pure pure_returns_heap_eq)
done
qed
then show ?thesis
by (meson pure_eq_iff)
qed
lemma get_root_node_si_pure [simp]: "pure (get_root_node_si ptr) h"
by(auto simp add: get_root_node_si_def bind_pure_I)
lemma get_ancestors_si_ptr_in_heap:
assumes "h ⊨ ok (get_ancestors_si ptr)"
shows "ptr |∈| object_ptr_kinds h"
using assms
by(auto simp add: get_ancestors_si_def check_in_heap_ptr_in_heap elim!: bind_is_OK_E
dest: is_OK_returns_result_I)
lemma get_ancestors_si_ptr:
assumes "h ⊨ get_ancestors_si ptr →r ancestors"
shows "ptr ∈ set ancestors"
using assms
by(simp add: get_ancestors_si_def)
(auto elim!: bind_returns_result_E2
split: option.splits
intro!: bind_pure_I)
lemma get_ancestors_si_never_empty:
assumes "h ⊨ get_ancestors_si child →r ancestors"
shows "ancestors ≠ []"
using assms
apply(simp add: get_ancestors_si_def)
by(auto elim!: bind_returns_result_E2 split: option.splits)
lemma get_root_node_si_no_parent:
"h ⊨ get_parent node_ptr →r None ==> h ⊨ get_root_node_si (cast node_ptr) →r cast node_ptr"
apply(auto simp add: check_in_heap_def get_root_node_si_def get_ancestors_si_def
intro!: bind_pure_returns_result_I )[1]
using get_parent_ptr_in_heap by blast
lemma get_root_node_si_root_not_shadow_root:
assumes "h ⊨ get_root_node_si ptr →r root"
shows "¬ is_shadow_root_ptrobject_ptr root"
using assms
proof(auto simp add: get_root_node_si_def elim!: bind_returns_result_E2)
fix y
assume "h ⊨
java.lang.NullPointerException: Cannot invoke "java.lang.CharSequence.toString()" because "replacement" is null
and "root y"
then
show False
proof(induct y arbitrary: ptr)
case Nil
then show ?case
using assms(1) get_ancestors_si_never_empty by blast
next
case (Cons a x)
then show ?case
apply(auto simp add: get_ancestors_si_def[of ptr]
elim!: bind_returns_result_E2
split: option.splits if_splits)[1]
singigget_ancestorss_never_empty apply blast
using Cons.prems(2) apply auto[1]
using 🚫
qed
qed
end
global_interpretation l_get_root_node_siShadow_DOM_defs get_parent get_parent_locs get_host get_host_locs
defines get_root_node_si = a_get_root_node_si
and get_root_node_si_locs = a_get_root_node_si_locs
and get_ancestors_si = a_get_ancestors_si
and get_ancestors_si_locs = a_get_ancestors_si_locs
.
declare a_get_ancestors_si.simps [code]
interpretation i_get_root_node_si?: l_get_root_node_siShadow_DOM type_wf known_ptr known_ptrs
get_parent get_parent_locs get_child_nodes get_child_nodes_locs get_host get_host_locs
get_ancestors_si get_ancestors_si_locs get_root_node_si get_root_node_si_locs
apply(auto simp add: l_get_root_node_siShadow_DOM_def l_get_root_node_siShadow_DOM_axioms_def
instances)[1]
by(auto simp add: get_root_node_si_def get_root_node_si_locs_def get_ancestors_si_def
get_ancestors_si_locs_def)
declare l_get_root_node_siShadow_DOM_axioms[instances]
lemma get_ancestors_si_is_l_get_ancestors [instances]: "l_get_ancestors get_ancestors_si"
unfolding l_get_ancestors_def
using get_ancestors_si_pure get_ancestors_si_ptr get_ancestors_si_ptr_in_heap
by blast
lemma get_root_node_si_is_l_get_root_node [instances]: "l_get_root_node get_root_node_si get_parent"
apply(simp add: l_get_root_node_def)
using get_root_node_si_no_parent
by fast
paragraph ‹set\_disconnected\_nodes›
locale l_set_disconnected_nodes_get_ancestors_siCore_DOM =
l_set_disconnected_nodes_get_parent
+ l_get_root_node_siShadow_DOM
+ l_set_disconnected_nodesShadow_DOM
+ l_set_disconnected_nodes_get_host
begin
lemma set_disconnected_nodes_get_ancestors_si:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_ancestors_si_locs. r h h'))"
by(auto simp add: get_parent_locs_def set_disconnected_nodes_locs_def
set_disconnected_nodes_get_host get_ancestors_si_locs_def all_args_def)
end
locale l_set_disconnected_nodes_get_ancestors_si =
l_set_disconnected_nodes_defs +
l_get_ancestors_si_defs +
assumes set_disconnected_nodes_get_ancestors_si:
"∀w ∈ set_disconnected_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_ancestors_si_locs. r h h'))"
interpretation i_set_disconnected_nodes_get_ancestors_si?:
l_set_disconnected_nodes_get_ancestors_siCore_DOM set_disconnected_nodes set_disconnected_nodes_locs
get_parent get_parent_locs type_wf known_ptr known_ptrs get_child_nodes get_child_nodes_locs
get_host get_host_locs get_ancestors_si get_ancestors_si_locs get_root_node_si
get_root_node_si_locs DocumentClass.type_wf
by (auto simp add: l_set_disconnected_nodes_get_ancestors_siCore_DOM_def instances)
declare l_set_disconnected_nodes_get_ancestors_siCore_DOM_axioms[instances]
lemma set_disconnected_nodes_get_ancestors_si_is_l_set_disconnected_nodes_get_ancestors_si [instances]:
"l_set_disconnected_nodes_get_ancestors_si set_disconnected_nodes_locs get_ancestors_si_locs"
using instances
apply(simp add: l_set_disconnected_nodes_get_ancestors_si_def)
using set_disconnected_nodes_get_ancestors_si
by fast
subsubsection ‹get\_attribute›
lemma get_attribute_is_l_get_attribute [instances]:
"l_get_attribute type_wf get_attribute get_attribute_locs"
apply(auto simp add: l_get_attribute_def)[1]
using i_get_attribute.get_attribute_reads apply fast
using type_wfDocument i_get_attribute.get_attribute_ok apply blast
using i_get_attribute.get_attribute_ptr_in_heap apply fast
done
subsubsection ‹to\_tree\_order›
global_interpretation l_to_tree_orderCore_DOM_defs get_child_nodes get_child_nodes_locs defines
to_tree_order = "l_to_tree_orderCore_DOM_defs.a_to_tree_order get_child_nodes" .
declare a_to_tree_order.simps [code]
interpretation i_to_tree_order?: l_to_tree_orderCore_DOM ShadowRootClass.known_ptr
ShadowRootClass.type_wf Shadow_DOM.get_child_nodes Shadow_DOM.get_child_nodes_locs to_tree_order
by(auto simp add: l_to_tree_orderCore_DOM_def l_to_tree_orderCore_DOM_axioms_def to_tree_order_def
instances)
declare l_to_tree_orderCore_DOM_axioms [instances]
subsubsection ‹to\_tree\_order\_si›
locale l_to_tree_order_siCore_DOM_defs =
l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs
for get_child_nodes :: "(_::linorder) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
partial_function (dom_prog) a_to_tree_order_si :: "(_) object_ptr ==> (_, (_) object_ptr list) dom_prog"
where
"a_to_tree_order_si ptr = (do {
children ← get_child_nodes ptr;
shadow_root_part ← (case cast ptr of
Some element_ptr ==> do {
shadow_root_opt ← get_shadow_root element_ptr;
(case shadow_root_opt of
Some shadow_root_ptr ==> return [cast shadow_root_ptr]
| None ==> return [])
} |
None ==> return []);
treeorders ← map_M a_to_tree_order_si ((map (cast) children) @ shadow_root_part);
return (ptr # concat treeorders)
})"
end
locale l_to_tree_order_si_defs =
fixes to_tree_order_si :: "(_) object_ptr ==> (_, (_) object_ptr list) dom_prog"
global_interpretation l_to_tree_order_siCore_DOM_defs get_child_nodes get_child_nodes_locs
get_shadow_root get_shadow_root_locs
defines to_tree_order_si = "a_to_tree_order_si" .
declare a_to_tree_order_si.simps [code]
locale l_to_tree_order_siShadow_DOM =
l_to_tree_order_si_defs +
l_to_tree_order_siCore_DOM_defs +
l_get_child_nodes +
l_get_shadow_root +
assumes to_tree_order_si_impl: "to_tree_order_si = a_to_tree_order_si"
begin
lemmas to_tree_order_si_def = a_to_tree_order_si.simps[folded to_tree_order_si_impl]
lemma to_tree_order_si_pure [simp]: "pure (to_tree_order_si ptr) h"
proof -
have "∀ptr h h' x. h ⊨ to_tree_order_si ptr →r x ⟶ h ⊨ to_tree_order_si ptr →h h' ⟶ h = h'"
proof (induct rule: a_to_tree_order_si.fixp_induct[folded to_tree_order_si_impl])
case 1
then show ?case
by (rule admissible_dom_prog)
next
case 2
then show ?case
by simp
next
case (3 f)
then have "∧x h. pure (f x) h"
by (metis is_OK_returns_heap_E is_OK_returns_result_E pure_def)
then have "∧xs h. pure (map_M f xs) h"
by(rule map_M_pure_I)
then show ?case
by(auto elim!: bind_returns_heap_E2 split: option.splits)
qed
then show ?thesis
unfolding pure_def
by (metis is_OK_returns_heap_E is_OK_returns_result_E)
qed
end
interpretation i_to_tree_order_si?: l_to_tree_order_siShadow_DOM to_tree_order_si get_child_nodes
get_child_nodes_locs get_shadow_root get_shadow_root_locs type_wf known_ptr
by(auto simp add: l_to_tree_order_siShadow_DOM_def l_to_tree_order_siShadow_DOM_axioms_def
to_tree_order_si_def instances)
declare l_to_tree_order_siShadow_DOM_axioms [instances]
subsubsection ‹first\_in\_tree\_order›
global_interpretation l_first_in_tree_orderCore_DOM_defs to_tree_order defines
first_in_tree_order = "l_first_in_tree_orderCore_DOM_defs.a_first_in_tree_order to_tree_order" .
interpretation i_first_in_tree_order?: l_first_in_tree_orderCore_DOM to_tree_order first_in_tree_order
by(auto simp add: l_first_in_tree_orderCore_DOM_def first_in_tree_order_def)
declare l_first_in_tree_orderCore_DOM_axioms [instances]
lemma to_tree_order_is_l_to_tree_order [instances]: "l_to_tree_order to_tree_order"
by(auto simp add: l_to_tree_order_def)
subsubsection ‹first\_in\_tree\_order›
global_interpretation l_dummy defines
first_in_tree_order_si = "l_first_in_tree_orderCore_DOM_defs.a_first_in_tree_order to_tree_order_si"
.
subsubsection ‹get\_element\_by›
global_interpretation l_get_element_byCore_DOM_defs to_tree_order first_in_tree_order get_attribute
get_attribute_locs
defines
get_element_by_id =
"l_get_element_byCore_DOM_defs.a_get_element_by_id first_in_tree_order get_attribute" and
get_elements_by_class_name =
"l_get_element_byCore_DOM_defs.a_get_elements_by_class_name to_tree_order get_attribute" and
get_elements_by_tag_name =
"l_get_element_byCore_DOM_defs.a_get_elements_by_tag_name to_tree_order" .
interpretation i_get_element_by?: l_get_element_byCore_DOM to_tree_order first_in_tree_order
get_attribute get_attribute_locs get_element_by_id get_elements_by_class_name
get_elements_by_tag_name type_wf
by(auto simp add: l_get_element_byCore_DOM_def l_get_element_byCore_DOM_axioms_def
get_element_by_id_def get_elements_by_class_name_def get_elements_by_tag_name_def
instances)
declare l_get_element_byCore_DOM_axioms[instances]
lemma get_element_by_is_l_get_element_by [instances]:
"l_get_element_by get_element_by_id get_elements_by_tag_name to_tree_order"
apply(auto simp add: l_get_element_by_def)[1]
using get_element_by_id_result_in_tree_order apply fast
done
subsubsection ‹get\_element\_by\_si›
global_interpretation l_dummy defines
get_element_by_id_si =
"l_get_element_byCore_DOM_defs.a_get_element_by_id first_in_tree_order_si get_attribute" and
get_elements_by_class_name_si =
"l_get_element_byCore_DOM_defs.a_get_elements_by_class_name to_tree_order_si get_attribute" and
get_elements_by_tag_name_si =
"l_get_element_byCore_DOM_defs.a_get_elements_by_tag_name to_tree_order_si"
.
subsubsection ‹find\_slot›
locale l_find_slotShadow_DOM_defs =
l_get_parent_defs get_parent get_parent_locs +
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs +
l_get_mode_defs get_mode get_mode_locs +
l_get_attribute_defs get_attribute get_attribute_locs +
l_get_tag_name_defs get_tag_name get_tag_name_locs +
l_first_in_tree_order_defs first_in_tree_order
for get_parent :: "(_) node_ptr ==> ((_) heap, exception, (_::linorder) object_ptr option) prog"
and get_parent_locs :: "((_) heap ==> (_) heap ==> bool) set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_mode :: "(_) shadow_root_ptr ==> ((_) heap, exception, shadow_root_mode) prog"
and get_mode_locs :: "(_) shadow_root_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_attribute :: "(_) element_ptr ==> char list ==> ((_) heap, exception, char list option) prog"
and get_attribute_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_tag_name :: "(_) element_ptr ==> ((_) heap, exception, char list) prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and first_in_tree_order ::
"(_) object_ptr ==> ((_) object_ptr ==> ((_) heap, exception, (_) element_ptr option) prog) ==>
((_) heap, exception, (_) element_ptr option) prog"
begin
definition a_find_slot :: "bool ==> (_) node_ptr ==> (_, (_) element_ptr option) dom_prog"
where
"a_find_slot open_flag slotable = do {
parent_opt ← get_parent slotable;
(case parent_opt of
Some parent ==>
if is_element_ptr_kind parent
then do {
shadow_root_ptr_opt ← get_shadow_root (the (cast parent));
(case shadow_root_ptr_opt of
Some shadow_root_ptr ==> do {
shadow_root_mode ← get_mode shadow_root_ptr;
if open_flag ∧ shadow_root_mode ≠ Open
then return None
else first_in_tree_order (cast shadow_root_ptr) (λptr. if is_element_ptr_kind ptr
then do {
tag ← get_tag_name (the (cast ptr));
name_attr ← get_attribute (the (cast ptr)) ''name'';
slotable_name_attr ← (if is_element_ptr_kind slotable
then get_attribute (the (cast slotable)) ''slot''
else return None);
(if (tag = ''slot'' ∧ (name_attr = slotable_name_attr ∨
(name_attr = None ∧ slotable_name_attr = Some '''') ∨
(name_attr = Some '''' ∧ slotable_name_attr = None)))
then return (Some (the (cast ptr)))
else return None)}
else return None)}
| None ==> return None)}
else return None
| _ ==> return None)}"
definition a_assigned_slot :: "(_) node_ptr ==> (_, (_) element_ptr option) dom_prog"
where
"a_assigned_slot = a_find_slot True"
end
global_interpretation l_find_slotShadow_DOM_defs get_parent get_parent_locs get_shadow_root
get_shadow_root_locs get_mode get_mode_locs get_attribute get_attribute_locs get_tag_name
get_tag_name_locs first_in_tree_order
defines find_slot = a_find_slot
and assigned_slot = a_assigned_slot
.
locale l_find_slot_defs =
fixes find_slot :: "bool ==> (_) node_ptr ==> (_, (_) element_ptr option) dom_prog"
and assigned_slot :: "(_) node_ptr ==> (_, (_) element_ptr option) dom_prog"
locale l_find_slotShadow_DOM =
l_find_slotShadow_DOM_defs +
l_find_slot_defs +
l_get_parent +
l_get_shadow_root +
l_get_mode +
l_get_attribute +
l_get_tag_name +
l_to_tree_order +
l_first_in_tree_orderCore_DOM +
assumes find_slot_impl: "find_slot = a_find_slot"
assumes assigned_slot_impl: "assigned_slot = a_assigned_slot"
begin
lemmas find_slot_def = find_slot_impl[unfolded a_find_slot_def]
lemmas assigned_slot_def = assigned_slot_impl[unfolded a_assigned_slot_def]
lemma find_slot_ptr_in_heap:
assumes "h ⊨ find_slot open_flag slotable →r slot_opt"
shows "slotable |∈| node_ptr_kinds h"
using assms
apply(auto simp add: find_slot_def elim!: bind_returns_result_E2)[1]
using get_parent_ptr_in_heap by blast
lemma find_slot_slot_in_heap:
assumes "h ⊨ find_slot open_flag slotable →r Some slot"
shows "slot |∈| element_ptr_kinds h"
using assms
apply(auto simp add: find_slot_def first_in_tree_order_def
elim!: bind_returns_result_E2 map_filter_M_pure_E[where y=slot]
split: option.splits if_splits list.splits
intro!: map_filter_M_pure bind_pure_I)[1]
using get_tag_name_ptr_in_heap by blast+
lemma find_slot_pure [simp]: "pure (find_slot open_flag slotable) h"
by(auto simp add: find_slot_def first_in_tree_order_def
intro!: bind_pure_I map_filter_M_pure
split: option.splits list.splits)
end
interpretation i_find_slot?: l_find_slotShadow_DOM get_parent get_parent_locs get_shadow_root
get_shadow_root_locs get_mode get_mode_locs get_attribute get_attribute_locs get_tag_name
get_tag_name_locs first_in_tree_order find_slot assigned_slot type_wf known_ptr known_ptrs
get_child_nodes get_child_nodes_locs to_tree_order
by (auto simp add: find_slot_def assigned_slot_def l_find_slotShadow_DOM_def
l_find_slotShadow_DOM_axioms_def instances)
declare l_find_slotShadow_DOM_axioms [instances]
locale l_find_slot = l_find_slot_defs +
assumes find_slot_ptr_in_heap:
"h ⊨ find_slot open_flag slotable →r slot_opt ==> slotable |∈| node_ptr_kinds h"
assumes find_slot_slot_in_heap:
"h ⊨ find_slot open_flag slotable →r Some slot ==> slot |∈| element_ptr_kinds h"
assumes find_slot_pure [simp]:
"pure (find_slot open_flag slotable) h"
lemma find_slot_is_l_find_slot [instances]: "l_find_slot find_slot"
apply(auto simp add: l_find_slot_def)[1]
using find_slot_ptr_in_heap apply fast
using find_slot_slot_in_heap apply fast
done
subsubsection ‹get\_disconnected\_nodes›
locale l_get_disconnected_nodesShadow_DOM =
CD: l_get_disconnected_nodesCore_DOM type_wfCore_DOM get_disconnected_nodes
get_disconnected_nodes_locs +
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and get_disconnected_nodes :: "(_) document_ptr ==> (_, (_) node_ptr list) dom_prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap ==> (_) heap ==> bool) set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
begin
lemma get_disconnected_nodes_ok:
"type_wf h ==> document_ptr |∈| document_ptr_kinds h ==>
h ⊨ ok (get_disconnected_nodes document_ptr)"
apply(unfold type_wf_impl get_disconnected_nodes_impl[unfolded a_get_disconnected_nodes_def])
using CD.get_disconnected_nodes_ok CD.type_wf_impl ShadowRootClass.type_wfDocument
by blast
end
interpretation i_get_disconnected_nodes?: l_get_disconnected_nodesShadow_DOM type_wf
DocumentClass.type_wf get_disconnected_nodes get_disconnected_nodes_locs
by(auto simp add: l_get_disconnected_nodesShadow_DOM_def l_get_disconnected_nodesShadow_DOM_axioms_def
instances)
declare l_get_disconnected_nodesShadow_DOM_axioms [instances]
lemma get_disconnected_nodes_is_l_get_disconnected_nodes [instances]:
"l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs"
apply(auto simp add: l_get_disconnected_nodes_def)[1]
using i_get_disconnected_nodes.get_disconnected_nodes_reads apply fast
using get_disconnected_nodes_ok apply fast
using i_get_disconnected_nodes.get_disconnected_nodes_ptr_in_heap apply fast
done
paragraph ‹set\_child\_nodes›
locale l_set_child_nodes_get_disconnected_nodesShadow_DOM =
l_set_child_nodesShadow_DOM +
l_get_disconnected_nodesShadow_DOM
begin
lemma set_child_nodes_get_disconnected_nodes:
"∀w ∈ set_child_nodes_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_disconnected_nodes_locs ptr'. r h h'))"
by(auto simp add: set_child_nodes_locs_def CD.set_child_nodes_locs_def
CD.get_disconnected_nodes_locs_def all_args_def)
end
interpretation
i_set_child_nodes_get_disconnected_nodes?: l_set_child_nodes_get_disconnected_nodesShadow_DOM type_wf
known_ptr DocumentClass.type_wf DocumentClass.known_ptr set_child_nodes set_child_nodes_locs
Core_DOM_Functions.set_child_nodes Core_DOM_Functions.set_child_nodes_locs
get_disconnected_nodes get_disconnected_nodes_locs
apply(auto simp add: l_set_child_nodes_get_disconnected_nodesShadow_DOM_def instances)[1]
by(unfold_locales)
declare l_set_child_nodes_get_disconnected_nodesShadow_DOM_axioms[instances]
lemma set_child_nodes_get_disconnected_nodes_is_l_set_child_nodes_get_disconnected_nodes [instances]:
"l_set_child_nodes_get_disconnected_nodes type_wf set_child_nodes set_child_nodes_locs
get_disconnected_nodes get_disconnected_nodes_locs"
using set_child_nodes_is_l_set_child_nodes get_disconnected_nodes_is_l_get_disconnected_nodes
apply(simp add: l_set_child_nodes_get_disconnected_nodes_def
l_set_child_nodes_get_disconnected_nodes_axioms_def)
using set_child_nodes_get_disconnected_nodes
by fast
paragraph ‹set\_disconnected\_nodes›
lemma set_disconnected_nodes_get_disconnected_nodes_l_set_disconnected_nodes_get_disconnected_nodes
[instances]:
"l_set_disconnected_nodes_get_disconnected_nodes ShadowRootClass.type_wf get_disconnected_nodes
get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs"
apply(auto simp add: l_set_disconnected_nodes_get_disconnected_nodes_def
l_set_disconnected_nodes_get_disconnected_nodes_axioms_def instances)[1]
using i_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes
apply fast
using i_set_disconnected_nodes_get_disconnected_nodes.set_disconnected_nodes_get_disconnected_nodes_different_pointers
apply fast
done
paragraph ‹delete\_shadow\_root›
locale l_delete_shadow_root_get_disconnected_nodesShadow_DOM =
l_get_disconnected_nodesShadow_DOM
begin
lemma get_disconnected_nodes_delete_shadow_root: "h ⊨ deleteShadowRoot_M shadow_root_ptr →h h'
==> r ∈ get_disconnected_nodes_locs ptr' ==> r h h'"
by(auto simp add: CD.get_disconnected_nodes_locs_def delete_shadow_root_get_MDocument)
end
locale l_delete_shadow_root_get_disconnected_nodes = l_get_disconnected_nodes_defs +
assumes get_disconnected_nodes_delete_shadow_root: "h ⊨ deleteShadowRoot_M shadow_root_ptr →h h'
==> r ∈ get_disconnected_nodes_locs ptr' ==> r h h'"
interpretation l_delete_shadow_root_get_disconnected_nodesShadow_DOM type_wf DocumentClass.type_wf
get_disconnected_nodes get_disconnected_nodes_locs
by(auto simp add: l_delete_shadow_root_get_disconnected_nodesShadow_DOM_def instances)
lemma l_delete_shadow_root_get_disconnected_nodes_get_disconnected_nodes_locs [instances]: "l_delete_shadow_root_get_disconnected_nodes get_disconnected_nodes_locs"
apply(auto simp add: l_delete_shadow_root_get_disconnected_nodes_def)[1]
using get_disconnected_nodes_delete_shadow_root apply fast
done
paragraph ‹set\_shadow\_root›
locale l_set_shadow_root_get_disconnected_nodesShadow_DOM =
l_set_shadow_rootShadow_DOM +
l_get_disconnected_nodesShadow_DOM
begin
lemma set_shadow_root_get_disconnected_nodes:
"∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_disconnected_nodes_locs ptr'. r h h'))"
by(auto simp add: set_shadow_root_locs_def CD.get_disconnected_nodes_locs_def all_args_def)
end
interpretation i_set_shadow_root_get_disconnected_nodes?:
l_set_shadow_root_get_disconnected_nodesShadow_DOM type_wf set_shadow_root set_shadow_root_locs
DocumentClass.type_wf get_disconnected_nodes get_disconnected_nodes_locs
apply(auto simp add: l_set_shadow_root_get_disconnected_nodesShadow_DOM_def instances)[1]
by(unfold_locales)
declare l_set_shadow_root_get_disconnected_nodesShadow_DOM_axioms[instances]
locale l_set_shadow_root_get_disconnected_nodes =
l_set_shadow_root_defs +
l_get_disconnected_nodes_defs +
assumes set_shadow_root_get_disconnected_nodes:
"∀w ∈ set_shadow_root_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_disconnected_nodes_locs ptr'. r h h'))"
lemma set_shadow_root_get_disconnected_nodes_is_l_set_shadow_root_get_disconnected_nodes [instances]:
"l_set_shadow_root_get_disconnected_nodes set_shadow_root_locs get_disconnected_nodes_locs"
using set_shadow_root_is_l_set_shadow_root get_disconnected_nodes_is_l_get_disconnected_nodes
apply(simp add: l_set_shadow_root_get_disconnected_nodes_def )
using set_shadow_root_get_disconnected_nodes
by fast
paragraph ‹set\_mode›
locale l_set_mode_get_disconnected_nodesShadow_DOM =
l_set_modeShadow_DOM +
l_get_disconnected_nodesShadow_DOM
begin
lemma set_mode_get_disconnected_nodes:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_disconnected_nodes_locs ptr'. r h h'))"
by(auto simp add: set_mode_locs_def
CD.get_disconnected_nodes_locs_impl[unfolded CD.a_get_disconnected_nodes_locs_def]
all_args_def)
end
interpretation i_set_mode_get_disconnected_nodes?: l_set_mode_get_disconnected_nodesShadow_DOM type_wf
set_mode set_mode_locs DocumentClass.type_wf get_disconnected_nodes get_disconnected_nodes_locs
by unfold_locales
declare l_set_mode_get_disconnected_nodesShadow_DOM_axioms[instances]
locale l_set_mode_get_disconnected_nodes = l_set_mode + l_get_disconnected_nodes +
assumes set_mode_get_disconnected_nodes:
"∀w ∈ set_mode_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_disconnected_nodes_locs ptr'. r h h'))"
lemma set_mode_get_disconnected_nodes_is_l_set_mode_get_disconnected_nodes [instances]:
"l_set_mode_get_disconnected_nodes type_wf set_mode set_mode_locs get_disconnected_nodes
get_disconnected_nodes_locs"
using set_mode_is_l_set_mode get_disconnected_nodes_is_l_get_disconnected_nodes
apply(simp add: l_set_mode_get_disconnected_nodes_def
l_set_mode_get_disconnected_nodes_axioms_def)
using set_mode_get_disconnected_nodes
by fast
paragraph ‹new\_shadow\_root›
locale l_new_shadow_root_get_disconnected_nodesShadow_DOM =
l_get_disconnected_nodesShadow_DOM type_wf type_wfCore_DOM get_disconnected_nodes
get_disconnected_nodes_locs
for type_wf :: "(_) heap ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and get_disconnected_nodes :: "(_) document_ptr ==> (_, (_) node_ptr list) dom_prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
lemma get_disconnected_nodes_new_shadow_root:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →h h'
==> r ∈ get_disconnected_nodes_locs ptr' ==> r h h'"
by(auto simp add: CD.get_disconnected_nodes_locs_def new_shadow_root_get_MDocument)
end
interpretation i_new_shadow_root_get_disconnected_nodes?:
l_new_shadow_root_get_disconnected_nodesShadow_DOM type_wf DocumentClass.type_wf
get_disconnected_nodes get_disconnected_nodes_locs
by unfold_locales
declare l_new_shadow_root_get_disconnected_nodesShadow_DOM_axioms[instances]
locale l_new_shadow_root_get_disconnected_nodes = l_get_disconnected_nodes_defs +
assumes get_disconnected_nodes_new_shadow_root:
"h ⊨ newShadowRoot_M →r new_shadow_root_ptr ==> h ⊨ newShadowRoot_M →h h'
==> r ∈ get_disconnected_nodes_locs ptr' ==> r h h'"
lemma new_shadow_root_get_disconnected_nodes_is_l_new_shadow_root_get_disconnected_nodes [instances]:
"l_new_shadow_root_get_disconnected_nodes get_disconnected_nodes_locs"
apply (auto simp add: l_new_shadow_root_get_disconnected_nodes_def)[1]
using get_disconnected_nodes_new_shadow_root apply fast
done
subsubsection ‹remove\_shadow\_root›
locale l_remove_shadow_rootShadow_DOM_defs =
l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs +
l_set_shadow_root_defs set_shadow_root set_shadow_root_locs +
l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs
for get_child_nodes :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and set_shadow_root ::
"(_) element_ptr ==> (_) shadow_root_ptr option ==> ((_) heap, exception, unit) prog"
and set_shadow_root_locs :: "(_) element_ptr ==> ((_) heap, exception, unit) prog set"
and get_disconnected_nodes :: "(_) document_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
definition a_remove_shadow_root :: "(_) element_ptr ==> (_, unit) dom_prog" where
"a_remove_shadow_root element_ptr = do {
shadow_root_ptr_opt ← get_shadow_root element_ptr;
(case shadow_root_ptr_opt of
Some shadow_root_ptr ==> do {
children ← get_child_nodes (cast shadow_root_ptr);
(if children = []
then do {
set_shadow_root element_ptr None;
delete_M shadow_root_ptr
} else do {
error HierarchyRequestError
})
} |
None ==> error HierarchyRequestError)
}"
definition a_remove_shadow_root_locs ::
"(_) element_ptr ==> (_) shadow_root_ptr ==> ((_, unit) dom_prog) set"
where
"a_remove_shadow_root_locs element_ptr shadow_root_ptr ≡
set_shadow_root_locs element_ptr ∪ {delete_M shadow_root_ptr}"
end
global_interpretation l_remove_shadow_rootShadow_DOM_defs get_child_nodes get_child_nodes_locs
get_shadow_root get_shadow_root_locs set_shadow_root set_shadow_root_locs get_disconnected_nodes
get_disconnected_nodes_locs
defines remove_shadow_root = "a_remove_shadow_root"
and remove_shadow_root_locs = a_remove_shadow_root_locs
.
locale l_remove_shadow_root_defs =
fixes remove_shadow_root :: "(_) element_ptr ==> (_, unit) dom_prog"
fixes remove_shadow_root_locs ::
"(_) element_ptr ==> (_) shadow_root_ptr ==> ((_, unit) dom_prog) set"
locale l_remove_shadow_rootShadow_DOM =
l_remove_shadow_rootShadow_DOM_defs +
l_remove_shadow_root_defs +
l_get_shadow_rootShadow_DOM +
l_set_shadow_rootShadow_DOM +
l_get_child_nodes +
l_get_disconnected_nodes type_wf get_disconnected_nodes get_disconnected_nodes_locs +
assumes remove_shadow_root_impl: "remove_shadow_root = a_remove_shadow_root"
assumes remove_shadow_root_locs_impl: "remove_shadow_root_locs = a_remove_shadow_root_locs"
begin
lemmas remove_shadow_root_def =
remove_shadow_root_impl[unfolded remove_shadow_root_def a_remove_shadow_root_def]
lemmas remove_shadow_root_locs_def =
remove_shadow_root_locs_impl[unfolded remove_shadow_root_locs_def a_remove_shadow_root_locs_def]
lemma remove_shadow_root_writes:
"writes (remove_shadow_root_locs element_ptr (the |h ⊨ get_shadow_root element_ptr|r))
(remove_shadow_root element_ptr) h h'"
apply(auto simp add: remove_shadow_root_locs_def remove_shadow_root_def all_args_def
writes_union_right_I writes_union_left_I set_shadow_root_writes
intro!: writes_bind writes_bind_pure[OF get_shadow_root_pure]
writes_bind_pure[OF get_child_nodes_pure]
intro: writes_subset[OF set_shadow_root_writes] writes_subset[OF writes_singleton2]
split: option.splits)[1]
using writes_union_left_I[OF set_shadow_root_writes]
apply (metis inf_sup_aci(5) insert_is_Un)
using writes_union_right_I[OF writes_singleton[of deleteShadowRoot_M]]
by (smt (verit, best) insert_is_Un writes_singleton2 writes_union_left_I)
end
interpretation i_remove_shadow_root?: l_remove_shadow_rootShadow_DOM get_child_nodes
get_child_nodes_locs get_shadow_root get_shadow_root_locs set_shadow_root set_shadow_root_locs
get_disconnected_nodes get_disconnected_nodes_locs remove_shadow_root remove_shadow_root_locs
type_wf known_ptr
by(auto simp add: l_remove_shadow_rootShadow_DOM_def l_remove_shadow_rootShadow_DOM_axioms_def
remove_shadow_root_def remove_shadow_root_locs_def instances)
declare l_remove_shadow_rootShadow_DOM_axioms [instances]
paragraph ‹get\_child\_nodes›
locale l_remove_shadow_root_get_child_nodesShadow_DOM =
l_get_child_nodesShadow_DOM +
l_remove_shadow_rootShadow_DOM
begin
lemma remove_shadow_root_get_child_nodes_different_pointers:
assumes "ptr ≠ cast shadow_root_ptr"
assumes "w ∈ remove_shadow_root_locs element_ptr shadow_root_ptr"
assumes "h ⊨ w →h h'"
assumes "r ∈ get_child_nodes_locs ptr"
shows "r h h'"
using assms
apply(auto simp add: all_args_def get_child_nodes_locs_def CD.get_child_nodes_locs_def
remove_shadow_root_locs_def set_shadow_root_locs_def
delete_shadow_root_get_MObject delete_shadow_root_get_MShadowRoot
delete_shadow_root_get_MShadowRoot delete_shadow_root_get_MElement
delete_shadow_root_get_MDocument[rotated]
element_put_get_preserved[where setter=shadow_root_opt_update]
intro: is_shadow_root_ptr_kind_obtains
elim: is_document_ptr_kind_obtains is_shadow_root_ptr_kind_obtains
split: if_splits option.splits)[1]
done
end
locale l_remove_shadow_root_get_child_nodes = l_get_child_nodes_defs + l_remove_shadow_root_defs +
assumes remove_shadow_root_get_child_nodes_different_pointers:
"ptr ≠ cast shadow_root_ptr ==> w ∈ remove_shadow_root_locs element_ptr shadow_root_ptr ==>
h ⊨ w →h h' ==> r ∈ get_child_nodes_locs ptr ==> r h h'"
interpretation i_remove_shadow_root_get_child_nodes?: l_remove_shadow_root_get_child_nodesShadow_DOM
type_wf known_ptr DocumentClass.type_wf DocumentClass.known_ptr get_child_nodes
get_child_nodes_locs Core_DOM_Functions.get_child_nodes Core_DOM_Functions.get_child_nodes_locs
get_shadow_root get_shadow_root_locs set_shadow_root set_shadow_root_locs get_disconnected_nodes
get_disconnected_nodes_locs remove_shadow_root remove_shadow_root_locs
by(auto simp add: l_remove_shadow_root_get_child_nodesShadow_DOM_def instances)
declare l_remove_shadow_root_get_child_nodesShadow_DOM_axioms[instances]
lemma remove_shadow_root_get_child_nodes_is_l_remove_shadow_root_get_child_nodes [instances]:
"l_remove_shadow_root_get_child_nodes get_child_nodes_locs remove_shadow_root_locs"
apply(auto simp add: l_remove_shadow_root_get_child_nodes_def instances )[1]
using remove_shadow_root_get_child_nodes_different_pointers apply fast
done
paragraph ‹get\_tag\_name›
locale l_remove_shadow_root_get_tag_nameShadow_DOM =
l_get_tag_nameShadow_DOM +
l_remove_shadow_rootShadow_DOM
begin
lemma remove_shadow_root_get_tag_name:
assumes "w ∈ remove_shadow_root_locs element_ptr shadow_root_ptr"
assumes "h ⊨ w →h h'"
assumes "r ∈ get_tag_name_locs ptr"
shows "r h h'"
using assms
by(auto simp add: all_args_def remove_shadow_root_locs_def set_shadow_root_locs_def
CD.get_tag_name_locs_def delete_shadow_root_get_MElement
element_put_get_preserved[where setter=shadow_root_opt_update]
split: if_splits option.splits)
end
locale l_remove_shadow_root_get_tag_name = l_get_tag_name_defs + l_remove_shadow_root_defs +
assumes remove_shadow_root_get_tag_name:
"w ∈ remove_shadow_root_locs element_ptr shadow_root_ptr ==> h ⊨ w →h h' ==>
r ∈ get_tag_name_locs ptr ==> r h h'"
interpretation i_remove_shadow_root_get_tag_name?: l_remove_shadow_root_get_tag_nameShadow_DOM type_wf
DocumentClass.type_wf get_tag_name get_tag_name_locs get_child_nodes get_child_nodes_locs
get_shadow_root get_shadow_root_locs set_shadow_root set_shadow_root_locs get_disconnected_nodes
get_disconnected_nodes_locs remove_shadow_root remove_shadow_root_locs known_ptr
by(auto simp add: l_remove_shadow_root_get_tag_nameShadow_DOM_def instances)
declare l_remove_shadow_root_get_tag_nameShadow_DOM_axioms[instances]
lemma remove_shadow_root_get_tag_name_is_l_remove_shadow_root_get_tag_name [instances]:
"l_remove_shadow_root_get_tag_name get_tag_name_locs remove_shadow_root_locs"
apply(auto simp add: l_remove_shadow_root_get_tag_name_def instances )[1]
using remove_shadow_root_get_tag_name apply fast
done
subsubsection ‹get\_owner\_document›
locale l_get_owner_documentShadow_DOM_defs =
l_get_host_defs get_host get_host_locs +
CD: l_get_owner_documentCore_DOM_defs get_root_node get_root_node_locs get_disconnected_nodes
get_disconnected_nodes_locs
for get_root_node :: "(_::linorder) object_ptr ==> ((_) heap, exception, (_) object_ptr) prog"
and get_root_node_locs :: "((_) heap ==> (_) heap ==> bool) set"
and get_disconnected_nodes :: "(_) document_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_host :: "(_) shadow_root_ptr ==> ((_) heap, exception, (_) element_ptr) prog"
and get_host_locs :: "((_) heap ==> (_) heap ==> bool) set"
begin
definition a_get_owner_documentshadow_root_ptr ::
"(_) shadow_root_ptr ==> unit ==> (_, (_) document_ptr) dom_prog"
where
"a_get_owner_documentshadow_root_ptr shadow_root_ptr _ = do {
host ← get_host shadow_root_ptr;
CD.a_get_owner_documentnode_ptr (cast host) ()
}"
definition a_get_owner_document_tups :: "(((_) object_ptr ==> bool) × ((_) object_ptr ==> unit
==> (_, (_) document_ptr) dom_prog)) list"
where
"a_get_owner_document_tups = [(is_shadow_root_ptr, a_get_owner_documentshadow_root_ptr ∘ the ∘ cast)]"
definition a_get_owner_document :: "(_::linorder) object_ptr ==> (_, (_) document_ptr) dom_prog"
where
"a_get_owner_document ptr = invoke (CD.a_get_owner_document_tups @ a_get_owner_document_tups) ptr ()"
end
global_interpretation l_get_owner_documentShadow_DOM_defs get_root_node_si get_root_node_si_locs
get_disconnected_nodes get_disconnected_nodes_locs get_host get_host_locs
defines get_owner_document_tups = a_get_owner_document_tups
and get_owner_document = a_get_owner_document
and get_owner_documentshadow_root_ptr = a_get_owner_documentshadow_root_ptr
and get_owner_document_tupsCore_DOM =
"l_get_owner_documentCore_DOM_defs.a_get_owner_document_tups
get_root_node_si get_disconnected_nodes"
and get_owner_documentnode_ptr =
"l_get_owner_documentCore_DOM_defs.a_get_owner_documentnode_ptr
get_root_node_si get_disconnected_nodes"
.
locale l_get_owner_documentShadow_DOM =
l_known_ptr known_ptr +
l_get_owner_documentShadow_DOM_defs get_root_node_si get_root_node_si_locs get_disconnected_nodes
get_disconnected_nodes_locs get_host get_host_locs +
l_get_owner_document_defs get_owner_document +
l_get_host get_host get_host_locs +
CD: l_get_owner_documentCore_DOM
get_parent get_parent_locs known_ptrCore_DOM type_wf get_disconnected_nodes
get_disconnected_nodes_locs get_root_node_si get_root_node_si_locs get_owner_documentCore_DOM
for known_ptr :: "(_::linorder) object_ptr ==> bool"
and known_ptrCore_DOM :: "(_::linorder) object_ptr ==> bool"
and get_parent :: "(_) node_ptr ==> ((_) heap, exception, (_) object_ptr option) prog"
and get_parent_locs :: "((_) heap ==> (_) heap ==> bool) set"
and type_wf :: "(_) heap ==> bool"
and get_disconnected_nodes :: "(_) document_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_root_node_si :: "(_) object_ptr ==> ((_) heap, exception, (_) object_ptr) prog"
and get_root_node_si_locs :: "((_) heap ==> (_) heap ==> bool) set"
and get_owner_documentCore_DOM :: "(_) object_ptr ==> ((_) heap, exception, (_) document_ptr) prog"
and get_host :: "(_) shadow_root_ptr ==> ((_) heap, exception, (_) element_ptr) prog"
and get_host_locs :: "((_) heap ==> (_) heap ==> bool) set"
and get_owner_document :: "(_) object_ptr ==> ((_) heap, exception, (_) document_ptr) prog" +
assumes known_ptr_impl: "known_ptr = a_known_ptr"
assumes get_owner_document_impl: "get_owner_document = a_get_owner_document"
begin
lemmas known_ptr_def = known_ptr_impl[unfolded a_known_ptr_def]
lemmas get_owner_document_def = a_get_owner_document_def[folded get_owner_document_impl]
lemma get_owner_document_pure [simp]:
"pure (get_owner_document ptr) h"
proof -
have "∧shadow_root_ptr. pure (a_get_owner_documentshadow_root_ptr shadow_root_ptr ()) h"
apply(auto simp add: a_get_owner_documentshadow_root_ptr_def
intro!: bind_pure_I filter_M_pure_I
split: option.splits)[1]
by(auto simp add: CD.a_get_owner_documentnode_ptr_def
intro!: bind_pure_I filter_M_pure_I
split: option.splits)
then show ?thesis
apply(auto simp add: get_owner_document_def)[1]
apply(split CD.get_owner_document_splits, rule conjI)+
apply(simp)
apply(auto simp add: a_get_owner_document_tups_def)[1]
apply(split invoke_splits, rule conjI)+
apply simp
by(auto intro!: bind_pure_I)
qed
lemma get_owner_document_ptr_in_heap:
assumes "h ⊨ ok (get_owner_document ptr)"
shows "ptr |∈| object_ptr_kinds h"
using assms
by(auto simp add: get_owner_document_def invoke_ptr_in_heap dest: is_OK_returns_heap_I)
end
interpretation i_get_owner_document?: l_get_owner_documentShadow_DOM known_ptr DocumentClass.known_ptr
get_parent get_parent_locs type_wf get_disconnected_nodes get_disconnected_nodes_locs
get_root_node_si get_root_node_si_locs CD.a_get_owner_document get_host get_host_locs
get_owner_document
by(auto simp add: instances l_get_owner_documentShadow_DOM_def l_get_owner_documentShadow_DOM_axioms_def
l_get_owner_documentCore_DOM_def l_get_owner_documentCore_DOM_axioms_def
get_owner_document_def Core_DOM_Functions.get_owner_document_def)
declare l_get_owner_documentShadow_DOM_axioms [instances]
lemma get_owner_document_is_l_get_owner_document [instances]:
"l_get_owner_document get_owner_document"
apply(auto simp add: l_get_owner_document_def)[1]
using get_owner_document_ptr_in_heap apply fast
done
subsubsection ‹remove\_child›
global_interpretation l_remove_childCore_DOM_defs get_child_nodes get_child_nodes_locs set_child_nodes
set_child_nodes_locs get_parent get_parent_locs get_owner_document get_disconnected_nodes
get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs
defines remove = "l_remove_childCore_DOM_defs.a_remove get_child_nodes set_child_nodes get_parent
get_owner_document get_disconnected_nodes set_disconnected_nodes"
and remove_child = "l_remove_childCore_DOM_defs.a_remove_child get_child_nodes set_child_nodes
get_owner_document get_disconnected_nodes set_disconnected_nodes"
and remove_child_locs = "l_remove_childCore_DOM_defs.a_remove_child_locs set_child_nodes_locs
set_disconnected_nodes_locs"
.
interpretation i_remove_child?: l_remove_childCore_DOM Shadow_DOM.get_child_nodes
Shadow_DOM.get_child_nodes_locs Shadow_DOM.set_child_nodes Shadow_DOM.set_child_nodes_locs
Shadow_DOM.get_parent Shadow_DOM.get_parent_locs Shadow_DOM.get_owner_document
get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
set_disconnected_nodes_locs remove_child remove_child_locs remove ShadowRootClass.type_wf
ShadowRootClass.known_ptr ShadowRootClass.known_ptrs
by(auto simp add: l_remove_childCore_DOM_def l_remove_childCore_DOM_axioms_def remove_child_def
remove_child_locs_def remove_def instances)
declare l_remove_childCore_DOM_axioms [instances]
subsubsection ‹get\_disconnected\_document›
locale l_get_disconnected_documentCore_DOM_defs =
l_get_disconnected_nodes_defs get_disconnected_nodes get_disconnected_nodes_locs
for get_disconnected_nodes ::
"(_::linorder) document_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
definition a_get_disconnected_document :: "(_) node_ptr ==> (_, (_) document_ptr) dom_prog"
where
"a_get_disconnected_document node_ptr = do {
check_in_heap (cast node_ptr);
ptrs ← document_ptr_kinds_M;
candidates ← filter_M (λdocument_ptr. do {
disconnected_nodes ← get_disconnected_nodes document_ptr;
return (node_ptr ∈ set disconnected_nodes)
}) ptrs;
(case candidates of
Cons document_ptr [] ==> return document_ptr |
_ ==> error HierarchyRequestError
)
}"
definition "a_get_disconnected_document_locs =
(∪document_ptr. get_disconnected_nodes_locs document_ptr) ∪
(∪ptr. {preserved (get_MObject ptr RObject.nothing)})"
end
locale l_get_disconnected_document_defs =
fixes get_disconnected_document :: "(_) node_ptr ==> (_, (_::linorder) document_ptr) dom_prog"
fixes get_disconnected_document_locs :: "((_) heap ==> (_) heap ==> bool) set"
locale l_get_disconnected_documentCore_DOM =
l_get_disconnected_documentCore_DOM_defs +
l_get_disconnected_document_defs +
l_get_disconnected_nodes +
assumes get_disconnected_document_impl:
"get_disconnected_document = a_get_disconnected_document"
assumes get_disconnected_document_locs_impl:
"get_disconnected_document_locs = a_get_disconnected_document_locs"
begin
lemmas get_disconnected_document_def =
get_disconnected_document_impl[unfolded a_get_disconnected_document_def]
lemmas get_disconnected_document_locs_def =
get_disconnected_document_locs_impl[unfolded a_get_disconnected_document_locs_def]
lemma get_disconnected_document_pure [simp]: "pure (get_disconnected_document ptr) h"
using get_disconnected_nodes_pure
by(auto simp add: get_disconnected_document_def
intro!: bind_pure_I filter_M_pure_I
split: list.splits)
lemma get_disconnected_document_ptr_in_heap [simp]:
"h ⊨ ok (get_disconnected_document node_ptr) ==> node_ptr |∈| node_ptr_kinds h"
using get_disconnected_document_def is_OK_returns_result_I check_in_heap_ptr_in_heap
by (metis (no_types, lifting) bind_returns_heap_E get_disconnected_document_pure
node_ptr_kinds_commutes pure_pure)
lemma get_disconnected_document_disconnected_document_in_heap:
assumes "h ⊨ get_disconnected_document child_node →r disconnected_document"
shows "disconnected_document |∈| document_ptr_kinds h"
using assms get_disconnected_nodes_pure
by(auto simp add: get_disconnected_document_def elim!: bind_returns_result_E2
dest!: filter_M_not_more_elements[where x=disconnected_document]
intro!: filter_M_pure_I bind_pure_I
split: if_splits list.splits)
lemma get_disconnected_document_reads:
"reads get_disconnected_document_locs (get_disconnected_document node_ptr) h h'"
using get_disconnected_nodes_reads[unfolded reads_def]
by(auto simp add: get_disconnected_document_def get_disconnected_document_locs_def
intro!: reads_bind_pure reads_subset[OF check_in_heap_reads]
reads_subset[OF error_reads]
reads_subset[OF get_disconnected_nodes_reads] reads_subset[OF return_reads]
reads_subset[OF document_ptr_kinds_M_reads] filter_M_reads filter_M_pure_I
bind_pure_I
split: list.splits)
end
locale l_get_disconnected_document = l_get_disconnected_document_defs +
assumes get_disconnected_document_reads:
"reads get_disconnected_document_locs (get_disconnected_document node_ptr) h h'"
assumes get_disconnected_document_ptr_in_heap:
"h ⊨ ok (get_disconnected_document node_ptr) ==> node_ptr |∈| node_ptr_kinds h"
assumes get_disconnected_document_pure [simp]:
"pure (get_disconnected_document node_ptr) h"
assumes get_disconnected_document_disconnected_document_in_heap:
"h ⊨ get_disconnected_document child_node →r disconnected_document ==>
disconnected_document |∈| document_ptr_kinds h"
global_interpretation l_get_disconnected_documentCore_DOM_defs get_disconnected_nodes
get_disconnected_nodes_locs defines
get_disconnected_document = a_get_disconnected_document and
get_disconnected_document_locs = a_get_disconnected_document_locs .
interpretation i_get_disconnected_document?: l_get_disconnected_documentCore_DOM
get_disconnected_nodes get_disconnected_nodes_locs get_disconnected_document
get_disconnected_document_locs type_wf
by(auto simp add: l_get_disconnected_documentCore_DOM_def l_get_disconnected_documentCore_DOM_axioms_def
get_disconnected_document_def get_disconnected_document_locs_def instances)
declare l_get_disconnected_documentCore_DOM_axioms [instances]
lemma get_disconnected_document_is_l_get_disconnected_document [instances]:
"l_get_disconnected_document get_disconnected_document get_disconnected_document_locs"
apply(auto simp add: l_get_disconnected_document_def instances)[1]
using get_disconnected_document_ptr_in_heap get_disconnected_document_pure
get_disconnected_document_disconnected_document_in_heap get_disconnected_document_reads
by blast+
paragraph ‹get\_disconnected\_nodes›
locale l_set_tag_name_get_disconnected_nodesShadow_DOM =
l_set_tag_nameShadow_DOM +
l_get_disconnected_nodesShadow_DOM
begin
lemma set_tag_name_get_disconnected_nodes:
"∀w ∈ set_tag_name_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_disconnected_nodes_locs ptr'. r h h'))"
by(auto simp add: CD.set_tag_name_locs_impl[unfolded CD.a_set_tag_name_locs_def]
CD.get_disconnected_nodes_locs_impl[unfolded CD.a_get_disconnected_nodes_locs_def]
all_args_def)
end
interpretation
i_set_tag_name_get_disconnected_nodes?: l_set_tag_name_get_disconnected_nodesShadow_DOM type_wf
DocumentClass.type_wf set_tag_name set_tag_name_locs get_disconnected_nodes
get_disconnected_nodes_locs
by unfold_locales
declare l_set_tag_name_get_disconnected_nodesCore_DOM_axioms[instances]
lemma set_tag_name_get_disconnected_nodes_is_l_set_tag_name_get_disconnected_nodes [instances]:
"l_set_tag_name_get_disconnected_nodes type_wf set_tag_name set_tag_name_locs
get_disconnected_nodes get_disconnected_nodes_locs"
using set_tag_name_is_l_set_tag_name get_disconnected_nodes_is_l_get_disconnected_nodes
apply(simp add: l_set_tag_name_get_disconnected_nodes_def
l_set_tag_name_get_disconnected_nodes_axioms_def)
using set_tag_name_get_disconnected_nodes
by fast
subsubsection ‹adopt\_node›
global_interpretation l_adopt_nodeCore_DOM_defs get_owner_document get_parent get_parent_locs
remove_child remove_child_locs get_disconnected_nodes get_disconnected_nodes_locs
set_disconnected_nodes set_disconnected_nodes_locs
defines adopt_node = a_adopt_node
and adopt_node_locs = a_adopt_node_locs
.
interpretation i_adopt_node?: l_adopt_nodeCore_DOM get_owner_document get_parent get_parent_locs
remove_child remove_child_locs get_disconnected_nodes get_disconnected_nodes_locs
set_disconnected_nodes set_disconnected_nodes_locs adopt_node adopt_node_locs known_ptr type_wf
get_child_nodes get_child_nodes_locs known_ptrs set_child_nodes set_child_nodes_locs remove
by(auto simp add: l_adopt_nodeCore_DOM_def l_adopt_nodeCore_DOM_axioms_def adopt_node_def
adopt_node_locs_def instances)
declare l_adopt_nodeCore_DOM_axioms[instances]
lemma adopt_node_is_l_adopt_node [instances]: "l_adopt_node type_wf known_ptr known_ptrs get_parent
adopt_node adopt_node_locs get_child_nodes get_owner_document"
apply(auto simp add: l_adopt_node_def l_adopt_node_axioms_def instances)[1]
using adopt_node_writes apply fast
using adopt_node_pointers_preserved apply (fast, fast)
using adopt_node_types_preserved apply (fast, fast)
using adopt_node_child_in_heap apply fast
using adopt_node_children_subset apply fast
done
paragraph ‹get\_shadow\_root›
locale l_adopt_node_get_shadow_rootShadow_DOM =
l_set_child_nodes_get_shadow_rootShadow_DOM +
l_set_disconnected_nodes_get_shadow_rootShadow_DOM +
l_adopt_nodeCore_DOM
begin
lemma adopt_node_get_shadow_root:
"∀w ∈ adopt_node_locs parent owner_document document_ptr.
(h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
by(auto simp add: adopt_node_locs_def remove_child_locs_def all_args_def
set_disconnected_nodes_get_shadow_root set_child_nodes_get_shadow_root)
end
locale l_adopt_node_get_shadow_root = l_adopt_node_defs + l_get_shadow_root_defs +
assumes adopt_node_get_shadow_root:
"∀w ∈ adopt_node_locs parent owner_document document_ptr.
(h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
interpretation i_adopt_node_get_shadow_root?: l_adopt_node_get_shadow_rootShadow_DOM type_wf known_ptr
DocumentClass.type_wf DocumentClass.known_ptr set_child_nodes set_child_nodes_locs
Core_DOM_Functions.set_child_nodes Core_DOM_Functions.set_child_nodes_locs get_shadow_root
get_shadow_root_locs set_disconnected_nodes set_disconnected_nodes_locs get_owner_document
get_parent get_parent_locs remove_child remove_child_locs get_disconnected_nodes
get_disconnected_nodes_locs adopt_node adopt_node_locs get_child_nodes get_child_nodes_locs
known_ptrs remove
by(auto simp add: l_adopt_node_get_shadow_rootShadow_DOM_def instances)
declare l_adopt_node_get_shadow_rootShadow_DOM_axioms[instances]
lemma adopt_node_get_shadow_root_is_l_adopt_node_get_shadow_root [instances]:
"l_adopt_node_get_shadow_root adopt_node_locs get_shadow_root_locs"
apply(auto simp add: l_adopt_node_get_shadow_root_def)[1]
using adopt_node_get_shadow_root apply fast
done
subsubsection ‹insert\_before›
global_interpretation l_insert_beforeCore_DOM_defs get_parent get_parent_locs get_child_nodes
get_child_nodes_locs set_child_nodes set_child_nodes_locs get_ancestors_si get_ancestors_si_locs
adopt_node adopt_node_locs set_disconnected_nodes set_disconnected_nodes_locs
get_disconnected_nodes get_disconnected_nodes_locs get_owner_document
defines
next_sibling = a_next_sibling and
insert_node = a_insert_node and
ensure_pre_insertion_validity = a_ensure_pre_insertion_validity and
insert_before = a_insert_before and
insert_before_locs = a_insert_before_locs
.
global_interpretation l_append_childCore_DOM_defs insert_before
defines append_child = "l_append_childCore_DOM_defs.a_append_child insert_before"
.
interpretation i_insert_before?: l_insert_beforeCore_DOM get_parent get_parent_locs get_child_nodes
get_child_nodes_locs set_child_nodes set_child_nodes_locs get_ancestors_si get_ancestors_si_locs
adopt_node adopt_node_locs set_disconnected_nodes set_disconnected_nodes_locs get_disconnected_nodes
get_disconnected_nodes_locs get_owner_document insert_before insert_before_locs append_child type_wf
known_ptr known_ptrs
by(auto simp add: l_insert_beforeCore_DOM_def l_insert_beforeCore_DOM_axioms_def insert_before_def
insert_before_locs_def instances)
declare l_insert_beforeCore_DOM_axioms [instances]
interpretation i_append_child?: l_append_childCore_DOM append_child insert_before insert_before_locs
by(simp add: l_append_childCore_DOM_def instances append_child_def)
declare l_append_childCore_DOM_axioms[instances]
subsubsection ‹get\_assigned\_nodes›
fun map_filter_M2 :: "('x ==> ('heap, 'e, 'y option) prog) ==> 'x list
==> ('heap, 'e, 'y list) prog"
where
"map_filter_M2 f [] = return []" |
"map_filter_M2 f (x # xs) = do {
res ← f x;
remainder ← map_filter_M2 f xs;
return ((case res of Some r ==> [r] | None ==> []) @ remainder)
}"
lemma map_filter_M2_pure [simp]:
assumes "∧x. x ∈ set xs ==> pure (f x) h"
shows "pure (map_filter_M2 f xs) h"
using assms
apply(induct xs arbitrary: h)
by(auto elim!: bind_returns_result_E2 intro!: bind_pure_I)
lemma map_filter_pure_no_monad:
assumes "∧x. x ∈ set xs ==> pure (f x) h"
assumes "h ⊨ map_filter_M2 f xs →r ys"
shows
"ys = map the (filter (λx. x ≠ None) (map (λx. |h ⊨ f x|r) xs))" and
"∧x. x ∈ set xs ==> h ⊨ ok (f x)"
using assms
apply(induct xs arbitrary: h ys)
by(auto elim!: bind_returns_result_E2)
lemma map_filter_pure_foo:
assumes "∧x. x ∈ set xs ==> pure (f x) h"
assumes "h ⊨ map_filter_M2 f xs →r ys"
assumes "y ∈ set ys"
obtains x where "h ⊨ f x →r Some y" and "x ∈ set xs"
using assms
apply(induct xs arbitrary: ys)
by(auto elim!: bind_returns_result_E2)
lemma map_filter_M2_in_result:
assumes "h ⊨ map_filter_M2 P xs →r ys"
assumes "a ∈ set xs"
assumes "∧x. x ∈ set xs ==> pure (P x) h"
assumes "h ⊨ P a →r Some b"
shows "b ∈ set ys"
using assms
apply(induct xs arbitrary: h ys)
by(auto elim!: bind_returns_result_E2 )
locale l_assigned_nodesShadow_DOM_defs =
l_get_tag_name_defs get_tag_name get_tag_name_locs +
l_get_root_node_defs get_root_node get_root_node_locs +
l_get_host_defs get_host get_host_locs +
l_get_child_nodes_defs get_child_nodes get_child_nodes_locs +
l_find_slot_defs find_slot assigned_slot +
l_remove_defs remove +
l_insert_before_defs insert_before insert_before_locs +
l_append_child_defs append_child +
l_remove_shadow_root_defs remove_shadow_root remove_shadow_root_locs
for get_child_nodes :: "(_::linorder) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_tag_name :: "(_) element_ptr ==> ((_) heap, exception, char list) prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_root_node :: "(_) object_ptr ==> ((_) heap, exception, (_) object_ptr) prog"
and get_root_node_locs :: "((_) heap ==> (_) heap ==> bool) set"
and get_host :: "(_) shadow_root_ptr ==> ((_) heap, exception, (_) element_ptr) prog"
and get_host_locs :: "((_) heap ==> (_) heap ==> bool) set"
and find_slot :: "bool ==> (_) node_ptr ==> ((_) heap, exception, (_) element_ptr option) prog"
and assigned_slot :: "(_) node_ptr ==> ((_) heap, exception, (_) element_ptr option) prog"
and remove :: "(_) node_ptr ==> ((_) heap, exception, unit) prog"
and insert_before ::
"(_) object_ptr ==> (_) node_ptr ==> (_) node_ptr option ==> ((_) heap, exception, unit) prog"
and insert_before_locs :: "(_) object_ptr ==> (_) object_ptr option ==> (_) document_ptr ==>
(_) document_ptr ==> (_, unit) dom_prog set"
and append_child :: "(_) object_ptr ==> (_) node_ptr ==> ((_) heap, exception, unit) prog"
and remove_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, unit) prog"
and remove_shadow_root_locs :: "(_) element_ptr ==> (_) shadow_root_ptr ==>
((_) heap, exception, unit) prog set"
begin
definition a_assigned_nodes :: "(_) element_ptr ==> (_, (_) node_ptr list) dom_prog"
where
"a_assigned_nodes slot = do {
tag ← get_tag_name slot;
(if tag ≠ ''slot''
then error HierarchyRequestError
else return ());
root ← get_root_node (cast slot);
if is_shadow_root_ptr_kind root
then do {
host ← get_host (the (cast root));
children ← get_child_nodes (cast host);
filter_M (λslotable. do {
found_slot ← find_slot False slotable;
return (found_slot = Some slot)}) children}
else return []}"
partial_function (dom_prog) a_assigned_nodes_flatten ::
"(_) element_ptr ==> (_, (_) node_ptr list) dom_prog"
where
"a_assigned_nodes_flatten slot = do {
tag ← get_tag_name slot;
(if tag ≠ ''slot''
then error HierarchyRequestError
else return ());
root ← get_root_node (cast slot);
(if is_shadow_root_ptr_kind root
then do {
slotables ← a_assigned_nodes slot;
slotables_or_child_nodes ← (if slotables = []
then do {
get_child_nodes (cast slot)
} else do {
return slotables
});
list_of_lists ← map_M (λnode_ptr. do {
(case cast node_ptr of
Some element_ptr ==> do {
tag ← get_tag_name element_ptr;
(if tag = ''slot''
then do {
root ← get_root_node (cast element_ptr);
(if is_shadow_root_ptr_kind root
then do {
a_assigned_nodes_flatten element_ptr
} else do {
return [node_ptr]
})
} else do {
return [node_ptr]
})
}
| None ==> return [node_ptr])
}) slotables_or_child_nodes;
return (concat list_of_lists)
} else return [])
}"
definition a_flatten_dom :: "(_, unit) dom_prog" where
"a_flatten_dom = do {
tups ← element_ptr_kinds_M ⤜ map_filter_M2 (λelement_ptr. do {
tag ← get_tag_name element_ptr;
assigned_nodes ← a_assigned_nodes element_ptr;
(if tag = ''slot'' ∧ assigned_nodes ≠ []
then return (Some (element_ptr, assigned_nodes))
else return None)});
forall_M (λ(slot, assigned_nodes). do {
get_child_nodes (cast slot) ⤜ forall_M remove;
forall_M (append_child (cast slot)) assigned_nodes
}) tups;
shadow_root_ptr_kinds_M ⤜ forall_M (λshadow_root_ptr. do {
host ← get_host shadow_root_ptr;
get_child_nodes (cast host) ⤜ forall_M remove;
get_child_nodes (cast shadow_root_ptr) ⤜ forall_M (append_child (cast host));
remove_shadow_root host
});
return ()
}"
end
global_interpretation l_assigned_nodesShadow_DOM_defs get_child_nodes get_child_nodes_locs
get_tag_name get_tag_name_locs get_root_node get_root_node_locs get_host get_host_locs find_slot
assigned_slot remove insert_before insert_before_locs append_child remove_shadow_root
remove_shadow_root_locs
defines assigned_nodes = a_assigned_nodes
and assigned_nodes_flatten = a_assigned_nodes_flatten
and flatten_dom = a_flatten_dom
.
declare a_assigned_nodes_flatten.simps [code]
locale l_assigned_nodes_defs =
fixes assigned_nodes :: "(_) element_ptr ==> (_, (_) node_ptr list) dom_prog"
fixes assigned_nodes_flatten :: "(_) element_ptr ==> (_, (_) node_ptr list) dom_prog"
fixes flatten_dom :: "(_, unit) dom_prog"
locale l_assigned_nodesShadow_DOM =
l_assigned_nodes_defs
assigned_nodes assigned_nodes_flatten flatten_dom
+ l_assigned_nodesShadow_DOM_defs
get_child_nodes get_child_nodes_locs get_tag_name get_tag_name_locs get_root_node
get_root_node_locs get_host get_host_locs find_slot assigned_slot remove insert_before
insert_before_locs append_child remove_shadow_root remove_shadow_root_locs
+ l_get_shadow_root
type_wf get_shadow_root get_shadow_root_locs
+ l_set_shadow_root
type_wf set_shadow_root set_shadow_root_locs
+ l_remove
+ l_insert_before
insert_before insert_before_locs
+ l_find_slot
find_slot assigned_slot
+ l_get_tag_name
type_wf get_tag_name get_tag_name_locs
+ l_get_root_node
get_root_node get_root_node_locs get_parent get_parent_locs
+ l_get_host
get_host get_host_locs
+ l_get_child_nodes
type_wf known_ptr get_child_nodes get_child_nodes_locs
+ l_to_tree_order
to_tree_order
for known_ptr :: "(_::linorder) object_ptr ==> bool"
and assigned_nodes :: "(_) element_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and assigned_nodes_flatten :: "(_) element_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and flatten_dom :: "((_) heap, exception, unit) prog"
and get_child_nodes :: "(_) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_tag_name :: "(_) element_ptr ==> ((_) heap, exception, char list) prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_root_node :: "(_) object_ptr ==> ((_) heap, exception, (_) object_ptr) prog"
and get_root_node_locs :: "((_) heap ==> (_) heap ==> bool) set"
and get_host :: "(_) shadow_root_ptr ==> ((_) heap, exception, (_) element_ptr) prog"
and get_host_locs :: "((_) heap ==> (_) heap ==> bool) set"
and find_slot :: "bool ==> (_) node_ptr ==> ((_) heap, exception, (_) element_ptr option) prog"
and assigned_slot :: "(_) node_ptr ==> ((_) heap, exception, (_) element_ptr option) prog"
and remove :: "(_) node_ptr ==> ((_) heap, exception, unit) prog"
and insert_before ::
"(_) object_ptr ==> (_) node_ptr ==> (_) node_ptr option ==> ((_) heap, exception, unit) prog"
and insert_before_locs :: "(_) object_ptr ==> (_) object_ptr option ==> (_) document_ptr ==>
(_) document_ptr ==> (_, unit) dom_prog set"
and append_child :: "(_) object_ptr ==> (_) node_ptr ==> ((_) heap, exception, unit) prog"
and remove_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, unit) prog"
and remove_shadow_root_locs :: "(_) element_ptr ==> (_) shadow_root_ptr ==>
((_) heap, exception, unit) prog set"
and type_wf :: "(_) heap ==> bool"
and get_shadow_root ::
"(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and set_shadow_root ::
"(_) element_ptr ==> (_) shadow_root_ptr option ==> ((_) heap, exception, unit) prog"
and set_shadow_root_locs :: "(_) element_ptr ==> ((_) heap, exception, unit) prog set"
and get_parent :: "(_) node_ptr ==> ((_) heap, exception, (_) object_ptr option) prog"
and get_parent_locs :: "((_) heap ==> (_) heap ==> bool) set"
and to_tree_order :: "(_) object_ptr ==> ((_) heap, exception, (_) object_ptr list) prog" +
assumes assigned_nodes_impl: "assigned_nodes = a_assigned_nodes"
assumes flatten_dom_impl: "flatten_dom = a_flatten_dom"
begin
lemmas assigned_nodes_def = assigned_nodes_impl[unfolded a_assigned_nodes_def]
lemmas flatten_dom_def = flatten_dom_impl[unfolded a_flatten_dom_def, folded assigned_nodes_impl]
lemma assigned_nodes_pure [simp]: "pure (assigned_nodes slot) h"
by(auto simp add: assigned_nodes_def intro!: bind_pure_I filter_M_pure_I)
lemma assigned_nodes_ptr_in_heap:
assumes "h ⊨ ok (assigned_nodes slot)"
shows "slot |∈| element_ptr_kinds h"
using assms
apply(auto simp add: assigned_nodes_def)[1]
by (meson bind_is_OK_E is_OK_returns_result_I local.get_tag_name_ptr_in_heap)
lemma assigned_nodes_slot_is_slot:
assumes "h ⊨ ok (assigned_nodes slot)"
shows "h ⊨ get_tag_name slot →r ''slot''"
using assms
by(auto simp add: assigned_nodes_def elim!: bind_is_OK_E split: if_splits)
lemma assigned_nodes_different_ptr:
assumes "h ⊨ assigned_nodes slot →r nodes"
assumes "h ⊨ assigned_nodes slot' →r nodes'"
assumes "slot ≠ slot'"
shows "set nodes ∩ set nodes' = {}"
proof (rule ccontr)
assume "set nodes ∩ set nodes' ≠ {} "
then obtain common_ptr where "common_ptr ∈ set nodes" and "common_ptr ∈ set nodes'"
by auto
have "h ⊨ find_slot False common_ptr →r Some slot"
using ‹common_ptr ∈ set nodes›
using assms(1)
by(auto simp add: assigned_nodes_def
elim!: bind_returns_result_E2
split: if_splits
dest!: filter_M_holds_for_result[where x=common_ptr]
intro!: bind_pure_I)
moreover
have "h ⊨ find_slot False common_ptr →r Some slot'"
using ‹common_ptr ∈ set nodes'›
using assms(2)
by(auto simp add: assigned_nodes_def
elim!: bind_returns_result_E2
split: if_splits
dest!: filter_M_holds_for_result[where x=common_ptr]
intro!: bind_pure_I)
ultimately
show False
using assms(3)
by (meson option.inject returns_result_eq)
qed
end
interpretation i_assigned_nodes?: l_assigned_nodesShadow_DOM known_ptr assigned_nodes
assigned_nodes_flatten flatten_dom get_child_nodes get_child_nodes_locs get_tag_name
get_tag_name_locs get_root_node get_root_node_locs get_host get_host_locs find_slot
assigned_slot remove insert_before insert_before_locs append_child remove_shadow_root
remove_shadow_root_locs type_wf get_shadow_root get_shadow_root_locs set_shadow_root
set_shadow_root_locs get_parent get_parent_locs to_tree_order
by(auto simp add: instances l_assigned_nodesShadow_DOM_def l_assigned_nodesShadow_DOM_axioms_def
assigned_nodes_def flatten_dom_def)
declare l_assigned_nodesShadow_DOM_axioms [instances]
locale l_assigned_nodes = l_assigned_nodes_defs +
assumes assigned_nodes_pure [simp]: "pure (assigned_nodes slot) h"
assumes assigned_nodes_ptr_in_heap:
"h ⊨ ok (assigned_nodes slot) ==> slot |∈| element_ptr_kinds h"
assumes assigned_nodes_slot_is_slot:
"h ⊨ ok (assigned_nodes slot) ==> h ⊨ get_tag_name slot →r ''slot''"
assumes assigned_nodes_different_ptr:
"h ⊨ assigned_nodes slot →r nodes ==> h ⊨ assigned_nodes slot' →r nodes' ==>
slot ≠ slot' ==> set nodes ∩ set nodes' = {}"
lemma assigned_nodes_is_l_assigned_nodes [instances]: "l_assigned_nodes assigned_nodes"
apply(auto simp add: l_assigned_nodes_def)[1]
using assigned_nodes_ptr_in_heap apply fast
using assigned_nodes_slot_is_slot apply fast
using assigned_nodes_different_ptr apply fast
done
subsubsection‹
locale l_set_valShopen>What happens only to the first part of the memory when executing ‹
java.lang.NullPointerException
l_type_wf type_wf
for type_wf :: "(_) heap ==> bool"
and type_wfO\^>M :: (_) he \<ightarrow
and set_val :: "(_) character_data_ptr ==> char list ==> (_, unit) dom_prog"
and set_val_locs :: "(_) character_data_ptr ==> (_, unit) dom_prog set" +
assumes type_wf_impl: "type_wf = ShadowRootClass.type_wf"
begin
lemma set_val_ok:
"type_wf h ==> character_data_ptr |∈| character_data_ptr_kinds h ==>
h \turnstile ok (s characttag)"
java.lang.NullPointerException
lemma set_val_writes:
"writes (set_val_locs character_data_ptr) (set_val character_data_ptr tag) by (me (no_yp, li) \Psi cblinfu)
using CD.set_val_writes .
lemma set_val_pointers_preserved:
assumes "w ∈ set_val_locs character_data_ptr"
assumes "h ⊨ w →0\rangle$.›
shows "object_ptr_kinds h = object_ptr_kinds h'"
using assms CD.set_val_pointers_preserved by simp
lemma set_val_typess_preserved:
assumes "w ∈ set_val_locs character_data_ptr"
assumes "h ⊨ w →h h'"
shows "type_wf h = type_wf h'"
apply(unfold type_wf_impl)
using assms(1) type_wf_preserved[OF writes_singleton2 assms(2)]
java.lang.StringIndexOutOfBoundsException: Range [23, 4) out of bounds for length 92
split: if_splits)
end
interpretation
i_set_val?: l_set_valdow_DOM type_wf DocumentClass.type_wf set_val set_val_locs
apply(unfold_locales)
by (auto simp add: set_val_def set_val_locs_def)
declare l_set_valSM_axioms[instances]
lemma set_val_is_l_set_val [instances]: "l_set_val type_wf set_val set_val_locs"
apply(simp add: l_set_val_def)
using set_val_ok set_val_writes set_val_pointers_preserved set_val_typess_preserved
by blast
paragraph ‹get\_shadow\_root›
locale l_set_val_get_shadow_rootShadow_DOM =
l_set_valShadow_DOM +
l_get_shadow_rootShadow_DOM
begin
lemma set_val_get_shadow_root:
"∀w ∈ set_val_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
by(auto simp add: CD.set_val_locs_impl[unfolded CD.a_set_val_locs_def]
get_shadow_root_locs_def all_args_def)
end
locale l_set_val_get_shadow_root = l_set_val + l_get_shadow_root +
assumes set_val_get_shadow_root:
"∀w ∈ set_val_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_shadow_root_locs ptr'. r h h'))"
interpretation
i_set_val_get_shadow_root?: l_set_val_get_shadow_rootShadow_DOM type_wf DocumentClass.type_wf
set_val set_val_locs
get_shadow_root get_shadow_root_locs
>\^sub>dow_DOM_def instances)[1]
u l_set_valShadow_DOM_axioms
by unfold_locales
declare l_set_val_get_shadow_rootShadow_DOM_axioms[instances]
lemma set_val_get_shadow_root_is_l_set_val_get_shadow_root [instances]:
"l_set_val_get_shadow_root type_wf set_val set_val_locs get_shadow_root
get_shadow_root_locs"
using set_val_is_l_set_val get_shadow_root_is_l_get_shadow_root
apply(simp add: l_set_val_get_shadow_root_def l_set_val_get_shadow_root_axioms_def)
using set_val_get_shadow_root
by fast
paragraph ‹get\_tag\_type›
locale l_set_val_get_tag_nameShadow_DOM =
l_set_valShadow_DOM +
l_get_tag_nameShadow_DOM
begin
lemma set_val_get_tag_name:
"∀w ∈ set_val_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
by(auto simp add: CD.set_val_locs_impl[unfolded CD.a_set_val_locs_def]
CD.get_tag_name_locs_impl[unfolded CD.a_get_tag_name_locs_def]
all_args_def)
end
locale l_set_val_get_tag_name = l_set_val + l_get_tag_name +
assumes set_val_get_tag_name:
"∀w ∈ set_val_locs ptr. (h ⊨ w →h h' ⟶ (∀r ∈ get_tag_name_locs ptr'. r h h'))"
interpretation
i_set_val_get_tag_name?: l_set_val_get_tag_nameShadow_DOM type_wf DocumentClass.type_wf set_val
set_val_locs get_tag_name get_tag_name_locs
by unfold_locales
declare l_set_val_get_tag_nameShadow_DOM_axioms[instances]
lemma set_val_get_tag_name_is_l_set_val_get_tag_name [instances]:
"l_set_val_get_tag_name type_wf set_val set_val_locs get_tag_name get_tag_name_locs"
using set_val_is_l_set_val get_tag_name_is_l_get_tag_name
apply(simp add: l_set_val_get_tag_name_def l_set_val_get_tag_name_axioms_def)
using set_val_get_tag_name
by fast
subsubsection ‹create\_character\_data›
locale l_create_character_dataShadow_DOM =
CD: l_create_character_dataCore_DOM _ _ _ _ _ _ type_wfCore_DOM _ known_ptrCore_DOM +
l_known_ptr known_ptr
for known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool" +
assumes known_ptr_impl: "known_ptr = a_known_ptr"
begin
lemma create_character_data_document_in_heap:
assumes "h ⊨ ok (create_character_data document_ptr text)"
shows "document_ptr |∈| document_ptr_kinds h"
using assms CD.create_character_data_document_in_heap by simp
lemma create_character_data_known_ptr:
assumes "h ⊨ create_character_data document_ptr text →r new_character_data_ptr"
shows "known_ptr (cast new_character_data_ptr)"
using assms CD.create_character_data_known_ptr
by(simp add: known_ptr_impl CD.known_ptr_impl ShadowRootClass.a_known_ptr_def)
end
locale l_create_character_data = l_create_character_data_defs
interpretation i_create_character_data?: l_create_character_dataShadow_DOM get_disconnected_nodes
get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_val set_val_locs
create_character_data known_ptr DocumentClass.type_wf DocumentClass.known_ptr
by(auto simp add: l_create_character_dataShadow_DOM_def l_create_character_dataShadow_DOM_axioms_def
instances)
declare l_create_character_dataCore_DOM_axioms [instances]
subsubsection ‹create\_element›
locale l_create_elementShadow_DOM =
CD: l_create_elementCore_DOM get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
set_disconnected_nodes_locs set_tag_name set_tag_name_locs type_wfCore_DOM create_element
known_ptrCore_DOM +
l_known_ptr known_ptr
for get_disconnected_nodes :: "(_) document_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and set_disconnected_nodes ::
"(_) document_ptr ==> (_) node_ptr list ==> ((_) heap, exception, unit) prog"
and set_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap, exception, unit) prog set"
and set_tag_name :: "(_) element_ptr ==> char list ==> ((_) heap, exception, unit) prog"
and set_tag_name_locs :: "(_) element_ptr ==> ((_) heap, exception, unit) prog set"
and type_wf :: "(_) heap ==> bool"
and create_element ::
"(_) document_ptr ==> char list ==> ((_) heap, exception, (_) element_ptr) prog"
and known_ptr :: "(_) object_ptr ==> bool"
and type_wfCore_DOM :: "(_) heap ==> bool"
and known_ptrCore_DOM :: "(_) object_ptr ==> bool" +
assumes known_ptr_impl: "known_ptr = a_known_ptr"
begin
lemmas create_element_def = CD.create_element_def
lemma create_element_document_in_heap:
assumes "h ⊨ ok (create_element document_ptr tag)"
shows "document_ptr |∈| document_ptr_kinds h"
using CD.create_element_document_in_heap assms .
lemma create_element_known_ptr:
assumes "h ⊨ create_element document_ptr tag →r new_element_ptr"
shows "known_ptr (cast new_element_ptr)"
proof -
have "is_element_ptr new_element_ptr"
using assms
apply(auto simp add: create_element_def elim!: bind_returns_result_E)[1]
using new_element_is_element_ptr
by blast
then show ?thesis
by(auto simp add: known_ptr_impl known_ptr_defs DocumentClass.known_ptr_defs
CharacterDataClass.known_ptr_defs ElementClass.known_ptr_defs)
qed
end
interpretation i_create_element?: l_create_elementShadow_DOM get_disconnected_nodes
get_disconnected_nodes_locs set_disconnected_nodes set_disconnected_nodes_locs set_tag_name
set_tag_name_locs type_wf create_element known_ptr DocumentClass.type_wf DocumentClass.known_ptr
by(auto simp add: l_create_elementShadow_DOM_def l_create_elementShadow_DOM_axioms_def instances)
declare l_create_elementShadow_DOM_axioms[instances]
subsection ‹A wellformed heap (Core DOM)›
subsubsection ‹wellformed\_heap›
locale l_heap_is_wellformedShadow_DOM_defs =
CD: l_heap_is_wellformedCore_DOM_defs get_child_nodes get_child_nodes_locs get_disconnected_nodes
get_disconnected_nodes_locs +
l_get_shadow_root_defs get_shadow_root get_shadow_root_locs +
l_get_tag_name_defs get_tag_name get_tag_name_locs
for get_child_nodes :: "(_::linorder) object_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_disconnected_nodes :: "(_) document_ptr ==> ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_shadow_root :: "(_) element_ptr ==> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
and get_tag_name :: "(_) element_ptr ==> ((_) heap, exception, char list) prog"
and get_tag_name_locs :: "(_) element_ptr ==> ((_) heap ==> (_) heap ==> bool) set"
begin
definition a_host_shadow_root_rel :: "(_) heap ==> ((_) object_ptr × (_) object_ptr) set"
where
"a_host_shadow_root_rel h = (λ(x, y). (cast x, cast y)) ` {(host, shadow_root).
host |∈| element_ptr_kinds h ∧ |h ⊨ get_shadow_root host|r = Some shadow_root}"
lemma a_host_shadow_root_rel_code [code]: "a_host_shadow_root_rel h = set (concat (map
(λhost. (case |h ⊨ get_shadow_root host|r of
Some shadow_root ==> [(cast host, cast shadow_root)] |
None ==> []))
(sorted_list_of_fset (element_ptr_kinds h)))
)"
by(auto simp add: a_host_shadow_root_rel_def)
definition a_all_ptrs_in_heap :: "(_) heap ==> bool" where
"a_all_ptrs_in_heap h = ((∀ not_S_embed S * run_pure_adv nUA (λnot_S_embed S) init X Y H"
(h ⊨ get_shadow_root host →r Some shadow_root_ptr) ⟶
shadow_root_ptr |∈| shadow_root_ptr_kinds h))"
definition a_distinct_lists :: "(_) heap ==> bool"
finally s show ?case unfolding 🚫norm UA ≤ 1›, we need to introduce the following error term:
"a_distinct_lists h = distinct (concat (
map (λelement_ptr. (case |h ⊨ get_shadow_root element_ptr|r of
Sometext ‹
|h ⊨ element_ptr_kinds_M|r
definition a_shadow_root_valid :: "(_) heap ==> bool" where
"a_shadow_root_valid h = (∀shadow_root_ptr ∈ fset (shadow_root_ptr_kinds h).
(∃host ∈ fset(element_ptr_kinds h).
|h ⊨ get_tag_name host|lemma pure_o2h: ‹(norm ((run_A ⊗s ket empty) - run_B))2 ≤ (d+1) * Pfind' + d * P_nonterm›
|h ⊨ get_shadow_root host|r = Some shadow_root_ptr))"
definition a_heap_is_wellformed :: "(_) heap \<Rightarrow
where
"a_heap_is_wellformed h ⟷ CD.a_heap_is_wellformed h ∧
acyclic (CD.a_parent_child_rel h ∪ a_host_shadow_root_rel h) ∧
a_all_ptrs_in_heap h ∧
a_distinct_lists h ∧
have *: "sum (Rep_ell2 (ket c)) {..<d + 1} *C ket 0 = ket 0" if "c<d+1" for c
end
global_interpretation l_heap_is_wellformedShadow_DOM_defs get_child_nodes get_child_nodes_locs
get_disconnected_nodes get_disconnected_nodes_locs get_shadow_root get_shadow_root_locs
get_tag_name get_tag_name_locs
defines heap_is_wellformed = a_heap_is_wellformed
and parent_child_rel = CD.a_parent_child_rel
ot_relrl= ahot_shdwro_rel
and all_ptrs_in_heap = a_all_ptrs_in_heap
and distinct_lists = a_distinct_lists
and shadow_root_valid = a_shadow_root_valid
java.lang.NullPointerException
and parent_child_rel^sub>C\^subor_OM = CD.a_parent_child_rel
and acyclic_heapCore_DOM = CD.a_acyclic_heap
and all_ptrs_in_heap\<open>‹ commutes with \<open>UUA\close>›
and distinct_listsCore_DOM = CD.a_distinct_lists
and owner_document_validCore_DOM = CD.a_owner_document_valid
.
interpretation i_heap_is_wellformedCore_DOM: l_heap_is_wellformedCore_DOM known_ptr type_wf
get_child_nodes get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs
heap_is_wellformedCore_DOM parent_child_rel
by (auto simp add: l_heap_is_wellformedCore_DOM_def l_heap_is_wellformedCore_DOM_axioms_def
heap_is_wellformedCore_DOM_def parent_child_rel_def instances)
declare i_heap_is_wellformedCore_DOM.l_heap_is_wellformedCore_DOM_axioms[instances]
lemma heap_is_wellformedCore_DOM_is_l_heap_is_wellformed [instances]:
"l_heap_is_wellformed type_wf known_ptr heap_is_wellformedCore_DOM parent_child_rel get_child_nodes
get_disconnected_nodes"
apply(auto simp add: l_heap_is_wellformed_def)[1]
using i_heap_is_wellformed\>ore_DOM.heap_is_wellformed_children_in_heap apply blast
using i_heap_is_wellformedCore_DOM.heap_is_wellformed_disc_nodes_in_heap apply blast
java.lang.NullPointerException
using i_heap_is_wellformedoe_DOM.heap_is_wellformed_one_disc_parent apply blast
using i_heap_is_wellformedCore_DOM.heap_is_wellformed_children_disc_nodes_different apply blast
java.lang.StringIndexOutOfBoundsException: Range [29, 28) out of bounds for length 151
using i_heap_is_wellformedCore_DOM.heap_is_wellformed_children_distinct apply blast
using i_heap_is_wellformedCore_DOM.heap_is_wellformed_children_disc_nodes apply blast
using i_heap_is_wellformedCore_DOM.parent_child_rel_child apply (blast, blast)
using i_heap_is_wellformedCore_DOM.parent_child_rel_finite apply blast
using i_heap_is_wellformedCore_DOM.parent_child_rel_acyclic apply blast
using i_heap_is_wellformedCore_DOM.parent_child_rel_node_ptr apply blast
using i_heap_is_wellformedusing sum_butterfly_ket0 y(2) by blast
<sub>Core_DOM.parent_child_rel_child_in_heap apply blast
done
locale l_heap_is_wellformedSh1mtrc]Prj_kt_se_de)
l_heap_is_wellformedShadow_DOM_defs
java.lang.StringIndexOutOfBoundsException: Range [43, 38) out of bounds for length 89
get_shadow_rootsu>V U_S' S *\^>V (UA 0 ⊗o id_cblinfun) *V init_B_count =
+ CD: l_heap_is_wellformedCore_DOM
known_ptr type_wf get_child_nodes get_child_nodes_locs get_disconnected_nodes
get_disconnected_nodes_locs heap_is_wellformedCore_DOM parent_child_rel
+ l_heap_is_wellformed_defs
simpcfun_apyclnun_cmpse)
+ l_get_host next
java.lang.StringIndexOutOfBoundsException: Range [44, 38) out of bounds for length 69
java.lang.StringIndexOutOfBoundsException: Range [8, 4) out of bounds for length 146
do the same on \'mem››
java.lang.NullPointerException
java.lang.StringIndexOutOfBoundsException: Index 33 out of bounds for length 33
and get_child_nodes_locs :: "(_) object_ptr \<Rightarrow( (_) heap \Rightarrow> b> bool) set
java.lang.StringIndexOutOfBoundsException: Range [53, 3) out of bounds for length 129
java.lang.StringIndexOutOfBoundsException: Index 60 out of bounds for length 0
m
the have **: "\Psi>s>sB empty_list \bullet>l<Psi>sB l<bullet>>\sub>C \i et_it *
lement_ptr \Rightarrow ((_) heap, exception, char list) prog"
<>((_) heap ==> (_) heap ==> bool) set"
known_ptr :: "(_) object_ptr ==> bool"
java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0
java.lang.StringIndexOutOfBoundsException: Range [31, 29) out of bounds for length 59
java.lang.StringIndexOutOfBoundsException: Index 100 out of bounds for length 100
^Cr_O bool"
and get_host :: "(_) shadow_root_ptr ==> ((_) heap, exception, (_) element_ptr) prog"
and get_host_locs :: "((_) heap ==> (_) heap ==> bool) set"
and get_disconnected_document :: "(_) node_ptr ==> ((_) heap, exception, (_) document_ptr) prog"
and get_disconnected_document_locs :: "((_) heap ==> (_) heap ==> bool) set" +
assumes heap_is_wellformed_impl: "heap_is_wellformed = a_heap_is_wellformed"
begin
lemmas heap_is_wellformed_def =
heap_is_wellformed_impl[unfolded a_heap_is_wellformed_def,
folded CD.heap_is_wellformed_impl CD.parent_child_rel_impl]
lemma a_distinct_lists_code [code]:
"a_all_ptrs_in_heap h = ((∀host ∈ fset (element_ptr_kinds h).
h ⊨ ok (get_shadow_root host) ⟶ (case |h ⊨ get_shadow_root host|r of
Some shadow_root_ptr ==> shadow_root_ptr |∈| shadow_root_ptr_kinds h |
None ==> True)))"
apply(auto simp add: a_all_ptrs_in_heap_def split: option.splits)[1]
by (meson is_OK_returns_result_I local.get_shadow_root_ptr_in_heap select_result_I2)
lemma get_shadow_root_shadow_root_ptr_in_heap:
assumes "heap_is_wellformed h"
assumes "h ⊨ get_shadow_root host →r Some shadow_root_ptr"
shows "shadow_root_ptr |∈| shadow_root_ptr_kinds h"
using assms
by(auto simp add: heap_is_wellformed_def a_all_ptrs_in_heap_def)
lemma get_host_ptr_in_heap:
assumes "heap_is_wellformed h"
assumes "h ⊨ get_host shadow_root_ptr →r host"
shows "shadow_root_ptr |∈| shadow_root_ptr_kinds h"
using assms get_shadow_root_shadow_root_ptr_in_heap
by(auto simp add: get_host_def
elim!: bind_returns_result_E2
dest!: filter_M_holds_for_result
intro!: bind_pure_I
split: list.splits)
lemma shadow_root_same_host:
assumes "heap_is_wellformed h" and "type_wf h"
assumes "h ⊨ get_shadow_root host →r Some shadow_root_ptr"
assumes "h ⊨ get_shadow_root host' →r Some shadow_root_ptr"
shows "host = host'"
proof (rule ccontr)
assume " host ≠ host'"
have "host |∈| element_ptr_kinds h"
using assms(3)
by (meson is_OK_returns_result_I local.get_shadow_root_ptr_in_heap)
moreover
have "host' |∈| element_ptr_kinds h"
using assms(4)
by (meson is_OK_returns_result_I local.get_shadow_root_ptr_in_heap)
ultimately show False
using assms
apply(auto simp add: heap_is_wellformed_def a_distinct_lists_def)[1]
apply(drule distinct_concat_map_E(1)[where x=host and y=host'])
apply(simp)
apply(simp)
using ‹host ≠ host'› apply(simp)
apply(auto)[1]
done
qed
lemma shadow_root_host_dual:
assumes "h ⊨ get_host shadow_root_ptr →r host"
shows "h ⊨ get_shadow_root host →r Some shadow_root_ptr"
using assms
by(auto simp add: get_host_def
dest: filter_M_holds_for_result
elim!: bind_returns_result_E2
intro!: bind_pure_I split: list.splits)
lemma disc_doc_disc_node_dual:
assumes "h ⊨ get_disconnected_document disc_node →r disc_doc"
obtains disc_nodes where
"h ⊨ get_disconnected_nodes disc_doc →r disc_nodes" and
"disc_node ∈ set disc_nodes"
using assms get_disconnected_nodes_pure
by(auto simp add: get_disconnected_document_def bind_pure_I
dest!: filter_M_holds_for_result
elim!: bind_returns_result_E2
intro!: filter_M_pure_I
split: if_splits list.splits)
lemma get_host_valid_tag_name:
assumes "heap_is_wellformed h" and "type_wf h"
assumes "h ⊨ get_host shadow_root_ptr →r host"
assumes "h ⊨ get_tag_name host →r tag"
shows "tag ∈ safe_shadow_root_element_types"
proof -
obtain host' where
"host' |∈| element_ptr_kinds h" and
"|h ⊨ get_tag_name host'|r ∈ safe_shadow_root_element_types"
and "h ⊨ get_shadow_root host' →r Some shadow_root_ptr"
using assms
by (metis get_host_ptr_in_heap local.a_shadow_root_valid_def
local.get_shadow_root_ok local.heap_is_wellformed_def returns_result_select_result)
then have "host = host'"
by (meson assms(1) assms(2) assms(3) shadow_root_host_dual shadow_root_same_host)
then show ?thesis
using ‹|h ⊨ get_tag_name host'|r ∈ safe_shadow_root_element_types› assms(4) by auto
qed
lemma a_host_shadow_root_rel_finite: "finite (a_host_shadow_root_rel h)"
proof -
have "a_host_shadow_root_rel h = (∪host ∈ fset (element_ptr_kinds h).
(case |h ⊨ get_shadow_root host|r of
Some shadow_root ==> {(cast host, cast shadow_root)} | None ==> {}))"
by(auto simp add: a_host_shadow_root_rel_def split: option.splits)
moreover have "finite (∪host ∈ fset (element_ptr_kinds h).
(case |h ⊨ get_shadow_root host|r of
Some shadow_root ==> {(castelement_ptr2object_ptr host, castshadow_root_ptr2object_ptr shadow_root)} |
None ==> {}))"
by(auto split: option.splits)
ultimately show ?thesis
by auto
qed
lemma heap_is_wellformed_children_in_heap:
"heap_is_wellformed h ==> h ⊨ get_child_nodes ptr →r children ==> child ∈ set children ==>
child |∈| node_ptr_kinds h"
using CD.heap_is_wellformed_children_in_heap local.heap_is_wellformed_def by blast
lemma heap_is_wellformed_disc_nodes_in_heap:
"heap_is_wellformed h ==> h ⊨ get_disconnected_nodes document_ptr →r disc_nodes ==>
node ∈ set disc_nodes ==> node |∈| node_ptr_kinds h"
using CD.heap_is_wellformed_disc_nodes_in_heap local.heap_is_wellformed_def by blast
lemma heap_is_wellformed_one_parent:
"heap_is_wellformed h ==> h ⊨ get_child_nodes ptr →r children ==>
h ⊨ get_child_nodes ptr' →r children' ==> set children ∩ set children' ≠ {} ==> ptr = ptr'"
using CD.heap_is_wellformed_one_parent local.heap_is_wellformed_def by blast
lemma heap_is_wellformed_one_disc_parent:
"heap_is_wellformed h ==> h ⊨ get_disconnected_nodes document_ptr →r disc_nodes ==>
h ⊨ get_disconnected_nodes document_ptr' →r disc_nodes' ==> set disc_nodes ∩ set disc_nodes' ≠ {}
==> document_ptr = document_ptr'"
using CD.heap_is_wellformed_one_disc_parent local.heap_is_wellformed_def by blast
lemma heap_is_wellformed_children_disc_nodes_different:
"heap_is_wellformed h ==> h ⊨ get_child_nodes ptr →r children ==>
h ⊨ get_disconnected_nodes document_ptr →r disc_nodes ==> set children ∩ set disc_nodes = {}"
using CD.heap_is_wellformed_children_disc_nodes_different local.heap_is_wellformed_def by blast
lemma heap_is_wellformed_disconnected_nodes_distinct:
"heap_is_wellformed h ==> h ⊨ get_disconnected_nodes document_ptr →r disc_nodes ==>
distinct disc_nodes"
using CD.heap_is_wellformed_disconnected_nodes_distinct local.heap_is_wellformed_def by blast
lemma heap_is_wellformed_children_distinct:
"heap_is_wellformed h ==> h ⊨ get_child_nodes ptr →r children ==> distinct children"
using CD.heap_is_wellformed_children_distinct local.heap_is_wellformed_def by blast
lemma heap_is_wellformed_children_disc_nodes:
"heap_is_wellformed h ==> node_ptr |∈| node_ptr_kinds h ==>
¬(∃parent ∈ fset (object_ptr_kinds h). node_ptr ∈ set |h ⊨ get_child_nodes parent|r) ==>
(∃document_ptr ∈ fset (document_ptr_kinds h).
node_ptr ∈ set |h ⊨ get_disconnected_nodes document_ptr|r)"
using CD.heap_is_wellformed_children_disc_nodes local.heap_is_wellformed_def by blast
lemma parent_child_rel_finite: "heap_is_wellformed h ==> finite (parent_child_rel h)"
using CD.parent_child_rel_finite by blast
lemma parent_child_rel_acyclic: "heap_is_wellformed h ==> acyclic (parent_child_rel h)"
using CD.parent_child_rel_acyclic heap_is_wellformed_def by blast
lemma parent_child_rel_child_in_heap:
"heap_is_wellformed h ==> type_wf h ==> known_ptr parent ==>
(parent, child_ptr) ∈ parent_child_rel h ==> child_ptr |∈| object_ptr_kinds h"
using CD.parent_child_rel_child_in_heap local.heap_is_wellformed_def by blast
end
interpretation i_heap_is_wellformed?: l_heap_is_wellformedShadow_DOM get_child_nodes
get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs get_shadow_root
get_shadow_root_locs get_tag_name get_tag_name_locs known_ptr type_wf heap_is_wellformed
parent_child_rel heap_is_wellformedCore_DOM get_host get_host_locs get_disconnected_document
get_disconnected_document_locs
by(auto simp add: l_heap_is_wellformedShadow_DOM_def l_heap_is_wellformedShadow_DOM_axioms_def
l_heap_is_wellformedCore_DOM_def l_heap_is_wellformedCore_DOM_axioms_def
heap_is_wellformedCore_DOM_def parent_child_rel_def heap_is_wellformed_def
instances)
declare l_heap_is_wellformedShadow_DOM_axioms [instances]
lemma heap_is_wellformed_is_l_heap_is_wellformed [instances]:
"l_heap_is_wellformed ShadowRootClass.type_wf ShadowRootClass.known_ptr
Shadow_DOM.heap_is_wellformed Shadow_DOM.parent_child_rel Shadow_DOM.get_child_nodes
get_disconnected_nodes"
apply(auto simp add: l_heap_is_wellformed_def instances)[1]
using heap_is_wellformed_children_in_heap apply metis
using heap_is_wellformed_disc_nodes_in_heap apply metis
using heap_is_wellformed_one_parent apply blast
using heap_is_wellformed_one_disc_parent apply blast
using heap_is_wellformed_children_disc_nodes_different apply blast
using heap_is_wellformed_disconnected_nodes_distinct apply metis
using heap_is_wellformed_children_distinct apply metis
using heap_is_wellformed_children_disc_nodes apply metis
using i_heap_is_wellformedCore_DOM.parent_child_rel_child apply(blast, blast)
using i_heap_is_wellformedCore_DOM.parent_child_rel_finite apply blast
using parent_child_rel_acyclic apply blast
using i_heap_is_wellformedCore_DOM.parent_child_rel_node_ptr apply blast
using i_heap_is_wellformedCore_DOM.parent_child_rel_parent_in_heap apply blast
using parent_child_rel_child_in_heap apply metis
done
subsubsection ‹get\_parent›
interpretation i_get_parent_wfCore_DOM: l_get_parent_wfCore_DOM known_ptr type_wf get_child_nodes
get_child_nodes_locs known_ptrs get_parent get_parent_locs heap_is_wellformedCore_DOM
parent_child_rel get_disconnected_nodes
by(simp add: l_get_parent_wfCore_DOM_def instances)
declare i_get_parent_wfCore_DOM.l_get_parent_wfCore_DOM_axioms[instances]
interpretation i_get_parent_wf2Core_DOM: l_get_parent_wf2Core_DOM known_ptr type_wf get_child_nodes
get_child_nodes_locs known_ptrs get_parent get_parent_locs heap_is_wellformedCore_DOM
parent_child_rel get_disconnected_nodes get_disconnected_nodes_locs
by(auto simp add: l_get_parent_wf2Core_DOM_def instances)
declare i_get_parent_wf2Core_DOM.l_get_parent_wf2Core_DOM_axioms[instances]
lemma get_parent_wfCore_DOM_is_l_get_parent_wf [instances]: "l_get_parent_wf type_wf known_ptr
known_ptrs heap_is_wellformedCore_DOM parent_child_rel get_child_nodes get_parent"
apply(auto simp add: l_get_parent_wf_def l_get_parent_wf_axioms_def instances)[1]
using i_get_parent_wf2Core_DOM.child_parent_dual apply fast
using i_get_parent_wf2Core_DOM.heap_wellformed_induct apply metis
using i_get_parent_wf2Core_DOM.heap_wellformed_induct_rev apply metis
using i_get_parent_wf2Core_DOM.parent_child_rel_parent apply fast
done
subsubsection ‹get\_disconnected\_nodes›
subsubsection ‹set\_disconnected\_nodes›
paragraph ‹get\_disconnected\_nodes›
interpretation i_set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM:
l_set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM known_ptr type_wf
get_disconnected_nodes get_disconnected_nodes_locs set_disconnected_nodes
set_disconnected_nodes_locs heap_is_wellformedCore_DOM parent_child_rel get_child_nodes
by (simp add: l_set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM_def instances)
declare i_set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM.l_set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM_axioms[instances]
lemma set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM_is_l_set_disconnected_nodes_get_disconnected_nodes_wf [instances]:
"l_set_disconnected_nodes_get_disconnected_nodes_wf type_wf known_ptr heap_is_wellformedCore_DOM
parent_child_rel get_child_nodes get_disconnected_nodes get_disconnected_nodes_locs
set_disconnected_nodes set_disconnected_nodes_locs"
apply(auto simp add: l_set_disconnected_nodes_get_disconnected_nodes_wf_def
l_set_disconnected_nodes_get_disconnected_nodes_wf_axioms_def instances)[1]
using i_set_disconnected_nodes_get_disconnected_nodes_wfCore_DOM.remove_from_disconnected_nodes_removes
apply fast
done
paragraph ‹get\_root\_node›
interpretation i_get_root_node_wfCore_DOM:l_get_root_node_wfCore_DOM known_ptr type_wf known_ptrs
heap_is_wellformedCore_DOM parent_child_rel get_child_nodes get_child_nodes_locs get_disconnected_nodes
get_disconnected_nodes_locs get_parent get_parent_locs get_ancestors get_ancestors_locs
get_root_node get_root_node_locs
by(simp add: l_get_root_node_wfCore_DOM_def instances)
declare i_get_root_node_wfCore_DOM.l_get_root_node_wfCore_DOM_axioms[instances]
lemma get_ancestors_wfCore_DOM_is_l_get_ancestors_wf [instances]:
"l_get_ancestors_wf heap_is_wellformedCore_DOM parent_child_rel known_ptr known_ptrs type_wf
get_ancestors get_ancestors_locs get_child_nodes get_parent"
apply(auto simp add: l_get_ancestors_wf_def l_get_ancestors_wf_axioms_def instances)[1]
using i_get_root_node_wfCore_DOM.get_ancestors_never_empty apply blast
using i_get_root_node_wfCore_DOM.get_ancestors_ok apply blast
using i_get_root_node_wfCore_DOM.get_ancestors_reads apply blast
using i_get_root_node_wfCore_DOM.get_ancestors_ptrs_in_heap apply blast
using i_get_root_node_wfCore_DOM.get_ancestors_remains_not_in_ancestors apply blast
using i_get_root_node_wfCore_DOM.get_ancestors_also_parent apply blast
using i_get_root_node_wfCore_DOM.get_ancestors_obtains_children apply blast
using i_get_root_node_wfCore_DOM.get_ancestors_parent_child_rel apply blast
using i_get_root_node_wfCore_DOM.get_ancestors_parent_child_rel apply blast
done
lemma get_root_node_wfCore_DOM_is_l_get_root_node_wf [instances]:
"l_get_root_node_wf heap_is_wellformedCore_DOM get_root_node type_wf known_ptr known_ptrs
get_ancestors get_parent"
apply(auto simp add: l_get_root_node_wf_def l_get_root_node_wf_axioms_def instances)[1]
using i_get_root_node_wfCore_DOM.get_root_node_ok apply blast
using i_get_root_node_wfCore_DOM.get_root_node_ptr_in_heap apply blast
using i_get_root_node_wfCore_DOM.get_root_node_root_in_heap apply blast
using i_get_root_node_wfCore_DOM.get_ancestors_same_root_node apply(blast, blast)
using i_get_root_node_wfCore_DOM.get_root_node_same_no_parent apply blast
(* using i_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.get_root_node_not_node_same apply blast *)
using i_get_root_node_wfCore_DOM.get_root_node_parent_same apply (blast, blast)
done
subsubsection ‹to\_tree\_order›
interpretation i_to_tree_order_wfCore_DOM: l_to_tree_order_wfCore_DOM known_ptr type_wf get_child_nodes
get_child_nodes_locs to_tree_order known_ptrs get_parent get_parent_locs heap_is_wellformedCore_DOM
parent_child_rel get_disconnected_nodes get_disconnected_nodes_locs
apply(simp add: l_to_tree_order_wfCore_DOM_def instances)
done
declare i_to_tree_order_wfCore_DOM.l_to_tree_order_wfCore_DOM_axioms [instances]
lemma to_tree_order_wfCr_OM_is_l_to_tree_order_wf [instances]:
java.lang.StringIndexOutOfBoundsException: Range [26, 21) out of bounds for length 150
to_tree_order get_parent get_child_nodes"
apply(auto simp add: l_to_tree_order_wf_def l_to_tree_order_wf_axioms_def instances)[1]
using i_to_tree_order_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.to_tree_order_ok apply blast
using i_to_tree_order_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.to_tree_order_ptrs_in_heap apply blast
using i_to_tree_order_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.to_tree_order_parent_child_rel apply(blast, blast)
using i_to_tree_order_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.to_tree_order_child2 apply blast
using i_to_tree_order_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.to_tree_order_node_ptrs apply blast
using i_to_tree_order_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.to_tree_order_child apply blast
using i_to_tree_order_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.to_tree_order_ptr_in_result apply blast
using i_to_tree_order_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.to_tree_order_parent apply blast
using i_to_tree_order_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.to_tree_order_subset apply blast
done
paragraph \<open>get\_root\_node\<close>
interpretation i_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M: l_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
known_ptr type_wf known_ptrs heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M parent_child_rel get_child_nodes
get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs get_parent get_parent_locs
get_ancestors get_ancestors_locs get_root_node get_root_node_locs to_tree_order
by(auto simp add: l_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare i_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.l_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
lemma to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_is_l_to_tree_order_wf_get_root_node_wf [instances]:
"l_to_tree_order_wf_get_root_node_wf type_wf known_ptr known_ptrs to_tree_order get_root_node
heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M"
apply(auto simp add: l_to_tree_order_wf_get_root_node_wf_def
l_to_tree_order_wf_get_root_node_wf_axioms_def instances)[1]
using i_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.to_tree_order_get_root_node apply blast
using i_to_tree_order_wf_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.to_tree_order_same_root apply blast
done
subsubsection \<open>remove\_child\<close>
interpretation i_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M: l_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_child_nodes get_child_nodes_locs
set_child_nodes set_child_nodes_locs get_parent
get_parent_locs get_owner_document get_disconnected_nodes get_disconnected_nodes_locs
set_disconnected_nodes set_disconnected_nodes_locs remove_child remove_child_locs remove type_wf
known_ptr known_ptrs heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M parent_child_rel
by unfold_locales
declare i_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.l_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
lemma remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_is_l_remove_child_wf2 [instances]: "l_remove_child_wf2 type_wf known_ptr
known_ptrs remove_child heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_child_nodes remove"
apply(auto simp add: l_remove_child_wf2_def l_remove_child_wf2_axioms_def instances)[1]
using i_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.remove_child_heap_is_wellformed_preserved apply(fast, fast, fast)
using i_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.remove_heap_is_wellformed_preserved apply(fast, fast, fast)
using i_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.remove_child_removes_child apply fast
using i_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.remove_child_removes_first_child apply fast
using i_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.remove_removes_child apply fast
using i_remove_child_wf2\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M.remove_for_all_empty_children apply fast
done
subsection \<open>A wellformed heap\<close>
subsubsection \<open>get\_parent\<close>
interpretation i_get_parent_wf?: l_get_parent_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M known_ptr type_wf get_child_nodes
get_child_nodes_locs known_ptrs get_parent get_parent_locs heap_is_wellformed parent_child_rel
get_disconnected_nodes
using instances
by(simp add: l_get_parent_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def)
declare l_get_parent_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
lemma get_parent_wf_is_l_get_parent_wf [instances]:
"l_get_parent_wf ShadowRootClass.type_wf ShadowRootClass.known_ptr ShadowRootClass.known_ptrs
heap_is_wellformed parent_child_rel Shadow_DOM.get_child_nodes Shadow_DOM.get_parent"
apply(auto simp add: l_get_parent_wf_def l_get_parent_wf_axioms_def instances)[1]
using child_parent_dual apply blast
using heap_wellformed_induct apply metis
using heap_wellformed_induct_rev apply metis
using parent_child_rel_parent apply metis
done
subsubsection \<open>remove\_shadow\_root\<close>
locale l_remove_shadow_root_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
l_get_tag_name +
l_get_disconnected_nodes +
l_set_shadow_root_get_tag_name +
l_get_child_nodes +
l_heap_is_wellformed\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
l_remove_shadow_root\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
l_delete_shadow_root_get_disconnected_nodes +
l_delete_shadow_root_get_child_nodes +
l_set_shadow_root_get_disconnected_nodes +
l_set_shadow_root_get_child_nodes +
l_delete_shadow_root_get_tag_name +
l_set_shadow_root_get_shadow_root +
l_delete_shadow_root_get_shadow_root +
l_get_parent\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
begin
lemma remove_shadow_root_preserves:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h \<turnstile> remove_shadow_root ptr \<rightarrow>\<^sub>h h'"
shows "known_ptrs h'" and "type_wf h'" "heap_is_wellformed h'"
proof -
obtain shadow_root_ptr h2 where
"h \<turnstile> get_shadow_root ptr \<rightarrow>\<^sub>r Some shadow_root_ptr" and
"h \<turnstile> get_child_nodes (cast shadow_root_ptr) \<rightarrow>\<^sub>r []" and
h2: "h \<turnstile> set_shadow_root ptr None \<rightarrow>\<^sub>h h2" and
h': "h2 \<turnstile> delete_M shadow_root_ptr \<rightarrow>\<^sub>h h'"
using assms(4)
by(auto simp add: remove_shadow_root_def
elim!: bind_returns_heap_E bind_returns_heap_E2[rotated, OF get_shadow_root_pure, rotated]
bind_returns_heap_E2[rotated, OF get_child_nodes_pure, rotated]
split: option.splits if_splits)
have "type_wf h2"
using writes_small_big[where P="\<lambda>h h'. type_wf h \<longrightarrow> type_wf h'", OF set_shadow_root_writes h2]
using \<open>type_wf h\<close> set_shadow_root_types_preserved
by(auto simp add: reflp_def transp_def)
then show "type_wf h'"
using h' delete_shadow_root_type_wf_preserved local.type_wf_impl
by blast
have object_ptr_kinds_eq_h: "object_ptr_kinds h = object_ptr_kinds h2"
apply(rule writes_small_big[where P="\<lambda>h h'. object_ptr_kinds h = object_ptr_kinds h'",
OF set_shadow_root_writes h2])
using set_shadow_root_pointers_preserved
apply blast
by (auto simp add: reflp_def transp_def)
have node_ptr_kinds_eq_h: "node_ptr_kinds h = node_ptr_kinds h2"
using object_ptr_kinds_eq_h
by (simp add: node_ptr_kinds_def)
have element_ptr_kinds_eq_h: "element_ptr_kinds h = element_ptr_kinds h2"
using node_ptr_kinds_eq_h
by (simp add: element_ptr_kinds_def)
have document_ptr_kinds_eq_h: "document_ptr_kinds h = document_ptr_kinds h2"
using object_ptr_kinds_eq_h
by (simp add: document_ptr_kinds_def)
have shadow_root_ptr_kinds_eq_h: "shadow_root_ptr_kinds h = shadow_root_ptr_kinds h2"
using object_ptr_kinds_eq_h
by (simp add: shadow_root_ptr_kinds_def)
have "known_ptrs h2"
using \<open>known_ptrs h\<close> object_ptr_kinds_eq_h known_ptrs_subset
by blast
have object_ptr_kinds_eq_h2: "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h2"
using h' delete_shadow_root_pointers
by auto
have object_ptr_kinds_eq2_h2:
"object_ptr_kinds h2 = object_ptr_kinds h' |\<union>| {|cast shadow_root_ptr|}"
using h' delete_shadow_root_pointers
by auto
have node_ptr_kinds_eq_h2: "node_ptr_kinds h2 = node_ptr_kinds h'"
using object_ptr_kinds_eq_h2
by(auto simp add: node_ptr_kinds_def delete_shadow_root_pointers[OF h'])
have element_ptr_kinds_eq_h2: "element_ptr_kinds h2 = element_ptr_kinds h'"
using node_ptr_kinds_eq_h2
by (simp add: element_ptr_kinds_def)
have document_ptr_kinds_eq_h2: "document_ptr_kinds h2 = document_ptr_kinds h'"
using object_ptr_kinds_eq_h2
by(auto simp add: document_ptr_kinds_def delete_shadow_root_pointers[OF h'])
have shadow_root_ptr_kinds_eq_h2: "shadow_root_ptr_kinds h' |\<subseteq>| shadow_root_ptr_kinds h2"
using object_ptr_kinds_eq_h2
by (auto simp add: shadow_root_ptr_kinds_def)
have shadow_root_ptr_kinds_eq2_h2:
"shadow_root_ptr_kinds h2 = shadow_root_ptr_kinds h' |\<union>| {|shadow_root_ptr|}"
using object_ptr_kinds_eq2_h2
by (auto simp add: shadow_root_ptr_kinds_def)
show "known_ptrs h'"
using object_ptr_kinds_eq_h2 \<open>known_ptrs h2\<close> known_ptrs_subset
by blast
have disconnected_nodes_eq_h:
"\<And>doc_ptr disc_nodes. h \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes =
h2 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes"
using get_disconnected_nodes_reads set_shadow_root_writes h2 set_shadow_root_get_disconnected_nodes
by(rule reads_writes_preserved)
then have disconnected_nodes_eq2_h:
"\<And>doc_ptr. |h \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r = |h2 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r"
using select_result_eq by force
have disconnected_nodes_eq_h2:
"\<And>doc_ptr disc_nodes. h2 \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes =
h' \<turnstile> get_disconnected_nodes doc_ptr \<rightarrow>\<^sub>r disc_nodes"
using get_disconnected_nodes_reads get_disconnected_nodes_delete_shadow_root[OF h']
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
by blast+
then have disconnected_nodes_eq2_h2:
"\<And>doc_ptr. |h2 \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r = |h' \<turnstile> get_disconnected_nodes doc_ptr|\<^sub>r"
using select_result_eq by force
have tag_name_eq_h:
"\<And>doc_ptr disc_nodes. h \<turnstile> get_tag_name doc_ptr \<rightarrow>\<^sub>r disc_nodes =
h2 \<turnstile> get_tag_name doc_ptr \<rightarrow>\<^sub>r disc_nodes"
using get_tag_name_reads set_shadow_root_writes h2 set_shadow_root_get_tag_name
by(rule reads_writes_preserved)
then have tag_name_eq2_h: "\<And>doc_ptr. |h \<turnstile> get_tag_name doc_ptr|\<^sub>r = |h2 \<turnstile> get_tag_name doc_ptr|\<^sub>r"
using select_result_eq by force
have tag_name_eq_h2:
"\<And>doc_ptr disc_nodes. h2 \<turnstile> get_tag_name doc_ptr \<rightarrow>\<^sub>r disc_nodes =
h' \<turnstile> get_tag_name doc_ptr \<rightarrow>\<^sub>r disc_nodes"
using get_tag_name_reads get_tag_name_delete_shadow_root[OF h']
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
by blast+
then have tag_name_eq2_h2: "\<And>doc_ptr. |h2 \<turnstile> get_tag_name doc_ptr|\<^sub>r = |h' \<turnstile> get_tag_name doc_ptr|\<^sub>r"
using select_result_eq by force
have children_eq_h:
"\<And>ptr' children. h \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children = h2 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children"
using get_child_nodes_reads set_shadow_root_writes h2 set_shadow_root_get_child_nodes
by(rule reads_writes_preserved)
then have children_eq2_h: "\<And>ptr'. |h \<turnstile> get_child_nodes ptr'|\<^sub>r = |h2 \<turnstile> get_child_nodes ptr'|\<^sub>r"
using select_result_eq by force
have children_eq_h2:
"\<And>ptr' children. ptr' \<noteq> cast shadow_root_ptr \<Longrightarrow> h2 \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children =
h' \<turnstile> get_child_nodes ptr' \<rightarrow>\<^sub>r children"
using get_child_nodes_reads h' get_child_nodes_delete_shadow_root
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
by blast+
then have children_eq2_h2:
"\<And>ptr'. ptr' \<noteq> cast shadow_root_ptr \<Longrightarrow> |h2 \<turnstile> get_child_nodes ptr'|\<^sub>r =
|h' \<turnstile> get_child_nodes ptr'|\<^sub>r"
using select_result_eq by force
have "cast shadow_root_ptr |\<notin>| object_ptr_kinds h'"
using h' delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_ptr_not_in_heap
by auto
have get_shadow_root_eq_h:
"\<And>shadow_root_opt ptr'. ptr \<noteq> ptr' \<Longrightarrow> h \<turnstile> get_shadow_root ptr' \<rightarrow>\<^sub>r shadow_root_opt =
h2 \<turnstile> get_shadow_root ptr' \<rightarrow>\<^sub>r shadow_root_opt"
using get_shadow_root_reads set_shadow_root_writes h2
apply(rule reads_writes_preserved)
using set_shadow_root_get_shadow_root_different_pointers
by fast
have get_shadow_root_eq_h2:
"\<And>shadow_root_opt ptr'. h2 \<turnstile> get_shadow_root ptr' \<rightarrow>\<^sub>r shadow_root_opt =
h' \<turnstile> get_shadow_root ptr' \<rightarrow>\<^sub>r shadow_root_opt"
using get_shadow_root_reads get_shadow_root_delete_shadow_root[OF h']
apply(auto simp add: reads_def reflp_def transp_def preserved_def)[1]
by blast+
then
have get_shadow_root_eq2_h2: "\<And>ptr'. |h2 \<turnstile> get_shadow_root ptr'|\<^sub>r =
|h' \<turnstile> get_shadow_root ptr'|\<^sub>r"
using select_result_eq by force
have "acyclic (parent_child_rel h)"
using \<open>heap_is_wellformed h\<close>
by (simp add: heap_is_wellformed_def CD.heap_is_wellformed_def CD.acyclic_heap_def)
moreover
have "parent_child_rel h = parent_child_rel h2"
by(auto simp add: CD.parent_child_rel_def object_ptr_kinds_eq_h children_eq2_h)
moreover
have "parent_child_rel h' \<subseteq> parent_child_rel h2"
using object_ptr_kinds_eq_h2
apply(auto simp add: CD.parent_child_rel_def)[1]
by (metis \<open>cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr |\<notin>| object_ptr_kinds h'\<close> children_eq2_h2)
ultimately
have "CD.a_acyclic_heap h'"
using acyclic_subset
by (auto simp add: heap_is_wellformed_def CD.heap_is_wellformed_def CD.acyclic_heap_def)
moreover
have "CD.a_all_ptrs_in_heap h"
using \<open>heap_is_wellformed h\<close>
by (simp add: heap_is_wellformed_def CD.heap_is_wellformed_def)
then have "CD.a_all_ptrs_in_heap h2"
by(auto simp add: children_eq2_h disconnected_nodes_eq2_h document_ptr_kinds_eq_h
CD.a_all_ptrs_in_heap_def object_ptr_kinds_eq_h node_ptr_kinds_def
children_eq_h disconnected_nodes_eq_h)
then have "CD.a_all_ptrs_in_heap h'"
using disconnected_nodes_eq2_h2 document_ptr_kinds_eq_h2
apply(auto simp add: CD.a_all_ptrs_in_heap_def node_ptr_kinds_eq_h2 children_eq_h2
object_ptr_kinds_eq_h2)[1]
by (metis (no_types, opaque_lifting) \<open>cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root_ptr |\<notin>| object_ptr_kinds h'\<close>
children_eq2_h2 fsubsetD in_mono object_ptr_kinds_eq_h2)
moreover
have "CD.a_distinct_lists h"
using \<open>heap_is_wellformed h\<close>
by (simp add: heap_is_wellformed_def CD.heap_is_wellformed_def)
then have "CD.a_distinct_lists h2"
by(auto simp add: CD.a_distinct_lists_def object_ptr_kinds_eq_h document_ptr_kinds_eq_h
children_eq2_h disconnected_nodes_eq2_h)
then have "CD.a_distinct_lists h'"
apply(auto simp add: CD.a_distinct_lists_def document_ptr_kinds_eq_h2
disconnected_nodes_eq2_h2)[1]
apply(auto simp add: intro!: distinct_concat_map_I)[1]
apply(case_tac "x = cast shadow_root_ptr")
using \<open>cast shadow_root_ptr |\<notin>| object_ptr_kinds h'\<close> apply simp
using children_eq_h2 concat_map_all_distinct[of "(\<lambda>ptr. |h2 \<turnstile> get_child_nodes ptr|\<^sub>r)"]
apply (metis (no_types, lifting) children_eq2_h2 finite_fset fset_mp
object_ptr_kinds_eq_h2 set_sorted_list_of_set)
apply(case_tac "x = cast shadow_root_ptr")
using \<open>cast shadow_root_ptr |\<notin>| object_ptr_kinds h'\<close> apply simp
apply(case_tac "y = cast shadow_root_ptr")
using \<open>cast shadow_root_ptr |\<notin>| object_ptr_kinds h'\<close> apply simp
using children_eq_h2 distinct_concat_map_E(1)[of "(\<lambda>ptr. |h2 \<turnstile> get_child_nodes ptr|\<^sub>r)"]
apply (metis (no_types, lifting) IntI \<open>known_ptrs h'\<close> \<open>type_wf h'\<close> children_eq2_h2 empty_iff
finite_fset is_OK_returns_result_I l_get_child_nodes.get_child_nodes_ptr_in_heap
local.get_child_nodes_ok local.known_ptrs_known_ptr local.l_get_child_nodes_axioms
returns_result_select_result sorted_list_of_set.set_sorted_key_list_of_set)
apply(case_tac "xa = cast shadow_root_ptr")
using \<open>cast shadow_root_ptr |\<notin>| object_ptr_kinds h'\<close> apply simp
by (metis (mono_tags, lifting) CD.distinct_lists_no_parent \<open>known_ptrs h'\<close>
\<open>local.CD.a_distinct_lists h2\<close> \<open>type_wf h'\<close> children_eq2_h2 children_eq_h2
disconnected_nodes_eq_h2 is_OK_returns_result_I l_get_child_nodes.get_child_nodes_ptr_in_heap
local.get_child_nodes_ok local.get_disconnected_nodes_ok local.known_ptrs_known_ptr
local.l_get_child_nodes_axioms returns_result_select_result)
moreover
have "CD.a_owner_document_valid h"
using \<open>heap_is_wellformed h\<close>
by (simp add: heap_is_wellformed_def CD.heap_is_wellformed_def)
then have "CD.a_owner_document_valid h2"
by(auto simp add: CD.a_owner_document_valid_def object_ptr_kinds_eq_h document_ptr_kinds_eq_h
node_ptr_kinds_eq_h children_eq2_h disconnected_nodes_eq2_h)
then have "CD.a_owner_document_valid h'"
apply(auto simp add: CD.a_owner_document_valid_def document_ptr_kinds_eq_h2 node_ptr_kinds_eq_h2
disconnected_nodes_eq2_h2)[1]
proof -
fix node_ptr
assume 0: "\<forall>node_ptr\<in>fset (node_ptr_kinds h').
(\<exists>document_ptr. document_ptr |\<in>| document_ptr_kinds h' \<and>
node_ptr \<in> set |h' \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r) \<or>
(\<exists>parent_ptr. parent_ptr |\<in>| object_ptr_kinds h2 \<and>
node_ptr \<in> set |h2 \<turnstile> get_child_nodes parent_ptr|\<^sub>r)"
and 1: "node_ptr |\<in>| node_ptr_kinds h'"
and 2: "\<forall>parent_ptr. parent_ptr |\<in>| object_ptr_kinds h' \<longrightarrow>
node_ptr \<notin> set |h' \<turnstile> get_child_nodes parent_ptr|\<^sub>r"
then have "\<forall>parent_ptr. parent_ptr |\<in>| object_ptr_kinds h2 \<longrightarrow>
node_ptr \<notin> set |h2 \<turnstile> get_child_nodes parent_ptr|\<^sub>r"
apply(auto)[1]
apply(case_tac "parent_ptr = cast shadow_root_ptr")
using \<open>h \<turnstile> get_child_nodes (cast shadow_root_ptr) \<rightarrow>\<^sub>r []\<close> children_eq_h
apply auto[1]
using children_eq2_h2 object_ptr_kinds_eq_h2 h' delete_shadow_root_pointers
by (metis fempty_iff finsert_iff funionE)
then show "\<exists>document_ptr. document_ptr |\<in>| document_ptr_kinds h' \<and>
node_ptr \<in> set |h' \<turnstile> get_disconnected_nodes document_ptr|\<^sub>r"
using 0 1
by auto
qed
ultimately have "heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M h'"
by(simp add: CD.heap_is_wellformed_def)
moreover
have "acyclic (parent_child_rel h \<union> a_host_shadow_root_rel h)"
using \<open>heap_is_wellformed h\<close>
by(simp add: heap_is_wellformed_def)
then
have "acyclic (parent_child_rel h2 \<union> a_host_shadow_root_rel h2)"
proof -
have "a_host_shadow_root_rel h2 \<subseteq> a_host_shadow_root_rel h"
apply(auto simp add: a_host_shadow_root_rel_def element_ptr_kinds_eq_h)[1]
apply(case_tac "aa = ptr")
apply(simp)
apply (metis (no_types, lifting) \<open>type_wf h2\<close> assms(2) h2 local.get_shadow_root_ok
local.type_wf_impl option.distinct(1) returns_result_eq
returns_result_select_result set_shadow_root_get_shadow_root)
using get_shadow_root_eq_h
by (metis (mono_tags, lifting) \<open>type_wf h2\<close> image_eqI is_OK_returns_result_E
local.get_shadow_root_ok mem_Collect_eq prod.simps(2) select_result_I2)
then show ?thesis
using \<open>parent_child_rel h = parent_child_rel h2\<close>
by (metis (no_types, opaque_lifting) \<open>acyclic (parent_child_rel h \<union> a_host_shadow_root_rel h)\<close>
acyclic_subset order_refl sup_mono)
qed
then
have "acyclic (parent_child_rel h' \<union> a_host_shadow_root_rel h')"
proof -
have "a_host_shadow_root_rel h' \<subseteq> a_host_shadow_root_rel h2"
by(auto simp add: a_host_shadow_root_rel_def element_ptr_kinds_eq_h2 get_shadow_root_eq2_h2)
then show ?thesis
using \<open>parent_child_rel h' \<subseteq> parent_child_rel h2\<close>
\<open>acyclic (parent_child_rel h2 \<union> a_host_shadow_root_rel h2)\<close>
using acyclic_subset sup_mono
by (metis (no_types, opaque_lifting))
qed
moreover
have "a_all_ptrs_in_heap h"
using \<open>heap_is_wellformed h\<close>
by(simp add: heap_is_wellformed_def)
then
have "a_all_ptrs_in_heap h2"
apply(auto simp add: a_all_ptrs_in_heap_def shadow_root_ptr_kinds_eq_h)[1]
apply(case_tac "host = ptr")
apply(simp)
apply (metis assms(2) h2 local.type_wf_impl option.distinct(1) returns_result_eq
set_shadow_root_get_shadow_root)
using get_shadow_root_eq_h
by fastforce
then
have "a_all_ptrs_in_heap h'"
apply(auto simp add: a_all_ptrs_in_heap_def get_shadow_root_eq_h2)[1]
apply(auto simp add: shadow_root_ptr_kinds_eq2_h2)[1]
by (metis (no_types, lifting) \<open>h \<turnstile> get_shadow_root ptr \<rightarrow>\<^sub>r Some shadow_root_ptr\<close> assms(1)
assms(2) get_shadow_root_eq_h get_shadow_root_eq_h2 h2 local.shadow_root_same_host
local.type_wf_impl option.distinct(1) select_result_I2 set_shadow_root_get_shadow_root)
moreover
have "a_distinct_lists h"
using \<open>heap_is_wellformed h\<close>
by(simp add: heap_is_wellformed_def)
then
have "a_distinct_lists h2"
apply(auto simp add: a_distinct_lists_def element_ptr_kinds_eq_h)[1]
apply(auto intro!: distinct_concat_map_I split: option.splits)[1]
apply(case_tac "x = ptr")
apply(simp)
apply (metis (no_types, opaque_lifting) assms(2) h2 is_OK_returns_result_I
l_set_shadow_root_get_shadow_root.set_shadow_root_get_shadow_root
l_set_shadow_root_get_shadow_root_axioms local.type_wf_impl option.discI
returns_result_eq returns_result_select_result)
apply(case_tac "y = ptr")
apply(simp)
apply (metis (no_types, opaque_lifting) assms(2) h2 is_OK_returns_result_I
l_set_shadow_root_get_shadow_root.set_shadow_root_get_shadow_root
l_set_shadow_root_get_shadow_root_axioms local.type_wf_impl option.discI
returns_result_eq returns_result_select_result)
by (metis \<open>type_wf h2\<close> assms(1) assms(2) get_shadow_root_eq_h local.get_shadow_root_ok
local.shadow_root_same_host returns_result_select_result)
then
have "a_distinct_lists h'"
by(auto simp add: a_distinct_lists_def element_ptr_kinds_eq_h2 get_shadow_root_eq2_h2)
moreover
have "a_shadow_root_valid h"
using \<open>heap_is_wellformed h\<close>
by(simp add: heap_is_wellformed_def)
then
have "a_shadow_root_valid h'"
by (smt (verit) \<open>h \<turnstile> get_shadow_root ptr \<rightarrow>\<^sub>r Some shadow_root_ptr\<close> assms(2)
delete\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>R\<^sub>o\<^sub>o\<^sub>t_M_ptr_not_in_heap element_ptr_kinds_eq_h element_ptr_kinds_eq_h2
finsert_iff funion_finsert_right get_shadow_root_eq2_h2 get_shadow_root_eq_h h'
local.a_shadow_root_valid_def local.get_shadow_root_ok object_ptr_kinds_eq2_h2
object_ptr_kinds_eq_h option.sel returns_result_select_result select_result_I2
shadow_root_ptr_kinds_commutes sup_bot.right_neutral tag_name_eq2_h tag_name_eq2_h2)
ultimately show "heap_is_wellformed h'"
by(simp add: heap_is_wellformed_def)
qed
end
interpretation i_remove_shadow_root_wf?: l_remove_shadow_root_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
type_wf get_tag_name get_tag_name_locs get_disconnected_nodes get_disconnected_nodes_locs
set_shadow_root set_shadow_root_locs known_ptr get_child_nodes get_child_nodes_locs get_shadow_root
get_shadow_root_locs heap_is_wellformed parent_child_rel heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_host
get_host_locs get_disconnected_document get_disconnected_document_locs remove_shadow_root
remove_shadow_root_locs known_ptrs get_parent get_parent_locs
by(auto simp add: l_remove_shadow_root_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_remove_shadow_root_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
subsubsection \<open>get\_root\_node\<close>
interpretation i_get_root_node_wf?: l_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M known_ptr type_wf known_ptrs
heap_is_wellformed parent_child_rel get_child_nodes get_child_nodes_locs get_disconnected_nodes
get_disconnected_nodes_locs get_parent get_parent_locs get_ancestors get_ancestors_locs
get_root_node get_root_node_locs
by(simp add: l_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_get_root_node_wf\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms[instances]
lemma get_ancestors_wf_is_l_get_ancestors_wf [instances]:
"l_get_ancestors_wf heap_is_wellformed parent_child_rel known_ptr known_ptrs type_wf get_ancestors
get_ancestors_locs get_child_nodes get_parent"
apply(auto simp add: l_get_ancestors_wf_def l_get_ancestors_wf_axioms_def instances)[1]
using get_ancestors_never_empty apply blast
ok
using get_ancestors_reads apply blast
estors_ptrs_in_heap
using get_ancestors_remains_not_in_ancestorst
using get_ancestors_also_parent apply blast
usings_obtains_children
usingarent_child_relblast
lemma get_root_node_wf_is_l_get_root_node_wf [instances]:
ot_node_wfype_wfown_ptrn_ptrsancestorsjava.lang.StringIndexOutOfBoundsException: Index 97 out of bounds for length 97
autol_get_root_node_wf_axioms_def
using get_root_node_ok applysimps2))
using
using get_ancestors_same_root_node>uot_dbfm A\<rbrakk>e = \<lbrakkt_dbfm>e'"
using get_root_node_parent_same apply (blast, blast)
done
subsubsection HPair (HTuple )
locale
mpminus_1
f
l_get_shadow_root +
get_host
begin
lemma host_shadow_root_rel_finite: "finite (a_host_shadow_root_rel definition vquot_fm : <> Rightarrow tm"
have "a_host_shadow_root_rel h = (\<Union>host \<in> fset (element_ptr_kinds h).
(case |h \<turnstile> get_shadow_root host|\<^sub>r of
Some shadow_root \<Rightarrow> {(cast host, cast shadow_root)} | None \<Rightarrow> {}))"
by(auto simp add: a_host_shadow_root_rel_def split: option.splits)
moreover have "finite (\<Union>host \<in> fset (element_ptr_kinds h).
(case |h \<turnstile> get_shadow_root host|\<^sub>r of
Some shadow_root \<Rightarrow> {(cast\<^sub>e\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r host, cast\<^sub>s\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>r\<^sub>o\<^sub>o\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r shadow_root)} |
None \<Rightarrow> {}))"
by(auto split: option.splits)
ultimately show ?thesis
by auto
qed
lemma host_shadow_root_rel_shadow_root:
"h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r shadow_root_option \<Longrightarrow>
shadow_root_option = Some shadow_root \<longleftrightarrow> ((cast host, cast shadow_root) \<in> a_host_shadow_root_rel h)"
apply(auto simp add: a_host_shadow_root_rel_def)[1]
by(metis (mono_tags, lifting) case_prodI is_OK_returns_result_I
l_get_shadow_root.get_shadow_root_ptr_in_heap local.l_get_shadow_root_axioms
mem_Collect_eq pair_imageI select_result_I2)
lemma host_shadow_root_rel_host:
"heap_is_wellformed h \<Longrightarrow> h \<turnstile> get_host shadow_root \<rightarrow>\<^sub>r host \<Longrightarrow>
(cast host, cast shadow_root) \<in> a_host_shadow_root_rel h"
apply(auto simp add: a_host_shadow_root_rel_def)[1]
using shadow_root_host_dual
by (metis (no_types, lifting) Collect_cong host_shadow_root_rel_shadow_root
local.a_host_shadow_root_rel_def split_cong)
lemma heap_wellformed_induct_si [consumes 1, case_names step]:
assumes "heap_is_wellformed h"
assumes "\<And>parent. (\<And>children child. h \<turnstile> get_child_nodes parent \<rightarrow>\<^sub>r children \<Longrightarrow>
child \<in> set children \<Longrightarrow> P (cast child)) \<Longrightarrow> (\<And>shadow_root host. parent = cast host \<Longrightarrow>
h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root \<Longrightarrow> P (cast shadow_root)) \<Longrightarrow> P parent"
shows "P ptr"
proof -
fix ptr
have "finite (parent_child_rel h \<union> a_host_shadow_root_rel h)"
using host_shadow_root_rel_finite
using local.CD.parent_child_rel_finite local.CD.parent_child_rel_impl
by auto
then
have "wf ((parent_child_rel h \<union> a_host_shadow_root_rel h)\<inverse>)"
using assms(1)
apply(simp add: heap_is_wellformed_def)
by (simp add: finite_acyclic_wf_converse local.CD.parent_child_rel_impl)
then show "?thesis"
proof (induct rule: wf_induct_rule)
case (less parent)
then show ?case
apply(auto)[1]
using assms host_shadow_root_rel_shadow_root local.CD.parent_child_rel_child
by blast
qed
qed
lemma heap_wellformed_induct_rev_si [consumes 1, case_names step]:
assumes "heap_is_wellformed h"
assumes "\<And>child. (\<And>parent child_node. child = cast child_node \<Longrightarrow>
h \<turnstile> get_parent child_node \<rightarrow>\<^sub>r Some parent \<Longrightarrow> P parent) \<Longrightarrow>
(\<And>host shadow_root. child = cast shadow_root \<Longrightarrow> h \<turnstile> get_host shadow_root \<rightarrow>\<^sub>r host \<Longrightarrow>
P (cast host)) \<Longrightarrow> P child"
shows "P ptr"
proof -
fix ptr
have "finite (parent_child_rel h \<union> a_host_shadow_root_rel h)"
using host_shadow_root_rel_finite
using local.CD.parent_child_rel_finite local.CD.parent_child_rel_impl
by auto
then
have "wf (parent_child_rel h \<union> a_host_shadow_root_rel h)"
using assms(1)
apply(simp add: heap_is_wellformed_def)
by (simp add: finite_acyclic_wf)
then show "?thesis"
proof (induct rule: wf_induct_rule)
case (less parent)
then show ?case
apply(auto)[1]
using parent_child_rel_parent host_shadow_root_rel_host
using assms(1) assms(2) by auto
qed
qed
end
interpretation i_get_parent_get_host_wf?: l_get_parent_get_host_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M
get_child_nodes get_child_nodes_locs get_disconnected_nodes get_disconnected_nodes_locs
get_shadow_root get_shadow_root_locs get_tag_name get_tag_name_locs known_ptr type_wf
heap_is_wellformed parent_child_rel heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_host get_host_locs
get_disconnected_document get_disconnected_document_locs known_ptrs get_parent get_parent_locs
by(auto simp add: l_get_parent_get_host_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_get_parent_get_host_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
locale l_get_parent_get_host_wf =
l_heap_is_wellformed_defs +
l_get_parent_defs +
l_get_shadow_root_defs +
l_get_host_defs +
l_get_child_nodes_defs +
assumes heap_wellformed_induct_si [consumes 1, case_names step]:
"heap_is_wellformed h
\<Longrightarrow> (\<And>parent. (\<And>children child. h \<turnstile> get_child_nodes parent \<rightarrow>\<^sub>r children \<Longrightarrow> child \<in> set children
\<Longrightarrow> P (cast child))
\<Longrightarrow> (\<And>shadow_root host. parent = cast host \<Longrightarrow> h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root
\<Longrightarrow> P (cast shadow_root))
\<Longrightarrow> P parent)
\<Longrightarrow> P ptr"
assumes heap_wellformed_induct_rev_si [consumes 1, case_names step]:
"heap_is_wellformed h
\<Longrightarrow> (\<And>child. (\<And>parent child_node. child = cast child_node \<Longrightarrow>
h \<turnstile> get_parent child_node \<rightarrow>\<^sub>r Some parent \<Longrightarrow> P parent)
\<Longrightarrow> (\<And>host shadow_root. child = cast shadow_root \<Longrightarrow> h \<turnstile> get_host shadow_root \<rightarrow>\<^sub>r host
\<Longrightarrow> P (cast host))
\<Longrightarrow> P child)
\<Longrightarrow> P ptr"
lemma l_get_parent_get_host_wf_is_get_parent_get_host_wf [instances]:
"l_get_parent_get_host_wf heap_is_wellformed get_parent get_shadow_root get_host get_child_nodes"
apply(auto simp add: l_get_parent_get_host_wf_def instances)[1]
using heap_wellformed_induct_si apply metis
using heap_wellformed_induct_rev_si apply blast
done
subsubsection \<open>get\_host\<close>
locale l_get_host_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
l_heap_is_wellformed\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_child_nodes get_child_nodes_locs get_disconnected_nodes
get_disconnected_nodes_locs get_shadow_root get_shadow_root_locs get_tag_name get_tag_name_locs
known_ptr type_wf heap_is_wellformed parent_child_rel heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_host
get_host_locs +
l_type_wf type_wf +
l_get_host\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_shadow_root get_shadow_root_locs get_host get_host_locs type_wf +
l_get_shadow_root type_wf get_shadow_root get_shadow_root_locs
for known_ptr :: "(_::linorder) object_ptr \<Rightarrow> bool"
and known_ptrs :: "(_) heap \<Rightarrow> bool"
and type_wf :: "(_) heap \<Rightarrow> bool"
and get_host :: "(_) shadow_root_ptr \<Rightarrow> ((_) heap, exception, (_) element_ptr) prog"
and get_host_locs :: "((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and get_shadow_root :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, (_) shadow_root_ptr option) prog"
and get_shadow_root_locs :: "(_) element_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and get_child_nodes :: "(_::linorder) object_ptr \<Rightarrow> ((_) heap, exception, (_) node_ptr list) prog"
and get_child_nodes_locs :: "(_) object_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and get_disconnected_nodes :: "(_) document_ptr \<Rightarrow> ((_) heap, exception, (_) node_ptr list) prog"
and get_disconnected_nodes_locs :: "(_) document_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and get_tag_name :: "(_) element_ptr \<Rightarrow> ((_) heap, exception, char list) prog"
and get_tag_name_locs :: "(_) element_ptr \<Rightarrow> ((_) heap \<Rightarrow> (_) heap \<Rightarrow> bool) set"
and heap_is_wellformed :: "(_) heap \<Rightarrow> bool"
and parent_child_rel :: "(_) heap \<Rightarrow> ((_) object_ptr \<times> (_) object_ptr) set"
and heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M :: "(_) heap \<Rightarrow> bool"
begin
lemma get_host_ok [simp]:
assumes "heap_is_wellformed h"
assumes "type_wf h"
assumes "known_ptrs h"
assumes "shadow_root_ptr |\<in>| shadow_root_ptr_kinds h"
shows "h \<turnstile> ok (get_host shadow_root_ptr)"
proof -
obtain host where host: "host |\<in>| element_ptr_kinds h"
and "|h \<turnstile> get_tag_name host|\<^sub>r \<in> safe_shadow_root_element_types"
and shadow_root: "h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some shadow_root_ptr"
using assms(1) assms(4) get_shadow_root_ok assms(2)
apply(auto simp add: heap_is_wellformed_def a_shadow_root_valid_def)[1]
by (smt returns_result_select_result)
obtain host_candidates where
host_candidates: "h \<turnstile> filter_M (\<lambda>element_ptr. Heap_Error_Monad.bind (get_shadow_root element_ptr)
(\<lambda>shadow_root_opt. return (shadow_root_opt = Some shadow_root_ptr)))
(sorted_list_of_set (fset (element_ptr_kinds h)))
\<rightarrow>\<^sub>r host_candidates"
apply(drule is_OK_returns_result_E[rotated])
using get_shadow_root_ok assms(2)
by(auto intro!: filter_M_is_OK_I bind_pure_I bind_is_OK_I2)
then have "host_candidates = [host]"
apply(rule filter_M_ex1)
apply (simp add: host)
apply (smt (verit) assms(1) assms(2) bind_pure_returns_result_I2 finite_fset
host local.get_shadow_root_ok local.get_shadow_root_pure local.shadow_root_same_host
return_returns_result returns_result_eq shadow_root sorted_list_of_set(1))
by (simp_all add: assms(2) bind_pure_I bind_pure_returns_result_I2 host local.get_shadow_root_ok
returns_result_eq shadow_root)
then
show ?thesis
using host_candidates host assms(1) get_shadow_root_ok
apply(auto simp add: get_host_def known_ptrs_known_ptr
intro!: bind_is_OK_pure_I filter_M_pure_I filter_M_is_OK_I bind_pure_I split: list.splits)[1]
using assms(2) apply blast
apply (meson list.distinct(1) returns_result_eq)
by (meson list.distinct(1) list.inject returns_result_eq)
qed
end
interpretation i_get_host_wf?: l_get_host_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M get_disconnected_document
get_disconnected_document_locs known_ptr known_ptrs type_wf get_host get_host_locs get_shadow_root
get_shadow_root_locs get_child_nodes get_child_nodes_locs get_disconnected_nodes
get_disconnected_nodes_locs get_tag_name get_tag_name_locs heap_is_wellformed parent_child_rel
heap_is_wellformed\<^sub>C\<^sub>o\<^sub>r\<^sub>e\<^sub>_\<^sub>D\<^sub>O\<^sub>M
by(auto simp add: l_get_host_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_def instances)
declare l_get_host_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms [instances]
locale l_get_host_wf = l_heap_is_wellformed_defs + l_known_ptrs + l_type_wf + l_get_host_defs +
assumes get_host_ok:
"heap_is_wellformed h \<Longrightarrow> known_ptrs h \<Longrightarrow> type_wf h \<Longrightarrow>
shadow_root_ptr |\<in>| shadow_root_ptr_kinds h \<Longrightarrow> h \<turnstile> ok (get_host shadow_root_ptr)"
lemma get_host_wf_is_l_get_host_wf [instances]:
"l_get_host_wf heap_is_wellformed known_ptr known_ptrs type_wf get_host"
by(auto simp add: l_get_host_wf_def l_get_host_wf_axioms_def instances)
subsubsection \<open>get\_root\_node\_si\<close>
locale l_get_root_node_si_wf\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M =
l_get_root_node_si\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
l_heap_is_wellformed\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M +
l_get_parent_wf +
l_get_parent_get_host_wf +
l_get_host_wf
begin
lemma get_root_node_si_ptr_in_heap:
assumes "h \<turnstile> ok (get_root_node_si ptr)"
shows "ptr |\<in>| object_ptr_kinds h"
using assms
unfolding get_root_node_si_def
using get_ancestors_si_ptr_in_heap
by auto
lemma get_ancestors_si_ok:
assumes "heap_is_wellformed h" and "known_ptrs h" and "type_wf h"
and "ptr |\<in>| object_ptr_kinds h"
shows "h \<turnstile> ok (get_ancestors_si ptr)"
proof (insert assms(1) assms(4), induct rule: heap_wellformed_induct_rev_si)
case (step child)
then show ?case
using assms(2) assms(3)
apply(auto simp add: get_ancestors_si_def[of child] assms(1) get_parent_parent_in_heap
intro!: bind_is_OK_pure_I
split: option.splits)[1]
using local.get_parent_ok apply blast
using get_host_ok assms(1) apply blast
by (meson assms(1) is_OK_returns_result_I local.get_shadow_root_ptr_in_heap
local.shadow_root_host_dual)
qed
lemma get_ancestors_si_remains_not_in_ancestors:
assumes "heap_is_wellformed h"
and "heap_is_wellformed h'"
and "h \<turnstile> get_ancestors_si ptr \<rightarrow>\<^sub>r ancestors"
and "h' \<turnstile> get_ancestors_si ptr \<rightarrow>\<^sub>r ancestors'"
and "\<And>p children children'. h \<turnstile> get_child_nodes p \<rightarrow>\<^sub>r children
\<Longrightarrow> h' \<turnstile> get_child_nodes p \<rightarrow>\<^sub>r children' \<Longrightarrow> set children' \<subseteq> set children"
and "\<And>p shadow_root_option shadow_root_option'. h \<turnstile> get_shadow_root p \<rightarrow>\<^sub>r shadow_root_option \<Longrightarrow>
h' \<turnstile> get_shadow_root p \<rightarrow>\<^sub>r shadow_root_option' \<Longrightarrow> (if shadow_root_option = None
then shadow_root_option' = None else shadow_root_option' = None \<or>
shadow_root_option' = shadow_root_option)"
and "node \<notin> set ancestors"
and object_ptr_kinds_eq3: "object_ptr_kinds h = object_ptr_kinds h'"
and known_ptrs: "known_ptrs h"
and type_wf: "type_wf h"
and type_wf': "type_wf h'"
shows "node \<notin> set ancestors'"
proof -
have object_ptr_kinds_M_eq:
"\<And>ptrs. h \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs = h' \<turnstile> object_ptr_kinds_M \<rightarrow>\<^sub>r ptrs"
using object_ptr_kinds_eq3
by(simp add: object_ptr_kinds_M_defs)
then have object_ptr_kinds_eq: "|h \<turnstile> object_ptr_kinds_M|\<^sub>r = |h' \<turnstile> object_ptr_kinds_M|\<^sub>r"
by(simp)
show ?thesis
proof (insert assms(1) assms(3) assms(4) assms(7), induct ptr arbitrary: ancestors ancestors'
rule: heap_wellformed_induct_rev_si)
case (step child)
obtain ancestors_remains where ancestors_remains:
"ancestors = child # ancestors_remains"
using \<open>h \<turnstile> get_ancestors_si child \<rightarrow>\<^sub>r ancestors\<close> get_ancestors_si_never_empty
by(auto simp add: get_ancestors_si_def[of child]
elim!: bind_returns_result_E2
split: option.splits)
obtain ancestors_remains' where ancestors_remains':
"ancestors' = child # ancestors_remains'"
using \<open>h' \<turnstile> get_ancestors_si child \<rightarrow>\<^sub>r ancestors'\<close> get_ancestors_si_never_empty
by(auto simp add: get_ancestors_si_def[of child]
elim!: bind_returns_result_E2
split: option.splits)
have "child |\<in>| object_ptr_kinds h"
using local.get_ancestors_si_ptr_in_heap object_ptr_kinds_eq3 step.prems(2) by fastforce
have "node \<noteq> child"
using ancestors_remains step.prems(3) by auto
have 1: "\<And>p parent. h' \<turnstile> get_parent p \<rightarrow>\<^sub>r Some parent \<Longrightarrow> h \<turnstile> get_parent p \<rightarrow>\<^sub>r Some parent"
proof -
fix p parent
assume "h' \<turnstile> get_parent p \<rightarrow>\<^sub>r Some parent"
then obtain children' where
children': "h' \<turnstile> get_child_nodes parent \<rightarrow>\<^sub>r children'" and
p_in_children': "p \<in> set children'"
using get_parent_child_dual by blast
obtain children where children: "h \<turnstile> get_child_nodes parent \<rightarrow>\<^sub>r children"
using get_child_nodes_ok assms(1) get_child_nodes_ptr_in_heap object_ptr_kinds_eq children'
known_ptrs
using type_wf type_wf'
by (metis \<open>h' \<turnstile> get_parent p \<rightarrow>\<^sub>r Some parent\<close> get_parent_parent_in_heap is_OK_returns_result_E
local.known_ptrs_known_ptr object_ptr_kinds_eq3)
have "p \<in> set children"
using assms(5) children children' p_in_children'
by blast
then show "h \<turnstile> get_parent p \<rightarrow>\<^sub>r Some parent"
using child_parent_dual assms(1) children known_ptrs type_wf by blast
qed
have 2: "\<And>p host. h' \<turnstile> get_host p \<rightarrow>\<^sub>r host \<Longrightarrow> h \<turnstile> get_host p \<rightarrow>\<^sub>r host"
proof -
fix p host
assume "h' \<turnstile> get_host p \<rightarrow>\<^sub>r host"
then have "h' \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some p"
using local.shadow_root_host_dual by blast
then have "h \<turnstile> get_shadow_root host \<rightarrow>\<^sub>r Some p"
by (metis assms(6) element_ptr_kinds_commutes is_OK_returns_result_I local.get_shadow_root_ok
local.get_shadow_root_ptr_in_heap node_ptr_kinds_commutes object_ptr_kinds_eq3
option.distinct(1) returns_result_select_result type_wf)
then show "h \<turnstile> get_host p \<rightarrow>\<^sub>r host"
by (metis assms(1) is_OK_returns_result_E known_ptrs local.get_host_ok
local.get_shadow_root_shadow_root_ptr_in_heap local.shadow_root_host_dual
local.shadow_root_same_host type_wf)
qed
show ?case
proof (cases "cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r child")
case None
then show ?thesis
using step(3) step(4) \<open>node \<noteq> child\<close>
apply(auto simp add: get_ancestors_si_def[of child]
elim!: bind_returns_result_E2
split: option.splits)[1]
by (metis "2" assms(1) l_heap_is_wellformed\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M.shadow_root_same_host list.set_intros(2)
local.l_heap_is_wellformed\<^sub>S\<^sub>h\<^sub>a\<^sub>d\<^sub>o\<^sub>w\<^sub>_\<^sub>D\<^sub>O\<^sub>M_axioms local.shadow_root_host_dual step.hyps(2)
step.prems(3) type_wf)
next
case (Some node_child)
then
show ?thesis
using step(3) step(4) \<open>node \<noteq> child\<close>
apply(auto simp add: get_ancestors_si_def[of child]
elim!: bind_returns_result_E2
split: option.splits)[1]
apply (meson "1" option.distinct(1) returns_result_eq)
by (metis "1" list.set_intros(2) option.inject returns_result_eq step.hyps(1) step.prems(3))
qed
qed
qed
lemma get_ancestors_si_ptrs_in_heap:
assumes "heap_is_wellformed h" and "type_wf h" and "known_ptrs h"
assumes "h \<turnstile> get_ancestors_si ptr \<rightarrow>\<^sub>r ancestors"
assumes "ptr' \<in> set ancestors"
shows "ptr' |\<in>| object_ptr_kinds h"
proof (insert assms(4) assms(5), induct ancestors arbitrary: ptr)
case Nil
then show ?case
by(auto)
next
case (Cons a ancestors)
then obtain x where x: "h \<turnstile> get_ancestors_si x \<rightarrow>\<^sub>r a # ancestors"
by(auto simp add: get_ancestors_si_def[of a] elim!: bind_returns_result_E2 split: option.splits)
then have "x = a"
by(auto simp add: get_ancestors_si_def[of x] elim!: bind_returns_result_E2 split: option.splits)
then show ?case
proof (cases "ptr' = a")
case True
then show ?thesis
using Cons.hyps Cons.prems(2) get_ancestors_si_ptr_in_heap x
using \<open>x = a\<close> by blast
next
case False
obtain ptr'' where ptr'': "h \<turnstile> get_ancestors_si ptr'' \<rightarrow>\<^sub>r ancestors"
using \<open> h \<turnstile> get_ancestors_si x \<rightarrow>\<^sub>r a # ancestors\<close> Cons.prems(2) False
by(auto simp add: get_ancestors_si_def[of x] elim!: bind_returns_result_E2 split: option.splits)
then show ?thesis
using Cons.hyps Cons.prems(2) False by auto
qed
qed
lemma get_ancestors_si_reads:
assumes "heap_is_wellformed h"
shows "reads get_ancestors_si_locs (get_ancestors_si node_ptr) h h'"
proof (insert assms(1), induct rule: heap_wellformed_induct_rev_si)
case (step child)
then show ?case
using [[simproc del: Product_Type.unit_eq]] get_parent_reads[unfolded reads_def]
get_host_reads[unfolded reads_def]
apply(simp (no_asm) add: get_ancestors_si_def)
by(auto simp add: get_ancestors_si_locs_def get_parent_reads_pointers
intro!: reads_bind_pure reads_subset[OF check_in_heap_reads]
reads_subset[OF return_reads] reads_subset[OF get_parent_reads]
reads_subset[OF get_child_nodes_reads] reads_subset[OF get_host_reads]
split: option.splits)
qed
lemma get_ancestors_si_subset:
assumes "heap_is_wellformed h"
and "h \<turnstile> get_ancestors_si ptr \<rightarrow>\<^sub>r ancestors"
and "ancestor \<in> set ancestors"
and "h \<turnstile> get_ancestors_si ancestor \<rightarrow>\<^sub>r ancestor_ancestors"
and type_wf: "type_wf h"
and known_ptrs: "known_ptrs h"
shows "set ancestor_ancestors \<subseteq> set ancestors"
proof (insert assms(1) assms(2) assms(3), induct ptr arbitrary: ancestors
rule: heap_wellformed_induct_rev_si)
case (step child)
have "child |\<in>| object_ptr_kinds h"
using get_ancestors_si_ptr_in_heap step(3) by auto
(* then have "h \<turnstile> check_in_heap child \<rightarrow>\<^sub>r ()"
using returns_result_select_result by force *)
obtain
[ indep_in
elim!s_inI_aux
java.lang.StringIndexOutOfBoundsException: Index 12 out of bounds for length 12
nductoj<e<tprnd_tjava.lang.NullPointerException
java.lang.StringIndexOutOfBoundsException: Index 13 out of bounds for length 13
show ?case
basis_in_def
thenn ∈ card E"
using step(3) ‹None = cast | | |