strategy: reachable is going well

diff --git a/strategy.tex b/strategy.tex
index 253ffc31fb1340fbd8dff16516d6caa0f8b33262..a4716b313dd577c5e74c6e1a7afe4f39ba8be082 100644 (file)
--- a/strategy.tex
+++ b/strategy.tex
@@ -124,17 +124,3 @@ The set of reachable commits at the point where we have just generated
 $\tippy$, i.e. just after $\alg{Merge-Tip}(\p)$.
 
 \end{basedescript}
 $\tippy$, i.e. just after $\alg{Merge-Tip}(\p)$.
 
 \end{basedescript}

-
-\stdsection{ WIP tip satisfaction, reachable commits }
-
-We preserve/ensure
-$$ \tippy >= \pendsof{\allreach_{\py}}{\py} $$
-($\tippy$ is computed during traversal for the patch $\p$)
-
-We ensure this property by:
-  - we do not generate any commits for py other than
-    during Merge-Tip
-  - so at the start of Merge-Tip pendsof (O, py) = pendsof (U, py)
-  - Merge-Tip itself wip wip wip
-
-

diff --git a/trav-alg.tex b/trav-alg.tex
index 82bca6d99239bfbc0c87e3da8f4c3cdb4ba7fcb8..e56a8a912cdf0274b83e4bae94b4a1a679429ac6 100644 (file)
--- a/trav-alg.tex
+++ b/trav-alg.tex
@@ -34,8 +34,8 @@ such that:
    \equiv
   \pa E \isdep \pc
 }
    \equiv
   \pa E \isdep \pc
 }

-\statement{Tip Covers Inputs}{
-  \tipcy \ge \pendsof{\allsrcs}{\pcy}
+\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 Inputs' Bases}{
   \bigforall_{E \in \pendsof{\allsrcs}{\pcy}} \tipcn \ge \baseof{E}


@@ -153,5 +153,3 @@ $\alg{Merge}$ with $L = W, \; R = S$ and any suitable $M$.
 (Tip Source Merge.)
 
 \end{enumerate}
 (Tip Source Merge.)
 
 \end{enumerate}

-
-

diff --git a/trav-proofs.tex b/trav-proofs.tex
index 06a54cfb0521161bd329823d9d685a877c52e30b..421bb61c296fb8979b9d0744f067921eed0c0e0d 100644 (file)
--- a/trav-proofs.tex
+++ b/trav-proofs.tex
@@ -3,11 +3,34 @@
 For each operation called for by the traversal algorithms, we prove
 that the commit generation preconditions are met.
 
 For each operation called for by the traversal algorithms, we prove
 that the commit generation preconditions are met.
 

-WIP WHAT ABOUT PROVING ALL THE TRAVERSAL RESULTS
+\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}
 
 
 \subsection{Traversal Lemmas}
 

-Firstly, some lemmas.

 \statement{Tip Correct Contents}{
   \tipcy \haspatch \pa E
     \equiv
 \statement{Tip Correct Contents}{
   \tipcy \haspatch \pa E
     \equiv