chiark / gitweb /
be6d4759945ccdbfacbe46ab9527357abb874df4
[topbloke-formulae.git] / article.tex
1 \documentclass[a4paper,leqno]{strayman}
2 \errorcontextlines=50
3 \let\numberwithin=\notdef
4 \usepackage{amsmath}
5 \usepackage{mathabx}
6 \usepackage{txfonts}
7 \usepackage{amsfonts}
8 \usepackage{mdwlist}
9 %\usepackage{accents}
10
11 \renewcommand{\ge}{\geqslant}
12 \renewcommand{\le}{\leqslant}
13
14 \newcommand{\has}{\sqsupseteq}
15 \newcommand{\isin}{\sqsubseteq}
16
17 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
18 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
19 \newcommand{\haspatch}{\sqSupset}
20 \newcommand{\patchisin}{\sqSubset}
21
22         \newif\ifhidehack\hidehackfalse
23         \DeclareRobustCommand\hidefromedef[2]{%
24           \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
25         \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
26
27 \newcommand{\set}[1]{\mathbb{#1}}
28 \newcommand{\pay}[1]{\pa{#1}^+}
29 \newcommand{\pan}[1]{\pa{#1}^-}
30
31 \newcommand{\p}{\pa{P}}
32 \newcommand{\py}{\pay{P}}
33 \newcommand{\pn}{\pan{P}}
34
35 \newcommand{\pr}{\pa{R}}
36 \newcommand{\pry}{\pay{R}}
37 \newcommand{\prn}{\pan{R}}
38
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}}
44
45 \renewcommand{\implies}{\Rightarrow}
46 \renewcommand{\equiv}{\Leftrightarrow}
47 \renewcommand{\land}{\wedge}
48 \renewcommand{\lor}{\vee}
49
50 \newcommand{\pancs}{{\mathcal A}}
51 \newcommand{\pends}{{\mathcal E}}
52
53 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
54 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
55
56 \newcommand{\merge}[4]{{\mathcal M}(#1,#2,#3,#4)}
57 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
58
59 \newcommand{\patch}{{\mathcal P}}
60 \newcommand{\base}{{\mathcal B}}
61
62 \newcommand{\patchof}[1]{\patch ( #1 ) }
63 \newcommand{\baseof}[1]{\base ( #1 ) }
64
65 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
66 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
67
68 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
69 \newcommand{\bigforall}{%
70   \mathop{\mathchoice%
71     {\hbox{\huge$\forall$}}%
72     {\hbox{\Large$\forall$}}%
73     {\hbox{\normalsize$\forall$}}%
74     {\hbox{\scriptsize$\forall$}}}%
75 }
76
77 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
78 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
79
80 \newcommand{\qed}{\square}
81 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
82
83 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
84 \newcommand{\gathnext}{\\ \tag*{}}
85
86 \newcommand{\true}{t}
87 \newcommand{\false}{f}
88
89 \begin{document}
90
91 \section{Notation}
92
93 \begin{basedescript}{
94 \desclabelwidth{5em}
95 \desclabelstyle{\nextlinelabel}
96 }
97 \item[ $ C \hasparents \set X $ ]
98 The parents of commit $C$ are exactly the set
99 $\set X$.
100
101 \item[ $ C \ge D $ ]
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 $.
105
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
113 is not transitive.
114
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:
121
122 \item[ $ \patchof{ C } $ ]
123 Either $\p$ s.t. $ C \in \p $, or $\bot$.  
124 A function from commits to patches' sets $\p$.
125
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$.
130
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}$.
136
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.
141
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$.
145
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$.  
149
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.
154
155 \item[ $\displaystyle \merge{C}{L}{M}{R} $ ]
156 The contents of a git merge result:
157
158 $\displaystyle D \isin C \equiv
159   \begin{cases}
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
163   \end{cases}
164
165
166 \end{basedescript}
167 \newpage
168 \section{Invariants}
169
170 We maintain these each time we construct a new commit. \\
171 \[ \eqn{No Replay:}{
172   C \has D \implies C \ge D
173 }\]
174 \[\eqn{Unique Base:}{
175  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
176 }\]
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) }
181 }\]
182 \[\eqn{Base Acyclic:}{
183   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
184 }\]
185 \[\eqn{Coherence:}{
186   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
187 }\]
188 \[\eqn{Foreign Inclusion:}{
189   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
190 }\]
191
192 \section{Some lemmas}
193
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 )
197       \Bigr]
198 }\]
199 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
200
201 \proof{
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$.
204 }
205 \[ \corrolary{
206   \bigforall_{C \in \py} D \isin C \equiv
207   \begin{cases}
208     D \in \py : & D \le C \\
209     D \not\in \py : & D \isin \baseof{C}
210   \end{cases}
211 }\]
212
213 \[ \eqn{Tip Self Inpatch:}{
214   \bigforall_{C \in \py} C \haspatch \p
215 }\]
216 Ie, tip commits contain their own patch.
217
218 \proof{
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 $
222 }
223
224 \[ \eqn{Exact Ancestors:}{
225   \bigforall_{ C \hasparents \set{R} }
226   D \le C \equiv
227     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
228     \lor D = C
229 }\]
230
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]
234 }\]
235
236 \proof{
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''$.
247 }
248 \[ \eqn{Calculation Of Ends:}{
249   \bigforall_{C \hasparents \set A}
250     \pendsof{C}{\set P} =
251        \Bigl\{ E \Big|
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]
256        \Bigr\}
257 }\]
258 XXX proof TBD.
259
260 \subsection{No Replay for Merge Results}
261
262 If we are constructing $C$, given
263 \gathbegin
264   \merge{C}{L}{M}{R}
265 \gathnext
266   L \le C
267 \gathnext
268   R \le C
269 \end{gather}
270 No Replay is preserved.  {\it Proof:}
271
272 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
273
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.
276
277 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
278 $D \not\isin C$.  OK.
279
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
283 R$ so $D \le C$.  OK.
284
285 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
286  \land D \isin M$:}
287 $D \not\isin C$.  OK.
288
289 $\qed$
290
291 \section{Commit annotation}
292
293 We annotate each Topbloke commit $C$ with:
294 \gathbegin
295  \patchof{C}
296 \gathnext
297  \baseof{C}, \text{ if } C \in \py
298 \gathnext
299  \bigforall_{\pa{Q}} 
300    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
301 \gathnext
302  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
303 \end{gather}
304
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\}$.
309
310 \section{Simple commit}
311
312 A simple single-parent forward commit $C$ as made by git-commit.
313 \begin{gather}
314 \tag*{} C \hasparents \{ A \} \\
315 \tag*{} \patchof{C} = \patchof{A} \\
316 \tag*{} D \isin C \equiv D \isin A \lor D = C
317 \end{gather}
318
319 \subsection{No Replay}
320 Trivial.
321
322 \subsection{Unique Base}
323 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
324
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 )
330     \lor D = C \]
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
340 ) \]
341 $\qed$
342
343 \subsection{Base Acyclic}
344
345 Need to consider only $A, C \in \pn$.  
346
347 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
348
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$
351
352 \subsection{Coherence and patch inclusion}
353
354 Need to consider $D \in \py$
355
356 \subsubsection{For $A \haspatch P, D = C$:}
357
358 Ancestors of $C$:
359 $ D \le C $.
360
361 Contents of $C$:
362 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
363
364 \subsubsection{For $A \haspatch P, D \neq C$:}
365 Ancestors: $ D \le C \equiv D \le A $.
366
367 Contents: $ D \isin C \equiv D \isin A \lor f $
368 so $ D \isin C \equiv D \isin A $.
369
370 So:
371 \[ A \haspatch P \implies C \haspatch P \]
372
373 \subsubsection{For $A \nothaspatch P$:}
374
375 Firstly, $C \not\in \py$ since if it were, $A \in \py$.  
376 Thus $D \neq C$.
377
378 Now by contents of $A$, $D \notin A$, so $D \notin C$.
379
380 So:
381 \[ A \nothaspatch P \implies C \nothaspatch P \]
382 $\qed$
383
384 \subsection{Foreign inclusion:}
385
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$
388
389 \section{Anticommit}
390
391 Given $L, R^+, R^-$ where
392 $R^+ \in \pry, R^- = \baseof{R^+}$.  
393 Construct $C$ which has $\pr$ removed.
394 Used for removing a branch dependency.
395 \gathbegin
396  C \hasparents \{ L \}
397 \gathnext
398  \patchof{C} = \patchof{L}
399 \gathnext
400  \merge{C}{L}{R^+}{R^-}
401 \end{gather}
402
403 \subsection{Conditions}
404
405 \[ \eqn{ Unique Tip }{
406  \pendsof{L}{\pry} = \{ R^+ \}
407 }\]
408 \[ \eqn{ Currently Included }{
409  L \haspatch \pry
410 }\]
411
412 \subsection{Desired Contents}
413
414 xxx need to prove $D \isin C \equiv D \not\in \pry \land D \isin L$.
415
416 \subsection{No Replay}
417
418 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
419 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$ and No Replay for
420 Merge Results applies. $\qed$
421
422 \subsection{Unique Base}
423
424 Need to consider only $C \in \py$, ie $L \in \py$.
425
426 xxx tbd
427
428 \section{Merge}
429
430 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
431 \gathbegin
432  C \hasparents \{ L, R \}
433 \gathnext
434  \patchof{C} = \patchof{L}
435 \gathnext
436  \merge{C}{L}{M}{R}
437 \end{gather}
438
439 \subsection{Conditions}
440
441 \[ \eqn{ Tip Merge }{
442  L \in \py \implies
443    \begin{cases}
444       R \in \py : & \baseof{R} \ge \baseof{L}
445               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
446       R \in \pn : & R \ge \baseof{L}
447               \land M = \baseof{L} \\
448       \text{otherwise} : & \false
449    \end{cases}
450 }\]
451
452 \subsection{Merge Results}
453
454 As above.
455
456 \subsection{Unique Base}
457
458 Need to consider only $C \in \py$, ie $L \in \py$,
459 and calculate $\pendsof{C}{\pn}$.  So we will consider some
460 putative ancestor $A \in \pn$ and see whether $A \le C$.
461
462 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
463 But $C \in py$ and $A \in \pn$ so $A \neq C$.  
464 Thus $A \le C \equiv A \le L \lor A \le R$.
465
466 By Unique Base of L and Transitive Ancestors,
467 $A \le L \equiv A \le \baseof{L}$.
468
469 \subsubsection{For $R \in \py$:}
470
471 By Unique Base of $R$ and Transitive Ancestors,
472 $A \le R \equiv A \le \baseof{R}$.
473
474 But by Tip Merge condition on $\baseof{R}$,
475 $A \le \baseof{L} \implies A \le \baseof{R}$, so
476 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
477 Thus $A \le C \equiv A \le \baseof{R}$.  
478 That is, $\baseof{C} = \baseof{R}$.
479
480 \subsubsection{For $R \in \pn$:}
481
482 By Tip Merge condition on $R$,
483 $A \le \baseof{L} \implies A \le R$, so
484 $A \le R \lor A \le \baseof{L} \equiv A \le R$.  
485 Thus $A \le C \equiv A \le R$.  
486 That is, $\baseof{C} = R$.
487
488 $\qed$
489
490 \end{document}