[protocol spec] Review definition of Knowledge Soundness

[daira]

@arielgabizon wrote the following in #92 about the definition of Knowledge Soundness in section 4.1.3:

Suggest to change to :

For any efficient adversary A there exists an efficient extractor E_A, such that for any input x:ZK.PrimaryInput given to both as input, the following holds.
The probability that A outputs \pi: ZK.proof such that ZK.Verify(x,\pi)=1 but E_A doesn't output w such that (x,w)\in ZK.SatisfyingInputs is negligible.
Here A and E_A are assumed to be deterministic and the probability is over the randomness of ZK.Gen.

(If you want A and E_A not to be deterministic you need to also give E_A access to random tape of A, I like to just assume they are deterministic as since they are non-uniform circuits you can fix A's randomness to maximize its success of producing a proof.)

(I'm splitting items that were not resolved out of that issue.)

I need to check whether the definition was changed already since Ariel's comment.