chiark / gitweb /
 author Ian Jackson Fri, 16 Mar 2012 23:14:18 +0000 (23:14 +0000) committer Ian Jackson Fri, 16 Mar 2012 23:14:18 +0000 (23:14 +0000)
 invariants.tex patch | blob | history lemmas.tex patch | blob | history

index 25d51c5..ab03491 100644 (file)
@@ -13,7 +13,7 @@ We maintain these each time we construct a new commit. \\
(D \in \py \land D \le C) }
}\]
$\eqn{Base Acyclic:}{ - \bigforall_{B \in \pn} D \isin B \implies D \notin \py + \bigforall_{C \in \pn} D \isin C \implies D \notin \py }$
$\eqn{Coherence:}{ \bigforall_{C,\p} C \haspatch \p \lor C \nothaspatch \p @@ -25,3 +25,10 @@ We maintain these each time we construct a new commit. \\ \bigforall_{C \text{ s.t. } \patchof{C} = \bot} D \le C \implies \patchof{D} = \bot }$
+
+A commit $C$ which satisfies all of the above is said to be
+conformant''.
+
+For each operation we will perform which generates a new commit, we
+will assume the conformance of the existing history and prove the
+conformance of the new commit.
index aeb6564..7d72e54 100644 (file)
@@ -54,7 +54,7 @@ So by Base Acyclic $D \isin B \implies D \notin \py$.
}\]

\subsection{Tip Self Inpatch}
-Given Exclusive Tip Contents and Base Acyclic for $C$,
+Given Base Acyclic for $C$,
$$\bigforall_{C \in \py} C \haspatch \p \land \neg[ C \nothaspatch \p ]$$
@@ -126,6 +126,7 @@ Otherwise, $E$ meets all the conditions for $\pends$.
}

\subsection{Ingredients Prevent Replay}
+Given conformant commits $A \in \set A$,
$$\left[ {C \hasparents \set A} \land @@ -142,12 +143,13 @@$$
$$\proof{ Trivial for D = C. Consider some D \neq C, D \isin C. - By the preconditions, there is some A s.t. D \in \set A + By the preconditions, there is some A s.t. A \in \set A and D \isin A. By No Replay for A, D \le A. And A \le C so D \le C. } \subsection{Simple Foreign Inclusion} +Given a conformant commit L,$$
\left[
C \hasparents \{ L \}
@@ -169,6 +171,7 @@ So $D \isin C \equiv D \le C$.
}

\subsection{Totally Foreign Contents}
+Given conformant commits $A \in \set A$,

\left[
C \hasparents \set A \land