-
Notifications
You must be signed in to change notification settings - Fork 3
/
QC_state.v
executable file
·368 lines (308 loc) · 17.3 KB
/
QC_state.v
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
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
Require Import Reals.
Require Import Psatz.
Require Import SQIR.
Require Import VectorStates UnitaryOps Coq.btauto.Btauto Coq.NArith.Nnat.
Require Import Dirac.
Require Import QPE.
Require Import BasicUtility.
Require Import Classical_Prop.
Require Import MathSpec.
Require Import OQASM.
Require Import OQIMP.
(**********************)
(** Unitary Programs **)
(**********************)
Declare Scope pexp_scope.
Delimit Scope pexp_scope with pexp.
Local Open Scope pexp_scope.
Local Open Scope nat_scope.
(* This will be replaced by PQASM. *)
(* For simplicity, let's assume that we deal with natural number arithemtic first. *)
Inductive aexp := BA (b:vari)
| Num (n:nat) | APlus (e1:aexp) (e2:aexp) | AMinus (e1:aexp) (e2:aexp) | AMult (e1:aexp) (e2:aexp)
| TwoTo (e1:aexp) | App (f:var) (x:aexp) (* uninterpreted function. *)
| FExpI (a:aexp) (* e ^ 2pi i * 1/2^a *)
| FAddExpI (b:bexp) (a:aexp) (* (1+ e ^ 2pi i * a) / 2 or (1- e ^ 2pi i * a) / 2, the b is the +- sign *)
| GetP (s:state) (* in a normal state alpha |b>, the alpha
if had_state get beta in R |0> + beta * R |1> *)
| Left (s:state) (* in a superposition alpha |0> + beta |1>, the alpha *)
| Right (s:state) (* in a superposition alpha |0> + beta |1>, the beta *)
| Bit (b:bexp)
| ASum (x:bexp) (y:aexp)
with vari := Var(x:var) | Index (x:var) (al:list aexp)
with bexp := BFalse | BTrue
| BEq (x:aexp) (y:aexp) | BGe (x:aexp) (y:aexp) | BLt (x:aexp) (y:aexp)
(* | FEq (x:fexp) (y:fexp) | FGe (x:fexp) (y:fexp) | FLt (x:fexp) (y:fexp) *)
| BTest (x:vari)
| BXOR (x:bexp) (y:bexp) | BITE (x:bexp) (e1:bexp) (e2:bexp) | BNeg (x:bexp)
| BAnd (x:bexp) (y:bexp)
| GetB (s:state) (* in a normal state alpha |b>, the b *)
with state :Type :=
| SA (x:list vari) (l:list (list vari * state))
| ket (b:bexp) (*normal state |0> false or |1> true *)
| qket (p:aexp) (b:bexp)
| upP (e:state) (a:aexp)
| SITE (x:bexp) (e1:state) (e2:state)
| Join (e1:state) (e2:state)
| SPlus (s1:state) (s2:state) (* Let's say that we only allow |0> + |1> first. *)
| Tensor (s1:list state) (* tensor of list of states, avoiding associativy definition *)
(* | Plus (s1:state) (s2:state) |x> + |y> state. x and y are not equal *)
| Sigma (n:aexp) (i:var) (b:aexp) (s:state) (* represent 1/sqrt{2^n} Sigma^n_{i=b} s *)
| NTensor (n:aexp) (i:var) (b:aexp) (s:state) (* represent Tensor^n_{i=b} s *).
(*
Definition posi :Type := (var * aexp).
*)
(*
Inductive fexp := Fixed (r:R) | FNeg (f1:fexp) | FPlus (f1:fexp) (f2:fexp) | FTimes (f1:fexp) (f2:fexp)
| FDiv (f1:fexp) (f2:fexp)
| FSum (n:aexp) (i:var) (b:aexp) (f:fexp)
| FExp (f:fexp) | FSin (f:fexp) | FCos (f:fexp)
| FCom (f:fexp) (f1:fexp) (* a + b i *)
| FExpI (a:aexp) (* e^ 2pi i * a *).
*)
(*
Inductive bexp := BFalse | BTrue
| BEq (x:aexp) (y:aexp) | BGe (x:aexp) (y:aexp) | BLt (x:aexp) (y:aexp)
(* | FEq (x:fexp) (y:fexp) | FGe (x:fexp) (y:fexp) | FLt (x:fexp) (y:fexp) *)
| BTest (i:aexp) (x:aexp) (* bit test on x[i] *)
| BXOR (x:bexp) (y:bexp) | BITE (x:bexp) (e1:bexp) (e2:bexp) | BNeg (x:bexp).
*)
Fixpoint list_mem (a:var) (l:list var) :=
match l with [] => false
| x::xs => if a =? x then true else list_mem a xs
end.
Definition diff l1 l2 := List.filter (fun a => ¬ (list_mem a l2)) l1.
Fixpoint collect_var_aexp (a:aexp) :=
match a with BA a => collect_var_basic a
| Num x => nil
| APlus e1 e2 => (collect_var_aexp e1)++(collect_var_aexp e2)
| AMinus e1 e2 => (collect_var_aexp e1)++(collect_var_aexp e2)
| AMult e1 e2 => (collect_var_aexp e1)++(collect_var_aexp e2)
| TwoTo e => collect_var_aexp e
| App f x => f::(collect_var_aexp x)
| FExpI x => collect_var_aexp x
| FAddExpI b x => collect_var_bexp b ++ collect_var_aexp x
| GetP s => collect_var_state s
| Left s => collect_var_state s
| Right s => collect_var_state s
| Bit s => collect_var_bexp s
| ASum s y => collect_var_bexp s ++ collect_var_aexp y
end
with collect_var_basic (b:vari) :=
match b with Var x => ([x]) | Index x e2 => [x]++(fold_left (fun acc b => acc++(collect_var_aexp b)) e2 []) end
(*
Fixpoint collect_var_fexp (a:fexp) :=
match a with Fixed a => nil
| FNeg e1 => (collect_var_fexp e1)
| FPlus e1 e2 => (collect_var_fexp e1)++(collect_var_fexp e2)
| FTimes e1 e2 => (collect_var_fexp e1)++(collect_var_fexp e2)
| FDiv e1 e2 => (collect_var_fexp e1)++(collect_var_fexp e2)
| FSum a i b f => (collect_var_aexp a)++(collect_var_aexp b)++(collect_var_fexp f)
| FCom e1 e2 => (collect_var_fexp e1)++(collect_var_fexp e2)
| FExp e1 => (collect_var_fexp e1)
| FSin e1 => (collect_var_fexp e1)
| FCos e1 => (collect_var_fexp e1)
| FExpI e1 => collect_var_aexp e1
end.
*)
with collect_var_bexp (b:bexp) :=
match b with BTrue => nil | BFalse => nil
| BEq x y => (collect_var_aexp x)++(collect_var_aexp y)
| BGe x y => (collect_var_aexp x)++(collect_var_aexp y)
| BLt x y => (collect_var_aexp x)++(collect_var_aexp y)
| BXOR x y => (collect_var_bexp x)++(collect_var_bexp y)
| BAnd x y => (collect_var_bexp x)++(collect_var_bexp y)
| BITE x y z => (collect_var_bexp x)++(collect_var_bexp y)++(collect_var_bexp z)
| BNeg x => (collect_var_bexp x)
| BTest x => collect_var_basic x
| GetB s => collect_var_state s
end
with collect_var_state (s:state) :=
match s with SA x xl => (fold_left (fun acc y => acc++ collect_var_basic y) x [])++(fold_left (fun acc yb =>
match yb with (yl,b) => acc++((fold_left (fun acc b => acc++(collect_var_basic b)) yl []))++(collect_var_state b) end) xl [])
| ket b => collect_var_bexp b
| qket p b => collect_var_aexp p ++ collect_var_bexp b
| SITE x y z => (collect_var_bexp x)++(collect_var_state y)++(collect_var_state z)
| SPlus s1 s2 => (collect_var_state s1)++(collect_var_state s2)
| Join s1 s2 => (collect_var_state s1)++(collect_var_state s2)
| upP s1 p => (collect_var_state s1)++(collect_var_aexp p)
| Tensor sl => (fold_left (fun acc b => acc++(collect_var_state b)) sl [])
| Sigma n i b s => (collect_var_aexp n)++(collect_var_aexp b)++(diff (collect_var_state s) [i])
| NTensor n i b s => (collect_var_aexp n)++(collect_var_aexp b)++(diff (collect_var_state s) [i])
end.
(*Pattern for walk. goto is describing matching patterns such as
match |01> -> |10> | |00> -> |11> ...
three type restriction:
1.left-hand and right hand must have the same number of bits.
2. the number of cases are exactly 2^n where n is the bit number.
3. only permutation, both the left and right bitstrings must be distinct. *)
Inductive numvar := NNum (n:nat) | NVar (x:var) | NFunApp (x:var) (y:var).
Definition rz_val := nat.
Definition addto (r : rz_val) (n : nat) (rmax : nat) : rz_val :=
(r + 2^(rmax - n)) mod 2^rmax.
Definition addto_n (r : rz_val) n (rmax : nat) :=
(r + 2^rmax - 2^(rmax - n)) mod 2^rmax.
Definition rotate (r :rz_val) (q:nat) rmax := addto r q rmax.
(* Quantum State *)
Definition qpred := list (list var * state).
Inductive var_sub := SVar (x:var) | Subs (x:var_sub) (a:vari) (s:state).
Inductive cpred_elem := PFalse | CState (b:bexp)
| QState (x:state) (s:state)
| QIn (p:aexp) (x:aexp) (s:state) (* (p,x) \in Sigma s. *)
| PNot (p:cpred_elem) | CForall (xs:list var) (p1:list cpred_elem) (p2:cpred_elem)
| Valid (range:bexp) (b:bexp).
Definition cpred := list cpred_elem.
Definition fresh (l:nat) := l +1.
(* compilation to Z3. *)
Inductive z3_exp := z3_var (x:var)
| z3_bit (n:ze_qubit_elem)
| Pair (a:ze_qubit_elem) (z2:ze_qubit_elem)
| ite (b:z3_pred) (l:z3_exp) (r:z3_exp)
| lambdaITE (x:var) (b:z3_pred) (l:z3_exp) (r:z3_exp)
| zread (a:z3_exp) (b:aexp)
| zwrite (a:z3_exp) (n:aexp) (v:z3_exp)
| zset (a:z3_exp) (p:aexp) (v:z3_exp) (s:aexp)
| zsetInf (a:z3_exp) (p:aexp) (v:z3_exp)
| zcopy (a:z3_exp) (p:aexp) (b:z3_exp) (q:z3_exp) (s:aexp)
| zcopyInf (a:z3_exp) (p:aexp) (b:z3_exp) (q:z3_exp)
| intRead (x:z3_exp) (a:aexp) | intValue (n:aexp)
with z3_pred := ztrue | zfalse
| zqeq (a:z3_exp) (b:z3_exp)
| zeq (a:aexp) (b:aexp)
| zle (a:aexp) (b:aexp) | zlt (a:aexp) (b:aexp)
| znot (a:z3_pred) | zand (a:z3_pred) (b:z3_pred)
| zor (a:z3_pred) (b:z3_pred)
| zimply (a:z3_pred) (b:z3_pred)
| zforall (x:var) (a:z3_pred)
with ze_qubit_elem := znone | zsome (n:aexp) | elem_var (x:var)
| zget (a:z3_exp) (b:aexp) (c:z3_exp) | ztimes (n1:aexp) (z:ze_qubit_elem).
(*
Definition write_left (a:z3_exp) (n:aexp) (v:aexp) := zwrite a n (Pair ((zsome v)) (zget a n (intValue (BA (Num 1))))).
Definition write_right (a:z3_exp) (n:aexp) (v:aexp) := zwrite a n (Pair (zget a n (intValue (BA (Num 0)))) ( (zsome v))).
Axiom var_num_map : var -> nat.
Axiom encode_fexp : fexp -> aexp.
Definition fresh (l:nat) := l +1.
*)
(*
Definition elem_diff x n y m u v :=
zforall u (zforall v (zimply (zand (zand (zle (z3_plus x (z3_ba (Num 0))) (z3_ba (Var u)))
(zlt (z3_ba (Var u)) (z3_plus x n)))
(zand (zle (z3_plus y (z3_ba (Num 0))) (z3_ba (Var v)))
(zlt (z3_ba (Var v)) (z3_plus y m)))) (znot (zeq (z3_ba (Var u)) (z3_ba (Var v)))))).
Definition set_diff :var := 1.
Fixpoint set_elem_diff_aux (x:var) (l:list var) (freshs:nat) :=
match l with [] => (ztrue,freshs)
| y::ys => let u := fresh freshs in let v := fresh (fresh freshs) in
match (set_elem_diff_aux x ys (fresh (fresh freshs))) with (next1,fre) =>
(zand (elem_diff (z3_ba (Var (var_map x))) (z3_ba (Var (var_map y)))
(z3_ba (Num (var_num_map x))) (z3_ba (Num (var_num_map y))) u v) next1,fre)
end
end.
Fixpoint set_elem_diff (l:list var) (freshs:nat) :=
match l with [] => ztrue
| (x::xs) =>
match set_elem_diff_aux x xs freshs with (new,fre) =>
zand new (set_elem_diff xs fre)
end
end.
*)
(*
Definition subst_basic (v:basic) (x:var) (i:nat) :=
match v with Var y => if x =? y then Num i else Var y
| Num a => Num a
end.
Fixpoint subst_aexp (a:aexp) (x:var) (i:nat) :=
match a with BA b => BA (subst_basic b x i)
| APlus e1 e2 => APlus (subst_aexp e1 x i) (subst_aexp e2 x i)
| AMinus e1 e2 => AMinus (subst_aexp e1 x i) (subst_aexp e2 x i)
| AMult e1 e2 => AMult (subst_aexp e1 x i) (subst_aexp e2 x i)
| TwoTo e1 => TwoTo (subst_aexp e1 x i)
| XOR e1 e2 => XOR (subst_aexp e1 x i) (subst_aexp e2 x i)
| Index y a => if y =? x then Index y a else Index y (subst_aexp a x i)
end.
Definition trans_qubit (v:state) (x:z3_exp) (i:aexp) :=
match v with ket a => Some (ite (zeq (a) ((BA (Num 0))))
(zwrite ( x) i (Pair (zsome (BA (Num 1))) znone))
(zwrite ( x) i (Pair znone (zsome (BA (Num 1))))), ztrue)
| qket p a => Some (ite (zeq ( a) ( (BA (Num 0))))
(zwrite ( x) i (Pair (zsome (encode_fexp p)) znone))
(zwrite ( x) i (Pair znone (zsome (encode_fexp p)))),ztrue)
| SPlus (qket p a) (qket q b) =>
Some (zwrite ( x) i (Pair (zsome (encode_fexp p)) (zsome (encode_fexp q))),
(zand (zeq ( a) ( (BA (Num 0))))
(zeq ( b) ( (BA (Num 1))))))
| Sigma (BA (Num 2)) j b (ket a) =>
Some (zwrite ( x) i (Pair (zsome (BA (Num 1))) (zsome (BA (Num 1)))),
(zand (zeq ( (subst_aexp a j 0)) ( (BA (Num 0))))
(zeq ( (subst_aexp a j 1)) ( (BA (Num 1))))))
| Sigma (BA (Num 2)) j b (qket p a) =>
Some (zwrite ( x) i (Pair (zsome (encode_fexp p)) (zsome (encode_fexp p))),
(zand (zeq ( (subst_aexp a j 0)) ( (BA (Num 0))))
(zeq ( (subst_aexp a j 1)) ( (BA (Num 1))))))
| _ => None
end.
Definition trans_qubit_one (v:state) (x:z3_exp) (i:aexp) (y:z3_exp) (ind:var) (m:nat) :=
match v with ket a => Some (zwrite y i (z3_bit (zget x i (intValue (subst_aexp a ind m)))))
| qket p a => Some (zwrite y i (z3_bit (ztimes (encode_fexp p) (zget x i (intValue (subst_aexp a ind m))))))
| _ => None
end.
Fixpoint trans_tensor' (v:state) (x:z3_exp) (i:aexp) (yh:z3_exp) :=
match v with NTensor h y l s =>
match trans_qubit s x (BA (Var y)) with None => None
| Some (ps,pr) => Some ((lambdaITE y (zand (zle ( i) ( (BA (Var y)))) (zlt ( (BA (Var y))) ( h)))
ps (zread x (BA (Var y)))), zand pr (zeq ( i) ( l)),h)
end
| Tensor s1 s2 => match trans_tensor' s1 x i yh with None => None
| Some (p1,pr1,h1) =>
match trans_tensor' s2 p1 h1 yh with None => None
| Some (p2,pr2,h2) =>
Some (p2, zand pr1 pr2, h2)
end
end
| Sigma (BA (Num 2)) j b (NTensor h k l s) =>
match trans_qubit_one s x (BA (Var k)) yh j 0 with None => None
| Some p1 =>
match trans_qubit_one s x (BA (Var k)) yh j 1 with None => None
| Some p2 => Some (lambdaITE k (zand (zle i (BA (Var k))) (zlt ( (BA (Var k))) ( h)))
(ite (zeq (BA (Var j)) (BA (Num 0))) p1 p2)
(zread yh (BA (Var k))), (zeq ( i) ( l)),h)
end
end
| a => match trans_qubit a x i with None => None | Some (p,pr) => Some (p,pr,APlus i (BA (Num 1))) end
end.
Definition trans_tensor (v:state) (x:z3_exp) (n:nat) (yh:var) :=
match trans_tensor' v x (BA (Num 0)) (z3_var yh) with None => None
| Some (p,pr,h) => Some (p,zand pr (zeq ( h) ( (BA (Num n)))),h)
end.
Definition is_tensor (v:state) := match v with NTensor h y l s => true | Tensor s1 s2 => true | _ => false end.
Definition trans_sigma (v:state) (x:var) (n:nat) (y:var) (z:var) (fresh:var) :=
match v with | Sigma (TwoTo q) j b s =>
let u := fresh in let v := fresh+1 in let w := fresh+2 in
Some (z3_var z, zforall u (zforall v (zimply (zand (zand (zle (BA (Num 0)) (BA (Var v))) (zlt (BA (Var v)) q))
(zor (zqeq ( (intRead (z3_var u) (BA (Var v)))) ( (intValue (BA (Num 0)))))
(zqeq ( (intRead (z3_var u) (BA (Var v)))) ( (intValue (BA (Num 1)))))))
(zqeq (lambdaITE w ((zand (zle (BA (Num 0)) (BA (Var v))) (zlt (BA (Var v)) q)))
(zread (z3_var z) (BA (Var w)))
(zread (z3_var z) (BA (Num 0))))
(lambdaITE w ((zand (zle (BA (Num 0)) (BA (Var v))) (zlt (BA (Var v)) q)))
(z3_bit (zget (z3_var x) (BA (Var w)) (intRead (z3_var u) (BA (Var w)))))
(zread (z3_var x) (BA (Num 0))))))), fresh+3)
| a => match trans_tensor a (z3_var x) n y with None => None
| Some (p,pr,h) => Some (p,pr,fresh)
end
end.
*)
(*
| NTensor n i b s =>
| Sigma n i b s =>
| STrue (* meaning that the initial state with any possible values. *)
| ket (b:aexp) (*normal state |0> false or |1> true *)
| qket (p:fexp) (b:aexp)
| SPlus (s1:state) (s2:state) (* Let's say that we only allow |0> + |1> first. *)
| Tensor (s1:state) (s2:state) (* |x> + |y> state. x and y are not equal *)
(* | Plus (s1:state) (s2:state) |x> + |y> state. x and y are not equal *)
| Sigma (n:aexp) (i:var) (b:aexp) (s:state) (* represent 1/sqrt{2^n} Sigma^n_{i=b} s *)
| NTensor (n:aexp) (i:var) (b:aexp) (s:state) (* represent Tensor^n_{i=b} s *).
Inductive aexp := BA (b:basic) | APlus (e1:aexp) (e2:aexp) | AMinus (e1:aexp) (e2:aexp) | AMult (e1:aexp) (e2:aexp)
| TwoTo (e1:basic) | XOR (e1:aexp) (e2:aexp) | Index (x:var) (a:aexp).
*)