-
Notifications
You must be signed in to change notification settings - Fork 0
/
counterexample.py
155 lines (113 loc) · 3.72 KB
/
counterexample.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
from giallar.core.spec.qcircuit import *
from giallar.core.spec.qgate import *
from giallar.core.spec.invariant import *
from giallar.z3_wrapper import *
size = Int('size')
size2 = Int('size2')
# assertion(size==2)
assertion(size2> size)
a = QCircuit(size=size)
# a.append(a[0])
gate_index = 0
gate = a[gate_index]
sucs = a.direct_successors(gate_index)
suc_gate = sucs['gates'][0]
suc_index = sucs['indices'][0]
b = a.remove(suc_index)
b = b.remove(0)
out_circ = QCircuit(size=2)
assertion(out_circ[0] == a[0])
assertion(out_circ[1] == suc_gate)
gid = fresh_int('gid')
op = fresh_int('op')
new_gate = QGate(gid, [op, op, op])
qubits = fresh_array("qubits", IntSort(), QubitStateType)
k = fresh_int("k")
assertion(ForAll([qubits, k], apply_on_qubit_state(qubits, new_gate)[k] == apply_on_qubit_state(apply_on_qubit_state(qubits, a[0]), suc_gate)[k]))
init_circ = QCircuit()
certiq_prove(equivalent(init_circ.append(new_gate).extend(b), init_circ.extend(a)))
"""
out_circ2 = QCircuit(size=1)
assertion(equivalent(out_circ, out_circ2))
# certiq_prove(equivalent(out_circ2.extend(b), a))
circ = QCircuit()
certiq_prove(equivalent(circ.extend(out_circ2).extend(b), circ.extend(a)))
"""
"""
assertion(a[0] == c[0])
assertion(b[0] == c[0])
assertion(a[1] == c[1])
assertion(b[1] == c[1])
certiq_prove(equivalent(a, b))
"""
"""
i = fresh_int()
j = fresh_int()
k = fresh_int()
assertion(And(i<j, i>0))
part1 = a.partial_circuit(0, i)
part2 = a.partial_circuit(i, j)
part3 = a.partial_circuit(0, j)
qubits = fresh_array("init_qubit", IntSort(), QubitStateType)
r1 = apply_circuit_on_qubit_state(qubits, part1, part1.size())
r2 = apply_circuit_on_qubit_state(r1, part2, part2.size())
r3 = apply_circuit_on_qubit_state(qubits, part3, part3.size())
m = fresh_int()
"""
# certiq_prove(ForAll([m], Implies(And(m>=0, m<a.size()), r2[m] == r3[m])))
# certiq_prove(equivalent(part1.extend(part2), part3))
"""
b = a.remove(1)
b_part_1 = b.partial_circuit(0, 1)
b_part_2 = b.partial_circuit(1, b.size())
a_part_1 = a.partial_circuit(0, 1)
a_part_2 = a.partial_circuit(2, a.size())
certiq_prove(equivalent(a_part_1, b_part_1))
certiq_prove(equivalent(a_part_2, b_part_2))
"""
"""
# certiq_prove(b.size() == a.size() - 1)
c = b.partial_circuit(1, a.size() - 1)
d = a.partial_circuit(2, a.size())
# print("hihi")
# certiq_prove(c.size() == d.size())
i = fresh_int()
certiq_prove(c.size() == a.size() - 2)
# certiq_prove(ForAll([i], Implies(And(i>=0, i<a.size()-2), c[i]==b[i+1])))
# assertion(ForAll([i], Implies(And(i>=0, i<a.size()-2), c[i]==b[i+1])))
j = fresh_int()
qubits = fresh_array("init_qubit", IntSort(), QubitStateType)
# certiq_prove(ForAll([i], Implies(And(i>=0, i<a.size()-2), b[i+1] == a[i+2])))
# assertion(ForAll([i], Implies(And(i>=0, i<a.size()-2), b[i+1] == a[i+2])))
certiq_prove(ForAll([i], Implies(And(i>=0, i<a.size()-2), c[i] == a[i+2])))
certiq_prove(ForAll([i], Implies(And(i>=0, i<a.size()-2), d[i] == a[i+2])))
certiq_prove(ForAll([i], Implies(And(i>=0, i<a.size()-2), c[i] == d[i])))
result_c = apply_circuit_on_qubit_state(qubits, c, c.size())
result_d = apply_circuit_on_qubit_state(qubits, d, d.size())
result_a_part = apply_part_circuit_on_qubit_state(
print("hihi")
print("hihi")
certiq_prove(ForAll([qubits, j], result_c[j] == result_d[j]))
"""
"""
i = fresh_int()
start=Int('start')
assertion(start==0)
assertion(ForAll([i], Implies(And(i<size, i>=start), a[i-start]==ex[i])))
assertion(ForAll([i], Implies(And(i<size, i>=0), b[i]==ex[i])))
certiq_prove(ForAll([i], Implies(And(i<size, i>=0), b[i]==a[i])))
"""
#########################
"""
i = Int('i')
assertion(And(i>0, i < size))
g = a[i]
"""
# a.append(g)
# a.extend(ex)
"""
b = a.remove(i)
c = a.partial_circuit(0, 1)
# d = a.partial_circuit(2, a.size())
d = a.partial_circuit(size2, a.size())
"""