chiark / gitweb /
assert that exact ancestors is trivial
[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{ ~ Truth table (ordered by original definition): \\
222   \begin{tabular}{cccc|c|cc}
223      $D = C$ &
224           $\isin L$ &
225                $\isin M$ &
226                     $\isin R$ & $\isin C$ &
227                                       $L$ vs. $R$ & $L$ vs. $M$
228   \\\hline
229      y &  ? &  ? &  ?      &      y   & ?         & ?            \\
230      n &  y &  y &  y      &      y   & $\equiv$  & $\equiv$     \\
231      n &  y &  n &  y      &      y   & $\equiv$  & $\nequiv$    \\
232      n &  n &  y &  n      &      n   & $\equiv$  & $\nequiv$    \\
233      n &  n &  n &  n      &      n   & $\equiv$  & $\equiv$     \\
234      n &  y &  y &  n      &      n   & $\nequiv$ & $\equiv$     \\
235      n &  n &  y &  y      &      n   & $\nequiv$ & $\nequiv$    \\
236      n &  y &  n &  n      &      y   & $\nequiv$ & $\nequiv$    \\
237      n &  n &  n &  y      &      y   & $\nequiv$ & $\equiv$     \\
238   \end{tabular} \\
239   And original definition is symmetrical in $L$ and $R$.
240 }
241
242 \[ \eqn{Exclusive Tip Contents:}{
243   \bigforall_{C \in \py}
244     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
245       \Bigr]
246 }\]
247 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
248
249 \proof{
250 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
251 So by Base Acyclic $D \isin B \implies D \notin \py$.
252 }
253 \[ \eqntag{{\it Corollary - equivalent to Tip Contents}}{
254   \bigforall_{C \in \py} D \isin C \equiv
255   \begin{cases}
256     D \in \py : & D \le C \\
257     D \not\in \py : & D \isin \baseof{C}
258   \end{cases}
259 }\]
260
261 \[ \eqn{Tip Self Inpatch:}{
262   \bigforall_{C \in \py} C \haspatch \p
263 }\]
264 Ie, tip commits contain their own patch.
265
266 \proof{
267 Apply Exclusive Tip Contents to some $D \in \py$:
268 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
269   D \isin C \equiv D \le C $
270 }
271
272 \[ \eqn{Exact Ancestors:}{
273   \bigforall_{ C \hasparents \set{R} }
274   D \le C \equiv
275     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
276     \lor D = C
277 }\]
278 \proof{ ~ Trivial.}
279
280 \[ \eqn{Transitive Ancestors:}{
281   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
282   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
283 }\]
284
285 \proof{
286 The implication from right to left is trivial because
287 $ \pends() \subset \pancs() $.
288 For the implication from left to right:
289 by the definition of $\mathcal E$,
290 for every such $A$, either $A \in \pends()$ which implies
291 $A \le M$ by the LHS directly,
292 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
293 in which case we repeat for $A'$.  Since there are finitely many
294 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
295 by the LHS.  And $A \le A''$.
296 }
297
298 \[ \eqn{Calculation Of Ends:}{
299   \bigforall_{C \hasparents \set A}
300     \pendsof{C}{\set P} =
301       \begin{cases}
302        C \in \p : & \{ C \}
303       \\
304        C \not\in \p : & \displaystyle
305        \left\{ E \Big|
306            \Bigl[ \Largeexists_{A \in \set A}
307                        E \in \pendsof{A}{\set P} \Bigr] \land
308            \Bigl[ \Largenexists_{B \in \set A}
309                        E \neq B \land E \le B \Bigr]
310        \right\}
311       \end{cases}
312 }\]
313 xxx proof tbd
314
315 \[ \eqn{Ingredients Prevent Replay:}{
316   \left[
317     {C \hasparents \set A} \land
318    \\
319     \left(
320       D \isin C \implies
321        D = C \lor
322        \Largeexists_{A \in \set A} D \isin A
323     \right)
324   \right] \implies \left[
325     D \isin C \implies D \le C
326   \right]
327 }\]
328 \proof{
329   Trivial for $D = C$.  Consider some $D \neq C$, $D \isin C$.
330   By the preconditions, there is some $A$ s.t. $D \in \set A$
331   and $D \isin A$.  By No Replay for $A$, $D \le A$.  And
332   $A \le C$ so $D \le C$.
333 }
334
335 \[ \eqn{Simple Foreign Inclusion:}{
336   \left[
337     C \hasparents \{ L \}
338    \land
339     \bigforall_{D} D \isin C \equiv D \isin L \lor D = C
340   \right]
341  \implies
342    \bigforall_{D \text{ s.t. } \patchof{D} = \bot}
343      D \isin C \equiv D \le C
344 }\]
345 \proof{
346 Consider some $D$ s.t. $\patchof{D} = \bot$.
347 If $D = C$, trivially true.  For $D \neq C$,
348 by Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
349 And by Exact Ancestors $D \le L \equiv D \le C$.
350 So $D \isin C \equiv D \le C$.
351 }
352
353 \[ \eqn{Totally Foreign Contents:}{
354   \bigforall_{C \hasparents \set A}
355    \left[
356     \patchof{C} = \bot \land
357       \bigforall_{A \in \set A} \patchof{A} = \bot
358    \right]
359   \implies
360    \left[
361     D \le C
362    \implies
363     \patchof{D} = \bot
364    \right]
365 }\]
366 \proof{
367 Consider some $D \le C$.  If $D = C$, $\patchof{D} = \bot$ trivially.
368 If $D \neq C$ then $D \le A$ where $A \in \set A$.  By Foreign
369 Contents of $A$, $\patchof{D} = \bot$.
370 }
371
372 \section{Commit annotation}
373
374 We annotate each Topbloke commit $C$ with:
375 \gathbegin
376  \patchof{C}
377 \gathnext
378  \baseof{C}, \text{ if } C \in \py
379 \gathnext
380  \bigforall_{\pq}
381    \text{ either } C \haspatch \pq \text{ or } C \nothaspatch \pq
382 \gathnext
383  \bigforall_{\pqy \not\ni C} \pendsof{C}{\pqy}
384 \end{gather}
385
386 $\patchof{C}$, for each kind of Topbloke-generated commit, is stated
387 in the summary in the section for that kind of commit.
388
389 Whether $\baseof{C}$ is required, and if so what the value is, is
390 stated in the proof of Unique Base for each kind of commit.
391
392 $C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
393 set $\{ \pq | C \haspatch \pq \}$.  Whether $C \haspatch \pq$
394 is in stated
395 (in terms of $I \haspatch \pq$ or $I \nothaspatch \pq$
396 for the ingredients $I$),
397 in the proof of Coherence for each kind of commit.
398
399 $\pendsof{C}{\pq^+}$ is computed, for all Topbloke-generated commits,
400 using the lemma Calculation of Ends, above.
401 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
402 make it wrong to make plain commits with git because the recorded $\pends$
403 would have to be updated.  The annotation is not needed in that case
404 because $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
405
406 \section{Simple commit}
407
408 A simple single-parent forward commit $C$ as made by git-commit.
409 \begin{gather}
410 \tag*{} C \hasparents \{ A \} \\
411 \tag*{} \patchof{C} = \patchof{A} \\
412 \tag*{} D \isin C \equiv D \isin A \lor D = C
413 \end{gather}
414 This also covers Topbloke-generated commits on plain git branches:
415 Topbloke strips the metadata when exporting.
416
417 \subsection{No Replay}
418
419 Ingredients Prevent Replay applies.  $\qed$
420
421 \subsection{Unique Base}
422 If $A, C \in \py$ then by Calculation of Ends for
423 $C, \py, C \not\in \py$:
424 $\pendsof{C}{\pn} = \pendsof{A}{\pn}$ so
425 $\baseof{C} = \baseof{A}$. $\qed$
426
427 \subsection{Tip Contents}
428 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
429 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
430 Substitute into the contents of $C$:
431 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
432     \lor D = C \]
433 Since $D = C \implies D \in \py$,
434 and substituting in $\baseof{C}$, this gives:
435 \[ D \isin C \equiv D \isin \baseof{C} \lor
436     (D \in \py \land D \le A) \lor
437     (D = C \land D \in \py) \]
438 \[ \equiv D \isin \baseof{C} \lor
439    [ D \in \py \land ( D \le A \lor D = C ) ] \]
440 So by Exact Ancestors:
441 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
442 ) \]
443 $\qed$
444
445 \subsection{Base Acyclic}
446
447 Need to consider only $A, C \in \pn$.
448
449 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
450
451 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
452 $A$, $D \isin C \implies D \not\in \py$.
453
454 $\qed$
455
456 \subsection{Coherence and patch inclusion}
457
458 Need to consider $D \in \py$
459
460 \subsubsection{For $A \haspatch P, D = C$:}
461
462 Ancestors of $C$:
463 $ D \le C $.
464
465 Contents of $C$:
466 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
467
468 \subsubsection{For $A \haspatch P, D \neq C$:}
469 Ancestors: $ D \le C \equiv D \le A $.
470
471 Contents: $ D \isin C \equiv D \isin A \lor f $
472 so $ D \isin C \equiv D \isin A $.
473
474 So:
475 \[ A \haspatch P \implies C \haspatch P \]
476
477 \subsubsection{For $A \nothaspatch P$:}
478
479 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
480 Thus $D \neq C$.
481
482 Now by contents of $A$, $D \notin A$, so $D \notin C$.
483
484 So:
485 \[ A \nothaspatch P \implies C \nothaspatch P \]
486 $\qed$
487
488 \subsection{Foreign Inclusion:}
489
490 Simple Foreign Inclusion applies.  $\qed$
491
492 \subsection{Foreign Contents:}
493
494 Only relevant if $\patchof{C} = \bot$, and in that case Totally
495 Foreign Contents applies. $\qed$
496
497 \section{Create Base}
498
499 Given $L$, create a Topbloke base branch initial commit $B$.
500 \gathbegin
501  B \hasparents \{ L \}
502 \gathnext
503  \patchof{B} = \pqn
504 \gathnext
505  D \isin B \equiv D \isin L \lor D = B
506 \end{gather}
507
508 \subsection{Conditions}
509
510 \[ \eqn{ Ingredients }{
511  \patchof{L} = \pa{L} \lor \patchof{L} = \bot
512 }\]
513 \[ \eqn{ Create Acyclic }{
514  L \not\haspatch \pq
515 }\]
516
517 \subsection{No Replay}
518
519 Ingredients Prevent Replay applies.  $\qed$
520
521 \subsection{Unique Base}
522
523 Not applicable.
524
525 \subsection{Tip Contents}
526
527 Not applicable.
528
529 \subsection{Base Acyclic}
530
531 Consider some $D \isin B$.  If $D = B$, $D \in \pqn$.
532 If $D \neq B$, $D \isin L$, and by Create Acyclic
533 $D \not\in \pqy$.  $\qed$
534
535 \subsection{Coherence and Patch Inclusion}
536
537 Consider some $D \in \p$.
538 $B \not\in \py$ so $D \neq B$.  So $D \isin B \equiv D \isin L$
539 and $D \le B \equiv D \le L$.
540
541 Thus $L \haspatch \p \implies B \haspatch P$
542 and $L \nothaspatch \p \implies B \nothaspatch P$.
543
544 $\qed$.
545
546 \subsection{Foreign Inclusion}
547
548 Simple Foreign Inclusion applies. $\qed$
549
550 \subsection{Foreign Contents}
551
552 Not applicable.
553
554 \section{Create Tip}
555
556 Given a Topbloke base $B$, create a tip branch initial commit B.
557 \gathbegin
558  C \hasparents \{ B \}
559 \gathnext
560  \patchof{B} = \pqy
561 \gathnext
562  D \isin C \equiv D \isin B \lor D = C
563 \end{gather}
564
565 \subsection{Conditions}
566
567 \[ \eqn{ Ingredients }{
568  \patchof{B} = \pqn
569 }\]
570 \[ \eqn{ No Sneak }{
571  \pendsof{B}{\pqy} = \{ \}
572 }\]
573
574 \subsection{No Replay}
575
576 Ingredients Prevent Replay applies.  $\qed$
577
578 \subsection{Unique Base}
579
580 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.  $\qed$
581
582 \subsection{Tip Contents}
583
584 Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.
585
586 If $D \neq C$, $D \isin C \equiv D \isin B$.
587 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
588 So $D \isin C \equiv D \isin \baseof{B}$.
589
590 $\qed$
591
592 \subsection{Base Acyclic}
593
594 Not applicable.
595
596 \subsection{Coherence and Patch Inclusion}
597
598 $$
599 \begin{cases}
600   \p = \pq    \lor B \haspatch \p : & C \haspatch \p \\
601   \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
602 \end{cases}
603 $$
604
605 \proofstarts
606 ~ Consider some $D \in \py$.
607
608 \subsubsection{For $\p = \pq$:}
609
610 By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
611 By No Sneak, $D \le B \equiv D = C$.  Thus $C \haspatch \pq$.
612
613 \subsubsection{For $\p \neq \pq$:}
614
615 $D \neq C$.  So $D \isin C \equiv D \isin B$,
616 and $D \le C \equiv D \le B$.
617
618 $\qed$
619
620 \subsection{Foreign Inclusion}
621
622 Simple Foreign Inclusion applies.  $\qed$
623
624 \subsection{Foreign Contents}
625
626 Not applicable.
627
628 \section{Anticommit}
629
630 Given $L$ and $\pr$ as represented by $R^+, R^-$.
631 Construct $C$ which has $\pr$ removed.
632 Used for removing a branch dependency.
633 \gathbegin
634  C \hasparents \{ L \}
635 \gathnext
636  \patchof{C} = \patchof{L}
637 \gathnext
638  \mergeof{C}{L}{R^+}{R^-}
639 \end{gather}
640
641 \subsection{Conditions}
642
643 \[ \eqn{ Ingredients }{
644 R^+ \in \pry \land R^- = \baseof{R^+}
645 }\]
646 \[ \eqn{ Into Base }{
647  L \in \pn
648 }\]
649 \[ \eqn{ Unique Tip }{
650  \pendsof{L}{\pry} = \{ R^+ \}
651 }\]
652 \[ \eqn{ Currently Included }{
653  L \haspatch \pry
654 }\]
655
656 \subsection{Ordering of Ingredients:}
657
658 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
659 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$.
660 $\qed$
661
662 (Note that $R^+ \not\le R^-$, i.e. the merge base
663 is a descendant, not an ancestor, of the 2nd parent.)
664
665 \subsection{No Replay}
666
667 By definition of $\merge$,
668 $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$.
669 So, by Ordering of Ingredients,
670 Ingredients Prevent Replay applies.  $\qed$
671
672 \subsection{Desired Contents}
673
674 \[ D \isin C \equiv [ D \notin \pry \land D \isin L ] \lor D = C \]
675 \proofstarts
676
677 \subsubsection{For $D = C$:}
678
679 Trivially $D \isin C$.  OK.
680
681 \subsubsection{For $D \neq C, D \not\le L$:}
682
683 By No Replay $D \not\isin L$.  Also $D \not\le R^-$ hence
684 $D \not\isin R^-$.  Thus $D \not\isin C$.  OK.
685
686 \subsubsection{For $D \neq C, D \le L, D \in \pry$:}
687
688 By Currently Included, $D \isin L$.
689
690 By Tip Self Inpatch, $D \isin R^+ \equiv D \le R^+$, but by
691 by Unique Tip, $D \le R^+ \equiv D \le L$.
692 So $D \isin R^+$.
693
694 By Base Acyclic, $D \not\isin R^-$.
695
696 Apply $\merge$: $D \not\isin C$.  OK.
697
698 \subsubsection{For $D \neq C, D \le L, D \notin \pry$:}
699
700 By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
701
702 Apply $\merge$: $D \isin C \equiv D \isin L$.  OK.
703
704 $\qed$
705
706 \subsection{Unique Base}
707
708 Into Base means that $C \in \pn$, so Unique Base is not
709 applicable. $\qed$
710
711 \subsection{Tip Contents}
712
713 Again, not applicable. $\qed$
714
715 \subsection{Base Acyclic}
716
717 By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
718 And by Into Base $C \not\in \py$.
719 Now from Desired Contents, above, $D \isin C
720 \implies D \isin L \lor D = C$, which thus
721 $\implies D \not\in \py$.  $\qed$.
722
723 \subsection{Coherence and Patch Inclusion}
724
725 Need to consider some $D \in \py$.  By Into Base, $D \neq C$.
726
727 \subsubsection{For $\p = \pr$:}
728 By Desired Contents, above, $D \not\isin C$.
729 So $C \nothaspatch \pr$.
730
731 \subsubsection{For $\p \neq \pr$:}
732 By Desired Contents, $D \isin C \equiv D \isin L$
733 (since $D \in \py$ so $D \not\in \pry$).
734
735 If $L \nothaspatch \p$, $D \not\isin L$ so $D \not\isin C$.
736 So $L \nothaspatch \p \implies C \nothaspatch \p$.
737
738 Whereas if $L \haspatch \p$, $D \isin L \equiv D \le L$.
739 so $L \haspatch \p \implies C \haspatch \p$.
740
741 $\qed$
742
743 \subsection{Foreign Inclusion}
744
745 Consider some $D$ s.t. $\patchof{D} = \bot$.  $D \neq C$.
746 So by Desired Contents $D \isin C \equiv D \isin L$.
747 By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.
748
749 And $D \le C \equiv D \le L$.
750 Thus $D \isin C \equiv D \le C$.
751
752 $\qed$
753
754 \subsection{Foreign Contents}
755
756 Not applicable.
757
758 \section{Merge}
759
760 Merge commits $L$ and $R$ using merge base $M$:
761 \gathbegin
762  C \hasparents \{ L, R \}
763 \gathnext
764  \patchof{C} = \patchof{L}
765 \gathnext
766  \mergeof{C}{L}{M}{R}
767 \end{gather}
768 We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
769
770 \subsection{Conditions}
771 \[ \eqn{ Ingredients }{
772  M \le L, M \le R
773 }\]
774 \[ \eqn{ Tip Merge }{
775  L \in \py \implies
776    \begin{cases}
777       R \in \py : & \baseof{R} \ge \baseof{L}
778               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
779       R \in \pn : & M = \baseof{L} \\
780       \text{otherwise} : & \false
781    \end{cases}
782 }\]
783 \[ \eqn{ Merge Acyclic }{
784     L \in \pn
785    \implies
786     R \nothaspatch \p
787 }\]
788 \[ \eqn{ Removal Merge Ends }{
789     X \not\haspatch \p \land
790     Y \haspatch \p \land
791     M \haspatch \p
792   \implies
793     \pendsof{Y}{\py} = \pendsof{M}{\py}
794 }\]
795 \[ \eqn{ Addition Merge Ends }{
796     X \not\haspatch \p \land
797     Y \haspatch \p \land
798     M \nothaspatch \p
799    \implies \left[
800     \bigforall_{E \in \pendsof{X}{\py}} E \le Y
801    \right]
802 }\]
803 \[ \eqn{ Foreign Merges }{
804     \patchof{L} = \bot \equiv \patchof{R} = \bot
805 }\]
806
807 \subsection{Non-Topbloke merges}
808
809 We require both $\patchof{L} = \bot$ and $\patchof{R} = \bot$
810 (Foreign Merges, above).
811 I.e. not only is it forbidden to merge into a Topbloke-controlled
812 branch without Topbloke's assistance, it is also forbidden to
813 merge any Topbloke-controlled branch into any plain git branch.
814
815 Given those conditions, Tip Merge and Merge Acyclic do not apply.
816 And $Y \not\in \py$ so $\neg [ Y \haspatch \p ]$ so neither
817 Merge Ends condition applies.
818
819 So a plain git merge of non-Topbloke branches meets the conditions and
820 is therefore consistent with our scheme.
821
822 \subsection{No Replay}
823
824 By definition of $\merge$,
825 $D \isin C \implies D \isin L \lor D \isin R \lor D = C$.
826 So, by Ingredients,
827 Ingredients Prevent Replay applies.  $\qed$
828
829 \subsection{Unique Base}
830
831 Need to consider only $C \in \py$, ie $L \in \py$,
832 and calculate $\pendsof{C}{\pn}$.  So we will consider some
833 putative ancestor $A \in \pn$ and see whether $A \le C$.
834
835 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
836 But $C \in py$ and $A \in \pn$ so $A \neq C$.
837 Thus $A \le C \equiv A \le L \lor A \le R$.
838
839 By Unique Base of L and Transitive Ancestors,
840 $A \le L \equiv A \le \baseof{L}$.
841
842 \subsubsection{For $R \in \py$:}
843
844 By Unique Base of $R$ and Transitive Ancestors,
845 $A \le R \equiv A \le \baseof{R}$.
846
847 But by Tip Merge condition on $\baseof{R}$,
848 $A \le \baseof{L} \implies A \le \baseof{R}$, so
849 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
850 Thus $A \le C \equiv A \le \baseof{R}$.
851 That is, $\baseof{C} = \baseof{R}$.
852
853 \subsubsection{For $R \in \pn$:}
854
855 By Tip Merge condition on $R$ and since $M \le R$,
856 $A \le \baseof{L} \implies A \le R$, so
857 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
858 Thus $A \le C \equiv A \le R$.
859 That is, $\baseof{C} = R$.
860
861 $\qed$
862
863 \subsection{Coherence and Patch Inclusion}
864
865 Need to determine $C \haspatch \p$ based on $L,M,R \haspatch \p$.
866 This involves considering $D \in \py$.
867
868 \subsubsection{For $L \nothaspatch \p, R \nothaspatch \p$:}
869 $D \not\isin L \land D \not\isin R$.  $C \not\in \py$ (otherwise $L
870 \in \py$ ie $L \haspatch \p$ by Tip Self Inpatch).  So $D \neq C$.
871 Applying $\merge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$.
872
873 \subsubsection{For $L \haspatch \p, R \haspatch \p$:}
874 $D \isin L \equiv D \le L$ and $D \isin R \equiv D \le R$.
875 (Likewise $D \isin X \equiv D \le X$ and $D \isin Y \equiv D \le Y$.)
876
877 Consider $D = C$: $D \isin C$, $D \le C$, OK for $C \haspatch \p$.
878
879 For $D \neq C$: $D \le C \equiv D \le L \lor D \le R
880  \equiv D \isin L \lor D \isin R$.
881 (Likewise $D \le C \equiv D \le X \lor D \le Y$.)
882
883 Consider $D \neq C, D \isin X \land D \isin Y$:
884 By $\merge$, $D \isin C$.  Also $D \le X$
885 so $D \le C$.  OK for $C \haspatch \p$.
886
887 Consider $D \neq C, D \not\isin X \land D \not\isin Y$:
888 By $\merge$, $D \not\isin C$.
889 And $D \not\le X \land D \not\le Y$ so $D \not\le C$.
890 OK for $C \haspatch \p$.
891
892 Remaining case, wlog, is $D \not\isin X \land D \isin Y$.
893 $D \not\le X$ so $D \not\le M$ so $D \not\isin M$.
894 Thus by $\merge$, $D \isin C$.  And $D \le Y$ so $D \le C$.
895 OK for $C \haspatch \p$.
896
897 So indeed $L \haspatch \p \land R \haspatch \p \implies C \haspatch \p$.
898
899 \subsubsection{For (wlog) $X \not\haspatch \p, Y \haspatch \p$:}
900
901 $M \haspatch \p \implies C \nothaspatch \p$.
902 $M \nothaspatch \p \implies C \haspatch \p$.
903
904 \proofstarts
905
906 One of the Merge Ends conditions applies.
907 Recall that we are considering $D \in \py$.
908 $D \isin Y \equiv D \le Y$.  $D \not\isin X$.
909 We will show for each of
910 various cases that $D \isin C \equiv M \nothaspatch \p \land D \le C$
911 (which suffices by definition of $\haspatch$ and $\nothaspatch$).
912
913 Consider $D = C$:  Thus $C \in \py, L \in \py$, and by Tip
914 Self Inpatch $L \haspatch \p$, so $L=Y, R=X$.  By Tip Merge,
915 $M=\baseof{L}$.  So by Base Acyclic $D \not\isin M$, i.e.
916 $M \nothaspatch \p$.  And indeed $D \isin C$ and $D \le C$.  OK.
917
918 Consider $D \neq C, M \nothaspatch P, D \isin Y$:
919 $D \le Y$ so $D \le C$.
920 $D \not\isin M$ so by $\merge$, $D \isin C$.  OK.
921
922 Consider $D \neq C, M \nothaspatch P, D \not\isin Y$:
923 $D \not\le Y$.  If $D \le X$ then
924 $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and
925 Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$.
926 Thus $D \not\le C$.  By $\merge$, $D \not\isin C$.  OK.
927
928 Consider $D \neq C, M \haspatch P, D \isin Y$:
929 $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends
930 and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$.
931 Thus $D \isin M$.  By $\merge$, $D \not\isin C$.  OK.
932
933 Consider $D \neq C, M \haspatch P, D \not\isin Y$:
934 By $\merge$, $D \not\isin C$.  OK.
935
936 $\qed$
937
938 \subsection{Base Acyclic}
939
940 This applies when $C \in \pn$.
941 $C \in \pn$ when $L \in \pn$ so by Merge Acyclic, $R \nothaspatch \p$.
942
943 Consider some $D \in \py$.
944
945 By Base Acyclic of $L$, $D \not\isin L$.  By the above, $D \not\isin
946 R$.  And $D \neq C$.  So $D \not\isin C$.
947
948 $\qed$
949
950 \subsection{Tip Contents}
951
952 We need worry only about $C \in \py$.
953 And $\patchof{C} = \patchof{L}$
954 so $L \in \py$ so $L \haspatch \p$.  We will use the Unique Base
955 of $C$, and its Coherence and Patch Inclusion, as just proved.
956
957 Firstly we show $C \haspatch \p$: If $R \in \py$, then $R \haspatch
958 \p$ and by Coherence/Inclusion $C \haspatch \p$ .  If $R \not\in \py$
959 then by Tip Merge $M = \baseof{L}$ so by Base Acyclic and definition
960 of $\nothaspatch$, $M \nothaspatch \p$.  So by Coherence/Inclusion $C
961 \haspatch \p$ (whether $R \haspatch \p$ or $\nothaspatch$).
962
963 We will consider an arbitrary commit $D$
964 and prove the Exclusive Tip Contents form.
965
966 \subsubsection{For $D \in \py$:}
967 $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D
968 \le C$.  OK.
969
970 \subsubsection{For $D \not\in \py, R \not\in \py$:}
971
972 $D \neq C$.  By Tip Contents of $L$,
973 $D \isin L \equiv D \isin \baseof{L}$, and by Tip Merge condition,
974 $D \isin L \equiv D \isin M$.  So by definition of $\merge$, $D \isin
975 C \equiv D \isin R$.  And $R = \baseof{C}$ by Unique Base of $C$.
976 Thus $D \isin C \equiv D \isin \baseof{C}$.  OK.
977
978 \subsubsection{For $D \not\in \py, R \in \py$:}
979
980 $D \neq C$.
981
982 By Tip Contents
983 $D \isin L \equiv D \isin \baseof{L}$ and
984 $D \isin R \equiv D \isin \baseof{R}$.
985
986 If $\baseof{L} = M$, trivially $D \isin M \equiv D \isin \baseof{L}.$
987 Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$,
988 $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$,
989 $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$.
990
991 So $D \isin M \equiv D \isin L$ and by $\merge$,
992 $D \isin C \equiv D \isin R$.  But from Unique Base,
993 $\baseof{C} = R$ so $D \isin C \equiv D \isin \baseof{C}$.  OK.
994
995 $\qed$
996
997 \subsection{Foreign Inclusion}
998
999 Consider some $D$ s.t. $\patchof{D} = \bot$.
1000 By Foreign Inclusion of $L, M, R$:
1001 $D \isin L \equiv D \le L$;
1002 $D \isin M \equiv D \le M$;
1003 $D \isin R \equiv D \le R$.
1004
1005 \subsubsection{For $D = C$:}
1006
1007 $D \isin C$ and $D \le C$.  OK.
1008
1009 \subsubsection{For $D \neq C, D \isin M$:}
1010
1011 Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin
1012 R$.  So by $\merge$, $D \isin C$.  And $D \le C$.  OK.
1013
1014 \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:}
1015
1016 By $\merge$, $D \isin C$.
1017 And $D \isin X$ means $D \le X$ so $D \le C$.
1018 OK.
1019
1020 \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:}
1021
1022 By $\merge$, $D \not\isin C$.
1023 And $D \not\le L, D \not\le R$ so $D \not\le C$.
1024 OK
1025
1026 $\qed$
1027
1028 \subsection{Foreign Contents}
1029
1030 Only relevant if $\patchof{L} = \bot$, in which case
1031 $\patchof{C} = \bot$ and by Foreign Merges $\patchof{R} = \bot$,
1032 so Totally Foreign Contents applies.  $\qed$
1033
1034 \end{document}