From 093447201aef03dc53d3f44fe941ec89313d6caa Mon Sep 17 00:00:00 2001 From: Mingkuan Xu Date: Wed, 12 Jun 2024 14:45:33 -0700 Subject: [PATCH] [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 | 75 +++++++++ src/quartz/circuitseq/circuitgate.h | 29 ++++ src/quartz/circuitseq/circuitseq.cpp | 116 +++++++------ src/quartz/circuitseq/circuitseq.h | 26 ++- src/quartz/generator/generator.cpp | 14 +- src/quartz/utils/utils.h | 9 + src/quartz/verifier/verifier.cpp | 229 ++++++++++++++++++++++++++ src/quartz/verifier/verifier.h | 22 ++- src/test/gen_ecc_set.cpp | 13 +- src/test/gen_ecc_set.h | 6 +- src/test/test_optimization_steps.cpp | 24 ++- 11 files changed, 470 insertions(+), 93 deletions(-) diff --git a/src/quartz/circuitseq/circuitgate.cpp b/src/quartz/circuitseq/circuitgate.cpp index be9a1f3f..950f7564 100644 --- a/src/quartz/circuitseq/circuitgate.cpp +++ b/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 &wires_mapping, + bool update_mapping, std::queue *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 diff --git a/src/quartz/circuitseq/circuitgate.h b/src/quartz/circuitseq/circuitgate.h index 9cfb70d5..d919fb8e 100644 --- a/src/quartz/circuitseq/circuitgate.h +++ b/src/quartz/circuitseq/circuitgate.h @@ -4,6 +4,8 @@ #include "../utils/utils.h" #include +#include +#include #include 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 &wires_mapping, + bool update_mapping, std::queue *wires_to_search, + bool backward = false); + std::vector input_wires; // Include parameters! std::vector output_wires; diff --git a/src/quartz/circuitseq/circuitseq.cpp b/src/quartz/circuitseq/circuitseq.cpp index b91cfb71..bd407315 100644 --- a/src/quartz/circuitseq/circuitseq.cpp +++ b/src/quartz/circuitseq/circuitseq.cpp @@ -53,35 +53,14 @@ bool CircuitSeq::fully_equivalent(const CircuitSeq &other) const { } std::unordered_map 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 &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 &qubit_permutation, return result; } +std::unique_ptr +CircuitSeq::get_suffix_seq(const std::unordered_set &start_gates, + Context *ctx) const { + // For topological sort + std::unordered_map gate_remaining_in_degree; + for (auto &gate : start_gates) { + gate_remaining_in_degree[gate] = 0; // ready to include + } + auto result = std::make_unique(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 &qubit_permutation, const std::vector ¶m_permutation, @@ -1592,20 +1586,22 @@ std::vector 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 CircuitSeq::last_quantum_gates() const { std::vector 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()); } } diff --git a/src/quartz/circuitseq/circuitseq.h b/src/quartz/circuitseq/circuitseq.h index de9e4fd3..5f8247a0 100644 --- a/src/quartz/circuitseq/circuitseq.h +++ b/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 &qubit_permutation, const std::vector &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 + get_suffix_seq(const std::unordered_set &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 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. diff --git a/src/quartz/generator/generator.cpp b/src/quartz/generator/generator.cpp index 87063945..7d712471 100644 --- a/src/quartz/generator/generator.cpp +++ b/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(num_qubits); empty_dag->hash(ctx_); // generate other hash values std::vector 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) { diff --git a/src/quartz/utils/utils.h b/src/quartz/utils/utils.h index f9e4c008..1bc63230 100644 --- a/src/quartz/utils/utils.h +++ b/src/quartz/utils/utils.h @@ -1,6 +1,8 @@ #pragma once #include +#include + using ParamType = double; #ifdef USE_ARBLIB #include "arb_complex.h" @@ -35,6 +37,13 @@ constexpr bool kUseRowRepresentationToCompare = false; constexpr int kDefaultQASMParamPrecision = 15; +const std::filesystem::path kQuartzRootPath = + std::filesystem::canonical(__FILE__) + .parent_path() + .parent_path() + .parent_path() + .parent_path(); + struct PairHash { public: template diff --git a/src/quartz/verifier/verifier.cpp b/src/quartz/verifier/verifier.cpp index a59d2bde..5c7a84a1 100644 --- a/src/quartz/verifier/verifier.cpp +++ b/src/quartz/verifier/verifier.cpp @@ -1,11 +1,240 @@ #include "verifier.h" +#include "quartz/dataset/dataset.h" #include "quartz/utils/utils.h" #include #include +#include +#include +#include namespace quartz { +bool Verifier::verify_transformation_steps(Context *ctx, + const std::string &steps_file_prefix, + bool verbose) { + int step_count = 0; + std::ifstream fin(steps_file_prefix + ".txt"); + assert(fin.is_open()); + fin >> step_count; + fin.close(); + std::vector> circuits; + circuits.reserve(step_count + 1); + for (int i = 0; i <= step_count; i++) { + circuits.push_back(CircuitSeq::from_qasm_file( + ctx, steps_file_prefix + std::to_string(i) + ".qasm")); + if (verbose) { + std::cout << "circuit " << i << std::endl; + std::cout << circuits[i]->to_string(/*line_number=*/true) << std::endl; + } + if (i > 0) { + if (verbose) { + std::cout << "Verifying circuit " << i - 1 << " -> circuit " << i + << std::endl; + } + if (!equivalent(ctx, circuits[i - 1].get(), circuits[i].get(), verbose)) { + return false; + } + } + } + if (verbose) { + std::cout << step_count << " transformations verified." << std::endl; + } + return true; +} + +bool Verifier::equivalent(Context *ctx, const CircuitSeq *circuit1, + const CircuitSeq *circuit2, bool verbose) { + if (circuit1->get_num_qubits() != circuit2->get_num_qubits()) { + if (verbose) { + std::cout << "Not equivalent: different numbers of qubits." << std::endl; + } + return false; + } + const int num_qubits = circuit1->get_num_qubits(); + + // Mappings for topological sort + std::unordered_map wires_mapping; + std::queue wires_to_search; + std::unordered_map gate_remaining_in_degree; + for (int i = 0; i < num_qubits; i++) { + wires_mapping[circuit1->wires[i].get()] = circuit2->wires[i].get(); + wires_to_search.push(circuit1->wires[i].get()); + } + // Try to remove common first gates and record the frontier + std::vector qubit_blocked(num_qubits, false); + std::unordered_set leftover_gates_start1; + std::unordered_set leftover_gates_start2; + // (Partial) topological sort on circuit1 + while (!wires_to_search.empty()) { + auto wire1 = wires_to_search.front(); + assert(wires_mapping.count(wire1) > 0); + auto wire2 = wires_mapping[wire1]; + wires_to_search.pop(); + assert(wire1->output_gates.size() <= 1); + assert(wire2->output_gates.size() <= 1); + if (wire1->output_gates.empty() || wire2->output_gates.empty() || + std::any_of(wire1->output_gates[0]->output_wires.begin(), + wire1->output_gates[0]->output_wires.end(), + [&qubit_blocked](CircuitWire *output_wire) { + return qubit_blocked[output_wire->index]; + })) { + // Block qubits of potential unmatched gates + for (auto &gate : wire1->output_gates) { + for (auto &output_wire : gate->output_wires) { + qubit_blocked[output_wire->index] = true; + } + // Use std::unordered_set to deduplicate, similarly hereinafter + leftover_gates_start1.insert(gate); + } + for (auto &gate : wire2->output_gates) { + for (auto &output_wire : gate->output_wires) { + qubit_blocked[output_wire->index] = true; + } + leftover_gates_start2.insert(gate); + } + continue; + } + + auto gate1 = wire1->output_gates[0]; + auto gate2 = wire2->output_gates[0]; + if (gate_remaining_in_degree.count(gate1) == 0) { + // A new gate + gate_remaining_in_degree[gate1] = gate1->gate->get_num_qubits(); + } + if (!--gate_remaining_in_degree[gate1]) { + // Check if this gate is the same as the other gate and continue + // the topological sort (wires_to_search is updated in + // CircuitGate::equivalent()) + if (!CircuitGate::equivalent(gate1, gate2, wires_mapping, + /*update_mapping=*/true, &wires_to_search)) { + // If not matched, block each qubit of both gates + for (auto &input_wire : gate1->input_wires) { + if (input_wire->is_qubit()) { + qubit_blocked[input_wire->index] = true; + // Note that this input wire might be not in the search queue now. + // We need to manually add the gate in circuit2 to the frontier. + assert(wires_mapping.count(input_wire) > 0); + for (auto &gate : wires_mapping[input_wire]->output_gates) { + leftover_gates_start2.insert(gate); + } + } + } + leftover_gates_start1.insert(gate1); + for (auto &output_wire : gate2->output_wires) { + qubit_blocked[output_wire->index] = true; + } + leftover_gates_start2.insert(gate2); + } + } + } + + if (leftover_gates_start1.empty() && leftover_gates_start2.empty()) { + // The two circuits are equivalent. + if (verbose) { + std::cout << "Equivalent: same circuit." << std::endl; + } + return true; + } + + auto c1 = circuit1->get_suffix_seq(leftover_gates_start1, ctx); + auto c2 = circuit2->get_suffix_seq(leftover_gates_start2, ctx); + // We should have removed the same number of gates + assert(circuit1->get_num_gates() - c1->get_num_gates() == + circuit2->get_num_gates() - c2->get_num_gates()); + + // Remove common last gates + while (true) { + bool removed_anything = false; + for (int i = 0; i < num_qubits; i++) { + if (c1->outputs[i]->input_gates.empty() || + c2->outputs[i]->input_gates.empty()) { + // At least of the two circuits does not have a gate at qubit i + continue; + } + assert(c1->outputs[i]->input_gates.size() == 1); + assert(c2->outputs[i]->input_gates.size() == 1); + auto gate1 = c1->outputs[i]->input_gates[0]; + auto gate2 = c2->outputs[i]->input_gates[0]; + if (gate1->gate != gate2->gate || + gate1->input_wires.size() != gate2->input_wires.size() || + !c1->is_one_of_last_gates(gate1) || + !c2->is_one_of_last_gates(gate2)) { + continue; + } + bool matched = true; + for (int j = 0; j < (int)gate1->input_wires.size(); j++) { + if (gate1->input_wires[j]->is_qubit() != + gate2->input_wires[j]->is_qubit()) { + matched = false; + break; + } + if (gate1->input_wires[j]->is_qubit()) { + if (gate1->input_wires[j]->index != gate2->input_wires[j]->index) { + matched = false; + break; + } + } else { + // parameters should not be mapped + if (gate1->input_wires[j] != gate2->input_wires[j]) { + matched = false; + break; + } + } + } + if (matched) { + c1->remove_gate_near_end(gate1); + c2->remove_gate_near_end(gate2); + removed_anything = true; + } + } + if (!removed_anything) { + break; + } + } + + if (verbose) { + std::cout << "Checking Verifier::equivalent() on:" << std::endl; + std::cout << c1->to_string(/*line_number=*/true) << std::endl; + std::cout << c2->to_string(/*line_number=*/true) << std::endl; + } + + Dataset dataset; + bool ret = dataset.insert(ctx, std::move(c1)); + assert(ret); + ret = dataset.insert_to_nearby_set_if_exists(ctx, std::move(c2)); + if (ret) { + // no nearby set + if (verbose) { + std::cout << "Not equivalent: different hash values." << std::endl; + } + return false; // hash value not equal or adjacent + } + ret = dataset.save_json(ctx, + kQuartzRootPath.string() + "/tmp_before_verify.json"); + assert(ret); + std::string command_string = + std::string("python ") + kQuartzRootPath.string() + + "/src/python/verifier/verify_equivalences.py " + + kQuartzRootPath.string() + "/tmp_before_verify.json " + + kQuartzRootPath.string() + "/tmp_after_verify.json"; + system(command_string.c_str()); + EquivalenceSet equiv_set; + ret = equiv_set.load_json(ctx, + kQuartzRootPath.string() + "/tmp_after_verify.json", + /*from_verifier=*/true, nullptr); + assert(ret); + if (equiv_set.num_equivalence_classes() == 1) { + return true; // equivalent + } else { + if (verbose) { + std::cout << "Not equivalent: Z3 cannot prove they are equivalent." + << std::endl; + } + return false; // not equivalent + } +} + bool Verifier::equivalent_on_the_fly(Context *ctx, CircuitSeq *circuit1, CircuitSeq *circuit2) { // Disable the verifier. diff --git a/src/quartz/verifier/verifier.h b/src/quartz/verifier/verifier.h index 7d9fd463..3656565f 100644 --- a/src/quartz/verifier/verifier.h +++ b/src/quartz/verifier/verifier.h @@ -8,7 +8,27 @@ namespace quartz { // Verify if two circuits are equivalent and other things about DAGs. class Verifier { public: - bool equivalent(Context *ctx, CircuitSeq *circuit1, CircuitSeq *circuit2); + /** + * Verify all transformation steps. + * @param ctx The context to load the circuits from files. + * @param steps_file_prefix The parameter |store_all_steps_file_prefix| when + * calling Graph::optimize(). + * @param verbose Print logs to the screen. + * @return True if we can verify all transformation steps. + */ + bool verify_transformation_steps(Context *ctx, + const std::string &steps_file_prefix, + bool verbose = false); + /** + * Verify if two circuits are functionally equivalent. They are expected + * to differ by only one small circuit transformation. + * @param ctx The context for both circuits. + * @param verbose Print logs to the screen. + * @return True if we can prove that the two circuits are functionally + * equivalent. + */ + bool equivalent(Context *ctx, const CircuitSeq *circuit1, + const CircuitSeq *circuit2, bool verbose = false); // On-the-fly equivalence checking while generating circuits bool equivalent_on_the_fly(Context *ctx, CircuitSeq *circuit1, CircuitSeq *circuit2); diff --git a/src/test/gen_ecc_set.cpp b/src/test/gen_ecc_set.cpp index 6b2a219d..838f2ecb 100644 --- a/src/test/gen_ecc_set.cpp +++ b/src/test/gen_ecc_set.cpp @@ -9,15 +9,12 @@ using namespace quartz; int main() { - std::filesystem::path this_file_path(__FILE__); - auto quartz_root_path = - this_file_path.parent_path().parent_path().parent_path(); // gen_ecc_set({GateType::u1, GateType::u2, GateType::u3, GateType::cx, // GateType::add}, // "IBM_3_3_", true, 3, 4, 3); gen_ecc_set({GateType::h, GateType::cz}, - quartz_root_path.string() + "/eccset/H_CZ_2_2_", true, false, 2, - 0, 2); + kQuartzRootPath.string() + "/eccset/H_CZ_2_2_", true, false, 2, 0, + 2); // for (int n = 5; n <= 8; n++) { // std::string file_prefix = "Rigetti_"; // file_prefix += std::to_string(n); @@ -30,12 +27,12 @@ int main() { // "IBM_4_3_", true, 3, 4, 4); gen_ecc_set({GateType::t, GateType::tdg, GateType::h, GateType::x, GateType::cx, GateType::add}, - quartz_root_path.string() + "/eccset/Clifford_T_5_3_", true, - false, 3, 0, 5); + kQuartzRootPath.string() + "/eccset/Clifford_T_5_3_", true, false, + 3, 0, 5); for (int n = 2; n <= 4; n++) { for (int q = 3; q <= 3; q++) { - std::string file_prefix = quartz_root_path.string() + "/eccset/Nam_"; + std::string file_prefix = kQuartzRootPath.string() + "/eccset/Nam_"; file_prefix += std::to_string(n); file_prefix += "_"; file_prefix += std::to_string(q); diff --git a/src/test/gen_ecc_set.h b/src/test/gen_ecc_set.h index 9feaa837..13a8e333 100644 --- a/src/test/gen_ecc_set.h +++ b/src/test/gen_ecc_set.h @@ -15,10 +15,6 @@ void gen_ecc_set(const std::vector &supported_gates, const std::string &file_prefix, bool unique_parameters, bool generate_representative_set, int num_qubits, int num_input_parameters, int max_num_quantum_gates) { - std::filesystem::path this_file_path(__FILE__); - auto quartz_root_path = - this_file_path.parent_path().parent_path().parent_path(); - ParamInfo param_info(/*num_input_symbolic_params=*/num_input_parameters); Context ctx(supported_gates, num_qubits, ¶m_info); Generator gen(&ctx); @@ -58,7 +54,7 @@ void gen_ecc_set(const std::vector &supported_gates, dataset1.save_json(&ctx, file_prefix + "pruning_unverified.json"); auto start2 = std::chrono::steady_clock::now(); - system(("python " + quartz_root_path.string() + + system(("python " + kQuartzRootPath.string() + "/src/python/verifier/verify_equivalences.py " + file_prefix + "pruning_unverified.json " + file_prefix + "pruning.json") .c_str()); diff --git a/src/test/test_optimization_steps.cpp b/src/test/test_optimization_steps.cpp index 6c7c5ab2..0cff4b30 100644 --- a/src/test/test_optimization_steps.cpp +++ b/src/test/test_optimization_steps.cpp @@ -1,6 +1,7 @@ #include "test_optimization_steps.h" #include "quartz/gate/gate_utils.h" +#include "quartz/verifier/verifier.h" #include #include @@ -13,17 +14,24 @@ int main() { GateType::h, GateType::t, GateType::tdg, GateType::x, GateType::add}, ¶m_info); - std::filesystem::path this_file_path(__FILE__); - auto quartz_root_path = - this_file_path.parent_path().parent_path().parent_path(); - if (!std::filesystem::exists(quartz_root_path / "logs")) { - std::filesystem::create_directory(quartz_root_path / "logs"); + if (!std::filesystem::exists(kQuartzRootPath / "logs")) { + std::filesystem::create_directory(kQuartzRootPath / "logs"); } test_optimization( &ctx, - (quartz_root_path / "circuit/example-circuits/barenco_tof_3.qasm") + (kQuartzRootPath / "circuit/example-circuits/barenco_tof_3.qasm") .string(), - (quartz_root_path / "eccset/Clifford_T_5_3_complete_ECC_set.json") + (kQuartzRootPath / "eccset/Clifford_T_5_3_complete_ECC_set.json") .string(), - /*timeout=*/10, (quartz_root_path / "logs/barenco_tof_3_").string()); + /*timeout=*/12, (kQuartzRootPath / "logs/barenco_tof_3_").string()); + Verifier verifier; + bool verified = verifier.verify_transformation_steps( + &ctx, (kQuartzRootPath / "logs/barenco_tof_3_").string(), + /*verbose=*/true); + if (verified) { + std::cout << "All transformations are verified." << std::endl; + } else { + std::cout << "Some transformation is not verified." << std::endl; + } + return 0; }