article.tex

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