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