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{\patchof}[1]{{\mathcal P} ( #1 ) }
60 \newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }
62 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
63 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
65 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
66 \newcommand{\bigforall}{%
68 {\hbox{\huge$\forall$}}%
69 {\hbox{\Large$\forall$}}%
70 {\hbox{\normalsize$\forall$}}%
71 {\hbox{\scriptsize$\forall$}}}%
74 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
75 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
77 \newcommand{\qed}{\square}
78 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
80 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
81 \newcommand{\gathnext}{\\ \tag*{}}
84 \newcommand{\false}{f}
92 \desclabelstyle{\nextlinelabel}
94 \item[ $ C \hasparents \set X $ ]
95 The parents of commit $C$ are exactly the set
99 $C$ is a descendant of $D$ in the git commit
100 graph. This is a partial order, namely the transitive closure of
101 $ D \in \set X $ where $ C \hasparents \set X $.
103 \item[ $ C \has D $ ]
104 Informally, the tree at commit $C$ contains the change
105 made in commit $D$. Does not take account of deliberate reversions by
106 the user or reversion, rebasing or rewinding in
107 non-Topbloke-controlled branches. For merges and Topbloke-generated
108 anticommits or re-commits, the ``change made'' is only to be thought
109 of as any conflict resolution. This is not a partial order because it
112 \item[ $ \p, \py, \pn $ ]
113 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
114 are respectively the base and tip git branches. $\p$ may be used
115 where the context requires a set, in which case the statement
116 is to be taken as applying to both $\py$ and $\pn$.
117 All these sets are distinct. Hence:
119 \item[ $ \patchof{ C } $ ]
120 Either $\p$ s.t. $ C \in \p $, or $\bot$.
121 A function from commits to patches' sets $\p$.
123 \item[ $ \pancsof{C}{\set P} $ ]
124 $ \{ A \; | \; A \le C \land A \in \set P \} $
125 i.e. all the ancestors of $C$
126 which are in $\set P$.
128 \item[ $ \pendsof{C}{\set P} $ ]
129 $ \{ E \; | \; E \in \pancsof{C}{\set P}
130 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
131 E \neq A \land E \le A \} $
132 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
134 \item[ $ \baseof{C} $ ]
135 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
136 A partial function from commits to commits.
137 See Unique Base, below.
139 \item[ $ C \haspatch \p $ ]
140 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
141 ~ Informally, $C$ has the contents of $\p$.
143 \item[ $ C \nothaspatch \p $ ]
144 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
145 ~ Informally, $C$ has none of the contents of $\p$.
147 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
148 patch is applied to a non-Topbloke branch and then bubbles back to
149 the Topbloke patch itself, we hope that git's merge algorithm will
150 DTRT or that the user will no longer care about the Topbloke patch.
152 \item[ $\displaystyle \merge{C}{L}{M}{R} $ ]
153 The contents of a git merge result:
155 $\displaystyle D \isin C \equiv
157 (D \isin L \land D \isin R) \lor D = C : & \true \\
158 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
159 \text{otherwise} : & D \not\isin M
167 We maintain these each time we construct a new commit. \\
169 C \has D \implies C \ge D
171 \[\eqn{Unique Base:}{
172 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
174 \[\eqn{Tip Contents:}{
175 \bigforall_{C \in \py} D \isin C \equiv
176 { D \isin \baseof{C} \lor \atop
177 (D \in \py \land D \le C) }
179 \[\eqn{Base Acyclic:}{
180 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
183 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
185 \[\eqn{Foreign Inclusion:}{
186 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
189 \section{Some lemmas}
191 \[ \eqn{Exclusive Tip Contents:}{
192 \bigforall_{C \in \py}
193 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
196 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
199 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
200 So by Base Acyclic $D \isin B \implies D \notin \py$.
203 \bigforall_{C \in \py} D \isin C \equiv
205 D \in \py : & D \le C \\
206 D \not\in \py : & D \isin \baseof{C}
210 \[ \eqn{Tip Self Inpatch:}{
211 \bigforall_{C \in \py} C \haspatch \p
213 Ie, tip commits contain their own patch.
216 Apply Exclusive Tip Contents to some $D \in \py$:
217 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
218 D \isin C \equiv D \le C $
221 \[ \eqn{Exact Ancestors:}{
222 \bigforall_{ C \hasparents \set{R} }
224 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
228 \[ \eqn{Transitive Ancestors:}{
229 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
230 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
234 The implication from right to left is trivial because
235 $ \pends() \subset \pancs() $.
236 For the implication from left to right:
237 by the definition of $\mathcal E$,
238 for every such $A$, either $A \in \pends()$ which implies
239 $A \le M$ by the LHS directly,
240 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
241 in which case we repeat for $A'$. Since there are finitely many
242 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
243 by the LHS. And $A \le A''$.
245 \[ \eqn{Calculation Of Ends:}{
246 \bigforall_{C \hasparents \set A}
247 \pendsof{C}{\set P} =
249 \Bigl[ \Largeexists_{A \in \set A}
250 E \in \pendsof{A}{\set P} \Bigr] \land
251 \Bigl[ \Largenexists_{B \in \set A}
252 E \neq B \land E \le B \Bigr]
257 \section{Commit annotation}
259 We annotate each Topbloke commit $C$ with:
263 \baseof{C}, \text{ if } C \in \py
266 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
268 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
271 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
272 make it wrong to make plain commits with git because the recorded $\pends$
273 would have to be updated. The annotation is not needed because
274 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
276 \section{Simple commit}
278 A simple single-parent forward commit $C$ as made by git-commit.
280 \tag*{} C \hasparents \{ A \} \\
281 \tag*{} \patchof{C} = \patchof{A} \\
282 \tag*{} D \isin C \equiv D \isin A \lor D = C
285 \subsection{No Replay}
288 \subsection{Unique Base}
289 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
291 \subsection{Tip Contents}
292 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
293 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
294 Substitute into the contents of $C$:
295 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
297 Since $D = C \implies D \in \py$,
298 and substituting in $\baseof{C}$, this gives:
299 \[ D \isin C \equiv D \isin \baseof{C} \lor
300 (D \in \py \land D \le A) \lor
301 (D = C \land D \in \py) \]
302 \[ \equiv D \isin \baseof{C} \lor
303 [ D \in \py \land ( D \le A \lor D = C ) ] \]
304 So by Exact Ancestors:
305 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
309 \subsection{Base Acyclic}
311 Need to consider only $A, C \in \pn$.
313 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
315 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
316 $A$, $D \isin C \implies D \not\in \py$. $\qed$
318 \subsection{Coherence and patch inclusion}
320 Need to consider $D \in \py$
322 \subsubsection{For $A \haspatch P, D = C$:}
328 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
330 \subsubsection{For $A \haspatch P, D \neq C$:}
331 Ancestors: $ D \le C \equiv D \le A $.
333 Contents: $ D \isin C \equiv D \isin A \lor f $
334 so $ D \isin C \equiv D \isin A $.
337 \[ A \haspatch P \implies C \haspatch P \]
339 \subsubsection{For $A \nothaspatch P$:}
341 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
344 Now by contents of $A$, $D \notin A$, so $D \notin C$.
347 \[ A \nothaspatch P \implies C \nothaspatch P \]
350 \subsection{Foreign inclusion:}
352 If $D = C$, trivial. For $D \neq C$:
353 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
357 Given $L, R^+, R^-$ where
358 $\patchof{R^+} = \pry, \patchof{R^-} = \prn$.
359 Construct $C$ which has $\pr$ removed.
360 Used for removing a branch dependency.
362 C \hasparents \{ L \}
364 \patchof{C} = \patchof{L}
368 R \in \py : & \baseof{R} \ge \baseof{L}
369 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
370 R \in \pn : & R \ge \baseof{L}
371 \land M = \baseof{L} \\
372 \text{otherwise} : & \false
376 xxx want to prove $D \isin C \equiv D \not\in pry \land D \isin L$.
380 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
382 C \hasparents \{ L, R \}
384 \patchof{C} = \patchof{L}
388 (D \isin L \land D \isin R) \lor D = C : & \true \\
389 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
390 \text{otherwise} : & D \not\isin M
394 \subsection{Conditions}
396 \[ \eqn{ Tip Merge }{
399 R \in \py : & \baseof{R} \ge \baseof{L}
400 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
401 R \in \pn : & R \ge \baseof{L}
402 \land M = \baseof{L} \\
403 \text{otherwise} : & \false
407 \subsection{No Replay}
409 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
411 \subsubsection{For $D \isin L \land D \isin R$:}
412 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
414 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
417 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
420 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
421 \land D \not\isin M$:}
422 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
425 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
427 $D \not\isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
432 \subsection{Unique Base}
434 Need to consider only $C \in \py$, ie $L \in \py$,
435 and calculate $\pendsof{C}{\pn}$. So we will consider some
436 putative ancestor $A \in \pn$ and see whether $A \le C$.
438 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
439 But $C \in py$ and $A \in \pn$ so $A \neq C$.
440 Thus $A \le C \equiv A \le L \lor A \le R$.
442 By Unique Base of L and Transitive Ancestors,
443 $A \le L \equiv A \le \baseof{L}$.
445 \subsubsection{For $R \in \py$:}
447 By Unique Base of $R$ and Transitive Ancestors,
448 $A \le R \equiv A \le \baseof{R}$.
450 But by Tip Merge condition on $\baseof{R}$,
451 $A \le \baseof{L} \implies A \le \baseof{R}$, so
452 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
453 Thus $A \le C \equiv A \le \baseof{R}$.
454 That is, $\baseof{C} = \baseof{R}$.
456 \subsubsection{For $R \in \pn$:}
458 By Tip Merge condition on $R$,
459 $A \le \baseof{L} \implies A \le R$, so
460 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
461 Thus $A \le C \equiv A \le R$.
462 That is, $\baseof{C} = R$.