Output scheme: FunkyPRGSymEnc.scheme

Here is the scheme file that was generated by Claude Code (Opus 4.6):

import '../../Primitives/SymEnc.primitive';
import '../../Primitives/PRG.primitive';

Scheme FunkyPRGSymEnc(PRG G) extends SymEnc {
    requires G.stretch == G.lambda;

    Int lambda = G.lambda;

    Set Key = BitString<lambda>;
    Set Message = BitString<2 * lambda>;
    Set Ciphertext = BitString<3 * lambda>;

    Key KeyGen() {
        Key k <- Key;
        return k;
    }

    Ciphertext Enc(Key k, Message m) {
        BitString<lambda> r <- BitString<lambda>;
        BitString<2 * lambda> z = G.evaluate(k + r);
        return r || (z + m);
    }

    Message Dec(Key k, Ciphertext c) {
        BitString<lambda> r = c[0 : lambda];
        BitString<2 * lambda> y = c[lambda : 3 * lambda];
        BitString<2 * lambda> z = G.evaluate(k + r);
        return y + z;
    }
}