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}
221 \proof{ ~ Truth table (ordered by original definition): \\
222 \begin{tabular}{cccc|c|cc}
226 $\isin R$ & $\isin C$ &
227 $L$ vs. $R$ & $L$ vs. $M$
229 y & ? & ? & ? & y & ? & ? \\
230 n & y & y & y & y & $\equiv$ & $\equiv$ \\
231 n & y & n & y & y & $\equiv$ & $\nequiv$ \\
232 n & n & y & n & n & $\equiv$ & $\nequiv$ \\
233 n & n & n & n & n & $\equiv$ & $\equiv$ \\
234 n & y & y & n & n & $\nequiv$ & $\equiv$ \\
235 n & n & y & y & n & $\nequiv$ & $\nequiv$ \\
236 n & y & n & n & y & $\nequiv$ & $\nequiv$ \\
237 n & n & n & y & y & $\nequiv$ & $\equiv$ \\
239 And original definition is symmetrical in $L$ and $R$.
242 \[ \eqn{Exclusive Tip Contents:}{
243 \bigforall_{C \in \py}
244 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
247 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
250 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
251 So by Base Acyclic $D \isin B \implies D \notin \py$.
253 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
254 \bigforall_{C \in \py} D \isin C \equiv
256 D \in \py : & D \le C \\
257 D \not\in \py : & D \isin \baseof{C}
261 \[ \eqn{Tip Self Inpatch:}{
262 \bigforall_{C \in \py} C \haspatch \p
264 Ie, tip commits contain their own patch.
267 Apply Exclusive Tip Contents to some $D \in \py$:
268 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
269 D \isin C \equiv D \le C $
272 \[ \eqn{Exact Ancestors:}{
273 \bigforall_{ C \hasparents \set{R} }
275 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
280 \[ \eqn{Transitive Ancestors:}{
281 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
282 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
286 The implication from right to left is trivial because
287 $ \pends() \subset \pancs() $.
288 For the implication from left to right:
289 by the definition of $\mathcal E$,
290 for every such $A$, either $A \in \pends()$ which implies
291 $A \le M$ by the LHS directly,
292 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
293 in which case we repeat for $A'$. Since there are finitely many
294 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
295 by the LHS. And $A \le A''$.
298 \[ \eqn{Calculation Of Ends:}{
299 \bigforall_{C \hasparents \set A}
300 \pendsof{C}{\set P} =
304 C \not\in \p : & \displaystyle
306 \Bigl[ \Largeexists_{A \in \set A}
307 E \in \pendsof{A}{\set P} \Bigr] \land
308 \Bigl[ \Largenexists_{B \in \set A}
309 E \neq B \land E \le B \Bigr]
315 \[ \eqn{Ingredients Prevent Replay:}{
317 {C \hasparents \set A} \land
322 \Largeexists_{A \in \set A} D \isin A
324 \right] \implies \left[
325 D \isin C \implies D \le C
329 Trivial for $D = C$. Consider some $D \neq C$, $D \isin C$.
330 By the preconditions, there is some $A$ s.t. $D \in \set A$
331 and $D \isin A$. By No Replay for $A$, $D \le A$. And
332 $A \le C$ so $D \le C$.
335 \[ \eqn{Simple Foreign Inclusion:}{
337 C \hasparents \{ L \}
339 \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
342 \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
343 D \isin C \equiv D \le C
346 Consider some $D$ s.t. $\patchof{D} = \bot$.
347 If $D = C$, trivially true. For $D \neq C$,
348 by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
349 And by Exact Ancestors $D \le L \equiv D \le C$.
350 So $D \isin C \equiv D \le C$.
353 \[ \eqn{Totally Foreign Contents:}{
354 \bigforall_{C \hasparents \set A}
356 \patchof{C} = \bot \land
357 \bigforall_{A \in \set A} \patchof{A} = \bot
367 Consider some $D \le C$. If $D = C$, $\patchof{D} = \bot$ trivially.
368 If $D \neq C$ then $D \le A$ where $A \in \set A$. By Foreign
369 Contents of $A$, $\patchof{D} = \bot$.
372 \section{Commit annotation}
374 We annotate each Topbloke commit $C$ with:
378 \baseof{C}, \text{ if } C \in \py
381 \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
383 \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
386 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
387 in the summary in the section for that kind of commit.
389 Whether $\baseof{C}$ is required, and if so what the value is, is
390 stated in the proof of Unique Base for each kind of commit.
392 $C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
393 set $\{ \pq | C \haspatch \pq \}$. Whether $C \haspatch \pq$
395 (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
396 for the ingredients $I$),
397 in the proof of Coherence for each kind of commit.
399 $\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
400 using the lemma Calculation of Ends, above.
401 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
402 make it wrong to make plain commits with git because the recorded $\pends$
403 would have to be updated. The annotation is not needed in that case
404 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
406 \section{Simple commit}
408 A simple single-parent forward commit $C$ as made by git-commit.
410 \tag*{} C \hasparents \{ A \} \\
411 \tag*{} \patchof{C} = \patchof{A} \\
412 \tag*{} D \isin C \equiv D \isin A \lor D = C
414 This also covers Topbloke-generated commits on plain git branches:
415 Topbloke strips the metadata when exporting.
417 \subsection{No Replay}
419 Ingredients Prevent Replay applies. $\qed$
421 \subsection{Unique Base}
422 If $A, C \in \py$ then by Calculation of Ends for
423 $C, \py, C \not\in \py$:
424 $\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
425 $\baseof{C} = \baseof{A}$. $\qed$
427 \subsection{Tip Contents}
428 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
429 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
430 Substitute into the contents of $C$:
431 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
433 Since $D = C \implies D \in \py$,
434 and substituting in $\baseof{C}$, this gives:
435 \[ D \isin C \equiv D \isin \baseof{C} \lor
436 (D \in \py \land D \le A) \lor
437 (D = C \land D \in \py) \]
438 \[ \equiv D \isin \baseof{C} \lor
439 [ D \in \py \land ( D \le A \lor D = C ) ] \]
440 So by Exact Ancestors:
441 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
445 \subsection{Base Acyclic}
447 Need to consider only $A, C \in \pn$.
449 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
451 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
452 $A$, $D \isin C \implies D \not\in \py$.
456 \subsection{Coherence and patch inclusion}
458 Need to consider $D \in \py$
460 \subsubsection{For $A \haspatch P, D = C$:}
466 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
468 \subsubsection{For $A \haspatch P, D \neq C$:}
469 Ancestors: $ D \le C \equiv D \le A $.
471 Contents: $ D \isin C \equiv D \isin A \lor f $
472 so $ D \isin C \equiv D \isin A $.
475 \[ A \haspatch P \implies C \haspatch P \]
477 \subsubsection{For $A \nothaspatch P$:}
479 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
482 Now by contents of $A$, $D \notin A$, so $D \notin C$.
485 \[ A \nothaspatch P \implies C \nothaspatch P \]
488 \subsection{Foreign Inclusion:}
490 Simple Foreign Inclusion applies. $\qed$
492 \subsection{Foreign Contents:}
494 Only relevant if $\patchof{C} = \bot$, and in that case Totally
495 Foreign Contents applies. $\qed$
497 \section{Create Base}
499 Given $L$, create a Topbloke base branch initial commit $B$.
501 B \hasparents \{ L \}
505 D \isin B \equiv D \isin L \lor D = B
508 \subsection{Conditions}
510 \[ \eqn{ Ingredients }{
511 \patchof{L} = \pa{L} \lor \patchof{L} = \bot
513 \[ \eqn{ Create Acyclic }{
517 \subsection{No Replay}
519 Ingredients Prevent Replay applies. $\qed$
521 \subsection{Unique Base}
525 \subsection{Tip Contents}
529 \subsection{Base Acyclic}
531 Consider some $D \isin B$. If $D = B$, $D \in \pqn$.
532 If $D \neq B$, $D \isin L$, and by Create Acyclic
533 $D \not\in \pqy$. $\qed$
535 \subsection{Coherence and Patch Inclusion}
537 Consider some $D \in \p$.
538 $B \not\in \py$ so $D \neq B$. So $D \isin B \equiv D \isin L$
539 and $D \le B \equiv D \le L$.
541 Thus $L \haspatch \p \implies B \haspatch P$
542 and $L \nothaspatch \p \implies B \nothaspatch P$.
546 \subsection{Foreign Inclusion}
548 Simple Foreign Inclusion applies. $\qed$
550 \subsection{Foreign Contents}
556 Given a Topbloke base $B$, create a tip branch initial commit B.
558 C \hasparents \{ B \}
562 D \isin C \equiv D \isin B \lor D = C
565 \subsection{Conditions}
567 \[ \eqn{ Ingredients }{
571 \pendsof{B}{\pqy} = \{ \}
574 \subsection{No Replay}
576 Ingredients Prevent Replay applies. $\qed$
578 \subsection{Unique Base}
580 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$. $\qed$
582 \subsection{Tip Contents}
584 Consider some arbitrary commit $D$. If $D = C$, trivially satisfied.
586 If $D \neq C$, $D \isin C \equiv D \isin B$.
587 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
588 So $D \isin C \equiv D \isin \baseof{B}$.
592 \subsection{Base Acyclic}
596 \subsection{Coherence and Patch Inclusion}
600 \p = \pq \lor B \haspatch \p : & C \haspatch \p \\
601 \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
606 ~ Consider some $D \in \py$.
608 \subsubsection{For $\p = \pq$:}
610 By Base Acyclic, $D \not\isin B$. So $D \isin C \equiv D = C$.
611 By No Sneak, $D \le B \equiv D = C$. Thus $C \haspatch \pq$.
613 \subsubsection{For $\p \neq \pq$:}
615 $D \neq C$. So $D \isin C \equiv D \isin B$,
616 and $D \le C \equiv D \le B$.
620 \subsection{Foreign Inclusion}
622 Simple Foreign Inclusion applies. $\qed$
624 \subsection{Foreign Contents}
630 Given $L$ and $\pr$ as represented by $R^+, R^-$.
631 Construct $C$ which has $\pr$ removed.
632 Used for removing a branch dependency.
634 C \hasparents \{ L \}
636 \patchof{C} = \patchof{L}
638 \mergeof{C}{L}{R^+}{R^-}
641 \subsection{Conditions}
643 \[ \eqn{ Ingredients }{
644 R^+ \in \pry \land R^- = \baseof{R^+}
646 \[ \eqn{ Into Base }{
649 \[ \eqn{ Unique Tip }{
650 \pendsof{L}{\pry} = \{ R^+ \}
652 \[ \eqn{ Currently Included }{
656 \subsection{Ordering of Ingredients:}
658 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
659 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$.
662 (Note that $R^+ \not\le R^-$, i.e. the merge base
663 is a descendant, not an ancestor, of the 2nd parent.)
665 \subsection{No Replay}
667 By definition of $\merge$,
668 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
669 So, by Ordering of Ingredients,
670 Ingredients Prevent Replay applies. $\qed$
672 \subsection{Desired Contents}
674 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
677 \subsubsection{For $D = C$:}
679 Trivially $D \isin C$. OK.
681 \subsubsection{For $D \neq C, D \not\le L$:}
683 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
684 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
686 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
688 By Currently Included, $D \isin L$.
690 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
691 by Unique Tip, $D \le R^+ \equiv D \le L$.
694 By Base Acyclic, $D \not\isin R^-$.
696 Apply $\merge$: $D \not\isin C$. OK.
698 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
700 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
702 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
706 \subsection{Unique Base}
708 Into Base means that $C \in \pn$, so Unique Base is not
711 \subsection{Tip Contents}
713 Again, not applicable. $\qed$
715 \subsection{Base Acyclic}
717 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
718 And by Into Base $C \not\in \py$.
719 Now from Desired Contents, above, $D \isin C
720 \implies D \isin L \lor D = C$, which thus
721 $\implies D \not\in \py$. $\qed$.
723 \subsection{Coherence and Patch Inclusion}
725 Need to consider some $D \in \py$. By Into Base, $D \neq C$.
727 \subsubsection{For $\p = \pr$:}
728 By Desired Contents, above, $D \not\isin C$.
729 So $C \nothaspatch \pr$.
731 \subsubsection{For $\p \neq \pr$:}
732 By Desired Contents, $D \isin C \equiv D \isin L$
733 (since $D \in \py$ so $D \not\in \pry$).
735 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
736 So $L \nothaspatch \p \implies C \nothaspatch \p$.
738 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
739 so $L \haspatch \p \implies C \haspatch \p$.
743 \subsection{Foreign Inclusion}
745 Consider some $D$ s.t. $\patchof{D} = \bot$. $D \neq C$.
746 So by Desired Contents $D \isin C \equiv D \isin L$.
747 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
749 And $D \le C \equiv D \le L$.
750 Thus $D \isin C \equiv D \le C$.
754 \subsection{Foreign Contents}
760 Merge commits $L$ and $R$ using merge base $M$:
762 C \hasparents \{ L, R \}
764 \patchof{C} = \patchof{L}
768 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
770 \subsection{Conditions}
771 \[ \eqn{ Ingredients }{
774 \[ \eqn{ Tip Merge }{
777 R \in \py : & \baseof{R} \ge \baseof{L}
778 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
779 R \in \pn : & M = \baseof{L} \\
780 \text{otherwise} : & \false
783 \[ \eqn{ Merge Acyclic }{
788 \[ \eqn{ Removal Merge Ends }{
789 X \not\haspatch \p \land
793 \pendsof{Y}{\py} = \pendsof{M}{\py}
795 \[ \eqn{ Addition Merge Ends }{
796 X \not\haspatch \p \land
800 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
803 \[ \eqn{ Foreign Merges }{
804 \patchof{L} = \bot \equiv \patchof{R} = \bot
807 \subsection{Non-Topbloke merges}
809 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
810 (Foreign Merges, above).
811 I.e. not only is it forbidden to merge into a Topbloke-controlled
812 branch without Topbloke's assistance, it is also forbidden to
813 merge any Topbloke-controlled branch into any plain git branch.
815 Given those conditions, Tip Merge and Merge Acyclic do not apply.
816 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
817 Merge Ends condition applies.
819 So a plain git merge of non-Topbloke branches meets the conditions and
820 is therefore consistent with our scheme.
822 \subsection{No Replay}
824 By definition of $\merge$,
825 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
827 Ingredients Prevent Replay applies. $\qed$
829 \subsection{Unique Base}
831 Need to consider only $C \in \py$, ie $L \in \py$,
832 and calculate $\pendsof{C}{\pn}$. So we will consider some
833 putative ancestor $A \in \pn$ and see whether $A \le C$.
835 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
836 But $C \in py$ and $A \in \pn$ so $A \neq C$.
837 Thus $A \le C \equiv A \le L \lor A \le R$.
839 By Unique Base of L and Transitive Ancestors,
840 $A \le L \equiv A \le \baseof{L}$.
842 \subsubsection{For $R \in \py$:}
844 By Unique Base of $R$ and Transitive Ancestors,
845 $A \le R \equiv A \le \baseof{R}$.
847 But by Tip Merge condition on $\baseof{R}$,
848 $A \le \baseof{L} \implies A \le \baseof{R}$, so
849 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
850 Thus $A \le C \equiv A \le \baseof{R}$.
851 That is, $\baseof{C} = \baseof{R}$.
853 \subsubsection{For $R \in \pn$:}
855 By Tip Merge condition on $R$ and since $M \le R$,
856 $A \le \baseof{L} \implies A \le R$, so
857 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
858 Thus $A \le C \equiv A \le R$.
859 That is, $\baseof{C} = R$.
863 \subsection{Coherence and Patch Inclusion}
865 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
866 This involves considering $D \in \py$.
868 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
869 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
870 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
871 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
873 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
874 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
875 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
877 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
879 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
880 \equiv D \isin L \lor D \isin R$.
881 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
883 Consider $D \neq C, D \isin X \land D \isin Y$:
884 By $\merge$, $D \isin C$. Also $D \le X$
885 so $D \le C$. OK for $C \haspatch \p$.
887 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
888 By $\merge$, $D \not\isin C$.
889 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
890 OK for $C \haspatch \p$.
892 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
893 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
894 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
895 OK for $C \haspatch \p$.
897 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
899 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
901 $M \haspatch \p \implies C \nothaspatch \p$.
902 $M \nothaspatch \p \implies C \haspatch \p$.
906 One of the Merge Ends conditions applies.
907 Recall that we are considering $D \in \py$.
908 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
909 We will show for each of
910 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
911 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
913 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
914 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
915 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
916 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
918 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
919 $D \le Y$ so $D \le C$.
920 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
922 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
923 $D \not\le Y$. If $D \le X$ then
924 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
925 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
926 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
928 Consider $D \neq C, M \haspatch P, D \isin Y$:
929 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
930 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
931 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
933 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
934 By $\merge$, $D \not\isin C$. OK.
938 \subsection{Base Acyclic}
940 This applies when $C \in \pn$.
941 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
943 Consider some $D \in \py$.
945 By Base Acyclic of $L$, $D \not\isin L$. By the above, $D \not\isin
946 R$. And $D \neq C$. So $D \not\isin C$.
950 \subsection{Tip Contents}
952 We need worry only about $C \in \py$.
953 And $\patchof{C} = \patchof{L}$
954 so $L \in \py$ so $L \haspatch \p$. We will use the Unique Base
955 of $C$, and its Coherence and Patch Inclusion, as just proved.
957 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
958 \p$ and by Coherence/Inclusion $C \haspatch \p$ . If $R \not\in \py$
959 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
960 of $\nothaspatch$, $M \nothaspatch \p$. So by Coherence/Inclusion $C
961 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
963 We will consider an arbitrary commit $D$
964 and prove the Exclusive Tip Contents form.
966 \subsubsection{For $D \in \py$:}
967 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
970 \subsubsection{For $D \not\in \py, R \not\in \py$:}
972 $D \neq C$. By Tip Contents of $L$,
973 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
974 $D \isin L \equiv D \isin M$. So by definition of $\merge$, $D \isin
975 C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$.
976 Thus $D \isin C \equiv D \isin \baseof{C}$. OK.
978 \subsubsection{For $D \not\in \py, R \in \py$:}
983 $D \isin L \equiv D \isin \baseof{L}$ and
984 $D \isin R \equiv D \isin \baseof{R}$.
986 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
987 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
988 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
989 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
991 So $D \isin M \equiv D \isin L$ and by $\merge$,
992 $D \isin C \equiv D \isin R$. But from Unique Base,
993 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$. OK.
997 \subsection{Foreign Inclusion}
999 Consider some $D$ s.t. $\patchof{D} = \bot$.
1000 By Foreign Inclusion of $L, M, R$:
1001 $D \isin L \equiv D \le L$;
1002 $D \isin M \equiv D \le M$;
1003 $D \isin R \equiv D \le R$.
1005 \subsubsection{For $D = C$:}
1007 $D \isin C$ and $D \le C$. OK.
1009 \subsubsection{For $D \neq C, D \isin M$:}
1011 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
1012 R$. So by $\merge$, $D \isin C$. And $D \le C$. OK.
1014 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
1016 By $\merge$, $D \isin C$.
1017 And $D \isin X$ means $D \le X$ so $D \le C$.
1020 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
1022 By $\merge$, $D \not\isin C$.
1023 And $D \not\le L, D \not\le R$ so $D \not\le C$.
1028 \subsection{Foreign Contents}
1030 Only relevant if $\patchof{L} = \bot$, in which case
1031 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
1032 so Totally Foreign Contents applies. $\qed$