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 }{
540 \pendsof{L}{\pqy} = \{ \}
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$, so by No Replay $D \le L$
559 and by Create Acyclic
560 $D \not\in \pqy$. $\qed$
562 \subsection{Coherence and Patch Inclusion}
564 Consider some $D \in \p$.
565 $B \not\in \py$ so $D \neq B$. So $D \isin B \equiv D \isin L$
566 and $D \le B \equiv D \le L$.
568 Thus $L \haspatch \p \implies B \haspatch P$
569 and $L \nothaspatch \p \implies B \nothaspatch P$.
573 \subsection{Foreign Inclusion}
575 Simple Foreign Inclusion applies. $\qed$
577 \subsection{Foreign Contents}
583 Given a Topbloke base $B$, create a tip branch initial commit B.
585 C \hasparents \{ B \}
589 D \isin C \equiv D \isin B \lor D = C
592 \subsection{Conditions}
594 \[ \eqn{ Ingredients }{
598 \pendsof{B}{\pqy} = \{ \}
601 \subsection{No Replay}
603 Ingredients Prevent Replay applies. $\qed$
605 \subsection{Unique Base}
607 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$. $\qed$
609 \subsection{Tip Contents}
611 Consider some arbitrary commit $D$. If $D = C$, trivially satisfied.
613 If $D \neq C$, $D \isin C \equiv D \isin B$.
614 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
615 So $D \isin C \equiv D \isin \baseof{B}$.
619 \subsection{Base Acyclic}
623 \subsection{Coherence and Patch Inclusion}
627 \p = \pq \lor B \haspatch \p : & C \haspatch \p \\
628 \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
633 ~ Consider some $D \in \py$.
635 \subsubsection{For $\p = \pq$:}
637 By Base Acyclic, $D \not\isin B$. So $D \isin C \equiv D = C$.
638 By No Sneak, $D \le B \equiv D = C$. Thus $C \haspatch \pq$.
640 \subsubsection{For $\p \neq \pq$:}
642 $D \neq C$. So $D \isin C \equiv D \isin B$,
643 and $D \le C \equiv D \le B$.
647 \subsection{Foreign Inclusion}
649 Simple Foreign Inclusion applies. $\qed$
651 \subsection{Foreign Contents}
657 Given $L$ and $\pr$ as represented by $R^+, R^-$.
658 Construct $C$ which has $\pr$ removed.
659 Used for removing a branch dependency.
661 C \hasparents \{ L \}
663 \patchof{C} = \patchof{L}
665 \mergeof{C}{L}{R^+}{R^-}
668 \subsection{Conditions}
670 \[ \eqn{ Ingredients }{
671 R^+ \in \pry \land R^- = \baseof{R^+}
673 \[ \eqn{ Into Base }{
676 \[ \eqn{ Unique Tip }{
677 \pendsof{L}{\pry} = \{ R^+ \}
679 \[ \eqn{ Currently Included }{
683 \subsection{Ordering of Ingredients:}
685 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
686 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$.
689 (Note that $R^+ \not\le R^-$, i.e. the merge base
690 is a descendant, not an ancestor, of the 2nd parent.)
692 \subsection{No Replay}
694 By definition of $\merge$,
695 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
696 So, by Ordering of Ingredients,
697 Ingredients Prevent Replay applies. $\qed$
699 \subsection{Desired Contents}
701 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
704 \subsubsection{For $D = C$:}
706 Trivially $D \isin C$. OK.
708 \subsubsection{For $D \neq C, D \not\le L$:}
710 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
711 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
713 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
715 By Currently Included, $D \isin L$.
717 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
718 by Unique Tip, $D \le R^+ \equiv D \le L$.
721 By Base Acyclic, $D \not\isin R^-$.
723 Apply $\merge$: $D \not\isin C$. OK.
725 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
727 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
729 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
733 \subsection{Unique Base}
735 Into Base means that $C \in \pn$, so Unique Base is not
738 \subsection{Tip Contents}
740 Again, not applicable. $\qed$
742 \subsection{Base Acyclic}
744 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
745 And by Into Base $C \not\in \py$.
746 Now from Desired Contents, above, $D \isin C
747 \implies D \isin L \lor D = C$, which thus
748 $\implies D \not\in \py$. $\qed$.
750 \subsection{Coherence and Patch Inclusion}
752 Need to consider some $D \in \py$. By Into Base, $D \neq C$.
754 \subsubsection{For $\p = \pr$:}
755 By Desired Contents, above, $D \not\isin C$.
756 So $C \nothaspatch \pr$.
758 \subsubsection{For $\p \neq \pr$:}
759 By Desired Contents, $D \isin C \equiv D \isin L$
760 (since $D \in \py$ so $D \not\in \pry$).
762 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
763 So $L \nothaspatch \p \implies C \nothaspatch \p$.
765 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
766 so $L \haspatch \p \implies C \haspatch \p$.
770 \subsection{Foreign Inclusion}
772 Consider some $D$ s.t. $\patchof{D} = \bot$. $D \neq C$.
773 So by Desired Contents $D \isin C \equiv D \isin L$.
774 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
776 And $D \le C \equiv D \le L$.
777 Thus $D \isin C \equiv D \le C$.
781 \subsection{Foreign Contents}
787 Merge commits $L$ and $R$ using merge base $M$:
789 C \hasparents \{ L, R \}
791 \patchof{C} = \patchof{L}
795 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
797 \subsection{Conditions}
798 \[ \eqn{ Ingredients }{
801 \[ \eqn{ Tip Merge }{
804 R \in \py : & \baseof{R} \ge \baseof{L}
805 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
806 R \in \pn : & M = \baseof{L} \\
807 \text{otherwise} : & \false
810 \[ \eqn{ Merge Acyclic }{
815 \[ \eqn{ Removal Merge Ends }{
816 X \not\haspatch \p \land
820 \pendsof{Y}{\py} = \pendsof{M}{\py}
822 \[ \eqn{ Addition Merge Ends }{
823 X \not\haspatch \p \land
827 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
830 \[ \eqn{ Foreign Merges }{
831 \patchof{L} = \bot \equiv \patchof{R} = \bot
834 \subsection{Non-Topbloke merges}
836 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
837 (Foreign Merges, above).
838 I.e. not only is it forbidden to merge into a Topbloke-controlled
839 branch without Topbloke's assistance, it is also forbidden to
840 merge any Topbloke-controlled branch into any plain git branch.
842 Given those conditions, Tip Merge and Merge Acyclic do not apply.
843 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
844 Merge Ends condition applies.
846 So a plain git merge of non-Topbloke branches meets the conditions and
847 is therefore consistent with our scheme.
849 \subsection{No Replay}
851 By definition of $\merge$,
852 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
854 Ingredients Prevent Replay applies. $\qed$
856 \subsection{Unique Base}
858 Need to consider only $C \in \py$, ie $L \in \py$,
859 and calculate $\pendsof{C}{\pn}$. So we will consider some
860 putative ancestor $A \in \pn$ and see whether $A \le C$.
862 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
863 But $C \in py$ and $A \in \pn$ so $A \neq C$.
864 Thus $A \le C \equiv A \le L \lor A \le R$.
866 By Unique Base of L and Transitive Ancestors,
867 $A \le L \equiv A \le \baseof{L}$.
869 \subsubsection{For $R \in \py$:}
871 By Unique Base of $R$ and Transitive Ancestors,
872 $A \le R \equiv A \le \baseof{R}$.
874 But by Tip Merge condition on $\baseof{R}$,
875 $A \le \baseof{L} \implies A \le \baseof{R}$, so
876 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
877 Thus $A \le C \equiv A \le \baseof{R}$.
878 That is, $\baseof{C} = \baseof{R}$.
880 \subsubsection{For $R \in \pn$:}
882 By Tip Merge condition on $R$ and since $M \le R$,
883 $A \le \baseof{L} \implies A \le R$, so
884 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
885 Thus $A \le C \equiv A \le R$.
886 That is, $\baseof{C} = R$.
890 \subsection{Coherence and Patch Inclusion}
892 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
893 This involves considering $D \in \py$.
895 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
896 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
897 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
898 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
900 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
901 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
902 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
904 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
906 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
907 \equiv D \isin L \lor D \isin R$.
908 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
910 Consider $D \neq C, D \isin X \land D \isin Y$:
911 By $\merge$, $D \isin C$. Also $D \le X$
912 so $D \le C$. OK for $C \haspatch \p$.
914 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
915 By $\merge$, $D \not\isin C$.
916 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
917 OK for $C \haspatch \p$.
919 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
920 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
921 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
922 OK for $C \haspatch \p$.
924 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
926 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
928 $M \haspatch \p \implies C \nothaspatch \p$.
929 $M \nothaspatch \p \implies C \haspatch \p$.
933 One of the Merge Ends conditions applies.
934 Recall that we are considering $D \in \py$.
935 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
936 We will show for each of
937 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
938 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
940 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
941 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
942 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
943 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
945 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
946 $D \le Y$ so $D \le C$.
947 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
949 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
950 $D \not\le Y$. If $D \le X$ then
951 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
952 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
953 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
955 Consider $D \neq C, M \haspatch P, D \isin Y$:
956 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
957 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
958 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
960 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
961 By $\merge$, $D \not\isin C$. OK.
965 \subsection{Base Acyclic}
967 This applies when $C \in \pn$.
968 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
970 Consider some $D \in \py$.
972 By Base Acyclic of $L$, $D \not\isin L$. By the above, $D \not\isin
973 R$. And $D \neq C$. So $D \not\isin C$.
977 \subsection{Tip Contents}
979 We need worry only about $C \in \py$.
980 And $\patchof{C} = \patchof{L}$
981 so $L \in \py$ so $L \haspatch \p$. We will use the Unique Base
982 of $C$, and its Coherence and Patch Inclusion, as just proved.
984 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
985 \p$ and by Coherence/Inclusion $C \haspatch \p$ . If $R \not\in \py$
986 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
987 of $\nothaspatch$, $M \nothaspatch \p$. So by Coherence/Inclusion $C
988 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
990 We will consider an arbitrary commit $D$
991 and prove the Exclusive Tip Contents form.
993 \subsubsection{For $D \in \py$:}
994 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
997 \subsubsection{For $D \not\in \py, R \not\in \py$:}
999 $D \neq C$. By Tip Contents of $L$,
1000 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
1001 $D \isin L \equiv D \isin M$. So by definition of $\merge$, $D \isin
1002 C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$.
1003 Thus $D \isin C \equiv D \isin \baseof{C}$. OK.
1005 \subsubsection{For $D \not\in \py, R \in \py$:}
1010 $D \isin L \equiv D \isin \baseof{L}$ and
1011 $D \isin R \equiv D \isin \baseof{R}$.
1013 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
1014 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
1015 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
1016 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
1018 So $D \isin M \equiv D \isin L$ and by $\merge$,
1019 $D \isin C \equiv D \isin R$. But from Unique Base,
1020 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$. OK.
1024 \subsection{Foreign Inclusion}
1026 Consider some $D$ s.t. $\patchof{D} = \bot$.
1027 By Foreign Inclusion of $L, M, R$:
1028 $D \isin L \equiv D \le L$;
1029 $D \isin M \equiv D \le M$;
1030 $D \isin R \equiv D \le R$.
1032 \subsubsection{For $D = C$:}
1034 $D \isin C$ and $D \le C$. OK.
1036 \subsubsection{For $D \neq C, D \isin M$:}
1038 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
1039 R$. So by $\merge$, $D \isin C$. And $D \le C$. OK.
1041 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
1043 By $\merge$, $D \isin C$.
1044 And $D \isin X$ means $D \le X$ so $D \le C$.
1047 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
1049 By $\merge$, $D \not\isin C$.
1050 And $D \not\le L, D \not\le R$ so $D \not\le C$.
1055 \subsection{Foreign Contents}
1057 Only relevant if $\patchof{L} = \bot$, in which case
1058 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
1059 so Totally Foreign Contents applies. $\qed$