-
Notifications
You must be signed in to change notification settings - Fork 62
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
write_coq_cryptol_module
generates functions with needlessly complicated types
#1813
Comments
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
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 |
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 |
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 |
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 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 |
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. |
Yep, I agree about the explicit return type. I'm working on that right now. |
Fixed in #1815. |
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:As well as this
_CoqProject
file:And run the following:
Next, try loading the following Coq proof that uses the generated Coq code:
Surprisingly, the call to
app dup
will fail to typecheck!I was baffled by this error message until I saw what the type of
dup
was in Coq:Somehow,
dup
's return type is dependent on its argument! As a result, the error message about is complaining that thex
inforall 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: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.The text was updated successfully, but these errors were encountered: