Reorder the assumptions of corres_split rules

[corlewis]

This PR reorders the assumptions of the various corres_split rules, finishing the work started in https://github.com/seL4/l4v/pull/218.

The changes in this PR were produced first by a sequence of sed and perl commands, which are recorded in the commit messages, and then by manually going through the proofs and making updates as required. Almost all of these changes are reordering lines of proof after uses of the rules, and the updates to indentation that this requires.

While this is unfortunately a large amount of churn, my feeling is that in general it improves the proofs. In particular, there were many examples that followed a similar pattern to the following, where side conditions of rules would end up being solved in locations far away from the original rule application.

lemma f_corres: "f_assumption ==> corres ... f f'"

...
  apply (rule corres_split_deprecated[OF _ f_corres])
       ...
        ...
         ...
        ...
       ...
      apply (solve_f_assumption)

Following this PR, this example would look like

lemma f_corres: "f_assumption ==> corres ... f f'"

...
  apply (rule corres_split[OF f_corres])
       apply (solve_f_assumption)
      ...
       ...
        ...
       ...
      ...

There were also quite a lot of cases where previously the corres and wp parts of proofs were interleaved. It is now more common that all of the corres subgoals are dealt with in one block, before the wp section is reached.

lib/Corres_UL.thy is probably the only part of this PR that can be reasonably reviewed. The indentation changes in many of the other files has caused some confusing diffs, which will unfortunately also cause problems if these commits are merged or rebased over in the future.

[lsf37]

@michaelmcinerney it might make sense to do a test merge with MCS for this one to see if it leads to massive conflicts or not. Unless the perl/sed path is reasonably easily repeatable there. What do you think @corlewis?

Overall I agree that it does make the proofs nicer.

[corlewis]

I missed some changes required in crefine, all of the tests should pass now. I am a bit concerned that I am missing something with https://github.com/seL4/l4v/pull/526/commits/da1a7e8dc7b26f28983bef27d77a8c3cf4c94793, but it solves my specific problem, seems nicer in general and is consistent with the other architectures.

[corlewis]

@michaelmcinerney it might make sense to do a test merge with MCS for this one to see if it leads to massive conflicts or not. Unless the perl/sed path is reasonably easily repeatable there. What do you think @corlewis?

Overall I agree that it does make the proofs nicer.

We might get lucky, but based on my experience of applying the refine changes as a patch to other architectures, I'm pretty confident that it won't merge nicely. The large blocks of changed indentation can confuse things enough that some of the changes are seen as separate - and + chunks. This can result in a strange state where the - chunk isn't applied due to a conflict but the corresponding + chunk is still applied.

The actual changes required for this PR are generally pretty simple, there's just a lot of them. My guess for the best way to merge it with MCS would be to blindly do the merge, defaulting to taking what is on MCS in case of conflicts, and then reapply all of the sed commands. This would hopefully cover most of the cases, but we would then need to manually go through refine to update both the proofs that had conflicts and any new MCS proofs that require reordering.

It will of course depend on how bad the merge is and how many new MCS proofs need to be manually updated, but my guess is that this would take a couple of days of background work to go through.

[corlewis]

It took a bit longer than I hoped, but I now have a branch with an updated MCS. Is there anything blocking this PR being merged?

The gitlint test is failing due to the long lines in the commit bodies, which record the sed and perl commands used. Is it ok to leave these as is?