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{\pr}{\pa{R}}
38 \newcommand{\pry}{\pay{R}}
39 \newcommand{\prn}{\pan{R}}
41 %\newcommand{\hasparents}{\underaccent{1}{>}}
42 %\newcommand{\hasparents}{{%
43 % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
44 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
45 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
47 \renewcommand{\implies}{\Rightarrow}
48 \renewcommand{\equiv}{\Leftrightarrow}
49 \renewcommand{\land}{\wedge}
50 \renewcommand{\lor}{\vee}
52 \newcommand{\pancs}{{\mathcal A}}
53 \newcommand{\pends}{{\mathcal E}}
55 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
56 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
58 \newcommand{\merge}{{\mathcal M}}
59 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
60 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
62 \newcommand{\patch}{{\mathcal P}}
63 \newcommand{\base}{{\mathcal B}}
65 \newcommand{\patchof}[1]{\patch ( #1 ) }
66 \newcommand{\baseof}[1]{\base ( #1 ) }
68 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
69 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
71 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
72 \newcommand{\bigforall}{%
74 {\hbox{\huge$\forall$}}%
75 {\hbox{\Large$\forall$}}%
76 {\hbox{\normalsize$\forall$}}%
77 {\hbox{\scriptsize$\forall$}}}%
80 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
81 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
83 \newcommand{\qed}{\square}
84 \newcommand{\proofstarts}{{\it Proof:}}
85 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
87 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
88 \newcommand{\gathnext}{\\ \tag*{}}
91 \newcommand{\false}{f}
99 \desclabelstyle{\nextlinelabel}
101 \item[ $ C \hasparents \set X $ ]
102 The parents of commit $C$ are exactly the set
106 $C$ is a descendant of $D$ in the git commit
107 graph. This is a partial order, namely the transitive closure of
108 $ D \in \set X $ where $ C \hasparents \set X $.
110 \item[ $ C \has D $ ]
111 Informally, the tree at commit $C$ contains the change
112 made in commit $D$. Does not take account of deliberate reversions by
113 the user or reversion, rebasing or rewinding in
114 non-Topbloke-controlled branches. For merges and Topbloke-generated
115 anticommits or re-commits, the ``change made'' is only to be thought
116 of as any conflict resolution. This is not a partial order because it
119 \item[ $ \p, \py, \pn $ ]
120 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
121 are respectively the base and tip git branches. $\p$ may be used
122 where the context requires a set, in which case the statement
123 is to be taken as applying to both $\py$ and $\pn$.
124 All these sets are distinct. Hence:
126 \item[ $ \patchof{ C } $ ]
127 Either $\p$ s.t. $ C \in \p $, or $\bot$.
128 A function from commits to patches' sets $\p$.
130 \item[ $ \pancsof{C}{\set P} $ ]
131 $ \{ A \; | \; A \le C \land A \in \set P \} $
132 i.e. all the ancestors of $C$
133 which are in $\set P$.
135 \item[ $ \pendsof{C}{\set P} $ ]
136 $ \{ E \; | \; E \in \pancsof{C}{\set P}
137 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
138 E \neq A \land E \le A \} $
139 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
141 \item[ $ \baseof{C} $ ]
142 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
143 A partial function from commits to commits.
144 See Unique Base, below.
146 \item[ $ C \haspatch \p $ ]
147 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
148 ~ Informally, $C$ has the contents of $\p$.
150 \item[ $ C \nothaspatch \p $ ]
151 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
152 ~ Informally, $C$ has none of the contents of $\p$.
154 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
155 patch is applied to a non-Topbloke branch and then bubbles back to
156 the Topbloke patch itself, we hope that git's merge algorithm will
157 DTRT or that the user will no longer care about the Topbloke patch.
159 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
160 The contents of a git merge result:
162 $\displaystyle D \isin C \equiv
164 (D \isin L \land D \isin R) \lor D = C : & \true \\
165 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
166 \text{otherwise} : & D \not\isin M
174 We maintain these each time we construct a new commit. \\
176 C \has D \implies C \ge D
178 \[\eqn{Unique Base:}{
179 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
181 \[\eqn{Tip Contents:}{
182 \bigforall_{C \in \py} D \isin C \equiv
183 { D \isin \baseof{C} \lor \atop
184 (D \in \py \land D \le C) }
186 \[\eqn{Base Acyclic:}{
187 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
190 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
192 \[\eqn{Foreign Inclusion:}{
193 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
196 \section{Some lemmas}
198 \[ \eqn{Exclusive Tip Contents:}{
199 \bigforall_{C \in \py}
200 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
203 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
206 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
207 So by Base Acyclic $D \isin B \implies D \notin \py$.
209 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
210 \bigforall_{C \in \py} D \isin C \equiv
212 D \in \py : & D \le C \\
213 D \not\in \py : & D \isin \baseof{C}
217 \[ \eqn{Tip Self Inpatch:}{
218 \bigforall_{C \in \py} C \haspatch \p
220 Ie, tip commits contain their own patch.
223 Apply Exclusive Tip Contents to some $D \in \py$:
224 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
225 D \isin C \equiv D \le C $
228 \[ \eqn{Exact Ancestors:}{
229 \bigforall_{ C \hasparents \set{R} }
231 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
235 \[ \eqn{Transitive Ancestors:}{
236 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
237 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
241 The implication from right to left is trivial because
242 $ \pends() \subset \pancs() $.
243 For the implication from left to right:
244 by the definition of $\mathcal E$,
245 for every such $A$, either $A \in \pends()$ which implies
246 $A \le M$ by the LHS directly,
247 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
248 in which case we repeat for $A'$. Since there are finitely many
249 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
250 by the LHS. And $A \le A''$.
252 \[ \eqn{Calculation Of Ends:}{
253 \bigforall_{C \hasparents \set A}
254 \pendsof{C}{\set P} =
256 \Bigl[ \Largeexists_{A \in \set A}
257 E \in \pendsof{A}{\set P} \Bigr] \land
258 \Bigl[ \Largenexists_{B \in \set A}
259 E \neq B \land E \le B \Bigr]
264 \subsection{No Replay for Merge Results}
266 If we are constructing $C$, with,
274 No Replay is preserved. \proofstarts
276 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
278 \subsubsection{For $D \isin L \land D \isin R$:}
279 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
281 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
284 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
285 \land D \not\isin M$:}
286 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
289 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
295 \section{Commit annotation}
297 We annotate each Topbloke commit $C$ with:
301 \baseof{C}, \text{ if } C \in \py
304 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
306 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
309 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
310 make it wrong to make plain commits with git because the recorded $\pends$
311 would have to be updated. The annotation is not needed because
312 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
314 \section{Simple commit}
316 A simple single-parent forward commit $C$ as made by git-commit.
318 \tag*{} C \hasparents \{ A \} \\
319 \tag*{} \patchof{C} = \patchof{A} \\
320 \tag*{} D \isin C \equiv D \isin A \lor D = C
323 \subsection{No Replay}
326 \subsection{Unique Base}
327 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
329 \subsection{Tip Contents}
330 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
331 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
332 Substitute into the contents of $C$:
333 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
335 Since $D = C \implies D \in \py$,
336 and substituting in $\baseof{C}$, this gives:
337 \[ D \isin C \equiv D \isin \baseof{C} \lor
338 (D \in \py \land D \le A) \lor
339 (D = C \land D \in \py) \]
340 \[ \equiv D \isin \baseof{C} \lor
341 [ D \in \py \land ( D \le A \lor D = C ) ] \]
342 So by Exact Ancestors:
343 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
347 \subsection{Base Acyclic}
349 Need to consider only $A, C \in \pn$.
351 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
353 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
354 $A$, $D \isin C \implies D \not\in \py$. $\qed$
356 \subsection{Coherence and patch inclusion}
358 Need to consider $D \in \py$
360 \subsubsection{For $A \haspatch P, D = C$:}
366 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
368 \subsubsection{For $A \haspatch P, D \neq C$:}
369 Ancestors: $ D \le C \equiv D \le A $.
371 Contents: $ D \isin C \equiv D \isin A \lor f $
372 so $ D \isin C \equiv D \isin A $.
375 \[ A \haspatch P \implies C \haspatch P \]
377 \subsubsection{For $A \nothaspatch P$:}
379 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
382 Now by contents of $A$, $D \notin A$, so $D \notin C$.
385 \[ A \nothaspatch P \implies C \nothaspatch P \]
388 \subsection{Foreign inclusion:}
390 If $D = C$, trivial. For $D \neq C$:
391 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
395 Given $L, R^+, R^-$ where
396 $R^+ \in \pry, R^- = \baseof{R^+}$.
397 Construct $C$ which has $\pr$ removed.
398 Used for removing a branch dependency.
400 C \hasparents \{ L \}
402 \patchof{C} = \patchof{L}
404 \mergeof{C}{L}{R^+}{R^-}
407 \subsection{Conditions}
409 \[ \eqn{ Unique Tip }{
410 \pendsof{L}{\pry} = \{ R^+ \}
412 \[ \eqn{ Currently Included }{
419 \subsection{No Replay}
421 By Unique Tip, $R^+ \le L$. By definition of $\base$, $R^- \le R^+$
422 so $R^- \le L$. So $R^+ \le C$ and $R^- \le C$ and No Replay for
423 Merge Results applies. $\qed$
425 \subsection{Desired Contents}
427 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
430 \subsubsection{For $D = C$:}
432 Trivially $D \isin C$. OK.
434 \subsubsection{For $D \neq C, D \not\le L$:}
436 By No Replay $D \not\isin L$. Also $D \not\le R^-$ hence
437 $D \not\isin R^-$. Thus $D \not\isin C$. OK.
439 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
441 By Currently Included, $D \isin L$.
443 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
444 by Unique Tip, $D \le R^+ \equiv D \le L$.
447 By Base Acyclic, $D \not\isin R^-$.
449 Apply $\merge$: $D \not\isin C$. OK.
451 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
453 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
455 Apply $\merge$: $D \isin C \equiv D \isin L$. OK.
459 \subsection{Unique Base}
461 Need to consider only $C \in \py$, ie $L \in \py$.
465 xxx need to finish anticommit
469 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
471 C \hasparents \{ L, R \}
473 \patchof{C} = \patchof{L}
477 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
479 \subsection{Conditions}
481 \[ \eqn{ Tip Merge }{
484 R \in \py : & \baseof{R} \ge \baseof{L}
485 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
486 R \in \pn : & R \ge \baseof{L}
487 \land M = \baseof{L} \\
488 \text{otherwise} : & \false
491 \[ \eqn{ Removal Merge Ends }{
492 X \not\haspatch \p \land
496 \pendsof{Y}{\py} = \pendsof{M}{\py}
498 \[ \eqn{ Addition Merge Ends }{
499 X \not\haspatch \p \land
503 \bigforall_{E \in \pendsof{X}{\py}} E \le Y
507 \subsection{No Replay}
509 See No Replay for Merge Results.
511 \subsection{Unique Base}
513 Need to consider only $C \in \py$, ie $L \in \py$,
514 and calculate $\pendsof{C}{\pn}$. So we will consider some
515 putative ancestor $A \in \pn$ and see whether $A \le C$.
517 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
518 But $C \in py$ and $A \in \pn$ so $A \neq C$.
519 Thus $A \le C \equiv A \le L \lor A \le R$.
521 By Unique Base of L and Transitive Ancestors,
522 $A \le L \equiv A \le \baseof{L}$.
524 \subsubsection{For $R \in \py$:}
526 By Unique Base of $R$ and Transitive Ancestors,
527 $A \le R \equiv A \le \baseof{R}$.
529 But by Tip Merge condition on $\baseof{R}$,
530 $A \le \baseof{L} \implies A \le \baseof{R}$, so
531 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
532 Thus $A \le C \equiv A \le \baseof{R}$.
533 That is, $\baseof{C} = \baseof{R}$.
535 \subsubsection{For $R \in \pn$:}
537 By Tip Merge condition on $R$,
538 $A \le \baseof{L} \implies A \le R$, so
539 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
540 Thus $A \le C \equiv A \le R$.
541 That is, $\baseof{C} = R$.
545 \subsection{Coherence and patch inclusion}
547 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
548 This involves considering $D \in \py$.
550 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
551 $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
552 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch). So $D \neq C$.
553 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
555 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
556 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
557 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
559 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
561 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
562 \equiv D \isin L \lor D \isin R$.
563 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
565 Consider $D \neq C, D \isin X \land D \isin Y$:
566 By $\merge$, $D \isin C$. Also $D \le X$
567 so $D \le C$. OK for $C \haspatch \p$.
569 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
570 By $\merge$, $D \not\isin C$.
571 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
572 OK for $C \haspatch \p$.
574 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
575 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
576 Thus by $\merge$, $D \isin C$. And $D \le Y$ so $D \le C$.
577 OK for $C \haspatch \p$.
579 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
581 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
583 $C \haspatch \p \equiv M \nothaspatch \p$.
587 One of the Merge Ends conditions applies.
588 Recall that we are considering $D \in \py$.
589 $D \isin Y \equiv D \le Y$. $D \not\isin X$.
590 We will show for each of
591 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
592 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
594 Consider $D = C$: Thus $C \in \py, L \in \py$, and by Tip
595 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$. By Tip Merge,
596 $M=\baseof{L}$. So by Base Acyclic $D \not\isin M$, i.e.
597 $M \nothaspatch \p$. And indeed $D \isin C$ and $D \le C$. OK.
599 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
600 $D \le Y$ so $D \le C$.
601 $D \not\isin M$ so by $\merge$, $D \isin C$. OK.
603 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
604 $D \not\le Y$. If $D \le X$ then
605 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
606 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
607 Thus $D \not\le C$. By $\merge$, $D \not\isin C$. OK.
609 Consider $D \neq C, M \haspatch P, D \isin Y$:
610 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
611 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
612 Thus $D \isin M$. By $\merge$, $D \not\isin C$. OK.
614 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
615 By $\merge$, $D \not\isin C$. OK.