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$.
 403
 404 $\qed$
 405
 406 \subsection{Coherence and patch inclusion}
 407
 408 Need to consider $D \in \py$
 409
 410 \subsubsection{For $A \haspatch P, D = C$:}
 411
 412 Ancestors of $C$:
 413 $ D \le C $.
 414
 415 Contents of $C$:
 416 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 417
 418 \subsubsection{For $A \haspatch P, D \neq C$:}
 419 Ancestors: $ D \le C \equiv D \le A $.
 420
 421 Contents: $ D \isin C \equiv D \isin A \lor f $
 422 so $ D \isin C \equiv D \isin A $.
 423
 424 So:
 425 \[ A \haspatch P \implies C \haspatch P \]
 426
 427 \subsubsection{For $A \nothaspatch P$:}
 428
 429 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 430 Thus $D \neq C$.
 431
 432 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 433
 434 So:
 435 \[ A \nothaspatch P \implies C \nothaspatch P \]
 436 $\qed$
 437
 438 \subsection{Foreign inclusion:}
 439
 440 If $D = C$, trivial.  For $D \neq C$:
 441 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 442
 443 \section{Create Base}
 444
 445 xxx tbd
 446
 447 \section{Create Tip}
 448
 449 xxx tbd\
 450
 451 \section{Anticommit}
 452
 453 Given $L$ and $\pr$ as represented by $R^+, R^-$.
 454 Construct $C$ which has $\pr$ removed.
 455 Used for removing a branch dependency.
 456 \gathbegin
 457  C \hasparents \{ L \}
 458 \gathnext
 459  \patchof{C} = \patchof{L}
 460 \gathnext
 461  \mergeof{C}{L}{R^+}{R^-}
 462 \end{gather}
 463
 464 \subsection{Conditions}
 465
 466 \[ \eqn{ Ingredients }{
 467 R^+ \in \pry \land R^- = \baseof{R^+}
 468 }\]
 469 \[ \eqn{ Into Base }{
 470  L \in \pn
 471 }\]
 472 \[ \eqn{ Unique Tip }{
 473  \pendsof{L}{\pry} = \{ R^+ \}
 474 }\]
 475 \[ \eqn{ Currently Included }{
 476  L \haspatch \pry
 477 }\]
 478
 479 \subsection{Ordering of ${L, R^+, R^-}$:}
 480
 481 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 482 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
 483 $\qed$
 484
 485 (Note that $R^+ \not\le R^-$, i.e. the merge base
 486 is a descendant, not an ancestor, of the 2nd parent.)
 487
 488 \subsection{No Replay}
 489
 490 No Replay for Merge Results applies.  $\qed$
 491
 492 \subsection{Desired Contents}
 493
 494 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 495 \proofstarts
 496
 497 \subsubsection{For $D = C$:}
 498
 499 Trivially $D \isin C$.  OK.
 500
 501 \subsubsection{For $D \neq C, D \not\le L$:}
 502
 503 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 504 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 505
 506 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 507
 508 By Currently Included, $D \isin L$.
 509
 510 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 511 by Unique Tip, $D \le R^+ \equiv D \le L$.
 512 So $D \isin R^+$.
 513
 514 By Base Acyclic, $D \not\isin R^-$.
 515
 516 Apply $\merge$: $D \not\isin C$.  OK.
 517
 518 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 519
 520 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 521
 522 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 523
 524 $\qed$
 525
 526 \subsection{Unique Base}
 527
 528 Into Base means that $C \in \pn$, so Unique Base is not
 529 applicable. $\qed$
 530
 531 \subsection{Tip Contents}
 532
 533 Again, not applicable. $\qed$
 534
 535 \subsection{Base Acyclic}
 536
 537 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
 538 And by Into Base $C \not\in \py$.
 539 Now from Desired Contents, above, $D \isin C
 540 \implies D \isin L \lor D = C$, which thus
 541 $\implies D \not\in \py$.  $\qed$.
 542
 543 \subsection{Coherence and Patch Inclusion}
 544
 545 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
 546
 547 \subsubsection{For $\p = \pr$:}
 548 By Desired Contents, above, $D \not\isin C$.
 549 So $C \nothaspatch \pr$.
 550
 551 \subsubsection{For $\p \neq \pr$:}
 552 By Desired Contents, $D \isin C \equiv D \isin L$
 553 (since $D \in \py$ so $D \not\in \pry$).
 554
 555 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
 556 So $L \nothaspatch \p \implies C \nothaspatch \p$.
 557
 558 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
 559 so $L \haspatch \p \implies C \haspatch \p$.
 560
 561 $\qed$
 562
 563 \section{Foreign Inclusion}
 564
 565 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
 566 So by Desired Contents $D \isin C \equiv D \isin L$.
 567 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 568
 569 And $D \le C \equiv D \le L$.
 570 Thus $D \isin C \equiv D \le C$.
 571
 572 $\qed$
 573
 574 \section{Merge}
 575
 576 Merge commits $L$ and $R$ using merge base $M$:
 577 \gathbegin
 578  C \hasparents \{ L, R \}
 579 \gathnext
 580  \patchof{C} = \patchof{L}
 581 \gathnext
 582  \mergeof{C}{L}{M}{R}
 583 \end{gather}
 584 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 585
 586 \subsection{Conditions}
 587 \[ \eqn{ Ingredients }{
 588  M \le L, M \le R
 589 }\]
 590 \[ \eqn{ Tip Merge }{
 591  L \in \py \implies
 592    \begin{cases}
 593       R \in \py : & \baseof{R} \ge \baseof{L}
 594               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 595       R \in \pn : & M = \baseof{L} \\
 596       \text{otherwise} : & \false
 597    \end{cases}
 598 }\]
 599 \[ \eqn{ Merge Acyclic }{
 600     L \in \pn
 601    \implies
 602     R \nothaspatch \p
 603 }\]
 604 \[ \eqn{ Removal Merge Ends }{
 605     X \not\haspatch \p \land
 606     Y \haspatch \p \land
 607     M \haspatch \p
 608   \implies
 609     \pendsof{Y}{\py} = \pendsof{M}{\py}
 610 }\]
 611 \[ \eqn{ Addition Merge Ends }{
 612     X \not\haspatch \p \land
 613     Y \haspatch \p \land
 614     M \nothaspatch \p
 615    \implies \left[
 616     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 617    \right]
 618 }\]
 619
 620 \subsection{Non-Topbloke merges}
 621
 622 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
 623 I.e. not only is it forbidden to merge into a Topbloke-controlled
 624 branch without Topbloke's assistance, it is also forbidden to
 625 merge any Topbloke-controlled branch into any plain git branch.
 626
 627 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 628 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 629 Merge Ends condition applies.  Good.
 630
 631 \subsection{No Replay}
 632
 633 No Replay for Merge Results applies.  $\qed$
 634
 635 \subsection{Unique Base}
 636
 637 Need to consider only $C \in \py$, ie $L \in \py$,
 638 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 639 putative ancestor $A \in \pn$ and see whether $A \le C$.
 640
 641 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 642 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 643 Thus $A \le C \equiv A \le L \lor A \le R$.
 644
 645 By Unique Base of L and Transitive Ancestors,
 646 $A \le L \equiv A \le \baseof{L}$.
 647
 648 \subsubsection{For $R \in \py$:}
 649
 650 By Unique Base of $R$ and Transitive Ancestors,
 651 $A \le R \equiv A \le \baseof{R}$.
 652
 653 But by Tip Merge condition on $\baseof{R}$,
 654 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 655 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 656 Thus $A \le C \equiv A \le \baseof{R}$.
 657 That is, $\baseof{C} = \baseof{R}$.
 658
 659 \subsubsection{For $R \in \pn$:}
 660
 661 By Tip Merge condition on $R$ and since $M \le R$,
 662 $A \le \baseof{L} \implies A \le R$, so
 663 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 664 Thus $A \le C \equiv A \le R$.
 665 That is, $\baseof{C} = R$.
 666
 667 $\qed$
 668
 669 \subsection{Coherence and Patch Inclusion}
 670
 671 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 672 This involves considering $D \in \py$.
 673
 674 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 675 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 676 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 677 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 678
 679 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 680 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 681 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 682
 683 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 684
 685 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 686  \equiv D \isin L \lor D \isin R$.
 687 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 688
 689 Consider $D \neq C, D \isin X \land D \isin Y$:
 690 By $\merge$, $D \isin C$.  Also $D \le X$
 691 so $D \le C$.  OK for $C \haspatch \p$.
 692
 693 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 694 By $\merge$, $D \not\isin C$.
 695 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 696 OK for $C \haspatch \p$.
 697
 698 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 699 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 700 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 701 OK for $C \haspatch \p$.
 702
 703 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 704
 705 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 706
 707 $M \haspatch \p \implies C \nothaspatch \p$.
 708 $M \nothaspatch \p \implies C \haspatch \p$.
 709
 710 \proofstarts
 711
 712 One of the Merge Ends conditions applies.
 713 Recall that we are considering $D \in \py$.
 714 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 715 We will show for each of
 716 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 717 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 718
 719 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 720 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 721 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 722 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 723
 724 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 725 $D \le Y$ so $D \le C$.
 726 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 727
 728 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 729 $D \not\le Y$.  If $D \le X$ then
 730 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 731 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 732 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 733
 734 Consider $D \neq C, M \haspatch P, D \isin Y$:
 735 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 736 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 737 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 738
 739 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 740 By $\merge$, $D \not\isin C$.  OK.
 741
 742 $\qed$
 743
 744 \subsection{Base Acyclic}
 745
 746 This applies when $C \in \pn$.
 747 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 748
 749 Consider some $D \in \py$.
 750
 751 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 752 R$.  And $D \neq C$.  So $D \not\isin C$.
 753
 754 $\qed$
 755
 756 \subsection{Tip Contents}
 757
 758 We need worry only about $C \in \py$.
 759 And $\patchof{C} = \patchof{L}$
 760 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 761 of $C$, and its Coherence and Patch Inclusion, as just proved.
 762
 763 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 764 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 765 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 766 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 767 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 768
 769 We will consider an arbitrary commit $D$
 770 and prove the Exclusive Tip Contents form.
 771
 772 \subsubsection{For $D \in \py$:}
 773 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 774 \le C$.  OK.
 775
 776 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 777
 778 $D \neq C$.  By Tip Contents of $L$,
 779 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
 780 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
 781 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
 782 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
 783
 784 \subsubsection{For $D \not\in \py, R \in \py$:}
 785
 786 $D \neq C$.
 787
 788 By Tip Contents
 789 $D \isin L \equiv D \isin \baseof{L}$ and
 790 $D \isin R \equiv D \isin \baseof{R}$.
 791
 792 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
 793 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
 794 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
 795 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
 796
 797 So $D \isin M \equiv D \isin L$ and by $\merge$,
 798 $D \isin C \equiv D \isin R$.  But from Unique Base,
 799 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
 800
 801 $\qed$
 802
 803 \subsection{Foreign Inclusion}
 804
 805 Consider some $D$ s.t. $\patchof{D} = \bot$.
 806 By Foreign Inclusion of $L, M, R$:
 807 $D \isin L \equiv D \le L$;
 808 $D \isin M \equiv D \le M$;
 809 $D \isin R \equiv D \le R$.
 810
 811 \subsubsection{For $D = C$:}
 812
 813 $D \isin C$ and $D \le C$.  OK.
 814
 815 \subsubsection{For $D \neq C, D \isin M$:}
 816
 817 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
 818 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
 819
 820 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
 821
 822 By $\merge$, $D \isin C$.
 823 And $D \isin X$ means $D \le X$ so $D \le C$.
 824 OK.
 825
 826 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
 827
 828 By $\merge$, $D \not\isin C$.
 829 And $D \not\le L, D \not\le R$ so $D \not\le C$.
 830 OK
 831
 832 $\qed$
 833
 834 \end{document}