MCS CRefine sorried for RISCV64

[michaelmcinerney]

This sorries the last files in the CRefine session, thereby completing the setup of the proof infrastructure for MCS CRefine.

In addition, this enables testing of the CRefine session via our continuous integration setup.

[Xaphiosis]

Looking at the commits for now:

The "update copyright" commit (no tags, no explanantion), at least the CRefine parts look like they should be folded into the sorrying run. Not sure about the lib part.

For the "rt crefine: finish sorrying run", I know I lost the battle about indicating in the tags that this is only for RISCV64, but maybe I could get a comment in the body of the commit, as it's quite a large commit?

For the run_tests and Makefile changes, why are they tagged "rt:", these are not rt specific. The first should say "run_tests: enable CRefine for RISCV64". The second is misleading, as it's RISCV64 only, and also not rt-specific; I'd suggest Gerwin-styled "riscv64 proofs: turn on quick_and_dirty for CRefine".

[Xaphiosis]

rt: update the sorrying-run to seL4 revision 4214775 commit is also crefine-only and not tagged as such. Also for consistency, it's "sorrying run" in one commit and "the sorrying-run" in the next.

The run_tests change is still not tagged with run_tests.

I'm trying to push you a bit towards more consistency with the rest of the repo. In future, if you're doing a change to run_tests or something, can you look at a few past commits with git log run_tests or whatever to see what they look like and try fit in with that rather than invent something new on the spot? It'll really cut down on the amount of these discussions, which I know you probably don't like, and I don't enjoy pointing these out either, believe it or not.

Similarly for the manifest commit, if you do git log mcs.xml you'll see what the previous ones look like, usually something like mcs: bump seL4 revision, whereas yours says rt: update seL4 for MCS testing to current master ... what MCS testing, what does that mean? There's no rt: branch on the manifest repo, and previous commits are tagged mcs:...

[lsf37]

Alright, the commit messages are cleaned up and the content has been good the entire time already, so that is also fine.

Thanks for diligently adding new lemmas for all of the new MCS functions, this makes the sorry-count much more useful.