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