The Coq mailing list

[Andrew Appel <appel AT cs.princeton.edu>]

I hereby announce the release of:

• VST 2.10 (July 2022)
• VST 2.11 (August 2022)
• VST 2.11.1 (December 2022).  As usual since 2020, the best way to install VST is through the Coq Platform.  That ensures your versions of VST, CompCert, and Coq are all compatible.
• Iris-in-VST, a new library by William Mansky allowing Iris-style concurrency and invariant reasoning (and Iris Proof Mode) in VST.  See description below.  Iris-in-VST is not yet part of the Coq Platform, you can install it as the opam package coq-vst-iris.

For a list of what's new in VST 2.10 / 2.11 / 2.11.1, see the CHANGES file.

---

Iris in VST (by William Mansky)

Iris is a Higher-Order Concurrent Separation Logic Framework, implemented and verified in Coq, based on a step-indexed model abstracted via modal operators. 

VST is a Higher-Order Concurrent Separation Logic for C, implemented and verified in Coq, based on a step-indexed model abstracted via modal operators.

Iris has many attractive features:  an elegant and well-designed internal model, a powerful logical system for reasoning about ghost state of concurrent programs, Iris Proof Mode (IPM) for convenient tactical reasoning in the modal logic.

VST has many attractive features:  a proved-sound program logic for almost the whole C language; a powerful proof automation system (Verifiable C) for applying the program logic to C programs via symbolic execution; Verified Software Units for modular verification of modular programs.

Why not have the best of both worlds, and use Iris's ghost-state reasoning system (with Iris Proof Mode) for reasoning about concurrent C programs!  One obstacle might be:  the underlying semantic models, while based on similar principles, are quite different.  But logic steps in to save us:  Iris abstracts its model into a logic with operators and inference rules;  VST abstracts its model into a logic with operators and inference rules; and the two logics are compatible enough to be able to use IPM and Iris's ghost-state features on top of VST.

 

The new release of Iris-in-VST includes a significant expansion of the Iris and Iris-inspired features available in VST, intended especially for verifying fine-grained concurrent programs. Available features include:

• MoSeL (Iris Proof Mode) integration – use the iIntros tactic on any entailment to switch into Iris mode, and then use any Iris tactics to prove the goal.
• Custom ghost state – any separation algebra can be used as ghost state in a program. In this version, ghost state is affine, and can be freely dropped at any point in a proof.
• Invariants and fancy updates – resources can be put into global invariants at any point in a program; resources in invariants can be accessed between steps and by atomic operations.
• Persistent assertions – invariants, snapshots, and other “information”-type ghost state can be declared persistent, and persistent resources are automatically duplicated as needed when using Iris tactics.
• Logically atomic specifications – functions can be verified against logically atomic specifications, proving that they appear to take effect at a single point in time. Our lock implementation is now verified against a TaDA-style atomic specification.

 

Ghost state, invariants, fancy updates, and atomic operations are foundational extensions to VST and are available without installing Iris. To use the features that directly integrate Iris infrastructure and tactics, you will need to install Iris. If installing VST through OPAM, you can install the package coq-vst-iris (which depends on both coq-vst and coq-iris) to enable all features. The tutorial in doc/concurrency.pdf walks through most of the new features; for more information, see the Iris documentation or contact William Mansky <mansky1 AT uic.edu>.