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