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