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 All of these sets are disjoint. 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{ Create Acyclic }{
537 \pendsof{L}{\pqy} = \{ \}
540 \subsection{No Replay}
542 Ingredients Prevent Replay applies. $\qed$
544 \subsection{Unique Base}
548 \subsection{Tip Contents}
552 \subsection{Base Acyclic}
554 Consider some $D \isin B$. If $D = B$, $D \in \pqn$.
555 If $D \neq B$, $D \isin L$, so by No Replay $D \le L$
556 and by Create Acyclic
557 $D \not\in \pqy$. $\qed$
559 \subsection{Coherence and Patch Inclusion}
561 Consider some $D \in \p$.
562 $B \not\in \py$ so $D \neq B$. So $D \isin B \equiv D \isin L$
563 and $D \le B \equiv D \le L$.
565 Thus $L \haspatch \p \implies B \haspatch P$
566 and $L \nothaspatch \p \implies B \nothaspatch P$.
570 \subsection{Foreign Inclusion}
572 Simple Foreign Inclusion applies. $\qed$
574 \subsection{Foreign Contents}
580 Given a Topbloke base $B$, create a tip branch initial commit B.
582 C \hasparents \{ B \}
586 D \isin C \equiv D \isin B \lor D = C
589 \subsection{Conditions}
591 \[ \eqn{ Ingredients }{
595 \pendsof{B}{\pqy} = \{ \}
598 \subsection{No Replay}
600 Ingredients Prevent Replay applies. $\qed$
602 \subsection{Unique Base}
604 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$. $\qed$
606 \subsection{Tip Contents}
608 Consider some arbitrary commit $D$. If $D = C$, trivially satisfied.
610 If $D \neq C$, $D \isin C \equiv D \isin B$.
611 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
612 So $D \isin C \equiv D \isin \baseof{B}$.
616 \subsection{Base Acyclic}
620 \subsection{Coherence and Patch Inclusion}
624 \p = \pq \lor B \haspatch \p : & C \haspatch \p \\
625 \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
630 ~ Consider some $D \in \py$.
632 \subsubsection{For $\p = \pq$:}
634 By Base Acyclic, $D \not\isin B$. So $D \isin C \equiv D = C$.
635 By No Sneak, $D \le B \equiv D = C$. Thus $C \haspatch \pq$.
637 \subsubsection{For $\p \neq \pq$:}
639 $D \neq C$. So $D \isin C \equiv D \isin B$,
640 and $D \le C \equiv D \le B$.
644 \subsection{Foreign Inclusion}
646 Simple Foreign Inclusion applies. $\qed$
648 \subsection{Foreign Contents}
654 Given $L$ and $\pr$ as represented by $R^+, R^-$.
655 Construct $C$ which has $\pr$ removed.
656 Used for removing a branch dependency.
658 C \hasparents \{ L \}
660 \patchof{C} = \patchof{L}
662 \mergeof{C}{L}{R^+}{R^-}
665 \subsection{Conditions}
667 \[ \eqn{ Ingredients }{
668 R^+ \in \pry \land R^- = \baseof{R^+}
670 \[ \eqn{ Into Base }{
673 \[ \eqn{ Unique Tip }{
674 \pendsof{L}{\pry} = \{ R^+ \}
676 \[ \eqn{ Currently Included }{
680 \subsection{Ordering of Ingredients:}
682 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
683 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$.
686 (Note that $R^+ \not\le R^-$, i.e. the merge base
687 is a descendant, not an ancestor, of the 2nd parent.)
689 \subsection{No Replay}
691 By definition of $\merge$,
692 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
693 So, by Ordering of Ingredients,
694 Ingredients Prevent Replay applies. $\qed$
696 \subsection{Desired Contents}
698 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
701 \subsubsection{For $D = C$:}
703 Trivially $D \isin C$. OK.
705 \subsubsection{For $D \neq C, D \not\le L$:}
707 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
708 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
710 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
712 By Currently Included, $D \isin L$.
714 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
715 by Unique Tip, $D \le R^+ \equiv D \le L$.
718 By Base Acyclic, $D \not\isin R^-$.
720 Apply $\merge$: $D \not\isin C$. OK.
722 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
724 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
726 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
730 \subsection{Unique Base}
732 Into Base means that $C \in \pn$, so Unique Base is not
735 \subsection{Tip Contents}
737 Again, not applicable. $\qed$
739 \subsection{Base Acyclic}
741 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
742 And by Into Base $C \not\in \py$.
743 Now from Desired Contents, above, $D \isin C
744 \implies D \isin L \lor D = C$, which thus
745 $\implies D \not\in \py$. $\qed$.
747 \subsection{Coherence and Patch Inclusion}
749 Need to consider some $D \in \py$. By Into Base, $D \neq C$.
751 \subsubsection{For $\p = \pr$:}
752 By Desired Contents, above, $D \not\isin C$.
753 So $C \nothaspatch \pr$.
755 \subsubsection{For $\p \neq \pr$:}
756 By Desired Contents, $D \isin C \equiv D \isin L$
757 (since $D \in \py$ so $D \not\in \pry$).
759 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
760 So $L \nothaspatch \p \implies C \nothaspatch \p$.
762 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
763 so $L \haspatch \p \implies C \haspatch \p$.
767 \subsection{Foreign Inclusion}
769 Consider some $D$ s.t. $\patchof{D} = \bot$. $D \neq C$.
770 So by Desired Contents $D \isin C \equiv D \isin L$.
771 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
773 And $D \le C \equiv D \le L$.
774 Thus $D \isin C \equiv D \le C$.
778 \subsection{Foreign Contents}
784 Merge commits $L$ and $R$ using merge base $M$:
786 C \hasparents \{ L, R \}
788 \patchof{C} = \patchof{L}
792 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
794 \subsection{Conditions}
795 \[ \eqn{ Ingredients }{
798 \[ \eqn{ Tip Merge }{
801 R \in \py : & \baseof{R} \ge \baseof{L}
802 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
803 R \in \pn : & M = \baseof{L} \\
804 \text{otherwise} : & \false
807 \[ \eqn{ Merge Acyclic }{
812 \[ \eqn{ Removal Merge Ends }{
813 X \not\haspatch \p \land
817 \pendsof{Y}{\py} = \pendsof{M}{\py}
819 \[ \eqn{ Addition Merge Ends }{
820 X \not\haspatch \p \land
824 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
827 \[ \eqn{ Foreign Merges }{
828 \patchof{L} = \bot \equiv \patchof{R} = \bot
831 \subsection{Non-Topbloke merges}
833 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
834 (Foreign Merges, above).
835 I.e. not only is it forbidden to merge into a Topbloke-controlled
836 branch without Topbloke's assistance, it is also forbidden to
837 merge any Topbloke-controlled branch into any plain git branch.
839 Given those conditions, Tip Merge and Merge Acyclic do not apply.
840 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
841 Merge Ends condition applies.
843 So a plain git merge of non-Topbloke branches meets the conditions and
844 is therefore consistent with our model.
846 \subsection{No Replay}
848 By definition of $\merge$,
849 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
851 Ingredients Prevent Replay applies. $\qed$
853 \subsection{Unique Base}
855 Need to consider only $C \in \py$, ie $L \in \py$,
856 and calculate $\pendsof{C}{\pn}$. So we will consider some
857 putative ancestor $A \in \pn$ and see whether $A \le C$.
859 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
860 But $C \in py$ and $A \in \pn$ so $A \neq C$.
861 Thus $A \le C \equiv A \le L \lor A \le R$.
863 By Unique Base of L and Transitive Ancestors,
864 $A \le L \equiv A \le \baseof{L}$.
866 \subsubsection{For $R \in \py$:}
868 By Unique Base of $R$ and Transitive Ancestors,
869 $A \le R \equiv A \le \baseof{R}$.
871 But by Tip Merge condition on $\baseof{R}$,
872 $A \le \baseof{L} \implies A \le \baseof{R}$, so
873 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
874 Thus $A \le C \equiv A \le \baseof{R}$.
875 That is, $\baseof{C} = \baseof{R}$.
877 \subsubsection{For $R \in \pn$:}
879 By Tip Merge condition on $R$ and since $M \le R$,
880 $A \le \baseof{L} \implies A \le R$, so
881 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
882 Thus $A \le C \equiv A \le R$.
883 That is, $\baseof{C} = R$.
887 \subsection{Coherence and Patch Inclusion}
889 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
890 This involves considering $D \in \py$.
892 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
893 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
894 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
895 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
897 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
898 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
899 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
901 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
903 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
904 \equiv D \isin L \lor D \isin R$.
905 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
907 Consider $D \neq C, D \isin X \land D \isin Y$:
908 By $\merge$, $D \isin C$. Also $D \le X$
909 so $D \le C$. OK for $C \haspatch \p$.
911 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
912 By $\merge$, $D \not\isin C$.
913 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
914 OK for $C \haspatch \p$.
916 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
917 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
918 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
919 OK for $C \haspatch \p$.
921 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
923 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
925 $M \haspatch \p \implies C \nothaspatch \p$.
926 $M \nothaspatch \p \implies C \haspatch \p$.
930 One of the Merge Ends conditions applies.
931 Recall that we are considering $D \in \py$.
932 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
933 We will show for each of
934 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
935 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
937 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
938 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
939 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
940 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
942 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
943 $D \le Y$ so $D \le C$.
944 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
946 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
947 $D \not\le Y$. If $D \le X$ then
948 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
949 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
950 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
952 Consider $D \neq C, M \haspatch P, D \isin Y$:
953 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
954 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
955 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
957 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
958 By $\merge$, $D \not\isin C$. OK.
962 \subsection{Base Acyclic}
964 This applies when $C \in \pn$.
965 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
967 Consider some $D \in \py$.
969 By Base Acyclic of $L$, $D \not\isin L$. By the above, $D \not\isin
970 R$. And $D \neq C$. So $D \not\isin C$.
974 \subsection{Tip Contents}
976 We need worry only about $C \in \py$.
977 And $\patchof{C} = \patchof{L}$
978 so $L \in \py$ so $L \haspatch \p$. We will use the Unique Base
979 of $C$, and its Coherence and Patch Inclusion, as just proved.
981 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
982 \p$ and by Coherence/Inclusion $C \haspatch \p$ . If $R \not\in \py$
983 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
984 of $\nothaspatch$, $M \nothaspatch \p$. So by Coherence/Inclusion $C
985 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
987 We will consider an arbitrary commit $D$
988 and prove the Exclusive Tip Contents form.
990 \subsubsection{For $D \in \py$:}
991 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
994 \subsubsection{For $D \not\in \py, R \not\in \py$:}
996 $D \neq C$. By Tip Contents of $L$,
997 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
998 $D \isin L \equiv D \isin M$. So by definition of $\merge$, $D \isin
999 C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$.
1000 Thus $D \isin C \equiv D \isin \baseof{C}$. OK.
1002 \subsubsection{For $D \not\in \py, R \in \py$:}
1007 $D \isin L \equiv D \isin \baseof{L}$ and
1008 $D \isin R \equiv D \isin \baseof{R}$.
1010 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
1011 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
1012 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
1013 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
1015 So $D \isin M \equiv D \isin L$ and by $\merge$,
1016 $D \isin C \equiv D \isin R$. But from Unique Base,
1017 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$. OK.
1021 \subsection{Foreign Inclusion}
1023 Consider some $D$ s.t. $\patchof{D} = \bot$.
1024 By Foreign Inclusion of $L, M, R$:
1025 $D \isin L \equiv D \le L$;
1026 $D \isin M \equiv D \le M$;
1027 $D \isin R \equiv D \le R$.
1029 \subsubsection{For $D = C$:}
1031 $D \isin C$ and $D \le C$. OK.
1033 \subsubsection{For $D \neq C, D \isin M$:}
1035 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
1036 R$. So by $\merge$, $D \isin C$. And $D \le C$. OK.
1038 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
1040 By $\merge$, $D \isin C$.
1041 And $D \isin X$ means $D \le X$ so $D \le C$.
1044 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
1046 By $\merge$, $D \not\isin C$.
1047 And $D \not\le L, D \not\le R$ so $D \not\le C$.
1052 \subsection{Foreign Contents}
1054 Only relevant if $\patchof{L} = \bot$, in which case
1055 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
1056 so Totally Foreign Contents applies. $\qed$