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