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{\pq}{\pa{Q}}
  38 \newcommand{\pqy}{\pay{Q}}
  39 \newcommand{\pqn}{\pan{Q}}
  40
  41 \newcommand{\pr}{\pa{R}}
  42 \newcommand{\pry}{\pay{R}}
  43 \newcommand{\prn}{\pan{R}}
  44
  45 %\newcommand{\hasparents}{\underaccent{1}{>}}
  46 %\newcommand{\hasparents}{{%
  47 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
  48 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
  49 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
  50
  51 \renewcommand{\implies}{\Rightarrow}
  52 \renewcommand{\equiv}{\Leftrightarrow}
  53 \renewcommand{\nequiv}{\nLeftrightarrow}
  54 \renewcommand{\land}{\wedge}
  55 \renewcommand{\lor}{\vee}
  56
  57 \newcommand{\pancs}{{\mathcal A}}
  58 \newcommand{\pends}{{\mathcal E}}
  59
  60 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
  61 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
  62
  63 \newcommand{\merge}{{\mathcal M}}
  64 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
  65 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
  66
  67 \newcommand{\patch}{{\mathcal P}}
  68 \newcommand{\base}{{\mathcal B}}
  69
  70 \newcommand{\patchof}[1]{\patch ( #1 ) }
  71 \newcommand{\baseof}[1]{\base ( #1 ) }
  72
  73 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
  74 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
  75
  76 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
  77 \newcommand{\bigforall}{%
  78   \mathop{\mathchoice%
  79     {\hbox{\huge$\forall$}}%
  80     {\hbox{\Large$\forall$}}%
  81     {\hbox{\normalsize$\forall$}}%
  82     {\hbox{\scriptsize$\forall$}}}%
  83 }
  84
  85 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
  86 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
  87
  88 \newcommand{\qed}{\square}
  89 \newcommand{\proofstarts}{{\it Proof:}}
  90 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
  91
  92 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
  93 \newcommand{\gathnext}{\\ \tag*{}}
  94
  95 \newcommand{\true}{t}
  96 \newcommand{\false}{f}
  97
  98 \begin{document}
  99
 100 \section{Notation}
 101
 102 \begin{basedescript}{
 103 \desclabelwidth{5em}
 104 \desclabelstyle{\nextlinelabel}
 105 }
 106 \item[ $ C \hasparents \set X $ ]
 107 The parents of commit $C$ are exactly the set
 108 $\set X$.
 109
 110 \item[ $ C \ge D $ ]
 111 $C$ is a descendant of $D$ in the git commit
 112 graph.  This is a partial order, namely the transitive closure of
 113 $ D \in \set X $ where $ C \hasparents \set X $.
 114
 115 \item[ $ C \has D $ ]
 116 Informally, the tree at commit $C$ contains the change
 117 made in commit $D$.  Does not take account of deliberate reversions by
 118 the user or reversion, rebasing or rewinding in
 119 non-Topbloke-controlled branches.  For merges and Topbloke-generated
 120 anticommits or re-commits, the ``change made'' is only to be thought
 121 of as any conflict resolution.  This is not a partial order because it
 122 is not transitive.
 123
 124 \item[ $ \p, \py, \pn $ ]
 125 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
 126 are respectively the base and tip git branches.  $\p$ may be used
 127 where the context requires a set, in which case the statement
 128 is to be taken as applying to both $\py$ and $\pn$.
 129 None of these sets overlap.  Hence:
 130
 131 \item[ $ \patchof{ C } $ ]
 132 Either $\p$ s.t. $ C \in \p $, or $\bot$.
 133 A function from commits to patches' sets $\p$.
 134
 135 \item[ $ \pancsof{C}{\set P} $ ]
 136 $ \{ A \; | \; A \le C \land A \in \set P \} $
 137 i.e. all the ancestors of $C$
 138 which are in $\set P$.
 139
 140 \item[ $ \pendsof{C}{\set P} $ ]
 141 $ \{ E \; | \; E \in \pancsof{C}{\set P}
 142   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
 143   E \neq A \land E \le A \} $
 144 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
 145
 146 \item[ $ \baseof{C} $ ]
 147 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
 148 A partial function from commits to commits.
 149 See Unique Base, below.
 150
 151 \item[ $ C \haspatch \p $ ]
 152 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
 153 ~ Informally, $C$ has the contents of $\p$.
 154
 155 \item[ $ C \nothaspatch \p $ ]
 156 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
 157 ~ Informally, $C$ has none of the contents of $\p$.
 158
 159 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$.  This
 160 includes commits on plain git branches made by applying a Topbloke
 161 patch.  If a Topbloke
 162 patch is applied to a non-Topbloke branch and then bubbles back to
 163 the relevant Topbloke branches, we hope that
 164 if the user still cares about the Topbloke patch,
 165 git's merge algorithm will DTRT when trying to re-apply the changes.
 166
 167 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
 168 The contents of a git merge result:
 169
 170 $\displaystyle D \isin C \equiv
 171   \begin{cases}
 172     (D \isin L \land D \isin R) \lor D = C : & \true \\
 173     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
 174     \text{otherwise} : & D \not\isin M
 175   \end{cases}
 176 $
 177
 178 \end{basedescript}
 179 \newpage
 180 \section{Invariants}
 181
 182 We maintain these each time we construct a new commit. \\
 183 \[ \eqn{No Replay:}{
 184   C \has D \implies C \ge D
 185 }\]
 186 \[\eqn{Unique Base:}{
 187  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
 188 }\]
 189 \[\eqn{Tip Contents:}{
 190   \bigforall_{C \in \py} D \isin C \equiv
 191     { D \isin \baseof{C} \lor \atop
 192       (D \in \py \land D \le C) }
 193 }\]
 194 \[\eqn{Base Acyclic:}{
 195   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
 196 }\]
 197 \[\eqn{Coherence:}{
 198   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
 199 }\]
 200 \[\eqn{Foreign Inclusion:}{
 201   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
 202 }\]
 203 \[\eqn{Foreign Contents:}{
 204   \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
 205     D \le C \implies \patchof{D} = \bot
 206 }\]
 207
 208 \section{Some lemmas}
 209
 210 \[ \eqn{Alternative (overlapping) formulations defining
 211   $\mergeof{C}{L}{M}{R}$:}{
 212  D \isin C \equiv
 213   \begin{cases}
 214     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
 215     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
 216     D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
 217     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
 218     \text{as above with L and R exchanged}
 219   \end{cases}
 220 }\]
 221 \proof{
 222   Truth table xxx
 223
 224   Original definition is symmetrical in $L$ and $R$.
 225 }
 226
 227 \[ \eqn{Exclusive Tip Contents:}{
 228   \bigforall_{C \in \py}
 229     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
 230       \Bigr]
 231 }\]
 232 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 233
 234 \proof{
 235 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
 236 So by Base Acyclic $D \isin B \implies D \notin \py$.
 237 }
 238 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
 239   \bigforall_{C \in \py} D \isin C \equiv
 240   \begin{cases}
 241     D \in \py : & D \le C \\
 242     D \not\in \py : & D \isin \baseof{C}
 243   \end{cases}
 244 }\]
 245
 246 \[ \eqn{Tip Self Inpatch:}{
 247   \bigforall_{C \in \py} C \haspatch \p
 248 }\]
 249 Ie, tip commits contain their own patch.
 250
 251 \proof{
 252 Apply Exclusive Tip Contents to some $D \in \py$:
 253 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
 254   D \isin C \equiv D \le C $
 255 }
 256
 257 \[ \eqn{Exact Ancestors:}{
 258   \bigforall_{ C \hasparents \set{R} }
 259   D \le C \equiv
 260     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
 261     \lor D = C
 262 }\]
 263 xxx proof tbd
 264
 265 \[ \eqn{Transitive Ancestors:}{
 266   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
 267   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
 268 }\]
 269
 270 \proof{
 271 The implication from right to left is trivial because
 272 $ \pends() \subset \pancs() $.
 273 For the implication from left to right:
 274 by the definition of $\mathcal E$,
 275 for every such $A$, either $A \in \pends()$ which implies
 276 $A \le M$ by the LHS directly,
 277 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
 278 in which case we repeat for $A'$.  Since there are finitely many
 279 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 280 by the LHS.  And $A \le A''$.
 281 }
 282
 283 \[ \eqn{Calculation Of Ends:}{
 284   \bigforall_{C \hasparents \set A}
 285     \pendsof{C}{\set P} =
 286       \begin{cases}
 287        C \in \p : & \{ C \}
 288       \\
 289        C \not\in \p : & \displaystyle
 290        \left\{ E \Big|
 291            \Bigl[ \Largeexists_{A \in \set A}
 292                        E \in \pendsof{A}{\set P} \Bigr] \land
 293            \Bigl[ \Largenexists_{B \in \set A}
 294                        E \neq B \land E \le B \Bigr]
 295        \right\}
 296       \end{cases}
 297 }\]
 298 xxx proof tbd
 299
 300 \[ \eqn{Ingredients Prevent Replay:}{
 301   \left[
 302     {C \hasparents \set A} \land
 303    \\
 304     \left(
 305       D \isin C \implies
 306        D = C \lor
 307        \Largeexists_{A \in \set A} D \isin A
 308     \right)
 309   \right] \implies \left[
 310     D \isin C \implies D \le C
 311   \right]
 312 }\]
 313 \proof{
 314   Trivial for $D = C$.  Consider some $D \neq C$, $D \isin C$.
 315   By the preconditions, there is some $A$ s.t. $D \in \set A$
 316   and $D \isin A$.  By No Replay for $A$, $D \le A$.  And
 317   $A \le C$ so $D \le C$.
 318 }
 319
 320 \[ \eqn{Totally Foreign Contents:}{
 321   \bigforall_{C \hasparents \set A}
 322    \left[
 323     \patchof{C} = \bot \land
 324       \bigforall_{A \in \set A} \patchof{A} = \bot
 325    \right]
 326   \implies
 327    \left[
 328     D \le C
 329    \implies
 330     \patchof{D} = \bot
 331    \right]
 332 }\]
 333 \proof{
 334 Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
 335 If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
 336 Contents of $A$, $\patchof{D} = \bot$.
 337 }
 338
 339 \section{Commit annotation}
 340
 341 We annotate each Topbloke commit $C$ with:
 342 \gathbegin
 343  \patchof{C}
 344 \gathnext
 345  \baseof{C}, \text{ if } C \in \py
 346 \gathnext
 347  \bigforall_{\pq}
 348    \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
 349 \gathnext
 350  \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
 351 \end{gather}
 352
 353 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
 354 in the summary in the section for that kind of commit.
 355
 356 Whether $\baseof{C}$ is required, and if so what the value is, is
 357 stated in the proof of Unique Base for each kind of commit.
 358
 359 $C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
 360 set $\{ \pq | C \haspatch \pq \}$.  Whether $C \haspatch \pq$
 361 is in stated
 362 (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
 363 for the ingredients $I$),
 364 in the proof of Coherence for each kind of commit.
 365
 366 $\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
 367 using the lemma Calculation of Ends, above.
 368 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 369 make it wrong to make plain commits with git because the recorded $\pends$
 370 would have to be updated.  The annotation is not needed in that case
 371 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 372
 373 \section{Simple commit}
 374
 375 A simple single-parent forward commit $C$ as made by git-commit.
 376 \begin{gather}
 377 \tag*{} C \hasparents \{ A \} \\
 378 \tag*{} \patchof{C} = \patchof{A} \\
 379 \tag*{} D \isin C \equiv D \isin A \lor D = C
 380 \end{gather}
 381 This also covers Topbloke-generated commits on plain git branches:
 382 Topbloke strips the metadata when exporting.
 383
 384 \subsection{No Replay}
 385
 386 Ingredients Prevent Replay applies.  $\qed$
 387
 388 \subsection{Unique Base}
 389 If $A, C \in \py$ then by Calculation of Ends for
 390 $C, \py, C \not\in \py$:
 391 $\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
 392 $\baseof{C} = \baseof{A}$. $\qed$
 393
 394 \subsection{Tip Contents}
 395 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 396 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 397 Substitute into the contents of $C$:
 398 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 399     \lor D = C \]
 400 Since $D = C \implies D \in \py$,
 401 and substituting in $\baseof{C}$, this gives:
 402 \[ D \isin C \equiv D \isin \baseof{C} \lor
 403     (D \in \py \land D \le A) \lor
 404     (D = C \land D \in \py) \]
 405 \[ \equiv D \isin \baseof{C} \lor
 406    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 407 So by Exact Ancestors:
 408 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 409 ) \]
 410 $\qed$
 411
 412 \subsection{Base Acyclic}
 413
 414 Need to consider only $A, C \in \pn$.
 415
 416 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 417
 418 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 419 $A$, $D \isin C \implies D \not\in \py$.
 420
 421 $\qed$
 422
 423 \subsection{Coherence and patch inclusion}
 424
 425 Need to consider $D \in \py$
 426
 427 \subsubsection{For $A \haspatch P, D = C$:}
 428
 429 Ancestors of $C$:
 430 $ D \le C $.
 431
 432 Contents of $C$:
 433 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 434
 435 \subsubsection{For $A \haspatch P, D \neq C$:}
 436 Ancestors: $ D \le C \equiv D \le A $.
 437
 438 Contents: $ D \isin C \equiv D \isin A \lor f $
 439 so $ D \isin C \equiv D \isin A $.
 440
 441 So:
 442 \[ A \haspatch P \implies C \haspatch P \]
 443
 444 \subsubsection{For $A \nothaspatch P$:}
 445
 446 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 447 Thus $D \neq C$.
 448
 449 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 450
 451 So:
 452 \[ A \nothaspatch P \implies C \nothaspatch P \]
 453 $\qed$
 454
 455 \subsection{Foreign inclusion:}
 456
 457 If $D = C$, trivial.  For $D \neq C$:
 458 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 459
 460 \subsection{Foreign Contents:}
 461
 462 Only relevant if $\patchof{C} = \bot$, and in that case Totally
 463 Foreign Contents applies. $\qed$
 464
 465 \section{Create Base}
 466
 467 Given $L$, create a Topbloke base branch initial commit $B$.
 468 \gathbegin
 469  B \hasparents \{ L \}
 470 \gathnext
 471  \patchof{B} = \pqn
 472 \gathnext
 473  D \isin B \equiv D \isin L \lor D = B
 474 \end{gather}
 475
 476 \subsection{Conditions}
 477
 478 \[ \eqn{ Ingredients }{
 479  \patchof{L} = \pa{L} \lor \patchof{L} = \bot
 480 }\]
 481 \[ \eqn{ Create Acyclic }{
 482  L \not\haspatch \pq
 483 }\]
 484
 485 \subsection{No Replay}
 486
 487 Ingredients Prevent Replay applies.  $\qed$
 488
 489 \subsection{Unique Base}
 490
 491 Not applicable.
 492
 493 \subsection{Tip Contents}
 494
 495 Not applicable.
 496
 497 \subsection{Base Acyclic}
 498
 499 Consider some $D \isin B$.  If $D = B$, $D \in \pqn$.
 500 If $D \neq B$, $D \isin L$, and by Create Acyclic
 501 $D \not\in \pqy$.  $\qed$
 502
 503 \subsection{Coherence and Patch Inclusion}
 504
 505 Consider some $D \in \p$.
 506 $B \not\in \py$ so $D \neq B$.  So $D \isin B \equiv D \isin L$
 507 and $D \le B \equiv D \le L$.
 508
 509 Thus $L \haspatch \p \implies B \haspatch P$
 510 and $L \nothaspatch \p \implies B \nothaspatch P$.
 511
 512 $\qed$.
 513
 514 \subsection{Foreign Inclusion}
 515
 516 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq B$
 517 so $D \isin B \equiv D \isin L$.
 518 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 519 And by Exact Ancestors $D \le L \equiv D \le B$.
 520 So $D \isin B \equiv D \le B$.  $\qed$
 521
 522 \subsection{Foreign Contents}
 523
 524 Not applicable.
 525
 526 \section{Create Tip}
 527
 528 Given a Topbloke base $B$, create a tip branch initial commit B.
 529 \gathbegin
 530  C \hasparents \{ B \}
 531 \gathnext
 532  \patchof{B} = \pqy
 533 \gathnext
 534  D \isin C \equiv D \isin B \lor D = C
 535 \end{gather}
 536
 537 \subsection{Conditions}
 538
 539 \[ \eqn{ Ingredients }{
 540  \patchof{B} = \pqn
 541 }\]
 542 \[ \eqn{ No Sneak }{
 543  \pendsof{B}{\pqy} = \{ \}
 544 }\]
 545
 546 \subsection{No Replay}
 547
 548 Ingredients Prevent Replay applies.  $\qed$
 549
 550 \subsection{Unique Base}
 551
 552 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.  $\qed$
 553
 554 \subsection{Tip Contents}
 555
 556 Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.
 557
 558 If $D \neq C$, $D \isin C \equiv D \isin B$.
 559 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
 560 So $D \isin C \equiv D \isin \baseof{B}$.
 561
 562 $\qed$
 563
 564 \subsection{Base Acyclic}
 565
 566 Not applicable.
 567
 568 \subsection{Coherence and Patch Inclusion}
 569
 570 Consider some $D \in \py$.
 571
 572 \subsubsection{For $\p = \pq$:}
 573
 574 By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
 575 By No Sneak, $D \le B \equiv D = C$.  Thus $C \haspatch \pq$.
 576
 577 xxx up to here
 578
 579 \section{Anticommit}
 580
 581 Given $L$ and $\pr$ as represented by $R^+, R^-$.
 582 Construct $C$ which has $\pr$ removed.
 583 Used for removing a branch dependency.
 584 \gathbegin
 585  C \hasparents \{ L \}
 586 \gathnext
 587  \patchof{C} = \patchof{L}
 588 \gathnext
 589  \mergeof{C}{L}{R^+}{R^-}
 590 \end{gather}
 591
 592 \subsection{Conditions}
 593
 594 \[ \eqn{ Ingredients }{
 595 R^+ \in \pry \land R^- = \baseof{R^+}
 596 }\]
 597 \[ \eqn{ Into Base }{
 598  L \in \pn
 599 }\]
 600 \[ \eqn{ Unique Tip }{
 601  \pendsof{L}{\pry} = \{ R^+ \}
 602 }\]
 603 \[ \eqn{ Currently Included }{
 604  L \haspatch \pry
 605 }\]
 606
 607 \subsection{Ordering of Ingredients:}
 608
 609 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 610 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
 611 $\qed$
 612
 613 (Note that $R^+ \not\le R^-$, i.e. the merge base
 614 is a descendant, not an ancestor, of the 2nd parent.)
 615
 616 \subsection{No Replay}
 617
 618 By definition of $\merge$,
 619 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
 620 So, by Ordering of Ingredients,
 621 Ingredients Prevent Replay applies.  $\qed$
 622
 623 \subsection{Desired Contents}
 624
 625 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
 626 \proofstarts
 627
 628 \subsubsection{For $D = C$:}
 629
 630 Trivially $D \isin C$.  OK.
 631
 632 \subsubsection{For $D \neq C, D \not\le L$:}
 633
 634 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
 635 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
 636
 637 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
 638
 639 By Currently Included, $D \isin L$.
 640
 641 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
 642 by Unique Tip, $D \le R^+ \equiv D \le L$.
 643 So $D \isin R^+$.
 644
 645 By Base Acyclic, $D \not\isin R^-$.
 646
 647 Apply $\merge$: $D \not\isin C$.  OK.
 648
 649 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
 650
 651 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
 652
 653 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
 654
 655 $\qed$
 656
 657 \subsection{Unique Base}
 658
 659 Into Base means that $C \in \pn$, so Unique Base is not
 660 applicable. $\qed$
 661
 662 \subsection{Tip Contents}
 663
 664 Again, not applicable. $\qed$
 665
 666 \subsection{Base Acyclic}
 667
 668 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
 669 And by Into Base $C \not\in \py$.
 670 Now from Desired Contents, above, $D \isin C
 671 \implies D \isin L \lor D = C$, which thus
 672 $\implies D \not\in \py$.  $\qed$.
 673
 674 \subsection{Coherence and Patch Inclusion}
 675
 676 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
 677
 678 \subsubsection{For $\p = \pr$:}
 679 By Desired Contents, above, $D \not\isin C$.
 680 So $C \nothaspatch \pr$.
 681
 682 \subsubsection{For $\p \neq \pr$:}
 683 By Desired Contents, $D \isin C \equiv D \isin L$
 684 (since $D \in \py$ so $D \not\in \pry$).
 685
 686 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
 687 So $L \nothaspatch \p \implies C \nothaspatch \p$.
 688
 689 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
 690 so $L \haspatch \p \implies C \haspatch \p$.
 691
 692 $\qed$
 693
 694 \subsection{Foreign Inclusion}
 695
 696 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
 697 So by Desired Contents $D \isin C \equiv D \isin L$.
 698 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
 699
 700 And $D \le C \equiv D \le L$.
 701 Thus $D \isin C \equiv D \le C$.
 702
 703 $\qed$
 704
 705 \subsection{Foreign Contents}
 706
 707 Not applicable.
 708
 709 \section{Merge}
 710
 711 Merge commits $L$ and $R$ using merge base $M$:
 712 \gathbegin
 713  C \hasparents \{ L, R \}
 714 \gathnext
 715  \patchof{C} = \patchof{L}
 716 \gathnext
 717  \mergeof{C}{L}{M}{R}
 718 \end{gather}
 719 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
 720
 721 \subsection{Conditions}
 722 \[ \eqn{ Ingredients }{
 723  M \le L, M \le R
 724 }\]
 725 \[ \eqn{ Tip Merge }{
 726  L \in \py \implies
 727    \begin{cases}
 728       R \in \py : & \baseof{R} \ge \baseof{L}
 729               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 730       R \in \pn : & M = \baseof{L} \\
 731       \text{otherwise} : & \false
 732    \end{cases}
 733 }\]
 734 \[ \eqn{ Merge Acyclic }{
 735     L \in \pn
 736    \implies
 737     R \nothaspatch \p
 738 }\]
 739 \[ \eqn{ Removal Merge Ends }{
 740     X \not\haspatch \p \land
 741     Y \haspatch \p \land
 742     M \haspatch \p
 743   \implies
 744     \pendsof{Y}{\py} = \pendsof{M}{\py}
 745 }\]
 746 \[ \eqn{ Addition Merge Ends }{
 747     X \not\haspatch \p \land
 748     Y \haspatch \p \land
 749     M \nothaspatch \p
 750    \implies \left[
 751     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
 752    \right]
 753 }\]
 754 \[ \eqn{ Foreign Merges }{
 755     \patchof{L} = \bot \equiv \patchof{R} = \bot
 756 }\]
 757
 758 \subsection{Non-Topbloke merges}
 759
 760 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
 761 (Foreign Merges, above).
 762 I.e. not only is it forbidden to merge into a Topbloke-controlled
 763 branch without Topbloke's assistance, it is also forbidden to
 764 merge any Topbloke-controlled branch into any plain git branch.
 765
 766 Given those conditions, Tip Merge and Merge Acyclic do not apply.
 767 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
 768 Merge Ends condition applies.
 769
 770 So a plain git merge of non-Topbloke branches meets the conditions and
 771 is therefore consistent with our scheme.
 772
 773 \subsection{No Replay}
 774
 775 By definition of $\merge$,
 776 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
 777 So, by Ingredients,
 778 Ingredients Prevent Replay applies.  $\qed$
 779
 780 \subsection{Unique Base}
 781
 782 Need to consider only $C \in \py$, ie $L \in \py$,
 783 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 784 putative ancestor $A \in \pn$ and see whether $A \le C$.
 785
 786 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 787 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 788 Thus $A \le C \equiv A \le L \lor A \le R$.
 789
 790 By Unique Base of L and Transitive Ancestors,
 791 $A \le L \equiv A \le \baseof{L}$.
 792
 793 \subsubsection{For $R \in \py$:}
 794
 795 By Unique Base of $R$ and Transitive Ancestors,
 796 $A \le R \equiv A \le \baseof{R}$.
 797
 798 But by Tip Merge condition on $\baseof{R}$,
 799 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 800 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 801 Thus $A \le C \equiv A \le \baseof{R}$.
 802 That is, $\baseof{C} = \baseof{R}$.
 803
 804 \subsubsection{For $R \in \pn$:}
 805
 806 By Tip Merge condition on $R$ and since $M \le R$,
 807 $A \le \baseof{L} \implies A \le R$, so
 808 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 809 Thus $A \le C \equiv A \le R$.
 810 That is, $\baseof{C} = R$.
 811
 812 $\qed$
 813
 814 \subsection{Coherence and Patch Inclusion}
 815
 816 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
 817 This involves considering $D \in \py$.
 818
 819 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
 820 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
 821 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
 822 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
 823
 824 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
 825 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
 826 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
 827
 828 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
 829
 830 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
 831  \equiv D \isin L \lor D \isin R$.
 832 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
 833
 834 Consider $D \neq C, D \isin X \land D \isin Y$:
 835 By $\merge$, $D \isin C$.  Also $D \le X$
 836 so $D \le C$.  OK for $C \haspatch \p$.
 837
 838 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
 839 By $\merge$, $D \not\isin C$.
 840 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
 841 OK for $C \haspatch \p$.
 842
 843 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
 844 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
 845 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
 846 OK for $C \haspatch \p$.
 847
 848 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
 849
 850 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
 851
 852 $M \haspatch \p \implies C \nothaspatch \p$.
 853 $M \nothaspatch \p \implies C \haspatch \p$.
 854
 855 \proofstarts
 856
 857 One of the Merge Ends conditions applies.
 858 Recall that we are considering $D \in \py$.
 859 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
 860 We will show for each of
 861 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
 862 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
 863
 864 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
 865 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
 866 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
 867 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
 868
 869 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
 870 $D \le Y$ so $D \le C$.
 871 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
 872
 873 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
 874 $D \not\le Y$.  If $D \le X$ then
 875 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
 876 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
 877 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
 878
 879 Consider $D \neq C, M \haspatch P, D \isin Y$:
 880 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
 881 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
 882 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
 883
 884 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
 885 By $\merge$, $D \not\isin C$.  OK.
 886
 887 $\qed$
 888
 889 \subsection{Base Acyclic}
 890
 891 This applies when $C \in \pn$.
 892 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
 893
 894 Consider some $D \in \py$.
 895
 896 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
 897 R$.  And $D \neq C$.  So $D \not\isin C$.
 898
 899 $\qed$
 900
 901 \subsection{Tip Contents}
 902
 903 We need worry only about $C \in \py$.
 904 And $\patchof{C} = \patchof{L}$
 905 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
 906 of $C$, and its Coherence and Patch Inclusion, as just proved.
 907
 908 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
 909 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
 910 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
 911 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
 912 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
 913
 914 We will consider an arbitrary commit $D$
 915 and prove the Exclusive Tip Contents form.
 916
 917 \subsubsection{For $D \in \py$:}
 918 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
 919 \le C$.  OK.
 920
 921 \subsubsection{For $D \not\in \py, R \not\in \py$:}
 922
 923 $D \neq C$.  By Tip Contents of $L$,
 924 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
 925 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
 926 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
 927 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
 928
 929 \subsubsection{For $D \not\in \py, R \in \py$:}
 930
 931 $D \neq C$.
 932
 933 By Tip Contents
 934 $D \isin L \equiv D \isin \baseof{L}$ and
 935 $D \isin R \equiv D \isin \baseof{R}$.
 936
 937 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
 938 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
 939 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
 940 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
 941
 942 So $D \isin M \equiv D \isin L$ and by $\merge$,
 943 $D \isin C \equiv D \isin R$.  But from Unique Base,
 944 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
 945
 946 $\qed$
 947
 948 \subsection{Foreign Inclusion}
 949
 950 Consider some $D$ s.t. $\patchof{D} = \bot$.
 951 By Foreign Inclusion of $L, M, R$:
 952 $D \isin L \equiv D \le L$;
 953 $D \isin M \equiv D \le M$;
 954 $D \isin R \equiv D \le R$.
 955
 956 \subsubsection{For $D = C$:}
 957
 958 $D \isin C$ and $D \le C$.  OK.
 959
 960 \subsubsection{For $D \neq C, D \isin M$:}
 961
 962 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
 963 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
 964
 965 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
 966
 967 By $\merge$, $D \isin C$.
 968 And $D \isin X$ means $D \le X$ so $D \le C$.
 969 OK.
 970
 971 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
 972
 973 By $\merge$, $D \not\isin C$.
 974 And $D \not\le L, D \not\le R$ so $D \not\le C$.
 975 OK
 976
 977 $\qed$
 978
 979 \subsection{Foreign Contents}
 980
 981 Only relevant if $\patchof{L} = \bot$, in which case
 982 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
 983 so Totally Foreign Contents applies.  $\qed$
 984
 985 \end{document}