\documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]
{scrreprt}
\usepackage[T1]{fontenc}
\usepackage[USenglish]{babel}
\usepackage[numbers, sort&compress]{natbib}
\usepackage{isabelle,isabellesym}
\usepackage{booktabs}
\usepackage{paralist}
\usepackage{graphicx}
\usepackage{amssymb}
\usepackage{xspace}
\usepackage{xcolor}
\usepackage{listings}
\lstloadlanguages{HTML}
\usepackage[]{mathtools}
\usepackage[pdfpagelabels, pageanchor=false, plainpages=false]{hyperref}
\lstdefinestyle{html}{language=XML,
  basicstyle=\ttfamily,
  commentstyle=\itshape,
  keywordstyle=\color{blue},
  ndkeywordstyle=\color{blue},
}
\lstdefinestyle{displayhtml}{style=html,
  floatplacement={tbp},
  captionpos=b,
  framexleftmargin=0pt,
  basicstyle=\ttfamily\scriptsize,
  backgroundcolor=\color{black!2},
  frame=lines,
}
\lstnewenvironment{html}[1][]{\lstset{style=displayhtml, #1}}{}
\def\inlinehtml{\lstinline[style=html, columns=fullflexible]}

\pagestyle{headings}
\isabellestyle{default}
\setcounter{tocdepth}{1}
\newcommand{\ie}{i.\,e.\xspace}
\newcommand{\eg}{e.\,g.\xspace}
\newcommand{\thy}{\isabellecontext}
\renewcommand{\isamarkupsection}[1]{%
  \begingroup% 
  \def\isacharunderscore{\textunderscore}%
  \section{#1 (\thy)}%
  \endgroup% 
}

\title{Shadow SC DOM\\\medskip \Large 
  A Formal Model of the Safely Composable Document Object Model \emph{with Shadow Roots}}%



\author{%
  \href{https://www.brucker.ch/}{Achim~D.~Brucker}\footnotemark[1]
  \and
  \href{https://www.michael-herzberg.de/}{Michael Herzberg}\footnotemark[2]
}  

\publishers{
  \footnotemark[1]~Department of Computer Science, University of Exeter, Exeter, UK\texorpdfstring{\\}{, }
  \texttt{a.brucker@exeter.ac.uk}\\[2em]
  %
  \footnotemark[2]~  Department of Computer Science, The University of Sheffield, Sheffield, UK\texorpdfstring{\\}{, }
   \texttt{msherzberg1@sheffield.ac.uk}
}
\begin{document}
  \maketitle
  \begin{abstract}
    \begin{quote}
      In this AFP entry, we extend our formalization of the safely
      composable  DOM
      (\href{https://www.isa-afp.org/entries/Core_SC_DOM.html}
      {Core\_SC\_DOM}) with \emph{Shadow Roots}. Shadow roots are a recent
      proposal of the web community to support a component-based
      development approach for client-side web applications. 

      Shadow roots are a significant extension to the DOM standard
      and, as web standards are condemned to be backward compatible,
      such extensions often result in complex specification that may
      contain unwanted subtleties that can be detected by a
      formalization.

      Our Isabelle/HOL formalization is, in the sense of
      object-orientation, an extension of our formalization of the
      core DOM and enjoys the same basic properties, i.e., it is
      \begin{inparaenum}
        \item \emph{extensible}, i.e., can be extended without the need of
              re-proving already proven properties and
        \item \emph{executable}, i.e., we can generate executable code
          from our specification.
      \end{inparaenum}
      We exploit the executability to show that our formalization
      complies to the official standard of the W3C, respectively,
      the WHATWG.

      \bigskip
      \noindent{\textbf{Keywords:}} 
      Document Object Model, DOM, Shadow Root, Web Component, Formal
      Semantics, Isabelle/HOL
    \end{quote}
  \end{abstract}


\tableofcontents
\cleardoublepage

\chapter{Introduction}

In a world in which more and more applications are offered as services
on the internet, web browsers start to take on a similarly central
role in our daily IT infrastructure as operating systems. Thus, web
browsers should be developed as rigidly and formally as operating
systems. While formal methods are a well-established technique in the
development of operating systems (see,
\eg,~\citet{klein:operating:2009} for an overview of formal
verification of operating systems), there are few proposals for
improving the development of web browsers using formal
approaches~\cite{gardner.ea:dom:2008,raad.ea:dom:2016,jang.ea:establishing:2012,bohannon.ea:featherweight:2010}.

In~\cite{brucker.ea:afp-core-sc-dom:2020}, we formalized the core of
the safely composable Document Object Model (DOM) in
Isabelle/HOL\@. The DOM~\cite{whatwg:dom:2017,w3c:dom:2015} is
\emph{the} central data structure of all modern web browsers. In this
work, we extend the formalization presented
in~\cite{brucker.ea:afp-core-dom:2018} with support for \emph{shadow
  trees}. Shadow trees are a recent addition to the DOM
standard~\cite{whatwg:dom:2017} that promise support for web
components. As we will see, this promise is not fully achieved and,
for example, the DOM standard itself does not formally define what a
component should be. In this work, we focus on a standard compliant
representation of the DOM with shadow
trees. As~\cite{brucker.ea:afp-core-sc-dom:2020}, our formalization has
the following properties:
\begin{itemize}
\item It provides a \emph{consistency guarantee.} Since all
  definitions in our formal semantics are conservative and all rules
  are derived, the logical consistency of the DOM node-tree is reduced
  to the consistency of HOL.
\item It serves as a \emph{technical basis for a proof system.}  Based
  on the derived rules and specific setup of proof tactics over
  node-trees, our formalization provides a generic proof environment
  for the verification of programs manipulating node-trees.
\item It is \emph{executable}, which allows to validate its compliance
  to the standard by evaluating the compliance test suite on the
  formal model and
\item It is \emph{extensible} in the sense
  of~\cite{brucker.ea:extensible:2008-b,brucker:interactive:2007},
  \ie, properties proven over the core DOM do not need to be re-proven
  for object-oriented extensions such as the HTML document model.
\end{itemize}

In this AFP entry, we limit ourselves to the faithful formalization of
the DOM. As the DOM standard does not formally define web components,
we address the question of formally defining web components and
discussing their safety properties
elsewhere~\cite{brucker.ea:afp-sc-dom-components:2020,brucker.ea:web-components:2019}.

The rest of this document is automatically generated from the formalization 
in Isabelle/HOL, i.e., all content is checked by Isabelle (for a more 
abstract presentation and more explanations, please 
see~\cite{herzberg:web-components:2020}). The structure follows the theory 
dependencies (see \autoref{fig:session-graph}): first, we formalize the DOM 
with Shadow Roots (\autoref{cha:dom}) and then formalize we the relevant
compliance test cases in \autoref{cha:tests}. 

\paragraph{Important Note:} This document describes the formalization
of the \emph{Safely Composable Document Object Model with Shadow
  Roots} (SC DOM with Shadow Roots), which deviated in one important
aspect from the official DOM standard: in the SC DOM, the shadow root
is a sub-class of the document class (instead of a base class). This
modification results in a stronger notion of web components that
provide improved safety properties for the composition of web
components. While the SC DOM still passes the compliance test suite as
provided by the authors of the DOM standard, its data model is
different. We refer readers interested in a formalisation of the
standard compliant DOM to the AFP entries
``Core\_DOM''~\cite{brucker.ea:afp-core-dom:2018} and
``Shadow\_DOM''~\cite{brucker.ea:afp-shadow-dom:2020}.


\begin{figure}
  \centering
  \includegraphics[angle=90,scale=0.5]{session_graph}
  \caption{The Dependency Graph of the Isabelle Theories.\label{fig:session-graph}}
\end{figure}

\clearpage

\chapter{The Shadow DOM}
\label{cha:dom}
In this chapter, we introduce the formalization of the core DOM
\emph{with Shadow Roots}, i.e., the most important algorithms for
querying or modifying the Shadow DOM, as defined in the standard.

\input{ShadowRootClass.tex}
\input{ShadowRootMonad.tex}
\input{Shadow_DOM.tex}


\chapter{Test Suite}
\label{cha:tests}
In this chapter, we present the formalized compliance test cases for
the core DOM. As our formalization is executable, we can
(symbolically) execute the test cases on top of our model. Executing
these test cases successfully shows that our model is compliant to the
official DOM standard. As future work, we plan to generate test cases
from our formal model (e.g.,
using~\cite{brucker.ea:interactive:2005,brucker.ea:theorem-prover:2012})
to improve the quality of the official compliance test suite. For more
details on the relation of test and proof in the context of web
standards, we refer the reader to
\cite{brucker.ea:standard-compliance-testing:2018}.

\input{Shadow_DOM_BaseTest.tex}
\input{slots.tex}
\input{slots_fallback.tex}
\input{Shadow_DOM_Document_adoptNode.tex}
\input{Shadow_DOM_Document_getElementById.tex}
\input{Shadow_DOM_Node_insertBefore.tex}
\input{Shadow_DOM_Node_removeChild.tex}
\input{Shadow_DOM_Tests.tex}


{\small
  \bibliographystyle{abbrvnat}
  \bibliography{root}
}
\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
