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        \Bigl\{ 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        \Bigr\}
 257 }\]
 258 XXX proof TBD.
 259
 260 \subsection{No Replay for Merge Results}
 261
 262 If we are constructing $C$ such that $\merge{C}{L}{M}{R}$, No Replay
 263 is preserved.  {\it Proof:}
 264
 265 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 266
 267 \subsubsection{For $D \isin L \land D \isin R$:}
 268 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
 269
 270 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 271 $D \not\isin C$.  OK.
 272
 273 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 274 $D \not\isin C$.  OK.
 275
 276 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 277  \land D \not\isin M$:}
 278 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
 279 R$ so $D \le C$.  OK.
 280
 281 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 282  \land D \isin M$:}
 283 $D \not\isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
 284 R$ so $D \le C$.  OK.
 285
 286 $\qed$
 287
 288 \section{Commit annotation}
 289
 290 We annotate each Topbloke commit $C$ with:
 291 \gathbegin
 292  \patchof{C}
 293 \gathnext
 294  \baseof{C}, \text{ if } C \in \py
 295 \gathnext
 296  \bigforall_{\pa{Q}}
 297    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
 298 \gathnext
 299  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 300 \end{gather}
 301
 302 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 303 make it wrong to make plain commits with git because the recorded $\pends$
 304 would have to be updated.  The annotation is not needed because
 305 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 306
 307 \section{Simple commit}
 308
 309 A simple single-parent forward commit $C$ as made by git-commit.
 310 \begin{gather}
 311 \tag*{} C \hasparents \{ A \} \\
 312 \tag*{} \patchof{C} = \patchof{A} \\
 313 \tag*{} D \isin C \equiv D \isin A \lor D = C
 314 \end{gather}
 315
 316 \subsection{No Replay}
 317 Trivial.
 318
 319 \subsection{Unique Base}
 320 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
 321
 322 \subsection{Tip Contents}
 323 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 324 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 325 Substitute into the contents of $C$:
 326 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 327     \lor D = C \]
 328 Since $D = C \implies D \in \py$,
 329 and substituting in $\baseof{C}$, this gives:
 330 \[ D \isin C \equiv D \isin \baseof{C} \lor
 331     (D \in \py \land D \le A) \lor
 332     (D = C \land D \in \py) \]
 333 \[ \equiv D \isin \baseof{C} \lor
 334    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 335 So by Exact Ancestors:
 336 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 337 ) \]
 338 $\qed$
 339
 340 \subsection{Base Acyclic}
 341
 342 Need to consider only $A, C \in \pn$.
 343
 344 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 345
 346 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 347 $A$, $D \isin C \implies D \not\in \py$. $\qed$
 348
 349 \subsection{Coherence and patch inclusion}
 350
 351 Need to consider $D \in \py$
 352
 353 \subsubsection{For $A \haspatch P, D = C$:}
 354
 355 Ancestors of $C$:
 356 $ D \le C $.
 357
 358 Contents of $C$:
 359 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 360
 361 \subsubsection{For $A \haspatch P, D \neq C$:}
 362 Ancestors: $ D \le C \equiv D \le A $.
 363
 364 Contents: $ D \isin C \equiv D \isin A \lor f $
 365 so $ D \isin C \equiv D \isin A $.
 366
 367 So:
 368 \[ A \haspatch P \implies C \haspatch P \]
 369
 370 \subsubsection{For $A \nothaspatch P$:}
 371
 372 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 373 Thus $D \neq C$.
 374
 375 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 376
 377 So:
 378 \[ A \nothaspatch P \implies C \nothaspatch P \]
 379 $\qed$
 380
 381 \subsection{Foreign inclusion:}
 382
 383 If $D = C$, trivial.  For $D \neq C$:
 384 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 385
 386 \section{Anticommit}
 387
 388 Given $L, R^+, R^-$ where
 389 $\patchof{R^+} = \pry, \patchof{R^-} = \prn$.
 390 Construct $C$ which has $\pr$ removed.
 391 Used for removing a branch dependency.
 392 \gathbegin
 393  C \hasparents \{ L \}
 394 \gathnext
 395  \patchof{C} = \patchof{L}
 396 \gathnext
 397  \merge{C}{L}{R^+}{R^-}
 398 \end{gather}
 399
 400 \subsection{Conditions}
 401
 402 \[ \eqn{ Unique Tip }{
 403  \pendsof{L}{\pry} = \{ R^+ \}
 404 }\]
 405 \[ \eqn{ Correct Base }{
 406  \baseof{R^+} = R^-
 407 }\]
 408 \[ \eqn{ Currently Included }{
 409  L \haspatch \pry
 410 }\]
 411
 412
 413
 414 xxx want to prove $D \isin C \equiv D \not\in \pry \land D \isin L$.
 415
 416 \section{Merge}
 417
 418 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 419 \gathbegin
 420  C \hasparents \{ L, R \}
 421 \gathnext
 422  \patchof{C} = \patchof{L}
 423 \gathnext
 424  \merge{C}{L}{M}{R}
 425 \end{gather}
 426
 427 \subsection{Conditions}
 428
 429 \[ \eqn{ Tip Merge }{
 430  L \in \py \implies
 431    \begin{cases}
 432       R \in \py : & \baseof{R} \ge \baseof{L}
 433               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 434       R \in \pn : & R \ge \baseof{L}
 435               \land M = \baseof{L} \\
 436       \text{otherwise} : & \false
 437    \end{cases}
 438 }\]
 439
 440 \subsection{Merge Results}
 441
 442 As above.
 443
 444 \subsection{Unique Base}
 445
 446 Need to consider only $C \in \py$, ie $L \in \py$,
 447 and calculate $\pendsof{C}{\pn}$.  So we will consider some
 448 putative ancestor $A \in \pn$ and see whether $A \le C$.
 449
 450 By Exact Ancestors for C, $A \le C \equiv A \le L \lor A \le R \lor A = C$.
 451 But $C \in py$ and $A \in \pn$ so $A \neq C$.
 452 Thus $A \le C \equiv A \le L \lor A \le R$.
 453
 454 By Unique Base of L and Transitive Ancestors,
 455 $A \le L \equiv A \le \baseof{L}$.
 456
 457 \subsubsection{For $R \in \py$:}
 458
 459 By Unique Base of $R$ and Transitive Ancestors,
 460 $A \le R \equiv A \le \baseof{R}$.
 461
 462 But by Tip Merge condition on $\baseof{R}$,
 463 $A \le \baseof{L} \implies A \le \baseof{R}$, so
 464 $A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
 465 Thus $A \le C \equiv A \le \baseof{R}$.
 466 That is, $\baseof{C} = \baseof{R}$.
 467
 468 \subsubsection{For $R \in \pn$:}
 469
 470 By Tip Merge condition on $R$,
 471 $A \le \baseof{L} \implies A \le R$, so
 472 $A \le R \lor A \le \baseof{L} \equiv A \le R$.
 473 Thus $A \le C \equiv A \le R$.
 474 That is, $\baseof{C} = R$.
 475
 476 $\qed$
 477
 478 \end{document}