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