[CN][Rocq] Lemma extraction doesn't support recursive definitions

[scuellar]

Summary

When translating CN lemmas to Coq it crashes on recursive definitions.

Bug

Extracting the lemmas described in the tutorial with

cn --lemmata=build-rocq/ExportedLemmas.v list_rev.c

Crashes with

./append.h:4:31: error: rec-def not yet handled:
append
function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
                              ^
converting pure lemma type: append_cons_r
./append.h:4:31: error: rec-def not yet handled:
append
function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
                              ^
./append.h:4:31: error: rec-def not yet handled:
append
function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
                              ^
./list_snoc_spec.h:2:31: error: rec-def not yet handled:
snoc
function [rec] (datatype seq) snoc(datatype seq xs, i32 y) {
                              ^
./append.h:4:31: error: rec-def not yet handled:
append
function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
                              ^

Indicating that translation of recursive definitions is not implemented.

The examples described in the tutorial uses multiple recursive definitions like append

/*@
function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
  match xs {
    Seq_Nil {} => {
      ys
    }
    Seq_Cons {head : h, tail : zs}  => {
      Seq_Cons {head: h, tail: append(zs, ys)}
    }
  }
}
@*/

Solution

Recursive functions should extract to Coq's fixpoint definitions.

version (commit)

commit 4dc961caa180beaff563356036461fcd1368e11c

[scuellar]

Simply replacing Definition with Fixpoint almost solves the issue with recursive definitions. The problem arises when Coq can't prove termination. That's not something CN checks so the user wouldn't find out until they try to run the Coq build process. I think that's a confusing place to receive an error about the generated code.

Here is a list of possibilities I have considered:

• Just generate Fixpoints and let Coq tell you when things don't obviously terminate. This seems like a bad design and confusing for the user, but it could be a starting point.
• Add a (simple!) CN termination check to catch the error early.
• Use Program Fixpoint and add termination proofs as obligations. I don't know a good way to generate the statements of these obligations other than calling Coq, so this can get complicated.

[bcpierce00]

Another intermediate point in the spectrum:

• Generate Fixpoint by default, but add an annotation on the CN side that causes it to generate a Program Fixpoint instead.

Seems like we should try just generating Fixpoints as a first step and see how far it gets us.

[cp526]

If one changes CN so it does not give up but generates a Fixpoint (or Program Fixpoint) for each recursive CN specification function, CN diverges.

Thomas S's best guess is that the reason for the divergence is CN's dependency handling in generating Coq lemmas: there is an "ensures-before" mechanism, whereby if CN tries to generate a definition it ensures it has produced definitions for all its dependencies. This may loop in the case of recursive definitions.

Two possible solutions are (1) to do a topological sort before the translation and drop the ensures-before mechanism or (2) to extend the ensures-before mechanism not to loop.

Will this produce sensible Coq output for mutually recursive CN functions or will those require more work?