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
  63 \newcommand{\qed}{\square}
  64 \newcommand{\proof}[1]{{\it Proof.} #1 $\qed$}
  65
  66 \newcommand{\gathbegin}{\begin{gather} \tag*{}}
  67 \newcommand{\gathnext}{\\ \tag*{}}
  68
  69 \newcommand{\true}{t}
  70 \newcommand{\false}{f}
  71
  72 \begin{document}
  73
  74 \section{Notation}
  75
  76 \begin{basedescript}{
  77 \desclabelwidth{5em}
  78 \desclabelstyle{\nextlinelabel}
  79 }
  80 \item[ $ C \hasparents \set X $ ]
  81 The parents of commit $C$ are exactly the set
  82 $\set X$.
  83
  84 \item[ $ C \ge D $ ]
  85 $C$ is a descendant of $D$ in the git commit
  86 graph.  This is a partial order, namely the transitive closure of
  87 $ D \in \set X $ where $ C \hasparents \set X $.
  88
  89 \item[ $ C \has D $ ]
  90 Informally, the tree at commit $C$ contains the change
  91 made in commit $D$.  Does not take account of deliberate reversions by
  92 the user or reversion, rebasing or rewinding in
  93 non-Topbloke-controlled branches.  For merges and Topbloke-generated
  94 anticommits or re-commits, the ``change made'' is only to be thought
  95 of as any conflict resolution.  This is not a partial order because it
  96 is not transitive.
  97
  98 \item[ $ \p, \py, \pn $ ]
  99 A patch $\p$ consists of two sets of commits $\pn$ and $\py$, which
 100 are respectively the base and tip git branches.  $\p$ may be used
 101 where the context requires a set, in which case the statement
 102 is to be taken as applying to both $\py$ and $\pn$.
 103 All these sets are distinct.  Hence:
 104
 105 \item[ $ \patchof{ C } $ ]
 106 Either $\p$ s.t. $ C \in \p $, or $\bot$.
 107 A function from commits to patches' sets $\p$.
 108
 109 \item[ $ \pancsof{C}{\set P} $ ]
 110 $ \{ A \; | \; A \le C \land A \in \set P \} $
 111 i.e. all the ancestors of $C$
 112 which are in $\set P$.
 113
 114 \item[ $ \pendsof{C}{\set P} $ ]
 115 $ \{ E \; | \; E \in \pancsof{C}{\set P}
 116   \land \mathop{\not\exists}_{A \in \pancsof{C}{\set P}}
 117   A \neq E \land E \le A \} $
 118 i.e. all $\le$-maximal commits in $\pancsof{C}{\set P}$.
 119
 120 \item[ $ \baseof{C} $ ]
 121 $ \pendsof{C}{\pn} = \{ \baseof{C} \} $ where $ C \in \py $.
 122 A partial function from commits to commits.
 123 See Unique Base, below.
 124
 125 \item[ $ C \haspatch \p $ ]
 126 $\displaystyle \bigforall_{D \in \py} D \isin C \equiv D \le C $.
 127 ~ Informally, $C$ has the contents of $\p$.
 128
 129 \item[ $ C \nothaspatch \p $ ]
 130 $\displaystyle \bigforall_{D \in \py} D \not\isin C $.
 131 ~ Informally, $C$ has none of the contents of $\p$.
 132
 133 Non-Topbloke commits are $\nothaspatch \p$ for all $\p$; if a Topbloke
 134 patch is applied to a non-Topbloke branch and then bubbles back to
 135 the Topbloke patch itself, we hope that git's merge algorithm will
 136 DTRT or that the user will no longer care about the Topbloke patch.
 137
 138 \end{basedescript}
 139 \newpage
 140 \section{Invariants}
 141
 142 We maintain these each time we construct a new commit. \\
 143 \[ \eqn{No Replay:}{
 144   C \has D \implies C \ge D
 145 }\]
 146 \[\eqn{Unique Base:}{
 147  \bigforall_{C \in \py} \pendsof{C}{\pn} = \{ B \}
 148 }\]
 149 \[\eqn{Tip Contents:}{
 150   \bigforall_{C \in \py} D \isin C \equiv
 151     { D \isin \baseof{C} \lor \atop
 152       (D \in \py \land D \le C) }
 153 }\]
 154 \[\eqn{Base Acyclic:}{
 155   \bigforall_{B \in \pn} D \isin B \implies D \notin \py
 156 }\]
 157 \[\eqn{Coherence:}{
 158   \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p
 159 }\]
 160 \[\eqn{Foreign Inclusion:}{
 161   \bigforall_{D \text{ s.t. } \patchof{D} = \bot} D \isin C \equiv D \leq C
 162 }\]
 163
 164 \section{Some lemmas}
 165
 166 \[ \eqn{Exclusive Tip Contents:}{
 167   \bigforall_{C \in \py}
 168     \neg \Bigl[ D \isin \baseof{C} \land ( D \in \py \land D \le C )
 169       \Bigr]
 170 }\]
 171 Ie, the two limbs of the RHS of Tip Contents are mutually exclusive.
 172
 173 \proof{
 174 Let $B = \baseof{C}$ in $D \isin \baseof{C}$.  Now $B \in \pn$.
 175 So by Base Acyclic $D \isin B \implies D \notin \py$.
 176 }
 177 \[ \corrolary{
 178   \bigforall_{C \in \py} D \isin C \equiv
 179   \begin{cases}
 180     D \in \py : & D \le C \\
 181     D \not\in \py : & D \isin \baseof{C}
 182   \end{cases}
 183 }\]
 184
 185 \[ \eqn{Tip Self Inpatch:}{
 186   \bigforall_{C \in \py} C \haspatch \p
 187 }\]
 188 Ie, tip commits contain their own patch.
 189
 190 \proof{
 191 Apply Exclusive Tip Contents to some $D \in \py$:
 192 $ \bigforall_{C \in \py}\bigforall_{D \in \py}
 193   D \isin C \equiv D \le C $
 194 }
 195
 196 \[ \eqn{Exact Ancestors:}{
 197   \bigforall_{ C \hasparents \set{R} }
 198   D \le C \equiv
 199     ( \mathop{\hbox{\huge{$\vee$}}}_{R \in \set R} D \le R )
 200     \lor D = C
 201 }\]
 202
 203 \[ \eqn{Transitive Ancestors:}{
 204   \left[ \bigforall_{ E \in \pendsof{C}{\set P} } E \le M \right] \equiv
 205   \left[ \bigforall_{ A \in \pancsof{C}{\set P} } A \le M \right]
 206 }\]
 207
 208 \proof{
 209 The implication from right to left is trivial because
 210 $ \pends() \subset \pancs() $.
 211 For the implication from left to right:
 212 by the definition of $\mathcal E$,
 213 for every such $A$, either $A \in \pends()$ which implies
 214 $A \le M$ by the LHS directly,
 215 or $\exists_{A' \in \pancs()} \; A' \neq A \land A \le A' $
 216 in which case we repeat for $A'$.  Since there are finitely many
 217 commits, this terminates with $A'' \in \pends()$, ie $A'' \le M$
 218 by the LHS.  And $A \le A''$.
 219 }
 220
 221 \section{Commit annotation}
 222
 223 We annotate each Topbloke commit $C$ with:
 224 \gathbegin
 225  \patchof{C}
 226 \gathnext
 227  \baseof{C}, \text{ if } C \in \py
 228 \gathnext
 229  \bigforall_{\pa{Q}}
 230    \text{ either } C \haspatch \pa{Q} \text{ or } C \nothaspatch \pa{Q}
 231 \gathnext
 232  \bigforall_{\pay{Q} \not\ni C} \pendsof{C}{\pay{Q}}
 233 \end{gather}
 234
 235 We do not annotate $\pendsof{C}{\py}$ for $C \in \py$.  Doing so would
 236 make it wrong to make plain commits with git because the recorded $\pends$
 237 would have to be updated.  The annotation is not needed because
 238 $\forall_{\py \ni C} \; \pendsof{C}{\py} = \{C\}$.
 239
 240 \section{Simple commit}
 241
 242 A simple single-parent forward commit $C$ as made by git-commit.
 243 \begin{gather}
 244 \tag*{} C \hasparents \{ A \} \\
 245 \tag*{} \patchof{C} = \patchof{A} \\
 246 \tag*{} D \isin C \equiv D \isin A \lor D = C
 247 \end{gather}
 248
 249 \subsection{No Replay}
 250 Trivial.
 251
 252 \subsection{Unique Base}
 253 If $A, C \in \py$ then $\baseof{C} = \baseof{A}$. $\qed$
 254
 255 \subsection{Tip Contents}
 256 We need to consider only $A, C \in \py$.  From Tip Contents for $A$:
 257 \[ D \isin A \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A ) \]
 258 Substitute into the contents of $C$:
 259 \[ D \isin C \equiv D \isin \baseof{A} \lor ( D \in \py \land D \le A )
 260     \lor D = C \]
 261 Since $D = C \implies D \in \py$,
 262 and substituting in $\baseof{C}$, this gives:
 263 \[ D \isin C \equiv D \isin \baseof{C} \lor
 264     (D \in \py \land D \le A) \lor
 265     (D = C \land D \in \py) \]
 266 \[ \equiv D \isin \baseof{C} \lor
 267    [ D \in \py \land ( D \le A \lor D = C ) ] \]
 268 So by Exact Ancestors:
 269 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
 270 ) \]
 271 $\qed$
 272
 273 \subsection{Base Acyclic}
 274
 275 Need to consider only $A, C \in \pn$.
 276
 277 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
 278
 279 For $D \neq C$: $D \isin C \equiv D \isin A$, so by Base Acyclic for
 280 $A$, $D \isin C \implies D \not\in \py$. $\qed$
 281
 282 \subsection{Coherence and patch inclusion}
 283
 284 Need to consider $D \in \py$
 285
 286 \subsubsection{For $A \haspatch P, D = C$:}
 287
 288 Ancestors of $C$:
 289 $ D \le C $.
 290
 291 Contents of $C$:
 292 $ D \isin C \equiv \ldots \lor \true \text{ so } D \haspatch C $.
 293
 294 \subsubsection{For $A \haspatch P, D \neq C$:}
 295 Ancestors: $ D \le C \equiv D \le A $.
 296
 297 Contents: $ D \isin C \equiv D \isin A \lor f $
 298 so $ D \isin C \equiv D \isin A $.
 299
 300 So:
 301 \[ A \haspatch P \implies C \haspatch P \]
 302
 303 \subsubsection{For $A \nothaspatch P$:}
 304
 305 Firstly, $C \not\in \py$ since if it were, $A \in \py$.
 306 Thus $D \neq C$.
 307
 308 Now by contents of $A$, $D \notin A$, so $D \notin C$.
 309
 310 So:
 311 \[ A \nothaspatch P \implies C \nothaspatch P \]
 312 $\qed$
 313
 314 \subsection{Foreign inclusion:}
 315
 316 If $D = C$, trivial.  For $D \neq C$:
 317 $D \isin C \equiv D \isin A \equiv D \le A \equiv D \le C$.  $\qed$
 318
 319 \section{Merge}
 320
 321 Given commits $L$, $R$, $M$:
 322 \gathbegin
 323  C \hasparents \{ L, R \}
 324 \gathnext
 325  \patchof{C} = \patchof{L}
 326 \gathnext
 327  D \isin C \equiv
 328   \begin{cases}
 329     (D \isin L \land D \isin R) \lor D = C : & \true \\
 330     (D \not\isin L \land D \not\isin R) \land D \neq C : & \false \\
 331     \text{otherwise} : & D \not\isin M
 332   \end{cases}
 333 \end{gather}
 334
 335 Conditions
 336 \gathbegin
 337  M < L, M < R
 338 \end{gather}
 339
 340 \end{document}