simple.tex

   1 \section{Simple commit}
   2
   3 A simple single-parent forward commit $C$ as made by git-commit.
   4 \begin{gather}
   5 \tag*{} C \hasparents \{ L \} \\
   6 \tag*{} \patchof{C} = \patchof{L} \\
   7 \tag*{} D \isin C \equiv D \isin L \lor D = C
   8 \end{gather}
   9 This also covers Topbloke-generated commits on plain git branches:
  10 Topbloke strips the metadata when exporting.
  11
  12 \subsection{No Replay}
  13
  14 Ingredients Prevent Replay applies.  $\qed$
  15
  16 \subsection{Unique Base}
  17 If $L, C \in \py$ then by Calculation of Ends,
  18 $\pendsof{C}{\pn} = \pendsof{L}{\pn}$ so
  19 $\baseof{C} = \baseof{L}$. $\qed$
  20
  21 \subsection{Tip Contents}
  22 We need to consider only $L, C \in \py$.  From Tip Contents for $L$:
  23 \[ D \isin L \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L ) \]
  24 Substitute into the contents of $C$:
  25 \[ D \isin C \equiv D \isin \baseof{L} \lor ( D \in \py \land D \le L )
  26     \lor D = C \]
  27 Since $D = C \implies D \in \py$,
  28 and substituting in $\baseof{C}$, from Unique Base above, this gives:
  29 \[ D \isin C \equiv D \isin \baseof{C} \lor
  30     (D \in \py \land D \le L) \lor
  31     (D = C \land D \in \py) \]
  32 \[ \equiv D \isin \baseof{C} \lor
  33    [ D \in \py \land ( D \le L \lor D = C ) ] \]
  34 So by Exact Ancestors:
  35 \[ D \isin C \equiv D \isin \baseof{C} \lor ( D \in \py \land D \le C
  36 ) \]
  37 $\qed$
  38
  39 \subsection{Base Acyclic}
  40
  41 Need to consider only $L, C \in \pn$.
  42
  43 For $D = C$: $D \in \pn$ so $D \not\in \py$. OK.
  44
  45 For $D \neq C$: $D \isin C \equiv D \isin L$, so by Base Acyclic for
  46 $L$, $D \isin C \implies D \not\in \py$.
  47
  48 $\qed$
  49
  50 \subsection{Coherence and Patch Inclusion}
  51
  52 $$
  53 \begin{cases}
  54   L \haspatch    \p : & C \haspatch    \p \\
  55   L \nothaspatch \p : & C \nothaspatch \p
  56 \end{cases}
  57 $$
  58 \proofstarts
  59
  60 Firstly, if $L \haspatch \p$, $\exists_{F \in \py} F \le L$
  61 and this $F$ is also $\le C$
  62 so $C \zhaspatch \p \implies C \haspatch \p$.
  63 We will prove $\zhaspatch$
  64
  65 We need to consider $D \in \py$.
  66
  67 \subsubsection{For $L \haspatch \p, D = C$:}
  68
  69 Ancestors of $C$:
  70 $ D \le C $.
  71
  72 Contents of $C$:
  73 $ D \isin C \equiv \ldots \lor \true$.  So $ D \zhaspatch C $.
  74 OK.
  75
  76 \subsubsection{For $L \haspatch \p, D \neq C$:}
  77 Ancestors: $ D \le C \equiv D \le L $.
  78
  79 Contents: $ D \isin C \equiv D \isin L \lor f $
  80 so $ D \isin C \equiv D \isin L $, i.e. $ C \zhaspatch P $.
  81 OK.
  82
  83 \subsubsection{For $L \nothaspatch \p$:}
  84
  85 Firstly, $C \not\in \py$ since if it were, $L \in \py$.
  86 Thus $D \neq C$.
  87
  88 Now by $\nothaspatch$, $D \not\isin L$ so $D \not\isin C$.
  89 OK.
  90
  91 $\qed$
  92
  93 \subsection{Unique Tips:}
  94
  95 Single Parent Unique Tips applies.  $\qed$
  96
  97 \subsection{Foreign Inclusion:}
  98
  99 Simple Foreign Inclusion applies.  $\qed$
 100
 101 \subsection{Foreign Contents:}
 102
 103 Only relevant if $\patchof{C} = \bot$, and in that case Totally
 104 Foreign Contents applies. $\qed$
 105