write_coq_cryptol_module generates functions with needlessly complicated types

[RyanGlScott]

I was recently stumped when trying to use write_coq_cryptol_module. Here is a greatly minimized way to reproduce the issue. Take these Cryptol and SAW files:

// dup.cry
dup : [64] -> [2][64]
dup x = [x, x]

// dup.saw
enable_experimental;

write_coq_cryptol_module
  "dup.cry" "dup_gen.v"
  [] [];

As well as this _CoqProject file:

-Q . Test
dup_gen.v

And run the following:

$ coq_makefile -f _CoqProject -o Makefile
$ saw dup.saw
$ make dup_gen.vo

Next, try loading the following Coq proof that uses the generated Coq code:

Require Import Test.dup_gen.

Definition app {a b} : (a -> b) -> a -> b :=
  fun f x => f x.

Check app dup.

Surprisingly, the call to app dup will fail to typecheck!

The term "dup" has type
 "forall
    x : CryptolPrimitivesForSAWCore.CryptolPrimitivesForSAWCore.seq
          (CryptolPrimitivesForSAWCore.CryptolPrimitivesForSAWCore.TCNum 64) bool,
  Vector.t
    (CryptolPrimitivesForSAWCore.CryptolPrimitivesForSAWCore.seq
       (CryptolPrimitivesForSAWCore.CryptolPrimitivesForSAWCore.TCNum 64) bool)
    (length (x :: x :: nil))" while it is expected to have type
 "CryptolPrimitivesForSAWCore.CryptolPrimitivesForSAWCore.seq
    (CryptolPrimitivesForSAWCore.CryptolPrimitivesForSAWCore.TCNum 64) bool -> 
  ?b" (cannot instantiate "?b" because "x" is not in its scope).

I was baffled by this error message until I saw what the type of dup was in Coq:

> Check dup.

dup
     : forall
         x : CryptolPrimitivesForSAWCore.CryptolPrimitivesForSAWCore.seq
               (CryptolPrimitivesForSAWCore.CryptolPrimitivesForSAWCore.TCNum 64) bool,
       Vector.t
         (CryptolPrimitivesForSAWCore.CryptolPrimitivesForSAWCore.seq
            (CryptolPrimitivesForSAWCore.CryptolPrimitivesForSAWCore.TCNum 64) bool)
         (length (x :: x :: nil))

Somehow, dup's return type is dependent on its argument! As a result, the error message about is complaining that the x in forall x is escaping its scope. Gah.

What's worse, there is really no need for this dependency. In fact, you can work around the issue by defining a copy of dup with a non-dependent type:

Definition dup_copy : VectorDef.t bool 64 -> VectorDef.t (VectorDef.t bool 64) 2 :=
  dup.

And that version can be passed to app without issue:

> Check app dup_copy.

app dup_copy
     : VectorDef.t bool 64 -> VectorDef.t (VectorDef.t bool 64) 2

This workaround shouldn't be necessary, however. The only reason that Coq infers a dependent type for dup is because the generated code code omits an explicit return type:

  Definition dup (x : CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum 64) Coq.Init.Datatypes.bool)  :=
    Vector.of_list [x; x].

If the generated code had given it an explicit return type of, say, CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum 2) (CryptolPrimitivesForSAWCore.seq (CryptolPrimitivesForSAWCore.TCNum 64) Coq.Init.Datatypes.bool), then this issue wouldn't have happened in the first place. We can see that the Cryptol-to-Coq machinery is already generated the argument types, so I propose that it generate the return type as well.

[eddywestbrook]

Whoa, that is wild. I did some digging (I'm waiting for a compile, so didn't have anything else to do), and the reason it has that type is because the SAW core to Coq translator is using Vector.of_list to translate the SAW core array value, which has type

forall l : list ?A, t ?A (length l)

I think you are right, that we should probably generate expected output types, but actually a much simpler fix for this particular issue would be to change the Coq translator here to use a Coq vector literal. This would also be a more direct translation anyway, rather than constructing an intermediate list value. Ironically, the same Coq.List AST constructor should work for this, without applying Vector.of_list, since the Coq notation is the same, and the vector notation is in scope by default in the environment we set up in Coq modules generated by the translator. I'll try it out...

[eddywestbrook]

Ooh, important point: in order to write a test for this (why don't we have any Coq translator integration tests?!), we need to change the CI to install Coq as its own CI step, rather than just as part of the heapster-tests action...

[RyanGlScott]

Yes, using Coq's vector literals would certainly improve things. That being said, I still think that the inferred return type would be something like Vector.t (seq (TCNum 64) bool) 2). Arguably, the return type should be explicitly set to seq (TCNum 2) (seq (TCNum 64) bool) so that it consistently uses seq throughout, rather than inconsistently using Vector.t and seq in different places.

[eddywestbrook]

Well, we could certainly add a type ascription, but the fact is that those two types are convertible, so it shouldn't break any type-checking like your example above did. I think the real question is whether we are viewing the generated Coq as human-readable or only machine-readable. If the latter, then this issue doesn't really matter, but you're right, if it's the former then an explicit seq type would be more uniform. I'm inclined to view it as machine-readable, as we have been doing so far, but I'm open to the idea of adding the type ascription.

Maybe the right answer is to add the output type at the top level of each definition, like you suggested earlier? This makes sense if we are viewing the Coq code itself as only machine-readable, but are viewing the types of things that are generated as something a human might look at, e.g., using Check dup like you did.

[RyanGlScott]

Indeed, I am currently working on a project where I, a human, am inspecting the types of these generated functions :)

It's true that a machine is generating these, so to some extent, these types will never be as pretty as they could be be. But adding an explicit return type would be a very simple way to improve the readability. In fact, we're already being explicit with the argument types, so we ought to be explicit about the return types if for no other reason than consistency.

[eddywestbrook]

Yep, I agree about the explicit return type. I'm working on that right now.

[RyanGlScott]

Fixed in #1815.