Updates to Cryptol Monadification (+ add qsort to saw-core)

[m-yac]

This PR mainly makes the following changes to Cryptol Monadification:

• Add a write_coq_cryptol_module_monadic command which monadifies all definitions in a Cryptol module and writes them to a Coq file
• Always monadify all contained constants, recursively (this was partially implemented before, but it did not always find all contained constants – see 37ba742)
• Write CryptolM.sawcore to a Coq file in generate_scaffolding.saw
• Resolve all remaining FIXMEs in CryptolM.sawcore. This mostly involved the mostly mechanical task of translating the Cryptol.sawcore definitions into the SpecM monad (which I did while waiting for things to compile) but also involved adding an uncurryMacro and generalizing the finMacro in Monadify.hs

However, it also adds a new type of sort, qsort, to saw-core. Like the existing isort, it is ignored during saw-core typechecking, but when translated to Coq adds an implicit typeclass argument. For isort this is the Inhabited typeclass, but for qsort this is the QuantType typeclass (needed for the existsS combinator and the CryptolM functions that use it, such as vecMapM and the number functions that in turn use that). This involved:

• Replacing the Bool in the Sort constructor of FlatTermF (which differentiated sort vs. isort) with a new record type SortFlags, which has two Bools: flagInhabited and flagQuantType.
• Updating the typed and untyped ASTs as well as the external format to account for replacing this Bool with this new type
• Updating the Lexer and Grammar to add the new qsort and qisort keywords
• Updating many places where the default False value for the old Bool flag was used with the new noFlags value of the record where all fields are False

An advantage of making a new SortFlags type instead of just adding another Bool flag is that in the future if we want to add another such flag, it should only involve adding a new field to SortFlags, updating the Coq translation, and updating the Lexer and Grammar. The changes to the external format as well as the many places False was replaced with noFlags should not need to happen again.

[eddywestbrook]

My initial thought is that I don't think we want an exponential explosion of different kinds of sorts. That is, we don't want isort, qsort, and also qisort, because that adds complexity that we don't need. Instead, the purpose of all of these is really just to express that a type comes from Cryptol. So let's have a single name that expresses that, i.e., why not just call it crysort. Let's also have a single typeclass in Coq as well, maybe called CryptolType, that has all the functionality we need for a Cryptol type. For now that's just that it's Inhabited and is a QuantType, but in the future it might be more, and this way we can just add to the CryptolType class and not change SAW core at all rather than having to add yet another Bool flag to sort.

[m-yac]

@eddywestbrook Oh, sorry for misunderstanding you! The worry I have with always bundling QuantType and Inhabited is that sometimes we might want to quantify over a Prop which we don't know is inhabited. If we weren't able to separate the two, this would force us to only use existsS over Props which we can prove are Inhabited. I feel like I can imagine a situation where the Inhabited-ness of a Prop we're quantifying over depends on the value of variables from earlier in the monadic term. Maybe this isn't a problem in practice, though? What are your thoughts on this

[eddywestbrook]

@m-yac I see your concern, and we certainly wouldn't want to existsS on a Prop that must be Inhabited because the Inhabited proof is a proof of that Prop! However, we already expose a separate assertS combinator in SAW, that does exactly what you are talking about, using existsS over Props. But it does that "under the hood", on the Coq side. So the solution would be to use existsS when quantifying over "actual data", in the form of Cryptol types, and to use assertP to quantify over Props (which always trivially satisfy QuantType). How does that sound?

[m-yac]

Update: We realized what we really want here is some sort of typeclass system in saw-core (#1845). At least, that was the best solution we could think of that was equally as easy to use as the current solution of having special sorts. Based on Eddy's comment we could simplify the hierarchy a little bit by making qsort imply isort, but we're just going to leave this as-is.

[eddywestbrook]

This mostly looks great! Please perform the small doc changes I requested. I'll mark as "approve" assuming that you'll make those changes and merge yourself.