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