Add ZKProof function to designate zero-knowledge scope

[ergomorphic]

ZK scoping

Motivation

We have SigmaProp type, Boolean type and there are connectives &&, || which allow to combine them. In ErgoScript frontend we allow implicit conversion from SigmaProp to Boolean to satisfy the type checker. For example the following script is valid, even though && has SigmaProp on the left and Boolean on the right.

((pkA || pkB) && HEIGHT > 1000) || pkC

For type checking this is made explicit by using isValid method of SigmaProp.

((pkA || pkB).isValid && HEIGHT > 1000) || pkC.isValid

However isValid function is revealing information, i.e. we may learn that the secret for pkC has not been provided or it was invalid.

To avoid such revealing the compiler is performing push-up transformation of all nested isValid invocations. The code above will be transformed to the following

(((pkA || pkB) && TrivialSigma(HEIGHT > 1000)) || pkC).isValid

We can call this process knowledge hiding or ZK-securing.

TrivialSigma nodes represent embedding of classical boolean values to SigmaProp type. At runtime HEIGHT > 1000 term will be evaluated to Boolean (true or false) and then TrivialSigma will become either TrueProof or FalseProof of the sigma tree.

Unfortunately, in general such push-up transformation not always possible. For example the following cannot be ZK-secured.

arr.where(x => someFunc(x).isValid)

Thus we have a conceptual problem, not every program in ErgoScript can be ZK evaluated due to non-interactive nature of sigma-protocols which are used.

Solution in ErgoScript

In order to give programmer control over ZK-securing process the following function can be used to designate zero-knowledge scope in the program

ZKProof: SigmaProp => Boolean

The function is lazy in its argument, so the whole syntactic subtree will become a scope of zero knowledge proofs. This is how the first example can be written

ZKProof {
  val deadlinePassed = HEIGHT > 1000
  val aliceOrBob = (pkA || pkB)
  (aliceOrBob && deadlinePassed) || pkC
}

Here the sub-tree is the whole block in curly braces, so the whole script can be easily made into ZKProof, or alternatively only part of the script can be ZK-secured.

Only single ZKProof scope is possible and it should be a root of the tree. Note, if ZKProof scope is not defined in the script, then implicit scoping is assumed, in which isValid push-up should be successfully performed.

Using ZK scoping we can correctly introduce isValid function into the language and clearly explain semantics of SigmaProp and Boolean interactions on both language and runtime level.

On language level isValid introduced as either implicit or explicit conversion which is valid only inside ZKProof scope (if ZKProof is defined). Usage of isValid outside of defined ZKProof scope will lead to compiler error message explaining this limitation. At the same time any usage of isValid inside ZKProof scope is valid as long as the scope can be secured, i.e. all isValid applications can be pushed up to the root. If push-up is not possible in ZKProof scope it is reported as a compiler error.

In the runtime isValid is always in the root position of the compiled tree because push-up transformation is successfully applied to ZKProof scope. The code sigmaTree.isValid is interpreted:

• as sigmaTree.generateProof by the prover
• as verify(generatedProof) by the verifier

[greenhat]

Todo:

• [ ] ZKProof can only be at the root of the tree;
• [ ] ZKProof can only be single;
• [ ] Usage of isValid outside of ZKProof scope should lead to a compiler error (this is only in the presence of ZKProof scope. If it is not declared then no such limitation);
• [ ] In the scope of ZKProof no Boolean value or operation is allowed
• [ ] Closure of ZKProof shouldn't contain Boolean values.

[kushti]

done with sigmaProp() it seems ?