The Coq mailing list

[Andrew Appel <appel AT princeton.edu>]

[correction:  the "Coq Platform" (coq + external packages) is not yet available for MacOS, only for Windows.  On MacOS, "How to get VST" is through opam.]

Release announcement:  

Verified Software Toolchain, version 2.6,  and

Software Foundations Volume 5:  Verifiable C

Verifiable C is a program logic based on higher-order separation logic for the C programming language.  Users work interactively in Coq to verify their C programs (as parsed by the front end of CompCert), applying "symbolic execution" proof-automation tactics.  VST is proved sound with respect to the operational semantics of CompCert Clight -- so if you compile the rest of the way with CompCert you get a machine-checked guarantee that the assembly language program conforms to the functional specification you proved.  But you can also compile with gcc or clang, and it's compatible (though not provably).

VST comes with three forms of documentation:

1.  Reference manual, VC.pdf, distributed with the release and also available here.

2.  Tutorial introduction with exercises, published as Volume 5 of the Software Foundations series.

3.  Many worked examples, available in the progs directory of the standard installation; additional examples in the sha,aes,hmac-drbg,mailbox, and other directories of the git repository.

How to get VST:

1. VST comes packaged with the Windows installer for the Coq 8.12.0 release -- perhaps you already have it!  Require Import VST.floyd.proofauto.

2. Or,  opam install coq-vst.2.6

3. Or,  download from github:   https://github.com/PrincetonUniversity/VST/releases/tag/v2.6 and read BUILD_ORGANIZATION.md for instructions.

New in VST, over the last year or two, are:

• Tutorial introduction with exercises, leading up to the "capstone exercise" of verifying a hash table with external chaining.  See  Software Foundations Volume 5:  Verifiable C, by Appel and Cao, 2020.
• Funspec subtyping and subsumption, for a more modular calculus of linking C modules and functions together.  See   Abstraction and Subsumption in Modular Verification of C Programs, by Beringer and Appel, revised and extended version of a FM 2019 paper.
• Proofs about input/output, using the "interaction trees" model, with the ability to do foundational verification of I/O system-calls. See  Connecting Higher-Order Separation Logic to a First-Order Outside World, by Mansky, Honoré, and Appel, ESOP 2020.
• Modular verification of modular programs: an improved system for linking the specifications/verifications of .c files.  Described in the Abstraction and Subsumption paper, see also the progs/pile directory of the distribution. (We should really document this better for users; expect better documentation of the linking system in the next release.)
• Better support for verification of C programs that use floating point.  See C-language floating-point proofs layered with VST and Flocq, by Appel and Bertot, July 2020.
• Improved proof automation, especially for array- and list- and sequence-manipulating programs, by Qinshi Wang.
• Opam and Coq-Platform easy-install, by Michael Soegtrop (see above, "How to get VST").
  

Other changes:

In release 2.6 (2 August 2020):  

Improved support for floating point proofs (described above).

Coq Platform and Opam (described above)

Adapted to Coq 8.11 and Coq 8.12; avoid most deprecated features.

Adapted to CompCert 3.7.

Improved support for funspec subsumption (described above).

New WITH notation for funspecs: instead of

    WITH ... PRE[ ] PROP...LOCAL...SEP POST [] PROP...LOCAL...SEP

  it is now,

    WITH ... PRE[ ] PROP...PARAMS...GLOBALS...SEP POST [] PROP...RETURNS...SEP

Improved some error messages.

Improved the list_solve and Zlength_solve tactics.

Fix issues #209 #270 (cancel tactic), #347 (typo in hint), #379 (sizeof, alignof), #232 #343 #407 (improve error messages), #363 (start_function efficency), #419 (forward_while), #420 (improve reference manual).

Many other small improvements.

Put "fash" notation in Module to avoid notation pollution.

Reasoning about "store integer field of union, load float" and vice versa.

In release 2.5 (8 January 2020):  

Support for proving connections to first-order external APIs  (see also this).

Funspec subsumption (see above).

Improved proof automation for sequences and arrays (improved "list_solve" tactic).

Put backtick notation in a Module for compatibility with other libraries that have their own notations.

Fix issues #321 (forward_for_simple_bound), #324 (error message), #332 (error message), #377 (incomplete typechecking long-integer negation).

Performance improvements in Floyd tactics.

In defining Gprogs, "with_library" no longer needed in most cases.

Soundness proof now based directly on CompCert Clight, instead of 2 layers via "Clight_new" semantics.

Avoid Coq features deprecated in Coq 8.10.

Experimental, nonfoundational support for printf and fprintf.

In release 2.4 (23 April 2019):  

Improved error messages in forward and forward_call.

Improved hints in "hint" tactic.

Minor improvements in "cancel" tactic.

Entailer no longer does "simpl", better preserving the form of user's conjuncts.

Updates for compatibility with latest Coq release.

Improved sep_apply, new tactics ecancel, EExists.

Respecification of i/o API using (I-Tree) monads.

Demonstration of i/o system calls with memory-buffer arguments.

Improved gather_SEP tactic notation using pattern arguments.

64-bit configurations of C now as robust as 32-bit configurations.

Update VST to CompCert 3.5.