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