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