The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hello Christopher,

Le 25/05/2021 à 01:21, Christopher Ernest Sally a écrit :
> Hi Club
>
> a finite data structure consisting of a map (from keys to elements) and 
> elements that contain (along with their own data) a key to a successor 
> element. Some elements have no successor key, indicating a kind of 
> "endpoint", resulting in DAGs. (actually, control-flow graphs).
>
> I want to write a recursive function over this data structure (but there 
> is no naive/obvious decreasing struct). I could use a fuel based 
> approach (# of elements as the bound) but wonder if that might hinder 
> any proofs I would later want to do over the function. I have not worked 
> much with Program before.
>
> Do people have experience with this, and any insights to the way forward?
>
> Bonus information:
> In fact, I am working with RTL from CompCert. (CompCert's pass out of 
> RTL is a validated pass i.e. the compiler code is in Ocaml and thus does 
> not provide an example) and the function is a translation of RTL code.


Actually, you will find examples of various approaches in CompCert.


1) The "fuel" approach:

For the "fuel" approach, look at Kildall, and in particular 
[fixpoint_from] function:

http://compcert.inria.fr/verasco/coqdoc/1.3/html/Kildall.html#Dataflow_Solver.fixpoint_from

It uses the "fuel" approach defined in the [PremIter] module:
http://compcert.inria.fr/verasco/coqdoc/1.3/html/Iteration.html#PrimIter

When you use this approach, you are in a kind of "partial correctness" 
setting: your fixpoint computation may fail on a "no fuel left error", 
and you prove properties only when the computation succeeds.

2) The "oracle" approach:

Thus, I often than an even simpler approach is to let an external oracle 
in OCaml compute the fixpoint and only program in Coq a verifier that 
checks that the result of the oracle is actually a fixpoint. This seems 
to me much modular, since you can tune/change the oracle without redoing 
any additional proof.

An example is provided by the register allocation, as you previously 
mentioned.

Another example is provided by my version of "branch tunneling" (on LTL, 
which is very similar to RTL):

https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx/html/compcert.backend.Tunneling.html

with the OCaml oracle here:

https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/compcert-kvx/-/blob/master/backend/Tunnelingaux.ml

This approach avoids the need to formalize in Coq a variant of 
union-find data-structure in contrast to Xavier Leroy's solution. In my 
approach, this data-structure is directly implemented in the above 
oracle, with imperative features of OCaml.

3) The "full correctness" approach, (with a termination proof):

An example is provided by [Postorder] (which computes a Postorder 
numbering on the graph):

https://compcert.org/doc/html/compcert.lib.Postorder.html

Regards,

Sylvain.