chiark / gitweb /
create tip
[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 \newcommand{\nge}{\ngeqslant}
14 \newcommand{\nle}{\nleqslant}
15
16 \newcommand{\has}{\sqsupseteq}
17 \newcommand{\isin}{\sqsubseteq}
18
19 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
20 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
21 \newcommand{\haspatch}{\sqSupset}
22 \newcommand{\patchisin}{\sqSubset}
23
24         \newif\ifhidehack\hidehackfalse
25         \DeclareRobustCommand\hidefromedef[2]{%
26           \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
27         \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
28
29 \newcommand{\set}[1]{\mathbb{#1}}
30 \newcommand{\pay}[1]{\pa{#1}^+}
31 \newcommand{\pan}[1]{\pa{#1}^-}
32
33 \newcommand{\p}{\pa{P}}
34 \newcommand{\py}{\pay{P}}
35 \newcommand{\pn}{\pan{P}}
36
37 \newcommand{\pq}{\pa{Q}}
38 \newcommand{\pqy}{\pay{Q}}
39 \newcommand{\pqn}{\pan{Q}}
40
41 \newcommand{\pr}{\pa{R}}
42 \newcommand{\pry}{\pay{R}}
43 \newcommand{\prn}{\pan{R}}
44
45 %\newcommand{\hasparents}{\underaccent{1}{>}}
46 %\newcommand{\hasparents}{{%
47 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
48 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
49 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
50
51 \renewcommand{\implies}{\Rightarrow}
52 \renewcommand{\equiv}{\Leftrightarrow}
53 \renewcommand{\nequiv}{\nLeftrightarrow}
54 \renewcommand{\land}{\wedge}
55 \renewcommand{\lor}{\vee}
56
57 \newcommand{\pancs}{{\mathcal A}}
58 \newcommand{\pends}{{\mathcal E}}
59
60 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
61 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
62
63 \newcommand{\merge}{{\mathcal M}}
64 \newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
65 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
66
67 \newcommand{\patch}{{\mathcal P}}
68 \newcommand{\base}{{\mathcal B}}
69
70 \newcommand{\patchof}[1]{\patch ( #1 ) }
71 \newcommand{\baseof}[1]{\base ( #1 ) }
72
73 \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
74 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
75
76 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
77 \newcommand{\bigforall}{%
78   \mathop{\mathchoice%
79     {\hbox{\huge$\forall$}}%
80     {\hbox{\Large$\forall$}}%
81     {\hbox{\normalsize$\forall$}}%
82     {\hbox{\scriptsize$\forall$}}}%
83 }
84
85 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
86 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
87
88 \newcommand{\qed}{\square}
89 \newcommand{\proofstarts}{{\it Proof:}}
90 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
91
92 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
93 \newcommand{\gathnext}{\\ \tag*{}}
94
95 \newcommand{\true}{t}
96 \newcommand{\false}{f}
97
98 \begin{document}
99
100 \section{Notation}
101
102 \begin{basedescript}{
103 \desclabelwidth{5em}
104 \desclabelstyle{\nextlinelabel}
105 }
106 \item[ $ C \hasparents \set X $ ]
107 The parents of commit $C$ are exactly the set
108 $\set X$.
109
110 \item[ $ C \ge D $ ]
111 $C$ is a descendant of $D$ in the git commit
112 graph.  This is a partial order, namely the transitive closure of 
113 $ D \in \set X $ where $ C \hasparents \set X $.
114
115 \item[ $ C \has D $ ]
116 Informally, the tree at commit $C$ contains the change
117 made in commit $D$.  Does not take account of deliberate reversions by
118 the user or reversion, rebasing or rewinding in
119 non-Topbloke-controlled branches.  For merges and Topbloke-generated
120 anticommits or re-commits, the ``change made'' is only to be thought
121 of as any conflict resolution.  This is not a partial order because it
122 is not transitive.
123
124 \item[ $ \p, \py, \pn $ ]
125 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
126 are respectively the base and tip git branches.  $\p$ may be used
127 where the context requires a set, in which case the statement
128 is to be taken as applying to both $\py$ and $\pn$.
129 None of these sets overlap.  Hence:
130
131 \item[ $ \patchof{ C } $ ]
132 Either $\p$ s.t. $ C \in \p $, or $\bot$.  
133 A function from commits to patches' sets $\p$.
134
135 \item[ $ \pancsof{C}{\set P} $ ]
136 $ \{ A \; | \; A \le C \land A \in \set P \} $ 
137 i.e. all the ancestors of $C$
138 which are in $\set P$.
139
140 \item[ $ \pendsof{C}{\set P} $ ]
141 $ \{ E \; | \; E \in \pancsof{C}{\set P}
142   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
143   E \neq A \land E \le A \} $ 
144 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
145
146 \item[ $ \baseof{C} $ ]
147 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
148 A partial function from commits to commits.
149 See Unique Base, below.
150
151 \item[ $ C \haspatch \p $ ]
152 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
153 ~ Informally, $C$ has the contents of $\p$.
154
155 \item[ $ C \nothaspatch \p $ ]
156 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
157 ~ Informally, $C$ has none of the contents of $\p$.  
158
159 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$.  This
160 includes commits on plain git branches made by applying a Topbloke
161 patch.  If a Topbloke
162 patch is applied to a non-Topbloke branch and then bubbles back to
163 the relevant Topbloke branches, we hope that 
164 if the user still cares about the Topbloke patch,
165 git's merge algorithm will DTRT when trying to re-apply the changes.
166
167 \item[ $\displaystyle \mergeof{C}{L}{M}{R} $ ]
168 The contents of a git merge result:
169
170 $\displaystyle D \isin C \equiv
171   \begin{cases}
172     (D \isin L \land D \isin R) \lor D = C : & \true \\
173     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
174     \text{otherwise} : & D \not\isin M
175   \end{cases}
176
177
178 \end{basedescript}
179 \newpage
180 \section{Invariants}
181
182 We maintain these each time we construct a new commit. \\
183 \[ \eqn{No Replay:}{
184   C \has D \implies C \ge D
185 }\]
186 \[\eqn{Unique Base:}{
187  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
188 }\]
189 \[\eqn{Tip Contents:}{
190   \bigforall_{C \in \py} D \isin C \equiv
191     { D \isin \baseof{C} \lor \atop
192       (D \in \py \land D \le C) }
193 }\]
194 \[\eqn{Base Acyclic:}{
195   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
196 }\]
197 \[\eqn{Coherence:}{
198   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
199 }\]
200 \[\eqn{Foreign Inclusion:}{
201   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
202 }\]
203 \[\eqn{Foreign Contents:}{
204   \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
205     D \le C \implies \patchof{D} = \bot
206 }\]
207
208 \section{Some lemmas}
209
210 \[ \eqn{Alternative (overlapping) formulations defining
211   $\mergeof{C}{L}{M}{R}$:}{
212  D \isin C \equiv
213   \begin{cases}
214     D \isin L  \equiv D \isin R  : & D = C \lor D \isin L     \\
215     D \isin L \nequiv D \isin R  : & D = C \lor D \not\isin M \\
216     D \isin L  \equiv D \isin M  : & D = C \lor D \isin R     \\
217     D \isin L \nequiv D \isin M  : & D = C \lor D \isin L     \\
218     \text{as above with L and R exchanged}
219   \end{cases}
220 }\]
221 \proof{
222   Truth table xxx
223
224   Original definition is symmetrical in $L$ and $R$.
225 }
226
227 \[ \eqn{Exclusive Tip Contents:}{
228   \bigforall_{C \in \py} 
229     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
230       \Bigr]
231 }\]
232 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
233
234 \proof{
235 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
236 So by Base Acyclic $D \isin B \implies D \notin \py$.
237 }
238 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
239   \bigforall_{C \in \py} D \isin C \equiv
240   \begin{cases}
241     D \in \py : & D \le C \\
242     D \not\in \py : & D \isin \baseof{C}
243   \end{cases}
244 }\]
245
246 \[ \eqn{Tip Self Inpatch:}{
247   \bigforall_{C \in \py} C \haspatch \p
248 }\]
249 Ie, tip commits contain their own patch.
250
251 \proof{
252 Apply Exclusive Tip Contents to some $D \in \py$:
253 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
254   D \isin C \equiv D \le C $
255 }
256
257 \[ \eqn{Exact Ancestors:}{
258   \bigforall_{ C \hasparents \set{R} }
259   D \le C \equiv
260     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
261     \lor D = C
262 }\]
263 xxx proof tbd
264
265 \[ \eqn{Transitive Ancestors:}{
266   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
267   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
268 }\]
269
270 \proof{
271 The implication from right to left is trivial because
272 $ \pends() \subset \pancs() $.
273 For the implication from left to right: 
274 by the definition of $\mathcal E$,
275 for every such $A$, either $A \in \pends()$ which implies
276 $A \le M$ by the LHS directly,
277 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
278 in which case we repeat for $A'$.  Since there are finitely many
279 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
280 by the LHS.  And $A \le A''$.
281 }
282
283 \[ \eqn{Calculation Of Ends:}{
284   \bigforall_{C \hasparents \set A}
285     \pendsof{C}{\set P} =
286       \begin{cases}
287        C \in \p : & \{ C \}
288       \\
289        C \not\in \p : & \displaystyle
290        \left\{ E \Big|
291            \Bigl[ \Largeexists_{A \in \set A} 
292                        E \in \pendsof{A}{\set P} \Bigr] \land
293            \Bigl[ \Largenexists_{B \in \set A} 
294                        E \neq B \land E \le B \Bigr]
295        \right\}
296       \end{cases}
297 }\]
298 xxx proof tbd
299
300 \[ \eqn{Ingredients Prevent Replay:}{
301   \left[
302     {C \hasparents \set A} \land
303    \\
304     \left(
305       D \isin C \implies
306        D = C \lor
307        \Largeexists_{A \in \set A} D \isin A
308     \right)
309   \right] \implies \left[
310     D \isin C \implies D \le C
311   \right]
312 }\]
313 \proof{
314   Trivial for $D = C$.  Consider some $D \neq C$, $D \isin C$.
315   By the preconditions, there is some $A$ s.t. $D \in \set A$
316   and $D \isin A$.  By No Replay for $A$, $D \le A$.  And
317   $A \le C$ so $D \le C$.
318 }
319
320 \[ \eqn{Simple Foreign Inclusion:}{
321   \left[
322     C \hasparents \{ L \}
323    \land
324     \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
325   \right]
326  \implies
327    \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
328      D \isin C \equiv D \le C
329 }\]
330 \proof{
331 Consider some $D$ s.t. $\patchof{D} = \bot$.
332 If $D = C$, trivially true.  For $D \neq C$,
333 by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
334 And by Exact Ancestors $D \le L \equiv D \le C$.
335 So $D \isin C \equiv D \le C$.
336 }
337
338 \[ \eqn{Totally Foreign Contents:}{
339   \bigforall_{C \hasparents \set A}
340    \left[
341     \patchof{C} = \bot \land
342       \bigforall_{A \in \set A} \patchof{A} = \bot
343    \right]
344   \implies
345    \left[
346     D \le C
347    \implies
348     \patchof{D} = \bot
349    \right]
350 }\]
351 \proof{
352 Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
353 If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
354 Contents of $A$, $\patchof{D} = \bot$.
355 }
356
357 \section{Commit annotation}
358
359 We annotate each Topbloke commit $C$ with:
360 \gathbegin
361  \patchof{C}
362 \gathnext
363  \baseof{C}, \text{ if } C \in \py
364 \gathnext
365  \bigforall_{\pq}
366    \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
367 \gathnext
368  \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
369 \end{gather}
370
371 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
372 in the summary in the section for that kind of commit.
373
374 Whether $\baseof{C}$ is required, and if so what the value is, is
375 stated in the proof of Unique Base for each kind of commit.
376
377 $C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
378 set $\{ \pq | C \haspatch \pq \}$.  Whether $C \haspatch \pq$
379 is in stated
380 (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
381 for the ingredients $I$),
382 in the proof of Coherence for each kind of commit.
383
384 $\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
385 using the lemma Calculation of Ends, above.
386 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
387 make it wrong to make plain commits with git because the recorded $\pends$
388 would have to be updated.  The annotation is not needed in that case
389 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
390
391 \section{Simple commit}
392
393 A simple single-parent forward commit $C$ as made by git-commit.
394 \begin{gather}
395 \tag*{} C \hasparents \{ A \} \\
396 \tag*{} \patchof{C} = \patchof{A} \\
397 \tag*{} D \isin C \equiv D \isin A \lor D = C
398 \end{gather}
399 This also covers Topbloke-generated commits on plain git branches:
400 Topbloke strips the metadata when exporting.
401
402 \subsection{No Replay}
403
404 Ingredients Prevent Replay applies.  $\qed$
405
406 \subsection{Unique Base}
407 If $A, C \in \py$ then by Calculation of Ends for
408 $C, \py, C \not\in \py$:
409 $\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
410 $\baseof{C} = \baseof{A}$. $\qed$
411
412 \subsection{Tip Contents}
413 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
414 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
415 Substitute into the contents of $C$:
416 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
417     \lor D = C \]
418 Since $D = C \implies D \in \py$, 
419 and substituting in $\baseof{C}$, this gives:
420 \[ D \isin C \equiv D \isin \baseof{C} \lor
421     (D \in \py \land D \le A) \lor
422     (D = C \land D \in \py) \]
423 \[ \equiv D \isin \baseof{C} \lor
424    [ D \in \py \land ( D \le A \lor D = C ) ] \]
425 So by Exact Ancestors:
426 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
427 ) \]
428 $\qed$
429
430 \subsection{Base Acyclic}
431
432 Need to consider only $A, C \in \pn$.  
433
434 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
435
436 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
437 $A$, $D \isin C \implies D \not\in \py$.
438
439 $\qed$
440
441 \subsection{Coherence and patch inclusion}
442
443 Need to consider $D \in \py$
444
445 \subsubsection{For $A \haspatch P, D = C$:}
446
447 Ancestors of $C$:
448 $ D \le C $.
449
450 Contents of $C$:
451 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
452
453 \subsubsection{For $A \haspatch P, D \neq C$:}
454 Ancestors: $ D \le C \equiv D \le A $.
455
456 Contents: $ D \isin C \equiv D \isin A \lor f $
457 so $ D \isin C \equiv D \isin A $.
458
459 So:
460 \[ A \haspatch P \implies C \haspatch P \]
461
462 \subsubsection{For $A \nothaspatch P$:}
463
464 Firstly, $C \not\in \py$ since if it were, $A \in \py$.  
465 Thus $D \neq C$.
466
467 Now by contents of $A$, $D \notin A$, so $D \notin C$.
468
469 So:
470 \[ A \nothaspatch P \implies C \nothaspatch P \]
471 $\qed$
472
473 \subsection{Foreign Inclusion:}
474
475 Simple Foreign Inclusion applies.  $\qed$
476
477 \subsection{Foreign Contents:}
478
479 Only relevant if $\patchof{C} = \bot$, and in that case Totally
480 Foreign Contents applies. $\qed$
481
482 \section{Create Base}
483
484 Given $L$, create a Topbloke base branch initial commit $B$.
485 \gathbegin
486  B \hasparents \{ L \}
487 \gathnext
488  \patchof{B} = \pqn
489 \gathnext
490  D \isin B \equiv D \isin L \lor D = B
491 \end{gather}
492
493 \subsection{Conditions}
494
495 \[ \eqn{ Ingredients }{
496  \patchof{L} = \pa{L} \lor \patchof{L} = \bot
497 }\]
498 \[ \eqn{ Create Acyclic }{
499  L \not\haspatch \pq
500 }\]
501
502 \subsection{No Replay}
503
504 Ingredients Prevent Replay applies.  $\qed$
505
506 \subsection{Unique Base}
507
508 Not applicable.
509
510 \subsection{Tip Contents}
511
512 Not applicable.
513
514 \subsection{Base Acyclic}
515
516 Consider some $D \isin B$.  If $D = B$, $D \in \pqn$.
517 If $D \neq B$, $D \isin L$, and by Create Acyclic
518 $D \not\in \pqy$.  $\qed$
519
520 \subsection{Coherence and Patch Inclusion}
521
522 Consider some $D \in \p$.
523 $B \not\in \py$ so $D \neq B$.  So $D \isin B \equiv D \isin L$
524 and $D \le B \equiv D \le L$.
525
526 Thus $L \haspatch \p \implies B \haspatch P$
527 and $L \nothaspatch \p \implies B \nothaspatch P$.
528
529 $\qed$.
530
531 \subsection{Foreign Inclusion}
532
533 Simple Foreign Inclusion applies. $\qed$
534
535 \subsection{Foreign Contents}
536
537 Not applicable.
538
539 \section{Create Tip}
540
541 Given a Topbloke base $B$, create a tip branch initial commit B.
542 \gathbegin
543  C \hasparents \{ B \}
544 \gathnext
545  \patchof{B} = \pqy
546 \gathnext
547  D \isin C \equiv D \isin B \lor D = C
548 \end{gather}
549
550 \subsection{Conditions}
551
552 \[ \eqn{ Ingredients }{
553  \patchof{B} = \pqn
554 }\]
555 \[ \eqn{ No Sneak }{
556  \pendsof{B}{\pqy} = \{ \}
557 }\]
558
559 \subsection{No Replay}
560
561 Ingredients Prevent Replay applies.  $\qed$
562
563 \subsection{Unique Base}
564
565 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.  $\qed$
566
567 \subsection{Tip Contents}
568
569 Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.
570
571 If $D \neq C$, $D \isin C \equiv D \isin B$.
572 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
573 So $D \isin C \equiv D \isin \baseof{B}$.
574
575 $\qed$
576
577 \subsection{Base Acyclic}
578
579 Not applicable.
580
581 \subsection{Coherence and Patch Inclusion}
582
583 $$
584 \begin{cases}
585   \p = \pq    \lor B \haspatch \p : & C \haspatch \p \\
586   \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
587 \end{cases}
588 $$
589
590 \proofstarts
591 ~ Consider some $D \in \py$.
592
593 \subsubsection{For $\p = \pq$:}
594
595 By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
596 By No Sneak, $D \le B \equiv D = C$.  Thus $C \haspatch \pq$.
597
598 \subsubsection{For $\p \neq \pq$:}
599
600 $D \neq C$.  So $D \isin C \equiv D \isin B$,
601 and $D \le C \equiv D \le B$.
602
603 $\qed$
604
605 \subsection{Foreign Inclusion}
606
607 Simple Foreign Inclusion applies.  $\qed$
608
609 \subsection{Foreign Contents}
610
611 Not applicable.
612
613 \section{Anticommit}
614
615 Given $L$ and $\pr$ as represented by $R^+, R^-$.
616 Construct $C$ which has $\pr$ removed.
617 Used for removing a branch dependency.
618 \gathbegin
619  C \hasparents \{ L \}
620 \gathnext
621  \patchof{C} = \patchof{L}
622 \gathnext
623  \mergeof{C}{L}{R^+}{R^-}
624 \end{gather}
625
626 \subsection{Conditions}
627
628 \[ \eqn{ Ingredients }{
629 R^+ \in \pry \land R^- = \baseof{R^+}
630 }\]
631 \[ \eqn{ Into Base }{
632  L \in \pn
633 }\]
634 \[ \eqn{ Unique Tip }{
635  \pendsof{L}{\pry} = \{ R^+ \}
636 }\]
637 \[ \eqn{ Currently Included }{
638  L \haspatch \pry
639 }\]
640
641 \subsection{Ordering of Ingredients:}
642
643 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
644 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
645 $\qed$
646
647 (Note that $R^+ \not\le R^-$, i.e. the merge base
648 is a descendant, not an ancestor, of the 2nd parent.)
649
650 \subsection{No Replay}
651
652 By definition of $\merge$,
653 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
654 So, by Ordering of Ingredients,
655 Ingredients Prevent Replay applies.  $\qed$
656
657 \subsection{Desired Contents}
658
659 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
660 \proofstarts
661
662 \subsubsection{For $D = C$:}
663
664 Trivially $D \isin C$.  OK.
665
666 \subsubsection{For $D \neq C, D \not\le L$:}
667
668 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
669 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
670
671 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
672
673 By Currently Included, $D \isin L$.
674
675 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
676 by Unique Tip, $D \le R^+ \equiv D \le L$.  
677 So $D \isin R^+$.
678
679 By Base Acyclic, $D \not\isin R^-$.
680
681 Apply $\merge$: $D \not\isin C$.  OK.
682
683 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
684
685 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
686
687 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
688
689 $\qed$
690
691 \subsection{Unique Base}
692
693 Into Base means that $C \in \pn$, so Unique Base is not
694 applicable. $\qed$
695
696 \subsection{Tip Contents}
697
698 Again, not applicable. $\qed$
699
700 \subsection{Base Acyclic}
701
702 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
703 And by Into Base $C \not\in \py$.
704 Now from Desired Contents, above, $D \isin C
705 \implies D \isin L \lor D = C$, which thus
706 $\implies D \not\in \py$.  $\qed$.
707
708 \subsection{Coherence and Patch Inclusion}
709
710 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
711
712 \subsubsection{For $\p = \pr$:}
713 By Desired Contents, above, $D \not\isin C$.
714 So $C \nothaspatch \pr$.
715
716 \subsubsection{For $\p \neq \pr$:}
717 By Desired Contents, $D \isin C \equiv D \isin L$
718 (since $D \in \py$ so $D \not\in \pry$).
719
720 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
721 So $L \nothaspatch \p \implies C \nothaspatch \p$.
722
723 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
724 so $L \haspatch \p \implies C \haspatch \p$.
725
726 $\qed$
727
728 \subsection{Foreign Inclusion}
729
730 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
731 So by Desired Contents $D \isin C \equiv D \isin L$.
732 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
733
734 And $D \le C \equiv D \le L$.
735 Thus $D \isin C \equiv D \le C$.
736
737 $\qed$
738
739 \subsection{Foreign Contents}
740
741 Not applicable.
742
743 \section{Merge}
744
745 Merge commits $L$ and $R$ using merge base $M$:
746 \gathbegin
747  C \hasparents \{ L, R \}
748 \gathnext
749  \patchof{C} = \patchof{L}
750 \gathnext
751  \mergeof{C}{L}{M}{R}
752 \end{gather}
753 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
754
755 \subsection{Conditions}
756 \[ \eqn{ Ingredients }{
757  M \le L, M \le R
758 }\]
759 \[ \eqn{ Tip Merge }{
760  L \in \py \implies
761    \begin{cases}
762       R \in \py : & \baseof{R} \ge \baseof{L}
763               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
764       R \in \pn : & M = \baseof{L} \\
765       \text{otherwise} : & \false
766    \end{cases}
767 }\]
768 \[ \eqn{ Merge Acyclic }{
769     L \in \pn
770    \implies
771     R \nothaspatch \p
772 }\]
773 \[ \eqn{ Removal Merge Ends }{
774     X \not\haspatch \p \land
775     Y \haspatch \p \land
776     M \haspatch \p
777   \implies
778     \pendsof{Y}{\py} = \pendsof{M}{\py}
779 }\]
780 \[ \eqn{ Addition Merge Ends }{
781     X \not\haspatch \p \land
782     Y \haspatch \p \land
783     M \nothaspatch \p
784    \implies \left[
785     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
786    \right]
787 }\]
788 \[ \eqn{ Foreign Merges }{
789     \patchof{L} = \bot \equiv \patchof{R} = \bot
790 }\]
791
792 \subsection{Non-Topbloke merges}
793
794 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
795 (Foreign Merges, above).
796 I.e. not only is it forbidden to merge into a Topbloke-controlled
797 branch without Topbloke's assistance, it is also forbidden to
798 merge any Topbloke-controlled branch into any plain git branch.
799
800 Given those conditions, Tip Merge and Merge Acyclic do not apply.
801 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
802 Merge Ends condition applies.
803
804 So a plain git merge of non-Topbloke branches meets the conditions and
805 is therefore consistent with our scheme.
806
807 \subsection{No Replay}
808
809 By definition of $\merge$,
810 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
811 So, by Ingredients,
812 Ingredients Prevent Replay applies.  $\qed$
813
814 \subsection{Unique Base}
815
816 Need to consider only $C \in \py$, ie $L \in \py$,
817 and calculate $\pendsof{C}{\pn}$.  So we will consider some
818 putative ancestor $A \in \pn$ and see whether $A \le C$.
819
820 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
821 But $C \in py$ and $A \in \pn$ so $A \neq C$.  
822 Thus $A \le C \equiv A \le L \lor A \le R$.
823
824 By Unique Base of L and Transitive Ancestors,
825 $A \le L \equiv A \le \baseof{L}$.
826
827 \subsubsection{For $R \in \py$:}
828
829 By Unique Base of $R$ and Transitive Ancestors,
830 $A \le R \equiv A \le \baseof{R}$.
831
832 But by Tip Merge condition on $\baseof{R}$,
833 $A \le \baseof{L} \implies A \le \baseof{R}$, so
834 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
835 Thus $A \le C \equiv A \le \baseof{R}$.  
836 That is, $\baseof{C} = \baseof{R}$.
837
838 \subsubsection{For $R \in \pn$:}
839
840 By Tip Merge condition on $R$ and since $M \le R$,
841 $A \le \baseof{L} \implies A \le R$, so
842 $A \le R \lor A \le \baseof{L} \equiv A \le R$.  
843 Thus $A \le C \equiv A \le R$.  
844 That is, $\baseof{C} = R$.
845
846 $\qed$
847
848 \subsection{Coherence and Patch Inclusion}
849
850 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
851 This involves considering $D \in \py$.  
852
853 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
854 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
855 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
856 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
857
858 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
859 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
860 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
861
862 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
863
864 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
865  \equiv D \isin L \lor D \isin R$.  
866 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
867
868 Consider $D \neq C, D \isin X \land D \isin Y$:
869 By $\merge$, $D \isin C$.  Also $D \le X$ 
870 so $D \le C$.  OK for $C \haspatch \p$.
871
872 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
873 By $\merge$, $D \not\isin C$.  
874 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.  
875 OK for $C \haspatch \p$.
876
877 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
878 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.  
879 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
880 OK for $C \haspatch \p$.
881
882 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
883
884 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
885
886 $M \haspatch \p \implies C \nothaspatch \p$.
887 $M \nothaspatch \p \implies C \haspatch \p$.
888
889 \proofstarts
890
891 One of the Merge Ends conditions applies.  
892 Recall that we are considering $D \in \py$.
893 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
894 We will show for each of
895 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
896 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
897
898 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
899 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
900 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
901 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
902
903 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
904 $D \le Y$ so $D \le C$.  
905 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
906
907 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
908 $D \not\le Y$.  If $D \le X$ then
909 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 
910 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
911 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
912
913 Consider $D \neq C, M \haspatch P, D \isin Y$:
914 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
915 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
916 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
917
918 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
919 By $\merge$, $D \not\isin C$.  OK.
920
921 $\qed$
922
923 \subsection{Base Acyclic}
924
925 This applies when $C \in \pn$.
926 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
927
928 Consider some $D \in \py$.
929
930 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
931 R$.  And $D \neq C$.  So $D \not\isin C$.
932
933 $\qed$
934
935 \subsection{Tip Contents}
936
937 We need worry only about $C \in \py$.  
938 And $\patchof{C} = \patchof{L}$
939 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
940 of $C$, and its Coherence and Patch Inclusion, as just proved.
941
942 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
943 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
944 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
945 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
946 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
947
948 We will consider an arbitrary commit $D$
949 and prove the Exclusive Tip Contents form.
950
951 \subsubsection{For $D \in \py$:}
952 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
953 \le C$.  OK.
954
955 \subsubsection{For $D \not\in \py, R \not\in \py$:}
956
957 $D \neq C$.  By Tip Contents of $L$,
958 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
959 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
960 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
961 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
962
963 \subsubsection{For $D \not\in \py, R \in \py$:}
964
965 $D \neq C$.
966
967 By Tip Contents
968 $D \isin L \equiv D \isin \baseof{L}$ and
969 $D \isin R \equiv D \isin \baseof{R}$.
970
971 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
972 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
973 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
974 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
975
976 So $D \isin M \equiv D \isin L$ and by $\merge$,
977 $D \isin C \equiv D \isin R$.  But from Unique Base,
978 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
979
980 $\qed$
981
982 \subsection{Foreign Inclusion}
983
984 Consider some $D$ s.t. $\patchof{D} = \bot$.
985 By Foreign Inclusion of $L, M, R$:
986 $D \isin L \equiv D \le L$;
987 $D \isin M \equiv D \le M$;
988 $D \isin R \equiv D \le R$.
989
990 \subsubsection{For $D = C$:}
991
992 $D \isin C$ and $D \le C$.  OK.
993
994 \subsubsection{For $D \neq C, D \isin M$:}
995
996 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
997 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
998
999 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
1000
1001 By $\merge$, $D \isin C$.
1002 And $D \isin X$ means $D \le X$ so $D \le C$.
1003 OK.
1004
1005 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
1006
1007 By $\merge$, $D \not\isin C$.
1008 And $D \not\le L, D \not\le R$ so $D \not\le C$.
1009 OK
1010
1011 $\qed$
1012
1013 \subsection{Foreign Contents}
1014
1015 Only relevant if $\patchof{L} = \bot$, in which case
1016 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
1017 so Totally Foreign Contents applies.  $\qed$
1018
1019 \end{document}