1 \documentclass[a4paper,leqno]{strayman}
2 \let\numberwithin=\notdef
10 \renewcommand{\ge}{\geqslant}
11 \renewcommand{\le}{\leqslant}
13 \newcommand{\has}{\sqsupseteq}
14 \newcommand{\isin}{\sqsubseteq}
16 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
17 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
18 \newcommand{\haspatch}{\sqSupset}
19 \newcommand{\patchisin}{\sqSubset}
21 \newif\ifhidehack\hidehackfalse
22 \DeclareRobustCommand\hidefromedef[2]{%
23 \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
24 \newcommand{\pa}[1]{\hidefromedef{\varmathbb #1}{#1}}
26 \newcommand{\set}[1]{\mathbb #1}
27 \newcommand{\pay}[1]{\pa{#1}^+}
28 \newcommand{\pan}[1]{\pa{#1}^-}
30 \newcommand{\p}{\pa{P}}
31 \newcommand{\py}{\pay{P}}
32 \newcommand{\pn}{\pan{P}}
34 %\newcommand{\hasparents}{\underaccent{1}{>}}
35 %\newcommand{\hasparents}{{%
36 % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
37 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
38 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
40 \renewcommand{\implies}{\Rightarrow}
41 \renewcommand{\equiv}{\Leftrightarrow}
42 \renewcommand{\land}{\wedge}
43 \renewcommand{\lor}{\vee}
45 \newcommand{\pancs}{{\mathcal A}}
46 \newcommand{\pends}{{\mathcal E}}
48 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
49 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
51 \newcommand{\patchof}[1]{{\mathcal P} ( #1 ) }
52 \newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }
54 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
55 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
57 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
58 \newcommand{\bigforall}{%
60 {\hbox{\huge$\forall$}}%
61 {\hbox{\Large$\forall$}}%
62 {\hbox{\normalsize$\forall$}}%
63 {\hbox{\scriptsize$\forall$}}}%
66 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
67 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
69 \newcommand{\qed}{\square}
70 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
72 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
73 \newcommand{\gathnext}{\\ \tag*{}}
76 \newcommand{\false}{f}
84 \desclabelstyle{\nextlinelabel}
86 \item[ $ C \hasparents \set X $ ]
87 The parents of commit $C$ are exactly the set
91 $C$ is a descendant of $D$ in the git commit
92 graph. This is a partial order, namely the transitive closure of
93 $ D \in \set X $ where $ C \hasparents \set X $.
96 Informally, the tree at commit $C$ contains the change
97 made in commit $D$. Does not take account of deliberate reversions by
98 the user or reversion, rebasing or rewinding in
99 non-Topbloke-controlled branches. For merges and Topbloke-generated
100 anticommits or re-commits, the ``change made'' is only to be thought
101 of as any conflict resolution. This is not a partial order because it
104 \item[ $ \p, \py, \pn $ ]
105 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
106 are respectively the base and tip git branches. $\p$ may be used
107 where the context requires a set, in which case the statement
108 is to be taken as applying to both $\py$ and $\pn$.
109 All these sets are distinct. Hence:
111 \item[ $ \patchof{ C } $ ]
112 Either $\p$ s.t. $ C \in \p $, or $\bot$.
113 A function from commits to patches' sets $\p$.
115 \item[ $ \pancsof{C}{\set P} $ ]
116 $ \{ A \; | \; A \le C \land A \in \set P \} $
117 i.e. all the ancestors of $C$
118 which are in $\set P$.
120 \item[ $ \pendsof{C}{\set P} $ ]
121 $ \{ E \; | \; E \in \pancsof{C}{\set P}
122 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
123 E \neq A \land E \le A \} $
124 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
126 \item[ $ \baseof{C} $ ]
127 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
128 A partial function from commits to commits.
129 See Unique Base, below.
131 \item[ $ C \haspatch \p $ ]
132 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
133 ~ Informally, $C$ has the contents of $\p$.
135 \item[ $ C \nothaspatch \p $ ]
136 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
137 ~ Informally, $C$ has none of the contents of $\p$.
139 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
140 patch is applied to a non-Topbloke branch and then bubbles back to
141 the Topbloke patch itself, we hope that git's merge algorithm will
142 DTRT or that the user will no longer care about the Topbloke patch.
148 We maintain these each time we construct a new commit. \\
150 C \has D \implies C \ge D
152 \[\eqn{Unique Base:}{
153 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
155 \[\eqn{Tip Contents:}{
156 \bigforall_{C \in \py} D \isin C \equiv
157 { D \isin \baseof{C} \lor \atop
158 (D \in \py \land D \le C) }
160 \[\eqn{Base Acyclic:}{
161 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
164 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
166 \[\eqn{Foreign Inclusion:}{
167 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
170 \section{Some lemmas}
172 \[ \eqn{Exclusive Tip Contents:}{
173 \bigforall_{C \in \py}
174 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
177 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
180 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
181 So by Base Acyclic $D \isin B \implies D \notin \py$.
184 \bigforall_{C \in \py} D \isin C \equiv
186 D \in \py : & D \le C \\
187 D \not\in \py : & D \isin \baseof{C}
191 \[ \eqn{Tip Self Inpatch:}{
192 \bigforall_{C \in \py} C \haspatch \p
194 Ie, tip commits contain their own patch.
197 Apply Exclusive Tip Contents to some $D \in \py$:
198 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
199 D \isin C \equiv D \le C $
202 \[ \eqn{Exact Ancestors:}{
203 \bigforall_{ C \hasparents \set{R} }
205 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
209 \[ \eqn{Transitive Ancestors:}{
210 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
211 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
215 The implication from right to left is trivial because
216 $ \pends() \subset \pancs() $.
217 For the implication from left to right:
218 by the definition of $\mathcal E$,
219 for every such $A$, either $A \in \pends()$ which implies
220 $A \le M$ by the LHS directly,
221 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
222 in which case we repeat for $A'$. Since there are finitely many
223 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
224 by the LHS. And $A \le A''$.
226 \[ \eqn{Calculation Of Ends:}{
227 \bigforall_{C \hasparents \set A}
228 \pendsof{C}{\set P} =
230 \Bigl[ \Largeexists_{A \in \set A}
231 E \in \pendsof{A}{\set P} \Bigr] \land
232 \Bigl[ \Largenexists_{B \in \set A}
233 E \neq B \land E \le B \Bigr]
238 \section{Commit annotation}
240 We annotate each Topbloke commit $C$ with:
244 \baseof{C}, \text{ if } C \in \py
247 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
249 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
252 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
253 make it wrong to make plain commits with git because the recorded $\pends$
254 would have to be updated. The annotation is not needed because
255 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
257 \section{Simple commit}
259 A simple single-parent forward commit $C$ as made by git-commit.
261 \tag*{} C \hasparents \{ A \} \\
262 \tag*{} \patchof{C} = \patchof{A} \\
263 \tag*{} D \isin C \equiv D \isin A \lor D = C
266 \subsection{No Replay}
269 \subsection{Unique Base}
270 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
272 \subsection{Tip Contents}
273 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
274 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
275 Substitute into the contents of $C$:
276 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
278 Since $D = C \implies D \in \py$,
279 and substituting in $\baseof{C}$, this gives:
280 \[ D \isin C \equiv D \isin \baseof{C} \lor
281 (D \in \py \land D \le A) \lor
282 (D = C \land D \in \py) \]
283 \[ \equiv D \isin \baseof{C} \lor
284 [ D \in \py \land ( D \le A \lor D = C ) ] \]
285 So by Exact Ancestors:
286 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
290 \subsection{Base Acyclic}
292 Need to consider only $A, C \in \pn$.
294 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
296 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
297 $A$, $D \isin C \implies D \not\in \py$. $\qed$
299 \subsection{Coherence and patch inclusion}
301 Need to consider $D \in \py$
303 \subsubsection{For $A \haspatch P, D = C$:}
309 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
311 \subsubsection{For $A \haspatch P, D \neq C$:}
312 Ancestors: $ D \le C \equiv D \le A $.
314 Contents: $ D \isin C \equiv D \isin A \lor f $
315 so $ D \isin C \equiv D \isin A $.
318 \[ A \haspatch P \implies C \haspatch P \]
320 \subsubsection{For $A \nothaspatch P$:}
322 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
325 Now by contents of $A$, $D \notin A$, so $D \notin C$.
328 \[ A \nothaspatch P \implies C \nothaspatch P \]
331 \subsection{Foreign inclusion:}
333 If $D = C$, trivial. For $D \neq C$:
334 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
338 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
340 C \hasparents \{ L, R \}
342 \patchof{C} = \patchof{L}
346 (D \isin L \land D \isin R) \lor D = C : & \true \\
347 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
348 \text{otherwise} : & D \not\isin M
352 \subsection{Conditions}
354 \[ \eqn{ Tip Merge }{
357 R \in \py : & \baseof{R} \ge \baseof{L}
358 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
359 R \in \pn : & R \ge \baseof{L}
360 \land M = \baseof{L} \\
361 \text{otherwise} : & \false
365 \subsection{No Replay}
367 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
369 \subsubsection{For $D \isin L \land D \isin R$:}
370 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
372 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
375 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
378 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
379 \land D \not\isin M$:}
380 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
383 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
385 $D \not\isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
390 \subsection{Unique Base}
392 Need to consider only $C \in \py$, ie $L \in \py$,
393 and calculate $\pendsof{C}{\pn}$. So we will consider some
394 putative ancestor $A \in \pn$ and see whether $A \le C$.
396 $A \le C \equiv A \le L \lor A \le R \lor A = C$.
397 But $C \in py$ and $A \in \pn$ so $A \neq C$.
398 Thus $A \le L \lor A \le R$.
400 By Unique Base of L and Transitive Ancestors,
401 $A \le L \equiv A \le \baseof{L}$.
403 \subsubsection{For $R \in \py$:}
405 By Unique Base of $R$ and Transitive Ancestors,
406 $A \le R \equiv A \le \baseof{R}$.
408 But by Tip Merge condition on $\baseof{R}$,
409 $A \le \baseof{L} \implies A \le \baseof{R}$, so
410 $A \le \baseof{R} \lor A \le \baseof{R} \equiv A \le \baseof{R}$.
411 Thus $A \le C \equiv A \le \baseof{R}$. Ie, $\baseof{C} =
416 By Tip Merge, $A \le $
420 R \in \py : & \baseof{R} \\
423 Then by Tip Merge $S \ge \baseof{L}$, and $R \ge S$ so $C \ge S$.
425 Consider some $A \in \pn$. If $A \le S$ then $A \le C$.
426 If $A \not\le S$ then
428 Let $A \in \pends{C}{\pn}$.
429 Then by Calculation Of Ends $A \in \pendsof{L,\pn} \lor A \in
436 %%\subsubsection{For $R \in \py$:}