article.tex

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