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