1 \documentclass[a4paper,leqno]{strayman}
3 \let\numberwithin=\notdef
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}{%
79 {\hbox{\huge$\forall$}}%
80 {\hbox{\Large$\forall$}}%
81 {\hbox{\normalsize$\forall$}}%
82 {\hbox{\scriptsize$\forall$}}}%
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*{}}
96 \newcommand{\false}{f}
102 \begin{basedescript}{
104 \desclabelstyle{\nextlinelabel}
106 \item[ $ C \hasparents \set X $ ]
107 The parents of commit $C$ are exactly the set
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
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
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
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
182 We maintain these each time we construct a new commit. \\
184 C \has D \implies C \ge D
186 \[\eqn{Unique Base:}{
187 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
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) }
194 \[\eqn{Base Acyclic:}{
195 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
198 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
200 \[\eqn{Foreign Inclusion:}{
201 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
203 \[\eqn{Foreign Contents:}{
204 \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
205 D \le C \implies \patchof{D} = \bot
208 \section{Some lemmas}
210 \[ \eqn{Alternative (overlapping) formulations defining
211 $\mergeof{C}{L}{M}{R}$:}{
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}
224 Original definition is symmetrical in $L$ and $R$.
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 )
232 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
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$.
238 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
239 \bigforall_{C \in \py} D \isin C \equiv
241 D \in \py : & D \le C \\
242 D \not\in \py : & D \isin \baseof{C}
246 \[ \eqn{Tip Self Inpatch:}{
247 \bigforall_{C \in \py} C \haspatch \p
249 Ie, tip commits contain their own patch.
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 $
257 \[ \eqn{Exact Ancestors:}{
258 \bigforall_{ C \hasparents \set{R} }
260 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
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]
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''$.
283 \[ \eqn{Calculation Of Ends:}{
284 \bigforall_{C \hasparents \set A}
285 \pendsof{C}{\set P} =
289 C \not\in \p : & \displaystyle
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]
300 \[ \eqn{Ingredients Prevent Replay:}{
302 {C \hasparents \set A} \land
307 \Largeexists_{A \in \set A} D \isin A
309 \right] \implies \left[
310 D \isin C \implies D \le C
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$.
320 \[ \eqn{Simple Foreign Inclusion:}{
322 C \hasparents \{ L \}
324 \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
327 \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
328 D \isin C \equiv D \le C
331 Consider some $D$ s.t. $\patchof{D} = \bot$.
332 If $D = C$, trivially true. For $D \neq C$,
333 by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
334 And by Exact Ancestors $D \le L \equiv D \le C$.
335 So $D \isin C \equiv D \le C$.
338 \[ \eqn{Totally Foreign Contents:}{
339 \bigforall_{C \hasparents \set A}
341 \patchof{C} = \bot \land
342 \bigforall_{A \in \set A} \patchof{A} = \bot
352 Consider some $D \le C$. If $D = C$, $\patchof{D} = \bot$ trivially.
353 If $D \neq C$ then $D \le A$ where $A \in \set A$. By Foreign
354 Contents of $A$, $\patchof{D} = \bot$.
357 \section{Commit annotation}
359 We annotate each Topbloke commit $C$ with:
363 \baseof{C}, \text{ if } C \in \py
366 \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
368 \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
371 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
372 in the summary in the section for that kind of commit.
374 Whether $\baseof{C}$ is required, and if so what the value is, is
375 stated in the proof of Unique Base for each kind of commit.
377 $C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
378 set $\{ \pq | C \haspatch \pq \}$. Whether $C \haspatch \pq$
380 (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
381 for the ingredients $I$),
382 in the proof of Coherence for each kind of commit.
384 $\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
385 using the lemma Calculation of Ends, above.
386 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
387 make it wrong to make plain commits with git because the recorded $\pends$
388 would have to be updated. The annotation is not needed in that case
389 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
391 \section{Simple commit}
393 A simple single-parent forward commit $C$ as made by git-commit.
395 \tag*{} C \hasparents \{ A \} \\
396 \tag*{} \patchof{C} = \patchof{A} \\
397 \tag*{} D \isin C \equiv D \isin A \lor D = C
399 This also covers Topbloke-generated commits on plain git branches:
400 Topbloke strips the metadata when exporting.
402 \subsection{No Replay}
404 Ingredients Prevent Replay applies. $\qed$
406 \subsection{Unique Base}
407 If $A, C \in \py$ then by Calculation of Ends for
408 $C, \py, C \not\in \py$:
409 $\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
410 $\baseof{C} = \baseof{A}$. $\qed$
412 \subsection{Tip Contents}
413 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
414 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
415 Substitute into the contents of $C$:
416 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
418 Since $D = C \implies D \in \py$,
419 and substituting in $\baseof{C}$, this gives:
420 \[ D \isin C \equiv D \isin \baseof{C} \lor
421 (D \in \py \land D \le A) \lor
422 (D = C \land D \in \py) \]
423 \[ \equiv D \isin \baseof{C} \lor
424 [ D \in \py \land ( D \le A \lor D = C ) ] \]
425 So by Exact Ancestors:
426 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
430 \subsection{Base Acyclic}
432 Need to consider only $A, C \in \pn$.
434 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
436 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
437 $A$, $D \isin C \implies D \not\in \py$.
441 \subsection{Coherence and patch inclusion}
443 Need to consider $D \in \py$
445 \subsubsection{For $A \haspatch P, D = C$:}
451 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
453 \subsubsection{For $A \haspatch P, D \neq C$:}
454 Ancestors: $ D \le C \equiv D \le A $.
456 Contents: $ D \isin C \equiv D \isin A \lor f $
457 so $ D \isin C \equiv D \isin A $.
460 \[ A \haspatch P \implies C \haspatch P \]
462 \subsubsection{For $A \nothaspatch P$:}
464 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
467 Now by contents of $A$, $D \notin A$, so $D \notin C$.
470 \[ A \nothaspatch P \implies C \nothaspatch P \]
473 \subsection{Foreign Inclusion:}
475 Simple Foreign Inclusion applies. $\qed$
477 \subsection{Foreign Contents:}
479 Only relevant if $\patchof{C} = \bot$, and in that case Totally
480 Foreign Contents applies. $\qed$
482 \section{Create Base}
484 Given $L$, create a Topbloke base branch initial commit $B$.
486 B \hasparents \{ L \}
490 D \isin B \equiv D \isin L \lor D = B
493 \subsection{Conditions}
495 \[ \eqn{ Ingredients }{
496 \patchof{L} = \pa{L} \lor \patchof{L} = \bot
498 \[ \eqn{ Create Acyclic }{
502 \subsection{No Replay}
504 Ingredients Prevent Replay applies. $\qed$
506 \subsection{Unique Base}
510 \subsection{Tip Contents}
514 \subsection{Base Acyclic}
516 Consider some $D \isin B$. If $D = B$, $D \in \pqn$.
517 If $D \neq B$, $D \isin L$, and by Create Acyclic
518 $D \not\in \pqy$. $\qed$
520 \subsection{Coherence and Patch Inclusion}
522 Consider some $D \in \p$.
523 $B \not\in \py$ so $D \neq B$. So $D \isin B \equiv D \isin L$
524 and $D \le B \equiv D \le L$.
526 Thus $L \haspatch \p \implies B \haspatch P$
527 and $L \nothaspatch \p \implies B \nothaspatch P$.
531 \subsection{Foreign Inclusion}
533 Simple Foreign Inclusion applies. $\qed$
535 \subsection{Foreign Contents}
541 Given a Topbloke base $B$, create a tip branch initial commit B.
543 C \hasparents \{ B \}
547 D \isin C \equiv D \isin B \lor D = C
550 \subsection{Conditions}
552 \[ \eqn{ Ingredients }{
556 \pendsof{B}{\pqy} = \{ \}
559 \subsection{No Replay}
561 Ingredients Prevent Replay applies. $\qed$
563 \subsection{Unique Base}
565 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$. $\qed$
567 \subsection{Tip Contents}
569 Consider some arbitrary commit $D$. If $D = C$, trivially satisfied.
571 If $D \neq C$, $D \isin C \equiv D \isin B$.
572 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
573 So $D \isin C \equiv D \isin \baseof{B}$.
577 \subsection{Base Acyclic}
581 \subsection{Coherence and Patch Inclusion}
585 \p = \pq \lor B \haspatch \p : & C \haspatch \p \\
586 \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
591 ~ Consider some $D \in \py$.
593 \subsubsection{For $\p = \pq$:}
595 By Base Acyclic, $D \not\isin B$. So $D \isin C \equiv D = C$.
596 By No Sneak, $D \le B \equiv D = C$. Thus $C \haspatch \pq$.
598 \subsubsection{For $\p \neq \pq$:}
600 $D \neq C$. So $D \isin C \equiv D \isin B$,
601 and $D \le C \equiv D \le B$.
609 Given $L$ and $\pr$ as represented by $R^+, R^-$.
610 Construct $C$ which has $\pr$ removed.
611 Used for removing a branch dependency.
613 C \hasparents \{ L \}
615 \patchof{C} = \patchof{L}
617 \mergeof{C}{L}{R^+}{R^-}
620 \subsection{Conditions}
622 \[ \eqn{ Ingredients }{
623 R^+ \in \pry \land R^- = \baseof{R^+}
625 \[ \eqn{ Into Base }{
628 \[ \eqn{ Unique Tip }{
629 \pendsof{L}{\pry} = \{ R^+ \}
631 \[ \eqn{ Currently Included }{
635 \subsection{Ordering of Ingredients:}
637 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
638 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$.
641 (Note that $R^+ \not\le R^-$, i.e. the merge base
642 is a descendant, not an ancestor, of the 2nd parent.)
644 \subsection{No Replay}
646 By definition of $\merge$,
647 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
648 So, by Ordering of Ingredients,
649 Ingredients Prevent Replay applies. $\qed$
651 \subsection{Desired Contents}
653 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
656 \subsubsection{For $D = C$:}
658 Trivially $D \isin C$. OK.
660 \subsubsection{For $D \neq C, D \not\le L$:}
662 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
663 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
665 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
667 By Currently Included, $D \isin L$.
669 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
670 by Unique Tip, $D \le R^+ \equiv D \le L$.
673 By Base Acyclic, $D \not\isin R^-$.
675 Apply $\merge$: $D \not\isin C$. OK.
677 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
679 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
681 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
685 \subsection{Unique Base}
687 Into Base means that $C \in \pn$, so Unique Base is not
690 \subsection{Tip Contents}
692 Again, not applicable. $\qed$
694 \subsection{Base Acyclic}
696 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
697 And by Into Base $C \not\in \py$.
698 Now from Desired Contents, above, $D \isin C
699 \implies D \isin L \lor D = C$, which thus
700 $\implies D \not\in \py$. $\qed$.
702 \subsection{Coherence and Patch Inclusion}
704 Need to consider some $D \in \py$. By Into Base, $D \neq C$.
706 \subsubsection{For $\p = \pr$:}
707 By Desired Contents, above, $D \not\isin C$.
708 So $C \nothaspatch \pr$.
710 \subsubsection{For $\p \neq \pr$:}
711 By Desired Contents, $D \isin C \equiv D \isin L$
712 (since $D \in \py$ so $D \not\in \pry$).
714 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
715 So $L \nothaspatch \p \implies C \nothaspatch \p$.
717 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
718 so $L \haspatch \p \implies C \haspatch \p$.
722 \subsection{Foreign Inclusion}
724 Consider some $D$ s.t. $\patchof{D} = \bot$. $D \neq C$.
725 So by Desired Contents $D \isin C \equiv D \isin L$.
726 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
728 And $D \le C \equiv D \le L$.
729 Thus $D \isin C \equiv D \le C$.
733 \subsection{Foreign Contents}
739 Merge commits $L$ and $R$ using merge base $M$:
741 C \hasparents \{ L, R \}
743 \patchof{C} = \patchof{L}
747 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
749 \subsection{Conditions}
750 \[ \eqn{ Ingredients }{
753 \[ \eqn{ Tip Merge }{
756 R \in \py : & \baseof{R} \ge \baseof{L}
757 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
758 R \in \pn : & M = \baseof{L} \\
759 \text{otherwise} : & \false
762 \[ \eqn{ Merge Acyclic }{
767 \[ \eqn{ Removal Merge Ends }{
768 X \not\haspatch \p \land
772 \pendsof{Y}{\py} = \pendsof{M}{\py}
774 \[ \eqn{ Addition Merge Ends }{
775 X \not\haspatch \p \land
779 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
782 \[ \eqn{ Foreign Merges }{
783 \patchof{L} = \bot \equiv \patchof{R} = \bot
786 \subsection{Non-Topbloke merges}
788 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
789 (Foreign Merges, above).
790 I.e. not only is it forbidden to merge into a Topbloke-controlled
791 branch without Topbloke's assistance, it is also forbidden to
792 merge any Topbloke-controlled branch into any plain git branch.
794 Given those conditions, Tip Merge and Merge Acyclic do not apply.
795 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
796 Merge Ends condition applies.
798 So a plain git merge of non-Topbloke branches meets the conditions and
799 is therefore consistent with our scheme.
801 \subsection{No Replay}
803 By definition of $\merge$,
804 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
806 Ingredients Prevent Replay applies. $\qed$
808 \subsection{Unique Base}
810 Need to consider only $C \in \py$, ie $L \in \py$,
811 and calculate $\pendsof{C}{\pn}$. So we will consider some
812 putative ancestor $A \in \pn$ and see whether $A \le C$.
814 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
815 But $C \in py$ and $A \in \pn$ so $A \neq C$.
816 Thus $A \le C \equiv A \le L \lor A \le R$.
818 By Unique Base of L and Transitive Ancestors,
819 $A \le L \equiv A \le \baseof{L}$.
821 \subsubsection{For $R \in \py$:}
823 By Unique Base of $R$ and Transitive Ancestors,
824 $A \le R \equiv A \le \baseof{R}$.
826 But by Tip Merge condition on $\baseof{R}$,
827 $A \le \baseof{L} \implies A \le \baseof{R}$, so
828 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
829 Thus $A \le C \equiv A \le \baseof{R}$.
830 That is, $\baseof{C} = \baseof{R}$.
832 \subsubsection{For $R \in \pn$:}
834 By Tip Merge condition on $R$ and since $M \le R$,
835 $A \le \baseof{L} \implies A \le R$, so
836 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
837 Thus $A \le C \equiv A \le R$.
838 That is, $\baseof{C} = R$.
842 \subsection{Coherence and Patch Inclusion}
844 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
845 This involves considering $D \in \py$.
847 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
848 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
849 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
850 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
852 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
853 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
854 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
856 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
858 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
859 \equiv D \isin L \lor D \isin R$.
860 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
862 Consider $D \neq C, D \isin X \land D \isin Y$:
863 By $\merge$, $D \isin C$. Also $D \le X$
864 so $D \le C$. OK for $C \haspatch \p$.
866 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
867 By $\merge$, $D \not\isin C$.
868 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
869 OK for $C \haspatch \p$.
871 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
872 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
873 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
874 OK for $C \haspatch \p$.
876 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
878 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
880 $M \haspatch \p \implies C \nothaspatch \p$.
881 $M \nothaspatch \p \implies C \haspatch \p$.
885 One of the Merge Ends conditions applies.
886 Recall that we are considering $D \in \py$.
887 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
888 We will show for each of
889 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
890 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
892 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
893 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
894 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
895 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
897 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
898 $D \le Y$ so $D \le C$.
899 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
901 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
902 $D \not\le Y$. If $D \le X$ then
903 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
904 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
905 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
907 Consider $D \neq C, M \haspatch P, D \isin Y$:
908 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
909 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
910 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
912 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
913 By $\merge$, $D \not\isin C$. OK.
917 \subsection{Base Acyclic}
919 This applies when $C \in \pn$.
920 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
922 Consider some $D \in \py$.
924 By Base Acyclic of $L$, $D \not\isin L$. By the above, $D \not\isin
925 R$. And $D \neq C$. So $D \not\isin C$.
929 \subsection{Tip Contents}
931 We need worry only about $C \in \py$.
932 And $\patchof{C} = \patchof{L}$
933 so $L \in \py$ so $L \haspatch \p$. We will use the Unique Base
934 of $C$, and its Coherence and Patch Inclusion, as just proved.
936 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
937 \p$ and by Coherence/Inclusion $C \haspatch \p$ . If $R \not\in \py$
938 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
939 of $\nothaspatch$, $M \nothaspatch \p$. So by Coherence/Inclusion $C
940 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
942 We will consider an arbitrary commit $D$
943 and prove the Exclusive Tip Contents form.
945 \subsubsection{For $D \in \py$:}
946 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
949 \subsubsection{For $D \not\in \py, R \not\in \py$:}
951 $D \neq C$. By Tip Contents of $L$,
952 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
953 $D \isin L \equiv D \isin M$. So by definition of $\merge$, $D \isin
954 C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$.
955 Thus $D \isin C \equiv D \isin \baseof{C}$. OK.
957 \subsubsection{For $D \not\in \py, R \in \py$:}
962 $D \isin L \equiv D \isin \baseof{L}$ and
963 $D \isin R \equiv D \isin \baseof{R}$.
965 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
966 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
967 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
968 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
970 So $D \isin M \equiv D \isin L$ and by $\merge$,
971 $D \isin C \equiv D \isin R$. But from Unique Base,
972 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$. OK.
976 \subsection{Foreign Inclusion}
978 Consider some $D$ s.t. $\patchof{D} = \bot$.
979 By Foreign Inclusion of $L, M, R$:
980 $D \isin L \equiv D \le L$;
981 $D \isin M \equiv D \le M$;
982 $D \isin R \equiv D \le R$.
984 \subsubsection{For $D = C$:}
986 $D \isin C$ and $D \le C$. OK.
988 \subsubsection{For $D \neq C, D \isin M$:}
990 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
991 R$. So by $\merge$, $D \isin C$. And $D \le C$. OK.
993 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
995 By $\merge$, $D \isin C$.
996 And $D \isin X$ means $D \le X$ so $D \le C$.
999 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
1001 By $\merge$, $D \not\isin C$.
1002 And $D \not\le L, D \not\le R$ so $D \not\le C$.
1007 \subsection{Foreign Contents}
1009 Only relevant if $\patchof{L} = \bot$, in which case
1010 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
1011 so Totally Foreign Contents applies. $\qed$