Revision 058022c3be6121e485ecf48e19424d1ed36dc535 authored by François Dupressoir on 19 January 2022, 19:29:05 UTC, committed by François Dupressoir on 19 January 2022, 19:29:05 UTC
1 parent 46ba308
Raw File
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.
back to top