\section{Traversal phase}

In general, unless stated otherwise below, when we generate a new
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$.

For each commit generation operation called for by the traversal
algorithms, we prove that the commit generation preconditions are met.

\subsection{Algorithm}

For each patch $\pc \in \allpatches$ in topological order by $\hasdep$,
lowest first:

\begin{enumerate}

\item Optionally, attempt
 $\alg{Merge-Base}(\pc)$.  This may or may not succeed.

\item If this didn't succeed, or was not attempted, execute
 $\alg{Recreate-Base}(\pc)$.

\item Then in any case, execute
 $\alg{Merge-Tip}(\pc)$.

\end{enumerate}

\subsection{Results}

After processing each $\pc$ we will have created $\tipcn$ and $\tipcy$
such that:
\statement{Correct Base}{
  \baseof{\tipcy} = \tipcn
}
\statement{Base Correct Contents}{
  \tipcn \haspatch \pa E
   \equiv
  \pa E \isdep \pc
}
\statement{Tip Covers Reachable}{
  \tipcy \ge \pendsof{\allreachof{\pcy}}{\pcy}
}
\statement{Base Covers Inputs' Bases}{
  \bigforall_{E \in \pendsof{\allsrcs}{\pcy}} \tipcn \ge \baseof{E}
}
\statement{Base Covers Base Inputs}{
  \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
base branch $\pcn$ using some existing version of $\pcn$ as a starting
point.

It should be executed noninteractively.  Specifically, if any step
fails with a merge conflict, the whole thing should be abandoned.
This avoids asking the user to resolve confusing conflicts.  It also
avoids asking the user to pointlessly resolve conflicts in situations
where we will later discover that $\alg{Merge-Base}$ wasn't feasible
after all.

If $\pc$ has only one direct dependency, this algorithm should not be
used as in that case $\alg{Recreate-Base}$ is trivial and guaranteed
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}

In some order, perhaps interleaving the two kinds of merge:

\begin{enumerate}

\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$.

\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$.
(Base Sibling Merge.)

\end{enumerate}

\subsubsection{Fixup}

Execute $\alg{Fixup-Base}(W,\pc)$.

TODO define Fixup-Base

\subsubsection{Result}

If all of that was successful, let $\tipcn = W$.

\subsection{$\alg{Recreate-Base}(\pc)$}

\begin{enumerate}

\item

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$.

 \commitproof{
  \condproof{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

Execute the subalgorithm $\alg{Recreate-Recurse}(\pc)$.

\item

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}$.

 \commitproof{
  \condproof{Base Only}{ $\patchof{W} = \patchof{L} = \pn$.  OK. }

  \condproof{Unique Tips}{
   Want to prove that for any $\p \isin C$, $\tipdy$ is a suitable $T$.
   WIP TODO
  }

  WIP TODO INCOMPLETE
 }

\end{enumerate}

\subsubsection{$\alg{Recreate-Recurse}(\pd)$}

\begin{enumerate}

\item Is $W \haspatch \pd$ ?  If so, there is nothing to do: return.

\item TODO what about non-Topbloke base branches

\item For all $\hasdep$-maximal $\pd' \isdirdep \pd$,
execute $\alg{Recreate-Recurse}(\pd')$.

\item Use $\alg{Pseudo-Merge}$ with $L = W,\; \set R = \{ \tipdn \}$.
(Recreate Base Dependency Base Declaration.)

\item Use $\alg{Merge}$ to apply $\pd$ to $W$.  That is,
$L = W, \; R = \tipdy, \; M = \baseof{R} = \tipdn$.
(Recreate Reapply.)

\end{enumerate}


\subsection{$\alg{Merge-Tip}(\pc)$}

\begin{enumerate}

\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 $M = \baseof{W}$.

 \commitproof{
  \condproof{Ingredients}{
   $M \le L$ is trivial.  For $M \le R$ we want
   $\tipcn \ge \baseof{W}$.
   Well $W \in \set S^{\pcy}$ so $W \in \allreachof{\pcn}$
   and $W \in \pcy$.  So $W \in \pendsof{\allreachof{\pcn}}{\pcy}$
   so Base Covers Reachable indeed
   $\tipcn \ge \baseof{W}$.
  }
  \condproof{Tip Merge}{ Trivial. }
  \condproof{Merge Acyclic}{
   By Base Acyclic, $\tipcn \nothaspatch \p$.
  }
  \condproof{Foreign Merges}{ Not applicable. }

  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$.

 \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 TODO CHECK THIS, $\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}
