swh:1:snp:deb9fd355bffe3d96f042bd4e5113afbb0d7cbb2
Tip revision: 0d55fac6a88ba3c22eb7ed09be1e85ceb220159c authored by Alley Stoughton on 04 April 2021, 17:25:21 UTC
Merge branch '1.0' into aprhl
Merge branch '1.0' into aprhl
Tip revision: 0d55fac
Pr_half.eca
require import AllCore Distr.
type input.
type output.
module type Adv = {
proc main(_:input) : output
}.
lemma equiv_not_pr_half (A<:Adv) (Pre: input -> glob A -> bool) (E: glob A -> output -> bool):
equiv [A.main ~ A.main : ={arg, glob A} /\ Pre arg{1} (glob A){1} ==> E (glob A){1} res{1} = !E (glob A){2} res{2}] =>
forall a &m,
Pre a (glob A){m} =>
Pr[A.main(a) @ &m : true] = 1%r =>
Pr[A.main(a) @ &m : E (glob A) res] = 1%r/2%r.
proof.
move => he a &m hpre hll.
have : Pr[A.main(a) @ &m : E (glob A) res] = Pr[A.main(a) @ &m : !E (glob A) res].
+ by byequiv he => // /#.
by rewrite Pr [mu_not] hll /#.
qed.