Port to Lean 4

[str4d]

No description provided.

[daira]

Tentatively I think we usually want to be more careful about the arguments of reusable definitions than (as far as I know) is possible by use of variable. In particular, we want to have precise control over whether a given argument is explicit or implicit. It's useful for an argument to be implicit when it can be reliably inferred, and explicit otherwise. Declaring it as a variable forces it to be always explicit or (I think this is also supported) always implicit.

The example I've come across in my experimentation is with elliptic curves and elliptic curve points. To get a reasonably ergonomic abstraction for elliptic curve points, you really want the curve and its field of definition to be implicit in functions that take curve points: they can reliably be inferred from the type of the point(s), and it would be horribly verbose to have to specify them. But when constructing a curve, you want the field (and any constraints on it, e.g. on the characteristic) to be explicit I think.

[daira]

I may have been wrong here. The following approach ends up working well in practice:

• use variable to specify a background context (for example the field of definition in the case of curves).
• make the implementations of operators ordinary functions that end up with this context as an explicit first argument (but it doesn't have to be referred to in most cases within the section, since it is captured).
• operator instances still take the context implicitly from their arguments (and for homogenous operator instances like Add they correctly constrain the arguments to be of the same type including context).

You end up not having to use implicits much (but they're there if you need them). It's really well thought out.

[daira]

As I mentioned in the hacking session, this is a definition of indistinguishability (specifically IND-CPA), not semantic security. The definition of semantic security allows the adversary to choose an arbitrary computable function that extracts one bit of information from the plaintext. They are equivalent, but that is not to say they mean the same thing. They mean clearly distinct things that happen to have a nontrivial proof of reductions in either direction between them (for the symmetric case, the reductions are tight; see https://iacr.org/archive/pkc2003/25670071/25670071.pdf ).

The equivalence is actually something that we might want to formalize in Lean, and we cannot do so if we conflate the two definitions. This is not just an issue of historical correctness; the two definitions and the equivalence between them are taught in modern cryptography courses. In any case, it's important to use the correct terminology in what we hope will be a widely used lib.

[daira]

The comment is correct; A2 needs at least G1. Depending on the attack model it might also need a decryption oracle. Without a decryption oracle this is implicitly trying to formalize IND-CPA, but it isn't documented as such.

(Some papers refer to IND-CPA as "semantic security" but that usage is at least confusing and obsolete, and arguably incorrect; see below.)

As an aside, I think this is a poor use of variable, since the definitions of A1 and A2 at least logically belong with the IND-CPA definition.