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{Totally Foreign Contents:}{ 297 \bigforall_{C \hasparents \set A} 298 \left[ 299 \patchof{C} = \bot \land 300 \bigforall_{A \in \set A} \patchof{A} = \bot 301 \right] 302 \implies 303 \left[ 304 D \le C 305 \implies 306 \patchof{D} = \bot 307 \right] 308 }$ 309 \proof{ 310 Consider some$D \le C$. If$D = C$,$\patchof{D} = \bot$trivially. 311 If$D \neq C$then$D \le A$where$A \in \set A$. By Foreign 312 Contents of$A$,$\patchof{D} = \bot$. 313 } 315 \subsection{No Replay for Merge Results} 317 If we are constructing$C$, with, 318 \gathbegin 319 \mergeof{C}{L}{M}{R} 320 \gathnext 321 L \le C 322 \gathnext 323 R \le C 324 \end{gather} 325 No Replay is preserved. \proofstarts 327 \subsubsection{For$D=C$:}$D \isin C, D \le C$. OK. 329 \subsubsection{For$D \isin L \land D \isin R$:} 330$D \isin C$. And$D \isin L \implies D \le L \implies D \le C$. OK. 332 \subsubsection{For$D \neq C \land D \not\isin L \land D \not\isin R$:} 333$D \not\isin C$. OK. 335 \subsubsection{For$D \neq C \land (D \isin L \equiv D \not\isin R)
336  \land D \not\isin M$:} 337$D \isin C$. Also$D \isin L \lor D \isin R$so$D \le L \lor D \le
338 R$so$D \le C$. OK. 340 \subsubsection{For$D \neq C \land (D \isin L \equiv D \not\isin R)
341  \land D \isin M$:} 342$D \not\isin C$. OK. 344$\qed$346 \section{Commit annotation} 348 We annotate each Topbloke commit$C$with: 349 \gathbegin 350 \patchof{C} 351 \gathnext 352 \baseof{C}, \text{ if } C \in \py 353 \gathnext 354 \bigforall_{\pa{Q}} 355 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q} 356 \gathnext 357 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}} 358 \end{gather} 360$\patchof{C}$, for each kind of Topbloke-generated commit, is stated 361 in the summary in the section for that kind of commit. 363 Whether$\baseof{C}$is required, and if so what the value is, is 364 stated in the proof of Unique Base for each kind of commit. 366$C \haspatch \pa{Q}$or$\nothaspatch \pa{Q}$is represented as the 367 set$\{ \pa{Q} | C \haspatch \pa{Q} \}$. Whether$C \haspatch \pa{Q}$368 is in stated 369 (in terms of$I \haspatch \pa{Q}$or$I \nothaspatch \pa{Q}$370 for the ingredients$I$), 371 in the proof of Coherence for each kind of commit. 373$\pendsof{C}{\pa{Q}^+}$is computed, for all Topbloke-generated commits, 374 using the lemma Calculation of Ends, above. 375 We do not annotate$\pendsof{C}{\py}$for$C \in \py$. Doing so would 376 make it wrong to make plain commits with git because the recorded$\pends$377 would have to be updated. The annotation is not needed in that case 378 because$\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$. 380 \section{Simple commit} 382 A simple single-parent forward commit$C$as made by git-commit. 383 \begin{gather} 384 \tag*{} C \hasparents \{ A \} \\ 385 \tag*{} \patchof{C} = \patchof{A} \\ 386 \tag*{} D \isin C \equiv D \isin A \lor D = C 387 \end{gather} 388 This also covers Topbloke-generated commits on plain git branches: 389 Topbloke strips the metadata when exporting. 391 \subsection{No Replay} 392 Trivial. 394 \subsection{Unique Base} 395 If$A, C \in \py$then by Calculation of Ends for 396$C, \py, C \not\in \py$: 397$\pendsof{C}{\pn} = \pendsof{A}{\pn}$so 398$\baseof{C} = \baseof{A}$.$\qed$400 \subsection{Tip Contents} 401 We need to consider only$A, C \in \py$. From Tip Contents for$A$: 402 $D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )$ 403 Substitute into the contents of$C$: 404 $D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) 405 \lor D = C$ 406 Since$D = C \implies D \in \py$, 407 and substituting in$\baseof{C}$, this gives: 408 $D \isin C \equiv D \isin \baseof{C} \lor 409 (D \in \py \land D \le A) \lor 410 (D = C \land D \in \py)$ 411 $\equiv D \isin \baseof{C} \lor 412 [ D \in \py \land ( D \le A \lor D = C ) ]$ 413 So by Exact Ancestors: 414 $D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C 415 )$ 416$\qed$418 \subsection{Base Acyclic} 420 Need to consider only$A, C \in \pn$. 422 For$D = C$:$D \in \pn$so$D \not\in \py$. OK. 424 For$D \neq C$:$D \isin C \equiv D \isin A$, so by Base Acyclic for 425$A$,$D \isin C \implies D \not\in \py$. 427$\qed$429 \subsection{Coherence and patch inclusion} 431 Need to consider$D \in \py$433 \subsubsection{For$A \haspatch P, D = C$:} 435 Ancestors of$C$: 436$ D \le C $. 438 Contents of$C$: 439$ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $. 441 \subsubsection{For$A \haspatch P, D \neq C$:} 442 Ancestors:$ D \le C \equiv D \le A $. 444 Contents:$ D \isin C \equiv D \isin A \lor f $445 so$ D \isin C \equiv D \isin A $. 447 So: 448 $A \haspatch P \implies C \haspatch P$ 450 \subsubsection{For$A \nothaspatch P$:} 452 Firstly,$C \not\in \py$since if it were,$A \in \py$. 453 Thus$D \neq C$. 455 Now by contents of$A$,$D \notin A$, so$D \notin C$. 457 So: 458 $A \nothaspatch P \implies C \nothaspatch P$ 459$\qed$461 \subsection{Foreign inclusion:} 463 If$D = C$, trivial. For$D \neq C$: 464$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.$\qed$466 \subsection{Foreign Contents:} 468 Only relevant if$\patchof{C} = \bot$, and in that case Totally 469 Foreign Contents applies.$\qed$471 \section{Create Base} 473 Given$L$, create a Topbloke base branch initial commit$B$. 474 \gathbegin 475 B \hasparents \{ L \} 476 \gathnext 477 \patchof{B} = \pan{B} 478 \gathnext 479 D \isin B \equiv D \isin L \lor D = B 480 \end{gather} 482 \subsection{Conditions} 484 $\eqn{ Ingredients }{ 485 \patchof{L} = \pa{L} \lor \patchof{L} = \bot 486 }$ 487 $\eqn{ Non-recursion }{ 488 L \not\in \pa{B} 489 }$ 491 \subsection{No Replay} 493 If$\patchof{L} = \pa{L}$, trivial by Base Acyclic for$L$. 495 If$\patchof{L} = \bot$, consider some$D \isin B$.$D \neq B$. 496 Thus$D \isin L$. So by No Replay of$D$in$L$,$D \le L$. 497 Thus$D \le B$. 499 \subsection{Unique Base} 501 Not applicable. 503 \subsection{Tip Contents} 505 Not applicable. 507 \subsection{Base Acyclic} 509 Consider some$D \isin B$. If$D = B$,$D \in \pn$, OK. 511 If$D \neq B$,$D \isin L$. By No Replay of$D$in$L$,$D \le L$. 512 Thus by Foreign Contents of$L$,$\patchof{D} = \bot$. OK. 514$\qed$516 \subsection{Coherence and Patch Inclusion} 518 Consider some$D \in \p$. 519$B \not\in \py$so$D \neq B$. So$D \isin B \equiv D \isin L$. 521 Thus$L \haspatch \p \implies B \haspatch P$522 and$L \nothaspatch \p \implies B \nothaspatch P$. 524$\qed$. 526 \subsection{Foreign Inclusion} 528 Consider some$D$s.t.$\patchof{D} = \bot$.$D \neq B$529 so$D \isin B \equiv D \isin L$. 530 By Foreign Inclusion of$D$in$L$,$D \isin L \equiv D \le L$. 531 And by Exact Ancestors$D \le L \equiv D \le B$. 532 So$D \isin B \equiv D \le B$.$\qed$534 \section{Create Tip} 536 xxx tbd 538 \section{Anticommit} 540 Given$L$and$\pr$as represented by$R^+, R^-$. 541 Construct$C$which has$\pr$removed. 542 Used for removing a branch dependency. 543 \gathbegin 544 C \hasparents \{ L \} 545 \gathnext 546 \patchof{C} = \patchof{L} 547 \gathnext 548 \mergeof{C}{L}{R^+}{R^-} 549 \end{gather} 551 \subsection{Conditions} 553 $\eqn{ Ingredients }{ 554 R^+ \in \pry \land R^- = \baseof{R^+} 555 }$ 556 $\eqn{ Into Base }{ 557 L \in \pn 558 }$ 559 $\eqn{ Unique Tip }{ 560 \pendsof{L}{\pry} = \{ R^+ \} 561 }$ 562 $\eqn{ Currently Included }{ 563 L \haspatch \pry 564 }$ 566 \subsection{Ordering of${L, R^+, R^-}$:} 568 By Unique Tip,$R^+ \le L$. By definition of$\base$,$R^- \le R^+$569 so$R^- \le L$. So$R^+ \le C$and$R^- \le C$. 570$\qed$572 (Note that$R^+ \not\le R^-$, i.e. the merge base 573 is a descendant, not an ancestor, of the 2nd parent.) 575 \subsection{No Replay} 577 No Replay for Merge Results applies.$\qed$579 \subsection{Desired Contents} 581 $D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C$ 582 \proofstarts 584 \subsubsection{For$D = C$:} 586 Trivially$D \isin C$. OK. 588 \subsubsection{For$D \neq C, D \not\le L$:} 590 By No Replay$D \not\isin L$. Also$D \not\le R^-$hence 591$D \not\isin R^-$. Thus$D \not\isin C$. OK. 593 \subsubsection{For$D \neq C, D \le L, D \in \pry$:} 595 By Currently Included,$D \isin L$. 597 By Tip Self Inpatch,$D \isin R^+ \equiv D \le R^+$, but by 598 by Unique Tip,$D \le R^+ \equiv D \le L$. 599 So$D \isin R^+$. 601 By Base Acyclic,$D \not\isin R^-$. 603 Apply$\merge$:$D \not\isin C$. OK. 605 \subsubsection{For$D \neq C, D \le L, D \notin \pry$:} 607 By Tip Contents for$R^+$,$D \isin R^+ \equiv D \isin R^-$. 609 Apply$\merge$:$D \isin C \equiv D \isin L$. OK. 611$\qed$613 \subsection{Unique Base} 615 Into Base means that$C \in \pn$, so Unique Base is not 616 applicable.$\qed$618 \subsection{Tip Contents} 620 Again, not applicable.$\qed$622 \subsection{Base Acyclic} 624 By Base Acyclic for$L$,$D \isin L \implies D \not\in \py$. 625 And by Into Base$C \not\in \py$. 626 Now from Desired Contents, above,$D \isin C
627 \implies D \isin L \lor D = C$, which thus 628$\implies D \not\in \py$.$\qed$. 630 \subsection{Coherence and Patch Inclusion} 632 Need to consider some$D \in \py$. By Into Base,$D \neq C$. 634 \subsubsection{For$\p = \pr$:} 635 By Desired Contents, above,$D \not\isin C$. 636 So$C \nothaspatch \pr$. 638 \subsubsection{For$\p \neq \pr$:} 639 By Desired Contents,$D \isin C \equiv D \isin L$640 (since$D \in \py$so$D \not\in \pry$). 642 If$L \nothaspatch \p$,$D \not\isin L$so$D \not\isin C$. 643 So$L \nothaspatch \p \implies C \nothaspatch \p$. 645 Whereas if$L \haspatch \p$,$D \isin L \equiv D \le L$. 646 so$L \haspatch \p \implies C \haspatch \p$. 648$\qed$650 \subsection{Foreign Inclusion} 652 Consider some$D$s.t.$\patchof{D} = \bot$.$D \neq C$. 653 So by Desired Contents$D \isin C \equiv D \isin L$. 654 By Foreign Inclusion of$D$in$L$,$D \isin L \equiv D \le L$. 656 And$D \le C \equiv D \le L$. 657 Thus$D \isin C \equiv D \le C$. 659$\qed$661 \subsection{Foreign Contents} 663 Not applicable. 665 \section{Merge} 667 Merge commits$L$and$R$using merge base$M$: 668 \gathbegin 669 C \hasparents \{ L, R \} 670 \gathnext 671 \patchof{C} = \patchof{L} 672 \gathnext 673 \mergeof{C}{L}{M}{R} 674 \end{gather} 675 We will occasionally use$X,Y$s.t.$\{X,Y\} = \{L,R\}$. 677 \subsection{Conditions} 678 $\eqn{ Ingredients }{ 679 M \le L, M \le R 680 }$ 681 $\eqn{ Tip Merge }{ 682 L \in \py \implies 683 \begin{cases} 684 R \in \py : & \baseof{R} \ge \baseof{L} 685 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\ 686 R \in \pn : & M = \baseof{L} \\ 687 \text{otherwise} : & \false 688 \end{cases} 689 }$ 690 $\eqn{ Merge Acyclic }{ 691 L \in \pn 692 \implies 693 R \nothaspatch \p 694 }$ 695 $\eqn{ Removal Merge Ends }{ 696 X \not\haspatch \p \land 697 Y \haspatch \p \land 698 M \haspatch \p 699 \implies 700 \pendsof{Y}{\py} = \pendsof{M}{\py} 701 }$ 702 $\eqn{ Addition Merge Ends }{ 703 X \not\haspatch \p \land 704 Y \haspatch \p \land 705 M \nothaspatch \p 706 \implies \left[ 707 \bigforall_{E \in \pendsof{X}{\py}} E \le Y 708 \right] 709 }$ 710 $\eqn{ Foreign Merges }{ 711 \patchof{L} = \bot \equiv \patchof{R} = \bot 712 }$ 714 \subsection{Non-Topbloke merges} 716 We require both$\patchof{L} = \bot$and$\patchof{R} = \bot$717 (Foreign Merges, above). 718 I.e. not only is it forbidden to merge into a Topbloke-controlled 719 branch without Topbloke's assistance, it is also forbidden to 720 merge any Topbloke-controlled branch into any plain git branch. 722 Given those conditions, Tip Merge and Merge Acyclic do not apply. 723 And$Y \not\in \py$so$\neg [ Y \haspatch \p ]$so neither 724 Merge Ends condition applies. 726 So a plain git merge of non-Topbloke branches meets the conditions and 727 is therefore consistent with our scheme. 729 \subsection{No Replay} 731 No Replay for Merge Results applies.$\qed$733 \subsection{Unique Base} 735 Need to consider only$C \in \py$, ie$L \in \py$, 736 and calculate$\pendsof{C}{\pn}$. So we will consider some 737 putative ancestor$A \in \pn$and see whether$A \le C$. 739 By Exact Ancestors for C,$A \le C \equiv A \le L \lor A \le R \lor A = C$. 740 But$C \in py$and$A \in \pn$so$A \neq C$. 741 Thus$A \le C \equiv A \le L \lor A \le R$. 743 By Unique Base of L and Transitive Ancestors, 744$A \le L \equiv A \le \baseof{L}$. 746 \subsubsection{For$R \in \py$:} 748 By Unique Base of$R$and Transitive Ancestors, 749$A \le R \equiv A \le \baseof{R}$. 751 But by Tip Merge condition on$\baseof{R}$, 752$A \le \baseof{L} \implies A \le \baseof{R}$, so 753$A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$. 754 Thus$A \le C \equiv A \le \baseof{R}$. 755 That is,$\baseof{C} = \baseof{R}$. 757 \subsubsection{For$R \in \pn$:} 759 By Tip Merge condition on$R$and since$M \le R$, 760$A \le \baseof{L} \implies A \le R$, so 761$A \le R \lor A \le \baseof{L} \equiv A \le R$. 762 Thus$A \le C \equiv A \le R$. 763 That is,$\baseof{C} = R$. 765$\qed$767 \subsection{Coherence and Patch Inclusion} 769 Need to determine$C \haspatch \p$based on$L,M,R \haspatch \p$. 770 This involves considering$D \in \py$. 772 \subsubsection{For$L \nothaspatch \p, R \nothaspatch \p$:} 773$D \not\isin L \land D \not\isin R$.$C \not\in \py$(otherwise$L
774 \in \py$ie$L \haspatch \p$by Tip Self Inpatch). So$D \neq C$. 775 Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch \p$. 777 \subsubsection{For$L \haspatch \p, R \haspatch \p$:} 778$D \isin L \equiv D \le L$and$D \isin R \equiv D \le R$. 779 (Likewise$D \isin X \equiv D \le X$and$D \isin Y \equiv D \le Y$.) 781 Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \haspatch \p$. 783 For$D \neq C$:$D \le C \equiv D \le L \lor D \le R
784  \equiv D \isin L \lor D \isin R$. 785 (Likewise$D \le C \equiv D \le X \lor D \le Y$.) 787 Consider$D \neq C, D \isin X \land D \isin Y$: 788 By$\merge$,$D \isin C$. Also$D \le X$789 so$D \le C$. OK for$C \haspatch \p$. 791 Consider$D \neq C, D \not\isin X \land D \not\isin Y$: 792 By$\merge$,$D \not\isin C$. 793 And$D \not\le X \land D \not\le Y$so$D \not\le C$. 794 OK for$C \haspatch \p$. 796 Remaining case, wlog, is$D \not\isin X \land D \isin Y$. 797$D \not\le X$so$D \not\le M$so$D \not\isin M$. 798 Thus by$\merge$,$D \isin C$. And$D \le Y$so$D \le C$. 799 OK for$C \haspatch \p$. 801 So indeed$L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$. 803 \subsubsection{For (wlog)$X \not\haspatch \p, Y \haspatch \p$:} 805$M \haspatch \p \implies C \nothaspatch \p$. 806$M \nothaspatch \p \implies C \haspatch \p$. 808 \proofstarts 810 One of the Merge Ends conditions applies. 811 Recall that we are considering$D \in \py$. 812$D \isin Y \equiv D \le Y$.$D \not\isin X$. 813 We will show for each of 814 various cases that$D \isin C \equiv M \nothaspatch \p \land D \le C$815 (which suffices by definition of$\haspatch$and$\nothaspatch$). 817 Consider$D = C$: Thus$C \in \py, L \in \py$, and by Tip 818 Self Inpatch$L \haspatch \p$, so$L=Y, R=X$. By Tip Merge, 819$M=\baseof{L}$. So by Base Acyclic$D \not\isin M$, i.e. 820$M \nothaspatch \p$. And indeed$D \isin C$and$D \le C$. OK. 822 Consider$D \neq C, M \nothaspatch P, D \isin Y$: 823$D \le Y$so$D \le C$. 824$D \not\isin M$so by$\merge$,$D \isin C$. OK. 826 Consider$D \neq C, M \nothaspatch P, D \not\isin Y$: 827$D \not\le Y$. If$D \le X$then 828$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 829 Transitive Ancestors$D \le Y$--- a contradiction, so$D \not\le X$. 830 Thus$D \not\le C$. By$\merge$,$D \not\isin C$. OK. 832 Consider$D \neq C, M \haspatch P, D \isin Y$: 833$D \le Y$so$D \in \pancsof{Y}{\py}$so by Removal Merge Ends 834 and Transitive Ancestors$D \in \pancsof{M}{\py}$so$D \le M$. 835 Thus$D \isin M$. By$\merge$,$D \not\isin C$. OK. 837 Consider$D \neq C, M \haspatch P, D \not\isin Y$: 838 By$\merge$,$D \not\isin C$. OK. 840$\qed$842 \subsection{Base Acyclic} 844 This applies when$C \in \pn$. 845$C \in \pn$when$L \in \pn$so by Merge Acyclic,$R \nothaspatch \p$. 847 Consider some$D \in \py$. 849 By Base Acyclic of$L$,$D \not\isin L$. By the above,$D \not\isin
850 R$. And$D \neq C$. So$D \not\isin C$. 852$\qed$854 \subsection{Tip Contents} 856 We need worry only about$C \in \py$. 857 And$\patchof{C} = \patchof{L}$858 so$L \in \py$so$L \haspatch \p$. We will use the Unique Base 859 of$C$, and its Coherence and Patch Inclusion, as just proved. 861 Firstly we show$C \haspatch \p$: If$R \in \py$, then$R \haspatch
862 \p$and by Coherence/Inclusion$C \haspatch \p$. If$R \not\in \py$863 then by Tip Merge$M = \baseof{L}$so by Base Acyclic and definition 864 of$\nothaspatch$,$M \nothaspatch \p$. So by Coherence/Inclusion$C
865 \haspatch \p$(whether$R \haspatch \p$or$\nothaspatch$). 867 We will consider an arbitrary commit$D$868 and prove the Exclusive Tip Contents form. 870 \subsubsection{For$D \in \py$:} 871$C \haspatch \p$so by definition of$\haspatch$,$D \isin C \equiv D
872 \le C$. OK. 874 \subsubsection{For$D \not\in \py, R \not\in \py$:} 876$D \neq C$. By Tip Contents of$L$, 877$D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition, 878$D \isin L \equiv D \isin M$. So by definition of$\merge$,$D \isin
879 C \equiv D \isin R$. And$R = \baseof{C}$by Unique Base of$C$. 880 Thus$D \isin C \equiv D \isin \baseof{C}$. OK. 882 \subsubsection{For$D \not\in \py, R \in \py$:} 884$D \neq C$. 886 By Tip Contents 887$D \isin L \equiv D \isin \baseof{L}$and 888$D \isin R \equiv D \isin \baseof{R}$. 890 If$\baseof{L} = M$, trivially$D \isin M \equiv D \isin \baseof{L}.$891 Whereas if$\baseof{L} = \baseof{M}$, by definition of$\base$, 892$\patchof{M} = \patchof{L} = \py$, so by Tip Contents of$M$, 893$D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$. 895 So$D \isin M \equiv D \isin L$and by$\merge$, 896$D \isin C \equiv D \isin R$. But from Unique Base, 897$\baseof{C} = R$so$D \isin C \equiv D \isin \baseof{C}$. OK. 899$\qed$901 \subsection{Foreign Inclusion} 903 Consider some$D$s.t.$\patchof{D} = \bot$. 904 By Foreign Inclusion of$L, M, R$: 905$D \isin L \equiv D \le L$; 906$D \isin M \equiv D \le M$; 907$D \isin R \equiv D \le R$. 909 \subsubsection{For$D = C$:} 911$D \isin C$and$D \le C$. OK. 913 \subsubsection{For$D \neq C, D \isin M$:} 915 Thus$D \le M$so$D \le L$and$D \le R$so$D \isin L$and$D \isin
916 R$. So by$\merge$,$D \isin C$. And$D \le C$. OK. 918 \subsubsection{For$D \neq C, D \not\isin M, D \isin X$:} 920 By$\merge$,$D \isin C$. 921 And$D \isin X$means$D \le X$so$D \le C$. 922 OK. 924 \subsubsection{For$D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:} 926 By$\merge$,$D \not\isin C$. 927 And$D \not\le L, D \not\le R$so$D \not\le C$. 928 OK 930$\qed$932 \subsection{Foreign Contents} 934 Only relevant if$\patchof{L} = \bot$, in which case 935$\patchof{C} = \bot$and by Foreign Merges$\patchof{R} = \bot$, 936 so Totally Foreign Contents applies.$\qed\$
938 \end{document}