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