[Verifier] Verify each circuit transformation step (#176)

* [Verifier] Verify each circuit transformation step

* [Generator] Switch back to the previous canonical representation version (#175)

* [Verifier] Verify all transformation steps

* code format

src/quartz/circuitseq/circuitgate.cpp

@@ -307,4 +307,79 @@ std::string CircuitGate::to_qasm_style_string(Context *ctx,
   return result;
 }
 
+bool CircuitGate::equivalent(
+    const CircuitGate *this_gate, const CircuitGate *other_gate,
+    std::unordered_map<CircuitWire *, CircuitWire *> &wires_mapping,
+    bool update_mapping, std::queue<CircuitWire *> *wires_to_search,
+    bool backward) {
+  if (this_gate->gate->tp != other_gate->gate->tp) {
+    return false;
+  }
+  if (this_gate->input_wires.size() != other_gate->input_wires.size() ||
+      this_gate->output_wires.size() != other_gate->output_wires.size()) {
+    return false;
+  }
+  if (backward) {
+    for (int j = 0; j < (int)this_gate->output_wires.size(); j++) {
+      assert(this_gate->output_wires[j]->is_qubit());
+      // The output wire must have been mapped.
+      assert(wires_mapping.count(this_gate->output_wires[j]) != 0);
+      if (wires_mapping[this_gate->output_wires[j]] !=
+          other_gate->output_wires[j]) {
+        return false;
+      }
+    }
+    if (update_mapping) {
+      // Map input wires
+      for (int j = 0; j < (int)this_gate->input_wires.size(); j++) {
+        assert(wires_mapping.count(this_gate->input_wires[j]) == 0);
+        wires_mapping[this_gate->input_wires[j]] = other_gate->input_wires[j];
+        wires_to_search->push(this_gate->input_wires[j]);
+      }
+    } else {
+      // Verify mapping
+      for (int j = 0; j < (int)this_gate->input_wires.size(); j++) {
+        if (wires_mapping[this_gate->input_wires[j]] !=
+            other_gate->input_wires[j]) {
+          return false;
+        }
+      }
+    }
+  } else {
+    for (int j = 0; j < (int)this_gate->input_wires.size(); j++) {
+      if (this_gate->input_wires[j]->is_qubit()) {
+        // The input wire must have been mapped.
+        assert(wires_mapping.count(this_gate->input_wires[j]) != 0);
+        if (wires_mapping[this_gate->input_wires[j]] !=
+            other_gate->input_wires[j]) {
+          return false;
+        }
+      } else {
+        // parameters should not be mapped
+        if (other_gate->input_wires[j] != this_gate->input_wires[j]) {
+          return false;
+        }
+      }
+    }
+    if (update_mapping) {
+      // Map output wires
+      for (int j = 0; j < (int)this_gate->output_wires.size(); j++) {
+        assert(wires_mapping.count(this_gate->output_wires[j]) == 0);
+        wires_mapping[this_gate->output_wires[j]] = other_gate->output_wires[j];
+        wires_to_search->push(this_gate->output_wires[j]);
+      }
+    } else {
+      // Verify mapping
+      for (int j = 0; j < (int)this_gate->output_wires.size(); j++) {
+        if (wires_mapping[this_gate->output_wires[j]] !=
+            other_gate->output_wires[j]) {
+          return false;
+        }
+      }
+    }
+  }
+  // Equivalent
+  return true;
+}
+
 }  // namespace quartz

src/quartz/circuitseq/circuitgate.h

@@ -4,6 +4,8 @@
 #include "../utils/utils.h"
 
 #include <istream>
+#include <queue>
+#include <unordered_map>
 #include <vector>
 
 namespace quartz {
@@ -48,6 +50,33 @@ class CircuitGate {
   [[nodiscard]] std::string to_qasm_style_string(Context *ctx,
                                                  int param_precision) const;
 
+  /**
+   * Check if two gates in two circuits are equivalent given a mapping of
+   * circuit wires.
+   * @param this_gate A gate in the first circuit.
+   * @param other_gate A gate in the second circuit.
+   * @param wires_mapping A mapping from the wires in the first circuit to the
+   * wires in the second circuit.
+   * @param update_mapping If true, map the output wires, and push the output
+   * wires in the first circuit to the queue;
+   * if false, also check if the output wires are already correctly mapped
+   * (only return true if the gates are equivalent and the output wires are
+   * correctly mapped).
+   * @param wires_to_search When |update_mapping| is true and the two gates
+   * are equivalent under the wires mapping, store the new wires to search in
+   * the topological sort procedure. Otherwise, this parameter has no effect.
+   * When |update_mapping| is false, this parameter can be nullptr.
+   * @param backward If true, the topological sort is performed from the end
+   * of the circuit to the beginning. Only the output wires instead of the
+   * input wires are compared when |update_mapping| is true.
+   * @return True iff the two gates are equivalent under the wires mapping.
+   */
+  static bool
+  equivalent(const CircuitGate *this_gate, const CircuitGate *other_gate,
+             std::unordered_map<CircuitWire *, CircuitWire *> &wires_mapping,
+             bool update_mapping, std::queue<CircuitWire *> *wires_to_search,
+             bool backward = false);
+
   std::vector<CircuitWire *> input_wires;  // Include parameters!
   std::vector<CircuitWire *> output_wires;
 

src/quartz/circuitseq/circuitseq.cpp

@@ -53,35 +53,14 @@ bool CircuitSeq::fully_equivalent(const CircuitSeq &other) const {
   }
   std::unordered_map<CircuitWire *, CircuitWire *> wires_mapping;
   for (int i = 0; i < (int)wires.size(); i++) {
-    wires_mapping[other.wires[i].get()] = wires[i].get();
+    wires_mapping[wires[i].get()] = other.wires[i].get();
   }
   for (int i = 0; i < (int)gates.size(); i++) {
-    if (gates[i]->gate->tp != other.gates[i]->gate->tp) {
-      return false;
-    }
-    if (gates[i]->input_wires.size() != other.gates[i]->input_wires.size() ||
-        gates[i]->output_wires.size() != other.gates[i]->output_wires.size()) {
+    if (!CircuitGate::equivalent(gates[i].get(), other.gates[i].get(),
+                                 wires_mapping,
+                                 /*update_mapping=*/false, nullptr)) {
       return false;
     }
-    for (int j = 0; j < (int)gates[i]->input_wires.size(); j++) {
-      if (other.gates[i]->input_wires[j]->is_qubit()) {
-        if (wires_mapping[other.gates[i]->input_wires[j]] !=
-            gates[i]->input_wires[j]) {
-          return false;
-        }
-      } else {
-        // parameters should not be mapped
-        if (other.gates[i]->input_wires[j] != gates[i]->input_wires[j]) {
-          return false;
-        }
-      }
-    }
-    for (int j = 0; j < (int)gates[i]->output_wires.size(); j++) {
-      if (wires_mapping[other.gates[i]->output_wires[j]] !=
-          gates[i]->output_wires[j]) {
-        return false;
-      }
-    }
   }
   return true;
 }
@@ -123,35 +102,11 @@ bool CircuitSeq::topologically_equivalent(const CircuitSeq &other) const {
       if (!--gate_remaining_in_degree[this_gate]) {
         // Check if this gate is the same as the other gate
         auto other_gate = other_wire->output_gates[i];
-        if (this_gate->gate->tp != other_gate->gate->tp) {
+        if (!CircuitGate::equivalent(this_gate, other_gate, wires_mapping,
+                                     /*update_mapping=*/true,
+                                     &wires_to_search)) {
           return false;
         }
-        if (this_gate->input_wires.size() != other_gate->input_wires.size() ||
-            this_gate->output_wires.size() != other_gate->output_wires.size()) {
-          return false;
-        }
-        for (int j = 0; j < (int)this_gate->input_wires.size(); j++) {
-          if (this_gate->input_wires[j]->is_qubit()) {
-            // The input wire must have been mapped.
-            assert(wires_mapping.count(this_gate->input_wires[j]) != 0);
-            if (wires_mapping[this_gate->input_wires[j]] !=
-                other_gate->input_wires[j]) {
-              return false;
-            }
-          } else {
-            // parameters should not be mapped
-            if (other_gate->input_wires[j] != this_gate->input_wires[j]) {
-              return false;
-            }
-          }
-        }
-        // Map output wires
-        for (int j = 0; j < (int)this_gate->output_wires.size(); j++) {
-          assert(wires_mapping.count(this_gate->output_wires[j]) == 0);
-          wires_mapping[this_gate->output_wires[j]] =
-              other_gate->output_wires[j];
-          wires_to_search.push(this_gate->output_wires[j]);
-        }
       }
     }
   }
@@ -484,6 +439,16 @@ bool CircuitSeq::remove_gate(CircuitGate *circuit_gate) {
   return true;
 }
 
+bool CircuitSeq::remove_gate_near_end(CircuitGate *circuit_gate) {
+  auto gate_pos = std::find_if(
+      gates.rbegin(), gates.rend(),
+      [&](std::unique_ptr<CircuitGate> &p) { return p.get() == circuit_gate; });
+  if (gate_pos == gates.rend()) {
+    return false;
+  }
+  return remove_gate((int)(gates.rend() - gate_pos) - 1);
+}
+
 bool CircuitSeq::remove_first_quantum_gate() {
   for (auto &circuit_gate : gates) {
     if (circuit_gate->gate->is_quantum_gate()) {
@@ -1307,6 +1272,35 @@ CircuitSeq::get_permuted_seq(const std::vector<int> &qubit_permutation,
   return result;
 }
 
+std::unique_ptr<CircuitSeq>
+CircuitSeq::get_suffix_seq(const std::unordered_set<CircuitGate *> &start_gates,
+                           Context *ctx) const {
+  // For topological sort
+  std::unordered_map<CircuitGate *, int> gate_remaining_in_degree;
+  for (auto &gate : start_gates) {
+    gate_remaining_in_degree[gate] = 0;  // ready to include
+  }
+  auto result = std::make_unique<CircuitSeq>(get_num_qubits());
+  // The result should be a subsequence of this circuit
+  for (auto &gate : gates) {
+    if (gate_remaining_in_degree.count(gate.get()) > 0 &&
+        gate_remaining_in_degree[gate.get()] <= 0) {
+      result->add_gate(gate.get(), ctx);
+      for (auto &output_wire : gate->output_wires) {
+        for (auto &output_gate : output_wire->output_gates) {
+          // For topological sort
+          if (gate_remaining_in_degree.count(output_gate) == 0) {
+            gate_remaining_in_degree[output_gate] =
+                output_gate->gate->get_num_qubits();
+          }
+          gate_remaining_in_degree[output_gate]--;
+        }
+      }
+    }
+  }
+  return result;
+}
+
 void CircuitSeq::clone_from(const CircuitSeq &other,
                             const std::vector<int> &qubit_permutation,
                             const std::vector<int> &param_permutation,
@@ -1592,20 +1586,22 @@ std::vector<int> CircuitSeq::first_quantum_gate_positions() const {
   return result;
 }
 
+bool CircuitSeq::is_one_of_last_gates(CircuitGate *circuit_gate) const {
+  for (const auto &output_wire : circuit_gate->output_wires) {
+    if (outputs[output_wire->index] != output_wire) {
+      return false;
+    }
+  }
+  return true;
+}
+
 std::vector<CircuitGate *> CircuitSeq::last_quantum_gates() const {
   std::vector<CircuitGate *> result;
   for (const auto &circuit_gate : gates) {
     if (circuit_gate->gate->is_parameter_gate()) {
       continue;
     }
-    bool all_output = true;
-    for (const auto &output_wire : circuit_gate->output_wires) {
-      if (outputs[output_wire->index] != output_wire) {
-        all_output = false;
-        break;
-      }
-    }
-    if (all_output) {
+    if (is_one_of_last_gates(circuit_gate.get())) {
       result.push_back(circuit_gate.get());
     }
   }

src/quartz/circuitseq/circuitseq.h

@@ -106,17 +106,23 @@ class CircuitSeq {
   bool remove_last_gate();
 
   /**
-   * Remove a quantum gate.
+   * Remove a quantum gate in O(|get_num_gates()| - |gate_position|).
    * @param gate_position The position of the gate to be removed (0-indexed).
    * @return True iff the removal is successful.
    */
   bool remove_gate(int gate_position);
   /**
-   * Remove a quantum gate.
+   * Remove a quantum gate in O(|get_num_gates()|).
    * @param circuit_gate The gate to be removed.
    * @return True iff the removal is successful.
    */
   bool remove_gate(CircuitGate *circuit_gate);
+  /**
+   * Remove a quantum gate in O(|get_num_gates()| - |gate_position|).
+   * @param circuit_gate The gate to be removed.
+   * @return True iff the removal is successful.
+   */
+  bool remove_gate_near_end(CircuitGate *circuit_gate);
   /**
    * Remove the first quantum gate (if there is one).
    * @return True iff the removal is successful.
@@ -279,6 +285,14 @@ class CircuitSeq {
   get_permuted_seq(const std::vector<int> &qubit_permutation,
                    const std::vector<int> &input_param_permutation,
                    Context *ctx) const;
+  /**
+   * Get a circuit with |start_gates| and all gates topologically after them.
+   * @param start_gates The first gates at each qubit to include in the
+   * circuit to return.
+   */
+  [[nodiscard]] std::unique_ptr<CircuitSeq>
+  get_suffix_seq(const std::unordered_set<CircuitGate *> &start_gates,
+                 Context *ctx) const;
 
   /**
    * Get a circuit which replaces RZ gates with T, Tdg, S, Sdg, and Z gates.
@@ -307,6 +321,14 @@ class CircuitSeq {
    * @return The positions (0-indexed) of the first quantum gates.
    */
   [[nodiscard]] std::vector<int> first_quantum_gate_positions() const;
+  /**
+   * Check if a quantum gate can appear at last in some topological
+   * order of the CircuitSeq.
+   * @param circuit_gate The pointer to a quantum gate in the circuit.
+   * @return True iff the gate can appear at last in some topological
+   * order of the CircuitSeq.
+   */
+  [[nodiscard]] bool is_one_of_last_gates(CircuitGate *circuit_gate) const;
   /**
    * Returns quantum gates which can appear at last in some topological
    * order of the CircuitSeq.

src/quartz/generator/generator.cpp

@@ -10,10 +10,6 @@ bool Generator::generate(
     bool invoke_python_verifier, EquivalenceSet *equiv_set,
     bool unique_parameters, bool verbose,
     std::chrono::steady_clock::duration *record_verification_time) {
-  std::filesystem::path this_file_path(__FILE__);
-  auto quartz_root_path =
-      this_file_path.parent_path().parent_path().parent_path().parent_path();
-
   auto empty_dag = std::make_unique<CircuitSeq>(num_qubits);
   empty_dag->hash(ctx_);  // generate other hash values
   std::vector<CircuitSeq *> dags_to_search(1, empty_dag.get());
@@ -61,7 +57,7 @@ bool Generator::generate(
       if (num_gates == max_num_quantum_gates) {
         break;
       }
-      bool ret = dataset->save_json(ctx_, quartz_root_path.string() +
+      bool ret = dataset->save_json(ctx_, kQuartzRootPath.string() +
                                               "/tmp_before_verify.json");
       assert(ret);
 
@@ -70,10 +66,10 @@ bool Generator::generate(
         start = std::chrono::steady_clock::now();
       }
       std::string command_string =
-          std::string("python ") + quartz_root_path.string() +
+          std::string("python ") + kQuartzRootPath.string() +
           "/src/python/verifier/verify_equivalences.py " +
-          quartz_root_path.string() + "/tmp_before_verify.json " +
-          quartz_root_path.string() + "/tmp_after_verify.json";
+          kQuartzRootPath.string() + "/tmp_before_verify.json " +
+          kQuartzRootPath.string() + "/tmp_after_verify.json";
       system(command_string.c_str());
       if (record_verification_time) {
         auto end = std::chrono::steady_clock::now();
@@ -82,7 +78,7 @@ bool Generator::generate(
 
       dags_to_search.clear();
       ret = equiv_set->load_json(
-          ctx_, quartz_root_path.string() + "/tmp_after_verify.json",
+          ctx_, kQuartzRootPath.string() + "/tmp_after_verify.json",
           /*from_verifier=*/true, &dags_to_search);
       assert(ret);
       for (auto &dag : dags_to_search) {