Kesha Hietala

Move Shor proofs to a separate repository

4

It would be cleaner to have the Shor proof (currently in `examples/shor`) in a separate repository. It is the largest application of SQIR, aside from VOQC, and it has different...

The two main proofs in [examples/shor/Main.v](https://github.com/inQWIRE/SQIR/tree/main/examples/shor/Main.v) are currently `end_to_end_shors_correct` which says that end_to_end_shors returns a factor (or nothing) and `end_to_end_shors_fails_with_low_probability` which says that it returns a factor with probability poly-log...

Improve circuit mapping

1

Sophisticated mapping routines (e.g. that use error-aware heuristics to find the best path through a graph) are likely tricky to implement and verify in Coq, so we may want to...

To describe a physical-to-logical qubit association for circuit mapping, we use an ad hoc pair of a `nat -> nat` map and its inverse (see the `layout` type in [Layouts.v](https://github.com/inQWIRE/SQIR/blob/main/VOQC/Layouts.v))....

In the VOQC directory, [uc_well_typed_l](https://github.com/inQWIRE/SQIR/blob/main/VOQC/UnitaryListRepresentation.v#L52) and [respects_constraints](https://github.com/inQWIRE/SQIR/blob/main/VOQC/MappingConstraints.v#L9) should be written in terms of [forall_gates](https://github.com/inQWIRE/SQIR/blob/main/VOQC/StandardGateSet.v#L758).

We define a larger gate set for SQIR in [ExtractionGateSet.v](https://github.com/inQWIRE/SQIR/blob/main/SQIR/ExtractionGateSet.v) and for VOQC in [FullGateSet.v](https://github.com/inQWIRE/SQIR/blob/main/VOQC/FullGateSet.v). Both are shown below. We should unify these two gate sets for consistency. This will...

1. **Remove the dim parameter from the ucom, gate_list, etc. types** So far, this dependent parameter has just complicated proofs (e.g. properties about [optimize_then_map](https://github.com/inQWIRE/SQIR/blob/main/VOQC/Main.v#L929)) and obfuscated definitions (e.g. the use...