https://github.com/EasyCrypt/easycrypt
Raw File
Tip revision: 82cc4d7ad1ca93dc93773f50b053591da4d479b1 authored by Pierre-Yves Strub on 09 June 2020, 19:55:20 UTC
binomial law + basic lemmas (full / support)
Tip revision: 82cc4d7
TCR.eca
require import AllCore.

type K.
op dk : K distr.

type t_from.
type t_to.

op H : K -> t_from -> t_to.

module type ADV_TCR = {
  proc c1 () : t_from
  proc c2 (k:K) : t_from
}.

module TCR (A:ADV_TCR) = {
  proc main() = {
    var x,y,k;
    x <- A.c1();
    k <$ dk;
    y <- A.c2(k);
    return (H k x = H k y /\ x <> y);
  }
}.


    
back to top