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{\pr}{\pa{R}}
38 \newcommand{\pry}{\pay{R}}
39 \newcommand{\prn}{\pan{R}}
41 %\newcommand{\hasparents}{\underaccent{1}{>}}
42 %\newcommand{\hasparents}{{%
43 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
44 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
45 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
47 \renewcommand{\implies}{\Rightarrow}
48 \renewcommand{\equiv}{\Leftrightarrow}
49 \renewcommand{\nequiv}{\nLeftrightarrow}
50 \renewcommand{\land}{\wedge}
51 \renewcommand{\lor}{\vee}
53 \newcommand{\pancs}{{\mathcal A}}
54 \newcommand{\pends}{{\mathcal E}}
56 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
57 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
59 \newcommand{\merge}{{\mathcal M}}
60 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
61 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
63 \newcommand{\patch}{{\mathcal P}}
64 \newcommand{\base}{{\mathcal B}}
66 \newcommand{\patchof}[1]{\patch ( #1 ) }
67 \newcommand{\baseof}[1]{\base ( #1 ) }
69 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
70 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
72 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
73 \newcommand{\bigforall}{%
74   \mathop{\mathchoice%
75     {\hbox{\huge$\forall$}}%
76     {\hbox{\Large$\forall$}}%
77     {\hbox{\normalsize$\forall$}}%
78     {\hbox{\scriptsize$\forall$}}}%
79 }
81 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
82 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
84 \newcommand{\qed}{\square}
85 \newcommand{\proofstarts}{{\it Proof:}}
86 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
88 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
89 \newcommand{\gathnext}{\\ \tag*{}}
91 \newcommand{\true}{t}
92 \newcommand{\false}{f}
94 \begin{document}
96 \section{Notation}
98 \begin{basedescript}{
99 \desclabelwidth{5em}
100 \desclabelstyle{\nextlinelabel}
101 }
102 \item[ $C \hasparents \set X$ ]
103 The parents of commit $C$ are exactly the set
104 $\set X$.
106 \item[ $C \ge D$ ]
107 $C$ is a descendant of $D$ in the git commit
108 graph.  This is a partial order, namely the transitive closure of
109 $D \in \set X$ where $C \hasparents \set X$.
111 \item[ $C \has D$ ]
112 Informally, the tree at commit $C$ contains the change
113 made in commit $D$.  Does not take account of deliberate reversions by
114 the user or reversion, rebasing or rewinding in
115 non-Topbloke-controlled branches.  For merges and Topbloke-generated
116 anticommits or re-commits, the change made'' is only to be thought
117 of as any conflict resolution.  This is not a partial order because it
118 is not transitive.
120 \item[ $\p, \py, \pn$ ]
121 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
122 are respectively the base and tip git branches.  $\p$ may be used
123 where the context requires a set, in which case the statement
124 is to be taken as applying to both $\py$ and $\pn$.
125 None of these sets overlap.  Hence:
127 \item[ $\patchof{ C }$ ]
128 Either $\p$ s.t. $C \in \p$, or $\bot$.
129 A function from commits to patches' sets $\p$.
131 \item[ $\pancsof{C}{\set P}$ ]
132 $\{ A \; | \; A \le C \land A \in \set P \}$
133 i.e. all the ancestors of $C$
134 which are in $\set P$.
136 \item[ $\pendsof{C}{\set P}$ ]
137 $\{ E \; | \; E \in \pancsof{C}{\set P} 138 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}} 139 E \neq A \land E \le A \}$
140 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
142 \item[ $\baseof{C}$ ]
143 $\pendsof{C}{\pn} = \{ \baseof{C} \}$ where $C \in \py$.
144 A partial function from commits to commits.
145 See Unique Base, below.
147 \item[ $C \haspatch \p$ ]
148 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C$.
149 ~ Informally, $C$ has the contents of $\p$.
151 \item[ $C \nothaspatch \p$ ]
152 $\displaystyle \bigforall_{D \in \py} D \not\isin C$.
153 ~ Informally, $C$ has none of the contents of $\p$.
155 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$.  This
156 includes commits on plain git branches made by applying a Topbloke
157 patch.  If a Topbloke
158 patch is applied to a non-Topbloke branch and then bubbles back to
159 the relevant Topbloke branches, we hope that
160 if the user still cares about the Topbloke patch,
161 git's merge algorithm will DTRT when trying to re-apply the changes.
163 \item[ $\displaystyle \mergeof{C}{L}{M}{R}$ ]
164 The contents of a git merge result:
166 $\displaystyle D \isin C \equiv 167 \begin{cases} 168 (D \isin L \land D \isin R) \lor D = C : & \true \\ 169 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\ 170 \text{otherwise} : & D \not\isin M 171 \end{cases} 172 174 \end{basedescript} 175 \newpage 176 \section{Invariants} 178 We maintain these each time we construct a new commit. \\ 179 $\eqn{No Replay:}{ 180 C \has D \implies C \ge D 181 }$ 182 $\eqn{Unique Base:}{ 183 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \} 184 }$ 185 $\eqn{Tip Contents:}{ 186 \bigforall_{C \in \py} D \isin C \equiv 187 { D \isin \baseof{C} \lor \atop 188 (D \in \py \land D \le C) } 189 }$ 190 $\eqn{Base Acyclic:}{ 191 \bigforall_{B \in \pn} D \isin B \implies D \notin \py 192 }$ 193 $\eqn{Coherence:}{ 194 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p 195 }$ 196 $\eqn{Foreign Inclusion:}{ 197 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C 198 }$ 199 $\eqn{Foreign Contents:}{ 200 \bigforall_{C \text{ s.t. } \patchof{C} = \bot} 201 D \le C \implies \patchof{D} = \bot 202 }$ 204 \section{Some lemmas} 206 $\eqn{Alternative (overlapping) formulations defining 207 \mergeof{C}{L}{M}{R}:}{ 208 D \isin C \equiv 209 \begin{cases} 210 D \isin L \equiv D \isin R : & D = C \lor D \isin L \\ 211 D \isin L \nequiv D \isin R : & D = C \lor D \not\isin M \\ 212 D \isin L \equiv D \isin M : & D = C \lor D \isin R \\ 213 D \isin L \nequiv D \isin M : & D = C \lor D \isin L \\ 214 \text{as above with L and R exchanged} 215 \end{cases} 216 }$ 217 \proof{ 218 Truth table xxx 220 Original definition is symmetrical in$L$and$R$. 221 } 223 $\eqn{Exclusive Tip Contents:}{ 224 \bigforall_{C \in \py} 225 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C ) 226 \Bigr] 227 }$ 228 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive. 230 \proof{ 231 Let$B = \baseof{C}$in$D \isin \baseof{C}$. Now$B \in \pn$. 232 So by Base Acyclic$D \isin B \implies D \notin \py$. 233 } 234 $\eqntag{{\it Corollary - equivalent to Tip Contents}}{ 235 \bigforall_{C \in \py} D \isin C \equiv 236 \begin{cases} 237 D \in \py : & D \le C \\ 238 D \not\in \py : & D \isin \baseof{C} 239 \end{cases} 240 }$ 242 $\eqn{Tip Self Inpatch:}{ 243 \bigforall_{C \in \py} C \haspatch \p 244 }$ 245 Ie, tip commits contain their own patch. 247 \proof{ 248 Apply Exclusive Tip Contents to some$D \in \py$: 249$ \bigforall_{C \in \py}\bigforall_{D \in \py}
250   D \isin C \equiv D \le C $251 } 253 $\eqn{Exact Ancestors:}{ 254 \bigforall_{ C \hasparents \set{R} } 255 D \le C \equiv 256 ( \mathop{\hbox{\huge{\vee}}}_{R \in \set R} D \le R ) 257 \lor D = C 258 }$ 259 xxx proof tbd 261 $\eqn{Transitive Ancestors:}{ 262 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv 263 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right] 264 }$ 266 \proof{ 267 The implication from right to left is trivial because 268$ \pends() \subset \pancs() $. 269 For the implication from left to right: 270 by the definition of$\mathcal E$, 271 for every such$A$, either$A \in \pends()$which implies 272$A \le M$by the LHS directly, 273 or$\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $274 in which case we repeat for$A'$. Since there are finitely many 275 commits, this terminates with$A'' \in \pends()$, ie$A'' \le M$276 by the LHS. And$A \le A''$. 277 } 279 $\eqn{Calculation Of Ends:}{ 280 \bigforall_{C \hasparents \set A} 281 \pendsof{C}{\set P} = 282 \begin{cases} 283 C \in \p : & \{ C \} 284 \\ 285 C \not\in \p : & \displaystyle 286 \left\{ E \Big| 287 \Bigl[ \Largeexists_{A \in \set A} 288 E \in \pendsof{A}{\set P} \Bigr] \land 289 \Bigl[ \Largenexists_{B \in \set A} 290 E \neq B \land E \le B \Bigr] 291 \right\} 292 \end{cases} 293 }$ 294 xxx proof tbd 296 $\eqn{Ingredients Prevent Replay:}{ 297 \left[ 298 {C \hasparents \set A} \land 299 \\ 300 \left( 301 D \isin C \implies 302 D = C \lor 303 \Largeexists_{A \in \set A} D \isin A 304 \right) 305 \right] \implies \left[ 306 D \isin C \implies D \le C 307 \right] 308 }$ 309 \proof{ 310 Trivial for$D = C$. Consider some$D \neq C$,$D \isin C$. 311 By the preconditions, there is some$A$s.t.$D \in \set A$312 and$D \isin A$. By No Replay for$A$,$D \le A$. And 313$A \le C$so$D \le C$. 314 } 316 $\eqn{Totally Foreign Contents:}{ 317 \bigforall_{C \hasparents \set A} 318 \left[ 319 \patchof{C} = \bot \land 320 \bigforall_{A \in \set A} \patchof{A} = \bot 321 \right] 322 \implies 323 \left[ 324 D \le C 325 \implies 326 \patchof{D} = \bot 327 \right] 328 }$ 329 \proof{ 330 Consider some$D \le C$. If$D = C$,$\patchof{D} = \bot$trivially. 331 If$D \neq C$then$D \le A$where$A \in \set A$. By Foreign 332 Contents of$A$,$\patchof{D} = \bot$. 333 } 335 \section{Commit annotation} 337 We annotate each Topbloke commit$C$with: 338 \gathbegin 339 \patchof{C} 340 \gathnext 341 \baseof{C}, \text{ if } C \in \py 342 \gathnext 343 \bigforall_{\pa{Q}} 344 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q} 345 \gathnext 346 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}} 347 \end{gather} 349$\patchof{C}$, for each kind of Topbloke-generated commit, is stated 350 in the summary in the section for that kind of commit. 352 Whether$\baseof{C}$is required, and if so what the value is, is 353 stated in the proof of Unique Base for each kind of commit. 355$C \haspatch \pa{Q}$or$\nothaspatch \pa{Q}$is represented as the 356 set$\{ \pa{Q} | C \haspatch \pa{Q} \}$. Whether$C \haspatch \pa{Q}$357 is in stated 358 (in terms of$I \haspatch \pa{Q}$or$I \nothaspatch \pa{Q}$359 for the ingredients$I$), 360 in the proof of Coherence for each kind of commit. 362$\pendsof{C}{\pa{Q}^+}$is computed, for all Topbloke-generated commits, 363 using the lemma Calculation of Ends, above. 364 We do not annotate$\pendsof{C}{\py}$for$C \in \py$. Doing so would 365 make it wrong to make plain commits with git because the recorded$\pends$366 would have to be updated. The annotation is not needed in that case 367 because$\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$. 369 \section{Simple commit} 371 A simple single-parent forward commit$C$as made by git-commit. 372 \begin{gather} 373 \tag*{} C \hasparents \{ A \} \\ 374 \tag*{} \patchof{C} = \patchof{A} \\ 375 \tag*{} D \isin C \equiv D \isin A \lor D = C 376 \end{gather} 377 This also covers Topbloke-generated commits on plain git branches: 378 Topbloke strips the metadata when exporting. 380 \subsection{No Replay} 382 Ingredients Prevent Replay applies.$\qed$384 \subsection{Unique Base} 385 If$A, C \in \py$then by Calculation of Ends for 386$C, \py, C \not\in \py$: 387$\pendsof{C}{\pn} = \pendsof{A}{\pn}$so 388$\baseof{C} = \baseof{A}$.$\qed$390 \subsection{Tip Contents} 391 We need to consider only$A, C \in \py$. From Tip Contents for$A$: 392 $D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )$ 393 Substitute into the contents of$C$: 394 $D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) 395 \lor D = C$ 396 Since$D = C \implies D \in \py$, 397 and substituting in$\baseof{C}$, this gives: 398 $D \isin C \equiv D \isin \baseof{C} \lor 399 (D \in \py \land D \le A) \lor 400 (D = C \land D \in \py)$ 401 $\equiv D \isin \baseof{C} \lor 402 [ D \in \py \land ( D \le A \lor D = C ) ]$ 403 So by Exact Ancestors: 404 $D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C 405 )$ 406$\qed$408 \subsection{Base Acyclic} 410 Need to consider only$A, C \in \pn$. 412 For$D = C$:$D \in \pn$so$D \not\in \py$. OK. 414 For$D \neq C$:$D \isin C \equiv D \isin A$, so by Base Acyclic for 415$A$,$D \isin C \implies D \not\in \py$. 417$\qed$419 \subsection{Coherence and patch inclusion} 421 Need to consider$D \in \py$423 \subsubsection{For$A \haspatch P, D = C$:} 425 Ancestors of$C$: 426$ D \le C $. 428 Contents of$C$: 429$ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $. 431 \subsubsection{For$A \haspatch P, D \neq C$:} 432 Ancestors:$ D \le C \equiv D \le A $. 434 Contents:$ D \isin C \equiv D \isin A \lor f $435 so$ D \isin C \equiv D \isin A $. 437 So: 438 $A \haspatch P \implies C \haspatch P$ 440 \subsubsection{For$A \nothaspatch P$:} 442 Firstly,$C \not\in \py$since if it were,$A \in \py$. 443 Thus$D \neq C$. 445 Now by contents of$A$,$D \notin A$, so$D \notin C$. 447 So: 448 $A \nothaspatch P \implies C \nothaspatch P$ 449$\qed$451 \subsection{Foreign inclusion:} 453 If$D = C$, trivial. For$D \neq C$: 454$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.$\qed$456 \subsection{Foreign Contents:} 458 Only relevant if$\patchof{C} = \bot$, and in that case Totally 459 Foreign Contents applies.$\qed$461 \section{Create Base} 463 Given$L$, create a Topbloke base branch initial commit$B$. 464 \gathbegin 465 B \hasparents \{ L \} 466 \gathnext 467 \patchof{B} = \pan{Q} 468 \gathnext 469 D \isin B \equiv D \isin L \lor D = B 470 \end{gather} 472 \subsection{Conditions} 474 $\eqn{ Ingredients }{ 475 \patchof{L} = \pa{L} \lor \patchof{L} = \bot 476 }$ 477 $\eqn{ Create Acyclic }{ 478 L \not\haspatch \pa{Q} 479 }$ 481 \subsection{No Replay} 483 Ingredients Prevent Replay applies.$\qed$485 \subsection{Unique Base} 487 Not applicable. 489 \subsection{Tip Contents} 491 Not applicable. 493 \subsection{Base Acyclic} 495 Consider some$D \isin B$. If$D = B$,$D \in \pan{Q}$. 496 If$D \neq B$,$D \isin L$, and by Create Acyclic 497$D \not\in \pay{Q}$.$\qed$499 \subsection{Coherence and Patch Inclusion} 501 Consider some$D \in \p$. 502$B \not\in \py$so$D \neq B$. So$D \isin B \equiv D \isin L$. 504 Thus$L \haspatch \p \implies B \haspatch P$505 and$L \nothaspatch \p \implies B \nothaspatch P$. 507$\qed$. 509 \subsection{Foreign Inclusion} 511 Consider some$D$s.t.$\patchof{D} = \bot$.$D \neq B$512 so$D \isin B \equiv D \isin L$. 513 By Foreign Inclusion of$D$in$L$,$D \isin L \equiv D \le L$. 514 And by Exact Ancestors$D \le L \equiv D \le B$. 515 So$D \isin B \equiv D \le B$.$\qed$517 \subsection{Foreign Contents} 519 Not applicable. 521 \section{Create Tip} 523 Given a Topbloke base$B$, create a tip branch initial commit B. 524 \gathbegin 525 C \hasparents \{ B \} 526 \gathnext 527 \patchof{B} = \pay{Q} 528 \gathnext 529 D \isin C \equiv D \isin B \lor D = C 530 \end{gather} 532 \subsection{Conditions} 534 $\eqn{ Ingredients }{ 535 \patchof{B} = \pan{Q} 536 }$ 538 \subsection{No Replay} 540 Ingredients Prevent Replay applies.$\qed$542 \subsection{Unique Base} 544 Trivially,$\pendsof{C}{\pan{Q}} = \{B\}$so$\baseof{C} = B$. 546 \subsection{Tip Contents} 548 Consider some arbitrary commit$D$. If$D = C$, trivially satisfied. 550 If$D \neq C$,$D \isin C \equiv D \isin B$. 551 By Base Acyclic of$B$,$D \isin B \implies D \not\in \pay{Q}$. 552 So$D \isin C \equiv D \isin \baseof{B}$. 554$\qed$556 xxx up to here 558 \section{Anticommit} 560 Given$L$and$\pr$as represented by$R^+, R^-$. 561 Construct$C$which has$\pr$removed. 562 Used for removing a branch dependency. 563 \gathbegin 564 C \hasparents \{ L \} 565 \gathnext 566 \patchof{C} = \patchof{L} 567 \gathnext 568 \mergeof{C}{L}{R^+}{R^-} 569 \end{gather} 571 \subsection{Conditions} 573 $\eqn{ Ingredients }{ 574 R^+ \in \pry \land R^- = \baseof{R^+} 575 }$ 576 $\eqn{ Into Base }{ 577 L \in \pn 578 }$ 579 $\eqn{ Unique Tip }{ 580 \pendsof{L}{\pry} = \{ R^+ \} 581 }$ 582 $\eqn{ Currently Included }{ 583 L \haspatch \pry 584 }$ 586 \subsection{Ordering of Ingredients:} 588 By Unique Tip,$R^+ \le L$. By definition of$\base$,$R^- \le R^+$589 so$R^- \le L$. So$R^+ \le C$and$R^- \le C$. 590$\qed$592 (Note that$R^+ \not\le R^-$, i.e. the merge base 593 is a descendant, not an ancestor, of the 2nd parent.) 595 \subsection{No Replay} 597 By definition of$\merge$, 598$D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$. 599 So, by Ordering of Ingredients, 600 Ingredients Prevent Replay applies.$\qed$602 \subsection{Desired Contents} 604 $D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C$ 605 \proofstarts 607 \subsubsection{For$D = C$:} 609 Trivially$D \isin C$. OK. 611 \subsubsection{For$D \neq C, D \not\le L$:} 613 By No Replay$D \not\isin L$. Also$D \not\le R^-$hence 614$D \not\isin R^-$. Thus$D \not\isin C$. OK. 616 \subsubsection{For$D \neq C, D \le L, D \in \pry$:} 618 By Currently Included,$D \isin L$. 620 By Tip Self Inpatch,$D \isin R^+ \equiv D \le R^+$, but by 621 by Unique Tip,$D \le R^+ \equiv D \le L$. 622 So$D \isin R^+$. 624 By Base Acyclic,$D \not\isin R^-$. 626 Apply$\merge$:$D \not\isin C$. OK. 628 \subsubsection{For$D \neq C, D \le L, D \notin \pry$:} 630 By Tip Contents for$R^+$,$D \isin R^+ \equiv D \isin R^-$. 632 Apply$\merge$:$D \isin C \equiv D \isin L$. OK. 634$\qed$636 \subsection{Unique Base} 638 Into Base means that$C \in \pn$, so Unique Base is not 639 applicable.$\qed$641 \subsection{Tip Contents} 643 Again, not applicable.$\qed$645 \subsection{Base Acyclic} 647 By Base Acyclic for$L$,$D \isin L \implies D \not\in \py$. 648 And by Into Base$C \not\in \py$. 649 Now from Desired Contents, above,$D \isin C
650 \implies D \isin L \lor D = C$, which thus 651$\implies D \not\in \py$.$\qed$. 653 \subsection{Coherence and Patch Inclusion} 655 Need to consider some$D \in \py$. By Into Base,$D \neq C$. 657 \subsubsection{For$\p = \pr$:} 658 By Desired Contents, above,$D \not\isin C$. 659 So$C \nothaspatch \pr$. 661 \subsubsection{For$\p \neq \pr$:} 662 By Desired Contents,$D \isin C \equiv D \isin L$663 (since$D \in \py$so$D \not\in \pry$). 665 If$L \nothaspatch \p$,$D \not\isin L$so$D \not\isin C$. 666 So$L \nothaspatch \p \implies C \nothaspatch \p$. 668 Whereas if$L \haspatch \p$,$D \isin L \equiv D \le L$. 669 so$L \haspatch \p \implies C \haspatch \p$. 671$\qed$673 \subsection{Foreign Inclusion} 675 Consider some$D$s.t.$\patchof{D} = \bot$.$D \neq C$. 676 So by Desired Contents$D \isin C \equiv D \isin L$. 677 By Foreign Inclusion of$D$in$L$,$D \isin L \equiv D \le L$. 679 And$D \le C \equiv D \le L$. 680 Thus$D \isin C \equiv D \le C$. 682$\qed$684 \subsection{Foreign Contents} 686 Not applicable. 688 \section{Merge} 690 Merge commits$L$and$R$using merge base$M$: 691 \gathbegin 692 C \hasparents \{ L, R \} 693 \gathnext 694 \patchof{C} = \patchof{L} 695 \gathnext 696 \mergeof{C}{L}{M}{R} 697 \end{gather} 698 We will occasionally use$X,Y$s.t.$\{X,Y\} = \{L,R\}$. 700 \subsection{Conditions} 701 $\eqn{ Ingredients }{ 702 M \le L, M \le R 703 }$ 704 $\eqn{ Tip Merge }{ 705 L \in \py \implies 706 \begin{cases} 707 R \in \py : & \baseof{R} \ge \baseof{L} 708 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\ 709 R \in \pn : & M = \baseof{L} \\ 710 \text{otherwise} : & \false 711 \end{cases} 712 }$ 713 $\eqn{ Merge Acyclic }{ 714 L \in \pn 715 \implies 716 R \nothaspatch \p 717 }$ 718 $\eqn{ Removal Merge Ends }{ 719 X \not\haspatch \p \land 720 Y \haspatch \p \land 721 M \haspatch \p 722 \implies 723 \pendsof{Y}{\py} = \pendsof{M}{\py} 724 }$ 725 $\eqn{ Addition Merge Ends }{ 726 X \not\haspatch \p \land 727 Y \haspatch \p \land 728 M \nothaspatch \p 729 \implies \left[ 730 \bigforall_{E \in \pendsof{X}{\py}} E \le Y 731 \right] 732 }$ 733 $\eqn{ Foreign Merges }{ 734 \patchof{L} = \bot \equiv \patchof{R} = \bot 735 }$ 737 \subsection{Non-Topbloke merges} 739 We require both$\patchof{L} = \bot$and$\patchof{R} = \bot$740 (Foreign Merges, above). 741 I.e. not only is it forbidden to merge into a Topbloke-controlled 742 branch without Topbloke's assistance, it is also forbidden to 743 merge any Topbloke-controlled branch into any plain git branch. 745 Given those conditions, Tip Merge and Merge Acyclic do not apply. 746 And$Y \not\in \py$so$\neg [ Y \haspatch \p ]$so neither 747 Merge Ends condition applies. 749 So a plain git merge of non-Topbloke branches meets the conditions and 750 is therefore consistent with our scheme. 752 \subsection{No Replay} 754 By definition of$\merge$, 755$D \isin C \implies D \isin L \lor D \isin R \lor D = C$. 756 So, by Ingredients, 757 Ingredients Prevent Replay applies.$\qed$759 \subsection{Unique Base} 761 Need to consider only$C \in \py$, ie$L \in \py$, 762 and calculate$\pendsof{C}{\pn}$. So we will consider some 763 putative ancestor$A \in \pn$and see whether$A \le C$. 765 By Exact Ancestors for C,$A \le C \equiv A \le L \lor A \le R \lor A = C$. 766 But$C \in py$and$A \in \pn$so$A \neq C$. 767 Thus$A \le C \equiv A \le L \lor A \le R$. 769 By Unique Base of L and Transitive Ancestors, 770$A \le L \equiv A \le \baseof{L}$. 772 \subsubsection{For$R \in \py$:} 774 By Unique Base of$R$and Transitive Ancestors, 775$A \le R \equiv A \le \baseof{R}$. 777 But by Tip Merge condition on$\baseof{R}$, 778$A \le \baseof{L} \implies A \le \baseof{R}$, so 779$A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$. 780 Thus$A \le C \equiv A \le \baseof{R}$. 781 That is,$\baseof{C} = \baseof{R}$. 783 \subsubsection{For$R \in \pn$:} 785 By Tip Merge condition on$R$and since$M \le R$, 786$A \le \baseof{L} \implies A \le R$, so 787$A \le R \lor A \le \baseof{L} \equiv A \le R$. 788 Thus$A \le C \equiv A \le R$. 789 That is,$\baseof{C} = R$. 791$\qed$793 \subsection{Coherence and Patch Inclusion} 795 Need to determine$C \haspatch \p$based on$L,M,R \haspatch \p$. 796 This involves considering$D \in \py$. 798 \subsubsection{For$L \nothaspatch \p, R \nothaspatch \p$:} 799$D \not\isin L \land D \not\isin R$.$C \not\in \py$(otherwise$L
800 \in \py$ie$L \haspatch \p$by Tip Self Inpatch). So$D \neq C$. 801 Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch \p$. 803 \subsubsection{For$L \haspatch \p, R \haspatch \p$:} 804$D \isin L \equiv D \le L$and$D \isin R \equiv D \le R$. 805 (Likewise$D \isin X \equiv D \le X$and$D \isin Y \equiv D \le Y$.) 807 Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \haspatch \p$. 809 For$D \neq C$:$D \le C \equiv D \le L \lor D \le R
810  \equiv D \isin L \lor D \isin R$. 811 (Likewise$D \le C \equiv D \le X \lor D \le Y$.) 813 Consider$D \neq C, D \isin X \land D \isin Y$: 814 By$\merge$,$D \isin C$. Also$D \le X$815 so$D \le C$. OK for$C \haspatch \p$. 817 Consider$D \neq C, D \not\isin X \land D \not\isin Y$: 818 By$\merge$,$D \not\isin C$. 819 And$D \not\le X \land D \not\le Y$so$D \not\le C$. 820 OK for$C \haspatch \p$. 822 Remaining case, wlog, is$D \not\isin X \land D \isin Y$. 823$D \not\le X$so$D \not\le M$so$D \not\isin M$. 824 Thus by$\merge$,$D \isin C$. And$D \le Y$so$D \le C$. 825 OK for$C \haspatch \p$. 827 So indeed$L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$. 829 \subsubsection{For (wlog)$X \not\haspatch \p, Y \haspatch \p$:} 831$M \haspatch \p \implies C \nothaspatch \p$. 832$M \nothaspatch \p \implies C \haspatch \p$. 834 \proofstarts 836 One of the Merge Ends conditions applies. 837 Recall that we are considering$D \in \py$. 838$D \isin Y \equiv D \le Y$.$D \not\isin X$. 839 We will show for each of 840 various cases that$D \isin C \equiv M \nothaspatch \p \land D \le C$841 (which suffices by definition of$\haspatch$and$\nothaspatch$). 843 Consider$D = C$: Thus$C \in \py, L \in \py$, and by Tip 844 Self Inpatch$L \haspatch \p$, so$L=Y, R=X$. By Tip Merge, 845$M=\baseof{L}$. So by Base Acyclic$D \not\isin M$, i.e. 846$M \nothaspatch \p$. And indeed$D \isin C$and$D \le C$. OK. 848 Consider$D \neq C, M \nothaspatch P, D \isin Y$: 849$D \le Y$so$D \le C$. 850$D \not\isin M$so by$\merge$,$D \isin C$. OK. 852 Consider$D \neq C, M \nothaspatch P, D \not\isin Y$: 853$D \not\le Y$. If$D \le X$then 854$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 855 Transitive Ancestors$D \le Y$--- a contradiction, so$D \not\le X$. 856 Thus$D \not\le C$. By$\merge$,$D \not\isin C$. OK. 858 Consider$D \neq C, M \haspatch P, D \isin Y$: 859$D \le Y$so$D \in \pancsof{Y}{\py}$so by Removal Merge Ends 860 and Transitive Ancestors$D \in \pancsof{M}{\py}$so$D \le M$. 861 Thus$D \isin M$. By$\merge$,$D \not\isin C$. OK. 863 Consider$D \neq C, M \haspatch P, D \not\isin Y$: 864 By$\merge$,$D \not\isin C$. OK. 866$\qed$868 \subsection{Base Acyclic} 870 This applies when$C \in \pn$. 871$C \in \pn$when$L \in \pn$so by Merge Acyclic,$R \nothaspatch \p$. 873 Consider some$D \in \py$. 875 By Base Acyclic of$L$,$D \not\isin L$. By the above,$D \not\isin
876 R$. And$D \neq C$. So$D \not\isin C$. 878$\qed$880 \subsection{Tip Contents} 882 We need worry only about$C \in \py$. 883 And$\patchof{C} = \patchof{L}$884 so$L \in \py$so$L \haspatch \p$. We will use the Unique Base 885 of$C$, and its Coherence and Patch Inclusion, as just proved. 887 Firstly we show$C \haspatch \p$: If$R \in \py$, then$R \haspatch
888 \p$and by Coherence/Inclusion$C \haspatch \p$. If$R \not\in \py$889 then by Tip Merge$M = \baseof{L}$so by Base Acyclic and definition 890 of$\nothaspatch$,$M \nothaspatch \p$. So by Coherence/Inclusion$C
891 \haspatch \p$(whether$R \haspatch \p$or$\nothaspatch$). 893 We will consider an arbitrary commit$D$894 and prove the Exclusive Tip Contents form. 896 \subsubsection{For$D \in \py$:} 897$C \haspatch \p$so by definition of$\haspatch$,$D \isin C \equiv D
898 \le C$. OK. 900 \subsubsection{For$D \not\in \py, R \not\in \py$:} 902$D \neq C$. By Tip Contents of$L$, 903$D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition, 904$D \isin L \equiv D \isin M$. So by definition of$\merge$,$D \isin
905 C \equiv D \isin R$. And$R = \baseof{C}$by Unique Base of$C$. 906 Thus$D \isin C \equiv D \isin \baseof{C}$. OK. 908 \subsubsection{For$D \not\in \py, R \in \py$:} 910$D \neq C$. 912 By Tip Contents 913$D \isin L \equiv D \isin \baseof{L}$and 914$D \isin R \equiv D \isin \baseof{R}$. 916 If$\baseof{L} = M$, trivially$D \isin M \equiv D \isin \baseof{L}.$917 Whereas if$\baseof{L} = \baseof{M}$, by definition of$\base$, 918$\patchof{M} = \patchof{L} = \py$, so by Tip Contents of$M$, 919$D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$. 921 So$D \isin M \equiv D \isin L$and by$\merge$, 922$D \isin C \equiv D \isin R$. But from Unique Base, 923$\baseof{C} = R$so$D \isin C \equiv D \isin \baseof{C}$. OK. 925$\qed$927 \subsection{Foreign Inclusion} 929 Consider some$D$s.t.$\patchof{D} = \bot$. 930 By Foreign Inclusion of$L, M, R$: 931$D \isin L \equiv D \le L$; 932$D \isin M \equiv D \le M$; 933$D \isin R \equiv D \le R$. 935 \subsubsection{For$D = C$:} 937$D \isin C$and$D \le C$. OK. 939 \subsubsection{For$D \neq C, D \isin M$:} 941 Thus$D \le M$so$D \le L$and$D \le R$so$D \isin L$and$D \isin
942 R$. So by$\merge$,$D \isin C$. And$D \le C$. OK. 944 \subsubsection{For$D \neq C, D \not\isin M, D \isin X$:} 946 By$\merge$,$D \isin C$. 947 And$D \isin X$means$D \le X$so$D \le C$. 948 OK. 950 \subsubsection{For$D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:} 952 By$\merge$,$D \not\isin C$. 953 And$D \not\le L, D \not\le R$so$D \not\le C$. 954 OK 956$\qed$958 \subsection{Foreign Contents} 960 Only relevant if$\patchof{L} = \bot$, in which case 961$\patchof{C} = \bot$and by Foreign Merges$\patchof{R} = \bot$, 962 so Totally Foreign Contents applies.$\qed\$
964 \end{document}