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