create-tip.tex

   1 \section{Create Tip}
   2
   3 Given a Topbloke base $B$ for a patch $\pq$,
   4 create a tip branch initial commit $C$.
   5 \gathbegin
   6  C \hasparents \{ B \}
   7 \gathnext
   8  \patchof{C} = \pqy
   9 \gathnext
  10  D \isin C \equiv D \isin B \lor D = C
  11 \end{gather}
  12
  13 \subsection{Conditions}
  14
  15 \[ \eqn{ Ingredients }{
  16  \patchof{B} = \pqn
  17 }\]
  18 \[ \eqn{ No Sneak }{
  19  \pendsof{B}{\pqy} = \{ \}
  20 }\]
  21
  22 \subsection{No Replay}
  23
  24 Ingredients Prevent Replay applies.  $\qed$
  25
  26 \subsection{Unique Base}
  27
  28 Trivially, $\pendsof{C}{\pqn} = \{B\}$ so $\baseof{C} = B$.  $\qed$
  29
  30 \subsection{Tip Contents}
  31
  32 Consider some arbitrary commit $D$.  If $D = C$, trivially satisfied.
  33
  34 If $D \neq C$, $D \isin C \equiv D \isin B$,
  35 which by Unique Base, above, $ \equiv D \isin \baseof{B}$.
  36 By Base Acyclic of $B$, $D \isin B \implies D \not\in \pqy$.
  37
  38
  39 $\qed$
  40
  41 \subsection{Base Acyclic}
  42
  43 Not applicable.
  44
  45 \subsection{Coherence and Patch Inclusion}
  46
  47 $$
  48 \begin{cases}
  49   \p = \pq    \lor B \haspatch \p : & C \haspatch \p \\
  50   \p \neq \pq \land B \nothaspatch \p : & C \nothaspatch \p
  51 \end{cases}
  52 $$
  53
  54 \proofstarts
  55 ~ Consider some $D \in \py$.
  56
  57 \subsubsection{For $\p = \pq$:}
  58
  59 By Base Acyclic, $D \not\isin B$.  So $D \isin C \equiv D = C$.
  60 By No Sneak, $D \not\le B$ so $D \le C \equiv D = C$.  Thus $C \zhaspatch \pq$.
  61 And we can set $F = C$ giving $F \in \pqy \land F \le C$ so $C
  62 \haspatch \pq$.
  63
  64 \subsubsection{For $\p \neq \pq$:}
  65
  66 $D \neq C$.  So $D \isin C \equiv D \isin B$,
  67 and $D \le C \equiv D \le B$.
  68
  69 $\qed$
  70
  71 \subsection{Unique Tips:}
  72
  73 Single Parent Unique Tips applies.  $\qed$
  74
  75 \subsection{Foreign Inclusion}
  76
  77 Simple Foreign Inclusion applies.  $\qed$
  78
  79 \subsection{Foreign Contents}
  80
  81 Not applicable.
  82