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 \renewcommand{\ge}{\geqslant}
  12 \renewcommand{\le}{\leqslant}
  13 \newcommand{\nge}{\ngeqslant}
  14 \newcommand{\nle}{\nleqslant}
  15
  16 \newcommand{\has}{\sqsupseteq}
  17 \newcommand{\isin}{\sqsubseteq}
  18
  19 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
  20 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
  21 \newcommand{\haspatch}{\sqSupset}
  22 \newcommand{\patchisin}{\sqSubset}
  23
  24         \newif\ifhidehack\hidehackfalse
  25         \DeclareRobustCommand\hidefromedef[2]{%
  26           \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
  27         \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
  28
  29 \newcommand{\set}[1]{\mathbb{#1}}
  30 \newcommand{\pay}[1]{\pa{#1}^+}
  31 \newcommand{\pan}[1]{\pa{#1}^-}
  32
  33 \newcommand{\p}{\pa{P}}
  34 \newcommand{\py}{\pay{P}}
  35 \newcommand{\pn}{\pan{P}}
  36
  37 \newcommand{\pr}{\pa{R}}
  38 \newcommand{\pry}{\pay{R}}
  39 \newcommand{\prn}{\pan{R}}
  40
  41 %\newcommand{\hasparents}{\underaccent{1}{>}}
  42 %\newcommand{\hasparents}{{%
  43 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
  44 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
  45 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
  46
  47 \renewcommand{\implies}{\Rightarrow}
  48 \renewcommand{\equiv}{\Leftrightarrow}
  49 \renewcommand{\nequiv}{\nLeftrightarrow}
  50 \renewcommand{\land}{\wedge}
  51 \renewcommand{\lor}{\vee}
  52
  53 \newcommand{\pancs}{{\mathcal A}}
  54 \newcommand{\pends}{{\mathcal E}}
  55
  56 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
  57 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
  58
  59 \newcommand{\merge}{{\mathcal M}}
  60 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
  61 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
  62
  63 \newcommand{\patch}{{\mathcal P}}
  64 \newcommand{\base}{{\mathcal B}}
  65
  66 \newcommand{\patchof}[1]{\patch ( #1 ) }
  67 \newcommand{\baseof}[1]{\base ( #1 ) }
  68
  69 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
  70 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
  71
  72 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
  73 \newcommand{\bigforall}{%
  74   \mathop{\mathchoice%
  75     {\hbox{\huge$\forall$}}%
  76     {\hbox{\Large$\forall$}}%
  77     {\hbox{\normalsize$\forall$}}%
  78     {\hbox{\scriptsize$\forall$}}}%
  79 }
  80
  81 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
  82 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
  83
  84 \newcommand{\qed}{\square}
  85 \newcommand{\proofstarts}{{\it Proof:}}
  86 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
  87
  88 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
  89 \newcommand{\gathnext}{\\ \tag*{}}
  90
  91 \newcommand{\true}{t}
  92 \newcommand{\false}{f}
  93
  94 \begin{document}
  95
  96 \section{Notation}
  97
  98 xxx make all conditions be in conditions, not in (or also in) intro
  99
 100 \begin{basedescript}{
 101 \desclabelwidth{5em}
 102 \desclabelstyle{\nextlinelabel}
 103 }
 104 \item[ $ C \hasparents \set X $ ]
 105 The parents of commit $C$ are exactly the set
 106 $\set X$.
 107
 108 \item[ $ C \ge D $ ]
 109 $C$ is a descendant of $D$ in the git commit
 110 graph.  This is a partial order, namely the transitive closure of
 111 $ D \in \set X $ where $ C \hasparents \set X $.
 112
 113 \item[ $ C \has D $ ]
 114 Informally, the tree at commit $C$ contains the change
 115 made in commit $D$.  Does not take account of deliberate reversions by
 116 the user or reversion, rebasing or rewinding in
 117 non-Topbloke-controlled branches.  For merges and Topbloke-generated
 118 anticommits or re-commits, the ``change made'' is only to be thought
 119 of as any conflict resolution.  This is not a partial order because it
 120 is not transitive.
 121
 122 \item[ $ \p, \py, \pn $ ]
 123 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
 124 are respectively the base and tip git branches.  $\p$ may be used
 125 where the context requires a set, in which case the statement
 126 is to be taken as applying to both $\py$ and $\pn$.
 127 None of these sets overlap.  Hence:
 128
 129 \item[ $ \patchof{ C } $ ]
 130 Either $\p$ s.t. $ C \in \p $, or $\bot$.
 131 A function from commits to patches' sets $\p$.
 132
 133 \item[ $ \pancsof{C}{\set P} $ ]
 134 $ \{ A \; | \; A \le C \land A \in \set P \} $
 135 i.e. all the ancestors of $C$
 136 which are in $\set P$.
 137
 138 \item[ $ \pendsof{C}{\set P} $ ]
 139 $ \{ E \; | \; E \in \pancsof{C}{\set P}
 140   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
 141   E \neq A \land E \le A \} $
 142 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
 143
 144 \item[ $ \baseof{C} $ ]
 145 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
 146 A partial function from commits to commits.
 147 See Unique Base, below.
 148
 149 \item[ $ C \haspatch \p $ ]
 150 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
 151 ~ Informally, $C$ has the contents of $\p$.
 152
 153 \item[ $ C \nothaspatch \p $ ]
 154 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
 155 ~ Informally, $C$ has none of the contents of $\p$.
 156
 157 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$.  This
 158 includes commits on plain git branches made by applying a Topbloke
 159 patch.  If a Topbloke
 160 patch is applied to a non-Topbloke branch and then bubbles back to
 161 the relevant Topbloke branches, we hope that
 162 if the user still cares about the Topbloke patch,
 163 git's merge algorithm will DTRT when trying to re-apply the changes.
 164
 165 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
 166 The contents of a git merge result:
 167
 168 $\displaystyle D \isin C \equiv
 169   \begin{cases}
 170     (D \isin L \land D \isin R) \lor D = C : & \true \\
 171     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
 172     \text{otherwise} : & D \not\isin M
 173   \end{cases}
 174 $
 175
 176 \end{basedescript}
 177 \newpage
 178 \section{Invariants}
 179
 180 We maintain these each time we construct a new commit. \\
 181 \[ \eqn{No Replay:}{
 182   C \has D \implies C \ge D
 183 }\]
 184 \[\eqn{Unique Base:}{
 185  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
 186 }\]
 187 \[\eqn{Tip Contents:}{
 188   \bigforall_{C \in \py} D \isin C \equiv
 189     { D \isin \baseof{C} \lor \atop
 190       (D \in \py \land D \le C) }
 191 }\]
 192 \[\eqn{Base Acyclic:}{
 193   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
 194 }\]
 195 \[\eqn{Coherence:}{
 196   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
 197 }\]
 198 \[\eqn{Foreign Inclusion:}{
 199   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
 200 }\]
 201
 202 \section{Some lemmas}
 203
 204 \[ \eqn{Alternative (overlapping) formulations defining
 205   $\mergeof{C}{L}{M}{R}$:}{
 206  D \isin C \equiv
 207   \begin{cases}
 208     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
 209     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
 210     D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
 211     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
 212     \text{as above with L and R exchanged}
 213   \end{cases}
 214 }\]
 215 \proof{
 216   Truth table xxx
 217
 218   Original definition is symmetrical in $L$ and $R$.
 219 }
 220
 221 \[ \eqn{Exclusive Tip Contents:}{
 222   \bigforall_{C \in \py}
 223     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
 224       \Bigr]
 225 }\]
 226 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 227
 228 \proof{
 229 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
 230 So by Base Acyclic $D \isin B \implies D \notin \py$.
 231 }
 232 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
 233   \bigforall_{C \in \py} D \isin C \equiv
 234   \begin{cases}
 235     D \in \py : & D \le C \\
 236     D \not\in \py : & D \isin \baseof{C}
 237   \end{cases}
 238 }\]
 239
 240 \[ \eqn{Tip Self Inpatch:}{
 241   \bigforall_{C \in \py} C \haspatch \p
 242 }\]
 243 Ie, tip commits contain their own patch.
 244
 245 \proof{
 246 Apply Exclusive Tip Contents to some $D \in \py$:
 247 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
 248   D \isin C \equiv D \le C $
 249 }
 250
 251 \[ \eqn{Exact Ancestors:}{
 252   \bigforall_{ C \hasparents \set{R} }
 253   D \le C \equiv
 254     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
 255     \lor D = C
 256 }\]
 257
 258 \[ \eqn{Transitive Ancestors:}{
 259   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
 260   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
 261 }\]
 262
 263 \proof{
 264 The implication from right to left is trivial because
 265 $ \pends() \subset \pancs() $.
 266 For the implication from left to right:
 267 by the definition of $\mathcal E$,
 268 for every such $A$, either $A \in \pends()$ which implies
 269 $A \le M$ by the LHS directly,
 270 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
 271 in which case we repeat for $A'$.  Since there are finitely many
 272 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 273 by the LHS.  And $A \le A''$.
 274 }
 275 \[ \eqn{Calculation Of Ends:}{
 276   \bigforall_{C \hasparents \set A}
 277     \pendsof{C}{\set P} =
 278        \left\{ E \Big|
 279            \Bigl[ \Largeexists_{A \in \set A}
 280                        E \in \pendsof{A}{\set P} \Bigr] \land
 281            \Bigl[ \Largenexists_{B \in \set A}
 282                        E \neq B \land E \le B \Bigr]
 283        \right\}
 284 }\]
 285 XXX proof TBD.
 286
 287 \subsection{No Replay for Merge Results}
 288
 289 If we are constructing $C$, with,
 290 \gathbegin
 291   \mergeof{C}{L}{M}{R}
 292 \gathnext
 293   L \le C
 294 \gathnext
 295   R \le C
 296 \end{gather}
 297 No Replay is preserved.  \proofstarts
 298
 299 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 300
 301 \subsubsection{For $D \isin L \land D \isin R$:}
 302 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
 303
 304 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 305 $D \not\isin C$.  OK.
 306
 307 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 308  \land D \not\isin M$:}
 309 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
 310 R$ so $D \le C$.  OK.
 311
 312 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 313  \land D \isin M$:}
 314 $D \not\isin C$.  OK.
 315
 316 $\qed$
 317
 318 \section{Commit annotation}
 319
 320 xxx need to compute annotation for every commit type
 321
 322 We annotate each Topbloke commit $C$ with:
 323 \gathbegin
 324  \patchof{C}
 325 \gathnext
 326  \baseof{C}, \text{ if } C \in \py
 327 \gathnext
 328  \bigforall_{\pa{Q}}
 329    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
 330 \gathnext
 331  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 332 \end{gather}
 333
 334 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 335 make it wrong to make plain commits with git because the recorded $\pends$
 336 would have to be updated.  The annotation is not needed because
 337 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 338
 339 \section{Simple commit}
 340
 341 A simple single-parent forward commit $C$ as made by git-commit.
 342 \begin{gather}
 343 \tag*{} C \hasparents \{ A \} \\
 344 \tag*{} \patchof{C} = \patchof{A} \\
 345 \tag*{} D \isin C \equiv D \isin A \lor D = C
 346 \end{gather}
 347 This also covers Topbloke-generated commits on plain git branches:
 348 Topbloke strips the metadata when exporting.
 349
 350 \subsection{No Replay}
 351 Trivial.
 352
 353 \subsection{Unique Base}
 354 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
 355
 356 \subsection{Tip Contents}
 357 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 358 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 359 Substitute into the contents of $C$:
 360 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 361     \lor D = C \]
 362 Since $D = C \implies D \in \py$,
 363 and substituting in $\baseof{C}$, this gives:
 364 \[ D \isin C \equiv D \isin \baseof{C} \lor
 365     (D \in \py \land D \le A) \lor
 366     (D = C \land D \in \py) \]
 367 \[ \equiv D \isin \baseof{C} \lor
 368    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 369 So by Exact Ancestors:
 370 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 371 ) \]
 372 $\qed$
 373
 374 \subsection{Base Acyclic}
 375
 376 Need to consider only $A, C \in \pn$.
 377
 378 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 379
 380 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 381 $A$, $D \isin C \implies D \not\in \py$. $\qed$
 382
 383 \subsection{Coherence and patch inclusion}
 384
 385 Need to consider $D \in \py$
 386
 387 \subsubsection{For $A \haspatch P, D = C$:}
 388
 389 Ancestors of $C$:
 390 $ D \le C $.
 391
 392 Contents of $C$:
 393 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 394
 395 \subsubsection{For $A \haspatch P, D \neq C$:}
 396 Ancestors: $ D \le C \equiv D \le A $.
 397
 398 Contents: $ D \isin C \equiv D \isin A \lor f $
 399 so $ D \isin C \equiv D \isin A $.
 400
 401 So:
 402 \[ A \haspatch P \implies C \haspatch P \]
 403
 404 \subsubsection{For $A \nothaspatch P$:}
 405
 406 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 407 Thus $D \neq C$.
 408
 409 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 410
 411 So:
 412 \[ A \nothaspatch P \implies C \nothaspatch P \]
 413 $\qed$
 414
 415 \subsection{Foreign inclusion:}
 416
 417 If $D = C$, trivial.  For $D \neq C$:
 418 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 419
 420 \section{Anticommit}
 421
 422 Given $L, R^+, R^-$ where
 423 $R^+ \in \pry, R^- = \baseof{R^+}$.
 424 Construct $C$ which has $\pr$ removed.
 425 Used for removing a branch dependency.
 426 \gathbegin
 427  C \hasparents \{ L \}
 428 \gathnext
 429  \patchof{C} = \patchof{L}
 430 \gathnext
 431  \mergeof{C}{L}{R^+}{R^-}
 432 \end{gather}
 433
 434 \subsection{Conditions}
 435
 436 \[ \eqn{ Into Base }{
 437  L \in \pn
 438 }\]
 439 \[ \eqn{ Unique Tip }{
 440  \pendsof{L}{\pry} = \{ R^+ \}
 441 }\]
 442 \[ \eqn{ Currently Included }{
 443  L \haspatch \pry
 444 }\]
 445
 446 \subsection{Ordering of ${L, R^+, R^-}$:}
 447
 448 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 449 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
 450
 451 (Note that the merge base $R^+ \not\le R^-$, i.e. the merge base is
 452 later than one of the branches to be merged.)
 453
 454 \subsection{No Replay}
 455
 456 No Replay for Merge Results applies.  $\qed$
 457
 458 \subsection{Desired Contents}
 459
 460 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 461 \proofstarts
 462
 463 \subsubsection{For $D = C$:}
 464
 465 Trivially $D \isin C$.  OK.
 466
 467 \subsubsection{For $D \neq C, D \not\le L$:}
 468
 469 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 470 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 471
 472 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 473
 474 By Currently Included, $D \isin L$.
 475
 476 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 477 by Unique Tip, $D \le R^+ \equiv D \le L$.
 478 So $D \isin R^+$.
 479
 480 By Base Acyclic, $D \not\isin R^-$.
 481
 482 Apply $\merge$: $D \not\isin C$.  OK.
 483
 484 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 485
 486 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 487
 488 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 489
 490 $\qed$
 491
 492 \subsection{Unique Base}
 493
 494 Into Base means that $C \in \pn$, so Unique Base is not
 495 applicable. $\qed$
 496
 497 \subsection{Tip Contents}
 498
 499 Again, not applicable. $\qed$
 500
 501 \subsection{Base Acyclic}
 502
 503 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
 504 And by Into Base $C \not\in \py$.
 505 Now from Desired Contents, above, $D \isin C
 506 \implies D \isin L \lor D = C$, which thus
 507 $\implies D \not\in \py$.  $\qed$.
 508
 509 \subsection{Coherence and Patch Inclusion}
 510
 511 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
 512
 513 \subsubsection{For $\p = \pr$:}
 514 By Desired Contents, above, $D \not\isin C$.
 515 So $C \nothaspatch \pr$.
 516
 517 \subsubsection{For $\p \neq \pr$:}
 518 By Desired Contents, $D \isin C \equiv D \isin L$
 519 (since $D \in \py$ so $D \not\in \pry$).
 520
 521 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
 522 So $L \nothaspatch \p \implies C \nothaspatch \p$.
 523
 524 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
 525 so $L \haspatch \p \implies C \haspatch \p$.
 526
 527 \section{Foreign Inclusion}
 528
 529 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
 530 So by Desired Contents $D \isin C \equiv D \isin L$.
 531 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 532
 533 And $D \le C \equiv D \le L$.
 534 Thus $D \isin C \equiv D \le C$.  $\qed$
 535
 536 \section{Merge}
 537
 538 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 539 \gathbegin
 540  C \hasparents \{ L, R \}
 541 \gathnext
 542  \patchof{C} = \patchof{L}
 543 \gathnext
 544  \mergeof{C}{L}{M}{R}
 545 \end{gather}
 546 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 547
 548 \subsection{Conditions}
 549
 550 \[ \eqn{ Tip Merge }{
 551  L \in \py \implies
 552    \begin{cases}
 553       R \in \py : & \baseof{R} \ge \baseof{L}
 554               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 555       R \in \pn : & M = \baseof{L} \\
 556       \text{otherwise} : & \false
 557    \end{cases}
 558 }\]
 559 \[ \eqn{ Merge Acyclic }{
 560     L \in \pn
 561    \implies
 562     R \nothaspatch \p
 563 }\]
 564 \[ \eqn{ Removal Merge Ends }{
 565     X \not\haspatch \p \land
 566     Y \haspatch \p \land
 567     M \haspatch \p
 568   \implies
 569     \pendsof{Y}{\py} = \pendsof{M}{\py}
 570 }\]
 571 \[ \eqn{ Addition Merge Ends }{
 572     X \not\haspatch \p \land
 573     Y \haspatch \p \land
 574     M \nothaspatch \p
 575    \implies \left[
 576     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 577    \right]
 578 }\]
 579
 580 \subsection{Non-Topbloke merges}
 581
 582 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
 583 I.e. not only is it forbidden to merge into a Topbloke-controlled
 584 branch without Topbloke's assistance, it is also forbidden to
 585 merge any Topbloke-controlled branch into any plain git branch.
 586
 587 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 588 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 589 Merge Ends condition applies.  Good.
 590
 591 \subsection{No Replay}
 592
 593 No Replay for Merge Results applies.  $\qed$
 594
 595 \subsection{Unique Base}
 596
 597 Need to consider only $C \in \py$, ie $L \in \py$,
 598 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 599 putative ancestor $A \in \pn$ and see whether $A \le C$.
 600
 601 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 602 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 603 Thus $A \le C \equiv A \le L \lor A \le R$.
 604
 605 By Unique Base of L and Transitive Ancestors,
 606 $A \le L \equiv A \le \baseof{L}$.
 607
 608 \subsubsection{For $R \in \py$:}
 609
 610 By Unique Base of $R$ and Transitive Ancestors,
 611 $A \le R \equiv A \le \baseof{R}$.
 612
 613 But by Tip Merge condition on $\baseof{R}$,
 614 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 615 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 616 Thus $A \le C \equiv A \le \baseof{R}$.
 617 That is, $\baseof{C} = \baseof{R}$.
 618
 619 \subsubsection{For $R \in \pn$:}
 620
 621 By Tip Merge condition on $R$ and since $M \le R$,
 622 $A \le \baseof{L} \implies A \le R$, so
 623 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 624 Thus $A \le C \equiv A \le R$.
 625 That is, $\baseof{C} = R$.
 626
 627 $\qed$
 628
 629 \subsection{Coherence and Patch Inclusion}
 630
 631 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 632 This involves considering $D \in \py$.
 633
 634 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 635 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 636 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 637 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 638
 639 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 640 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 641 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 642
 643 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 644
 645 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 646  \equiv D \isin L \lor D \isin R$.
 647 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 648
 649 Consider $D \neq C, D \isin X \land D \isin Y$:
 650 By $\merge$, $D \isin C$.  Also $D \le X$
 651 so $D \le C$.  OK for $C \haspatch \p$.
 652
 653 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 654 By $\merge$, $D \not\isin C$.
 655 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 656 OK for $C \haspatch \p$.
 657
 658 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 659 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 660 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 661 OK for $C \haspatch \p$.
 662
 663 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 664
 665 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 666
 667 $M \haspatch \p \implies C \nothaspatch \p$.
 668 $M \nothaspatch \p \implies C \haspatch \p$.
 669
 670 \proofstarts
 671
 672 One of the Merge Ends conditions applies.
 673 Recall that we are considering $D \in \py$.
 674 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 675 We will show for each of
 676 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 677 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 678
 679 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 680 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 681 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 682 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 683
 684 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 685 $D \le Y$ so $D \le C$.
 686 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 687
 688 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 689 $D \not\le Y$.  If $D \le X$ then
 690 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 691 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 692 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 693
 694 Consider $D \neq C, M \haspatch P, D \isin Y$:
 695 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 696 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 697 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 698
 699 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 700 By $\merge$, $D \not\isin C$.  OK.
 701
 702 $\qed$
 703
 704 \subsection{Base Acyclic}
 705
 706 This applies when $C \in \pn$.
 707 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 708
 709 Consider some $D \in \py$.
 710
 711 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 712 R$.  And $D \neq C$.  So $D \not\isin C$.  $\qed$
 713
 714 \subsection{Tip Contents}
 715
 716 We need worry only about $C \in \py$.
 717 And $\patchof{C} = \patchof{L}$
 718 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 719 of $C$, and its Coherence and Patch Inclusion, as just proved.
 720
 721 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 722 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 723 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 724 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 725 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 726
 727 We will consider an arbitrary commit $D$
 728 and prove the Exclusive Tip Contents form.
 729
 730 \subsubsection{For $D \in \py$:}
 731 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 732 \le C$.  OK.
 733
 734 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 735
 736 $D \neq C$.  By Tip Contents of $L$,
 737 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
 738 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
 739 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
 740 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
 741
 742 \subsubsection{For $D \not\in \py, R \in \py$:}
 743
 744 $D \neq C$.
 745
 746 By Tip Contents
 747 $D \isin L \equiv D \isin \baseof{L}$ and
 748 $D \isin R \equiv D \isin \baseof{R}$.
 749
 750 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
 751 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
 752 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
 753 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
 754
 755 So $D \isin M \equiv D \isin L$ and by $\merge$,
 756 $D \isin C \equiv D \isin R$.  But from Unique Base,
 757 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
 758
 759 $\qed$
 760
 761 \subsection{Foreign Inclusion}
 762
 763 Consider some $D$ s.t. $\patchof{D} = \bot$.
 764 By Foreign Inclusion of $L, M, R$:
 765 $D \isin L \equiv D \le L$;
 766 $D \isin M \equiv D \le M$;
 767 $D \isin R \equiv D \le R$.
 768
 769 \subsubsection{For $D = C$:}
 770
 771 $D \isin C$ and $D \le C$.  OK.
 772
 773 \subsubsection{For $D \neq C, D \isin M$:}
 774
 775 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
 776 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
 777
 778 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
 779
 780 By $\merge$, $D \isin C$.
 781 And $D \isin X$ means $D \le X$ so $D \le C$.
 782 OK.
 783
 784 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
 785
 786 By $\merge$, $D \not\isin C$.
 787 And $D \not\le L, D \not\le R$ so $D \not\le C$.
 788 OK
 789
 790 $\qed$
 791
 792 \end{document}