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 \[ \eqn{ Foreign Merges }{
 688     \patchof{L} = \bot \equiv \patchof{R} = \bot
 689 }\]
 690
 691 \subsection{Non-Topbloke merges}
 692
 693 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
 694 (Foreign Merges, above).
 695 I.e. not only is it forbidden to merge into a Topbloke-controlled
 696 branch without Topbloke's assistance, it is also forbidden to
 697 merge any Topbloke-controlled branch into any plain git branch.
 698
 699 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 700 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 701 Merge Ends condition applies.
 702
 703 So a plain git merge of non-Topbloke branches meets the conditions and
 704 is therefore consistent with our scheme.
 705
 706 \subsection{No Replay}
 707
 708 No Replay for Merge Results applies.  $\qed$
 709
 710 \subsection{Unique Base}
 711
 712 Need to consider only $C \in \py$, ie $L \in \py$,
 713 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 714 putative ancestor $A \in \pn$ and see whether $A \le C$.
 715
 716 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 717 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 718 Thus $A \le C \equiv A \le L \lor A \le R$.
 719
 720 By Unique Base of L and Transitive Ancestors,
 721 $A \le L \equiv A \le \baseof{L}$.
 722
 723 \subsubsection{For $R \in \py$:}
 724
 725 By Unique Base of $R$ and Transitive Ancestors,
 726 $A \le R \equiv A \le \baseof{R}$.
 727
 728 But by Tip Merge condition on $\baseof{R}$,
 729 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 730 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 731 Thus $A \le C \equiv A \le \baseof{R}$.
 732 That is, $\baseof{C} = \baseof{R}$.
 733
 734 \subsubsection{For $R \in \pn$:}
 735
 736 By Tip Merge condition on $R$ and since $M \le R$,
 737 $A \le \baseof{L} \implies A \le R$, so
 738 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 739 Thus $A \le C \equiv A \le R$.
 740 That is, $\baseof{C} = R$.
 741
 742 $\qed$
 743
 744 \subsection{Coherence and Patch Inclusion}
 745
 746 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 747 This involves considering $D \in \py$.
 748
 749 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 750 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 751 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 752 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 753
 754 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 755 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 756 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 757
 758 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 759
 760 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 761  \equiv D \isin L \lor D \isin R$.
 762 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 763
 764 Consider $D \neq C, D \isin X \land D \isin Y$:
 765 By $\merge$, $D \isin C$.  Also $D \le X$
 766 so $D \le C$.  OK for $C \haspatch \p$.
 767
 768 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 769 By $\merge$, $D \not\isin C$.
 770 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 771 OK for $C \haspatch \p$.
 772
 773 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 774 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 775 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 776 OK for $C \haspatch \p$.
 777
 778 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 779
 780 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 781
 782 $M \haspatch \p \implies C \nothaspatch \p$.
 783 $M \nothaspatch \p \implies C \haspatch \p$.
 784
 785 \proofstarts
 786
 787 One of the Merge Ends conditions applies.
 788 Recall that we are considering $D \in \py$.
 789 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 790 We will show for each of
 791 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 792 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 793
 794 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 795 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 796 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 797 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 798
 799 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 800 $D \le Y$ so $D \le C$.
 801 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 802
 803 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 804 $D \not\le Y$.  If $D \le X$ then
 805 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 806 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 807 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 808
 809 Consider $D \neq C, M \haspatch P, D \isin Y$:
 810 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 811 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 812 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 813
 814 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 815 By $\merge$, $D \not\isin C$.  OK.
 816
 817 $\qed$
 818
 819 \subsection{Base Acyclic}
 820
 821 This applies when $C \in \pn$.
 822 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 823
 824 Consider some $D \in \py$.
 825
 826 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 827 R$.  And $D \neq C$.  So $D \not\isin C$.
 828
 829 $\qed$
 830
 831 \subsection{Tip Contents}
 832
 833 We need worry only about $C \in \py$.
 834 And $\patchof{C} = \patchof{L}$
 835 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 836 of $C$, and its Coherence and Patch Inclusion, as just proved.
 837
 838 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 839 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 840 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 841 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 842 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 843
 844 We will consider an arbitrary commit $D$
 845 and prove the Exclusive Tip Contents form.
 846
 847 \subsubsection{For $D \in \py$:}
 848 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 849 \le C$.  OK.
 850
 851 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 852
 853 $D \neq C$.  By Tip Contents of $L$,
 854 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
 855 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
 856 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
 857 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
 858
 859 \subsubsection{For $D \not\in \py, R \in \py$:}
 860
 861 $D \neq C$.
 862
 863 By Tip Contents
 864 $D \isin L \equiv D \isin \baseof{L}$ and
 865 $D \isin R \equiv D \isin \baseof{R}$.
 866
 867 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
 868 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
 869 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
 870 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
 871
 872 So $D \isin M \equiv D \isin L$ and by $\merge$,
 873 $D \isin C \equiv D \isin R$.  But from Unique Base,
 874 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
 875
 876 $\qed$
 877
 878 \subsection{Foreign Inclusion}
 879
 880 Consider some $D$ s.t. $\patchof{D} = \bot$.
 881 By Foreign Inclusion of $L, M, R$:
 882 $D \isin L \equiv D \le L$;
 883 $D \isin M \equiv D \le M$;
 884 $D \isin R \equiv D \le R$.
 885
 886 \subsubsection{For $D = C$:}
 887
 888 $D \isin C$ and $D \le C$.  OK.
 889
 890 \subsubsection{For $D \neq C, D \isin M$:}
 891
 892 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
 893 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
 894
 895 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
 896
 897 By $\merge$, $D \isin C$.
 898 And $D \isin X$ means $D \le X$ so $D \le C$.
 899 OK.
 900
 901 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
 902
 903 By $\merge$, $D \not\isin C$.
 904 And $D \not\le L, D \not\le R$ so $D \not\le C$.
 905 OK
 906
 907 $\qed$
 908
 909 \subsection{Foreign Contents:}
 910
 911 xxx use Totally Foreign Contents
 912
 913 If $\patchof{C} = \bot$, by Foreign Merges
 914 $\patchof{L} = \patchof{R} = \bot$.
 915
 916 \end{document}