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$.
605 \subsection{Foreign Inclusion}
607 Simple Foreign Inclusion applies. $\qed$
609 \subsection{Foreign Contents}
615 Given $L$ and $\pr$ as represented by $R^+, R^-$.
616 Construct $C$ which has $\pr$ removed.
617 Used for removing a branch dependency.
619 C \hasparents \{ L \}
621 \patchof{C} = \patchof{L}
623 \mergeof{C}{L}{R^+}{R^-}
626 \subsection{Conditions}
628 \[ \eqn{ Ingredients }{
629 R^+ \in \pry \land R^- = \baseof{R^+}
631 \[ \eqn{ Into Base }{
634 \[ \eqn{ Unique Tip }{
635 \pendsof{L}{\pry} = \{ R^+ \}
637 \[ \eqn{ Currently Included }{
641 \subsection{Ordering of Ingredients:}
643 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
644 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$.
647 (Note that $R^+ \not\le R^-$, i.e. the merge base
648 is a descendant, not an ancestor, of the 2nd parent.)
650 \subsection{No Replay}
652 By definition of $\merge$,
653 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
654 So, by Ordering of Ingredients,
655 Ingredients Prevent Replay applies. $\qed$
657 \subsection{Desired Contents}
659 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
662 \subsubsection{For $D = C$:}
664 Trivially $D \isin C$. OK.
666 \subsubsection{For $D \neq C, D \not\le L$:}
668 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
669 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
671 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
673 By Currently Included, $D \isin L$.
675 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
676 by Unique Tip, $D \le R^+ \equiv D \le L$.
679 By Base Acyclic, $D \not\isin R^-$.
681 Apply $\merge$: $D \not\isin C$. OK.
683 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
685 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
687 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
691 \subsection{Unique Base}
693 Into Base means that $C \in \pn$, so Unique Base is not
696 \subsection{Tip Contents}
698 Again, not applicable. $\qed$
700 \subsection{Base Acyclic}
702 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
703 And by Into Base $C \not\in \py$.
704 Now from Desired Contents, above, $D \isin C
705 \implies D \isin L \lor D = C$, which thus
706 $\implies D \not\in \py$. $\qed$.
708 \subsection{Coherence and Patch Inclusion}
710 Need to consider some $D \in \py$. By Into Base, $D \neq C$.
712 \subsubsection{For $\p = \pr$:}
713 By Desired Contents, above, $D \not\isin C$.
714 So $C \nothaspatch \pr$.
716 \subsubsection{For $\p \neq \pr$:}
717 By Desired Contents, $D \isin C \equiv D \isin L$
718 (since $D \in \py$ so $D \not\in \pry$).
720 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
721 So $L \nothaspatch \p \implies C \nothaspatch \p$.
723 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
724 so $L \haspatch \p \implies C \haspatch \p$.
728 \subsection{Foreign Inclusion}
730 Consider some $D$ s.t. $\patchof{D} = \bot$. $D \neq C$.
731 So by Desired Contents $D \isin C \equiv D \isin L$.
732 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
734 And $D \le C \equiv D \le L$.
735 Thus $D \isin C \equiv D \le C$.
739 \subsection{Foreign Contents}
745 Merge commits $L$ and $R$ using merge base $M$:
747 C \hasparents \{ L, R \}
749 \patchof{C} = \patchof{L}
753 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
755 \subsection{Conditions}
756 \[ \eqn{ Ingredients }{
759 \[ \eqn{ Tip Merge }{
762 R \in \py : & \baseof{R} \ge \baseof{L}
763 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
764 R \in \pn : & M = \baseof{L} \\
765 \text{otherwise} : & \false
768 \[ \eqn{ Merge Acyclic }{
773 \[ \eqn{ Removal Merge Ends }{
774 X \not\haspatch \p \land
778 \pendsof{Y}{\py} = \pendsof{M}{\py}
780 \[ \eqn{ Addition Merge Ends }{
781 X \not\haspatch \p \land
785 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
788 \[ \eqn{ Foreign Merges }{
789 \patchof{L} = \bot \equiv \patchof{R} = \bot
792 \subsection{Non-Topbloke merges}
794 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
795 (Foreign Merges, above).
796 I.e. not only is it forbidden to merge into a Topbloke-controlled
797 branch without Topbloke's assistance, it is also forbidden to
798 merge any Topbloke-controlled branch into any plain git branch.
800 Given those conditions, Tip Merge and Merge Acyclic do not apply.
801 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
802 Merge Ends condition applies.
804 So a plain git merge of non-Topbloke branches meets the conditions and
805 is therefore consistent with our scheme.
807 \subsection{No Replay}
809 By definition of $\merge$,
810 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
812 Ingredients Prevent Replay applies. $\qed$
814 \subsection{Unique Base}
816 Need to consider only $C \in \py$, ie $L \in \py$,
817 and calculate $\pendsof{C}{\pn}$. So we will consider some
818 putative ancestor $A \in \pn$ and see whether $A \le C$.
820 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
821 But $C \in py$ and $A \in \pn$ so $A \neq C$.
822 Thus $A \le C \equiv A \le L \lor A \le R$.
824 By Unique Base of L and Transitive Ancestors,
825 $A \le L \equiv A \le \baseof{L}$.
827 \subsubsection{For $R \in \py$:}
829 By Unique Base of $R$ and Transitive Ancestors,
830 $A \le R \equiv A \le \baseof{R}$.
832 But by Tip Merge condition on $\baseof{R}$,
833 $A \le \baseof{L} \implies A \le \baseof{R}$, so
834 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
835 Thus $A \le C \equiv A \le \baseof{R}$.
836 That is, $\baseof{C} = \baseof{R}$.
838 \subsubsection{For $R \in \pn$:}
840 By Tip Merge condition on $R$ and since $M \le R$,
841 $A \le \baseof{L} \implies A \le R$, so
842 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
843 Thus $A \le C \equiv A \le R$.
844 That is, $\baseof{C} = R$.
848 \subsection{Coherence and Patch Inclusion}
850 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
851 This involves considering $D \in \py$.
853 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
854 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
855 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
856 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
858 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
859 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
860 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
862 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
864 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
865 \equiv D \isin L \lor D \isin R$.
866 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
868 Consider $D \neq C, D \isin X \land D \isin Y$:
869 By $\merge$, $D \isin C$. Also $D \le X$
870 so $D \le C$. OK for $C \haspatch \p$.
872 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
873 By $\merge$, $D \not\isin C$.
874 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
875 OK for $C \haspatch \p$.
877 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
878 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
879 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
880 OK for $C \haspatch \p$.
882 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
884 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
886 $M \haspatch \p \implies C \nothaspatch \p$.
887 $M \nothaspatch \p \implies C \haspatch \p$.
891 One of the Merge Ends conditions applies.
892 Recall that we are considering $D \in \py$.
893 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
894 We will show for each of
895 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
896 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
898 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
899 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
900 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
901 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
903 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
904 $D \le Y$ so $D \le C$.
905 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
907 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
908 $D \not\le Y$. If $D \le X$ then
909 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
910 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
911 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
913 Consider $D \neq C, M \haspatch P, D \isin Y$:
914 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
915 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
916 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
918 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
919 By $\merge$, $D \not\isin C$. OK.
923 \subsection{Base Acyclic}
925 This applies when $C \in \pn$.
926 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
928 Consider some $D \in \py$.
930 By Base Acyclic of $L$, $D \not\isin L$. By the above, $D \not\isin
931 R$. And $D \neq C$. So $D \not\isin C$.
935 \subsection{Tip Contents}
937 We need worry only about $C \in \py$.
938 And $\patchof{C} = \patchof{L}$
939 so $L \in \py$ so $L \haspatch \p$. We will use the Unique Base
940 of $C$, and its Coherence and Patch Inclusion, as just proved.
942 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
943 \p$ and by Coherence/Inclusion $C \haspatch \p$ . If $R \not\in \py$
944 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
945 of $\nothaspatch$, $M \nothaspatch \p$. So by Coherence/Inclusion $C
946 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
948 We will consider an arbitrary commit $D$
949 and prove the Exclusive Tip Contents form.
951 \subsubsection{For $D \in \py$:}
952 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
955 \subsubsection{For $D \not\in \py, R \not\in \py$:}
957 $D \neq C$. By Tip Contents of $L$,
958 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
959 $D \isin L \equiv D \isin M$. So by definition of $\merge$, $D \isin
960 C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$.
961 Thus $D \isin C \equiv D \isin \baseof{C}$. OK.
963 \subsubsection{For $D \not\in \py, R \in \py$:}
968 $D \isin L \equiv D \isin \baseof{L}$ and
969 $D \isin R \equiv D \isin \baseof{R}$.
971 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
972 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
973 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
974 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
976 So $D \isin M \equiv D \isin L$ and by $\merge$,
977 $D \isin C \equiv D \isin R$. But from Unique Base,
978 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$. OK.
982 \subsection{Foreign Inclusion}
984 Consider some $D$ s.t. $\patchof{D} = \bot$.
985 By Foreign Inclusion of $L, M, R$:
986 $D \isin L \equiv D \le L$;
987 $D \isin M \equiv D \le M$;
988 $D \isin R \equiv D \le R$.
990 \subsubsection{For $D = C$:}
992 $D \isin C$ and $D \le C$. OK.
994 \subsubsection{For $D \neq C, D \isin M$:}
996 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
997 R$. So by $\merge$, $D \isin C$. And $D \le C$. OK.
999 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
1001 By $\merge$, $D \isin C$.
1002 And $D \isin X$ means $D \le X$ so $D \le C$.
1005 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
1007 By $\merge$, $D \not\isin C$.
1008 And $D \not\le L, D \not\le R$ so $D \not\le C$.
1013 \subsection{Foreign Contents}
1015 Only relevant if $\patchof{L} = \bot$, in which case
1016 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
1017 so Totally Foreign Contents applies. $\qed$