Skip to main content

Browse the archive

https://github.com/EasyCrypt/easycrypt
22 January 2022, 00:03:31 UTC
Revision 20a61830f765f48b70031a8e065bb0db0ff723e3 authored by Pierre-Yves Strub on 04 April 2021, 06:42:50 UTC, committed by Pierre-Yves Strub on 04 April 2021, 06:42:50 UTC 
Move to Why3 1.4
1 parent fb59000
Raw File
Tip revision: 20a61830f765f48b70031a8e065bb0db0ff723e3 authored by Pierre-Yves Strub on 04 April 2021, 06:42:50 UTC
Move to Why3 1.4
Tip revision: 20a6183
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.
back to top