VST
VST copied to clipboard
PrincetonUniversity
VST on Iris
@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.)
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.
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.
Aside from the 32-bit question, how fast is the performance of VST-Floyd in this branch, compared to the master branch?
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).
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).
Status update: Reduced the slowdown considerably. Some 8.18 tests still fail due to a bug (and 8.18.1 doesn't actually exist yet). I haven't made much progress on test5 (VSUs), but everything else is working.
My most recent commit c4a2d30 brings @lennartberinger's recent proofs about VSU dry safety into the vst_on_iris branch, all commented out. I wonder how difficult it will be to uncomment and port these to the vst_on_iris model.