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