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