# q-solved - zer0pts CTF 2022
###### tags: `zer0pts CTF 2022` `rev` `quantum`
Writeups: https://hackmd.io/@ptr-yudai/rJgjygUM9

## Overview
You're given a quantum circuit to calculate something and prints the flag based on the measurement.

## Analysis
The circuit looks like this:

main.x(target)
main.h(target)
for i in range(circ['memory']):
    main.h(i)

t = circ['memory']
for cs in circ['circuit']:
    ctrl = ''.join(['0' if x else '1' for (x, _) in cs])
    l = [c for (_, c) in cs]
    sub.append(XGate().control(len(cs), ctrl_state=ctrl), l + [t])
    t += 1

sub.append(XGate().control(na, ctrl_state='0'*na),
           [i for i in range(nq, nq + na)] + [target])

for cs in circ['circuit'][::-1]:
    t -= 1
    ctrl = ''.join(['0' if x else '1' for (x, _) in cs])
    l = [c for (_, c) in cs]
    sub.append(XGate().control(len(cs), ctrl_state=ctrl), l + [t])

sub.h([i for i in range(nq)])
sub.append(XGate().control(nq, ctrl_state='0'*nq),
           [i for i in range(nq)] + [target])
sub.h([i for i in range(nq)])

for i in range(round(0.785 * int(gmpy2.isqrt(2**nq)) - 0.5)):
    main.append(sub, [i for i in range(na + nq + 1)])

for i in range(nq):
    main.measure(i, i)

After initializing the input by Hadamard gates, it calls a subroutine `sub` many times. At last, the input bits are measured and the most possible combination of the measured bits become the flag.

You can devide the subroutine into 4 parts.
The first part calculates some logical operations:

t = circ['memory']
for cs in circ['circuit']:
    ctrl = ''.join(['0' if x else '1' for (x, _) in cs])
    l = [c for (_, c) in cs]
    sub.append(XGate().control(len(cs), ctrl_state=ctrl), l + [t])
    t += 1

The second part applies multi-controlled X gate to ancilla bit with the result of the previous operations.

sub.append(XGate().control(na, ctrl_state='0'*na),
           [i for i in range(nq, nq + na)] + [target])

The third part reverses the operations of the first part, which is just restoring the input state.

for cs in circ['circuit'][::-1]:
    t -= 1
    ctrl = ''.join(['0' if x else '1' for (x, _) in cs])
    l = [c for (_, c) in cs]
    sub.append(XGate().control(len(cs), ctrl_state=ctrl), l + [t])

The last part is applying Hadamard gates and X gate.

sub.h([i for i in range(nq)])
sub.append(XGate().control(nq, ctrl_state='0'*nq),
           [i for i in range(nq)] + [target])
sub.h([i for i in range(nq)])

This is obviously the circuit for amplitude amplification.

So, we can understand the circuit is searching an input that satisfies the given logical operations. This is equivalent to a SAT solver. In fact, you can input the circuit JSON to Z3 without any calculation.

## Solver

import json
from z3 import *

with open("../distfiles/circuit.json", "r") as f:
    circ = json.load(f)

bits = [Bool(f'b{i}') for i in range(circ['memory'])]

s = Solver()
for cs in circ['circuit']:
    l = []
    for (x, c) in cs:
        l.append(bits[c] if x else Not(bits[c]))
    s.add(Or(l))

r = s.check()
if r == sat:
    m = s.model()
    f = 0
    for i, b in enumerate(bits):
        f |= (1 if m[b] else 0) << i

    print(int.to_bytes(f, circ['memory']//8, 'little'))

else:
    print(":(")