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