article.tex

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