Uninformative message "cryptol error"

[msaaltink]

Here's a recent SAW error message, in full:

Symbolic simulation completed with side conditions.
user error ("include" (/proof/develop.saw:9:1-9:8):
"really_verify" (/proof/file1.saw:239:24-239:37):
"crucible_llvm_verify" (/proof/base.saw:46:5-46:25):
"tactic" (/proof/base.saw:46:55-46:61):
"unint_yices" (/proof/file2.saw:20:10-20:21):
cryptol error)

The command in question is a crucible llvm verification, the setup describes a call, with a postcondition of {{True}}. Or I can drop the postcondition and just have the crucible_execute_func end the setup.

The simulation appears to have completed, so what's the issue? Where might I look for a Cryptol error? Is there no way to SAW to provide some additional information about the error?

[brianhuffman]

The source of this error message is in the Cryptol saw-core prelude from the cryptol-verifier package, which provides saw-core implementations for cryptol's primitives.

saw/Cryptol.sawcore:ecError a len msg = error a "cryptol error"; -- FIXME: don't throw away message

So this is how the cryptol error primitive is encoded in saw-core. If you see "cryptol error" in an error message, that means that somewhere you must be calling "error" or "undefined" in some cryptol code.

[msaaltink]

OK, that's helpful: print_goal_consts is then a way to figure out what function it might be. Thanks.

[msaaltink]

Oddly enough, running simplify (cryptol_ss ()); before yices eliminates the error, and the proof succeeds. It makes sense in a way, as the definition of that function is immaterial to the subgoals (which were about overrides), but I wonder if that is supposed to happen.

[atomb]

I've improved the error message in the Cryptol -> SAWCore translation a bit. It's not a lot more informative, but should at least make it clearer that the source of the problem is a call to the error function in some Cryptol code.

[sauclovian-g]

Duplicate of #1326 (q.v.) which contains more info and has a draft patch.