Functions scCryptolType and mkTypedTerm considered harmful

[brianhuffman]

Function scCryptolType from module Verifier.SAW.Cryptol in package cryptol-verifier should pretty much never be used. Nor should function mkTypedTerm from module Verifier.SAW.TypedTerm, or scCryptolEq from module Verifier.SAW.Cryptol, which are defined in terms of it.

The main problem is that scCryptolType can call error or panic if it is given a type that it cannot recognize as corresponding to a Cryptol type. The second problem is that it is supposed to be an inverse function to importType, which converts a Cryptol type to a saw-core term, but it's not: importType is not injective, so even if it works, it may return a different Cryptol type than the one you started with.

Unfortunately scCryptolType and especially mkTypedTerm are used in lots of places in saw-script. Every one of these uses is a potential bug or panic waiting to happen. We need to remove all of them.

[brianhuffman]

The fundamental reason why scCryptolType and mkTypedTerm are a problem is that the mapping from Cryptol types to saw-core types is not injective. Honestly, that is probably the real problem we should fix, especially considering issues like #878.

[robdockins]

Do we have a plan for addressing this?

Ultimately, I think the problem here is assuming that a Term always has a corresponding Cryptol type. I've run into a situation where I'd like to represent a tuple containing the arguments to a SAWCore function, but those arguments contain things that don't have corresponding Cryptol value types (Cryptol.Num, in particular).

Maybe we should just get rid of the TypedTerm construct altogether?

[robdockins]

See also #1248

[robdockins]

Or, perhaps less drastically, make TypedTerm basically have a Maybe Schema to recognize that some SAWCore terms don't make sense as Cryptol values.

[brianhuffman]

Yes, making TypedTerms have a Maybe Schema is something I've been thinking about for a while. It's definitely important for some TypedTerms (i.e. things of saw-script type Term) to have a cryptol type, so that we can refer to them from within cryptol syntax and use the cryptol type checker. But it makes sense to have terms with more general non-cryptol types too.

The other thing I want to do is make a new saw-core encoding of cryptol tuples and records (again) so that the mapping from cryptol types to saw-core types is injective. Instead of getting rid of scCryptolType and mkTypedTerm, the goal should be to make it so that we can implement them properly: For terms translated from cryptol, they should faithfully return the original cryptol type, and they should return a Maybe Schema so that they never need to panic or call error.

[robdockins]

OK, I think I'm going to take a crack at making TypedTerm appropriately partial, since that's what I need for the moment.

[brianhuffman]

Closing because avoiding scCryptolType and mkTypedTerm is not the right long-term approach in my opinion; we should just make them work correctly and return Maybe types. This will require fixing #1613.