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