Merge branch 'main' of github.com:Qbricks/qbricks.github.io into main

Qbricks · Mar 7, 2023 · 4afdf06 · 4afdf06
2 parents 7417c21 + ae0efbb
commit 4afdf06
Show file tree

Hide file tree

Showing 210 changed files with 282,869 additions and 46,501 deletions.
diff --git a/Case_studies/Shor/no_anc_shor_circ.mlw b/Case_studies/Shor/no_anc_shor_circ.mlw
@@ -321,7 +321,8 @@ let ghost function ket_with_ancs (i:int)
 let function modular_multiplier(p:int) :circuit
                                           requires{0< p < bound}
                                           requires{co_prime p  bound}
-             ensures{forall i. 0<=i < bound  ->
+                                          ensures{ancilla_free result}
+                                          ensures{forall i. 0<=i < bound  ->
                      path_sem result  (ket_with_ancs i)  = ket_with_ancs (mod (p * i) bound)}
               ensures{width result = 2*n+4}
   =
@@ -364,10 +365,12 @@ let function modular_multiplier(p:int) :circuit
               assert{forall i. 0<=i < bound ->
                      path_sem c (kronecker  (ket (n+1) i)  (kronecker (ket (n+2) 0) (ket 1 0))) = kronecker  (ket (n+1) (mod (p * i) bound ))  (kronecker (ket (n+2) 0) (ket 1 0))};
               assert{width c = 2*n+4};
+              assert{ancilla_free c};                      
               c := with_permutation c (fun i -> if i< 1 then i + (2*n+4)-1 else  i - 1) ;
               assert{forall i. 0<=i < bound ->
                      path_sem c (kronecker (kronecker  (ket n i)   (ket (n+3) 0) ) (ket 1 0)) = (kronecker (kronecker  (ket n (mod (p * i) bound ))  ( ket (n+3) 0)) (ket 1 0)) };
               assert{width c = 2*n+4};
+              assert{ancilla_free c};                      
               c
 
 let ghost function reg_final

diff --git a/Case_studies/Shor/no_anc_shor_circ/why3session.xml b/Case_studies/Shor/no_anc_shor_circ/why3session.xml
diff --git a/Case_studies/Shor/no_anc_shor_circ/why3session.xml.bak b/Case_studies/Shor/no_anc_shor_circ/why3session.xml.bak
diff --git a/Case_studies/Shor/no_anc_shor_circ/why3shapes.gz b/Case_studies/Shor/no_anc_shor_circ/why3shapes.gz
diff --git a/Case_studies/Shor/no_anc_shor_circ/why3shapes.gz.bak b/Case_studies/Shor/no_anc_shor_circ/why3shapes.gz.bak
diff --git a/Case_studies/Shor/shor_circ.mlw b/Case_studies/Shor/shor_circ.mlw
@@ -57,10 +57,7 @@ module Circuit
          use qdata.Sqrt_two
          use qdata.Ket_basis
          use qft.Rev_qft
-
-type shor_ = {composite:int; compos_log : int; picked : int}
-               invariant{0<compos_log /\  1< picked < composite /\power 2 (compos_log-1)<= composite < power 2 compos_log /\co_prime picked composite /\0< compos_log}
-               by{composite = 5; compos_log =3 ; picked =3}
+         use shor_type.Shor_type
 
  val constant s() : ref shor_
 let constant  bound= !(s()).composite   

diff --git a/Case_studies/Shor/shor_circ/why3session.xml b/Case_studies/Shor/shor_circ/why3session.xml
diff --git a/Case_studies/Shor/shor_circ/why3session.xml.bak b/Case_studies/Shor/shor_circ/why3session.xml.bak
diff --git a/Case_studies/Shor/shor_circ/why3shapes.gz b/Case_studies/Shor/shor_circ/why3shapes.gz
diff --git a/Case_studies/Shor/shor_circ/why3shapes.gz.bak b/Case_studies/Shor/shor_circ/why3shapes.gz.bak
diff --git a/Case_studies/Shor/shor_inst/why3shapes.gz b/Case_studies/Shor/shor_inst/why3shapes.gz
diff --git a/Case_studies/Shor/shor_spec/why3session.xml b/Case_studies/Shor/shor_spec/why3session.xml
diff --git a/Case_studies/Shor/shor_spec/why3session.xml.bak b/Case_studies/Shor/shor_spec/why3session.xml.bak
diff --git a/Case_studies/Shor/shor_spec/why3shapes.gz b/Case_studies/Shor/shor_spec/why3shapes.gz
diff --git a/Case_studies/Shor/shor_spec/why3shapes.gz.bak b/Case_studies/Shor/shor_spec/why3shapes.gz.bak
diff --git a/Case_studies/Shor/shor_type/why3shapes.gz b/Case_studies/Shor/shor_type/why3shapes.gz
diff --git a/Case_studies/deutsch-jozsa/why3session.xml b/Case_studies/deutsch-jozsa/why3session.xml
diff --git a/Case_studies/deutsch-jozsa/why3session.xml.bak b/Case_studies/deutsch-jozsa/why3session.xml.bak
diff --git a/Case_studies/deutsch-jozsa/why3shapes.gz b/Case_studies/deutsch-jozsa/why3shapes.gz
diff --git a/Case_studies/grover/why3session.xml b/Case_studies/grover/why3session.xml
diff --git a/Case_studies/grover/why3session.xml.bak b/Case_studies/grover/why3session.xml.bak
diff --git a/Case_studies/grover/why3shapes.gz b/Case_studies/grover/why3shapes.gz
diff --git a/Case_studies/modular_adder/why3session.xml b/Case_studies/modular_adder/why3session.xml
diff --git a/Case_studies/modular_adder/why3session.xml.bak b/Case_studies/modular_adder/why3session.xml.bak
diff --git a/Case_studies/modular_adder/why3shapes.gz b/Case_studies/modular_adder/why3shapes.gz
diff --git a/Case_studies/modular_adder/why3shapes.gz.bak b/Case_studies/modular_adder/why3shapes.gz.bak
diff --git a/Case_studies/modular_multiplier/why3session.xml b/Case_studies/modular_multiplier/why3session.xml
diff --git a/Case_studies/modular_multiplier/why3session.xml.bak b/Case_studies/modular_multiplier/why3session.xml.bak
diff --git a/Case_studies/modular_multiplier/why3shapes.gz b/Case_studies/modular_multiplier/why3shapes.gz
diff --git a/Case_studies/modular_multiplier/why3shapes.gz.bak b/Case_studies/modular_multiplier/why3shapes.gz.bak
diff --git a/Case_studies/qft.mlw b/Case_studies/qft.mlw
@@ -641,7 +641,7 @@ let function apply_from_qft_zero_path (n k:int)(c:circuit):circuit
                                                         ensures{size result <= polysquare n   (cont_size*2)   0 0 + size c}
                                                         ensures{ancillas result = ancillas c}
                                                         ensures{width result = n+k}
-                                                        ensures{forall y z:matrix complex. forall i:int.  is_a_ket_l y k ->is_a_ket_l z k ->
+                                                        ensures{forall y z:matrix complex. forall i:int. 0<=i < power 2 n ->    is_a_ket_l y k ->is_a_ket_l z k ->
                                                                                                     path_sem c (kronecker (ket n (mod i (power 2 n))) y) = (kronecker (ket n (mod i (power 2 n))) z)
                                                                                                     -> path_sem result (kronecker (apply_qft n i) y) = (kronecker (apply_qft n i) z)}
   = apply_from_qft_zero n k c
@@ -656,7 +656,7 @@ let function apply_in_qft_zero_path (n k:int)(c:circuit):circuit
                                                       ensures{forall y z:matrix complex. forall i:int. 0<=i < power 2 n ->  is_a_ket_l y k ->is_a_ket_l z k ->
                                                                                                   path_sem c (kronecker (apply_qft n i) y) = (kronecker (apply_qft n i) z)
                                                                                                   -> path_sem result (kronecker (ket n i) y) = (kronecker (ket n i) z)}
-  = apply_from_qft_zero n k c
+  = apply_in_qft_zero n k c
 
 end
 

diff --git a/Case_studies/qft/why3session.xml b/Case_studies/qft/why3session.xml
diff --git a/Case_studies/qft/why3session.xml.bak b/Case_studies/qft/why3session.xml.bak
diff --git a/Case_studies/qft/why3shapes.gz b/Case_studies/qft/why3shapes.gz
diff --git a/Case_studies/qft/why3shapes.gz.bak b/Case_studies/qft/why3shapes.gz.bak
diff --git a/Case_studies/qft_test.mlw b/Case_studies/qft_test.mlw
@@ -74,7 +74,8 @@ let qft ( n:int) :circuit
             ensures{forall x y. ang_ind result x y  = (ind_isum(fun k ->
                    (ind_isum (fun l -> x l * y k * power 2 (n-l - 1+k)) k n))0 n) /./ n}          
   end
-
+use binary.Binary_Op
+
 let qft_d ( n:int) :circuit
                       requires{0<n}
   =
@@ -85,8 +86,8 @@ let qft_d ( n:int) :circuit
             invariant{width !c = n}
               invariant{0<= !q<=n}
               invariant{range !c = !q}
-              invariant{forall x y i. 0<= i < n -> basis_ket !c x y i = if 0<= i < !q then y i else x i}
-              invariant{forall x y. ang_ind !c x y = (ind_isum(fun k -> (ind_isum (fun l -> x l * y k * power 2 (n-l - 1+k)) k n))0 !q) /./ n}
+              invariant{forall x y i. binary_l x n -> binary_l y (!q) -> 0<= i < n -> basis_ket !c x y i = if 0<= i < !q then y i else x i}
+              invariant{forall x y. binary_l x n -> binary_l y (!q) -> ang_ind !c x y = (ind_isum(fun k -> (ind_isum (fun l -> x l * y k * power 2 (n-l - 1+k)) k n))0 !q) /./ n}
               variant{n- !q}
               begin
                 let i = ref (!q+1)
@@ -95,24 +96,24 @@ let qft_d ( n:int) :circuit
                         invariant{width !cl = n}
                           invariant{!q< !i<=n}
                           invariant{range !cl = 0}
-                          invariant{forall x y i. 0<= i < n -> basis_ket !cl x y i = x i}
-                          invariant{forall x y. ang_ind !cl x y = (ind_isum (fun l -> x l * x !q * power 2 (n- l -1+ !q)) (!q+1) !i) /./n}
+                          invariant{forall x y i.binary_l x n ->  0<= i < n -> basis_ket !cl x y i = x i}
+                          invariant{forall x y. binary_l x n -> ang_ind !cl x y = (ind_isum (fun l -> x l * x !q * power 2 (n- l -1+ !q)) (!q+1) !i) /./n}
                           variant{n- !i}
                           cl := seq_diag !cl  (crz !i (!q) (!i - !q+1) n );
                         i := !i +1
                       done;
                       cl:=  seq_diag_right (place_hadamard (!q) n)  !cl;
-                      assert{forall x y i. 0<= i < n -> basis_ket !cl x y i = if i = !q then y 0 else x i};
-                      assert{forall x y. ang_ind !cl x y = (ind_isum (fun l -> x l * y 0 * power 2 (n-l - 1+ !q)) !q n) /./ n};
+                      assert{forall x y i. 0<= i < n -> binary_l x n -> binary_l y 1-> basis_ket !cl x y i = if i = !q then y 0 else x i};
+                      assert{forall x y. binary_l x n ->  binary_l y 1 -> ang_ind !cl x y = (ind_isum (fun l -> x l * y 0 * power 2 (n-l - 1+ !q)) !q n) /./ n};
                       c:= !c -- !cl;
                       q := !q+1
               end
           done;
           return (!c)
             ensures{width result = n}
             ensures{range result = n}
-            ensures{forall x y i. 0<= i < n -> basis_ket result x y i = y i}
-            ensures{forall x y. ang_ind result x y  = (ind_isum(fun k -> (ind_isum (fun l -> x l * y k * power 2 (n-l - 1+k)) k n))0 n) /./ n}
+            ensures{forall x y i. 0<= i < n ->binary_l x n ->  binary_l y n -> basis_ket result x y i = y i}
+            ensures{forall x y. binary_l x n -> binary_l y n -> ang_ind result x y  = (ind_isum(fun k -> (ind_isum (fun l -> x l * y k * power 2 (n-l - 1+k)) k n))0 n) /./ n}
 
   end