chiark / gitweb /
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}
11 \renewcommand{\ge}{\geqslant}
12 \renewcommand{\le}{\leqslant}
13 \newcommand{\nge}{\ngeqslant}
14 \newcommand{\nle}{\nleqslant}
16 \newcommand{\has}{\sqsupseteq}
17 \newcommand{\isin}{\sqsubseteq}
19 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
20 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
21 \newcommand{\haspatch}{\sqSupset}
22 \newcommand{\patchisin}{\sqSubset}
24         \newif\ifhidehack\hidehackfalse
25         \DeclareRobustCommand\hidefromedef[2]{%
26           \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
27         \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
29 \newcommand{\set}[1]{\mathbb{#1}}
30 \newcommand{\pay}[1]{\pa{#1}^+}
31 \newcommand{\pan}[1]{\pa{#1}^-}
33 \newcommand{\p}{\pa{P}}
34 \newcommand{\py}{\pay{P}}
35 \newcommand{\pn}{\pan{P}}
37 \newcommand{\pq}{\pa{Q}}
38 \newcommand{\pqy}{\pay{Q}}
39 \newcommand{\pqn}{\pan{Q}}
41 \newcommand{\pr}{\pa{R}}
42 \newcommand{\pry}{\pay{R}}
43 \newcommand{\prn}{\pan{R}}
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}}
51 \renewcommand{\implies}{\Rightarrow}
52 \renewcommand{\equiv}{\Leftrightarrow}
53 \renewcommand{\nequiv}{\nLeftrightarrow}
54 \renewcommand{\land}{\wedge}
55 \renewcommand{\lor}{\vee}
57 \newcommand{\pancs}{{\mathcal A}}
58 \newcommand{\pends}{{\mathcal E}}
60 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
61 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
63 \newcommand{\merge}{{\mathcal M}}
64 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
65 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
67 \newcommand{\patch}{{\mathcal P}}
68 \newcommand{\base}{{\mathcal B}}
70 \newcommand{\patchof}[1]{\patch ( #1 ) }
71 \newcommand{\baseof}[1]{\base ( #1 ) }
73 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
74 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
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 }
85 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
86 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
88 \newcommand{\qed}{\square}
89 \newcommand{\proofstarts}{{\it Proof:}}
90 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
92 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
93 \newcommand{\gathnext}{\\ \tag*{}}
95 \newcommand{\true}{t}
96 \newcommand{\false}{f}
98 \begin{document}
100 \section{Notation}
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$.
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$.
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.
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:
131 \item[ $\patchof{ C }$ ]
132 Either $\p$ s.t. $C \in \p$, or $\bot$.
133 A function from commits to patches' sets $\p$.
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$.
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}$.
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.
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$.
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$.
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.
167 \item[ $\displaystyle \mergeof{C}{L}{M}{R}$ ]
168 The contents of a git merge result:
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 178 \end{basedescript} 179 \newpage 180 \section{Invariants} 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 }$ 208 \section{Some lemmas} 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 224 Original definition is symmetrical in$L$and$R$. 225 } 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. 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 }$ 246 $\eqn{Tip Self Inpatch:}{ 247 \bigforall_{C \in \py} C \haspatch \p 248 }$ 249 Ie, tip commits contain their own patch. 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 } 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 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 }$ 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 } 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 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 } 320 $\eqn{Totally Foreign Contents:}{ 321 \bigforall_{C \hasparents \set A} 322 \left[ 323 \patchof{C} = \bot \land 324 \bigforall_{A \in \set A} \patchof{A} = \bot 325 \right] 326 \implies 327 \left[ 328 D \le C 329 \implies 330 \patchof{D} = \bot 331 \right] 332 }$ 333 \proof{ 334 Consider some$D \le C$. If$D = C$,$\patchof{D} = \bot$trivially. 335 If$D \neq C$then$D \le A$where$A \in \set A$. By Foreign 336 Contents of$A$,$\patchof{D} = \bot$. 337 } 339 \section{Commit annotation} 341 We annotate each Topbloke commit$C$with: 342 \gathbegin 343 \patchof{C} 344 \gathnext 345 \baseof{C}, \text{ if } C \in \py 346 \gathnext 347 \bigforall_{\pq} 348 \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq 349 \gathnext 350 \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy} 351 \end{gather} 353$\patchof{C}$, for each kind of Topbloke-generated commit, is stated 354 in the summary in the section for that kind of commit. 356 Whether$\baseof{C}$is required, and if so what the value is, is 357 stated in the proof of Unique Base for each kind of commit. 359$C \haspatch \pq$or$\nothaspatch \pq$is represented as the 360 set$\{ \pq | C \haspatch \pq \}$. Whether$C \haspatch \pq$361 is in stated 362 (in terms of$I \haspatch \pq$or$I \nothaspatch \pq$363 for the ingredients$I$), 364 in the proof of Coherence for each kind of commit. 366$\pendsof{C}{\pq^+}$is computed, for all Topbloke-generated commits, 367 using the lemma Calculation of Ends, above. 368 We do not annotate$\pendsof{C}{\py}$for$C \in \py$. Doing so would 369 make it wrong to make plain commits with git because the recorded$\pends$370 would have to be updated. The annotation is not needed in that case 371 because$\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$. 373 \section{Simple commit} 375 A simple single-parent forward commit$C$as made by git-commit. 376 \begin{gather} 377 \tag*{} C \hasparents \{ A \} \\ 378 \tag*{} \patchof{C} = \patchof{A} \\ 379 \tag*{} D \isin C \equiv D \isin A \lor D = C 380 \end{gather} 381 This also covers Topbloke-generated commits on plain git branches: 382 Topbloke strips the metadata when exporting. 384 \subsection{No Replay} 386 Ingredients Prevent Replay applies.$\qed$388 \subsection{Unique Base} 389 If$A, C \in \py$then by Calculation of Ends for 390$C, \py, C \not\in \py$: 391$\pendsof{C}{\pn} = \pendsof{A}{\pn}$so 392$\baseof{C} = \baseof{A}$.$\qed$394 \subsection{Tip Contents} 395 We need to consider only$A, C \in \py$. From Tip Contents for$A$: 396 $D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )$ 397 Substitute into the contents of$C$: 398 $D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) 399 \lor D = C$ 400 Since$D = C \implies D \in \py$, 401 and substituting in$\baseof{C}$, this gives: 402 $D \isin C \equiv D \isin \baseof{C} \lor 403 (D \in \py \land D \le A) \lor 404 (D = C \land D \in \py)$ 405 $\equiv D \isin \baseof{C} \lor 406 [ D \in \py \land ( D \le A \lor D = C ) ]$ 407 So by Exact Ancestors: 408 $D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C 409 )$ 410$\qed$412 \subsection{Base Acyclic} 414 Need to consider only$A, C \in \pn$. 416 For$D = C$:$D \in \pn$so$D \not\in \py$. OK. 418 For$D \neq C$:$D \isin C \equiv D \isin A$, so by Base Acyclic for 419$A$,$D \isin C \implies D \not\in \py$. 421$\qed$423 \subsection{Coherence and patch inclusion} 425 Need to consider$D \in \py$427 \subsubsection{For$A \haspatch P, D = C$:} 429 Ancestors of$C$: 430$ D \le C $. 432 Contents of$C$: 433$ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $. 435 \subsubsection{For$A \haspatch P, D \neq C$:} 436 Ancestors:$ D \le C \equiv D \le A $. 438 Contents:$ D \isin C \equiv D \isin A \lor f $439 so$ D \isin C \equiv D \isin A $. 441 So: 442 $A \haspatch P \implies C \haspatch P$ 444 \subsubsection{For$A \nothaspatch P$:} 446 Firstly,$C \not\in \py$since if it were,$A \in \py$. 447 Thus$D \neq C$. 449 Now by contents of$A$,$D \notin A$, so$D \notin C$. 451 So: 452 $A \nothaspatch P \implies C \nothaspatch P$ 453$\qed$455 \subsection{Foreign inclusion:} 457 If$D = C$, trivial. For$D \neq C$: 458$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.$\qed$460 \subsection{Foreign Contents:} 462 Only relevant if$\patchof{C} = \bot$, and in that case Totally 463 Foreign Contents applies.$\qed$465 \section{Create Base} 467 Given$L$, create a Topbloke base branch initial commit$B$. 468 \gathbegin 469 B \hasparents \{ L \} 470 \gathnext 471 \patchof{B} = \pqn 472 \gathnext 473 D \isin B \equiv D \isin L \lor D = B 474 \end{gather} 476 \subsection{Conditions} 478 $\eqn{ Ingredients }{ 479 \patchof{L} = \pa{L} \lor \patchof{L} = \bot 480 }$ 481 $\eqn{ Create Acyclic }{ 482 L \not\haspatch \pq 483 }$ 485 \subsection{No Replay} 487 Ingredients Prevent Replay applies.$\qed$489 \subsection{Unique Base} 491 Not applicable. 493 \subsection{Tip Contents} 495 Not applicable. 497 \subsection{Base Acyclic} 499 Consider some$D \isin B$. If$D = B$,$D \in \pqn$. 500 If$D \neq B$,$D \isin L$, and by Create Acyclic 501$D \not\in \pqy$.$\qed$503 \subsection{Coherence and Patch Inclusion} 505 Consider some$D \in \p$. 506$B \not\in \py$so$D \neq B$. So$D \isin B \equiv D \isin L$507 and$D \le B \equiv D \le L$. 509 Thus$L \haspatch \p \implies B \haspatch P$510 and$L \nothaspatch \p \implies B \nothaspatch P$. 512$\qed$. 514 \subsection{Foreign Inclusion} 516 Consider some$D$s.t.$\patchof{D} = \bot$.$D \neq B$517 so$D \isin B \equiv D \isin L$. 518 By Foreign Inclusion of$D$in$L$,$D \isin L \equiv D \le L$. 519 And by Exact Ancestors$D \le L \equiv D \le B$. 520 So$D \isin B \equiv D \le B$.$\qed$522 \subsection{Foreign Contents} 524 Not applicable. 526 \section{Create Tip} 528 Given a Topbloke base$B$, create a tip branch initial commit B. 529 \gathbegin 530 C \hasparents \{ B \} 531 \gathnext 532 \patchof{B} = \pqy 533 \gathnext 534 D \isin C \equiv D \isin B \lor D = C 535 \end{gather} 537 \subsection{Conditions} 539 $\eqn{ Ingredients }{ 540 \patchof{B} = \pqn 541 }$ 542 $\eqn{ No Sneak }{ 543 \pendsof{B}{\pqy} = \{ \} 544 }$ 546 \subsection{No Replay} 548 Ingredients Prevent Replay applies.$\qed$550 \subsection{Unique Base} 552 Trivially,$\pendsof{C}{\pqn} = \{B\}$so$\baseof{C} = B$.$\qed$554 \subsection{Tip Contents} 556 Consider some arbitrary commit$D$. If$D = C$, trivially satisfied. 558 If$D \neq C$,$D \isin C \equiv D \isin B$. 559 By Base Acyclic of$B$,$D \isin B \implies D \not\in \pqy$. 560 So$D \isin C \equiv D \isin \baseof{B}$. 562$\qed$564 \subsection{Base Acyclic} 566 Not applicable. 568 \subsection{Coherence and Patch Inclusion} 570 $$571 \begin{cases} 572 \p = \pq \lor B \haspatch \p : & C \haspatch \p \\ 573 \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p 574 \end{cases} 575$$ 577 \proofstarts 578 ~ Consider some$D \in \py$. 580 \subsubsection{For$\p = \pq$:} 582 By Base Acyclic,$D \not\isin B$. So$D \isin C \equiv D = C$. 583 By No Sneak,$D \le B \equiv D = C$. Thus$C \haspatch \pq$. 585 \subsubsection{For$\p \neq \pq$:} 587$D \neq C$. So$D \isin C \equiv D \isin B$, 588 and$D \le C \equiv D \le B$. 590$\qed$592 xxx up to here 594 \section{Anticommit} 596 Given$L$and$\pr$as represented by$R^+, R^-$. 597 Construct$C$which has$\pr$removed. 598 Used for removing a branch dependency. 599 \gathbegin 600 C \hasparents \{ L \} 601 \gathnext 602 \patchof{C} = \patchof{L} 603 \gathnext 604 \mergeof{C}{L}{R^+}{R^-} 605 \end{gather} 607 \subsection{Conditions} 609 $\eqn{ Ingredients }{ 610 R^+ \in \pry \land R^- = \baseof{R^+} 611 }$ 612 $\eqn{ Into Base }{ 613 L \in \pn 614 }$ 615 $\eqn{ Unique Tip }{ 616 \pendsof{L}{\pry} = \{ R^+ \} 617 }$ 618 $\eqn{ Currently Included }{ 619 L \haspatch \pry 620 }$ 622 \subsection{Ordering of Ingredients:} 624 By Unique Tip,$R^+ \le L$. By definition of$\base$,$R^- \le R^+$625 so$R^- \le L$. So$R^+ \le C$and$R^- \le C$. 626$\qed$628 (Note that$R^+ \not\le R^-$, i.e. the merge base 629 is a descendant, not an ancestor, of the 2nd parent.) 631 \subsection{No Replay} 633 By definition of$\merge$, 634$D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$. 635 So, by Ordering of Ingredients, 636 Ingredients Prevent Replay applies.$\qed$638 \subsection{Desired Contents} 640 $D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C$ 641 \proofstarts 643 \subsubsection{For$D = C$:} 645 Trivially$D \isin C$. OK. 647 \subsubsection{For$D \neq C, D \not\le L$:} 649 By No Replay$D \not\isin L$. Also$D \not\le R^-$hence 650$D \not\isin R^-$. Thus$D \not\isin C$. OK. 652 \subsubsection{For$D \neq C, D \le L, D \in \pry$:} 654 By Currently Included,$D \isin L$. 656 By Tip Self Inpatch,$D \isin R^+ \equiv D \le R^+$, but by 657 by Unique Tip,$D \le R^+ \equiv D \le L$. 658 So$D \isin R^+$. 660 By Base Acyclic,$D \not\isin R^-$. 662 Apply$\merge$:$D \not\isin C$. OK. 664 \subsubsection{For$D \neq C, D \le L, D \notin \pry$:} 666 By Tip Contents for$R^+$,$D \isin R^+ \equiv D \isin R^-$. 668 Apply$\merge$:$D \isin C \equiv D \isin L$. OK. 670$\qed$672 \subsection{Unique Base} 674 Into Base means that$C \in \pn$, so Unique Base is not 675 applicable.$\qed$677 \subsection{Tip Contents} 679 Again, not applicable.$\qed$681 \subsection{Base Acyclic} 683 By Base Acyclic for$L$,$D \isin L \implies D \not\in \py$. 684 And by Into Base$C \not\in \py$. 685 Now from Desired Contents, above,$D \isin C
686 \implies D \isin L \lor D = C$, which thus 687$\implies D \not\in \py$.$\qed$. 689 \subsection{Coherence and Patch Inclusion} 691 Need to consider some$D \in \py$. By Into Base,$D \neq C$. 693 \subsubsection{For$\p = \pr$:} 694 By Desired Contents, above,$D \not\isin C$. 695 So$C \nothaspatch \pr$. 697 \subsubsection{For$\p \neq \pr$:} 698 By Desired Contents,$D \isin C \equiv D \isin L$699 (since$D \in \py$so$D \not\in \pry$). 701 If$L \nothaspatch \p$,$D \not\isin L$so$D \not\isin C$. 702 So$L \nothaspatch \p \implies C \nothaspatch \p$. 704 Whereas if$L \haspatch \p$,$D \isin L \equiv D \le L$. 705 so$L \haspatch \p \implies C \haspatch \p$. 707$\qed$709 \subsection{Foreign Inclusion} 711 Consider some$D$s.t.$\patchof{D} = \bot$.$D \neq C$. 712 So by Desired Contents$D \isin C \equiv D \isin L$. 713 By Foreign Inclusion of$D$in$L$,$D \isin L \equiv D \le L$. 715 And$D \le C \equiv D \le L$. 716 Thus$D \isin C \equiv D \le C$. 718$\qed$720 \subsection{Foreign Contents} 722 Not applicable. 724 \section{Merge} 726 Merge commits$L$and$R$using merge base$M$: 727 \gathbegin 728 C \hasparents \{ L, R \} 729 \gathnext 730 \patchof{C} = \patchof{L} 731 \gathnext 732 \mergeof{C}{L}{M}{R} 733 \end{gather} 734 We will occasionally use$X,Y$s.t.$\{X,Y\} = \{L,R\}$. 736 \subsection{Conditions} 737 $\eqn{ Ingredients }{ 738 M \le L, M \le R 739 }$ 740 $\eqn{ Tip Merge }{ 741 L \in \py \implies 742 \begin{cases} 743 R \in \py : & \baseof{R} \ge \baseof{L} 744 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\ 745 R \in \pn : & M = \baseof{L} \\ 746 \text{otherwise} : & \false 747 \end{cases} 748 }$ 749 $\eqn{ Merge Acyclic }{ 750 L \in \pn 751 \implies 752 R \nothaspatch \p 753 }$ 754 $\eqn{ Removal Merge Ends }{ 755 X \not\haspatch \p \land 756 Y \haspatch \p \land 757 M \haspatch \p 758 \implies 759 \pendsof{Y}{\py} = \pendsof{M}{\py} 760 }$ 761 $\eqn{ Addition Merge Ends }{ 762 X \not\haspatch \p \land 763 Y \haspatch \p \land 764 M \nothaspatch \p 765 \implies \left[ 766 \bigforall_{E \in \pendsof{X}{\py}} E \le Y 767 \right] 768 }$ 769 $\eqn{ Foreign Merges }{ 770 \patchof{L} = \bot \equiv \patchof{R} = \bot 771 }$ 773 \subsection{Non-Topbloke merges} 775 We require both$\patchof{L} = \bot$and$\patchof{R} = \bot$776 (Foreign Merges, above). 777 I.e. not only is it forbidden to merge into a Topbloke-controlled 778 branch without Topbloke's assistance, it is also forbidden to 779 merge any Topbloke-controlled branch into any plain git branch. 781 Given those conditions, Tip Merge and Merge Acyclic do not apply. 782 And$Y \not\in \py$so$\neg [ Y \haspatch \p ]$so neither 783 Merge Ends condition applies. 785 So a plain git merge of non-Topbloke branches meets the conditions and 786 is therefore consistent with our scheme. 788 \subsection{No Replay} 790 By definition of$\merge$, 791$D \isin C \implies D \isin L \lor D \isin R \lor D = C$. 792 So, by Ingredients, 793 Ingredients Prevent Replay applies.$\qed$795 \subsection{Unique Base} 797 Need to consider only$C \in \py$, ie$L \in \py$, 798 and calculate$\pendsof{C}{\pn}$. So we will consider some 799 putative ancestor$A \in \pn$and see whether$A \le C$. 801 By Exact Ancestors for C,$A \le C \equiv A \le L \lor A \le R \lor A = C$. 802 But$C \in py$and$A \in \pn$so$A \neq C$. 803 Thus$A \le C \equiv A \le L \lor A \le R$. 805 By Unique Base of L and Transitive Ancestors, 806$A \le L \equiv A \le \baseof{L}$. 808 \subsubsection{For$R \in \py$:} 810 By Unique Base of$R$and Transitive Ancestors, 811$A \le R \equiv A \le \baseof{R}$. 813 But by Tip Merge condition on$\baseof{R}$, 814$A \le \baseof{L} \implies A \le \baseof{R}$, so 815$A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$. 816 Thus$A \le C \equiv A \le \baseof{R}$. 817 That is,$\baseof{C} = \baseof{R}$. 819 \subsubsection{For$R \in \pn$:} 821 By Tip Merge condition on$R$and since$M \le R$, 822$A \le \baseof{L} \implies A \le R$, so 823$A \le R \lor A \le \baseof{L} \equiv A \le R$. 824 Thus$A \le C \equiv A \le R$. 825 That is,$\baseof{C} = R$. 827$\qed$829 \subsection{Coherence and Patch Inclusion} 831 Need to determine$C \haspatch \p$based on$L,M,R \haspatch \p$. 832 This involves considering$D \in \py$. 834 \subsubsection{For$L \nothaspatch \p, R \nothaspatch \p$:} 835$D \not\isin L \land D \not\isin R$.$C \not\in \py$(otherwise$L
836 \in \py$ie$L \haspatch \p$by Tip Self Inpatch). So$D \neq C$. 837 Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch \p$. 839 \subsubsection{For$L \haspatch \p, R \haspatch \p$:} 840$D \isin L \equiv D \le L$and$D \isin R \equiv D \le R$. 841 (Likewise$D \isin X \equiv D \le X$and$D \isin Y \equiv D \le Y$.) 843 Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \haspatch \p$. 845 For$D \neq C$:$D \le C \equiv D \le L \lor D \le R
846  \equiv D \isin L \lor D \isin R$. 847 (Likewise$D \le C \equiv D \le X \lor D \le Y$.) 849 Consider$D \neq C, D \isin X \land D \isin Y$: 850 By$\merge$,$D \isin C$. Also$D \le X$851 so$D \le C$. OK for$C \haspatch \p$. 853 Consider$D \neq C, D \not\isin X \land D \not\isin Y$: 854 By$\merge$,$D \not\isin C$. 855 And$D \not\le X \land D \not\le Y$so$D \not\le C$. 856 OK for$C \haspatch \p$. 858 Remaining case, wlog, is$D \not\isin X \land D \isin Y$. 859$D \not\le X$so$D \not\le M$so$D \not\isin M$. 860 Thus by$\merge$,$D \isin C$. And$D \le Y$so$D \le C$. 861 OK for$C \haspatch \p$. 863 So indeed$L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$. 865 \subsubsection{For (wlog)$X \not\haspatch \p, Y \haspatch \p$:} 867$M \haspatch \p \implies C \nothaspatch \p$. 868$M \nothaspatch \p \implies C \haspatch \p$. 870 \proofstarts 872 One of the Merge Ends conditions applies. 873 Recall that we are considering$D \in \py$. 874$D \isin Y \equiv D \le Y$.$D \not\isin X$. 875 We will show for each of 876 various cases that$D \isin C \equiv M \nothaspatch \p \land D \le C$877 (which suffices by definition of$\haspatch$and$\nothaspatch$). 879 Consider$D = C$: Thus$C \in \py, L \in \py$, and by Tip 880 Self Inpatch$L \haspatch \p$, so$L=Y, R=X$. By Tip Merge, 881$M=\baseof{L}$. So by Base Acyclic$D \not\isin M$, i.e. 882$M \nothaspatch \p$. And indeed$D \isin C$and$D \le C$. OK. 884 Consider$D \neq C, M \nothaspatch P, D \isin Y$: 885$D \le Y$so$D \le C$. 886$D \not\isin M$so by$\merge$,$D \isin C$. OK. 888 Consider$D \neq C, M \nothaspatch P, D \not\isin Y$: 889$D \not\le Y$. If$D \le X$then 890$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 891 Transitive Ancestors$D \le Y$--- a contradiction, so$D \not\le X$. 892 Thus$D \not\le C$. By$\merge$,$D \not\isin C$. OK. 894 Consider$D \neq C, M \haspatch P, D \isin Y$: 895$D \le Y$so$D \in \pancsof{Y}{\py}$so by Removal Merge Ends 896 and Transitive Ancestors$D \in \pancsof{M}{\py}$so$D \le M$. 897 Thus$D \isin M$. By$\merge$,$D \not\isin C$. OK. 899 Consider$D \neq C, M \haspatch P, D \not\isin Y$: 900 By$\merge$,$D \not\isin C$. OK. 902$\qed$904 \subsection{Base Acyclic} 906 This applies when$C \in \pn$. 907$C \in \pn$when$L \in \pn$so by Merge Acyclic,$R \nothaspatch \p$. 909 Consider some$D \in \py$. 911 By Base Acyclic of$L$,$D \not\isin L$. By the above,$D \not\isin
912 R$. And$D \neq C$. So$D \not\isin C$. 914$\qed$916 \subsection{Tip Contents} 918 We need worry only about$C \in \py$. 919 And$\patchof{C} = \patchof{L}$920 so$L \in \py$so$L \haspatch \p$. We will use the Unique Base 921 of$C$, and its Coherence and Patch Inclusion, as just proved. 923 Firstly we show$C \haspatch \p$: If$R \in \py$, then$R \haspatch
924 \p$and by Coherence/Inclusion$C \haspatch \p$. If$R \not\in \py$925 then by Tip Merge$M = \baseof{L}$so by Base Acyclic and definition 926 of$\nothaspatch$,$M \nothaspatch \p$. So by Coherence/Inclusion$C
927 \haspatch \p$(whether$R \haspatch \p$or$\nothaspatch$). 929 We will consider an arbitrary commit$D$930 and prove the Exclusive Tip Contents form. 932 \subsubsection{For$D \in \py$:} 933$C \haspatch \p$so by definition of$\haspatch$,$D \isin C \equiv D
934 \le C$. OK. 936 \subsubsection{For$D \not\in \py, R \not\in \py$:} 938$D \neq C$. By Tip Contents of$L$, 939$D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition, 940$D \isin L \equiv D \isin M$. So by definition of$\merge$,$D \isin
941 C \equiv D \isin R$. And$R = \baseof{C}$by Unique Base of$C$. 942 Thus$D \isin C \equiv D \isin \baseof{C}$. OK. 944 \subsubsection{For$D \not\in \py, R \in \py$:} 946$D \neq C$. 948 By Tip Contents 949$D \isin L \equiv D \isin \baseof{L}$and 950$D \isin R \equiv D \isin \baseof{R}$. 952 If$\baseof{L} = M$, trivially$D \isin M \equiv D \isin \baseof{L}.$953 Whereas if$\baseof{L} = \baseof{M}$, by definition of$\base$, 954$\patchof{M} = \patchof{L} = \py$, so by Tip Contents of$M$, 955$D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$. 957 So$D \isin M \equiv D \isin L$and by$\merge$, 958$D \isin C \equiv D \isin R$. But from Unique Base, 959$\baseof{C} = R$so$D \isin C \equiv D \isin \baseof{C}$. OK. 961$\qed$963 \subsection{Foreign Inclusion} 965 Consider some$D$s.t.$\patchof{D} = \bot$. 966 By Foreign Inclusion of$L, M, R$: 967$D \isin L \equiv D \le L$; 968$D \isin M \equiv D \le M$; 969$D \isin R \equiv D \le R$. 971 \subsubsection{For$D = C$:} 973$D \isin C$and$D \le C$. OK. 975 \subsubsection{For$D \neq C, D \isin M$:} 977 Thus$D \le M$so$D \le L$and$D \le R$so$D \isin L$and$D \isin
978 R$. So by$\merge$,$D \isin C$. And$D \le C$. OK. 980 \subsubsection{For$D \neq C, D \not\isin M, D \isin X$:} 982 By$\merge$,$D \isin C$. 983 And$D \isin X$means$D \le X$so$D \le C$. 984 OK. 986 \subsubsection{For$D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:} 988 By$\merge$,$D \not\isin C$. 989 And$D \not\le L, D \not\le R$so$D \not\le C$. 990 OK 992$\qed$994 \subsection{Foreign Contents} 996 Only relevant if$\patchof{L} = \bot$, in which case 997$\patchof{C} = \bot$and by Foreign Merges$\patchof{R} = \bot$, 998 so Totally Foreign Contents applies.$\qed\$
1000 \end{document}