chiark / gitweb /
65be01f4e3e5b51b9a378e5dc73d854c82723f1c
[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} = \pa{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$, xxx
496
497 Trivial from Base Acyclic for $L$.  $\qed$
498
499 \subsection{Unique Base}
500
501 Not applicable. $\qed$
502
503 \subsection{Tip Contents}
504
505 Not applicable. $\qed$
506
507 \subsection{Base Acyclic}
508
509 xxx
510
511 xxx unfinished
512
513 \section{Create Tip}
514
515 xxx tbd
516
517 \section{Anticommit}
518
519 Given $L$ and $\pr$ as represented by $R^+, R^-$.
520 Construct $C$ which has $\pr$ removed.
521 Used for removing a branch dependency.
522 \gathbegin
523  C \hasparents \{ L \}
524 \gathnext
525  \patchof{C} = \patchof{L}
526 \gathnext
527  \mergeof{C}{L}{R^+}{R^-}
528 \end{gather}
529
530 \subsection{Conditions}
531
532 \[ \eqn{ Ingredients }{
533 R^+ \in \pry \land R^- = \baseof{R^+}
534 }\]
535 \[ \eqn{ Into Base }{
536  L \in \pn
537 }\]
538 \[ \eqn{ Unique Tip }{
539  \pendsof{L}{\pry} = \{ R^+ \}
540 }\]
541 \[ \eqn{ Currently Included }{
542  L \haspatch \pry
543 }\]
544
545 \subsection{Ordering of ${L, R^+, R^-}$:}
546
547 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
548 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
549 $\qed$
550
551 (Note that $R^+ \not\le R^-$, i.e. the merge base
552 is a descendant, not an ancestor, of the 2nd parent.)
553
554 \subsection{No Replay}
555
556 No Replay for Merge Results applies.  $\qed$
557
558 \subsection{Desired Contents}
559
560 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
561 \proofstarts
562
563 \subsubsection{For $D = C$:}
564
565 Trivially $D \isin C$.  OK.
566
567 \subsubsection{For $D \neq C, D \not\le L$:}
568
569 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
570 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
571
572 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
573
574 By Currently Included, $D \isin L$.
575
576 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
577 by Unique Tip, $D \le R^+ \equiv D \le L$.  
578 So $D \isin R^+$.
579
580 By Base Acyclic, $D \not\isin R^-$.
581
582 Apply $\merge$: $D \not\isin C$.  OK.
583
584 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
585
586 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
587
588 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
589
590 $\qed$
591
592 \subsection{Unique Base}
593
594 Into Base means that $C \in \pn$, so Unique Base is not
595 applicable. $\qed$
596
597 \subsection{Tip Contents}
598
599 Again, not applicable. $\qed$
600
601 \subsection{Base Acyclic}
602
603 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
604 And by Into Base $C \not\in \py$.
605 Now from Desired Contents, above, $D \isin C
606 \implies D \isin L \lor D = C$, which thus
607 $\implies D \not\in \py$.  $\qed$.
608
609 \subsection{Coherence and Patch Inclusion}
610
611 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
612
613 \subsubsection{For $\p = \pr$:}
614 By Desired Contents, above, $D \not\isin C$.
615 So $C \nothaspatch \pr$.
616
617 \subsubsection{For $\p \neq \pr$:}
618 By Desired Contents, $D \isin C \equiv D \isin L$
619 (since $D \in \py$ so $D \not\in \pry$).
620
621 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
622 So $L \nothaspatch \p \implies C \nothaspatch \p$.
623
624 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
625 so $L \haspatch \p \implies C \haspatch \p$.
626
627 $\qed$
628
629 \subsection{Foreign Inclusion}
630
631 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
632 So by Desired Contents $D \isin C \equiv D \isin L$.
633 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
634
635 And $D \le C \equiv D \le L$.
636 Thus $D \isin C \equiv D \le C$.
637
638 $\qed$
639
640 \subsection{Foreign Contents}
641
642 Not applicable. $\qed$
643
644 \section{Merge}
645
646 Merge commits $L$ and $R$ using merge base $M$:
647 \gathbegin
648  C \hasparents \{ L, R \}
649 \gathnext
650  \patchof{C} = \patchof{L}
651 \gathnext
652  \mergeof{C}{L}{M}{R}
653 \end{gather}
654 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
655
656 \subsection{Conditions}
657 \[ \eqn{ Ingredients }{
658  M \le L, M \le R
659 }\]
660 \[ \eqn{ Tip Merge }{
661  L \in \py \implies
662    \begin{cases}
663       R \in \py : & \baseof{R} \ge \baseof{L}
664               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
665       R \in \pn : & M = \baseof{L} \\
666       \text{otherwise} : & \false
667    \end{cases}
668 }\]
669 \[ \eqn{ Merge Acyclic }{
670     L \in \pn
671    \implies
672     R \nothaspatch \p
673 }\]
674 \[ \eqn{ Removal Merge Ends }{
675     X \not\haspatch \p \land
676     Y \haspatch \p \land
677     M \haspatch \p
678   \implies
679     \pendsof{Y}{\py} = \pendsof{M}{\py}
680 }\]
681 \[ \eqn{ Addition Merge Ends }{
682     X \not\haspatch \p \land
683     Y \haspatch \p \land
684     M \nothaspatch \p
685    \implies \left[
686     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
687    \right]
688 }\]
689 \[ \eqn{ Foreign Merges }{
690     \patchof{L} = \bot \equiv \patchof{R} = \bot
691 }\]
692
693 \subsection{Non-Topbloke merges}
694
695 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
696 (Foreign Merges, above).
697 I.e. not only is it forbidden to merge into a Topbloke-controlled
698 branch without Topbloke's assistance, it is also forbidden to
699 merge any Topbloke-controlled branch into any plain git branch.
700
701 Given those conditions, Tip Merge and Merge Acyclic do not apply.
702 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
703 Merge Ends condition applies.
704
705 So a plain git merge of non-Topbloke branches meets the conditions and
706 is therefore consistent with our scheme.
707
708 \subsection{No Replay}
709
710 No Replay for Merge Results applies.  $\qed$
711
712 \subsection{Unique Base}
713
714 Need to consider only $C \in \py$, ie $L \in \py$,
715 and calculate $\pendsof{C}{\pn}$.  So we will consider some
716 putative ancestor $A \in \pn$ and see whether $A \le C$.
717
718 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
719 But $C \in py$ and $A \in \pn$ so $A \neq C$.  
720 Thus $A \le C \equiv A \le L \lor A \le R$.
721
722 By Unique Base of L and Transitive Ancestors,
723 $A \le L \equiv A \le \baseof{L}$.
724
725 \subsubsection{For $R \in \py$:}
726
727 By Unique Base of $R$ and Transitive Ancestors,
728 $A \le R \equiv A \le \baseof{R}$.
729
730 But by Tip Merge condition on $\baseof{R}$,
731 $A \le \baseof{L} \implies A \le \baseof{R}$, so
732 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
733 Thus $A \le C \equiv A \le \baseof{R}$.  
734 That is, $\baseof{C} = \baseof{R}$.
735
736 \subsubsection{For $R \in \pn$:}
737
738 By Tip Merge condition on $R$ and since $M \le R$,
739 $A \le \baseof{L} \implies A \le R$, so
740 $A \le R \lor A \le \baseof{L} \equiv A \le R$.  
741 Thus $A \le C \equiv A \le R$.  
742 That is, $\baseof{C} = R$.
743
744 $\qed$
745
746 \subsection{Coherence and Patch Inclusion}
747
748 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
749 This involves considering $D \in \py$.  
750
751 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
752 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
753 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
754 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
755
756 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
757 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
758 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
759
760 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
761
762 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
763  \equiv D \isin L \lor D \isin R$.  
764 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
765
766 Consider $D \neq C, D \isin X \land D \isin Y$:
767 By $\merge$, $D \isin C$.  Also $D \le X$ 
768 so $D \le C$.  OK for $C \haspatch \p$.
769
770 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
771 By $\merge$, $D \not\isin C$.  
772 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.  
773 OK for $C \haspatch \p$.
774
775 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
776 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.  
777 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
778 OK for $C \haspatch \p$.
779
780 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
781
782 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
783
784 $M \haspatch \p \implies C \nothaspatch \p$.
785 $M \nothaspatch \p \implies C \haspatch \p$.
786
787 \proofstarts
788
789 One of the Merge Ends conditions applies.  
790 Recall that we are considering $D \in \py$.
791 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
792 We will show for each of
793 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
794 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
795
796 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
797 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
798 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
799 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
800
801 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
802 $D \le Y$ so $D \le C$.  
803 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
804
805 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
806 $D \not\le Y$.  If $D \le X$ then
807 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and 
808 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
809 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
810
811 Consider $D \neq C, M \haspatch P, D \isin Y$:
812 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
813 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
814 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
815
816 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
817 By $\merge$, $D \not\isin C$.  OK.
818
819 $\qed$
820
821 \subsection{Base Acyclic}
822
823 This applies when $C \in \pn$.
824 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
825
826 Consider some $D \in \py$.
827
828 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
829 R$.  And $D \neq C$.  So $D \not\isin C$.
830
831 $\qed$
832
833 \subsection{Tip Contents}
834
835 We need worry only about $C \in \py$.  
836 And $\patchof{C} = \patchof{L}$
837 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
838 of $C$, and its Coherence and Patch Inclusion, as just proved.
839
840 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
841 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
842 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
843 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
844 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
845
846 We will consider an arbitrary commit $D$
847 and prove the Exclusive Tip Contents form.
848
849 \subsubsection{For $D \in \py$:}
850 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
851 \le C$.  OK.
852
853 \subsubsection{For $D \not\in \py, R \not\in \py$:}
854
855 $D \neq C$.  By Tip Contents of $L$,
856 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
857 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
858 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
859 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
860
861 \subsubsection{For $D \not\in \py, R \in \py$:}
862
863 $D \neq C$.
864
865 By Tip Contents
866 $D \isin L \equiv D \isin \baseof{L}$ and
867 $D \isin R \equiv D \isin \baseof{R}$.
868
869 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
870 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
871 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
872 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
873
874 So $D \isin M \equiv D \isin L$ and by $\merge$,
875 $D \isin C \equiv D \isin R$.  But from Unique Base,
876 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
877
878 $\qed$
879
880 \subsection{Foreign Inclusion}
881
882 Consider some $D$ s.t. $\patchof{D} = \bot$.
883 By Foreign Inclusion of $L, M, R$:
884 $D \isin L \equiv D \le L$;
885 $D \isin M \equiv D \le M$;
886 $D \isin R \equiv D \le R$.
887
888 \subsubsection{For $D = C$:}
889
890 $D \isin C$ and $D \le C$.  OK.
891
892 \subsubsection{For $D \neq C, D \isin M$:}
893
894 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
895 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
896
897 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
898
899 By $\merge$, $D \isin C$.
900 And $D \isin X$ means $D \le X$ so $D \le C$.
901 OK.
902
903 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
904
905 By $\merge$, $D \not\isin C$.
906 And $D \not\le L, D \not\le R$ so $D \not\le C$.
907 OK
908
909 $\qed$
910
911 \subsection{Foreign Contents}
912
913 Only relevant if $\patchof{L} = \bot$, in which case
914 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
915 so Totally Foreign Contents applies.  $\qed$
916
917 \end{document}