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 }$ 200 \section{Some lemmas} 202 $\eqn{Alternative (overlapping) formulations defining 203 \mergeof{C}{L}{M}{R}:}{ 204 D \isin C \equiv 205 \begin{cases} 206 D \isin L \equiv D \isin R : & D = C \lor D \isin L \\ 207 D \isin L \nequiv D \isin R : & D = C \lor D \not\isin M \\ 208 D \isin L \equiv D \isin M : & D = C \lor D \isin R \\ 209 D \isin L \nequiv D \isin M : & D = C \lor D \isin L \\ 210 \text{as above with L and R exchanged} 211 \end{cases} 212 }$ 213 \proof{ 214 Truth table xxx 216 Original definition is symmetrical in$L$and$R$. 217 } 219 $\eqn{Exclusive Tip Contents:}{ 220 \bigforall_{C \in \py} 221 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C ) 222 \Bigr] 223 }$ 224 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive. 226 \proof{ 227 Let$B = \baseof{C}$in$D \isin \baseof{C}$. Now$B \in \pn$. 228 So by Base Acyclic$D \isin B \implies D \notin \py$. 229 } 230 $\eqntag{{\it Corollary - equivalent to Tip Contents}}{ 231 \bigforall_{C \in \py} D \isin C \equiv 232 \begin{cases} 233 D \in \py : & D \le C \\ 234 D \not\in \py : & D \isin \baseof{C} 235 \end{cases} 236 }$ 238 $\eqn{Tip Self Inpatch:}{ 239 \bigforall_{C \in \py} C \haspatch \p 240 }$ 241 Ie, tip commits contain their own patch. 243 \proof{ 244 Apply Exclusive Tip Contents to some$D \in \py$: 245$ \bigforall_{C \in \py}\bigforall_{D \in \py}
246   D \isin C \equiv D \le C $247 } 249 $\eqn{Exact Ancestors:}{ 250 \bigforall_{ C \hasparents \set{R} } 251 D \le C \equiv 252 ( \mathop{\hbox{\huge{\vee}}}_{R \in \set R} D \le R ) 253 \lor D = C 254 }$ 255 xxx proof tbd 257 $\eqn{Transitive Ancestors:}{ 258 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv 259 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right] 260 }$ 262 \proof{ 263 The implication from right to left is trivial because 264$ \pends() \subset \pancs() $. 265 For the implication from left to right: 266 by the definition of$\mathcal E$, 267 for every such$A$, either$A \in \pends()$which implies 268$A \le M$by the LHS directly, 269 or$\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $270 in which case we repeat for$A'$. Since there are finitely many 271 commits, this terminates with$A'' \in \pends()$, ie$A'' \le M$272 by the LHS. And$A \le A''$. 273 } 275 $\eqn{Calculation Of Ends:}{ 276 \bigforall_{C \hasparents \set A} 277 \pendsof{C}{\set P} = 278 \begin{cases} 279 C \in \p : & \{ C \} 280 \\ 281 C \not\in \p : & \displaystyle 282 \left\{ E \Big| 283 \Bigl[ \Largeexists_{A \in \set A} 284 E \in \pendsof{A}{\set P} \Bigr] \land 285 \Bigl[ \Largenexists_{B \in \set A} 286 E \neq B \land E \le B \Bigr] 287 \right\} 288 \end{cases} 289 }$ 290 xxx proof tbd 292 \subsection{No Replay for Merge Results} 294 If we are constructing$C$, with, 295 \gathbegin 296 \mergeof{C}{L}{M}{R} 297 \gathnext 298 L \le C 299 \gathnext 300 R \le C 301 \end{gather} 302 No Replay is preserved. \proofstarts 304 \subsubsection{For$D=C$:}$D \isin C, D \le C$. OK. 306 \subsubsection{For$D \isin L \land D \isin R$:} 307$D \isin C$. And$D \isin L \implies D \le L \implies D \le C$. OK. 309 \subsubsection{For$D \neq C \land D \not\isin L \land D \not\isin R$:} 310$D \not\isin C$. OK. 312 \subsubsection{For$D \neq C \land (D \isin L \equiv D \not\isin R)
313  \land D \not\isin M$:} 314$D \isin C$. Also$D \isin L \lor D \isin R$so$D \le L \lor D \le
315 R$so$D \le C$. OK. 317 \subsubsection{For$D \neq C \land (D \isin L \equiv D \not\isin R)
318  \land D \isin M$:} 319$D \not\isin C$. OK. 321$\qed$323 \section{Commit annotation} 325 We annotate each Topbloke commit$C$with: 326 \gathbegin 327 \patchof{C} 328 \gathnext 329 \baseof{C}, \text{ if } C \in \py 330 \gathnext 331 \bigforall_{\pa{Q}} 332 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q} 333 \gathnext 334 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}} 335 \end{gather} 337$\patchof{C}$, for each kind of Topbloke-generated commit, is stated 338 in the summary in the section for that kind of commit. 340 Whether$\baseof{C}$is required, and if so what the value is, is 341 stated in the proof of Unique Base for each kind of commit. 343$C \haspatch \pa{Q}$or$\nothaspatch \pa{Q}$is represented as the 344 set$\{ \pa{Q} | C \haspatch \pa{Q} \}$. Whether$C \haspatch \pa{Q}$345 is in stated 346 (in terms of$I \haspatch \pa{Q}$or$I \nothaspatch \pa{Q}$347 for the ingredients$I$), 348 in the proof of Coherence for each kind of commit. 350$\pendsof{C}{\pa{Q}^+}$is computed, for all Topbloke-generated commits, 351 using the lemma Calculation of Ends, above. 352 We do not annotate$\pendsof{C}{\py}$for$C \in \py$. Doing so would 353 make it wrong to make plain commits with git because the recorded$\pends$354 would have to be updated. The annotation is not needed in that case 355 because$\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$. 357 \section{Simple commit} 359 A simple single-parent forward commit$C$as made by git-commit. 360 \begin{gather} 361 \tag*{} C \hasparents \{ A \} \\ 362 \tag*{} \patchof{C} = \patchof{A} \\ 363 \tag*{} D \isin C \equiv D \isin A \lor D = C 364 \end{gather} 365 This also covers Topbloke-generated commits on plain git branches: 366 Topbloke strips the metadata when exporting. 368 \subsection{No Replay} 369 Trivial. 371 \subsection{Unique Base} 372 If$A, C \in \py$then by Calculation of Ends for 373$C, \py, C \not\in \py$: 374$\pendsof{C}{\pn} = \pendsof{A}{\pn}$so 375$\baseof{C} = \baseof{A}$.$\qed$377 \subsection{Tip Contents} 378 We need to consider only$A, C \in \py$. From Tip Contents for$A$: 379 $D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )$ 380 Substitute into the contents of$C$: 381 $D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) 382 \lor D = C$ 383 Since$D = C \implies D \in \py$, 384 and substituting in$\baseof{C}$, this gives: 385 $D \isin C \equiv D \isin \baseof{C} \lor 386 (D \in \py \land D \le A) \lor 387 (D = C \land D \in \py)$ 388 $\equiv D \isin \baseof{C} \lor 389 [ D \in \py \land ( D \le A \lor D = C ) ]$ 390 So by Exact Ancestors: 391 $D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C 392 )$ 393$\qed$395 \subsection{Base Acyclic} 397 Need to consider only$A, C \in \pn$. 399 For$D = C$:$D \in \pn$so$D \not\in \py$. OK. 401 For$D \neq C$:$D \isin C \equiv D \isin A$, so by Base Acyclic for 402$A$,$D \isin C \implies D \not\in \py$. 404$\qed$406 \subsection{Coherence and patch inclusion} 408 Need to consider$D \in \py$410 \subsubsection{For$A \haspatch P, D = C$:} 412 Ancestors of$C$: 413$ D \le C $. 415 Contents of$C$: 416$ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $. 418 \subsubsection{For$A \haspatch P, D \neq C$:} 419 Ancestors:$ D \le C \equiv D \le A $. 421 Contents:$ D \isin C \equiv D \isin A \lor f $422 so$ D \isin C \equiv D \isin A $. 424 So: 425 $A \haspatch P \implies C \haspatch P$ 427 \subsubsection{For$A \nothaspatch P$:} 429 Firstly,$C \not\in \py$since if it were,$A \in \py$. 430 Thus$D \neq C$. 432 Now by contents of$A$,$D \notin A$, so$D \notin C$. 434 So: 435 $A \nothaspatch P \implies C \nothaspatch P$ 436$\qed$438 \subsection{Foreign inclusion:} 440 If$D = C$, trivial. For$D \neq C$: 441$D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.$\qed$443 \section{Create Base} 445 xxx tbd 447 \section{Create Tip} 449 xxx tbd\ 451 \section{Anticommit} 453 Given$L$and$\pr$as represented by$R^+, R^-$. 454 Construct$C$which has$\pr$removed. 455 Used for removing a branch dependency. 456 \gathbegin 457 C \hasparents \{ L \} 458 \gathnext 459 \patchof{C} = \patchof{L} 460 \gathnext 461 \mergeof{C}{L}{R^+}{R^-} 462 \end{gather} 464 \subsection{Conditions} 466 $\eqn{ Ingredients }{ 467 R^+ \in \pry \land R^- = \baseof{R^+} 468 }$ 469 $\eqn{ Into Base }{ 470 L \in \pn 471 }$ 472 $\eqn{ Unique Tip }{ 473 \pendsof{L}{\pry} = \{ R^+ \} 474 }$ 475 $\eqn{ Currently Included }{ 476 L \haspatch \pry 477 }$ 479 \subsection{Ordering of${L, R^+, R^-}$:} 481 By Unique Tip,$R^+ \le L$. By definition of$\base$,$R^- \le R^+$482 so$R^- \le L$. So$R^+ \le C$and$R^- \le C$. 483$\qed$485 (Note that the merge base$R^+ \not\le R^-$, i.e. the merge base is 486 later than one of the branches to be merged.) 488 \subsection{No Replay} 490 No Replay for Merge Results applies.$\qed$492 \subsection{Desired Contents} 494 $D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C$ 495 \proofstarts 497 \subsubsection{For$D = C$:} 499 Trivially$D \isin C$. OK. 501 \subsubsection{For$D \neq C, D \not\le L$:} 503 By No Replay$D \not\isin L$. Also$D \not\le R^-$hence 504$D \not\isin R^-$. Thus$D \not\isin C$. OK. 506 \subsubsection{For$D \neq C, D \le L, D \in \pry$:} 508 By Currently Included,$D \isin L$. 510 By Tip Self Inpatch,$D \isin R^+ \equiv D \le R^+$, but by 511 by Unique Tip,$D \le R^+ \equiv D \le L$. 512 So$D \isin R^+$. 514 By Base Acyclic,$D \not\isin R^-$. 516 Apply$\merge$:$D \not\isin C$. OK. 518 \subsubsection{For$D \neq C, D \le L, D \notin \pry$:} 520 By Tip Contents for$R^+$,$D \isin R^+ \equiv D \isin R^-$. 522 Apply$\merge$:$D \isin C \equiv D \isin L$. OK. 524$\qed$526 \subsection{Unique Base} 528 Into Base means that$C \in \pn$, so Unique Base is not 529 applicable.$\qed$531 \subsection{Tip Contents} 533 Again, not applicable.$\qed$535 \subsection{Base Acyclic} 537 By Base Acyclic for$L$,$D \isin L \implies D \not\in \py$. 538 And by Into Base$C \not\in \py$. 539 Now from Desired Contents, above,$D \isin C
540 \implies D \isin L \lor D = C$, which thus 541$\implies D \not\in \py$.$\qed$. 543 \subsection{Coherence and Patch Inclusion} 545 Need to consider some$D \in \py$. By Into Base,$D \neq C$. 547 \subsubsection{For$\p = \pr$:} 548 By Desired Contents, above,$D \not\isin C$. 549 So$C \nothaspatch \pr$. 551 \subsubsection{For$\p \neq \pr$:} 552 By Desired Contents,$D \isin C \equiv D \isin L$553 (since$D \in \py$so$D \not\in \pry$). 555 If$L \nothaspatch \p$,$D \not\isin L$so$D \not\isin C$. 556 So$L \nothaspatch \p \implies C \nothaspatch \p$. 558 Whereas if$L \haspatch \p$,$D \isin L \equiv D \le L$. 559 so$L \haspatch \p \implies C \haspatch \p$. 561$\qed$563 \section{Foreign Inclusion} 565 Consider some$D$s.t.$\patchof{D} = \bot$.$D \neq C$. 566 So by Desired Contents$D \isin C \equiv D \isin L$. 567 By Foreign Inclusion of$D$in$L$,$D \isin L \equiv D \le L$. 569 And$D \le C \equiv D \le L$. 570 Thus$D \isin C \equiv D \le C$. 572$\qed$574 \section{Merge} 576 Merge commits$L$and$R$using merge base$M$($M < L, M < R$): 577 \gathbegin 578 C \hasparents \{ L, R \} 579 \gathnext 580 \patchof{C} = \patchof{L} 581 \gathnext 582 \mergeof{C}{L}{M}{R} 583 \end{gather} 584 We will occasionally use$X,Y$s.t.$\{X,Y\} = \{L,R\}$. 586 \subsection{Conditions} 588 $\eqn{ Tip Merge }{ 589 L \in \py \implies 590 \begin{cases} 591 R \in \py : & \baseof{R} \ge \baseof{L} 592 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\ 593 R \in \pn : & M = \baseof{L} \\ 594 \text{otherwise} : & \false 595 \end{cases} 596 }$ 597 $\eqn{ Merge Acyclic }{ 598 L \in \pn 599 \implies 600 R \nothaspatch \p 601 }$ 602 $\eqn{ Removal Merge Ends }{ 603 X \not\haspatch \p \land 604 Y \haspatch \p \land 605 M \haspatch \p 606 \implies 607 \pendsof{Y}{\py} = \pendsof{M}{\py} 608 }$ 609 $\eqn{ Addition Merge Ends }{ 610 X \not\haspatch \p \land 611 Y \haspatch \p \land 612 M \nothaspatch \p 613 \implies \left[ 614 \bigforall_{E \in \pendsof{X}{\py}} E \le Y 615 \right] 616 }$ 618 \subsection{Non-Topbloke merges} 620 We require both$\patchof{L} = \bot$and$\patchof{R} = \bot$. 621 I.e. not only is it forbidden to merge into a Topbloke-controlled 622 branch without Topbloke's assistance, it is also forbidden to 623 merge any Topbloke-controlled branch into any plain git branch. 625 Given those conditions, Tip Merge and Merge Acyclic do not apply. 626 And$Y \not\in \py$so$\neg [ Y \haspatch \p ]$so neither 627 Merge Ends condition applies. Good. 629 \subsection{No Replay} 631 No Replay for Merge Results applies.$\qed$633 \subsection{Unique Base} 635 Need to consider only$C \in \py$, ie$L \in \py$, 636 and calculate$\pendsof{C}{\pn}$. So we will consider some 637 putative ancestor$A \in \pn$and see whether$A \le C$. 639 By Exact Ancestors for C,$A \le C \equiv A \le L \lor A \le R \lor A = C$. 640 But$C \in py$and$A \in \pn$so$A \neq C$. 641 Thus$A \le C \equiv A \le L \lor A \le R$. 643 By Unique Base of L and Transitive Ancestors, 644$A \le L \equiv A \le \baseof{L}$. 646 \subsubsection{For$R \in \py$:} 648 By Unique Base of$R$and Transitive Ancestors, 649$A \le R \equiv A \le \baseof{R}$. 651 But by Tip Merge condition on$\baseof{R}$, 652$A \le \baseof{L} \implies A \le \baseof{R}$, so 653$A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$. 654 Thus$A \le C \equiv A \le \baseof{R}$. 655 That is,$\baseof{C} = \baseof{R}$. 657 \subsubsection{For$R \in \pn$:} 659 By Tip Merge condition on$R$and since$M \le R$, 660$A \le \baseof{L} \implies A \le R$, so 661$A \le R \lor A \le \baseof{L} \equiv A \le R$. 662 Thus$A \le C \equiv A \le R$. 663 That is,$\baseof{C} = R$. 665$\qed$667 \subsection{Coherence and Patch Inclusion} 669 Need to determine$C \haspatch \p$based on$L,M,R \haspatch \p$. 670 This involves considering$D \in \py$. 672 \subsubsection{For$L \nothaspatch \p, R \nothaspatch \p$:} 673$D \not\isin L \land D \not\isin R$.$C \not\in \py$(otherwise$L
674 \in \py$ie$L \haspatch \p$by Tip Self Inpatch). So$D \neq C$. 675 Applying$\merge$gives$D \not\isin C$i.e.$C \nothaspatch \p$. 677 \subsubsection{For$L \haspatch \p, R \haspatch \p$:} 678$D \isin L \equiv D \le L$and$D \isin R \equiv D \le R$. 679 (Likewise$D \isin X \equiv D \le X$and$D \isin Y \equiv D \le Y$.) 681 Consider$D = C$:$D \isin C$,$D \le C$, OK for$C \haspatch \p$. 683 For$D \neq C$:$D \le C \equiv D \le L \lor D \le R
684  \equiv D \isin L \lor D \isin R$. 685 (Likewise$D \le C \equiv D \le X \lor D \le Y$.) 687 Consider$D \neq C, D \isin X \land D \isin Y$: 688 By$\merge$,$D \isin C$. Also$D \le X$689 so$D \le C$. OK for$C \haspatch \p$. 691 Consider$D \neq C, D \not\isin X \land D \not\isin Y$: 692 By$\merge$,$D \not\isin C$. 693 And$D \not\le X \land D \not\le Y$so$D \not\le C$. 694 OK for$C \haspatch \p$. 696 Remaining case, wlog, is$D \not\isin X \land D \isin Y$. 697$D \not\le X$so$D \not\le M$so$D \not\isin M$. 698 Thus by$\merge$,$D \isin C$. And$D \le Y$so$D \le C$. 699 OK for$C \haspatch \p$. 701 So indeed$L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$. 703 \subsubsection{For (wlog)$X \not\haspatch \p, Y \haspatch \p$:} 705$M \haspatch \p \implies C \nothaspatch \p$. 706$M \nothaspatch \p \implies C \haspatch \p$. 708 \proofstarts 710 One of the Merge Ends conditions applies. 711 Recall that we are considering$D \in \py$. 712$D \isin Y \equiv D \le Y$.$D \not\isin X$. 713 We will show for each of 714 various cases that$D \isin C \equiv M \nothaspatch \p \land D \le C$715 (which suffices by definition of$\haspatch$and$\nothaspatch$). 717 Consider$D = C$: Thus$C \in \py, L \in \py$, and by Tip 718 Self Inpatch$L \haspatch \p$, so$L=Y, R=X$. By Tip Merge, 719$M=\baseof{L}$. So by Base Acyclic$D \not\isin M$, i.e. 720$M \nothaspatch \p$. And indeed$D \isin C$and$D \le C$. OK. 722 Consider$D \neq C, M \nothaspatch P, D \isin Y$: 723$D \le Y$so$D \le C$. 724$D \not\isin M$so by$\merge$,$D \isin C$. OK. 726 Consider$D \neq C, M \nothaspatch P, D \not\isin Y$: 727$D \not\le Y$. If$D \le X$then 728$D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 729 Transitive Ancestors$D \le Y$--- a contradiction, so$D \not\le X$. 730 Thus$D \not\le C$. By$\merge$,$D \not\isin C$. OK. 732 Consider$D \neq C, M \haspatch P, D \isin Y$: 733$D \le Y$so$D \in \pancsof{Y}{\py}$so by Removal Merge Ends 734 and Transitive Ancestors$D \in \pancsof{M}{\py}$so$D \le M$. 735 Thus$D \isin M$. By$\merge$,$D \not\isin C$. OK. 737 Consider$D \neq C, M \haspatch P, D \not\isin Y$: 738 By$\merge$,$D \not\isin C$. OK. 740$\qed$742 \subsection{Base Acyclic} 744 This applies when$C \in \pn$. 745$C \in \pn$when$L \in \pn$so by Merge Acyclic,$R \nothaspatch \p$. 747 Consider some$D \in \py$. 749 By Base Acyclic of$L$,$D \not\isin L$. By the above,$D \not\isin
750 R$. And$D \neq C$. So$D \not\isin C$. 752$\qed$754 \subsection{Tip Contents} 756 We need worry only about$C \in \py$. 757 And$\patchof{C} = \patchof{L}$758 so$L \in \py$so$L \haspatch \p$. We will use the Unique Base 759 of$C$, and its Coherence and Patch Inclusion, as just proved. 761 Firstly we show$C \haspatch \p$: If$R \in \py$, then$R \haspatch
762 \p$and by Coherence/Inclusion$C \haspatch \p$. If$R \not\in \py$763 then by Tip Merge$M = \baseof{L}$so by Base Acyclic and definition 764 of$\nothaspatch$,$M \nothaspatch \p$. So by Coherence/Inclusion$C
765 \haspatch \p$(whether$R \haspatch \p$or$\nothaspatch$). 767 We will consider an arbitrary commit$D$768 and prove the Exclusive Tip Contents form. 770 \subsubsection{For$D \in \py$:} 771$C \haspatch \p$so by definition of$\haspatch$,$D \isin C \equiv D
772 \le C$. OK. 774 \subsubsection{For$D \not\in \py, R \not\in \py$:} 776$D \neq C$. By Tip Contents of$L$, 777$D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition, 778$D \isin L \equiv D \isin M$. So by definition of$\merge$,$D \isin
779 C \equiv D \isin R$. And$R = \baseof{C}$by Unique Base of$C$. 780 Thus$D \isin C \equiv D \isin \baseof{C}$. OK. 782 \subsubsection{For$D \not\in \py, R \in \py$:} 784$D \neq C$. 786 By Tip Contents 787$D \isin L \equiv D \isin \baseof{L}$and 788$D \isin R \equiv D \isin \baseof{R}$. 790 If$\baseof{L} = M$, trivially$D \isin M \equiv D \isin \baseof{L}.$791 Whereas if$\baseof{L} = \baseof{M}$, by definition of$\base$, 792$\patchof{M} = \patchof{L} = \py$, so by Tip Contents of$M$, 793$D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$. 795 So$D \isin M \equiv D \isin L$and by$\merge$, 796$D \isin C \equiv D \isin R$. But from Unique Base, 797$\baseof{C} = R$so$D \isin C \equiv D \isin \baseof{C}$. OK. 799$\qed$801 \subsection{Foreign Inclusion} 803 Consider some$D$s.t.$\patchof{D} = \bot$. 804 By Foreign Inclusion of$L, M, R$: 805$D \isin L \equiv D \le L$; 806$D \isin M \equiv D \le M$; 807$D \isin R \equiv D \le R$. 809 \subsubsection{For$D = C$:} 811$D \isin C$and$D \le C$. OK. 813 \subsubsection{For$D \neq C, D \isin M$:} 815 Thus$D \le M$so$D \le L$and$D \le R$so$D \isin L$and$D \isin
816 R$. So by$\merge$,$D \isin C$. And$D \le C$. OK. 818 \subsubsection{For$D \neq C, D \not\isin M, D \isin X$:} 820 By$\merge$,$D \isin C$. 821 And$D \isin X$means$D \le X$so$D \le C$. 822 OK. 824 \subsubsection{For$D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:} 826 By$\merge$,$D \not\isin C$. 827 And$D \not\le L, D \not\le R$so$D \not\le C$. 828 OK 830$\qed\$
832 \end{document}