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