type key. (* encryption keys, key_len bits *)
type text. (* plaintexts, text_len bits *)
type cipher. (* ciphertexts *)

module type ENC = {
  proc key_gen(): key
  proc enc(k: key, x: text): cipher
  proc dec(k: key, c: cipher): text
}

module Cor (Enc: ENC) = {
  proc main(x: text): bool = {
    var k: key; var c: cipher; var y: text;
    k <@ Enc.key_gen();
    c <@ Enc.enc(k, x);
    y <@ Enc.dec(k, c);
    return x = y;
  }
}