1 \documentclass[a4paper,leqno]{strayman}
3 \let\numberwithin=\notdef
15 \let\stdsection\section
16 \renewcommand\section{\newpage\stdsection}
18 \renewcommand{\ge}{\geqslant}
19 \renewcommand{\le}{\leqslant}
20 \newcommand{\nge}{\ngeqslant}
21 \newcommand{\nle}{\nleqslant}
23 \newcommand{\has}{\sqsupseteq}
24 \newcommand{\isin}{\sqsubseteq}
26 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
27 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
28 \newcommand{\haspatch}{\sqSupset}
29 \newcommand{\patchisin}{\sqSubset}
31 \newif\ifhidehack\hidehackfalse
32 \DeclareRobustCommand\hidefromedef[2]{%
33 \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
34 \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
36 \newcommand{\set}[1]{\mathbb{#1}}
37 \newcommand{\pay}[1]{\pa{#1}^+}
38 \newcommand{\pan}[1]{\pa{#1}^-}
40 \newcommand{\p}{\pa{P}}
41 \newcommand{\py}{\pay{P}}
42 \newcommand{\pn}{\pan{P}}
44 \newcommand{\pq}{\pa{Q}}
45 \newcommand{\pqy}{\pay{Q}}
46 \newcommand{\pqn}{\pan{Q}}
48 \newcommand{\pr}{\pa{R}}
49 \newcommand{\pry}{\pay{R}}
50 \newcommand{\prn}{\pan{R}}
52 %\newcommand{\hasparents}{\underaccent{1}{>}}
53 %\newcommand{\hasparents}{{%
54 % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
55 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
56 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
58 \renewcommand{\implies}{\Rightarrow}
59 \renewcommand{\equiv}{\Leftrightarrow}
60 \renewcommand{\nequiv}{\nLeftrightarrow}
61 \renewcommand{\land}{\wedge}
62 \renewcommand{\lor}{\vee}
64 \newcommand{\pancs}{{\mathcal A}}
65 \newcommand{\pends}{{\mathcal E}}
67 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
68 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
70 \newcommand{\merge}{{\mathcal M}}
71 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
72 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
74 \newcommand{\patch}{{\mathcal P}}
75 \newcommand{\base}{{\mathcal B}}
77 \newcommand{\patchof}[1]{\patch ( #1 ) }
78 \newcommand{\baseof}[1]{\base ( #1 ) }
80 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
81 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
83 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
84 \newcommand{\bigforall}{%
86 {\hbox{\huge$\forall$}}%
87 {\hbox{\Large$\forall$}}%
88 {\hbox{\normalsize$\forall$}}%
89 {\hbox{\scriptsize$\forall$}}}%
92 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
93 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
95 \newcommand{\qed}{\square}
96 \newcommand{\proofstarts}{{\it Proof:}}
97 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
99 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
100 \newcommand{\gathnext}{\\ \tag*{}}
102 \newcommand{\true}{t}
103 \newcommand{\false}{f}
109 \begin{basedescript}{
111 \desclabelstyle{\nextlinelabel}
113 \item[ $ C \hasparents \set X $ ]
114 The parents of commit $C$ are exactly the set
118 $C$ is a descendant of $D$ in the git commit
119 graph. This is a partial order, namely the transitive closure of
120 $ D \in \set X $ where $ C \hasparents \set X $.
122 \item[ $ C \has D $ ]
123 Informally, the tree at commit $C$ contains the change
124 made in commit $D$. Does not take account of deliberate reversions by
125 the user or reversion, rebasing or rewinding in
126 non-Topbloke-controlled branches. For merges and Topbloke-generated
127 anticommits or re-commits, the ``change made'' is only to be thought
128 of as any conflict resolution. This is not a partial order because it
131 \item[ $ \p, \py, \pn $ ]
132 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
133 are respectively the base and tip git branches. $\p$ may be used
134 where the context requires a set, in which case the statement
135 is to be taken as applying to both $\py$ and $\pn$.
136 None of these sets overlap. Hence:
138 \item[ $ \patchof{ C } $ ]
139 Either $\p$ s.t. $ C \in \p $, or $\bot$.
140 A function from commits to patches' sets $\p$.
142 \item[ $ \pancsof{C}{\set P} $ ]
143 $ \{ A \; | \; A \le C \land A \in \set P \} $
144 i.e. all the ancestors of $C$
145 which are in $\set P$.
147 \item[ $ \pendsof{C}{\set P} $ ]
148 $ \{ E \; | \; E \in \pancsof{C}{\set P}
149 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
150 E \neq A \land E \le A \} $
151 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
153 \item[ $ \baseof{C} $ ]
154 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
155 A partial function from commits to commits.
156 See Unique Base, below.
158 \item[ $ C \haspatch \p $ ]
159 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
160 ~ Informally, $C$ has the contents of $\p$.
162 \item[ $ C \nothaspatch \p $ ]
163 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
164 ~ Informally, $C$ has none of the contents of $\p$.
166 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$. This
167 includes commits on plain git branches made by applying a Topbloke
169 patch is applied to a non-Topbloke branch and then bubbles back to
170 the relevant Topbloke branches, we hope that
171 if the user still cares about the Topbloke patch,
172 git's merge algorithm will DTRT when trying to re-apply the changes.
174 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
175 The contents of a git merge result:
177 $\displaystyle D \isin C \equiv
179 (D \isin L \land D \isin R) \lor D = C : & \true \\
180 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
181 \text{otherwise} : & D \not\isin M
189 We maintain these each time we construct a new commit. \\
191 C \has D \implies C \ge D
193 \[\eqn{Unique Base:}{
194 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
196 \[\eqn{Tip Contents:}{
197 \bigforall_{C \in \py} D \isin C \equiv
198 { D \isin \baseof{C} \lor \atop
199 (D \in \py \land D \le C) }
201 \[\eqn{Base Acyclic:}{
202 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
205 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
207 \[\eqn{Foreign Inclusion:}{
208 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
210 \[\eqn{Foreign Contents:}{
211 \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
212 D \le C \implies \patchof{D} = \bot
215 \section{Some lemmas}
217 \subsection{Alternative (overlapping) formulations of $\mergeof{C}{L}{M}{R}$}
221 D \isin L \equiv D \isin R : & D = C \lor D \isin L \\
222 D \isin L \nequiv D \isin R : & D = C \lor D \not\isin M \\
223 D \isin L \equiv D \isin M : & D = C \lor D \isin R \\
224 D \isin L \nequiv D \isin M : & D = C \lor D \isin L \\
225 \text{as above with L and R exchanged}
228 \proof{ ~ Truth table (ordered by original definition): \\
229 \begin{tabular}{cccc|c|cc}
233 $\isin R$ & $\isin C$ &
234 $L$ vs. $R$ & $L$ vs. $M$
236 y & ? & ? & ? & y & ? & ? \\
237 n & y & y & y & y & $\equiv$ & $\equiv$ \\
238 n & y & n & y & y & $\equiv$ & $\nequiv$ \\
239 n & n & y & n & n & $\equiv$ & $\nequiv$ \\
240 n & n & n & n & n & $\equiv$ & $\equiv$ \\
241 n & y & y & n & n & $\nequiv$ & $\equiv$ \\
242 n & n & y & y & n & $\nequiv$ & $\nequiv$ \\
243 n & y & n & n & y & $\nequiv$ & $\nequiv$ \\
244 n & n & n & y & y & $\nequiv$ & $\equiv$ \\
246 And original definition is symmetrical in $L$ and $R$.
249 \subsection{Exclusive Tip Contents}
251 \bigforall_{C \in \py}
252 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
255 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
258 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
259 So by Base Acyclic $D \isin B \implies D \notin \py$.
261 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
262 \bigforall_{C \in \py} D \isin C \equiv
264 D \in \py : & D \le C \\
265 D \not\in \py : & D \isin \baseof{C}
269 \subsection{Tip Self Inpatch}
271 \bigforall_{C \in \py} C \haspatch \p
273 Ie, tip commits contain their own patch.
276 Apply Exclusive Tip Contents to some $D \in \py$:
277 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
278 D \isin C \equiv D \le C $
281 \subsection{Exact Ancestors}
283 \bigforall_{ C \hasparents \set{R} }
285 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
290 \subsection{Transitive Ancestors}
292 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
293 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
297 The implication from right to left is trivial because
298 $ \pends() \subset \pancs() $.
299 For the implication from left to right:
300 by the definition of $\mathcal E$,
301 for every such $A$, either $A \in \pends()$ which implies
302 $A \le M$ by the LHS directly,
303 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
304 in which case we repeat for $A'$. Since there are finitely many
305 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
306 by the LHS. And $A \le A''$.
309 \subsection{Calculation Of Ends}
311 \bigforall_{C \hasparents \set A}
312 \pendsof{C}{\set P} =
316 C \not\in \p : & \displaystyle
318 \Bigl[ \Largeexists_{A \in \set A}
319 E \in \pendsof{A}{\set P} \Bigr] \land
320 \Bigl[ \Largenexists_{B \in \set A, F \in \pendsof{B}{\p}}
321 E \neq F \land E \le F \Bigr]
326 Trivial for $C \in \set P$. For $C \not\in \set P$,
327 $\pancsof{C}{\set P} = \bigcup_{A \in \set A} \pancsof{A}{\set P}$.
328 So $\pendsof{C}{\set P} \subset \bigcup_{E in \set E} \pendsof{E}{\set P}$.
329 Consider some $E \in \pendsof{A}{\set P}$. If $\exists_{B,F}$ as
330 specified, then either $F$ is going to be in our result and
331 disqualifies $E$, or there is some other $F'$ (or, eventually,
332 an $F''$) which disqualifies $F$.
333 Otherwise, $E$ meets all the conditions for $\pends$.
336 \subsection{Ingredients Prevent Replay}
339 {C \hasparents \set A} \land
344 \Largeexists_{A \in \set A} D \isin A
346 \right] \implies \left[
347 D \isin C \implies D \le C
351 Trivial for $D = C$. Consider some $D \neq C$, $D \isin C$.
352 By the preconditions, there is some $A$ s.t. $D \in \set A$
353 and $D \isin A$. By No Replay for $A$, $D \le A$. And
354 $A \le C$ so $D \le C$.
357 \subsection{Simple Foreign Inclusion}
360 C \hasparents \{ L \}
362 \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
366 \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
367 D \isin C \equiv D \le C
371 Consider some $D$ s.t. $\patchof{D} = \bot$.
372 If $D = C$, trivially true. For $D \neq C$,
373 by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
374 And by Exact Ancestors $D \le L \equiv D \le C$.
375 So $D \isin C \equiv D \le C$.
378 \subsection{Totally Foreign Contents}
380 \bigforall_{C \hasparents \set A}
382 \patchof{C} = \bot \land
383 \bigforall_{A \in \set A} \patchof{A} = \bot
393 Consider some $D \le C$. If $D = C$, $\patchof{D} = \bot$ trivially.
394 If $D \neq C$ then $D \le A$ where $A \in \set A$. By Foreign
395 Contents of $A$, $\patchof{D} = \bot$.
398 \section{Commit annotation}
400 We annotate each Topbloke commit $C$ with:
404 \baseof{C}, \text{ if } C \in \py
407 \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
409 \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
412 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
413 in the summary in the section for that kind of commit.
415 Whether $\baseof{C}$ is required, and if so what the value is, is
416 stated in the proof of Unique Base for each kind of commit.
418 $C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
419 set $\{ \pq | C \haspatch \pq \}$. Whether $C \haspatch \pq$
421 (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
422 for the ingredients $I$),
423 in the proof of Coherence for each kind of commit.
425 $\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
426 using the lemma Calculation of Ends, above.
427 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
428 make it wrong to make plain commits with git because the recorded $\pends$
429 would have to be updated. The annotation is not needed in that case
430 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
432 \section{Simple commit}
434 A simple single-parent forward commit $C$ as made by git-commit.
436 \tag*{} C \hasparents \{ L \} \\
437 \tag*{} \patchof{C} = \patchof{L} \\
438 \tag*{} D \isin C \equiv D \isin L \lor D = C
440 This also covers Topbloke-generated commits on plain git branches:
441 Topbloke strips the metadata when exporting.
443 \subsection{No Replay}
445 Ingredients Prevent Replay applies. $\qed$
447 \subsection{Unique Base}
448 If $L, C \in \py$ then by Calculation of Ends for
449 $C, \py, C \not\in \py$:
450 $\pendsof{C}{\pn} = \pendsof{L}{\pn}$ so
451 $\baseof{C} = \baseof{L}$. $\qed$
453 \subsection{Tip Contents}
454 We need to consider only $L, C \in \py$. From Tip Contents for $L$:
455 \[ D \isin L \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L ) \]
456 Substitute into the contents of $C$:
457 \[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L )
459 Since $D = C \implies D \in \py$,
460 and substituting in $\baseof{C}$, this gives:
461 \[ D \isin C \equiv D \isin \baseof{C} \lor
462 (D \in \py \land D \le L) \lor
463 (D = C \land D \in \py) \]
464 \[ \equiv D \isin \baseof{C} \lor
465 [ D \in \py \land ( D \le L \lor D = C ) ] \]
466 So by Exact Ancestors:
467 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
471 \subsection{Base Acyclic}
473 Need to consider only $L, C \in \pn$.
475 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
477 For $D \neq C$: $D \isin C \equiv D \isin L$, so by Base Acyclic for
478 $L$, $D \isin C \implies D \not\in \py$.
482 \subsection{Coherence and patch inclusion}
484 Need to consider $D \in \py$
486 \subsubsection{For $L \haspatch P, D = C$:}
492 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
494 \subsubsection{For $L \haspatch P, D \neq C$:}
495 Ancestors: $ D \le C \equiv D \le L $.
497 Contents: $ D \isin C \equiv D \isin L \lor f $
498 so $ D \isin C \equiv D \isin L $.
501 \[ L \haspatch P \implies C \haspatch P \]
503 \subsubsection{For $L \nothaspatch P$:}
505 Firstly, $C \not\in \py$ since if it were, $L \in \py$.
508 Now by contents of $L$, $D \notin L$, so $D \notin C$.
511 \[ L \nothaspatch P \implies C \nothaspatch P \]
514 \subsection{Foreign Inclusion:}
516 Simple Foreign Inclusion applies. $\qed$
518 \subsection{Foreign Contents:}
520 Only relevant if $\patchof{C} = \bot$, and in that case Totally
521 Foreign Contents applies. $\qed$
523 \section{Create Base}
525 Given $L$, create a Topbloke base branch initial commit $B$.
527 B \hasparents \{ L \}
531 D \isin B \equiv D \isin L \lor D = B
534 \subsection{Conditions}
536 \[ \eqn{ Ingredients }{
537 \patchof{L} = \pa{L} \lor \patchof{L} = \bot
539 \[ \eqn{ Create Acyclic }{
543 \subsection{No Replay}
545 Ingredients Prevent Replay applies. $\qed$
547 \subsection{Unique Base}
551 \subsection{Tip Contents}
555 \subsection{Base Acyclic}
557 Consider some $D \isin B$. If $D = B$, $D \in \pqn$.
558 If $D \neq B$, $D \isin L$, and by Create Acyclic
559 $D \not\in \pqy$. $\qed$
561 \subsection{Coherence and Patch Inclusion}
563 Consider some $D \in \p$.
564 $B \not\in \py$ so $D \neq B$. So $D \isin B \equiv D \isin L$
565 and $D \le B \equiv D \le L$.
567 Thus $L \haspatch \p \implies B \haspatch P$
568 and $L \nothaspatch \p \implies B \nothaspatch P$.
572 \subsection{Foreign Inclusion}
574 Simple Foreign Inclusion applies. $\qed$
576 \subsection{Foreign Contents}
582 Given a Topbloke base $B$, create a tip branch initial commit B.
584 C \hasparents \{ B \}
588 D \isin C \equiv D \isin B \lor D = C
591 \subsection{Conditions}
593 \[ \eqn{ Ingredients }{
597 \pendsof{B}{\pqy} = \{ \}
600 \subsection{No Replay}
602 Ingredients Prevent Replay applies. $\qed$
604 \subsection{Unique Base}
606 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$. $\qed$
608 \subsection{Tip Contents}
610 Consider some arbitrary commit $D$. If $D = C$, trivially satisfied.
612 If $D \neq C$, $D \isin C \equiv D \isin B$.
613 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
614 So $D \isin C \equiv D \isin \baseof{B}$.
618 \subsection{Base Acyclic}
622 \subsection{Coherence and Patch Inclusion}
626 \p = \pq \lor B \haspatch \p : & C \haspatch \p \\
627 \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
632 ~ Consider some $D \in \py$.
634 \subsubsection{For $\p = \pq$:}
636 By Base Acyclic, $D \not\isin B$. So $D \isin C \equiv D = C$.
637 By No Sneak, $D \le B \equiv D = C$. Thus $C \haspatch \pq$.
639 \subsubsection{For $\p \neq \pq$:}
641 $D \neq C$. So $D \isin C \equiv D \isin B$,
642 and $D \le C \equiv D \le B$.
646 \subsection{Foreign Inclusion}
648 Simple Foreign Inclusion applies. $\qed$
650 \subsection{Foreign Contents}
656 Given $L$ and $\pr$ as represented by $R^+, R^-$.
657 Construct $C$ which has $\pr$ removed.
658 Used for removing a branch dependency.
660 C \hasparents \{ L \}
662 \patchof{C} = \patchof{L}
664 \mergeof{C}{L}{R^+}{R^-}
667 \subsection{Conditions}
669 \[ \eqn{ Ingredients }{
670 R^+ \in \pry \land R^- = \baseof{R^+}
672 \[ \eqn{ Into Base }{
675 \[ \eqn{ Unique Tip }{
676 \pendsof{L}{\pry} = \{ R^+ \}
678 \[ \eqn{ Currently Included }{
682 \subsection{Ordering of Ingredients:}
684 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
685 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$.
688 (Note that $R^+ \not\le R^-$, i.e. the merge base
689 is a descendant, not an ancestor, of the 2nd parent.)
691 \subsection{No Replay}
693 By definition of $\merge$,
694 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
695 So, by Ordering of Ingredients,
696 Ingredients Prevent Replay applies. $\qed$
698 \subsection{Desired Contents}
700 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
703 \subsubsection{For $D = C$:}
705 Trivially $D \isin C$. OK.
707 \subsubsection{For $D \neq C, D \not\le L$:}
709 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
710 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
712 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
714 By Currently Included, $D \isin L$.
716 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
717 by Unique Tip, $D \le R^+ \equiv D \le L$.
720 By Base Acyclic, $D \not\isin R^-$.
722 Apply $\merge$: $D \not\isin C$. OK.
724 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
726 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
728 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
732 \subsection{Unique Base}
734 Into Base means that $C \in \pn$, so Unique Base is not
737 \subsection{Tip Contents}
739 Again, not applicable. $\qed$
741 \subsection{Base Acyclic}
743 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
744 And by Into Base $C \not\in \py$.
745 Now from Desired Contents, above, $D \isin C
746 \implies D \isin L \lor D = C$, which thus
747 $\implies D \not\in \py$. $\qed$.
749 \subsection{Coherence and Patch Inclusion}
751 Need to consider some $D \in \py$. By Into Base, $D \neq C$.
753 \subsubsection{For $\p = \pr$:}
754 By Desired Contents, above, $D \not\isin C$.
755 So $C \nothaspatch \pr$.
757 \subsubsection{For $\p \neq \pr$:}
758 By Desired Contents, $D \isin C \equiv D \isin L$
759 (since $D \in \py$ so $D \not\in \pry$).
761 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
762 So $L \nothaspatch \p \implies C \nothaspatch \p$.
764 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
765 so $L \haspatch \p \implies C \haspatch \p$.
769 \subsection{Foreign Inclusion}
771 Consider some $D$ s.t. $\patchof{D} = \bot$. $D \neq C$.
772 So by Desired Contents $D \isin C \equiv D \isin L$.
773 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
775 And $D \le C \equiv D \le L$.
776 Thus $D \isin C \equiv D \le C$.
780 \subsection{Foreign Contents}
786 Merge commits $L$ and $R$ using merge base $M$:
788 C \hasparents \{ L, R \}
790 \patchof{C} = \patchof{L}
794 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
796 \subsection{Conditions}
797 \[ \eqn{ Ingredients }{
800 \[ \eqn{ Tip Merge }{
803 R \in \py : & \baseof{R} \ge \baseof{L}
804 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
805 R \in \pn : & M = \baseof{L} \\
806 \text{otherwise} : & \false
809 \[ \eqn{ Merge Acyclic }{
814 \[ \eqn{ Removal Merge Ends }{
815 X \not\haspatch \p \land
819 \pendsof{Y}{\py} = \pendsof{M}{\py}
821 \[ \eqn{ Addition Merge Ends }{
822 X \not\haspatch \p \land
826 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
829 \[ \eqn{ Foreign Merges }{
830 \patchof{L} = \bot \equiv \patchof{R} = \bot
833 \subsection{Non-Topbloke merges}
835 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
836 (Foreign Merges, above).
837 I.e. not only is it forbidden to merge into a Topbloke-controlled
838 branch without Topbloke's assistance, it is also forbidden to
839 merge any Topbloke-controlled branch into any plain git branch.
841 Given those conditions, Tip Merge and Merge Acyclic do not apply.
842 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
843 Merge Ends condition applies.
845 So a plain git merge of non-Topbloke branches meets the conditions and
846 is therefore consistent with our scheme.
848 \subsection{No Replay}
850 By definition of $\merge$,
851 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
853 Ingredients Prevent Replay applies. $\qed$
855 \subsection{Unique Base}
857 Need to consider only $C \in \py$, ie $L \in \py$,
858 and calculate $\pendsof{C}{\pn}$. So we will consider some
859 putative ancestor $A \in \pn$ and see whether $A \le C$.
861 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
862 But $C \in py$ and $A \in \pn$ so $A \neq C$.
863 Thus $A \le C \equiv A \le L \lor A \le R$.
865 By Unique Base of L and Transitive Ancestors,
866 $A \le L \equiv A \le \baseof{L}$.
868 \subsubsection{For $R \in \py$:}
870 By Unique Base of $R$ and Transitive Ancestors,
871 $A \le R \equiv A \le \baseof{R}$.
873 But by Tip Merge condition on $\baseof{R}$,
874 $A \le \baseof{L} \implies A \le \baseof{R}$, so
875 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
876 Thus $A \le C \equiv A \le \baseof{R}$.
877 That is, $\baseof{C} = \baseof{R}$.
879 \subsubsection{For $R \in \pn$:}
881 By Tip Merge condition on $R$ and since $M \le R$,
882 $A \le \baseof{L} \implies A \le R$, so
883 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
884 Thus $A \le C \equiv A \le R$.
885 That is, $\baseof{C} = R$.
889 \subsection{Coherence and Patch Inclusion}
891 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
892 This involves considering $D \in \py$.
894 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
895 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
896 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
897 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
899 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
900 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
901 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
903 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
905 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
906 \equiv D \isin L \lor D \isin R$.
907 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
909 Consider $D \neq C, D \isin X \land D \isin Y$:
910 By $\merge$, $D \isin C$. Also $D \le X$
911 so $D \le C$. OK for $C \haspatch \p$.
913 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
914 By $\merge$, $D \not\isin C$.
915 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
916 OK for $C \haspatch \p$.
918 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
919 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
920 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
921 OK for $C \haspatch \p$.
923 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
925 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
927 $M \haspatch \p \implies C \nothaspatch \p$.
928 $M \nothaspatch \p \implies C \haspatch \p$.
932 One of the Merge Ends conditions applies.
933 Recall that we are considering $D \in \py$.
934 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
935 We will show for each of
936 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
937 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
939 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
940 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
941 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
942 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
944 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
945 $D \le Y$ so $D \le C$.
946 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
948 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
949 $D \not\le Y$. If $D \le X$ then
950 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
951 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
952 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
954 Consider $D \neq C, M \haspatch P, D \isin Y$:
955 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
956 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
957 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
959 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
960 By $\merge$, $D \not\isin C$. OK.
964 \subsection{Base Acyclic}
966 This applies when $C \in \pn$.
967 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
969 Consider some $D \in \py$.
971 By Base Acyclic of $L$, $D \not\isin L$. By the above, $D \not\isin
972 R$. And $D \neq C$. So $D \not\isin C$.
976 \subsection{Tip Contents}
978 We need worry only about $C \in \py$.
979 And $\patchof{C} = \patchof{L}$
980 so $L \in \py$ so $L \haspatch \p$. We will use the Unique Base
981 of $C$, and its Coherence and Patch Inclusion, as just proved.
983 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
984 \p$ and by Coherence/Inclusion $C \haspatch \p$ . If $R \not\in \py$
985 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
986 of $\nothaspatch$, $M \nothaspatch \p$. So by Coherence/Inclusion $C
987 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
989 We will consider an arbitrary commit $D$
990 and prove the Exclusive Tip Contents form.
992 \subsubsection{For $D \in \py$:}
993 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
996 \subsubsection{For $D \not\in \py, R \not\in \py$:}
998 $D \neq C$. By Tip Contents of $L$,
999 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
1000 $D \isin L \equiv D \isin M$. So by definition of $\merge$, $D \isin
1001 C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$.
1002 Thus $D \isin C \equiv D \isin \baseof{C}$. OK.
1004 \subsubsection{For $D \not\in \py, R \in \py$:}
1009 $D \isin L \equiv D \isin \baseof{L}$ and
1010 $D \isin R \equiv D \isin \baseof{R}$.
1012 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
1013 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
1014 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
1015 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
1017 So $D \isin M \equiv D \isin L$ and by $\merge$,
1018 $D \isin C \equiv D \isin R$. But from Unique Base,
1019 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$. OK.
1023 \subsection{Foreign Inclusion}
1025 Consider some $D$ s.t. $\patchof{D} = \bot$.
1026 By Foreign Inclusion of $L, M, R$:
1027 $D \isin L \equiv D \le L$;
1028 $D \isin M \equiv D \le M$;
1029 $D \isin R \equiv D \le R$.
1031 \subsubsection{For $D = C$:}
1033 $D \isin C$ and $D \le C$. OK.
1035 \subsubsection{For $D \neq C, D \isin M$:}
1037 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
1038 R$. So by $\merge$, $D \isin C$. And $D \le C$. OK.
1040 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
1042 By $\merge$, $D \isin C$.
1043 And $D \isin X$ means $D \le X$ so $D \le C$.
1046 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
1048 By $\merge$, $D \not\isin C$.
1049 And $D \not\le L, D \not\le R$ so $D \not\le C$.
1054 \subsection{Foreign Contents}
1056 Only relevant if $\patchof{L} = \bot$, in which case
1057 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
1058 so Totally Foreign Contents applies. $\qed$