inqwire / vqo Goto Github PK

Cleaning up the Coq code in QVM directory in the rcir-plus branch. Adding more comments, breaking definitions into different files. making sure definitions are understandable.

In the rcir-plus branch, currently, we allow quantum oracle definitions in PQASM/QIMP, and it is compiled to SQIR, and packed with the SQIR quantum algorithm definitions, and we learn the behaviors the whole program in SQIR. We want to flesh out the way to write a full algorithm, with quantum parts and the oracle, together. QuantumOne compilation via PQASM and SQIR.

QIMP language design improvements, so that functions are actually reusable. E.g., imagine writing out an implementation for multiplication in QIMP, rather than in Coq, and then reusing it in the implementation of sine.

https://arxiv.org/pdf/1711.10980.pdf

In QVM/rcir-plus, try to update PQASM to include some quantum entanglement features so that we are able to define most quantum walk oracles and Hamiltonian Simulation oracles. Then, we want to define Hamiltonian Simulation in PQASM and simulate it.

The proofs in QVM for different operations contain similar theorem proofs . We want to make proof more modular so that proofs of correctness of x+y and x+a and a+b can share much of the same underlying proof script.

The Coq generated Ocaml file causes stack overflow. One possible solution is to turn definitions in QVM to be tail recursions. Our goal is to generate circuits in the Coq generated Ocaml code for small QIMP programs. In rcir-plus branch.

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.

The current addition operations used in defining multiplication operations are from ripple-carry addition and QFT-based. The Quipper has a different addition implementation for multiplications. We want to also include that addition algorithm.