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