Error handling

[weaversa]

Cryptol does not provide a standard way to handle error cases. Sure, most crypto functions are total, but not all. It would be good to come up with a way (perhaps using the current error keyword) to standardize how errors should be handled.

[yav]

Could you say a bit more about that? In particular, are you thinking of handling errors during verification (i.e., proving that error is never called), or do you mean some sort of error handling at run-time?

[weaversa]

Well, yes, it would be nice to handle errors during verification.

However, I was thinking along the lines of "Cryptol as a service". How do external tools operate with Cryptol functions that aren't total, or contain the error keyword? Sure, we can just say error "Error", but it would be nice to have, at the least, an idiomatic way to report errors, followed by some way to check for errors during run-time. Right now, when we hit the error keyword, we see a string containing the error text plus a Run-time error: prefix.

Some ideas --- Could we make another command to check for success in the interpreter? Could we massage the error prefix a bit to add more information about the error (such as file, line number, or function name)?

[yav]

OK, thanks, that makes sense. We can probably do a few different things on this front.

[LeventErkok]

Blast from the past: Cryptol-1 used to have a :safe command which found and flagged if any error calls were possible. (Or division by zero, index-out-of-bounds, etc.) I believe Cryptol-2 never implemented that functionality.

Truth be told, it wasn't the most useful command as most everything was obviously total, but was nice to have that command. And it's more or less free to implement since the symbolic-evaluator already kept track of all those cases and substituted zero if memory serves. All you have to do is to ask the proof backend to make sure the "path-condition" where you do the substitution is unsatisfiable. (If SAT, then the model gives you input values that can trigger the bad-behavior at run time.)

[robdockins]

@weaversa, what are your current thoughts about this issue? Is this primarily a REPL concern, or is this more a use case for the remote API?

Here's one idea we could do without too much trouble, I think. We can add a :status command that would reflect on the outcome of the previous interaction, and bind a record of data to the magic it variable. Or we could always set some designated variable with this information, similar to it. Or... we could make it configurable somehow.

I'm imagining something like:

> 5 + 6 : Integer
11
> :status 
{ ok = True, command = "eval" }
> error "asdf" : Integer

Run-time error: asdf
-- Backtrace --
Cryptol::error called at <interactive>:5:1--5:6

> :status
{ ok = False, command = "eval", msg = "Run-time error: asdf\n <etc>" } 
> let badTheorem = \x -> x == False
> :prove badTheorem
Counterexample
badTheorem True = False
(Total Elapsed Time: 0.006s, using "Z3")

> :status
{ ok = False, command = ":prove", property = "badTheorem" }

[weaversa]

Let's say the current cryptol-remote-api solves this and if I come up with a compelling issue I'll revisit.