\section{Commit annotation}

We annotate each Topbloke commit $C$ with:
\gathbegin
 \patchof{C}
\gathnext
 \baseof{C}, \text{ if } C \in \pay{C}
\gathnext
 \bigforall_{\p}
   \text{ either } C \haspatch \p \text{ or } C \nothaspatch \p
\gathnext
 \bigforall_{\py \not\ni C} \pendsof{C}{\py}
\end{gather}

$\patchof{C}$, for each kind of Topbloke-generated commit, is stated
in the summary in the section for that kind of commit.

Whether $\baseof{C}$ is required, and if so what the value is, is
stated in the proof of Unique Base for each kind of commit.

$C \haspatch \p$ or $\nothaspatch \p$ is represented as a
list of $\p$ for which it is known that $C \haspatch \p$;
for any $\p$ not listed, $C \nothaspatch \p$.
Whether to record $C \haspatch \p$ in a new commit
is in stated
(in terms of $I \haspatch \p$ or $I \nothaspatch \p$
for the ingredients $I$)
in the proof of Coherence for each kind of commit.

$\pendsof{C}{\py}$ is computed, for all Topbloke-generated commits,
using the lemma Calculation of Ends, above.
We do not annotate $\pendsof{C}{\pay{C}}$ for $C \in \pay{C}$.  Doing so would
make it wrong to make plain commits with git because the recorded $\pends$
would have to be updated.  The annotation is not needed in that case
because $\forall_{\pay{C} \ni C} \; \pendsof{C}{\pay{C}} = \{C\}$.

