chiark / gitweb /
fde6e2f5cccd274528791679a0be616000352cca
[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 \newcommand{\merge}{{\mathcal M}}
53
54 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
55 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
56 \newcommand{\mergeof}[3]{\merge ( #1 , #2, #3 ) }
57
58 \newcommand{\patchof}[1]{{\mathcal P} ( #1 ) }
59 \newcommand{\baseof}[1]{{\mathcal B} ( #1 ) }
60
61 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
62 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
63
64 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
65 \newcommand{\bigforall}{%
66   \mathop{\mathchoice%
67     {\hbox{\huge$\forall$}}%
68     {\hbox{\Large$\forall$}}%
69     {\hbox{\normalsize$\forall$}}%
70     {\hbox{\scriptsize$\forall$}}}%
71 }
72
73 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
74 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
75
76 \newcommand{\qed}{\square}
77 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
78
79 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
80 \newcommand{\gathnext}{\\ \tag*{}}
81
82 \newcommand{\true}{t}
83 \newcommand{\false}{f}
84
85 \begin{document}
86
87 \section{Notation}
88
89 \begin{basedescript}{
90 \desclabelwidth{5em}
91 \desclabelstyle{\nextlinelabel}
92 }
93 \item[ $ C \hasparents \set X $ ]
94 The parents of commit $C$ are exactly the set
95 $\set X$.
96
97 \item[ $ C \ge D $ ]
98 $C$ is a descendant of $D$ in the git commit
99 graph.  This is a partial order, namely the transitive closure of 
100 $ D \in \set X $ where $ C \hasparents \set X $.
101
102 \item[ $ C \has D $ ]
103 Informally, the tree at commit $C$ contains the change
104 made in commit $D$.  Does not take account of deliberate reversions by
105 the user or reversion, rebasing or rewinding in
106 non-Topbloke-controlled branches.  For merges and Topbloke-generated
107 anticommits or re-commits, the ``change made'' is only to be thought
108 of as any conflict resolution.  This is not a partial order because it
109 is not transitive.
110
111 \item[ $ \p, \py, \pn $ ]
112 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
113 are respectively the base and tip git branches.  $\p$ may be used
114 where the context requires a set, in which case the statement
115 is to be taken as applying to both $\py$ and $\pn$.
116 All these sets are distinct.  Hence:
117
118 \item[ $ \patchof{ C } $ ]
119 Either $\p$ s.t. $ C \in \p $, or $\bot$.  
120 A function from commits to patches' sets $\p$.
121
122 \item[ $ \pancsof{C}{\set P} $ ]
123 $ \{ A \; | \; A \le C \land A \in \set P \} $ 
124 i.e. all the ancestors of $C$
125 which are in $\set P$.
126
127 \item[ $ \pendsof{C}{\set P} $ ]
128 $ \{ E \; | \; E \in \pancsof{C}{\set P}
129   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
130   E \neq A \land E \le A \} $ 
131 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
132
133 \item[ $ \baseof{C} $ ]
134 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
135 A partial function from commits to commits.
136 See Unique Base, below.
137
138 \item[ $ C \haspatch \p $ ]
139 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
140 ~ Informally, $C$ has the contents of $\p$.
141
142 \item[ $ C \nothaspatch \p $ ]
143 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
144 ~ Informally, $C$ has none of the contents of $\p$.  
145
146 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
147 patch is applied to a non-Topbloke branch and then bubbles back to
148 the Topbloke patch itself, we hope that git's merge algorithm will
149 DTRT or that the user will no longer care about the Topbloke patch.
150
151 \item[ $ \mergeof{L}{M}{R} $ ]
152 $\displaystyle \left\{ C \middle|
153   \begin{cases}
154     (D \isin L \land D \isin R) \lor D = C : & \true \\
155     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
156     \text{otherwise} : & D \not\isin M
157   \end{cases}
158  \right\} $
159
160 \end{basedescript}
161 \newpage
162 \section{Invariants}
163
164 We maintain these each time we construct a new commit. \\
165 \[ \eqn{No Replay:}{
166   C \has D \implies C \ge D
167 }\]
168 \[\eqn{Unique Base:}{
169  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
170 }\]
171 \[\eqn{Tip Contents:}{
172   \bigforall_{C \in \py} D \isin C \equiv
173     { D \isin \baseof{C} \lor \atop
174       (D \in \py \land D \le C) }
175 }\]
176 \[\eqn{Base Acyclic:}{
177   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
178 }\]
179 \[\eqn{Coherence:}{
180   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
181 }\]
182 \[\eqn{Foreign Inclusion:}{
183   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
184 }\]
185
186 \section{Some lemmas}
187
188 \[ \eqn{Exclusive Tip Contents:}{
189   \bigforall_{C \in \py} 
190     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
191       \Bigr]
192 }\]
193 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
194
195 \proof{
196 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
197 So by Base Acyclic $D \isin B \implies D \notin \py$.
198 }
199 \[ \corrolary{
200   \bigforall_{C \in \py} D \isin C \equiv
201   \begin{cases}
202     D \in \py : & D \le C \\
203     D \not\in \py : & D \isin \baseof{C}
204   \end{cases}
205 }\]
206
207 \[ \eqn{Tip Self Inpatch:}{
208   \bigforall_{C \in \py} C \haspatch \p
209 }\]
210 Ie, tip commits contain their own patch.
211
212 \proof{
213 Apply Exclusive Tip Contents to some $D \in \py$:
214 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
215   D \isin C \equiv D \le C $
216 }
217
218 \[ \eqn{Exact Ancestors:}{
219   \bigforall_{ C \hasparents \set{R} }
220   D \le C \equiv
221     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
222     \lor D = C
223 }\]
224
225 \[ \eqn{Transitive Ancestors:}{
226   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
227   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
228 }\]
229
230 \proof{
231 The implication from right to left is trivial because
232 $ \pends() \subset \pancs() $.
233 For the implication from left to right: 
234 by the definition of $\mathcal E$,
235 for every such $A$, either $A \in \pends()$ which implies
236 $A \le M$ by the LHS directly,
237 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
238 in which case we repeat for $A'$.  Since there are finitely many
239 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
240 by the LHS.  And $A \le A''$.
241 }
242 \[ \eqn{Calculation Of Ends:}{
243   \bigforall_{C \hasparents \set A}
244     \pendsof{C}{\set P} =
245        \Bigl\{ E \Big|
246            \Bigl[ \Largeexists_{A \in \set A} 
247                        E \in \pendsof{A}{\set P} \Bigr] \land
248            \Bigl[ \Largenexists_{B \in \set A} 
249                        E \neq B \land E \le B \Bigr]
250        \Bigr\}
251 }\]
252 XXX proof TBD.
253
254 \section{Commit annotation}
255
256 We annotate each Topbloke commit $C$ with:
257 \gathbegin
258  \patchof{C}
259 \gathnext
260  \baseof{C}, \text{ if } C \in \py
261 \gathnext
262  \bigforall_{\pa{Q}} 
263    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
264 \gathnext
265  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
266 \end{gather}
267
268 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
269 make it wrong to make plain commits with git because the recorded $\pends$
270 would have to be updated.  The annotation is not needed because
271 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
272
273 \section{Simple commit}
274
275 A simple single-parent forward commit $C$ as made by git-commit.
276 \begin{gather}
277 \tag*{} C \hasparents \{ A \} \\
278 \tag*{} \patchof{C} = \patchof{A} \\
279 \tag*{} D \isin C \equiv D \isin A \lor D = C
280 \end{gather}
281
282 \subsection{No Replay}
283 Trivial.
284
285 \subsection{Unique Base}
286 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
287
288 \subsection{Tip Contents}
289 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
290 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
291 Substitute into the contents of $C$:
292 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
293     \lor D = C \]
294 Since $D = C \implies D \in \py$, 
295 and substituting in $\baseof{C}$, this gives:
296 \[ D \isin C \equiv D \isin \baseof{C} \lor
297     (D \in \py \land D \le A) \lor
298     (D = C \land D \in \py) \]
299 \[ \equiv D \isin \baseof{C} \lor
300    [ D \in \py \land ( D \le A \lor D = C ) ] \]
301 So by Exact Ancestors:
302 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
303 ) \]
304 $\qed$
305
306 \subsection{Base Acyclic}
307
308 Need to consider only $A, C \in \pn$.  
309
310 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
311
312 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
313 $A$, $D \isin C \implies D \not\in \py$. $\qed$
314
315 \subsection{Coherence and patch inclusion}
316
317 Need to consider $D \in \py$
318
319 \subsubsection{For $A \haspatch P, D = C$:}
320
321 Ancestors of $C$:
322 $ D \le C $.
323
324 Contents of $C$:
325 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
326
327 \subsubsection{For $A \haspatch P, D \neq C$:}
328 Ancestors: $ D \le C \equiv D \le A $.
329
330 Contents: $ D \isin C \equiv D \isin A \lor f $
331 so $ D \isin C \equiv D \isin A $.
332
333 So:
334 \[ A \haspatch P \implies C \haspatch P \]
335
336 \subsubsection{For $A \nothaspatch P$:}
337
338 Firstly, $C \not\in \py$ since if it were, $A \in \py$.  
339 Thus $D \neq C$.
340
341 Now by contents of $A$, $D \notin A$, so $D \notin C$.
342
343 So:
344 \[ A \nothaspatch P \implies C \nothaspatch P \]
345 $\qed$
346
347 \subsection{Foreign inclusion:}
348
349 If $D = C$, trivial.  For $D \neq C$:
350 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
351
352 \section{Anticommit}
353
354 Given $L, R^+, R^-$ where
355 $\patchof{R^+} = \pry, \patchof{R^-} = \prn$.  
356 Construct $C$ which has $\pr$ removed.
357 Used for removing a branch dependency.
358 \gathbegin
359  C \hasparents \{ L \}
360 \gathnext
361  \patchof{C} = \patchof{L}
362 \gathnext
363  D \isin C \equiv
364    \begin{cases}
365       R \in \py : & \baseof{R} \ge \baseof{L}
366               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
367       R \in \pn : & R \ge \baseof{L}
368               \land M = \baseof{L} \\
369       \text{otherwise} : & \false
370    \end{cases}
371 \end{gather}
372
373 xxx want to prove $D \isin C \equiv D \not\in pry \land D \isin L$.
374
375 \section{Merge}
376
377 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
378 \gathbegin
379  C \hasparents \{ L, R \}
380 \gathnext
381  \patchof{C} = \patchof{L}
382 \gathnext
383  D \isin C \equiv
384   \begin{cases}
385     (D \isin L \land D \isin R) \lor D = C : & \true \\
386     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
387     \text{otherwise} : & D \not\isin M
388   \end{cases}
389 \end{gather}
390
391 \subsection{Conditions}
392
393 \[ \eqn{ Tip Merge }{
394  L \in \py \implies
395    \begin{cases}
396       R \in \py : & \baseof{R} \ge \baseof{L}
397               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
398       R \in \pn : & R \ge \baseof{L}
399               \land M = \baseof{L} \\
400       \text{otherwise} : & \false
401    \end{cases}
402 }\]
403
404 \subsection{No Replay}
405
406 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
407
408 \subsubsection{For $D \isin L \land D \isin R$:}
409 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
410
411 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
412 $D \not\isin C$.  OK.
413
414 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
415 $D \not\isin C$.  OK.
416
417 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
418  \land D \not\isin M$:}
419 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
420 R$ so $D \le C$.  OK.
421
422 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
423  \land D \isin M$:}
424 $D \not\isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
425 R$ so $D \le C$.  OK.
426
427 $\qed$
428
429 \subsection{Unique Base}
430
431 Need to consider only $C \in \py$, ie $L \in \py$,
432 and calculate $\pendsof{C}{\pn}$.  So we will consider some
433 putative ancestor $A \in \pn$ and see whether $A \le C$.
434
435 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
436 But $C \in py$ and $A \in \pn$ so $A \neq C$.  
437 Thus $A \le C \equiv A \le L \lor A \le R$.
438
439 By Unique Base of L and Transitive Ancestors,
440 $A \le L \equiv A \le \baseof{L}$.
441
442 \subsubsection{For $R \in \py$:}
443
444 By Unique Base of $R$ and Transitive Ancestors,
445 $A \le R \equiv A \le \baseof{R}$.
446
447 But by Tip Merge condition on $\baseof{R}$,
448 $A \le \baseof{L} \implies A \le \baseof{R}$, so
449 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
450 Thus $A \le C \equiv A \le \baseof{R}$.  
451 That is, $\baseof{C} = \baseof{R}$.
452
453 \subsubsection{For $R \in \pn$:}
454
455 By Tip Merge condition on $R$,
456 $A \le \baseof{L} \implies A \le R$, so
457 $A \le R \lor A \le \baseof{L} \equiv A \le R$.  
458 Thus $A \le C \equiv A \le R$.  
459 That is, $\baseof{C} = R$.
460
461 $\qed$
462
463 \end{document}