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
 223 \section{Commit annotation}
 224
 225 We annotate each Topbloke commit $C$ with:
 226 \gathbegin
 227  \patchof{C}
 228 \gathnext
 229  \baseof{C}, \text{ if } C \in \py
 230 \gathnext
 231  \bigforall_{\pa{Q}}
 232    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
 233 \gathnext
 234  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 235 \end{gather}
 236
 237 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 238 make it wrong to make plain commits with git because the recorded $\pends$
 239 would have to be updated.  The annotation is not needed because
 240 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 241
 242 \section{Simple commit}
 243
 244 A simple single-parent forward commit $C$ as made by git-commit.
 245 \begin{gather}
 246 \tag*{} C \hasparents \{ A \} \\
 247 \tag*{} \patchof{C} = \patchof{A} \\
 248 \tag*{} D \isin C \equiv D \isin A \lor D = C
 249 \end{gather}
 250
 251 \subsection{No Replay}
 252 Trivial.
 253
 254 \subsection{Unique Base}
 255 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
 256
 257 \subsection{Tip Contents}
 258 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 259 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 260 Substitute into the contents of $C$:
 261 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 262     \lor D = C \]
 263 Since $D = C \implies D \in \py$,
 264 and substituting in $\baseof{C}$, this gives:
 265 \[ D \isin C \equiv D \isin \baseof{C} \lor
 266     (D \in \py \land D \le A) \lor
 267     (D = C \land D \in \py) \]
 268 \[ \equiv D \isin \baseof{C} \lor
 269    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 270 So by Exact Ancestors:
 271 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 272 ) \]
 273 $\qed$
 274
 275 \subsection{Base Acyclic}
 276
 277 Need to consider only $A, C \in \pn$.
 278
 279 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 280
 281 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 282 $A$, $D \isin C \implies D \not\in \py$. $\qed$
 283
 284 \subsection{Coherence and patch inclusion}
 285
 286 Need to consider $D \in \py$
 287
 288 \subsubsection{For $A \haspatch P, D = C$:}
 289
 290 Ancestors of $C$:
 291 $ D \le C $.
 292
 293 Contents of $C$:
 294 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 295
 296 \subsubsection{For $A \haspatch P, D \neq C$:}
 297 Ancestors: $ D \le C \equiv D \le A $.
 298
 299 Contents: $ D \isin C \equiv D \isin A \lor f $
 300 so $ D \isin C \equiv D \isin A $.
 301
 302 So:
 303 \[ A \haspatch P \implies C \haspatch P \]
 304
 305 \subsubsection{For $A \nothaspatch P$:}
 306
 307 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 308 Thus $D \neq C$.
 309
 310 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 311
 312 So:
 313 \[ A \nothaspatch P \implies C \nothaspatch P \]
 314 $\qed$
 315
 316 \subsection{Foreign inclusion:}
 317
 318 If $D = C$, trivial.  For $D \neq C$:
 319 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 320
 321 \section{Merge}
 322
 323 Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
 324 \gathbegin
 325  C \hasparents \{ L, R \}
 326 \gathnext
 327  \patchof{C} = \patchof{L}
 328 \gathnext
 329  D \isin C \equiv
 330   \begin{cases}
 331     (D \isin L \land D \isin R) \lor D = C : & \true \\
 332     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
 333     \text{otherwise} : & D \not\isin M
 334   \end{cases}
 335 \end{gather}
 336
 337 \subsection{Conditions}
 338
 339 \[ \eqn{ Tip Merge }{
 340  L \in \py \implies
 341    \begin{cases}
 342       R \in \py : & \baseof{R} \ge \baseof{L}
 343               \land [\baseof{L} = M \lor \baseof{L} = \baseof{M}] \\
 344       R \in \pn : & R \ge \baseof{L}
 345               \land M = \baseof{L} \\
 346       \text{otherwise} : & \false
 347    \end{cases}
 348 }\]
 349
 350 \subsection{No Replay}
 351
 352 \subsubsection{For $D=C$:} $D \isin C, D \le C$.  OK.
 353
 354 \subsubsection{For $D \isin L \land D \isin R$:}
 355 $D \isin C$.  And $D \isin L \implies D \le L \implies D \le C$.  OK.
 356
 357 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 358 $D \not\isin C$.  OK.
 359
 360 \subsubsection{For $D \neq C \land D \not\isin L \land D \not\isin R$:}
 361 $D \not\isin C$.  OK.
 362
 363 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 364  \land D \not\isin M$:}
 365 $D \isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
 366 R$ so $D \le C$.  OK.
 367
 368 \subsubsection{For $D \neq C \land (D \isin L \equiv D \not\isin R)
 369  \land D \isin M$:}
 370 $D \not\isin C$.  Also $D \isin L \lor D \isin R$ so $D \le L \lor D \le
 371 R$ so $D \le C$.  OK.
 372
 373 $\qed$
 374
 375 \end{document}