swh:1:snp:f686447e80898ff64d6f35af9095157ddc6a18e3
Tip revision: 8e47fe3d10d154d0653552a905fee3a3113265d4 authored by Pierre-Yves Strub on 03 December 2021, 16:11:39 UTC
Fix bug that prevents `rewrite //= in h` to simplify in `h`
Fix bug that prevents `rewrite //= in h` to simplify in `h`
Tip revision: 8e47fe3
PlugAndPray.eca
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2021 - Inria
* Copyright (c) - 2012--2021 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
require import AllCore List Distr.
type tval.
op indices : { tval list | indices <> [] } as indices_not_nil.
abbrev card = size (undup indices).
type tin, tres.
module type Game = {
proc main(x:tin): tres
}.
module Guess (G:Game) = {
proc main(x:tin): tval * tres = {
var o,i;
o <@ G.main(x);
i <$ duniform indices;
return (i,o);
}
}.
lemma PBound (G <: Game )
(phi : (glob G) -> tres -> bool)
(psi : (glob G) -> tres -> tval)
x0 &m:
(forall gG o, phi gG o => psi gG o \in indices) =>
(1%r/card%r) * Pr[G.main(x0) @ &m: phi (glob G) res]
= Pr[Guess(G).main(x0) @ &m:
phi (glob G) res.`2 /\
res.`1 = psi (glob G) res.`2].
proof.
move=> psi_in_indices.
byphoare (_: (glob G) = (glob G){m} /\ x0 = x ==>
phi (glob G) (snd res) /\
res.`1 = psi (glob G) res.`2)=> //.
pose p:= Pr[G.main(x0) @ &m: phi (glob G) res].
proc.
seq 1: (phi (glob G) o)
(p) (1%r/card%r)
_ 0%r => //.
(* FIXME: This is more verbose than it should be! *)
+ call (: (glob G) = (glob G){m} /\ x = x0 ==> phi (glob G) res) => //.
bypr=> &m0 @/p [#] eq_globs ->.
byequiv (: ={glob G, x} ==> ={glob G, res})=> //=.
by proc true.
+ rnd (pred1 (psi (glob G) o)); skip=> /> &m0 hphi.
by rewrite duniform1E psi_in_indices.
by hoare; auto=> /> &m0 ->.
qed.
lemma PBound_mult (G <: Game )
(phi : (glob G) -> tres -> bool)
(psi : (glob G) -> tres -> tval)
x0 &m:
(forall gG o, phi gG o => psi gG o \in indices) =>
Pr[G.main(x0) @ &m: phi (glob G) res]
= card%r * Pr[Guess(G).main(x0) @ &m:
phi (glob G) res.`2 /\
res.`1 = psi (glob G) res.`2].
proof.
move=> h; rewrite -(PBound G phi psi x0 &m h); field.
by rewrite /card eq_fromint size_eq0 undup_nilp indices_not_nil.
qed.