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