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