CI Workflow

Terminology

So, to ground our discussion about CI workflows, we'll need some terminology. To start, we have two repos with the following commit references:

Target Repo	Branch/Commit Ref	Data Source	Description
evm-semantics	master	evm-semantics git history	primary branch
evm-semantics	evm-pointer	git-tracked file in revm	evm-semantics master tracking branch
revm	pi2-release	revm git history	primary branch

There are three cases of PRs to consider. Without loss of generality, we will pick branch names to illustrate each case.

Case #	Description	Branch Name(s)
1	modifies evm-semantics only	evm-semantics:feat
2	modifies revm only	revm:feat
3	modifies both evm-semantics and revm	evm-semantics:shared-feat, revm:shared-feat

To name the commit generated by merging a PR into a branch b, we'll write b' (pronounced b prime).

We'll also need some predicates on Git commit references. Suppose r:a and r:b are commit references for the same Git repo r. When it's clear from context, we'll drop the repo name r. Then let:

r:a = r:b denote that the two commits are equal, i.e., they are two references to the same commit hash
r:a != r:b denote that the two commits are unequal, i.e., they have different commit hashes
r:a < r:b denote that a is an ancestor of b such that a != b
r:a <= r:b denote that either a < b or a = b
r:a ~ r:b denote that commits a and b have identical contents (even though their commit hashes may be different)

Definitions

I argue that correctness of my proposed CI workflow boils down to the following claim:

Central Claim: for every new commit on evm-semantics:master, there exists some commit on revm:pi2-release where evm-semantics:evm-pointer ~ evm-semantics:master.

Before proceeding, you should check whether you agree with the central claim --- because for the rest of this snippet, I will assume that this claim is valid.

Our CI workflow itself is defined by two predicates CI_EVM() and CI_REVM() which captures the permitted relationships between the various commit references:

CI_EVM(evm-semantics:master, evm-semantics:feat, revm:pi2-release, evm-semantics:evm-pointer) :=
```
master < feat && feat = evm-pointer
```
CI_REVM(revm:pi2-release, revm:feat, evm-semantics:master, evm-semantics:evm-pointer, evm-semantics:evm-pointer') :=
```
tests_pass( feat, evm-pointer' ) &&
[ ( master < evm-pointer <= evm-pointer' ) ||
  ( evm-pointer' <= master && evm-pointer = evm-pointer' && master ~ evm-pointer' ) ]
```
where a < b <= c is an abbreviation for a < b && b <= c && a < c

Note that:

we let evm-pointer be the value of the evm-semantics commit stored on commit revm:pi2-release while evm-pointer' is the value of the evm-semantics commit stored on some PR branch revm:feat (which may or may not be equal to evm-pointer);
the commit ref evm-pointer will not exist on revm:pi2-release before the first revm feature branch revm:feat which defines it is merged --- in cases where a commit-ref doesn't exist, we assume that any constraint it participates in is trivially true (i.e. non-existent-ref = some-ref is assumed true).
The constraint that evm-semantics:master < evm-semantics:feat and evm-semantics:master < evm-semantics:evm-pointer' is designed to ensure that we can always perform fast-forwards when updating evm-semantics and avoid the complexity of non-trivial merge commits.

CI Workflow Commit Graph Preservation

We first prove a property about how our CI workflow preserves git commit graphs of a certain shape. We will show that, if continously applied, starting from a commit graph of shape (A) or (B) defined below, our CI workflow will always remain in commit graphs of shapes (A), (B), or (C) --- also defined below. Then we use that preservation property to prove the central claim.

Base Case

In particular, we assert that we begin with one of the two following cases:

(A) An evm-semantics commit graph tip of the following form:
```
-A              (master)
  \
   `-B-.....-C  (evm-pointer')
```
where the ..... represents any number of commits between B and C (including the case where B == C). We have only an evm-pointer' at this point, since only branch revm:feat has a pointer (this is when the pointer was first added). At this point, we know that CI_REVM may be able to run successfully, since constraint

master < evm-pointer <= evm-pointer'

is satisfied because:
- we assume equalities with undefined values (in this case, evm-pointer) trivially hold and;
- we have master < evm-pointer'
(B) An evm-semantics commit graph tip of the following form:
```
-A         (master, evm-pointer')
```
At this point, we know that CI_REVM may be able to run successfully, since:
- constraint master ~ evm-pointer' by definition
- constraint evm-pointer' <= master is satisfied since evm-pointer' = master
- since evm-pointer doesn't exist, so we consider evm-pointer = evm-pointer' to be trivially satisfied.

At this starting point, we assert that we applied CI_REVM successfully, so that the value of evm-pointer is set for the first time.

Then, for our next step, we will either want to run CI_EVM or CI_REVM again.

Step 2 - CI_EVM

Suppose we now run CI_EVM.

If we were in case (B), there is nothing to be done for evm-semantics --- and we remain in case (B).

Thus, assume we were in case (A). We now need to update evm-semantics and must apply workflow CI_EVM. To apply it, we must setup a PR branch, which in general, has the following form:

-A-.....-C    (master)
  \
   `-D        (feat)

However, we know that, for this to pass, we must have: feat = evm-pointer. Thus, in the passing case, we must have B=D and A=C and thus we have:

-A         (master)
  \
   `-B     (feat, evm-pointer)

By assumption, master < evm-pointer', from the prior step, we have master < evm-pointer now, as required. But this means we will either: perform a useless non-fast-forward merge (or) fast-forward. Thus, we will obtain one of the following commit graph shapes:

In the useless non-fast-forward merge case we have:
```
-A---*---D   (master')
  \     /
   `-B-'     (feat, evm-pointer)
```
Note that, By definition, such merges have the property that B ~ D and thus evm-pointer ~ master'. Let's call this graph shape (C).
In the fast-forward case, we obtain:
```
-A---B   (master', feat, evm-pointer)
```
But note that, this shape is isomorphic to case (B).

Step 2 - CI_REVM

Instead, at step 2, we could have run CI_REVM again. Now, either the evm-pointer will be updated or it won't be:

If the evm-pointer is not updated, then we will fall into one of the two original cases.

If we started in case (A), we now have:
```
-A         (master)
  \
   `-B     (evm-pointer, evm-pointer')
```
But then we satisfy master < evm-pointer <= evm-pointer', as required.

If we started in case (B), we now have:
```
-A         (master, evm-pointer, evm-pointer')
```
This then satisfies evm-pointer = evm-pointer' && master ~ evm-pointer && evm-pointer <= master
If the evm-pointer is updated, then we can only fall into a variation of case A, since case B would satisfy constraint evm-pointer <= master but our assumption that evm-pointer is updated contradicts evm-pointer = evm-pointer'. Thus, our graph tip will look like:
```
-A                          (master)
  \
   `-B-.....-C              (evm-pointer)
              \
               `-D-.....-E  (evm-pointer')
```
This then satisfies the constraints master < evm-pointer <= evm-pointer'. But note that this graph shape falls again into case A, since we didn't make any assumptions about the number of commits between master and evm-pointer.

Final Step

We have already shown that, starting from case (A) or (B), CI_REVM always remains in case (A) or (B).

Similarly, we have shown that, starting form case (A) or (B), CI_EVM will reach case (B) or (C).

Thus, it is enough to show that, starting from case (C), both CI_REVM and CI_REVM remain in cases (A), (B), or (C). So, suppose our commit graph starts from shape (C):

-A---*---D   (master)
  \     /
   `-B-'     (evm-pointer)

where B ~ D, by definition.

To apply CI_EVM, we must create a commit feat that satisfies the constraints master < feat && feat = evm-pointer. But this contradicts our graph which has master > feat = evm-pointer.

Thus, we can only apply CI_REVM. Then, we either update evm-pointer or we do not.

If we do not update evm-pointer, we will have the graph:

-A---*---D   (master)
  \     /
   `-B-'     (evm-pointer, evm-pointer')

But this precisely satisfies evm-pointer = evm-pointer' && master ~ evm-pointer && evm-pointer <= master. Thus, we remain in case (C).

If we update evm-pointer, the only possible passing case in predicate CI_REVM has the form master < evm-pointer <= evm-pointer'. Since we updated evm-pointer, we must have master < evm-pointer < evm-pointer'. Thus, our graph must have the shape:

            E-.....-F (evm-pointer')
           /
-A---*---D'           (master)
  \     /
   `-B-'              (evm-pointer)

But this is now another form of shape (A).

Central Claim Proof

Now that we know that, starting from shapes (A) or (B), our CI workflow will infinitely generate graphs of the form (A), (B), or (C). To prove the central claim holds, we must show that, for each commit to evm-semantics:master, there was a corresopnding commit to evm-semantics:evm-pointer such that evm-pointer ~ master. And this will be the case as long as we fairly apply CI_EVM and CI_REVM, so that we continously generate graph shapes (B) and (C) --- and do not infinitely remain in shape (A), where we extend the evm-pointer branch without updating evm-semantics:master.

sskeirik/ci-argument.md