I wrote a very brief OVERVIEW.md to say in the most basic way what CertiGraph is for. But I am sure that CertiGraph has many other interesting capabilities that I don't know about. One or more of the CertiGraph authors should expand OVERVIEW.md by another page or two, to describe what else you can do with CertiGraph.

1. There is a bug in the specification of the garbage collector: it does not permit no-scan objects (tag >= NO_SCAN_TAG) to have even numbers in its fields. That is, it insists that all fields be tagged integers, when the purpose of no-scan is to permit untagged data.

2. There is a bug in the implementation of the garbage collector. In the forward function, where it says,

        if (depth>0)
          for (i=0; i<sz; i++)
            forward(from_start, from_limit, next, &Field(newv,i), depth-1);

it should say instead:

        if (depth>0)
	  if (!No_scan(Tag_hd(hd)))
          for (i=0; i<sz; i++)
            forward(from_start, from_limit, next, &Field(newv,i), depth-1);

The only change is an extra if-statement.

This bug has been in there from the beginning, and the only reason we didn't notice it is that it requires both depth>0 (which we rarely test) and primitive no-scan objects (which we haven't much tested).

The bug was found during the verification, when I generalized the specification of the G.C. to address point 1 above.

Issue: CertiGraph is not a public repo, and now it's ready to be, so I suggest: make it so!

But first: remove mention of VST from the LICENSE file. You may have needed that when CertiGraph's predecessor was installed as a component of VST, but now they are separable (either by git subrepos or by opam), so you don't need that part of the LICENSE file. And if you want to be even smoother about it, paste in a version of the MIT license (if that's what you're using) that's so exact that github recognizes it as "MIT license" -- which will make things even more clear.

On the main repo page, at right, github has a "license" symbol, and if it can detect that you are using a standard license it will (1) name that license right there, and (2) add that to its database.

https://github.blog/2016-09-21-license-now-displayed-on-repository-overview/

Although CertiGraph is using the MIT license, it's not word-for-word the same, because of the first paragraph that's about VST. That first paragraph is unnecessary, because VST is no longer included within the CertiGraph distribution.

I suggest it would be a good idea to make the license recognizable to github's license-detector, to the point where it displays the license-name automatically. That is, delete the paragraph about VST, and paste the standard MIT license in word-for-word, editing only the copyright line to put in the names of the three or four principal authors.

CertiGraph ought to be able to build in the standard Coq Platform installation of VST. Right now, that build of VST does not include the file VST.msl.msl_direct. That msl_direct is still in the VST repo, but it is not in the opam-build configuration.

For now I will try disabling such files as CertiGraph/msl_ext/overlapping_direct.v form the makefile. But if msl/msl_direct is important to CertiGraph, then I suggest you file a VST issue report requesting that msl_direct be added to the make targets in VST/util/calc_install_files

I suggest that the URLs for finding the papers in the readme should be to their definitive DOIs, especially because they are open-access at those locations:

https://doi.org/10.1007/978-3-030-81688-9_37
https://doi.org/10.1145/3360597

The "mark" demo, in the mark subdirectory,

1. Needs a Makefile and a _CoqProject
2. Should build independently of the main repo, just as the "demo" subdirectory does
3. Should probably be merged into the demo directory, which would then have two .c files, one a tree-traversal and one a depth-first-search

In conventional mathematical terminology, "bigraph" is short for "bipartite graph". Within CertiGraph, "biGraph" appears to mean "binary graph", that is, a graph where every nontrivial node has 2 out-edges. This is unnecessarily confusing. I suggest you rename the module, and all the relevant files. Perhaps binGraph and demo/mark_bin.c, et cetera.

In the current live branch, such as 1be5141, it appears that the continuous integration does not work.

Someone with "owner" access to this repo should click the gear-wheel next to "About" and add the following repository-description text, which I just copied from the README.

A library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.

CertiGraph should be brought up to date with respect to the Coq Platform 2022.04 for Coq 8.15.1. That means VST 2.9.1, CompCert 3.10.

I don't think this will be very difficult.
The first issue I notice is that instead of VST.floyd.sublist you should now refer to VST.zlist.sublist.

I was trying to build CertiGraph. But build fails with the following

File ".//CertiGC/verif_forward1.v", line 164, characters 74-77:
Error: The variable H19 was not found in the current environment.

I am on the latest commit 786e7ed
of branch "live"

Recent changes in Coq and in VST broke some things in CertiGraph.
Recently I fixed core CertiGraph and also got CertiGC working again, at least in 64-bit mode (maybe also 32-bit mode? Can't remember).

But dijkstra and perhaps some of the other application demos are broken in Coq 8.15/8.16 with VST 2.11. Can someone bring them up to date?