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