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