article.tex

   1 \documentclass[a4paper,leqno]{strayman}
   2 \errorcontextlines=50
   3 \let\numberwithin=\notdef
   4 \usepackage{amsmath}
   5 \usepackage{mathabx}
   6 \usepackage{txfonts}
   7 \usepackage{amsfonts}
   8 \usepackage{mdwlist}
   9 %\usepackage{accents}
  10
  11 \usepackage{fancyhdr}
  12 \pagestyle{fancy}
  13 \lhead[\rightmark]{}
  14
  15 \let\stdsection\section
  16 \renewcommand\section{\newpage\stdsection}
  17
  18 \renewcommand{\ge}{\geqslant}
  19 \renewcommand{\le}{\leqslant}
  20 \newcommand{\nge}{\ngeqslant}
  21 \newcommand{\nle}{\nleqslant}
  22
  23 \newcommand{\has}{\sqsupseteq}
  24 \newcommand{\isin}{\sqsubseteq}
  25
  26 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
  27 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
  28 \newcommand{\haspatch}{\sqSupset}
  29 \newcommand{\patchisin}{\sqSubset}
  30
  31         \newif\ifhidehack\hidehackfalse
  32         \DeclareRobustCommand\hidefromedef[2]{%
  33           \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
  34         \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
  35
  36 \newcommand{\set}[1]{\mathbb{#1}}
  37 \newcommand{\pay}[1]{\pa{#1}^+}
  38 \newcommand{\pan}[1]{\pa{#1}^-}
  39
  40 \newcommand{\p}{\pa{P}}
  41 \newcommand{\py}{\pay{P}}
  42 \newcommand{\pn}{\pan{P}}
  43
  44 \newcommand{\pq}{\pa{Q}}
  45 \newcommand{\pqy}{\pay{Q}}
  46 \newcommand{\pqn}{\pan{Q}}
  47
  48 \newcommand{\pr}{\pa{R}}
  49 \newcommand{\pry}{\pay{R}}
  50 \newcommand{\prn}{\pan{R}}
  51
  52 %\newcommand{\hasparents}{\underaccent{1}{>}}
  53 %\newcommand{\hasparents}{{%
  54 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
  55 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
  56 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
  57
  58 \renewcommand{\implies}{\Rightarrow}
  59 \renewcommand{\equiv}{\Leftrightarrow}
  60 \renewcommand{\nequiv}{\nLeftrightarrow}
  61 \renewcommand{\land}{\wedge}
  62 \renewcommand{\lor}{\vee}
  63
  64 \newcommand{\pancs}{{\mathcal A}}
  65 \newcommand{\pends}{{\mathcal E}}
  66
  67 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
  68 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
  69
  70 \newcommand{\merge}{{\mathcal M}}
  71 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
  72 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
  73
  74 \newcommand{\patch}{{\mathcal P}}
  75 \newcommand{\base}{{\mathcal B}}
  76
  77 \newcommand{\patchof}[1]{\patch ( #1 ) }
  78 \newcommand{\baseof}[1]{\base ( #1 ) }
  79
  80 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
  81 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
  82
  83 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
  84 \newcommand{\bigforall}{%
  85   \mathop{\mathchoice%
  86     {\hbox{\huge$\forall$}}%
  87     {\hbox{\Large$\forall$}}%
  88     {\hbox{\normalsize$\forall$}}%
  89     {\hbox{\scriptsize$\forall$}}}%
  90 }
  91
  92 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
  93 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
  94
  95 \newcommand{\qed}{\square}
  96 \newcommand{\proofstarts}{{\it Proof:}}
  97 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
  98
  99 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
 100 \newcommand{\gathnext}{\\ \tag*{}}
 101
 102 \newcommand{\true}{t}
 103 \newcommand{\false}{f}
 104
 105 \begin{document}
 106
 107 \section{Notation}
 108
 109 \begin{basedescript}{
 110 \desclabelwidth{5em}
 111 \desclabelstyle{\nextlinelabel}
 112 }
 113 \item[ $ C \hasparents \set X $ ]
 114 The parents of commit $C$ are exactly the set
 115 $\set X$.
 116
 117 \item[ $ C \ge D $ ]
 118 $C$ is a descendant of $D$ in the git commit
 119 graph.  This is a partial order, namely the transitive closure of
 120 $ D \in \set X $ where $ C \hasparents \set X $.
 121
 122 \item[ $ C \has D $ ]
 123 Informally, the tree at commit $C$ contains the change
 124 made in commit $D$.  Does not take account of deliberate reversions by
 125 the user or reversion, rebasing or rewinding in
 126 non-Topbloke-controlled branches.  For merges and Topbloke-generated
 127 anticommits or re-commits, the ``change made'' is only to be thought
 128 of as any conflict resolution.  This is not a partial order because it
 129 is not transitive.
 130
 131 \item[ $ \p, \py, \pn $ ]
 132 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
 133 are respectively the base and tip git branches.  $\p$ may be used
 134 where the context requires a set, in which case the statement
 135 is to be taken as applying to both $\py$ and $\pn$.
 136 None of these sets overlap.  Hence:
 137
 138 \item[ $ \patchof{ C } $ ]
 139 Either $\p$ s.t. $ C \in \p $, or $\bot$.
 140 A function from commits to patches' sets $\p$.
 141
 142 \item[ $ \pancsof{C}{\set P} $ ]
 143 $ \{ A \; | \; A \le C \land A \in \set P \} $
 144 i.e. all the ancestors of $C$
 145 which are in $\set P$.
 146
 147 \item[ $ \pendsof{C}{\set P} $ ]
 148 $ \{ E \; | \; E \in \pancsof{C}{\set P}
 149   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
 150   E \neq A \land E \le A \} $
 151 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
 152
 153 \item[ $ \baseof{C} $ ]
 154 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
 155 A partial function from commits to commits.
 156 See Unique Base, below.
 157
 158 \item[ $ C \haspatch \p $ ]
 159 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
 160 ~ Informally, $C$ has the contents of $\p$.
 161
 162 \item[ $ C \nothaspatch \p $ ]
 163 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
 164 ~ Informally, $C$ has none of the contents of $\p$.
 165
 166 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$.  This
 167 includes commits on plain git branches made by applying a Topbloke
 168 patch.  If a Topbloke
 169 patch is applied to a non-Topbloke branch and then bubbles back to
 170 the relevant Topbloke branches, we hope that
 171 if the user still cares about the Topbloke patch,
 172 git's merge algorithm will DTRT when trying to re-apply the changes.
 173
 174 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
 175 The contents of a git merge result:
 176
 177 $\displaystyle D \isin C \equiv
 178   \begin{cases}
 179     (D \isin L \land D \isin R) \lor D = C : & \true \\
 180     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
 181     \text{otherwise} : & D \not\isin M
 182   \end{cases}
 183 $
 184
 185 \end{basedescript}
 186 \newpage
 187 \section{Invariants}
 188
 189 We maintain these each time we construct a new commit. \\
 190 \[ \eqn{No Replay:}{
 191   C \has D \implies C \ge D
 192 }\]
 193 \[\eqn{Unique Base:}{
 194  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
 195 }\]
 196 \[\eqn{Tip Contents:}{
 197   \bigforall_{C \in \py} D \isin C \equiv
 198     { D \isin \baseof{C} \lor \atop
 199       (D \in \py \land D \le C) }
 200 }\]
 201 \[\eqn{Base Acyclic:}{
 202   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
 203 }\]
 204 \[\eqn{Coherence:}{
 205   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
 206 }\]
 207 \[\eqn{Foreign Inclusion:}{
 208   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
 209 }\]
 210 \[\eqn{Foreign Contents:}{
 211   \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
 212     D \le C \implies \patchof{D} = \bot
 213 }\]
 214
 215 \section{Some lemmas}
 216
 217 \subsection{Alternative (overlapping) formulations of $\mergeof{C}{L}{M}{R}$}
 218 $$
 219  D \isin C \equiv
 220   \begin{cases}
 221     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
 222     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
 223     D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
 224     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
 225     \text{as above with L and R exchanged}
 226   \end{cases}
 227 $$
 228 \proof{ ~ Truth table (ordered by original definition): \\
 229   \begin{tabular}{cccc|c|cc}
 230      $D = C$ &
 231           $\isin L$ &
 232                $\isin M$ &
 233                     $\isin R$ & $\isin C$ &
 234                                       $L$ vs. $R$ & $L$ vs. $M$
 235   \\\hline
 236      y &  ? &  ? &  ?      &      y   & ?         & ?            \\
 237      n &  y &  y &  y      &      y   & $\equiv$  & $\equiv$     \\
 238      n &  y &  n &  y      &      y   & $\equiv$  & $\nequiv$    \\
 239      n &  n &  y &  n      &      n   & $\equiv$  & $\nequiv$    \\
 240      n &  n &  n &  n      &      n   & $\equiv$  & $\equiv$     \\
 241      n &  y &  y &  n      &      n   & $\nequiv$ & $\equiv$     \\
 242      n &  n &  y &  y      &      n   & $\nequiv$ & $\nequiv$    \\
 243      n &  y &  n &  n      &      y   & $\nequiv$ & $\nequiv$    \\
 244      n &  n &  n &  y      &      y   & $\nequiv$ & $\equiv$     \\
 245   \end{tabular} \\
 246   And original definition is symmetrical in $L$ and $R$.
 247 }
 248
 249 \subsection{Exclusive Tip Contents}
 250 $$
 251   \bigforall_{C \in \py}
 252     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
 253       \Bigr]
 254 $$
 255 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 256
 257 \proof{
 258 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
 259 So by Base Acyclic $D \isin B \implies D \notin \py$.
 260 }
 261 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
 262   \bigforall_{C \in \py} D \isin C \equiv
 263   \begin{cases}
 264     D \in \py : & D \le C \\
 265     D \not\in \py : & D \isin \baseof{C}
 266   \end{cases}
 267 }\]
 268
 269 \subsection{Tip Self Inpatch}
 270 $$
 271   \bigforall_{C \in \py} C \haspatch \p
 272 $$
 273 Ie, tip commits contain their own patch.
 274
 275 \proof{
 276 Apply Exclusive Tip Contents to some $D \in \py$:
 277 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
 278   D \isin C \equiv D \le C $
 279 }
 280
 281 \subsection{Exact Ancestors}
 282 $$
 283   \bigforall_{ C \hasparents \set{R} }
 284   D \le C \equiv
 285     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
 286     \lor D = C
 287 $$
 288 \proof{ ~ Trivial.}
 289
 290 \subsection{Transitive Ancestors}
 291 $$
 292   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
 293   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
 294 $$
 295
 296 \proof{
 297 The implication from right to left is trivial because
 298 $ \pends() \subset \pancs() $.
 299 For the implication from left to right:
 300 by the definition of $\mathcal E$,
 301 for every such $A$, either $A \in \pends()$ which implies
 302 $A \le M$ by the LHS directly,
 303 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
 304 in which case we repeat for $A'$.  Since there are finitely many
 305 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 306 by the LHS.  And $A \le A''$.
 307 }
 308
 309 \subsection{Calculation Of Ends}
 310 $$
 311   \bigforall_{C \hasparents \set A}
 312     \pendsof{C}{\set P} =
 313       \begin{cases}
 314        C \in \p : & \{ C \}
 315       \\
 316        C \not\in \p : & \displaystyle
 317        \left\{ E \Big|
 318            \Bigl[ \Largeexists_{A \in \set A}
 319                        E \in \pendsof{A}{\set P} \Bigr] \land
 320            \Bigl[ \Largenexists_{B \in \set A, F \in \pendsof{B}{\p}}
 321                        E \neq F \land E \le F \Bigr]
 322        \right\}
 323       \end{cases}
 324 $$
 325 \proof{
 326 Trivial for $C \in \set P$.  For $C \not\in \set P$,
 327 $\pancsof{C}{\set P} = \bigcup_{A \in \set A} \pancsof{A}{\set P}$.
 328 So $\pendsof{C}{\set P} \subset \bigcup_{E in \set E} \pendsof{E}{\set P}$.
 329 Consider some $E \in \pendsof{A}{\set P}$.  If $\exists_{B,F}$ as
 330 specified, then either $F$ is going to be in our result and
 331 disqualifies $E$, or there is some other $F'$ (or, eventually,
 332 an $F''$) which disqualifies $F$.
 333 Otherwise, $E$ meets all the conditions for $\pends$.
 334 }
 335
 336 \subsection{Ingredients Prevent Replay}
 337 $$
 338   \left[
 339     {C \hasparents \set A} \land
 340    \\
 341     \left(
 342       D \isin C \implies
 343        D = C \lor
 344        \Largeexists_{A \in \set A} D \isin A
 345     \right)
 346   \right] \implies \left[
 347     D \isin C \implies D \le C
 348   \right]
 349 $$
 350 \proof{
 351   Trivial for $D = C$.  Consider some $D \neq C$, $D \isin C$.
 352   By the preconditions, there is some $A$ s.t. $D \in \set A$
 353   and $D \isin A$.  By No Replay for $A$, $D \le A$.  And
 354   $A \le C$ so $D \le C$.
 355 }
 356
 357 \subsection{Simple Foreign Inclusion}
 358 $$
 359   \left[
 360     C \hasparents \{ L \}
 361    \land
 362     \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
 363   \right]
 364  \implies
 365   \left[
 366    \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
 367      D \isin C \equiv D \le C
 368   \right]
 369 $$
 370 \proof{
 371 Consider some $D$ s.t. $\patchof{D} = \bot$.
 372 If $D = C$, trivially true.  For $D \neq C$,
 373 by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 374 And by Exact Ancestors $D \le L \equiv D \le C$.
 375 So $D \isin C \equiv D \le C$.
 376 }
 377
 378 \subsection{Totally Foreign Contents}
 379 $$
 380   \bigforall_{C \hasparents \set A}
 381    \left[
 382     \patchof{C} = \bot \land
 383       \bigforall_{A \in \set A} \patchof{A} = \bot
 384    \right]
 385   \implies
 386    \left[
 387     D \le C
 388    \implies
 389     \patchof{D} = \bot
 390    \right]
 391 $$
 392 \proof{
 393 Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
 394 If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
 395 Contents of $A$, $\patchof{D} = \bot$.
 396 }
 397
 398 \section{Commit annotation}
 399
 400 We annotate each Topbloke commit $C$ with:
 401 \gathbegin
 402  \patchof{C}
 403 \gathnext
 404  \baseof{C}, \text{ if } C \in \py
 405 \gathnext
 406  \bigforall_{\pq}
 407    \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
 408 \gathnext
 409  \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
 410 \end{gather}
 411
 412 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
 413 in the summary in the section for that kind of commit.
 414
 415 Whether $\baseof{C}$ is required, and if so what the value is, is
 416 stated in the proof of Unique Base for each kind of commit.
 417
 418 $C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
 419 set $\{ \pq | C \haspatch \pq \}$.  Whether $C \haspatch \pq$
 420 is in stated
 421 (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
 422 for the ingredients $I$),
 423 in the proof of Coherence for each kind of commit.
 424
 425 $\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
 426 using the lemma Calculation of Ends, above.
 427 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 428 make it wrong to make plain commits with git because the recorded $\pends$
 429 would have to be updated.  The annotation is not needed in that case
 430 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 431
 432 \section{Simple commit}
 433
 434 A simple single-parent forward commit $C$ as made by git-commit.
 435 \begin{gather}
 436 \tag*{} C \hasparents \{ L \} \\
 437 \tag*{} \patchof{C} = \patchof{L} \\
 438 \tag*{} D \isin C \equiv D \isin L \lor D = C
 439 \end{gather}
 440 This also covers Topbloke-generated commits on plain git branches:
 441 Topbloke strips the metadata when exporting.
 442
 443 \subsection{No Replay}
 444
 445 Ingredients Prevent Replay applies.  $\qed$
 446
 447 \subsection{Unique Base}
 448 If $L, C \in \py$ then by Calculation of Ends for
 449 $C, \py, C \not\in \py$:
 450 $\pendsof{C}{\pn} = \pendsof{L}{\pn}$ so
 451 $\baseof{C} = \baseof{L}$. $\qed$
 452
 453 \subsection{Tip Contents}
 454 We need to consider only $L, C \in \py$.  From Tip Contents for $L$:
 455 \[ D \isin L \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L ) \]
 456 Substitute into the contents of $C$:
 457 \[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L )
 458     \lor D = C \]
 459 Since $D = C \implies D \in \py$,
 460 and substituting in $\baseof{C}$, this gives:
 461 \[ D \isin C \equiv D \isin \baseof{C} \lor
 462     (D \in \py \land D \le L) \lor
 463     (D = C \land D \in \py) \]
 464 \[ \equiv D \isin \baseof{C} \lor
 465    [ D \in \py \land ( D \le L \lor D = C ) ] \]
 466 So by Exact Ancestors:
 467 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 468 ) \]
 469 $\qed$
 470
 471 \subsection{Base Acyclic}
 472
 473 Need to consider only $L, C \in \pn$.
 474
 475 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 476
 477 For $D \neq C$: $D \isin C \equiv D \isin L$, so by Base Acyclic for
 478 $L$, $D \isin C \implies D \not\in \py$.
 479
 480 $\qed$
 481
 482 \subsection{Coherence and patch inclusion}
 483
 484 Need to consider $D \in \py$
 485
 486 \subsubsection{For $L \haspatch P, D = C$:}
 487
 488 Ancestors of $C$:
 489 $ D \le C $.
 490
 491 Contents of $C$:
 492 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 493
 494 \subsubsection{For $L \haspatch P, D \neq C$:}
 495 Ancestors: $ D \le C \equiv D \le L $.
 496
 497 Contents: $ D \isin C \equiv D \isin L \lor f $
 498 so $ D \isin C \equiv D \isin L $.
 499
 500 So:
 501 \[ L \haspatch P \implies C \haspatch P \]
 502
 503 \subsubsection{For $L \nothaspatch P$:}
 504
 505 Firstly, $C \not\in \py$ since if it were, $L \in \py$.
 506 Thus $D \neq C$.
 507
 508 Now by contents of $L$, $D \notin L$, so $D \notin C$.
 509
 510 So:
 511 \[ L \nothaspatch P \implies C \nothaspatch P \]
 512 $\qed$
 513
 514 \subsection{Foreign Inclusion:}
 515
 516 Simple Foreign Inclusion applies.  $\qed$
 517
 518 \subsection{Foreign Contents:}
 519
 520 Only relevant if $\patchof{C} = \bot$, and in that case Totally
 521 Foreign Contents applies. $\qed$
 522
 523 \section{Create Base}
 524
 525 Given $L$, create a Topbloke base branch initial commit $B$.
 526 \gathbegin
 527  B \hasparents \{ L \}
 528 \gathnext
 529  \patchof{B} = \pqn
 530 \gathnext
 531  D \isin B \equiv D \isin L \lor D = B
 532 \end{gather}
 533
 534 \subsection{Conditions}
 535
 536 \[ \eqn{ Ingredients }{
 537  \patchof{L} = \pa{L} \lor \patchof{L} = \bot
 538 }\]
 539 \[ \eqn{ Create Acyclic }{
 540  L \not\haspatch \pq
 541 }\]
 542
 543 \subsection{No Replay}
 544
 545 Ingredients Prevent Replay applies.  $\qed$
 546
 547 \subsection{Unique Base}
 548
 549 Not applicable.
 550
 551 \subsection{Tip Contents}
 552
 553 Not applicable.
 554
 555 \subsection{Base Acyclic}
 556
 557 Consider some $D \isin B$.  If $D = B$, $D \in \pqn$.
 558 If $D \neq B$, $D \isin L$, and by Create Acyclic
 559 $D \not\in \pqy$.  $\qed$
 560
 561 \subsection{Coherence and Patch Inclusion}
 562
 563 Consider some $D \in \p$.
 564 $B \not\in \py$ so $D \neq B$.  So $D \isin B \equiv D \isin L$
 565 and $D \le B \equiv D \le L$.
 566
 567 Thus $L \haspatch \p \implies B \haspatch P$
 568 and $L \nothaspatch \p \implies B \nothaspatch P$.
 569
 570 $\qed$.
 571
 572 \subsection{Foreign Inclusion}
 573
 574 Simple Foreign Inclusion applies. $\qed$
 575
 576 \subsection{Foreign Contents}
 577
 578 Not applicable.
 579
 580 \section{Create Tip}
 581
 582 Given a Topbloke base $B$, create a tip branch initial commit B.
 583 \gathbegin
 584  C \hasparents \{ B \}
 585 \gathnext
 586  \patchof{B} = \pqy
 587 \gathnext
 588  D \isin C \equiv D \isin B \lor D = C
 589 \end{gather}
 590
 591 \subsection{Conditions}
 592
 593 \[ \eqn{ Ingredients }{
 594  \patchof{B} = \pqn
 595 }\]
 596 \[ \eqn{ No Sneak }{
 597  \pendsof{B}{\pqy} = \{ \}
 598 }\]
 599
 600 \subsection{No Replay}
 601
 602 Ingredients Prevent Replay applies.  $\qed$
 603
 604 \subsection{Unique Base}
 605
 606 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.  $\qed$
 607
 608 \subsection{Tip Contents}
 609
 610 Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.
 611
 612 If $D \neq C$, $D \isin C \equiv D \isin B$.
 613 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
 614 So $D \isin C \equiv D \isin \baseof{B}$.
 615
 616 $\qed$
 617
 618 \subsection{Base Acyclic}
 619
 620 Not applicable.
 621
 622 \subsection{Coherence and Patch Inclusion}
 623
 624 $$
 625 \begin{cases}
 626   \p = \pq    \lor B \haspatch \p : & C \haspatch \p \\
 627   \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
 628 \end{cases}
 629 $$
 630
 631 \proofstarts
 632 ~ Consider some $D \in \py$.
 633
 634 \subsubsection{For $\p = \pq$:}
 635
 636 By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
 637 By No Sneak, $D \le B \equiv D = C$.  Thus $C \haspatch \pq$.
 638
 639 \subsubsection{For $\p \neq \pq$:}
 640
 641 $D \neq C$.  So $D \isin C \equiv D \isin B$,
 642 and $D \le C \equiv D \le B$.
 643
 644 $\qed$
 645
 646 \subsection{Foreign Inclusion}
 647
 648 Simple Foreign Inclusion applies.  $\qed$
 649
 650 \subsection{Foreign Contents}
 651
 652 Not applicable.
 653
 654 \section{Anticommit}
 655
 656 Given $L$ and $\pr$ as represented by $R^+, R^-$.
 657 Construct $C$ which has $\pr$ removed.
 658 Used for removing a branch dependency.
 659 \gathbegin
 660  C \hasparents \{ L \}
 661 \gathnext
 662  \patchof{C} = \patchof{L}
 663 \gathnext
 664  \mergeof{C}{L}{R^+}{R^-}
 665 \end{gather}
 666
 667 \subsection{Conditions}
 668
 669 \[ \eqn{ Ingredients }{
 670 R^+ \in \pry \land R^- = \baseof{R^+}
 671 }\]
 672 \[ \eqn{ Into Base }{
 673  L \in \pn
 674 }\]
 675 \[ \eqn{ Unique Tip }{
 676  \pendsof{L}{\pry} = \{ R^+ \}
 677 }\]
 678 \[ \eqn{ Currently Included }{
 679  L \haspatch \pry
 680 }\]
 681
 682 \subsection{Ordering of Ingredients:}
 683
 684 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 685 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
 686 $\qed$
 687
 688 (Note that $R^+ \not\le R^-$, i.e. the merge base
 689 is a descendant, not an ancestor, of the 2nd parent.)
 690
 691 \subsection{No Replay}
 692
 693 By definition of $\merge$,
 694 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
 695 So, by Ordering of Ingredients,
 696 Ingredients Prevent Replay applies.  $\qed$
 697
 698 \subsection{Desired Contents}
 699
 700 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 701 \proofstarts
 702
 703 \subsubsection{For $D = C$:}
 704
 705 Trivially $D \isin C$.  OK.
 706
 707 \subsubsection{For $D \neq C, D \not\le L$:}
 708
 709 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 710 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 711
 712 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 713
 714 By Currently Included, $D \isin L$.
 715
 716 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 717 by Unique Tip, $D \le R^+ \equiv D \le L$.
 718 So $D \isin R^+$.
 719
 720 By Base Acyclic, $D \not\isin R^-$.
 721
 722 Apply $\merge$: $D \not\isin C$.  OK.
 723
 724 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 725
 726 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 727
 728 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 729
 730 $\qed$
 731
 732 \subsection{Unique Base}
 733
 734 Into Base means that $C \in \pn$, so Unique Base is not
 735 applicable. $\qed$
 736
 737 \subsection{Tip Contents}
 738
 739 Again, not applicable. $\qed$
 740
 741 \subsection{Base Acyclic}
 742
 743 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
 744 And by Into Base $C \not\in \py$.
 745 Now from Desired Contents, above, $D \isin C
 746 \implies D \isin L \lor D = C$, which thus
 747 $\implies D \not\in \py$.  $\qed$.
 748
 749 \subsection{Coherence and Patch Inclusion}
 750
 751 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
 752
 753 \subsubsection{For $\p = \pr$:}
 754 By Desired Contents, above, $D \not\isin C$.
 755 So $C \nothaspatch \pr$.
 756
 757 \subsubsection{For $\p \neq \pr$:}
 758 By Desired Contents, $D \isin C \equiv D \isin L$
 759 (since $D \in \py$ so $D \not\in \pry$).
 760
 761 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
 762 So $L \nothaspatch \p \implies C \nothaspatch \p$.
 763
 764 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
 765 so $L \haspatch \p \implies C \haspatch \p$.
 766
 767 $\qed$
 768
 769 \subsection{Foreign Inclusion}
 770
 771 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
 772 So by Desired Contents $D \isin C \equiv D \isin L$.
 773 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 774
 775 And $D \le C \equiv D \le L$.
 776 Thus $D \isin C \equiv D \le C$.
 777
 778 $\qed$
 779
 780 \subsection{Foreign Contents}
 781
 782 Not applicable.
 783
 784 \section{Merge}
 785
 786 Merge commits $L$ and $R$ using merge base $M$:
 787 \gathbegin
 788  C \hasparents \{ L, R \}
 789 \gathnext
 790  \patchof{C} = \patchof{L}
 791 \gathnext
 792  \mergeof{C}{L}{M}{R}
 793 \end{gather}
 794 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 795
 796 \subsection{Conditions}
 797 \[ \eqn{ Ingredients }{
 798  M \le L, M \le R
 799 }\]
 800 \[ \eqn{ Tip Merge }{
 801  L \in \py \implies
 802    \begin{cases}
 803       R \in \py : & \baseof{R} \ge \baseof{L}
 804               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 805       R \in \pn : & M = \baseof{L} \\
 806       \text{otherwise} : & \false
 807    \end{cases}
 808 }\]
 809 \[ \eqn{ Merge Acyclic }{
 810     L \in \pn
 811    \implies
 812     R \nothaspatch \p
 813 }\]
 814 \[ \eqn{ Removal Merge Ends }{
 815     X \not\haspatch \p \land
 816     Y \haspatch \p \land
 817     M \haspatch \p
 818   \implies
 819     \pendsof{Y}{\py} = \pendsof{M}{\py}
 820 }\]
 821 \[ \eqn{ Addition Merge Ends }{
 822     X \not\haspatch \p \land
 823     Y \haspatch \p \land
 824     M \nothaspatch \p
 825    \implies \left[
 826     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 827    \right]
 828 }\]
 829 \[ \eqn{ Foreign Merges }{
 830     \patchof{L} = \bot \equiv \patchof{R} = \bot
 831 }\]
 832
 833 \subsection{Non-Topbloke merges}
 834
 835 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
 836 (Foreign Merges, above).
 837 I.e. not only is it forbidden to merge into a Topbloke-controlled
 838 branch without Topbloke's assistance, it is also forbidden to
 839 merge any Topbloke-controlled branch into any plain git branch.
 840
 841 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 842 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 843 Merge Ends condition applies.
 844
 845 So a plain git merge of non-Topbloke branches meets the conditions and
 846 is therefore consistent with our scheme.
 847
 848 \subsection{No Replay}
 849
 850 By definition of $\merge$,
 851 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
 852 So, by Ingredients,
 853 Ingredients Prevent Replay applies.  $\qed$
 854
 855 \subsection{Unique Base}
 856
 857 Need to consider only $C \in \py$, ie $L \in \py$,
 858 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 859 putative ancestor $A \in \pn$ and see whether $A \le C$.
 860
 861 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 862 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 863 Thus $A \le C \equiv A \le L \lor A \le R$.
 864
 865 By Unique Base of L and Transitive Ancestors,
 866 $A \le L \equiv A \le \baseof{L}$.
 867
 868 \subsubsection{For $R \in \py$:}
 869
 870 By Unique Base of $R$ and Transitive Ancestors,
 871 $A \le R \equiv A \le \baseof{R}$.
 872
 873 But by Tip Merge condition on $\baseof{R}$,
 874 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 875 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 876 Thus $A \le C \equiv A \le \baseof{R}$.
 877 That is, $\baseof{C} = \baseof{R}$.
 878
 879 \subsubsection{For $R \in \pn$:}
 880
 881 By Tip Merge condition on $R$ and since $M \le R$,
 882 $A \le \baseof{L} \implies A \le R$, so
 883 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 884 Thus $A \le C \equiv A \le R$.
 885 That is, $\baseof{C} = R$.
 886
 887 $\qed$
 888
 889 \subsection{Coherence and Patch Inclusion}
 890
 891 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 892 This involves considering $D \in \py$.
 893
 894 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 895 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 896 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 897 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 898
 899 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 900 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 901 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 902
 903 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 904
 905 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 906  \equiv D \isin L \lor D \isin R$.
 907 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 908
 909 Consider $D \neq C, D \isin X \land D \isin Y$:
 910 By $\merge$, $D \isin C$.  Also $D \le X$
 911 so $D \le C$.  OK for $C \haspatch \p$.
 912
 913 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 914 By $\merge$, $D \not\isin C$.
 915 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 916 OK for $C \haspatch \p$.
 917
 918 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 919 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 920 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 921 OK for $C \haspatch \p$.
 922
 923 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 924
 925 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 926
 927 $M \haspatch \p \implies C \nothaspatch \p$.
 928 $M \nothaspatch \p \implies C \haspatch \p$.
 929
 930 \proofstarts
 931
 932 One of the Merge Ends conditions applies.
 933 Recall that we are considering $D \in \py$.
 934 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 935 We will show for each of
 936 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 937 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 938
 939 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 940 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 941 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 942 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 943
 944 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 945 $D \le Y$ so $D \le C$.
 946 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 947
 948 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 949 $D \not\le Y$.  If $D \le X$ then
 950 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 951 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 952 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 953
 954 Consider $D \neq C, M \haspatch P, D \isin Y$:
 955 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 956 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 957 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 958
 959 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 960 By $\merge$, $D \not\isin C$.  OK.
 961
 962 $\qed$
 963
 964 \subsection{Base Acyclic}
 965
 966 This applies when $C \in \pn$.
 967 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 968
 969 Consider some $D \in \py$.
 970
 971 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 972 R$.  And $D \neq C$.  So $D \not\isin C$.
 973
 974 $\qed$
 975
 976 \subsection{Tip Contents}
 977
 978 We need worry only about $C \in \py$.
 979 And $\patchof{C} = \patchof{L}$
 980 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 981 of $C$, and its Coherence and Patch Inclusion, as just proved.
 982
 983 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 984 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 985 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 986 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 987 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 988
 989 We will consider an arbitrary commit $D$
 990 and prove the Exclusive Tip Contents form.
 991
 992 \subsubsection{For $D \in \py$:}
 993 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 994 \le C$.  OK.
 995
 996 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 997
 998 $D \neq C$.  By Tip Contents of $L$,
 999 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
1000 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
1001 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
1002 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
1003
1004 \subsubsection{For $D \not\in \py, R \in \py$:}
1005
1006 $D \neq C$.
1007
1008 By Tip Contents
1009 $D \isin L \equiv D \isin \baseof{L}$ and
1010 $D \isin R \equiv D \isin \baseof{R}$.
1011
1012 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
1013 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
1014 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
1015 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
1016
1017 So $D \isin M \equiv D \isin L$ and by $\merge$,
1018 $D \isin C \equiv D \isin R$.  But from Unique Base,
1019 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
1020
1021 $\qed$
1022
1023 \subsection{Foreign Inclusion}
1024
1025 Consider some $D$ s.t. $\patchof{D} = \bot$.
1026 By Foreign Inclusion of $L, M, R$:
1027 $D \isin L \equiv D \le L$;
1028 $D \isin M \equiv D \le M$;
1029 $D \isin R \equiv D \le R$.
1030
1031 \subsubsection{For $D = C$:}
1032
1033 $D \isin C$ and $D \le C$.  OK.
1034
1035 \subsubsection{For $D \neq C, D \isin M$:}
1036
1037 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
1038 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
1039
1040 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
1041
1042 By $\merge$, $D \isin C$.
1043 And $D \isin X$ means $D \le X$ so $D \le C$.
1044 OK.
1045
1046 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
1047
1048 By $\merge$, $D \not\isin C$.
1049 And $D \not\le L, D \not\le R$ so $D \not\le C$.
1050 OK
1051
1052 $\qed$
1053
1054 \subsection{Foreign Contents}
1055
1056 Only relevant if $\patchof{L} = \bot$, in which case
1057 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
1058 so Totally Foreign Contents applies.  $\qed$
1059
1060 \end{document}