VST on Iris

[mansky1]

Replaced MSL with Iris, rebuilt VeriC and Floyd on top of it.

[mansky1]

@andrew-appel I'm now working on getting this to pass the CI -- it currently works only for 8.17 and 64-bit mode. Which Coq versions and bitsizes does it need to pass? (I'd prefer not to have to support 8.16, if that makes sense.)

[andrew-appel]

Not necessary to support 8.16. If you can support 8.18 and newer, that will be good enough for any release AFTER April of 2024, which will (presumably) be for a Coq Platform for Coq 8.20.

[andrew-appel]

But please do support 32-bit mode.

[mansky1]

Okay! It looks like the main obstacle to supporting 32-bit mode will simply be maintaining all of the examples -- list_dt is messy and hasn't been touched in years, and there are a bunch of other examples that aren't in 64-bit and aren't quite trivial to port. I'll do as many as I can in the next few weeks, but I'd love to know if there are any programs in progs that don't really need to be in the CI.

[andrew-appel]

Aside from the 32-bit question, how fast is the performance of VST-Floyd in this branch, compared to the master branch?

[mansky1]

The slowdown on the CI tests is between 0% and 60%. At the level of individual tactics, forward is sometimes equal or faster, sometimes 3-4x slower. Most of the remaining slowdown is from autorewrite (esp. in normalize). I can't tell how much of that is inevitable and how much could be improved, because I have no idea how to get diagnostics on autorewrite (basically I want this but it seems not to have happened).

[mansky1]

By the way, it looks like this anomaly is crashing some of my tests on Coq 8.18.0 specifically. It appears to be fixed in 8.18.1, but I don't know how to change the CI to test on that instead (just changing 8.18 to 8.18.1 in coq-action.yml didn't work).

[andrew-appel]

I have just done some very small updates to the VST master branch, tagged as release v2.15. It is probably worth merging master into vst_on_iris, and I expect that this won't cause you any problems (since you were already up to date as of August 2024 if I recall correctly).