Revised semantics for errors

[brianhuffman]

@robdockins and I have been thinking about changing the denotational semantics for error values in cryptol for quite some time. Currently the reference interpreter says that error values (things like DivideByZero or OutOfBounds or ⊥) only exist at base types (e.g. Bit and Integer). But this design makes it very tricky to implement certain partial operations correctly, for example indexing operators like @. (See #422.)

We'd like to change the semantic domains to include error values at every type, not just at base types. This should make it easier to implement an efficient evaluator that also agrees with the reference interpreter. It should also make it easier to eventually implement a :safe command (#284) because it will make it simpler to specify whether an expression denotes an error.

[yav]

It would be nice to still support an implementation technique where arrays are "exploded" into individual elements (i.e., eta expanded). Not sure if allowing errors everywhere interferes with that or not, but it seems like a worthwhile use case to support.

[robdockins]

We revised the reference semantics in #866 along these lines, and it now agrees much more closely with the actual behavior of the REPL interpreter. The main interpreter still does not agree in some cases with the reference semantics, but all the cases I know about are related to the special handling of bitvector values.

[robdockins]

I believe this is now complete, as of #1136