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