Revision 408d1b0826ca0d4f6a3573dd071eb6354c7e40cb authored by Asif Mallik on 10 October 2019, 07:19:29 UTC, committed by Pierre-Yves Strub on 10 October 2019, 07:19:29 UTC
1 parent e9598be
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);
}
}.
Computing file changes ...
