From 6e7093d49c00150e48ebc264fb1a29de2004aeed Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Sat, 14 Jul 2012 02:43:34 +0100 Subject: [PATCH 1/1] strategy: move traversal proofs inline --- article.tex | 2 + trav-alg.tex | 97 ++++++++++++++++++++++++++++++++++++++++++--- trav-proofs.tex | 102 ------------------------------------------------ 3 files changed, 93 insertions(+), 108 deletions(-) diff --git a/article.tex b/article.tex index 2b54eec..6bbe082 100644 --- a/article.tex +++ b/article.tex @@ -159,6 +159,8 @@ \newcommand{\qed}{\square} \newcommand{\proofstarts}{{\it Proof:}} \newcommand{\proof}[1]{\proofstarts #1 $\qed$} +\newcommand{\commitproof}[1]{{\it Proof of commit generation conditions:} + #1 $\qed$} \newcommand{\statement}[2]{\[\eqn{ #1 }{ #2 }\]} diff --git a/trav-alg.tex b/trav-alg.tex index e56a8a9..c9647ad 100644 --- a/trav-alg.tex +++ b/trav-alg.tex @@ -4,8 +4,10 @@ commit $C$ using one of the commit kind recipies, we update $W \assign C$. In any such case where we say we're going to Merge with $L = W$, if $R \ge W$ we do not Merge but instead simply set -$W \assign R$.) +$W \assign R$. +For each commit generation operation called for by the traversal +algorithms, we prove that the commit generation preconditions are met.) For each patch $\pc \in \allpatches$ in topological order by $\hasdep$, lowest first: @@ -44,6 +46,46 @@ such that: \bigforall_{H \in \set H^{\pn}} \tipcn \ge H } +\subsection{Reachability and coverage} + +We ensure Tip Covers Reachable as follows: + +\begin{itemize} +\item We do not generate any commits $\in \py$ other than + during $\alg{Merge-Tip}(\py)$; +\item So at the start of $\alg{Merge-Tip}(\py)$, + $ \pendsof{\allreach}{\py} = \pendsof{\allsrcs}{\py} $ +\item $\alg{Merge-tip}$ arranges that when it is done + $\tippy \ge \pendsof{\allreach}{\py}$ --- see below. +\end{itemize} + +A corrolary is as follows: +\statement{Tip Covers Superior Reachable} { + \bigforall_{\pd \isdep \pc} + \tipdy \ge \pendsof{\allreachof{\pcy}}{\pdy} +} +\proof{ + No commits $\in \pdy$ are created other than during + $\alg{Merge-Tip}(\pd)$, which runs (and has thus completed) + before $\alg{Merge-Tip}(\pcy)$ + So $\pendsof{\allreachof{\pcy}}{\pdy} = + \pendsof{\allreachof{\pdy}}{\pdy}$. +} + +\subsection{Traversal Lemmas} + +\statement{Tip Correct Contents}{ + \tipcy \haspatch \pa E + \equiv + \pa E = \pc \lor \pa E \isdep \pc +} +\proof{ + For $\pc = \pa E$, Tip Own Contents suffices. + For $\pc \neq \pa E$, Exclusive Tip Contents + gives $D \isin \tipcy \equiv D \isin \baseof{\tipcy}$ + which by Correct Base $\equiv D \isin \tipcn$. +} + \subsection{$\alg{Merge-Base}(\pc)$} This algorithm attempts to construct a suitably updated version of the @@ -63,6 +105,10 @@ to generate a perfect answer, whereas this algorithm might involve merges and therefore might not produce a perfect answer if the situation is complicated. +For \alg{Merge-Base} we do not prove that the preconditions are met. +Instead, we check them at runtime. If they turn out not to be met, we +abandon \alg{Merge-Base} and resort to \alg{Recreate-Base}. + Initially, set $W \iassign W^{\pcn}$. \subsubsection{Bases and sources} @@ -74,7 +120,6 @@ In some order, perhaps interleaving the two kinds of merge: \item For each $\hasdep$-maximal $\pd \isdirdep \pc$, find a merge base $M \le W,\; \le \tipdy$ and merge $\tipdy$ into $W$. That is, use $\alg{Merge}$ with $L = W,\; R = \tipdy$. -(Base Dependency Merge.) \item For each $S \in S^{\pcn}_i$, merge it into $W$. That is, use $\alg{Merge}$ with $L = W,\; R = S,\; M = M^{\pcn}_i$. @@ -103,7 +148,17 @@ Choose a $\hasdep$-maximal direct dependency $\pd$ of $\pc$. \item Use $\alg{Create Base}$ with $L$ = $\tipdy,\; \pq = \pc$ to generate $C$ -and set $W \iassign C$. (Recreate Base Beginning.) +and set $W \iassign C$. + + \commitproof{ + Create Acyclic: by Tip Correct Contents of $L$, + $L \haspatch \pa E \equiv \pa E = \pd \lor \pa E \isdep \pd$. + Now $\pd \isdirdep \pc$, + so by Coherence, and setting $\pa E = \pc$, + $L \nothaspatch \pc$. I.e. $L \nothaspatch \pq$. OK. + + That's everything for Create Base. + } \item @@ -114,7 +169,16 @@ Execute the subalgorithm $\alg{Recreate-Recurse}(\pc)$. Declare that we contain all of the relevant information from the sources. That is, use $\alg{Pseudo-Merge}$ with $L = W, \; \set R = \{ W \} \cup \set S^{\pcn}$. -(Recreate Base Final Declaration.) + + \commitproof{ + Base Only: $\patchof{W} = \patchof{L} = \pn$. OK. + + Unique Tips: + Want to prove that for any $\p \isin C$, $\tipdy$ is a suitable $T$. + WIP TODO + + WIP TODO INCOMPLETE + } \end{enumerate} @@ -146,10 +210,31 @@ $L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$. \item TODO CHOOSE/REFINE W AND S as was done during Ranking for bases \item $\alg{Merge}$ from $\tipcn$. That is, $L = W, \; -R = \tipcn$ and choose any suitable $M$. (Tip Base Merge.) +R = \tipcn$ and choose any suitable $M$. + + \commitproof{ + $L = W$, $R = \tipcn$. + TODO TBD + + Afterwards, $\baseof{W} = \tipcn$. + } \item For each source $S \in \set S^{\pcy}$, $\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$. -(Tip Source Merge.) + + \commitproof{ + In fact, we do this backwards: $L = S$, $R = W$. + Since $S \in \pcy$, + the resulting $C \in \pcy$ and the remaining properties of the Merge + commit construction are symmetrical in $L$ and $R$ so this is fine. + + By the results of Tip Base Merge, $\baseof{W} = \tipcn$. + + By Base Ends Supreme, $\tipcn \ge \baseof{S}$ i.e. + $\baseof{R} \ge \baseof{L}$. + + Either $\baseof{L} = \baseof{M}$, or we must choose a different $M$ in + which case $M = \baseof{S}$ will suffice. + } \end{enumerate} diff --git a/trav-proofs.tex b/trav-proofs.tex index 421bb61..e69de29 100644 --- a/trav-proofs.tex +++ b/trav-proofs.tex @@ -1,102 +0,0 @@ -\section{Traversal phase --- proofs} - -For each operation called for by the traversal algorithms, we prove -that the commit generation preconditions are met. - -\subsection{Reachability and coverage} - -We ensure Tip Covers Reachable as follows: - -\begin{itemize} -\item We do not generate any commits $\in \py$ other than - during $\alg{Merge-Tip}(\py)$; -\item So at the start of $\alg{Merge-Tip}(\py)$, - $ \pendsof{\allreach}{\py} = \pendsof{\allsrcs}{\py} $ -\item $\alg{Merge-tip}$ arranges that when it is done - $\tippy \ge \pendsof{\allreach}{\py}$ --- see below. -\end{itemize} - -A corrolary is as follows: -\statement{Tip Covers Superior Reachable} { - \bigforall_{\pd \isdep \pc} - \tipdy \ge \pendsof{\allreachof{\pcy}}{\pdy} -} -\proof{ - No commits $\in \pdy$ are created other than during - $\alg{Merge-Tip}(\pd)$, which runs (and has thus completed) - before $\alg{Merge-Tip}(\pcy)$ - So $\pendsof{\allreachof{\pcy}}{\pdy} = - \pendsof{\allreachof{\pdy}}{\pdy}$. -} - -\subsection{Traversal Lemmas} - -\statement{Tip Correct Contents}{ - \tipcy \haspatch \pa E - \equiv - \pa E = \pc \lor \pa E \isdep \pc -} -\proof{ - For $\pc = \pa E$, Tip Own Contents suffices. - For $\pc \neq \pa E$, Exclusive Tip Contents - gives $D \isin \tipcy \equiv D \isin \baseof{\tipcy}$ - which by Correct Base $\equiv D \isin \tipcn$. -} - -\subsection{Base Dependency Merge, Base Sibling Merge} - -We do not prove that the preconditions are met. Instead, we check -them at runtime. If they turn out not to be met, we abandon -\alg{Merge-Base} and resort to \alg{Recreate-Base}. - -TODO COMPLETE MERGE-BASE STUFF - -WIP WHAT ABOUT PROVING ALL THE TRAVERSAL RESULTS - -\subsection{Recreate Base Beginning} - -To recap we are executing Create Base with -$L = \tipdy$ and $\pq = \pc$. - -\subsubsection{Create Acyclic} - -By Tip Correct Contents of $L$, -$L \haspatch \pa E \equiv \pa E = \pd \lor \pa E \isdep \pd$. -Now $\pd \isdirdep \pc$, -so by Coherence, and setting $\pa E = \pc$, -$L \nothaspatch \pc$. I.e. $L \nothaspatch \pq$. OK. - -That's everything for Create Base. $\qed$ - -\subsection{Recreate Base Final Declaration} - -\subsubsection{Base Only} $\patchof{W} = \patchof{L} = \pn$. OK. - -\subsubsection{Unique Tips} - -Want to prove that for any $\p \isin C$, $\tipdy$ is a suitable $T$. - -WIP - -\subsection{Tip Base Merge} - -$L = W$, $R = \tipcn$. - -TODO TBD - -Afterwards, $\baseof{W} = \tipcn$. - -\subsection{Tip Source Merge} - -In fact, we do this backwards: $L = S$, $R = W$. Since $S \in \pcy$, -the resulting $C \in \pcy$ and the remaining properties of the Merge -commit construction are symmetrical in $L$ and $R$ so this is fine. - -By the results of Tip Base Merge, $\baseof{W} = \tipcn$. - -By Base Ends Supreme, $\tipcn \ge \baseof{S}$ i.e. -$\baseof{R} \ge \baseof{L}$. - -Either $\baseof{L} = \baseof{M}$, or we must choose a different $M$ in -which case $M = \baseof{S}$ will suffice. - -- 2.30.2