The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT univ-grenoble-alpes.fr>]

Hello Christopher,

In addition you may be interested in the Braga method,
which precisely targets situations where you want to write recursive
functions without a priori knowledge on termination (including
the type of the termination certificate).
Without fuel.
A draft version of the (to be soon published) long description is here:
https://members.loria.fr/DLarchey/files/papers/the_braga_method.pdf

Regards,
Jean-Francois

On Tue, May 25, 2021 at 08:31:47AM -0700, Christopher Ernest Sally wrote:
>    Dear Sylvain
>    Ah, thank you for those excellent pointers! Indeed, I had forgotten all
>    about the analyses.
>    Cordialement
>    Chris
>    On Mon, 24 May 2021 at 23:48, Sylvain Boulmé
>    <[1]Sylvain.Boulme AT univ-grenoble-alpes.fr> wrote:
> 
>      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:
> 
>      
> [2]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:
>      
> [3]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):
> 
>      
> [4]https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx/html/compcert.backend.Tunneling.html
> 
>      with the OCaml oracle here:
> 
>      
> [5]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):
> 
>      [6]https://compcert.org/doc/html/compcert.lib.Postorder.html
> 
>      Regards,
> 
>      Sylvain.
> 
> References
> 
>    Visible links
>    1. mailto:Sylvain.Boulme AT univ-grenoble-alpes.fr
>    2. 
> http://compcert.inria.fr/verasco/coqdoc/1.3/html/Kildall.html#Dataflow_Solver.fixpoint_from
>    3. 
> http://compcert.inria.fr/verasco/coqdoc/1.3/html/Iteration.html#PrimIter
>    4. 
> https://certicompil.gricad-pages.univ-grenoble-alpes.fr/compcert-kvx/html/compcert.backend.Tunneling.html
>    5. 
> https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/compcert-kvx/-/blob/master/backend/Tunnelingaux.ml
>    6. https://compcert.org/doc/html/compcert.lib.Postorder.html

-- 
Jean-Francois Monin
Verimag
Universite Grenoble Alpes