1 \documentclass[a4paper,leqno]{strayman}
3 \let\numberwithin=\notdef
11 \renewcommand{\ge}{\geqslant}
12 \renewcommand{\le}{\leqslant}
14 \newcommand{\has}{\sqsupseteq}
15 \newcommand{\isin}{\sqsubseteq}
17 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
18 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
19 \newcommand{\haspatch}{\sqSupset}
20 \newcommand{\patchisin}{\sqSubset}
22 \newif\ifhidehack\hidehackfalse
23 \DeclareRobustCommand\hidefromedef[2]{%
24 \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
25 \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
27 \newcommand{\set}[1]{\mathbb{#1}}
28 \newcommand{\pay}[1]{\pa{#1}^+}
29 \newcommand{\pan}[1]{\pa{#1}^-}
31 \newcommand{\p}{\pa{P}}
32 \newcommand{\py}{\pay{P}}
33 \newcommand{\pn}{\pan{P}}
35 \newcommand{\pr}{\pa{R}}
36 \newcommand{\pry}{\pay{R}}
37 \newcommand{\prn}{\pan{R}}
39 %\newcommand{\hasparents}{\underaccent{1}{>}}
40 %\newcommand{\hasparents}{{%
41 % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
42 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
43 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
45 \renewcommand{\implies}{\Rightarrow}
46 \renewcommand{\equiv}{\Leftrightarrow}
47 \renewcommand{\land}{\wedge}
48 \renewcommand{\lor}{\vee}
50 \newcommand{\pancs}{{\mathcal A}}
51 \newcommand{\pends}{{\mathcal E}}
53 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
54 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
56 \newcommand{\merge}[4]{{\mathcal M}(#1,#2,#3,#4)}
57 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
59 \newcommand{\patch}{{\mathcal P}}
60 \newcommand{\base}{{\mathcal B}}
62 \newcommand{\patchof}[1]{\patch ( #1 ) }
63 \newcommand{\baseof}[1]{\base ( #1 ) }
65 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
66 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
68 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
69 \newcommand{\bigforall}{%
71 {\hbox{\huge$\forall$}}%
72 {\hbox{\Large$\forall$}}%
73 {\hbox{\normalsize$\forall$}}%
74 {\hbox{\scriptsize$\forall$}}}%
77 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
78 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
80 \newcommand{\qed}{\square}
81 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
83 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
84 \newcommand{\gathnext}{\\ \tag*{}}
87 \newcommand{\false}{f}
95 \desclabelstyle{\nextlinelabel}
97 \item[ $ C \hasparents \set X $ ]
98 The parents of commit $C$ are exactly the set
102 $C$ is a descendant of $D$ in the git commit
103 graph. This is a partial order, namely the transitive closure of
104 $ D \in \set X $ where $ C \hasparents \set X $.
106 \item[ $ C \has D $ ]
107 Informally, the tree at commit $C$ contains the change
108 made in commit $D$. Does not take account of deliberate reversions by
109 the user or reversion, rebasing or rewinding in
110 non-Topbloke-controlled branches. For merges and Topbloke-generated
111 anticommits or re-commits, the ``change made'' is only to be thought
112 of as any conflict resolution. This is not a partial order because it
115 \item[ $ \p, \py, \pn $ ]
116 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
117 are respectively the base and tip git branches. $\p$ may be used
118 where the context requires a set, in which case the statement
119 is to be taken as applying to both $\py$ and $\pn$.
120 All these sets are distinct. Hence:
122 \item[ $ \patchof{ C } $ ]
123 Either $\p$ s.t. $ C \in \p $, or $\bot$.
124 A function from commits to patches' sets $\p$.
126 \item[ $ \pancsof{C}{\set P} $ ]
127 $ \{ A \; | \; A \le C \land A \in \set P \} $
128 i.e. all the ancestors of $C$
129 which are in $\set P$.
131 \item[ $ \pendsof{C}{\set P} $ ]
132 $ \{ E \; | \; E \in \pancsof{C}{\set P}
133 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
134 E \neq A \land E \le A \} $
135 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
137 \item[ $ \baseof{C} $ ]
138 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
139 A partial function from commits to commits.
140 See Unique Base, below.
142 \item[ $ C \haspatch \p $ ]
143 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
144 ~ Informally, $C$ has the contents of $\p$.
146 \item[ $ C \nothaspatch \p $ ]
147 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
148 ~ Informally, $C$ has none of the contents of $\p$.
150 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
151 patch is applied to a non-Topbloke branch and then bubbles back to
152 the Topbloke patch itself, we hope that git's merge algorithm will
153 DTRT or that the user will no longer care about the Topbloke patch.
155 \item[ $\displaystyle \merge{C}{L}{M}{R} $ ]
156 The contents of a git merge result:
158 $\displaystyle D \isin C \equiv
160 (D \isin L \land D \isin R) \lor D = C : & \true \\
161 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
162 \text{otherwise} : & D \not\isin M
170 We maintain these each time we construct a new commit. \\
172 C \has D \implies C \ge D
174 \[\eqn{Unique Base:}{
175 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
177 \[\eqn{Tip Contents:}{
178 \bigforall_{C \in \py} D \isin C \equiv
179 { D \isin \baseof{C} \lor \atop
180 (D \in \py \land D \le C) }
182 \[\eqn{Base Acyclic:}{
183 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
186 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
188 \[\eqn{Foreign Inclusion:}{
189 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
192 \section{Some lemmas}
194 \[ \eqn{Exclusive Tip Contents:}{
195 \bigforall_{C \in \py}
196 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
199 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
202 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
203 So by Base Acyclic $D \isin B \implies D \notin \py$.
206 \bigforall_{C \in \py} D \isin C \equiv
208 D \in \py : & D \le C \\
209 D \not\in \py : & D \isin \baseof{C}
213 \[ \eqn{Tip Self Inpatch:}{
214 \bigforall_{C \in \py} C \haspatch \p
216 Ie, tip commits contain their own patch.
219 Apply Exclusive Tip Contents to some $D \in \py$:
220 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
221 D \isin C \equiv D \le C $
224 \[ \eqn{Exact Ancestors:}{
225 \bigforall_{ C \hasparents \set{R} }
227 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
231 \[ \eqn{Transitive Ancestors:}{
232 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
233 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
237 The implication from right to left is trivial because
238 $ \pends() \subset \pancs() $.
239 For the implication from left to right:
240 by the definition of $\mathcal E$,
241 for every such $A$, either $A \in \pends()$ which implies
242 $A \le M$ by the LHS directly,
243 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
244 in which case we repeat for $A'$. Since there are finitely many
245 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
246 by the LHS. And $A \le A''$.
248 \[ \eqn{Calculation Of Ends:}{
249 \bigforall_{C \hasparents \set A}
250 \pendsof{C}{\set P} =
252 \Bigl[ \Largeexists_{A \in \set A}
253 E \in \pendsof{A}{\set P} \Bigr] \land
254 \Bigl[ \Largenexists_{B \in \set A}
255 E \neq B \land E \le B \Bigr]
260 \subsection{No Replay for Merge Results}
262 If we are constructing $C$, given
270 No Replay is preserved. {\it Proof:}
272 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
274 \subsubsection{For $D \isin L \land D \isin R$:}
275 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
277 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
280 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
281 \land D \not\isin M$:}
282 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
285 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
291 \section{Commit annotation}
293 We annotate each Topbloke commit $C$ with:
297 \baseof{C}, \text{ if } C \in \py
300 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
302 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
305 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
306 make it wrong to make plain commits with git because the recorded $\pends$
307 would have to be updated. The annotation is not needed because
308 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
310 \section{Simple commit}
312 A simple single-parent forward commit $C$ as made by git-commit.
314 \tag*{} C \hasparents \{ A \} \\
315 \tag*{} \patchof{C} = \patchof{A} \\
316 \tag*{} D \isin C \equiv D \isin A \lor D = C
319 \subsection{No Replay}
322 \subsection{Unique Base}
323 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
325 \subsection{Tip Contents}
326 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
327 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
328 Substitute into the contents of $C$:
329 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
331 Since $D = C \implies D \in \py$,
332 and substituting in $\baseof{C}$, this gives:
333 \[ D \isin C \equiv D \isin \baseof{C} \lor
334 (D \in \py \land D \le A) \lor
335 (D = C \land D \in \py) \]
336 \[ \equiv D \isin \baseof{C} \lor
337 [ D \in \py \land ( D \le A \lor D = C ) ] \]
338 So by Exact Ancestors:
339 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
343 \subsection{Base Acyclic}
345 Need to consider only $A, C \in \pn$.
347 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
349 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
350 $A$, $D \isin C \implies D \not\in \py$. $\qed$
352 \subsection{Coherence and patch inclusion}
354 Need to consider $D \in \py$
356 \subsubsection{For $A \haspatch P, D = C$:}
362 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
364 \subsubsection{For $A \haspatch P, D \neq C$:}
365 Ancestors: $ D \le C \equiv D \le A $.
367 Contents: $ D \isin C \equiv D \isin A \lor f $
368 so $ D \isin C \equiv D \isin A $.
371 \[ A \haspatch P \implies C \haspatch P \]
373 \subsubsection{For $A \nothaspatch P$:}
375 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
378 Now by contents of $A$, $D \notin A$, so $D \notin C$.
381 \[ A \nothaspatch P \implies C \nothaspatch P \]
384 \subsection{Foreign inclusion:}
386 If $D = C$, trivial. For $D \neq C$:
387 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
391 Given $L, R^+, R^-$ where
392 $\patchof{R^+} = \pry, \patchof{R^-} = \prn$.
393 Construct $C$ which has $\pr$ removed.
394 Used for removing a branch dependency.
396 C \hasparents \{ L \}
398 \patchof{C} = \patchof{L}
400 \merge{C}{L}{R^+}{R^-}
403 \subsection{Conditions}
405 \[ \eqn{ Unique Tip }{
406 \pendsof{L}{\pry} = \{ R^+ \}
408 \[ \eqn{ Correct Base }{
411 \[ \eqn{ Currently Included }{
417 xxx want to prove $D \isin C \equiv D \not\in \pry \land D \isin L$.
421 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
423 C \hasparents \{ L, R \}
425 \patchof{C} = \patchof{L}
430 \subsection{Conditions}
432 \[ \eqn{ Tip Merge }{
435 R \in \py : & \baseof{R} \ge \baseof{L}
436 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
437 R \in \pn : & R \ge \baseof{L}
438 \land M = \baseof{L} \\
439 \text{otherwise} : & \false
443 \subsection{Merge Results}
447 \subsection{Unique Base}
449 Need to consider only $C \in \py$, ie $L \in \py$,
450 and calculate $\pendsof{C}{\pn}$. So we will consider some
451 putative ancestor $A \in \pn$ and see whether $A \le C$.
453 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
454 But $C \in py$ and $A \in \pn$ so $A \neq C$.
455 Thus $A \le C \equiv A \le L \lor A \le R$.
457 By Unique Base of L and Transitive Ancestors,
458 $A \le L \equiv A \le \baseof{L}$.
460 \subsubsection{For $R \in \py$:}
462 By Unique Base of $R$ and Transitive Ancestors,
463 $A \le R \equiv A \le \baseof{R}$.
465 But by Tip Merge condition on $\baseof{R}$,
466 $A \le \baseof{L} \implies A \le \baseof{R}$, so
467 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
468 Thus $A \le C \equiv A \le \baseof{R}$.
469 That is, $\baseof{C} = \baseof{R}$.
471 \subsubsection{For $R \in \pn$:}
473 By Tip Merge condition on $R$,
474 $A \le \baseof{L} \implies A \le R$, so
475 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
476 Thus $A \le C \equiv A \le R$.
477 That is, $\baseof{C} = R$.