Create opam release of coq-vst.3.0beta1

[andrew-appel]

This is VST 3.0beta1.

VST 3.x is "VST on Iris", a rebuild of VST's core logic in the generic Iris framework. This means that most of msl no longer exists, veric has been rebuilt as a more maintainable and extensible logic, and it is possible to freely use Iris theorems and tactics in VST proofs. The top-level guarantee is exactly the same as in VST 2.x: soundness w.r.t. the operational semantics of CompCert Clight. See also: https://doi.org/10.1145/3632848

Key new features include:

1. Support for Iris typeclasses and Iris Proof Mode (IPM). Predicates can be proved Persistent, Absorbing, etc., and then automatically handled accordingly in IPM. At any entailment, you can use iIntros to enter Iris Proof Mode. For details on Iris Proof Mode, see the Iris documentation (https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/proof_mode.md). It is also possible to rewrite with both entailments and equivalences, as an alternative to using derives_trans or sep_apply to modify part of a separation logic assertion.

2. Full support for Iris ghost state (rather than the "Iris-style ghost state" of previous versions). Any Iris resource algebra can be used as ghost state after adding a thin wrapper (see ora/theories/algebra/frac_auth.v and progs64/verif_incr_gen.v). Ghost state can be discarded at any time, while memory resources are still treated linearly.

3. A compatibility mode, available by importing VST.floyd.compat. This hides Iris-related boilerplate and restores the notation and lemmas of VST 2.x, so that existing proofs will largely work as is. There are a few incompatibilities; proofs that use ghost state or external state (e.g., I/O via ITrees) cannot use compat, and proofs that manually manipulate entailment clauses with sepcon_assoc and sepcon_comm may break (but they're more easily proved with IPM anyway). For a full list of known incompatibilities and advice on porting, see PORTING.md [hyperlink this file].

4. Installation instructions: coq-vst.3.0+beta1 in the coq-released archive, or fetch the v3.0beta1 release from VST and build it in Coq 8.18-8.19 with CompCert 3.13.1 ...

5. It is likely that VST 2.x will be supported only until 2025, perhaps up to VST 2.16, in parallel with releases of VST 3.x. Release 2.14 of VST, compatible with Coq 8.17-8.19 and CompCert 3.13.1, was recently released and will soon be available via the Coq Platform 2024 release for Coq 8.19.

[mansky1]

This depends on a dev version of Iris from iris-dev, so it can't currently pass the CI. Does that mean we need to host it through iris-dev rather than here?

[andrew-appel]

@mansky1 and I have tentatively decided to suspend this P.R. until an Iris release is available for Coq 8.19, which @RalfJung says should happen by the end of April 2024. At that time we will update the P.R. to refer to the Iris release instead of iris-dev.

[RalfJung]

An Iris release compatible with Coq 8.19 is now waiting to be published at https://github.com/coq/opam/pull/3015.

[RalfJung]

Also I am quite excited to see this release, and I am curious what the future will bring now that porting proofs between Iris-based projects and VST should be practical. :)

[robbertkrebbers]

Like Ralf I am also excited about this! Great Job to the VST team!

[mansky1]

There's some kind of issue with the path to the git submodule. I'll do some debugging and see why it works in our CI but not in opam.

[mansky1]

Okay, it should be ready!

[andrew-appel]

@silene or any other maintainer: As @mansky1 wrote, this P.R. is now ready to be merged. Thank you.