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  \pendsof{L}{\pqy} = \{ \}
 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$, so by No Replay $D \le L$
 559 and by Create Acyclic
 560 $D \not\in \pqy$.  $\qed$
 561
 562 \subsection{Coherence and Patch Inclusion}
 563
 564 Consider some $D \in \p$.
 565 $B \not\in \py$ so $D \neq B$.  So $D \isin B \equiv D \isin L$
 566 and $D \le B \equiv D \le L$.
 567
 568 Thus $L \haspatch \p \implies B \haspatch P$
 569 and $L \nothaspatch \p \implies B \nothaspatch P$.
 570
 571 $\qed$.
 572
 573 \subsection{Foreign Inclusion}
 574
 575 Simple Foreign Inclusion applies. $\qed$
 576
 577 \subsection{Foreign Contents}
 578
 579 Not applicable.
 580
 581 \section{Create Tip}
 582
 583 Given a Topbloke base $B$, create a tip branch initial commit B.
 584 \gathbegin
 585  C \hasparents \{ B \}
 586 \gathnext
 587  \patchof{B} = \pqy
 588 \gathnext
 589  D \isin C \equiv D \isin B \lor D = C
 590 \end{gather}
 591
 592 \subsection{Conditions}
 593
 594 \[ \eqn{ Ingredients }{
 595  \patchof{B} = \pqn
 596 }\]
 597 \[ \eqn{ No Sneak }{
 598  \pendsof{B}{\pqy} = \{ \}
 599 }\]
 600
 601 \subsection{No Replay}
 602
 603 Ingredients Prevent Replay applies.  $\qed$
 604
 605 \subsection{Unique Base}
 606
 607 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.  $\qed$
 608
 609 \subsection{Tip Contents}
 610
 611 Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.
 612
 613 If $D \neq C$, $D \isin C \equiv D \isin B$.
 614 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
 615 So $D \isin C \equiv D \isin \baseof{B}$.
 616
 617 $\qed$
 618
 619 \subsection{Base Acyclic}
 620
 621 Not applicable.
 622
 623 \subsection{Coherence and Patch Inclusion}
 624
 625 $$
 626 \begin{cases}
 627   \p = \pq    \lor B \haspatch \p : & C \haspatch \p \\
 628   \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
 629 \end{cases}
 630 $$
 631
 632 \proofstarts
 633 ~ Consider some $D \in \py$.
 634
 635 \subsubsection{For $\p = \pq$:}
 636
 637 By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
 638 By No Sneak, $D \le B \equiv D = C$.  Thus $C \haspatch \pq$.
 639
 640 \subsubsection{For $\p \neq \pq$:}
 641
 642 $D \neq C$.  So $D \isin C \equiv D \isin B$,
 643 and $D \le C \equiv D \le B$.
 644
 645 $\qed$
 646
 647 \subsection{Foreign Inclusion}
 648
 649 Simple Foreign Inclusion applies.  $\qed$
 650
 651 \subsection{Foreign Contents}
 652
 653 Not applicable.
 654
 655 \section{Anticommit}
 656
 657 Given $L$ and $\pr$ as represented by $R^+, R^-$.
 658 Construct $C$ which has $\pr$ removed.
 659 Used for removing a branch dependency.
 660 \gathbegin
 661  C \hasparents \{ L \}
 662 \gathnext
 663  \patchof{C} = \patchof{L}
 664 \gathnext
 665  \mergeof{C}{L}{R^+}{R^-}
 666 \end{gather}
 667
 668 \subsection{Conditions}
 669
 670 \[ \eqn{ Ingredients }{
 671 R^+ \in \pry \land R^- = \baseof{R^+}
 672 }\]
 673 \[ \eqn{ Into Base }{
 674  L \in \pn
 675 }\]
 676 \[ \eqn{ Unique Tip }{
 677  \pendsof{L}{\pry} = \{ R^+ \}
 678 }\]
 679 \[ \eqn{ Currently Included }{
 680  L \haspatch \pry
 681 }\]
 682
 683 \subsection{Ordering of Ingredients:}
 684
 685 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 686 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
 687 $\qed$
 688
 689 (Note that $R^+ \not\le R^-$, i.e. the merge base
 690 is a descendant, not an ancestor, of the 2nd parent.)
 691
 692 \subsection{No Replay}
 693
 694 By definition of $\merge$,
 695 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
 696 So, by Ordering of Ingredients,
 697 Ingredients Prevent Replay applies.  $\qed$
 698
 699 \subsection{Desired Contents}
 700
 701 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 702 \proofstarts
 703
 704 \subsubsection{For $D = C$:}
 705
 706 Trivially $D \isin C$.  OK.
 707
 708 \subsubsection{For $D \neq C, D \not\le L$:}
 709
 710 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 711 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 712
 713 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 714
 715 By Currently Included, $D \isin L$.
 716
 717 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 718 by Unique Tip, $D \le R^+ \equiv D \le L$.
 719 So $D \isin R^+$.
 720
 721 By Base Acyclic, $D \not\isin R^-$.
 722
 723 Apply $\merge$: $D \not\isin C$.  OK.
 724
 725 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 726
 727 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 728
 729 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 730
 731 $\qed$
 732
 733 \subsection{Unique Base}
 734
 735 Into Base means that $C \in \pn$, so Unique Base is not
 736 applicable. $\qed$
 737
 738 \subsection{Tip Contents}
 739
 740 Again, not applicable. $\qed$
 741
 742 \subsection{Base Acyclic}
 743
 744 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
 745 And by Into Base $C \not\in \py$.
 746 Now from Desired Contents, above, $D \isin C
 747 \implies D \isin L \lor D = C$, which thus
 748 $\implies D \not\in \py$.  $\qed$.
 749
 750 \subsection{Coherence and Patch Inclusion}
 751
 752 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
 753
 754 \subsubsection{For $\p = \pr$:}
 755 By Desired Contents, above, $D \not\isin C$.
 756 So $C \nothaspatch \pr$.
 757
 758 \subsubsection{For $\p \neq \pr$:}
 759 By Desired Contents, $D \isin C \equiv D \isin L$
 760 (since $D \in \py$ so $D \not\in \pry$).
 761
 762 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
 763 So $L \nothaspatch \p \implies C \nothaspatch \p$.
 764
 765 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
 766 so $L \haspatch \p \implies C \haspatch \p$.
 767
 768 $\qed$
 769
 770 \subsection{Foreign Inclusion}
 771
 772 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
 773 So by Desired Contents $D \isin C \equiv D \isin L$.
 774 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 775
 776 And $D \le C \equiv D \le L$.
 777 Thus $D \isin C \equiv D \le C$.
 778
 779 $\qed$
 780
 781 \subsection{Foreign Contents}
 782
 783 Not applicable.
 784
 785 \section{Merge}
 786
 787 Merge commits $L$ and $R$ using merge base $M$:
 788 \gathbegin
 789  C \hasparents \{ L, R \}
 790 \gathnext
 791  \patchof{C} = \patchof{L}
 792 \gathnext
 793  \mergeof{C}{L}{M}{R}
 794 \end{gather}
 795 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 796
 797 \subsection{Conditions}
 798 \[ \eqn{ Ingredients }{
 799  M \le L, M \le R
 800 }\]
 801 \[ \eqn{ Tip Merge }{
 802  L \in \py \implies
 803    \begin{cases}
 804       R \in \py : & \baseof{R} \ge \baseof{L}
 805               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 806       R \in \pn : & M = \baseof{L} \\
 807       \text{otherwise} : & \false
 808    \end{cases}
 809 }\]
 810 \[ \eqn{ Merge Acyclic }{
 811     L \in \pn
 812    \implies
 813     R \nothaspatch \p
 814 }\]
 815 \[ \eqn{ Removal Merge Ends }{
 816     X \not\haspatch \p \land
 817     Y \haspatch \p \land
 818     M \haspatch \p
 819   \implies
 820     \pendsof{Y}{\py} = \pendsof{M}{\py}
 821 }\]
 822 \[ \eqn{ Addition Merge Ends }{
 823     X \not\haspatch \p \land
 824     Y \haspatch \p \land
 825     M \nothaspatch \p
 826    \implies \left[
 827     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 828    \right]
 829 }\]
 830 \[ \eqn{ Foreign Merges }{
 831     \patchof{L} = \bot \equiv \patchof{R} = \bot
 832 }\]
 833
 834 \subsection{Non-Topbloke merges}
 835
 836 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
 837 (Foreign Merges, above).
 838 I.e. not only is it forbidden to merge into a Topbloke-controlled
 839 branch without Topbloke's assistance, it is also forbidden to
 840 merge any Topbloke-controlled branch into any plain git branch.
 841
 842 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 843 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 844 Merge Ends condition applies.
 845
 846 So a plain git merge of non-Topbloke branches meets the conditions and
 847 is therefore consistent with our scheme.
 848
 849 \subsection{No Replay}
 850
 851 By definition of $\merge$,
 852 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
 853 So, by Ingredients,
 854 Ingredients Prevent Replay applies.  $\qed$
 855
 856 \subsection{Unique Base}
 857
 858 Need to consider only $C \in \py$, ie $L \in \py$,
 859 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 860 putative ancestor $A \in \pn$ and see whether $A \le C$.
 861
 862 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 863 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 864 Thus $A \le C \equiv A \le L \lor A \le R$.
 865
 866 By Unique Base of L and Transitive Ancestors,
 867 $A \le L \equiv A \le \baseof{L}$.
 868
 869 \subsubsection{For $R \in \py$:}
 870
 871 By Unique Base of $R$ and Transitive Ancestors,
 872 $A \le R \equiv A \le \baseof{R}$.
 873
 874 But by Tip Merge condition on $\baseof{R}$,
 875 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 876 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 877 Thus $A \le C \equiv A \le \baseof{R}$.
 878 That is, $\baseof{C} = \baseof{R}$.
 879
 880 \subsubsection{For $R \in \pn$:}
 881
 882 By Tip Merge condition on $R$ and since $M \le R$,
 883 $A \le \baseof{L} \implies A \le R$, so
 884 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 885 Thus $A \le C \equiv A \le R$.
 886 That is, $\baseof{C} = R$.
 887
 888 $\qed$
 889
 890 \subsection{Coherence and Patch Inclusion}
 891
 892 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 893 This involves considering $D \in \py$.
 894
 895 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 896 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 897 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 898 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 899
 900 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 901 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 902 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 903
 904 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 905
 906 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 907  \equiv D \isin L \lor D \isin R$.
 908 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 909
 910 Consider $D \neq C, D \isin X \land D \isin Y$:
 911 By $\merge$, $D \isin C$.  Also $D \le X$
 912 so $D \le C$.  OK for $C \haspatch \p$.
 913
 914 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 915 By $\merge$, $D \not\isin C$.
 916 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 917 OK for $C \haspatch \p$.
 918
 919 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 920 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 921 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 922 OK for $C \haspatch \p$.
 923
 924 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 925
 926 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 927
 928 $M \haspatch \p \implies C \nothaspatch \p$.
 929 $M \nothaspatch \p \implies C \haspatch \p$.
 930
 931 \proofstarts
 932
 933 One of the Merge Ends conditions applies.
 934 Recall that we are considering $D \in \py$.
 935 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 936 We will show for each of
 937 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 938 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 939
 940 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 941 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 942 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 943 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 944
 945 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 946 $D \le Y$ so $D \le C$.
 947 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 948
 949 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 950 $D \not\le Y$.  If $D \le X$ then
 951 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 952 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 953 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 954
 955 Consider $D \neq C, M \haspatch P, D \isin Y$:
 956 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 957 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 958 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 959
 960 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 961 By $\merge$, $D \not\isin C$.  OK.
 962
 963 $\qed$
 964
 965 \subsection{Base Acyclic}
 966
 967 This applies when $C \in \pn$.
 968 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 969
 970 Consider some $D \in \py$.
 971
 972 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 973 R$.  And $D \neq C$.  So $D \not\isin C$.
 974
 975 $\qed$
 976
 977 \subsection{Tip Contents}
 978
 979 We need worry only about $C \in \py$.
 980 And $\patchof{C} = \patchof{L}$
 981 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 982 of $C$, and its Coherence and Patch Inclusion, as just proved.
 983
 984 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 985 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 986 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 987 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 988 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 989
 990 We will consider an arbitrary commit $D$
 991 and prove the Exclusive Tip Contents form.
 992
 993 \subsubsection{For $D \in \py$:}
 994 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 995 \le C$.  OK.
 996
 997 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 998
 999 $D \neq C$.  By Tip Contents of $L$,
1000 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
1001 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
1002 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
1003 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
1004
1005 \subsubsection{For $D \not\in \py, R \in \py$:}
1006
1007 $D \neq C$.
1008
1009 By Tip Contents
1010 $D \isin L \equiv D \isin \baseof{L}$ and
1011 $D \isin R \equiv D \isin \baseof{R}$.
1012
1013 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
1014 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
1015 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
1016 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
1017
1018 So $D \isin M \equiv D \isin L$ and by $\merge$,
1019 $D \isin C \equiv D \isin R$.  But from Unique Base,
1020 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
1021
1022 $\qed$
1023
1024 \subsection{Foreign Inclusion}
1025
1026 Consider some $D$ s.t. $\patchof{D} = \bot$.
1027 By Foreign Inclusion of $L, M, R$:
1028 $D \isin L \equiv D \le L$;
1029 $D \isin M \equiv D \le M$;
1030 $D \isin R \equiv D \le R$.
1031
1032 \subsubsection{For $D = C$:}
1033
1034 $D \isin C$ and $D \le C$.  OK.
1035
1036 \subsubsection{For $D \neq C, D \isin M$:}
1037
1038 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
1039 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
1040
1041 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
1042
1043 By $\merge$, $D \isin C$.
1044 And $D \isin X$ means $D \le X$ so $D \le C$.
1045 OK.
1046
1047 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
1048
1049 By $\merge$, $D \not\isin C$.
1050 And $D \not\le L, D \not\le R$ so $D \not\le C$.
1051 OK
1052
1053 $\qed$
1054
1055 \subsection{Foreign Contents}
1056
1057 Only relevant if $\patchof{L} = \bot$, in which case
1058 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
1059 so Totally Foreign Contents applies.  $\qed$
1060
1061 \end{document}