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