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 \newcommand{\set}[1]{\mathbb #1}
22 \newcommand{\pa}[1]{\varmathbb #1}
23 \newcommand{\pay}[1]{\pa{#1}^+}
24 \newcommand{\pan}[1]{\pa{#1}^-}
26 \newcommand{\p}{\pa{P}}
27 \newcommand{\py}{\pay{P}}
28 \newcommand{\pn}{\pan{P}}
30 %\newcommand{\hasparents}{\underaccent{1}{>}}
31 %\newcommand{\hasparents}{{%
32 % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
33 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
34 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
36 \renewcommand{\implies}{\Rightarrow}
37 \renewcommand{\equiv}{\Leftrightarrow}
38 \renewcommand{\land}{\wedge}
39 \renewcommand{\lor}{\vee}
41 \newcommand{\pancs}{{\mathcal A}}
42 \newcommand{\pends}{{\mathcal E}}
44 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
45 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
47 \newcommand{\patchof}[1]{{\mathcal P} ( #1 ) }
48 \newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }
50 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
51 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
53 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
54 \newcommand{\bigforall}{%
56 {\hbox{\huge$\forall$}}%
57 {\hbox{\Large$\forall$}}%
58 {\hbox{\normalsize$\forall$}}%
59 {\hbox{\scriptsize$\forall$}}}%
62 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
63 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
65 \newcommand{\qed}{\square}
66 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
68 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
69 \newcommand{\gathnext}{\\ \tag*{}}
72 \newcommand{\false}{f}
80 \desclabelstyle{\nextlinelabel}
82 \item[ $ C \hasparents \set X $ ]
83 The parents of commit $C$ are exactly the set
87 $C$ is a descendant of $D$ in the git commit
88 graph. This is a partial order, namely the transitive closure of
89 $ D \in \set X $ where $ C \hasparents \set X $.
92 Informally, the tree at commit $C$ contains the change
93 made in commit $D$. Does not take account of deliberate reversions by
94 the user or reversion, rebasing or rewinding in
95 non-Topbloke-controlled branches. For merges and Topbloke-generated
96 anticommits or re-commits, the ``change made'' is only to be thought
97 of as any conflict resolution. This is not a partial order because it
100 \item[ $ \p, \py, \pn $ ]
101 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
102 are respectively the base and tip git branches. $\p$ may be used
103 where the context requires a set, in which case the statement
104 is to be taken as applying to both $\py$ and $\pn$.
105 All these sets are distinct. Hence:
107 \item[ $ \patchof{ C } $ ]
108 Either $\p$ s.t. $ C \in \p $, or $\bot$.
109 A function from commits to patches' sets $\p$.
111 \item[ $ \pancsof{C}{\set P} $ ]
112 $ \{ A \; | \; A \le C \land A \in \set P \} $
113 i.e. all the ancestors of $C$
114 which are in $\set P$.
116 \item[ $ \pendsof{C}{\set P} $ ]
117 $ \{ E \; | \; E \in \pancsof{C}{\set P}
118 \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
119 E \neq A \land E \le A \} $
120 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
122 \item[ $ \baseof{C} $ ]
123 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
124 A partial function from commits to commits.
125 See Unique Base, below.
127 \item[ $ C \haspatch \p $ ]
128 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
129 ~ Informally, $C$ has the contents of $\p$.
131 \item[ $ C \nothaspatch \p $ ]
132 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
133 ~ Informally, $C$ has none of the contents of $\p$.
135 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
136 patch is applied to a non-Topbloke branch and then bubbles back to
137 the Topbloke patch itself, we hope that git's merge algorithm will
138 DTRT or that the user will no longer care about the Topbloke patch.
144 We maintain these each time we construct a new commit. \\
146 C \has D \implies C \ge D
148 \[\eqn{Unique Base:}{
149 \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
151 \[\eqn{Tip Contents:}{
152 \bigforall_{C \in \py} D \isin C \equiv
153 { D \isin \baseof{C} \lor \atop
154 (D \in \py \land D \le C) }
156 \[\eqn{Base Acyclic:}{
157 \bigforall_{B \in \pn} D \isin B \implies D \notin \py
160 \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
162 \[\eqn{Foreign Inclusion:}{
163 \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
166 \section{Some lemmas}
168 \[ \eqn{Exclusive Tip Contents:}{
169 \bigforall_{C \in \py}
170 \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
173 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
176 Let $B = \baseof{C}$ in $D \isin \baseof{C}$. Now $B \in \pn$.
177 So by Base Acyclic $D \isin B \implies D \notin \py$.
180 \bigforall_{C \in \py} D \isin C \equiv
182 D \in \py : & D \le C \\
183 D \not\in \py : & D \isin \baseof{C}
187 \[ \eqn{Tip Self Inpatch:}{
188 \bigforall_{C \in \py} C \haspatch \p
190 Ie, tip commits contain their own patch.
193 Apply Exclusive Tip Contents to some $D \in \py$:
194 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
195 D \isin C \equiv D \le C $
198 \[ \eqn{Exact Ancestors:}{
199 \bigforall_{ C \hasparents \set{R} }
201 ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
205 \[ \eqn{Transitive Ancestors:}{
206 \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
207 \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
211 The implication from right to left is trivial because
212 $ \pends() \subset \pancs() $.
213 For the implication from left to right:
214 by the definition of $\mathcal E$,
215 for every such $A$, either $A \in \pends()$ which implies
216 $A \le M$ by the LHS directly,
217 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
218 in which case we repeat for $A'$. Since there are finitely many
219 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
220 by the LHS. And $A \le A''$.
222 \[ \eqn{Calculation Of Ends:}{
223 \bigforall_{C \hasparents \set A}
224 \pendsof{C}{\set P} =
226 \Bigl[ \Largeexists_{A \in \set A}
227 E \in \pendsof{A}{\set P} \Bigr] \land
228 \Bigl[ \Largenexists_{B \in \set A}
229 E \neq B \land E \le B \Bigr]
234 \section{Commit annotation}
236 We annotate each Topbloke commit $C$ with:
240 \baseof{C}, \text{ if } C \in \py
243 \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
245 \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
248 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
249 make it wrong to make plain commits with git because the recorded $\pends$
250 would have to be updated. The annotation is not needed because
251 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
253 \section{Simple commit}
255 A simple single-parent forward commit $C$ as made by git-commit.
257 \tag*{} C \hasparents \{ A \} \\
258 \tag*{} \patchof{C} = \patchof{A} \\
259 \tag*{} D \isin C \equiv D \isin A \lor D = C
262 \subsection{No Replay}
265 \subsection{Unique Base}
266 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
268 \subsection{Tip Contents}
269 We need to consider only $A, C \in \py$. From Tip Contents for $A$:
270 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
271 Substitute into the contents of $C$:
272 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
274 Since $D = C \implies D \in \py$,
275 and substituting in $\baseof{C}$, this gives:
276 \[ D \isin C \equiv D \isin \baseof{C} \lor
277 (D \in \py \land D \le A) \lor
278 (D = C \land D \in \py) \]
279 \[ \equiv D \isin \baseof{C} \lor
280 [ D \in \py \land ( D \le A \lor D = C ) ] \]
281 So by Exact Ancestors:
282 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
286 \subsection{Base Acyclic}
288 Need to consider only $A, C \in \pn$.
290 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
292 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
293 $A$, $D \isin C \implies D \not\in \py$. $\qed$
295 \subsection{Coherence and patch inclusion}
297 Need to consider $D \in \py$
299 \subsubsection{For $A \haspatch P, D = C$:}
305 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
307 \subsubsection{For $A \haspatch P, D \neq C$:}
308 Ancestors: $ D \le C \equiv D \le A $.
310 Contents: $ D \isin C \equiv D \isin A \lor f $
311 so $ D \isin C \equiv D \isin A $.
314 \[ A \haspatch P \implies C \haspatch P \]
316 \subsubsection{For $A \nothaspatch P$:}
318 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
321 Now by contents of $A$, $D \notin A$, so $D \notin C$.
324 \[ A \nothaspatch P \implies C \nothaspatch P \]
327 \subsection{Foreign inclusion:}
329 If $D = C$, trivial. For $D \neq C$:
330 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$. $\qed$
334 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
336 C \hasparents \{ L, R \}
338 \patchof{C} = \patchof{L}
342 (D \isin L \land D \isin R) \lor D = C : & \true \\
343 (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
344 \text{otherwise} : & D \not\isin M
348 \subsection{Conditions}
350 \[ \eqn{ Tip Merge }{
353 R \in \py : & \baseof{R} \ge \baseof{L}
354 \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
355 R \in \pn : & R \ge \baseof{L}
356 \land M = \baseof{L} \\
357 \text{otherwise} : & \false
361 \subsection{No Replay}
363 \subsubsection{For $D=C$:} $D \isin C, D \le C$. OK.
365 \subsubsection{For $D \isin L \land D \isin R$:}
366 $D \isin C$. And $D \isin L \implies D \le L \implies D \le C$. OK.
368 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
371 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
374 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
375 \land D \not\isin M$:}
376 $D \isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
379 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
381 $D \not\isin C$. Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
386 \subsection{Unique Base}
388 Need to consider only $C \in \py$, ie $L \in \py$,
389 and calculate $\pendsof{C}{\pn}$.
391 %\subsubsection{For $R \in \py$:}