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