Theory Collision
section ‹‹Collision› – Invariant preservation for collision resistance›
theory Collision imports
CO_Invariants
Oracle_Programs
Aux_Sturm_Calculation
begin
context compressed_oracle begin
definition ‹no_collision = {(x,y,D::'x⇀'y). inj_map D}›
definition ‹no_collision' = {D::'x⇀'y. inj_map D}›
lemma no_collision_no_collision': ‹no_collision = UNIV × UNIV × no_collision'›
by (auto intro!: simp: no_collision_def no_collision'_def)
lemma ket_invariant_no_collision_no_collision': ‹ket_invariant no_collision = ⊤ ⊗⇩S ⊤ ⊗⇩S ket_invariant no_collision'›
by (auto simp: ket_invariant_tensor no_collision_no_collision' simp flip: ket_invariant_UNIV)
text ‹We show the preservation of the \<^const>‹no_collision› invariant.
We show it with respect to the oracle \<^const>‹query› first.›
lemma preserves_no_collision: ‹preserves_ket query (no_collision ∩ num_queries q) no_collision (6 * sqrt q / sqrt N)›
proof -
define K where ‹K = (λ(x::'x,D0::'x⇀'y). ket_invariant {(x, y, D0(x:=d)) | (y::'y) d.
D0 x = None ∧ card (dom D0) ≤ q ∧ inj_map D0})›
define I1 J1 :: ‹('x⇀'y) ⇒ ('y × 'y option) set›
where ‹I1 D0 = UNIV × (if card (dom D0) ≤ q then - Some ` ran D0 else {})›
and ‹J1 D0 = (UNIV × - Some ` ran D0)›
for D0 :: ‹'x ⇀ 'y›
show ?thesis
proof (rule inv_split_reg_query[where X=‹reg_1_3› and Y=‹reg_2_3› and H=‹reg_3_3› and K=K
and ?I1.0=‹λ(x,D0). ket_invariant (I1 D0)› and ?J1.0=‹λ(x,D0). ket_invariant (J1 D0)›])
show ‹query = (reg_1_3;(reg_2_3;reg_3_3)) query›
by (auto simp: reg_1_3_def reg_2_3_def reg_3_3_def pair_Fst_Snd)
show ‹compatible reg_1_3 reg_2_3› ‹compatible reg_1_3 reg_3_3› ‹compatible reg_2_3 reg_3_3›
by simp_all
show ‹compatible_register_invariant reg_2_3 (K xD0)› for xD0
apply (cases xD0)
by (auto simp add: K_def reg_2_3_def
intro!: compatible_register_invariant_Snd_comp compatible_register_invariant_Fst)
show ‹compatible_register_invariant (reg_3_3 o function_at (fst xD0)) (K xD0)› for xD0
apply (cases xD0)
by (auto simp add: K_def reg_3_3_def comp_assoc
intro!: compatible_register_invariant_Snd_comp compatible_register_invariant_Fst
compatible_register_invariant_function_at)
have aux: ‹inj_map b ⟹
card (dom b) ≤ q ⟹
∃ba. (card (dom ba) ≤ q ⟶
(∃d. b = ba(a := d)) ∧ ba a = None ∧ inj_map ba ∧ b a ∉ Some ` ran ba) ∧
card (dom ba) ≤ q› for b a
apply (intro exI[of _ ‹b(a:=None)›] exI[of _ ‹b a›] impI conjI)
apply fastforce
apply force
apply (smt (verit, ccfv_SIG) array_rules(2) inj_map_def)
apply (auto simp: ran_def inj_map_def)[1]
by (simp add: dom_fun_upd card_Diff1_le[THEN order_trans])
show ‹ket_invariant (no_collision ∩ num_queries q)
≤ (SUP xD0∈UNIV. K xD0 ⊓ lift_invariant (reg_2_3;reg_3_3 ∘ function_at (fst xD0)) (case xD0 of (x, D0) ⇒ ket_invariant (I1 D0)))›
by (auto intro!: aux simp add: K_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter ket_invariant_SUP[symmetric] I1_def
lift_inv_prod lift_invariant_comp lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv case_prod_beta
no_collision_def num_queries_def)
have aux: ‹d ∉ Some ` ran (snd xD0) ⟹ inj_map (snd xD0) ⟹ inj_map ((snd xD0)(fst xD0 := d))› for d xD0
by (smt (verit, del_insts) fun_upd_other fun_upd_same image_iff inj_map_def not_Some_eq ranI)
show ‹K xD0 ⊓ lift_invariant (reg_2_3;reg_3_3 ∘ function_at (fst xD0)) (case xD0 of (x, D0) ⇒ ket_invariant (J1 D0))
≤ ket_invariant no_collision› for xD0
apply (simp add: K_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter
ket_invariant_SUP[symmetric] J1_def lift_inv_prod lift_invariant_comp
lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv case_prod_beta)
unfolding no_collision_def
using aux[of _ xD0] by auto
have aux: ‹b aa = None ⟹
ba aa = None ⟹
b ≠ ba ⟹
card (dom b) ≤ q ⟹
inj_map b ⟹ card (dom ba) ≤ q ⟹ inj_map ba ⟹ b(aa := d) ≠ ba(aa := da)›
for aa b ba d da
by (metis fun_upd_triv fun_upd_upd)
have aux: ‹⋀b aa ba d da.
b(aa := d) = ba(aa := da) ⟹
b aa = None ⟹
ba aa = None ⟹
b ≠ ba ⟹
card (dom b) ≤ q ⟹
inj_map b ⟹ card (dom ba) ≤ q ⟹ inj_map ba ⟹ False›
by (metis fun_upd_triv fun_upd_upd)
show ‹orthogonal_spaces (K xD0) (K xD0')› if ‹xD0 ≠ xD0'› for xD0 xD0'
apply (cases xD0; cases xD0')
unfolding K_def using that by (auto elim!: aux)
have ‹preserves_ket query1 (I1 D0) (J1 D0) (6 * sqrt q / sqrt N)› for D0 :: ‹'x⇀'y›
proof (cases ‹card (dom D0) ≤ q›)
case True
have [simp]: ‹card (ran D0) ≤ q›
using True ran_smaller_dom[of D0] by simp
show ?thesis
apply (simp add: I1_def J1_def True)
apply (rule preserve_query1_simplified)
by (auto simp add: inj_vimage_image_eq vimage_Compl)
next
case False
then show ?thesis
unfolding I1_def by simp
qed
then show ‹preserves query1 (case xD0 of (x, D0) ⇒ ket_invariant (I1 D0)) (case xD0 of (x::'x, D0) ⇒ ket_invariant (J1 D0)) (6 * sqrt q / sqrt N)› for xD0
apply (cases xD0) by auto
show ‹6 * sqrt q / sqrt N ≥ 0›
by auto
show ‹K xD0 ≤ lift_invariant reg_1_3 (ket_invariant {fst xD0})› for xD0
apply (cases xD0)
by (auto simp add: K_def reg_1_3_def lift_Fst_ket_inv)
qed simp
qed
text ‹Like @{thm [source] preserves_no_collision} but with respect to the oracle \<^const>‹query›.›
lemma preserves_no_collision': ‹preserves_ket query' (no_collision ∩ num_queries q) no_collision (5 * sqrt q / sqrt N)›
proof -
define K where ‹K = (λ(x::'x,D0::'x⇀'y). ket_invariant {(x, y, D0(x:=d)) | (y::'y) d.
D0 x = None ∧ card (dom D0) ≤ q ∧ inj_map D0})›
define I1 J1 :: ‹('x⇀'y) ⇒ ('y × 'y option) set›
where ‹I1 D0 = UNIV × (if card (dom D0) ≤ q then - Some ` ran D0 else {})›
and ‹J1 D0 = (UNIV × - Some ` ran D0)›
for D0 :: ‹'x ⇀ 'y›
show ?thesis
proof (rule inv_split_reg_query'[where X=‹reg_1_3› and Y=‹reg_2_3› and H=‹reg_3_3› and K=K
and ?I1.0=‹λ(x,D0). ket_invariant (I1 D0)› and ?J1.0=‹λ(x,D0). ket_invariant (J1 D0)›])
show ‹query' = (reg_1_3;(reg_2_3;reg_3_3)) query'›
by (simp add: reg_1_3_def reg_2_3_def reg_3_3_def pair_Fst_Snd)
show ‹compatible reg_1_3 reg_2_3› ‹compatible reg_1_3 reg_3_3› ‹compatible reg_2_3 reg_3_3›
by simp_all
show ‹compatible_register_invariant reg_2_3 (K xD0)› for xD0
apply (cases xD0)
by (auto simp add: K_def reg_2_3_def
intro!: compatible_register_invariant_Snd_comp compatible_register_invariant_Fst)
show ‹compatible_register_invariant (reg_3_3 o function_at (fst xD0)) (K xD0)› for xD0
apply (cases xD0)
by (auto simp add: K_def reg_3_3_def comp_assoc
intro!: compatible_register_invariant_Snd_comp compatible_register_invariant_Fst
compatible_register_invariant_function_at)
have aux: ‹inj_map b ⟹
card (dom b) ≤ q ⟹
∃ba. (card (dom ba) ≤ q ⟶
(∃d. b = ba(a := d)) ∧ ba a = None ∧ inj_map ba ∧ b a ∉ Some ` ran ba) ∧
card (dom ba) ≤ q› for a b
apply (intro exI[of _ ‹b(a:=None)›] exI[of _ ‹b a›] impI conjI)
apply fastforce
apply force
apply (smt (verit, ccfv_SIG) array_rules(2) inj_map_def)
apply (auto simp: ran_def inj_map_def)[1]
by (simp add: dom_fun_upd card_Diff1_le[THEN order_trans])
show ‹ket_invariant (no_collision ∩ num_queries q)
≤ (SUP xD0∈UNIV. K xD0 ⊓ lift_invariant (reg_2_3;reg_3_3 ∘ function_at (fst xD0)) (case xD0 of (x, D0) ⇒ ket_invariant (I1 D0)))›
by (auto intro!: aux simp add: K_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter ket_invariant_SUP[symmetric] I1_def
lift_inv_prod lift_invariant_comp lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv case_prod_beta
no_collision_def num_queries_def)
show ‹K xD0 ⊓ lift_invariant (reg_2_3;reg_3_3 ∘ function_at (fst xD0)) (case xD0 of (x, D0) ⇒ ket_invariant (J1 D0))
≤ ket_invariant no_collision› for xD0
proof -
have aux: ‹d ∉ Some ` ran (snd xD0) ⟹
snd xD0 (fst xD0) = None ⟹
card (dom (snd xD0)) ≤ q ⟹ inj_map (snd xD0) ⟹ inj_map ((snd xD0)(fst xD0 := d))› for d
by (smt (verit, del_insts) fun_upd_other fun_upd_same image_iff inj_map_def not_Some_eq ranI)
show ?thesis
apply (simp add: K_def lift_Fst_ket_inv reg_1_3_def reg_2_3_def ket_invariant_inter
ket_invariant_SUP[symmetric] J1_def lift_inv_prod lift_invariant_comp
lift_invariant_function_at_ket_inv reg_3_3_def lift_Snd_ket_inv case_prod_beta no_collision_def)
using aux by auto
qed
have aux: ‹b aa = None ⟹ ba aa = None ⟹ b ≠ ba ⟹ b(aa := d) = ba(aa := da) ⟹ False› for aa b ba d da
by (metis fun_upd_triv fun_upd_upd)
show ‹orthogonal_spaces (K xD0) (K xD0')› if ‹xD0 ≠ xD0'› for xD0 xD0'
apply (cases xD0; cases xD0')
unfolding K_def using that aux by auto
have ‹preserves_ket query1' (I1 D0) (J1 D0) (5 * sqrt q / sqrt N)› for D0 :: ‹'x⇀'y›
proof (cases ‹card (dom D0) ≤ q›)
case True
have [simp]: ‹card (ran D0) ≤ q›
using True ran_smaller_dom[of D0] by simp
show ?thesis
apply (simp add: I1_def J1_def True)
apply (rule preserve_query1'_simplified)
by (auto simp add: inj_vimage_image_eq vimage_Compl)
next
case False
then show ?thesis
unfolding I1_def by simp
qed
then show ‹preserves query1' (case xD0 of (x, D0) ⇒ ket_invariant (I1 D0)) (case xD0 of (x::'x, D0) ⇒ ket_invariant (J1 D0)) (5 * sqrt q / sqrt N)› for xD0
apply (cases xD0) by auto
show ‹5 * sqrt q / sqrt N ≥ 0›
by auto
show ‹K xD0 ≤ lift_invariant reg_1_3 (ket_invariant {fst xD0})› for xD0
apply (cases xD0)
by (auto simp add: K_def reg_1_3_def lift_Fst_ket_inv)
qed simp
qed
lemma preserves_no_collision_num: ‹preserves_ket query (no_collision ∩ num_queries q) (no_collision ∩ num_queries (q+1)) (6 * sqrt q / sqrt N)›
apply (subst add_0_right[of ‹6 * sqrt q / sqrt N›, symmetric])
apply (rule preserves_intersect_ket)
apply (rule preserves_no_collision)
apply (rule preserves_mono[OF preserves_num])
by auto
lemma preserves_no_collision'_num: ‹preserves_ket query' (no_collision ∩ num_queries q) (no_collision ∩ num_queries (q+1)) (5 * sqrt q / sqrt N)›
apply (subst add_0_right[of ‹5 * sqrt q / sqrt N›, symmetric])
apply (rule preserves_intersect_ket)
apply (rule preserves_no_collision')
apply (rule preserves_mono[OF preserves_num'])
by auto
subsection ‹Collision-finding is hard for q-query adversaries›
lemma collision_finding_is_hard:
fixes program :: ‹('mem, 'x, 'y) program›
and adv_output :: ‹('x × 'x) update ⇒ 'mem update›
and initial_state
assumes [iff]: ‹valid_program program›
assumes ‹norm initial_state = 1›
assumes [register]: ‹register adv_output›
shows ‹(∑h∈UNIV. ∑(x1,x2)|x1 ≠ x2 ∧ h x1 = h x2. measurement_probability adv_output (exec_program h program initial_state) (x1,x2)) / CARD('x ⇒ 'y)
≤ 12 * (query_count program + 154)^3 / N›
proof -
note [[simproc del: Laws_Quantum.compatibility_warn]]
text ‹In this game based proof, we consider three different quantum memory models:
▪ The one from the statement of the lemma, where the overall quantum state lives in \<^typ>‹'mem›,
and the adversary output register is described by \<^term>‹adv_output›, and the initial state
in \<^term>‹initial_state›. The program \<^term>‹program› assumes this memory model.
▪ The "extra output" (short XO) memory model, where there is an extra auxiliary register ‹aux› of type \<^typ>‹'y×'y›.
The type of the memory is then \<^typ>‹'mem × ('y × 'y)›. (I.e., the extra register is in addition to the content of \<^typ>‹'mem›.)
▪ The "compressed oracle" (short CO) memory model, where additionally to XO, we have an oracle register
that can holds the content of the compressed oracle (or the standard oracle).›
text ‹Since the register \<^term>‹adv_output :: _ ⇒ ('mem ell2 ⇒⇩C⇩L 'mem ell2)› is defined w.r.t. a specific memory,
we define convenience definitions for the same register as it would be accessed in the other memories:›
define adv_output_in_xo :: ‹('x×'x) update ⇒ ('mem×'y×'y) update› where ‹adv_output_in_xo = Fst o adv_output›
define adv_output_in_co :: ‹('x×'x) update ⇒ (('mem×'y×'y) × ('x⇀'y)) update› where ‹adv_output_in_co = Fst o adv_output_in_xo›
text ‹Analogously, we defined the ‹aux›-register and the oracle register in the applicable memories:›
define aux_in_xo :: ‹('y×'y) update ⇒ ('mem×'y×'y) update› where ‹aux_in_xo = Snd›
define aux_in_co :: ‹('y×'y) update ⇒ (('mem×'y×'y) × ('x⇀'y)) update› where ‹aux_in_co = Fst o aux_in_xo›
define oracle_in_co :: ‹('x⇀'y) update ⇒ (('mem×'y×'y) × ('x⇀'y)) update› where ‹oracle_in_co = Snd›
define aao_in_co where ‹aao_in_co = (adv_output_in_co; (aux_in_co; oracle_in_co))›
have [register]: ‹compatible aux_in_co oracle_in_co›
by (simp add: adv_output_in_co_def aux_in_co_def oracle_in_co_def adv_output_in_xo_def aux_in_xo_def)
have [register]: ‹compatible adv_output_in_xo aux_in_xo›
by (simp add: adv_output_in_xo_def aux_in_xo_def)
have [register]: ‹compatible adv_output_in_co aux_in_co›
by (simp add: adv_output_in_co_def aux_in_co_def)
have [register]: ‹compatible adv_output_in_co oracle_in_co›
by (simp add: adv_output_in_co_def oracle_in_co_def)
have [register]: ‹compatible aux_in_xo Fst›
by (simp add: aux_in_xo_def)
have [register]: ‹compatible aux_in_co (Fst o Fst)›
by (simp add: aux_in_co_def)
have [register]: ‹compatible aux_in_co Snd›
by (simp add: aux_in_co_def)
have [register]: ‹register aao_in_co›
by (simp add: aao_in_co_def)
text ‹The initial states in XO/CO are like the original initial state, but with
\<^term>‹ket (0,0)› in ‹aux› and \<^term>‹ket Map.empty› (the fully undefined function) in the oracle register.›
define initial_state_in_xo where ‹initial_state_in_xo = initial_state ⊗⇩s ket ((0,0) :: 'y×'y)›
define initial_state_in_co :: ‹(('mem×'y×'y) × ('x⇀'y)) ell2› where ‹initial_state_in_co = initial_state_in_xo ⊗⇩s ket Map.empty›
text ‹We define an extended program ‹ext_program› that executes \<^term>‹program›, followed by two additional queries to the oracle.
Input register is the adversary output register. Output register is the additional register ‹aux›.
Hence ‹ext_program› is only meaningful in the models XO and CO. (Our definition is for XO.)›
define ext_program where ‹ext_program = lift_program Fst program
@ [QueryStep (adv_output_in_xo o Fst) (aux_in_xo o Fst), QueryStep (adv_output_in_xo o Snd) (aux_in_xo o Snd)]›
have [iff]: ‹valid_program ext_program›
by (auto intro!: valid_program_lift simp add: valid_program_append adv_output_in_xo_def aux_in_xo_def ext_program_def)
text ‹We define the final states of the programs \<^term>‹program› and \<^term>‹ext_program›, in the original model, and in XO, and CO.›
define final :: ‹('x ⇒ 'y) ⇒ 'mem ell2› where ‹final h = exec_program h program initial_state› for h
define xo_ext_final :: ‹('x ⇒ 'y) ⇒ ('mem×'y×'y) ell2› where ‹xo_ext_final h = exec_program h ext_program initial_state_in_xo› for h
define xo_final :: ‹('x ⇒ 'y) ⇒ ('mem×'y×'y) ell2› where ‹xo_final h = exec_program h (lift_program Fst program) initial_state_in_xo› for h
define co_ext_final :: ‹(('mem×'y×'y) × ('x⇀'y)) ell2› where ‹co_ext_final = exec_program_with query' ext_program initial_state_in_co›
define co_final :: ‹(('mem×'y×'y) × ('x⇀'y)) ell2› where ‹co_final = exec_program_with query' (lift_program Fst program) initial_state_in_co›
have [simp]: ‹norm initial_state_in_xo = 1›
by (simp add: initial_state_in_xo_def norm_tensor_ell2 assms)
have norm_initial_state_in_co[simp]: ‹norm initial_state_in_co = 1›
by (simp add: initial_state_in_co_def norm_tensor_ell2)
have norm_co_final[simp]: ‹norm co_final ≤ 1›
unfolding co_final_def
using norm_exec_program_with valid_program_lift ‹valid_program program›
norm_query' register_Fst norm_initial_state_in_co
by smt
text ‹We derive the relationships between the various final states:›
have co_ext_final_prefinal:
‹co_ext_final = (adv_output_in_co o Snd; (aux_in_co o Snd; oracle_in_co)) query' *⇩V
(adv_output_in_co o Fst; (aux_in_co o Fst; oracle_in_co)) query' *⇩V co_final›
by (simp add: co_ext_final_def ext_program_def exec_program_with_append adv_output_in_co_def aux_in_co_def oracle_in_co_def comp_assoc
flip: initial_state_in_co_def co_final_def)
have xo_final_final: ‹xo_final h = final h ⊗⇩s ket (0,0)› for h
by (simp add: xo_final_def final_def initial_state_in_xo_def exec_lift_program_Fst)
have xo_ext_final_xo_final: ‹xo_ext_final h = (adv_output_in_xo o Snd; aux_in_xo o Snd) (function_oracle h) *⇩V
(adv_output_in_xo o Fst; aux_in_xo o Fst) (function_oracle h) *⇩V xo_final h› for h
by (simp add: xo_ext_final_def xo_final_def ext_program_def exec_program_def)
text ‹After executing \<^term>‹program› (in XO), the ‹aux›-register is in state \<^term>‹ket (0,0)›:›
have xo_final_has_y0: ‹dist_inv_avg (adv_output_in_xo;aux_in_xo) (λ_. ket_invariant {(xx,yy). yy = (0,0)}) xo_final = 0›
proof -
have ‹dist_inv_avg aux_in_xo (λ_::'x⇒'y. ket_invariant {(0,0)}) xo_final
≤ dist_inv_avg aux_in_xo (λ_::'x⇒'y. ket_invariant {(0,0)}) (λh. initial_state_in_xo)›
unfolding xo_final_def
apply (subst dist_inv_avg_exec_compatible)
using dist_inv_avg_exec_compatible
by auto
also have ‹… = 0›
by (auto intro!: tensor_ell2_in_tensor_ccsubspace ket_in_ket_invariantI
simp add: initial_state_in_xo_def dist_inv_0_iff distance_from_inv_avg0I aux_in_xo_def lift_Snd_inv)
finally have ‹dist_inv_avg aux_in_xo (λ_. ket_invariant {(0,0)}) xo_final = 0›
by (smt (verit, ccfv_SIG) dist_inv_avg_pos)
then show ?thesis
apply (rewrite at ‹{(xx, yy). yy = (0,0)}› to ‹UNIV × {(0,0)}› DEADID.rel_mono_strong, blast)
apply (subst dist_inv_avg_register_rewrite)
by (simp_all add: lift_inv_prod)
qed
text ‹Same as @{thm [source] xo_final_has_y0}, but in CO:›
have co_final_has_y0: ‹dist_inv aao_in_co (ket_invariant {(x,y,D). y = (0,0)}) co_final = 0›
proof -
have ‹dist_inv aux_in_co (ket_invariant {(0,0)}) co_final
≤ dist_inv aux_in_co (ket_invariant {(0,0)}) initial_state_in_co›
unfolding co_final_def
apply (rule dist_inv_exec'_compatible)
by simp_all
also have ‹… = 0›
by (auto intro!: tensor_ell2_in_tensor_ccsubspace ket_in_ket_invariantI
simp add: initial_state_in_co_def initial_state_in_xo_def dist_inv_0_iff
aux_in_co_def aux_in_xo_def lift_Fst_inv lift_Snd_inv lift_invariant_comp)
finally have ‹dist_inv aux_in_co (ket_invariant {(0,0)}) co_final = 0›
by (smt (verit, best) dist_inv_pos)
then show ?thesis
apply (rewrite at ‹{(xx, yy, D). yy = (0,0)}› to ‹UNIV × {(0,0)} × UNIV› DEADID.rel_mono_strong, blast)
apply (subst dist_inv_register_rewrite)
by (simp_all add: lift_inv_prod aao_in_co_def)
qed
define q where ‹q = query_count program›
text ‹The following term occurs a lot (it's how much the \<^term>‹no_collision› invariant is preserved after running \<^term>‹ext_program›).
So we abbreviate it as ‹d›.›
define d :: real where ‹d = (10/3 * sqrt (q+2)^3 + 20) / sqrt N›
have [iff]: ‹d ≥ 0›
by (simp add: d_def)
have ‹dist_inv oracle_in_co (ket_invariant (no_collision' ∩ num_queries' (q+2))) co_ext_final ≤ 10/3 * sqrt (q+2)^3 / sqrt N›
unfolding co_ext_final_def
proof (rule dist_inv_induct[where g=‹λi::nat. 5 * sqrt i / sqrt N›
and J=‹λi. ket_invariant (no_collision' ∩ num_queries' i)›])
show ‹compatible oracle_in_co Fst›
using oracle_in_co_def by simp
show ‹initial_state_in_co ∈ space_as_set (lift_invariant oracle_in_co (ket_invariant (no_collision' ∩ num_queries' 0)))›
by (auto intro!: tensor_ell2_in_tensor_ccsubspace ket_in_ket_invariantI
simp add: initial_state_in_co_def oracle_in_co_def lift_Snd_ket_inv inj_map_def num_queries'_def
initial_state_in_xo_def tensor_ell2_ket ket_in_ket_invariantI no_collision'_def
simp flip: ket_invariant_tensor)
show ‹ket_invariant (no_collision' ∩ num_queries' (query_count ext_program)) ≤ ket_invariant (no_collision' ∩ num_queries' (q+2))›
by (simp add: q_def ext_program_def)
show ‹valid_program ext_program›
by simp
show ‹preserves ((Fst ∘ X_in_xo;(Fst ∘ Y_in_xo;Snd)) query') (lift_invariant oracle_in_co (ket_invariant (no_collision' ∩ num_queries' i)))
(lift_invariant oracle_in_co (ket_invariant (no_collision' ∩ num_queries' (Suc i)))) (5 * sqrt i / sqrt N)›
if [register]: ‹compatible X_in_xo Y_in_xo› for X_in_xo Y_in_xo i
proof -
from preserves_no_collision'_num
have ‹preserves ((Fst ∘ X_in_xo;(Fst ∘ Y_in_xo;Snd)) query')
(lift_invariant (Fst ∘ X_in_xo;(Fst ∘ Y_in_xo;Snd)) (ket_invariant (no_collision ∩ num_queries i)))
(lift_invariant (Fst ∘ X_in_xo;(Fst ∘ Y_in_xo;Snd)) (ket_invariant (no_collision ∩ num_queries (i+1))))
(5 * sqrt (real i) / sqrt N)›
apply (rule preserves_lift_invariant[THEN iffD2, rotated])
by simp
moreover have ‹lift_invariant (Fst ∘ X_in_xo;(Fst ∘ Y_in_xo;Snd)) (ket_invariant (no_collision ∩ num_queries i))
= lift_invariant oracle_in_co (ket_invariant (no_collision' ∩ num_queries' i))› for i
by (simp add: oracle_in_co_def no_collision_no_collision' num_queries_num_queries' lift_inv_prod Times_Int_Times)
ultimately show ?thesis
by simp
qed
show ‹norm query' ≤ 1›
by simp
show ‹norm initial_state_in_co ≤ 1›
by simp
show ‹(∑i<query_count ext_program. 5 * sqrt i / sqrt N) ≤ 10/3 * sqrt (q+2)^3 / sqrt N›
proof -
have ‹(∑i<q+2. sqrt i) ≤ 2/3 * sqrt (q+2) ^ 3›
by (rule sum_sqrt)
then have ‹(∑i<q+2. 5 * sqrt i / sqrt N) ≤ 5 * (2/3 * sqrt (q+2) ^ 3) / sqrt N›
by (auto intro!: divide_right_mono real_sqrt_ge_zero simp only: simp flip: sum_distrib_left sum_divide_distrib)
also have ‹… = 10/3 * sqrt (q+2)^3 / sqrt N›
by simp
finally
show ‹(∑i<query_count ext_program. 5 * sqrt i / sqrt N) ≤ 10/3 * sqrt (q+2)^3 / sqrt N›
by (simp add: q_def ext_program_def)
qed
qed
then have ‹dist_inv oracle_in_co (ket_invariant no_collision') co_ext_final ≤ 10/3 * sqrt (q+2)^3 / sqrt N›
apply (rule le_back_subst_le)
apply (rule dist_inv_mono)
by auto
then have dist_collision: ‹dist_inv aao_in_co (ket_invariant no_collision) co_ext_final ≤ 10/3 * sqrt (q+2)^3 / sqrt N›
apply (rule le_back_subst)
apply (rule dist_inv_register_rewrite)
by (auto intro!: simp: aao_in_co_def no_collision_no_collision' lift_inv_prod)
have dist_Dxy: ‹dist_inv aao_in_co (ket_invariant {((x1,x2),(y1,y2),D). D x1 = Some y1 ∧ D x2 = Some y2}) co_ext_final ≤ 20 / sqrt N›
proof -
have aao_in_co_decomp: ‹aao_in_co = ((adv_output_in_co o Fst; adv_output_in_co o Snd); ((aux_in_co o Fst; aux_in_co o Snd); oracle_in_co))›
by (simp add: register_pair_Snd register_pair_Fst aao_in_co_def flip: register_comp_pair comp_assoc)
have ‹dist_inv ((adv_output_in_co ∘ Fst;adv_output_in_co ∘ Snd);((aux_in_co ∘ Fst;aux_in_co ∘ Snd);oracle_in_co))
(ket_invariant {((x1, x2), (y1, y2), D). y1 = 0 ∧ y2 = 0}) co_final = 0›
using co_final_has_y0
by (simp add: aao_in_co_decomp case_prod_unfold prod_eq_iff)
then show ?thesis
apply (rewrite at ‹20 / sqrt N› to ‹0 + 20 / sqrt N› DEADID.rel_mono_strong, simp)
unfolding co_ext_final_prefinal aao_in_co_decomp
apply (rule dist_inv_double_query')
by (simp_all add: aao_in_co_decomp)
qed
have ‹dist_inv aao_in_co
(ket_invariant {((x1,x2),(y1,y2),D). inj_map D ∧ D x1 = Some y1 ∧ D x2 = Some y2}) co_ext_final ≤ d› (is ‹?lhs ≤ d›)
proof -
have ‹?lhs = dist_inv aao_in_co (ket_invariant no_collision ⊓ ket_invariant {((x1,x2),(y1,y2),D). D x1 = Some y1 ∧ D x2 = Some y2}) co_ext_final›
apply (rule arg_cong3[where f=dist_inv])
by (auto intro!: simp: no_collision_def ket_invariant_inter)
also have ‹… ≤ sqrt ((dist_inv aao_in_co (ket_invariant no_collision) co_ext_final)⇧2
+ (dist_inv aao_in_co (ket_invariant {((x1,x2),(y1,y2),D). D x1 = Some y1 ∧ D x2 = Some y2}) co_ext_final)⇧2)›
apply (rule dist_inv_intersect)
by auto
also have ‹… ≤ sqrt ((10/3 * sqrt (q+2)^3 / sqrt N)⇧2 + (20 / sqrt N)⇧2)›
apply (rule real_sqrt_le_mono)
apply (rule add_mono)
using dist_collision dist_Dxy
by auto
also have ‹… ≤ (10/3 * sqrt (q+2)^3 + 20) / sqrt N›
apply (rule sqrt_sum_squares_le_sum[THEN order_trans])
by (auto, argo)
finally show ?thesis
by (simp add: d_def)
qed
then have ‹dist_inv aao_in_co (ket_invariant {((x1,x2),(y1,y2),D). x1 ≠ x2 ⟶ y1 ≠ y2}) co_ext_final ≤ d›
apply (rule le_back_subst_le)
apply (rule dist_inv_mono)
by (auto simp: inj_map_def)
then have ‹dist_inv (adv_output_in_co; aux_in_co) (ket_invariant {((x1,x2), (y1,y2)). x1 ≠ x2 ⟶ y1 ≠ y2}) co_ext_final ≤ d›
apply (rule le_back_subst)
apply (rule dist_inv_register_rewrite)
apply (simp, simp)
apply (rewrite at ‹(adv_output_in_co;aux_in_co)› to ‹aao_in_co o (reg_1_3; reg_2_3)› DEADID.rel_mono_strong)
apply (simp add: aao_in_co_def flip: register_comp_pair)
apply (subst lift_invariant_comp, simp)
by (auto intro!: simp: lift_inv_prod' reg_1_3_def reg_3_3_def reg_2_3_def lift_invariant_comp lift_Snd_ket_inv lift_Fst_ket_inv
ket_invariant_inter case_prod_unfold
simp flip: ket_invariant_SUP)
then have *: ‹dist_inv_avg (adv_output_in_xo; aux_in_xo) (λh. ket_invariant {((x1,x2), (y1,y2)). x1 ≠ x2 ⟶ y1 ≠ y2}) xo_ext_final ≤ d›
apply (rule le_back_subst)
unfolding co_ext_final_def xo_ext_final_def
apply (rewrite at ‹(adv_output_in_co;aux_in_co)› to ‹Fst o (adv_output_in_xo;aux_in_xo)› DEADID.rel_mono_strong)
apply (simp add: adv_output_in_co_def aux_in_co_def register_comp_pair)
by (simp add: initial_state_in_co_def dist_inv_exec_query'_exec_fixed)
have ‹dist_inv_avg (adv_output_in_xo; aux_in_xo)
(λh. ket_invariant {((x1,x2), yy). (x1 ≠ x2 ⟶ h x1 ≠ h x2) ∨ yy ≠ (0,0)}) xo_final ≤ d›
proof -
define state2 where ‹state2 h = (adv_output_in_xo o Fst; aux_in_xo o Fst) (function_oracle h) *⇩V xo_final h› for h
have xo_ext_final_state2: ‹xo_ext_final h = (adv_output_in_xo ∘ Snd;aux_in_xo ∘ Snd) (function_oracle h) *⇩V state2 h› for h
using state2_def xo_ext_final_xo_final by presburger
have fo_apply2: ‹(Snd ⊗⇩r Snd) (function_oracle h)* *⇩S ket_invariant {((x1, x2), y1, y2). x1 ≠ x2 ⟶ y1 ≠ y2}
≤ ket_invariant {((x1,x2), (y1,y2)). (x1 ≠ x2 ⟶ y1 ≠ h x2) ∨ y2 ≠ 0}› for h :: ‹'x ⇒ 'y›
proof -
have ‹(Snd ⊗⇩r Snd) (function_oracle h)* *⇩S ket_invariant {((x1, x2), y1, y2). x1 ≠ x2 ⟶ y1 ≠ y2}
= (Snd ⊗⇩r Snd) (function_oracle h) *⇩S ket_invariant {((x1, x2), y1, y2). x1 ≠ x2 ⟶ y1 ≠ y2}›
by (simp add: uminus_y flip: register_adj)
also have ‹… = lift_invariant (Fst ⊗⇩r Fst;Snd ⊗⇩r Snd) (Snd (function_oracle h) *⇩S ket_invariant {((x1, y1), x2, y2). x1 ≠ x2 ⟶ y1 ≠ y2})›
apply (rewrite at ‹(Snd ⊗⇩r Snd)› to ‹(Fst ⊗⇩r Fst; Snd ⊗⇩r Snd) o Snd› DEADID.rel_mono_strong)
apply (simp add: register_pair_Snd compatible_register_tensor)
apply (rewrite at ‹ket_invariant {((x1, x2), y1, y2). x1 ≠ x2 ⟶ y1 ≠ y2}›
to ‹lift_invariant (Fst ⊗⇩r Fst; Snd ⊗⇩r Snd) (ket_invariant {((x1, y1), x2, y2). x1 ≠ x2 ⟶ y1 ≠ y2})› DEADID.rel_mono_strong)
apply (auto intro!: simp: lift_inv_prod' compatible_register_tensor lift_inv_tensor' lift_Fst_ket_inv lift_Snd_ket_inv
ket_invariant_tensor case_prod_unfold ket_invariant_inter
simp flip: ket_invariant_SUP)[1]
by (simp add: o_apply register_image_lift_invariant compatible_register_tensor register_isometry)
also have ‹… = lift_invariant (Fst ⊗⇩r Fst; Snd ⊗⇩r Snd) (ket_invariant {((x1, y1), (x2, y2 + h x2)) | x1 y1 x2 y2. x1 ≠ x2 ⟶ y1 ≠ y2})›
apply (simp add: function_oracle_Snd_ket_invariant)
apply (rule arg_cong[where f=‹λx. lift_invariant _ (ket_invariant x)›])
by (auto simp add: image_iff)
also have ‹… ≤ lift_invariant (Fst ⊗⇩r Fst; Snd ⊗⇩r Snd) (ket_invariant {((x1, y1), (x2, y2)). (x1 ≠ x2 ⟶ y1 ≠ h x2) ∨ y2 ≠ 0})›
proof -
have aux: ‹x1 ≠ x2 ⟹ h x2 ≠ y2 ⟹ y2 + h x2 ≠ 0› for x1 x2 y2
by (metis add_right_cancel y_cancel)
show ?thesis
apply (rule lift_invariant_mono, simp add: compatible_register_tensor)
apply (rule ket_invariant_mono)
using aux by auto
qed
also have ‹… = ket_invariant {((x1, x2), (y1, y2)). (x1 ≠ x2 ⟶ y1 ≠ h x2) ∨ y2 ≠ 0}›
by (auto intro!: simp: lift_inv_prod' compatible_register_tensor lift_inv_tensor' lift_Fst_ket_inv lift_Snd_ket_inv
ket_invariant_tensor case_prod_unfold ket_invariant_inter
simp flip: ket_invariant_SUP)[1]
finally show ?thesis
by -
qed
have fo_apply1: ‹(Fst ⊗⇩r Fst) (function_oracle h)* *⇩S ket_invariant {((x1, x2), (y1, y2)). x1 ≠ x2 ⟶ y1 = h x2 ⟶ y2 ≠ 0}
≤ ket_invariant {((x1,x2), yy). (x1 ≠ x2 ⟶ h x1 ≠ h x2) ∨ yy ≠ (0,0)}› for h :: ‹'x ⇒ 'y›
proof -
have ‹(Fst ⊗⇩r Fst) (function_oracle h)* *⇩S ket_invariant {((x1, x2), (y1, y2)). x1 ≠ x2 ⟶ y1 = h x2 ⟶ y2 ≠ 0}
= (Fst ⊗⇩r Fst) (function_oracle h) *⇩S ket_invariant {((x1, x2), (y1, y2)). x1 ≠ x2 ⟶ y1 = h x2 ⟶ y2 ≠ 0}›
by (simp add: uminus_y flip: register_adj)
also have ‹… = lift_invariant (Snd ⊗⇩r Snd;Fst ⊗⇩r Fst) (Snd (function_oracle h) *⇩S ket_invariant {((x2, y2), (x1, y1)). x1 ≠ x2 ⟶ y1 = h x2 ⟶ y2 ≠ 0})›
apply (rewrite at ‹(Fst ⊗⇩r Fst)› to ‹(Snd ⊗⇩r Snd; Fst ⊗⇩r Fst) o Snd› DEADID.rel_mono_strong)
apply (simp add: register_pair_Snd compatible_register_tensor)
apply (rewrite at ‹ket_invariant {((x1, x2), (y1, y2)). x1 ≠ x2 ⟶ y1 = h x2 ⟶ y2 ≠ 0}›
to ‹lift_invariant (Snd ⊗⇩r Snd; Fst ⊗⇩r Fst) (ket_invariant {((x2, y2), (x1, y1)). x1 ≠ x2 ⟶ y1 = h x2 ⟶ y2 ≠ 0})› DEADID.rel_mono_strong)
apply (auto intro!: simp: lift_inv_prod' compatible_register_tensor lift_inv_tensor' lift_Snd_ket_inv lift_Fst_ket_inv
ket_invariant_tensor case_prod_unfold ket_invariant_inter
simp flip: ket_invariant_SUP)[1]
by (simp_all add: o_apply register_image_lift_invariant compatible_register_tensor register_isometry)
also have ‹… = lift_invariant (Snd ⊗⇩r Snd; Fst ⊗⇩r Fst) (ket_invariant {((x2, y2), (x1, y1 + h x1)) | x1 y1 x2 y2. x1 ≠ x2 ⟶ y1 = h x2 ⟶ y2 ≠ 0})›
apply (simp add: function_oracle_Snd_ket_invariant)
apply (rule arg_cong[where f=‹λx. lift_invariant _ (ket_invariant x)›])
by (auto simp add: image_iff)
also have ‹… ≤ lift_invariant (Snd ⊗⇩r Snd; Fst ⊗⇩r Fst) (ket_invariant {((x2, y2), (x1, y1)). (x1 ≠ x2 ⟶ h x1 ≠ h x2) ∨ (y1,y2) ≠ (0,0)})›
proof -
have aux: ‹y1 + h x2 = 0 ⟹ x1 ≠ x2 ⟹ h x1 = h x2 ⟹ y1 = h x2› for y1 x2 x1
by (metis add_right_cancel y_cancel)
show ?thesis
apply (rule lift_invariant_mono, simp add: compatible_register_tensor)
apply (rule ket_invariant_mono)
using aux by auto
qed
also have ‹… = ket_invariant {((x1,x2), yy). (x1 ≠ x2 ⟶ h x1 ≠ h x2) ∨ yy ≠ (0,0)}›
by (auto intro!: simp: lift_inv_prod' compatible_register_tensor lift_inv_tensor' lift_Snd_ket_inv lift_Fst_ket_inv
ket_invariant_tensor case_prod_unfold ket_invariant_inter
simp flip: ket_invariant_SUP)[1]
finally show ?thesis
by -
qed
from * have ‹dist_inv_avg (adv_output_in_xo; aux_in_xo)
(λh. ket_invariant {((x1,x2), (y1,y2)). (x1 ≠ x2 ⟶ y1 ≠ h x2) ∨ y2 ≠ 0}) state2 ≤ d›
apply (rule le_back_subst_le)
unfolding xo_ext_final_state2[abs_def]
apply (subst dist_inv_avg_apply[where U=‹λh. function_oracle h› and S=‹Snd ⊗⇩r Snd›])
using fo_apply2 by (auto intro!: dist_inv_avg_mono simp: function_oracle_ket_invariant pair_o_tensor simp del: o_apply)
then show ?thesis
apply (rule le_back_subst_le)
unfolding state2_def[abs_def]
apply (subst dist_inv_avg_apply[where U=‹λh. function_oracle h› and S=‹Fst ⊗⇩r Fst›])
using fo_apply1 by (auto intro!: dist_inv_avg_mono simp: function_oracle_ket_invariant pair_o_tensor simp del: o_apply)
qed
then have *: ‹dist_inv_avg (adv_output_in_xo; aux_in_xo)
(λh. ket_invariant {((x1,x2), yy). x1 ≠ x2 ⟶ h x1 ≠ h x2}) xo_final ≤ d›
apply (rule le_back_subst_le)
apply (rule ord_le_eq_trans)
apply (rule dist_inv_avg_mono[where I=‹λh. ket_invariant {((x1,x2), yy). (x1 ≠ x2 ⟶ h x1 ≠ h x2) ∨ yy ≠ (0,0)} ⊓ ket_invariant {(xx,yy). yy=(0,0)}›])
apply (auto simp: ket_invariant_inter)[2]
apply (rule dist_inv_avg_intersect)
apply simp_all[2]
by (fact xo_final_has_y0)
then have ‹dist_inv_avg adv_output_in_xo
(λh. ket_invariant {(x1,x2). x1 ≠ x2 ⟶ h x1 ≠ h x2}) xo_final ≤ d›
apply (subst dist_inv_avg_register_rewrite[where R=‹(adv_output_in_xo; aux_in_xo)› and J=‹λh. ket_invariant {((x1,x2),yy). x1 ≠ x2 ⟶ h x1 ≠ h x2}›])
apply (simp, simp)
apply (rewrite at ‹{((x1,x2),yy). x1 ≠ x2 ⟶ h x1 ≠ h x2}› in for (h) to ‹{(x1,x2). x1 ≠ x2 ⟶ h x1 ≠ h x2} × UNIV› DEADID.rel_mono_strong)
apply fastforce
by (simp add: lift_inv_prod)
then have ‹dist_inv_avg adv_output (λh. ket_invariant {(x1,x2). x1 ≠ x2 ⟶ h x1 ≠ h x2}) final ≤ d›
by (simp add: xo_final_final[abs_def] adv_output_in_xo_def dist_inv_avg_Fst_tensor)
then have ‹(∑h∈UNIV. ∑(x1,x2)|x1 ≠ x2 ∧ h x1 = h x2. measurement_probability adv_output (final h) (x1,x2)) / CARD('x ⇒ 'y) ≤ d⇧2›
unfolding case_prod_unfold prod.collapse
apply (subst dist_inv_avg_measurement_probability)
apply simp
apply (rewrite at ‹- {p. fst p ≠ snd p ∧ h (fst p) = h (snd p)}› in ‹λh. ⌑› to ‹{p. fst p ≠ snd p ⟶ h (fst p) ≠ h (snd p)}› DEADID.rel_mono_strong)
apply blast
by auto
also have ‹d⇧2 ≤ 12 * (q+154)^3 / N›
proof -
define r where ‹r = sqrt q›
have [iff]: ‹r ≥ 0›
using r_def by force
have 1: ‹sqrt (r⇧2 + 2) ≤ r + 2›
apply (rule real_le_lsqrt)
by (simp_all add: power2_sum)
have ‹N * d⇧2 = (10/3 * sqrt (r⇧2+2)^3 + 20)⇧2›
apply (simp add: d_def power_divide of_nat_add r_def) by argo
also have ‹… ≤ (10/3 * (r+2)^3 + 20)⇧2›
using 1 by (auto intro!: power_mono add_right_mono mult_left_mono)
also have ‹… ≤ 12 * (r⇧2+154)^3›
proof -
define f where ‹f r = 12 * (r⇧2+154)^3 - (10/3 * (r+2)^3 + 20)⇧2› for r :: real
have fr: ‹f r ≠ 0› if ‹r ≥ 0› for r :: real
unfolding f_def using that by (rule sturm_calculation)
have f0: ‹f 0 ≥ 0›
by (simp add: f_def power2_eq_square)
have ‹isCont f r› for r
unfolding f_def
by (intro continuous_intros)
have ‹f r ≥ 0› if ‹r ≥ 0› for r :: real
proof (rule ccontr)
assume ‹¬ 0 ≤ f r›
then have ‹∃x≥0. x ≤ r ∧ f x = 0›
apply (rule_tac IVT2[where f=f and a=0 and b=r and y=0])
by (auto intro!: ‹isCont f _› simp: f0 that)
then show False
using fr by blast
qed
then show ?thesis
by (simp add: f_def)
qed
finally show ?thesis
apply (rule_tac mult_left_le_imp_le[where c=‹real N›])
using Nneq0 r_def by force+
qed
finally show ?thesis
by (simp add: final_def q_def)
qed
end
end