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 \[\eqn{Foreign Contents:}{
 200   \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
 201     D \le C \implies \patchof{D} = \bot
 202 }\]
 203
 204 \section{Some lemmas}
 205
 206 \[ \eqn{Alternative (overlapping) formulations defining
 207   $\mergeof{C}{L}{M}{R}$:}{
 208  D \isin C \equiv
 209   \begin{cases}
 210     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
 211     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
 212     D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
 213     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
 214     \text{as above with L and R exchanged}
 215   \end{cases}
 216 }\]
 217 \proof{
 218   Truth table xxx
 219
 220   Original definition is symmetrical in $L$ and $R$.
 221 }
 222
 223 \[ \eqn{Exclusive Tip Contents:}{
 224   \bigforall_{C \in \py}
 225     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
 226       \Bigr]
 227 }\]
 228 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 229
 230 \proof{
 231 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
 232 So by Base Acyclic $D \isin B \implies D \notin \py$.
 233 }
 234 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
 235   \bigforall_{C \in \py} D \isin C \equiv
 236   \begin{cases}
 237     D \in \py : & D \le C \\
 238     D \not\in \py : & D \isin \baseof{C}
 239   \end{cases}
 240 }\]
 241
 242 \[ \eqn{Tip Self Inpatch:}{
 243   \bigforall_{C \in \py} C \haspatch \p
 244 }\]
 245 Ie, tip commits contain their own patch.
 246
 247 \proof{
 248 Apply Exclusive Tip Contents to some $D \in \py$:
 249 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
 250   D \isin C \equiv D \le C $
 251 }
 252
 253 \[ \eqn{Exact Ancestors:}{
 254   \bigforall_{ C \hasparents \set{R} }
 255   D \le C \equiv
 256     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
 257     \lor D = C
 258 }\]
 259 xxx proof tbd
 260
 261 \[ \eqn{Transitive Ancestors:}{
 262   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
 263   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
 264 }\]
 265
 266 \proof{
 267 The implication from right to left is trivial because
 268 $ \pends() \subset \pancs() $.
 269 For the implication from left to right:
 270 by the definition of $\mathcal E$,
 271 for every such $A$, either $A \in \pends()$ which implies
 272 $A \le M$ by the LHS directly,
 273 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
 274 in which case we repeat for $A'$.  Since there are finitely many
 275 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 276 by the LHS.  And $A \le A''$.
 277 }
 278
 279 \[ \eqn{Calculation Of Ends:}{
 280   \bigforall_{C \hasparents \set A}
 281     \pendsof{C}{\set P} =
 282       \begin{cases}
 283        C \in \p : & \{ C \}
 284       \\
 285        C \not\in \p : & \displaystyle
 286        \left\{ E \Big|
 287            \Bigl[ \Largeexists_{A \in \set A}
 288                        E \in \pendsof{A}{\set P} \Bigr] \land
 289            \Bigl[ \Largenexists_{B \in \set A}
 290                        E \neq B \land E \le B \Bigr]
 291        \right\}
 292       \end{cases}
 293 }\]
 294 xxx proof tbd
 295
 296 \[ \eqn{Totally Foreign Contents:}{
 297   \bigforall_{C \hasparents \set A}
 298    \left[
 299     \patchof{C} = \bot \land
 300       \bigforall_{A \in \set A} \patchof{A} = \bot
 301    \right]
 302   \implies
 303    \left[
 304     D \isin C
 305    \implies
 306     \patchof{D} = \bot
 307    \right]
 308 }\]
 309 xxx proof tbd
 310
 311 \subsection{No Replay for Merge Results}
 312
 313 If we are constructing $C$, with,
 314 \gathbegin
 315   \mergeof{C}{L}{M}{R}
 316 \gathnext
 317   L \le C
 318 \gathnext
 319   R \le C
 320 \end{gather}
 321 No Replay is preserved.  \proofstarts
 322
 323 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 324
 325 \subsubsection{For $D \isin L \land D \isin R$:}
 326 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
 327
 328 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 329 $D \not\isin C$.  OK.
 330
 331 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 332  \land D \not\isin M$:}
 333 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
 334 R$ so $D \le C$.  OK.
 335
 336 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 337  \land D \isin M$:}
 338 $D \not\isin C$.  OK.
 339
 340 $\qed$
 341
 342 \section{Commit annotation}
 343
 344 We annotate each Topbloke commit $C$ with:
 345 \gathbegin
 346  \patchof{C}
 347 \gathnext
 348  \baseof{C}, \text{ if } C \in \py
 349 \gathnext
 350  \bigforall_{\pa{Q}}
 351    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
 352 \gathnext
 353  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 354 \end{gather}
 355
 356 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
 357 in the summary in the section for that kind of commit.
 358
 359 Whether $\baseof{C}$ is required, and if so what the value is, is
 360 stated in the proof of Unique Base for each kind of commit.
 361
 362 $C \haspatch \pa{Q}$ or $\nothaspatch \pa{Q}$ is represented as the
 363 set $\{ \pa{Q} | C \haspatch \pa{Q} \}$.  Whether $C \haspatch \pa{Q}$
 364 is in stated
 365 (in terms of $I \haspatch \pa{Q}$ or $I \nothaspatch \pa{Q}$
 366 for the ingredients $I$),
 367 in the proof of Coherence for each kind of commit.
 368
 369 $\pendsof{C}{\pa{Q}^+}$ is computed, for all Topbloke-generated commits,
 370 using the lemma Calculation of Ends, above.
 371 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 372 make it wrong to make plain commits with git because the recorded $\pends$
 373 would have to be updated.  The annotation is not needed in that case
 374 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 375
 376 \section{Simple commit}
 377
 378 A simple single-parent forward commit $C$ as made by git-commit.
 379 \begin{gather}
 380 \tag*{} C \hasparents \{ A \} \\
 381 \tag*{} \patchof{C} = \patchof{A} \\
 382 \tag*{} D \isin C \equiv D \isin A \lor D = C
 383 \end{gather}
 384 This also covers Topbloke-generated commits on plain git branches:
 385 Topbloke strips the metadata when exporting.
 386
 387 \subsection{No Replay}
 388 Trivial.
 389
 390 \subsection{Unique Base}
 391 If $A, C \in \py$ then by Calculation of Ends for
 392 $C, \py, C \not\in \py$:
 393 $\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
 394 $\baseof{C} = \baseof{A}$. $\qed$
 395
 396 \subsection{Tip Contents}
 397 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 398 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 399 Substitute into the contents of $C$:
 400 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 401     \lor D = C \]
 402 Since $D = C \implies D \in \py$,
 403 and substituting in $\baseof{C}$, this gives:
 404 \[ D \isin C \equiv D \isin \baseof{C} \lor
 405     (D \in \py \land D \le A) \lor
 406     (D = C \land D \in \py) \]
 407 \[ \equiv D \isin \baseof{C} \lor
 408    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 409 So by Exact Ancestors:
 410 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 411 ) \]
 412 $\qed$
 413
 414 \subsection{Base Acyclic}
 415
 416 Need to consider only $A, C \in \pn$.
 417
 418 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 419
 420 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 421 $A$, $D \isin C \implies D \not\in \py$.
 422
 423 $\qed$
 424
 425 \subsection{Coherence and patch inclusion}
 426
 427 Need to consider $D \in \py$
 428
 429 \subsubsection{For $A \haspatch P, D = C$:}
 430
 431 Ancestors of $C$:
 432 $ D \le C $.
 433
 434 Contents of $C$:
 435 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 436
 437 \subsubsection{For $A \haspatch P, D \neq C$:}
 438 Ancestors: $ D \le C \equiv D \le A $.
 439
 440 Contents: $ D \isin C \equiv D \isin A \lor f $
 441 so $ D \isin C \equiv D \isin A $.
 442
 443 So:
 444 \[ A \haspatch P \implies C \haspatch P \]
 445
 446 \subsubsection{For $A \nothaspatch P$:}
 447
 448 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 449 Thus $D \neq C$.
 450
 451 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 452
 453 So:
 454 \[ A \nothaspatch P \implies C \nothaspatch P \]
 455 $\qed$
 456
 457 \subsection{Foreign inclusion:}
 458
 459 If $D = C$, trivial.  For $D \neq C$:
 460 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 461
 462 \subsection{Foreign Contents:}
 463
 464 Only relevant if $\patchof{C} = \bot$.  Trivial by Foreign Contents of
 465 $A$.  $\qed$
 466
 467 xxx fixme not trivial use Totally Foreign Contents
 468
 469 \section{Create Base}
 470
 471 Given $L$, create a Topbloke base branch initial commit $B$.
 472 \gathbegin
 473  B \hasparents \{ L \}
 474 \gathnext
 475  \patchof{B} = \pa{B}
 476 \gathnext
 477  D \isin B \equiv D \isin L \lor D = B
 478 \end{gather}
 479
 480 \subsection{Conditions}
 481
 482 \[ \eqn{ Ingredients }{
 483  \patchof{L} = \pa{L} \lor \patchof{L} = \bot
 484 }\]
 485 \[ \eqn{ Non-recursion }{
 486  L \not\in \pa{B}
 487 }\]
 488
 489 \subsection{No Replay}
 490
 491 If $\patchof{L} = \pa{L}$, trivial by Base Acyclic for $L$.
 492
 493 If $\patchof{L} = \bot$, xxx
 494
 495 Trivial from Base Acyclic for $L$.  $\qed$
 496
 497 \subsection{Unique Base}
 498
 499 Not applicable. $\qed$
 500
 501 \subsection{Tip Contents}
 502
 503 Not applicable. $\qed$
 504
 505 \subsection{Base Acyclic}
 506
 507 xxx
 508
 509 xxx unfinished
 510
 511 \section{Create Tip}
 512
 513 xxx tbd
 514
 515 \section{Anticommit}
 516
 517 Given $L$ and $\pr$ as represented by $R^+, R^-$.
 518 Construct $C$ which has $\pr$ removed.
 519 Used for removing a branch dependency.
 520 \gathbegin
 521  C \hasparents \{ L \}
 522 \gathnext
 523  \patchof{C} = \patchof{L}
 524 \gathnext
 525  \mergeof{C}{L}{R^+}{R^-}
 526 \end{gather}
 527
 528 \subsection{Conditions}
 529
 530 \[ \eqn{ Ingredients }{
 531 R^+ \in \pry \land R^- = \baseof{R^+}
 532 }\]
 533 \[ \eqn{ Into Base }{
 534  L \in \pn
 535 }\]
 536 \[ \eqn{ Unique Tip }{
 537  \pendsof{L}{\pry} = \{ R^+ \}
 538 }\]
 539 \[ \eqn{ Currently Included }{
 540  L \haspatch \pry
 541 }\]
 542
 543 \subsection{Ordering of ${L, R^+, R^-}$:}
 544
 545 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 546 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
 547 $\qed$
 548
 549 (Note that $R^+ \not\le R^-$, i.e. the merge base
 550 is a descendant, not an ancestor, of the 2nd parent.)
 551
 552 \subsection{No Replay}
 553
 554 No Replay for Merge Results applies.  $\qed$
 555
 556 \subsection{Desired Contents}
 557
 558 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 559 \proofstarts
 560
 561 \subsubsection{For $D = C$:}
 562
 563 Trivially $D \isin C$.  OK.
 564
 565 \subsubsection{For $D \neq C, D \not\le L$:}
 566
 567 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 568 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 569
 570 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 571
 572 By Currently Included, $D \isin L$.
 573
 574 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 575 by Unique Tip, $D \le R^+ \equiv D \le L$.
 576 So $D \isin R^+$.
 577
 578 By Base Acyclic, $D \not\isin R^-$.
 579
 580 Apply $\merge$: $D \not\isin C$.  OK.
 581
 582 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 583
 584 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 585
 586 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 587
 588 $\qed$
 589
 590 \subsection{Unique Base}
 591
 592 Into Base means that $C \in \pn$, so Unique Base is not
 593 applicable. $\qed$
 594
 595 \subsection{Tip Contents}
 596
 597 Again, not applicable. $\qed$
 598
 599 \subsection{Base Acyclic}
 600
 601 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
 602 And by Into Base $C \not\in \py$.
 603 Now from Desired Contents, above, $D \isin C
 604 \implies D \isin L \lor D = C$, which thus
 605 $\implies D \not\in \py$.  $\qed$.
 606
 607 \subsection{Coherence and Patch Inclusion}
 608
 609 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
 610
 611 \subsubsection{For $\p = \pr$:}
 612 By Desired Contents, above, $D \not\isin C$.
 613 So $C \nothaspatch \pr$.
 614
 615 \subsubsection{For $\p \neq \pr$:}
 616 By Desired Contents, $D \isin C \equiv D \isin L$
 617 (since $D \in \py$ so $D \not\in \pry$).
 618
 619 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
 620 So $L \nothaspatch \p \implies C \nothaspatch \p$.
 621
 622 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
 623 so $L \haspatch \p \implies C \haspatch \p$.
 624
 625 $\qed$
 626
 627 \subsection{Foreign Inclusion}
 628
 629 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
 630 So by Desired Contents $D \isin C \equiv D \isin L$.
 631 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 632
 633 And $D \le C \equiv D \le L$.
 634 Thus $D \isin C \equiv D \le C$.
 635
 636 $\qed$
 637
 638 \subsection{Foreign Contents:}
 639
 640 Not applicable. $\qed$
 641
 642 \section{Merge}
 643
 644 Merge commits $L$ and $R$ using merge base $M$:
 645 \gathbegin
 646  C \hasparents \{ L, R \}
 647 \gathnext
 648  \patchof{C} = \patchof{L}
 649 \gathnext
 650  \mergeof{C}{L}{M}{R}
 651 \end{gather}
 652 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 653
 654 \subsection{Conditions}
 655 \[ \eqn{ Ingredients }{
 656  M \le L, M \le R
 657 }\]
 658 \[ \eqn{ Tip Merge }{
 659  L \in \py \implies
 660    \begin{cases}
 661       R \in \py : & \baseof{R} \ge \baseof{L}
 662               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 663       R \in \pn : & M = \baseof{L} \\
 664       \text{otherwise} : & \false
 665    \end{cases}
 666 }\]
 667 \[ \eqn{ Merge Acyclic }{
 668     L \in \pn
 669    \implies
 670     R \nothaspatch \p
 671 }\]
 672 \[ \eqn{ Removal Merge Ends }{
 673     X \not\haspatch \p \land
 674     Y \haspatch \p \land
 675     M \haspatch \p
 676   \implies
 677     \pendsof{Y}{\py} = \pendsof{M}{\py}
 678 }\]
 679 \[ \eqn{ Addition Merge Ends }{
 680     X \not\haspatch \p \land
 681     Y \haspatch \p \land
 682     M \nothaspatch \p
 683    \implies \left[
 684     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 685    \right]
 686 }\]
 687
 688 \subsection{Non-Topbloke merges}
 689
 690 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$.
 691 I.e. not only is it forbidden to merge into a Topbloke-controlled
 692 branch without Topbloke's assistance, it is also forbidden to
 693 merge any Topbloke-controlled branch into any plain git branch.
 694
 695 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 696 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 697 Merge Ends condition applies.  Good.
 698
 699 \subsection{No Replay}
 700
 701 No Replay for Merge Results applies.  $\qed$
 702
 703 \subsection{Unique Base}
 704
 705 Need to consider only $C \in \py$, ie $L \in \py$,
 706 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 707 putative ancestor $A \in \pn$ and see whether $A \le C$.
 708
 709 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 710 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 711 Thus $A \le C \equiv A \le L \lor A \le R$.
 712
 713 By Unique Base of L and Transitive Ancestors,
 714 $A \le L \equiv A \le \baseof{L}$.
 715
 716 \subsubsection{For $R \in \py$:}
 717
 718 By Unique Base of $R$ and Transitive Ancestors,
 719 $A \le R \equiv A \le \baseof{R}$.
 720
 721 But by Tip Merge condition on $\baseof{R}$,
 722 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 723 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 724 Thus $A \le C \equiv A \le \baseof{R}$.
 725 That is, $\baseof{C} = \baseof{R}$.
 726
 727 \subsubsection{For $R \in \pn$:}
 728
 729 By Tip Merge condition on $R$ and since $M \le R$,
 730 $A \le \baseof{L} \implies A \le R$, so
 731 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 732 Thus $A \le C \equiv A \le R$.
 733 That is, $\baseof{C} = R$.
 734
 735 $\qed$
 736
 737 \subsection{Coherence and Patch Inclusion}
 738
 739 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 740 This involves considering $D \in \py$.
 741
 742 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 743 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 744 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 745 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 746
 747 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 748 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 749 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 750
 751 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 752
 753 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 754  \equiv D \isin L \lor D \isin R$.
 755 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 756
 757 Consider $D \neq C, D \isin X \land D \isin Y$:
 758 By $\merge$, $D \isin C$.  Also $D \le X$
 759 so $D \le C$.  OK for $C \haspatch \p$.
 760
 761 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 762 By $\merge$, $D \not\isin C$.
 763 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 764 OK for $C \haspatch \p$.
 765
 766 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 767 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 768 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 769 OK for $C \haspatch \p$.
 770
 771 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 772
 773 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 774
 775 $M \haspatch \p \implies C \nothaspatch \p$.
 776 $M \nothaspatch \p \implies C \haspatch \p$.
 777
 778 \proofstarts
 779
 780 One of the Merge Ends conditions applies.
 781 Recall that we are considering $D \in \py$.
 782 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 783 We will show for each of
 784 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 785 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 786
 787 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 788 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 789 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 790 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 791
 792 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 793 $D \le Y$ so $D \le C$.
 794 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 795
 796 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 797 $D \not\le Y$.  If $D \le X$ then
 798 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 799 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 800 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 801
 802 Consider $D \neq C, M \haspatch P, D \isin Y$:
 803 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 804 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 805 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 806
 807 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 808 By $\merge$, $D \not\isin C$.  OK.
 809
 810 $\qed$
 811
 812 \subsection{Base Acyclic}
 813
 814 This applies when $C \in \pn$.
 815 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 816
 817 Consider some $D \in \py$.
 818
 819 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 820 R$.  And $D \neq C$.  So $D \not\isin C$.
 821
 822 $\qed$
 823
 824 \subsection{Tip Contents}
 825
 826 We need worry only about $C \in \py$.
 827 And $\patchof{C} = \patchof{L}$
 828 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 829 of $C$, and its Coherence and Patch Inclusion, as just proved.
 830
 831 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 832 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 833 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 834 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 835 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 836
 837 We will consider an arbitrary commit $D$
 838 and prove the Exclusive Tip Contents form.
 839
 840 \subsubsection{For $D \in \py$:}
 841 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 842 \le C$.  OK.
 843
 844 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 845
 846 $D \neq C$.  By Tip Contents of $L$,
 847 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
 848 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
 849 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
 850 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
 851
 852 \subsubsection{For $D \not\in \py, R \in \py$:}
 853
 854 $D \neq C$.
 855
 856 By Tip Contents
 857 $D \isin L \equiv D \isin \baseof{L}$ and
 858 $D \isin R \equiv D \isin \baseof{R}$.
 859
 860 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
 861 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
 862 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
 863 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
 864
 865 So $D \isin M \equiv D \isin L$ and by $\merge$,
 866 $D \isin C \equiv D \isin R$.  But from Unique Base,
 867 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
 868
 869 $\qed$
 870
 871 \subsection{Foreign Inclusion}
 872
 873 Consider some $D$ s.t. $\patchof{D} = \bot$.
 874 By Foreign Inclusion of $L, M, R$:
 875 $D \isin L \equiv D \le L$;
 876 $D \isin M \equiv D \le M$;
 877 $D \isin R \equiv D \le R$.
 878
 879 \subsubsection{For $D = C$:}
 880
 881 $D \isin C$ and $D \le C$.  OK.
 882
 883 \subsubsection{For $D \neq C, D \isin M$:}
 884
 885 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
 886 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
 887
 888 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
 889
 890 By $\merge$, $D \isin C$.
 891 And $D \isin X$ means $D \le X$ so $D \le C$.
 892 OK.
 893
 894 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
 895
 896 By $\merge$, $D \not\isin C$.
 897 And $D \not\le L, D \not\le R$ so $D \not\le C$.
 898 OK
 899
 900 $\qed$
 901
 902 \subsection{Foreign Contents:}
 903
 904 xxx use Totally Foreign Contents
 905
 906 If $\patchof{C} = \bot$, by Foreign Merges
 907 $\patchof{L} = \patchof{R} = \bot$.
 908
 909 \end{document}