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
  14 \newcommand{\has}{\sqsupseteq}
  15 \newcommand{\isin}{\sqsubseteq}
  16
  17 \newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
  18 \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
  19 \newcommand{\haspatch}{\sqSupset}
  20 \newcommand{\patchisin}{\sqSubset}
  21
  22         \newif\ifhidehack\hidehackfalse
  23         \DeclareRobustCommand\hidefromedef[2]{%
  24           \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
  25         \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
  26
  27 \newcommand{\set}[1]{\mathbb{#1}}
  28 \newcommand{\pay}[1]{\pa{#1}^+}
  29 \newcommand{\pan}[1]{\pa{#1}^-}
  30
  31 \newcommand{\p}{\pa{P}}
  32 \newcommand{\py}{\pay{P}}
  33 \newcommand{\pn}{\pan{P}}
  34
  35 \newcommand{\pr}{\pa{R}}
  36 \newcommand{\pry}{\pay{R}}
  37 \newcommand{\prn}{\pan{R}}
  38
  39 %\newcommand{\hasparents}{\underaccent{1}{>}}
  40 %\newcommand{\hasparents}{{%
  41 %  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
  42 \newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
  43 \newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
  44
  45 \renewcommand{\implies}{\Rightarrow}
  46 \renewcommand{\equiv}{\Leftrightarrow}
  47 \renewcommand{\land}{\wedge}
  48 \renewcommand{\lor}{\vee}
  49
  50 \newcommand{\pancs}{{\mathcal A}}
  51 \newcommand{\pends}{{\mathcal E}}
  52
  53 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
  54 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
  55
  56 \newcommand{\merge}[4]{{\mathcal M}(#1,#2,#3,#4)}
  57 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
  58
  59 \newcommand{\patch}{{\mathcal P}}
  60 \newcommand{\base}{{\mathcal B}}
  61
  62 \newcommand{\patchof}[1]{\patch ( #1 ) }
  63 \newcommand{\baseof}[1]{\base ( #1 ) }
  64
  65 \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
  66 \newcommand{\corrolary}[1]{ #1 \tag*{\mbox{\it Corrolary.}} }
  67
  68 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
  69 \newcommand{\bigforall}{%
  70   \mathop{\mathchoice%
  71     {\hbox{\huge$\forall$}}%
  72     {\hbox{\Large$\forall$}}%
  73     {\hbox{\normalsize$\forall$}}%
  74     {\hbox{\scriptsize$\forall$}}}%
  75 }
  76
  77 \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
  78 \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
  79
  80 \newcommand{\qed}{\square}
  81 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
  82
  83 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
  84 \newcommand{\gathnext}{\\ \tag*{}}
  85
  86 \newcommand{\true}{t}
  87 \newcommand{\false}{f}
  88
  89 \begin{document}
  90
  91 \section{Notation}
  92
  93 \begin{basedescript}{
  94 \desclabelwidth{5em}
  95 \desclabelstyle{\nextlinelabel}
  96 }
  97 \item[ $ C \hasparents \set X $ ]
  98 The parents of commit $C$ are exactly the set
  99 $\set X$.
 100
 101 \item[ $ C \ge D $ ]
 102 $C$ is a descendant of $D$ in the git commit
 103 graph.  This is a partial order, namely the transitive closure of
 104 $ D \in \set X $ where $ C \hasparents \set X $.
 105
 106 \item[ $ C \has D $ ]
 107 Informally, the tree at commit $C$ contains the change
 108 made in commit $D$.  Does not take account of deliberate reversions by
 109 the user or reversion, rebasing or rewinding in
 110 non-Topbloke-controlled branches.  For merges and Topbloke-generated
 111 anticommits or re-commits, the ``change made'' is only to be thought
 112 of as any conflict resolution.  This is not a partial order because it
 113 is not transitive.
 114
 115 \item[ $ \p, \py, \pn $ ]
 116 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
 117 are respectively the base and tip git branches.  $\p$ may be used
 118 where the context requires a set, in which case the statement
 119 is to be taken as applying to both $\py$ and $\pn$.
 120 All these sets are distinct.  Hence:
 121
 122 \item[ $ \patchof{ C } $ ]
 123 Either $\p$ s.t. $ C \in \p $, or $\bot$.
 124 A function from commits to patches' sets $\p$.
 125
 126 \item[ $ \pancsof{C}{\set P} $ ]
 127 $ \{ A \; | \; A \le C \land A \in \set P \} $
 128 i.e. all the ancestors of $C$
 129 which are in $\set P$.
 130
 131 \item[ $ \pendsof{C}{\set P} $ ]
 132 $ \{ E \; | \; E \in \pancsof{C}{\set P}
 133   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
 134   E \neq A \land E \le A \} $
 135 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
 136
 137 \item[ $ \baseof{C} $ ]
 138 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
 139 A partial function from commits to commits.
 140 See Unique Base, below.
 141
 142 \item[ $ C \haspatch \p $ ]
 143 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
 144 ~ Informally, $C$ has the contents of $\p$.
 145
 146 \item[ $ C \nothaspatch \p $ ]
 147 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
 148 ~ Informally, $C$ has none of the contents of $\p$.
 149
 150 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
 151 patch is applied to a non-Topbloke branch and then bubbles back to
 152 the Topbloke patch itself, we hope that git's merge algorithm will
 153 DTRT or that the user will no longer care about the Topbloke patch.
 154
 155 \item[ $\displaystyle \merge{C}{L}{M}{R} $ ]
 156 The contents of a git merge result:
 157
 158 $\displaystyle D \isin C \equiv
 159   \begin{cases}
 160     (D \isin L \land D \isin R) \lor D = C : & \true \\
 161     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
 162     \text{otherwise} : & D \not\isin M
 163   \end{cases}
 164 $
 165
 166 \end{basedescript}
 167 \newpage
 168 \section{Invariants}
 169
 170 We maintain these each time we construct a new commit. \\
 171 \[ \eqn{No Replay:}{
 172   C \has D \implies C \ge D
 173 }\]
 174 \[\eqn{Unique Base:}{
 175  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
 176 }\]
 177 \[\eqn{Tip Contents:}{
 178   \bigforall_{C \in \py} D \isin C \equiv
 179     { D \isin \baseof{C} \lor \atop
 180       (D \in \py \land D \le C) }
 181 }\]
 182 \[\eqn{Base Acyclic:}{
 183   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
 184 }\]
 185 \[\eqn{Coherence:}{
 186   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
 187 }\]
 188 \[\eqn{Foreign Inclusion:}{
 189   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
 190 }\]
 191
 192 \section{Some lemmas}
 193
 194 \[ \eqn{Exclusive Tip Contents:}{
 195   \bigforall_{C \in \py}
 196     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
 197       \Bigr]
 198 }\]
 199 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 200
 201 \proof{
 202 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
 203 So by Base Acyclic $D \isin B \implies D \notin \py$.
 204 }
 205 \[ \corrolary{
 206   \bigforall_{C \in \py} D \isin C \equiv
 207   \begin{cases}
 208     D \in \py : & D \le C \\
 209     D \not\in \py : & D \isin \baseof{C}
 210   \end{cases}
 211 }\]
 212
 213 \[ \eqn{Tip Self Inpatch:}{
 214   \bigforall_{C \in \py} C \haspatch \p
 215 }\]
 216 Ie, tip commits contain their own patch.
 217
 218 \proof{
 219 Apply Exclusive Tip Contents to some $D \in \py$:
 220 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
 221   D \isin C \equiv D \le C $
 222 }
 223
 224 \[ \eqn{Exact Ancestors:}{
 225   \bigforall_{ C \hasparents \set{R} }
 226   D \le C \equiv
 227     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
 228     \lor D = C
 229 }\]
 230
 231 \[ \eqn{Transitive Ancestors:}{
 232   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
 233   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
 234 }\]
 235
 236 \proof{
 237 The implication from right to left is trivial because
 238 $ \pends() \subset \pancs() $.
 239 For the implication from left to right:
 240 by the definition of $\mathcal E$,
 241 for every such $A$, either $A \in \pends()$ which implies
 242 $A \le M$ by the LHS directly,
 243 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
 244 in which case we repeat for $A'$.  Since there are finitely many
 245 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 246 by the LHS.  And $A \le A''$.
 247 }
 248 \[ \eqn{Calculation Of Ends:}{
 249   \bigforall_{C \hasparents \set A}
 250     \pendsof{C}{\set P} =
 251        \left\{ E \Big|
 252            \Bigl[ \Largeexists_{A \in \set A}
 253                        E \in \pendsof{A}{\set P} \Bigr] \land
 254            \Bigl[ \Largenexists_{B \in \set A}
 255                        E \neq B \land E \le B \Bigr]
 256        \right\}
 257 }\]
 258 XXX proof TBD.
 259
 260 \subsection{No Replay for Merge Results}
 261
 262 If we are constructing $C$, given
 263 \gathbegin
 264   \merge{C}{L}{M}{R}
 265 \gathnext
 266   L \le C
 267 \gathnext
 268   R \le C
 269 \end{gather}
 270 No Replay is preserved.  {\it Proof:}
 271
 272 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 273
 274 \subsubsection{For $D \isin L \land D \isin R$:}
 275 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
 276
 277 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 278 $D \not\isin C$.  OK.
 279
 280 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 281  \land D \not\isin M$:}
 282 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
 283 R$ so $D \le C$.  OK.
 284
 285 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 286  \land D \isin M$:}
 287 $D \not\isin C$.  OK.
 288
 289 $\qed$
 290
 291 \section{Commit annotation}
 292
 293 We annotate each Topbloke commit $C$ with:
 294 \gathbegin
 295  \patchof{C}
 296 \gathnext
 297  \baseof{C}, \text{ if } C \in \py
 298 \gathnext
 299  \bigforall_{\pa{Q}}
 300    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
 301 \gathnext
 302  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 303 \end{gather}
 304
 305 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 306 make it wrong to make plain commits with git because the recorded $\pends$
 307 would have to be updated.  The annotation is not needed because
 308 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 309
 310 \section{Simple commit}
 311
 312 A simple single-parent forward commit $C$ as made by git-commit.
 313 \begin{gather}
 314 \tag*{} C \hasparents \{ A \} \\
 315 \tag*{} \patchof{C} = \patchof{A} \\
 316 \tag*{} D \isin C \equiv D \isin A \lor D = C
 317 \end{gather}
 318
 319 \subsection{No Replay}
 320 Trivial.
 321
 322 \subsection{Unique Base}
 323 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
 324
 325 \subsection{Tip Contents}
 326 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 327 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 328 Substitute into the contents of $C$:
 329 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 330     \lor D = C \]
 331 Since $D = C \implies D \in \py$,
 332 and substituting in $\baseof{C}$, this gives:
 333 \[ D \isin C \equiv D \isin \baseof{C} \lor
 334     (D \in \py \land D \le A) \lor
 335     (D = C \land D \in \py) \]
 336 \[ \equiv D \isin \baseof{C} \lor
 337    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 338 So by Exact Ancestors:
 339 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 340 ) \]
 341 $\qed$
 342
 343 \subsection{Base Acyclic}
 344
 345 Need to consider only $A, C \in \pn$.
 346
 347 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 348
 349 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 350 $A$, $D \isin C \implies D \not\in \py$. $\qed$
 351
 352 \subsection{Coherence and patch inclusion}
 353
 354 Need to consider $D \in \py$
 355
 356 \subsubsection{For $A \haspatch P, D = C$:}
 357
 358 Ancestors of $C$:
 359 $ D \le C $.
 360
 361 Contents of $C$:
 362 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 363
 364 \subsubsection{For $A \haspatch P, D \neq C$:}
 365 Ancestors: $ D \le C \equiv D \le A $.
 366
 367 Contents: $ D \isin C \equiv D \isin A \lor f $
 368 so $ D \isin C \equiv D \isin A $.
 369
 370 So:
 371 \[ A \haspatch P \implies C \haspatch P \]
 372
 373 \subsubsection{For $A \nothaspatch P$:}
 374
 375 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 376 Thus $D \neq C$.
 377
 378 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 379
 380 So:
 381 \[ A \nothaspatch P \implies C \nothaspatch P \]
 382 $\qed$
 383
 384 \subsection{Foreign inclusion:}
 385
 386 If $D = C$, trivial.  For $D \neq C$:
 387 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 388
 389 \section{Anticommit}
 390
 391 Given $L, R^+, R^-$ where
 392 $R^+ \in \pry, R^- = \baseof{R^+}$.
 393 Construct $C$ which has $\pr$ removed.
 394 Used for removing a branch dependency.
 395 \gathbegin
 396  C \hasparents \{ L \}
 397 \gathnext
 398  \patchof{C} = \patchof{L}
 399 \gathnext
 400  \merge{C}{L}{R^+}{R^-}
 401 \end{gather}
 402
 403 \subsection{Conditions}
 404
 405 \[ \eqn{ Unique Tip }{
 406  \pendsof{L}{\pry} = \{ R^+ \}
 407 }\]
 408 \[ \eqn{ Currently Included }{
 409  L \haspatch \pry
 410 }\]
 411 \[ \eqn{ Not Self }{
 412  L \not\in \{ R^+ \}
 413 }\]
 414
 415 \subsection{No Replay}
 416
 417 By Unique Tip, $R^+ \le L$.  By definition of $\base$, $R^- \le R^+$
 418 so $R^- \le L$.  So $R^+ \le C$ and $R^- \le C$ and No Replay for
 419 Merge Results applies. $\qed$
 420
 421 \subsection{Desired Contents}
 422
 423 \[ $D \isin C \equiv [ D \not\in \pry \land D \isin L$ ] \lor D = C \]
 424 {\it Proof.}
 425
 426 \subsubsection{For $D = C$:}
 427
 428 Trivially $D \isin C$.  OK.
 429
 430 \subsubsection{For $D \not\le C$:}
 431
 432
 433
 434 \subsubsection{For $D \in R^+$:}
 435 By Currently Included,
 436
 437 \subsection{Unique Base}
 438
 439 Need to consider only $C \in \py$, ie $L \in \py$.
 440
 441 xxx tbd
 442
 443 \section{Merge}
 444
 445 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 446 \gathbegin
 447  C \hasparents \{ L, R \}
 448 \gathnext
 449  \patchof{C} = \patchof{L}
 450 \gathnext
 451  \merge{C}{L}{M}{R}
 452 \end{gather}
 453
 454 \subsection{Conditions}
 455
 456 \[ \eqn{ Tip Merge }{
 457  L \in \py \implies
 458    \begin{cases}
 459       R \in \py : & \baseof{R} \ge \baseof{L}
 460               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 461       R \in \pn : & R \ge \baseof{L}
 462               \land M = \baseof{L} \\
 463       \text{otherwise} : & \false
 464    \end{cases}
 465 }\]
 466
 467 \subsection{No Replay}
 468
 469 See No Replay for Merge Results.
 470
 471 \subsection{Unique Base}
 472
 473 Need to consider only $C \in \py$, ie $L \in \py$,
 474 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 475 putative ancestor $A \in \pn$ and see whether $A \le C$.
 476
 477 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 478 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 479 Thus $A \le C \equiv A \le L \lor A \le R$.
 480
 481 By Unique Base of L and Transitive Ancestors,
 482 $A \le L \equiv A \le \baseof{L}$.
 483
 484 \subsubsection{For $R \in \py$:}
 485
 486 By Unique Base of $R$ and Transitive Ancestors,
 487 $A \le R \equiv A \le \baseof{R}$.
 488
 489 But by Tip Merge condition on $\baseof{R}$,
 490 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 491 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 492 Thus $A \le C \equiv A \le \baseof{R}$.
 493 That is, $\baseof{C} = \baseof{R}$.
 494
 495 \subsubsection{For $R \in \pn$:}
 496
 497 By Tip Merge condition on $R$,
 498 $A \le \baseof{L} \implies A \le R$, so
 499 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 500 Thus $A \le C \equiv A \le R$.
 501 That is, $\baseof{C} = R$.
 502
 503 $\qed$
 504
 505 \end{document}