Enhancements that could be made to the QVM testing framework

[fvoichick]

As Mike suggested, I'm creating a GitHub issue for things that could be done to improve QVM.

• A full proof of Grover's correctness with a single conjecture hole. Currently, there are SQIR proofs showing that Grover's algorithm is correct given oracle behavior, and there are QVM tests that validate oracle behavior. However, these are still somewhat disconnected. It would be nice if we had a full end-to-end proof that "this instantiation of Grover's algorithm inverts this hash function." This proof should depend on a single conjecture that is QuickChickable.
• Performant data types. Right now, the semantics of QVM are defined in terms of natural numbers and functional maps. Sometimes, natural numbers are used to represent values that will be very large, like an input number to an addition circuit. Whenever nat is used for a value that will be very large, and it's relevant to semantics or something that will be run in tests, then binary representations of numbers should be used, like N or positive. Functional maps can also eat up a lot of memory and time, so using FMaps for maps relevant to the semantics would be good. If we really want good performance, we could use positive instead of nat to represent variables, and then use PositiveMap.
• Testing at the QIMP level. We will definitely get much better testing performance if we can do things like addition using Coq functions rather than running circuits. However, we don't (yet) have verified compilation from QIMP to PQASM, so we won't be able to draw as many conclusions from testing results.
• Better utilities for automatically computing parameters to the various compilation and semantic functions. I found it very difficult to figure out what values should be in the maps that I'm passing to the various compilers, and the documentation is lacking. A lot of them can be automatically generated, and some clearer and simpler usage examples might be nice.
• Maybe part of the first one, but better reasoning about the relationship between PQASM semantics and SQIR semantics. Obviously, we have the verified compiler, and the verification of this compiler depends on this relationship already. However, it would be nice if PQASM semantics could be more directly translated into the kinds of propositions currently used in the proofs of correctness of algorithms.