Add protocol annotations to variables, expressions, statements etc.

[cacay]

We should add annotations that let the programmer specify which protocol should execute a piece of code. This sounds like the antithesis of Viaduct, and it is! After all, the whole point of Viaduct is to figure that out for the programmer and hide all crypto. But there are good reasons to add these annotations:

1. It gives a canonical way to display protocol selection. Protocol selection produces a map from variables to protocols, but this map is separate from the program. Embedding this information in the program would make debugging easier for us and for the end users.
2. Viaduct with these annotations becomes a formal IR for mixed-protocol multiparty computation. It could replace languages like L1 and Wysteria more directly.
3. It makes Viaduct more practical. The Viaduct protocol selector is meant to be smart, but having these annotations would give the programmers the option to override default behavior when Viaduct is being stupid. It would also help cryptographers extending Viaduct (IBM folks) to get Viaduct to use their libraries. Finally, the fully "protocol selected" program can now be stored on disk, which could facilitate, for example, incremental computation.

The main questions to answer are (1) what constructs need/allow a protocol annotations, and (2) what is the syntax.

We can definitely put annotations on temporaries, objects, and expressions. A possible syntax is as follows:

val x@Local(alice) = 5;
val y@MPCWithAbort(alice, bob) = Array(10);

val z = ((x + 2) * y[0]) @MPCWithAbort(alice, bob)

Coming up with syntax for statements is not hard:

@Local(alice) x += 2;
@Local(bob) {
    ...
}

The question is, how do we interpret the scope of these annotations? The same question applies to complex expression. For instance, in the above example, the annotation definitely requires the multiplication to happen on MPC, but what about the addition? If the annotations are granular or local, then they will be easy to explain and won't cause unexpected behavior. On the other hand, go too granular (expect annotation on every variable and every subexpression) and they become unusable.

Finally, do we support any form of partial annotation (à la Haskell's partial type signatures)? For example, can I write @MPCWithAbort (elides hosts), @MPC(alice, bob) (MPC is the superclass of MPCWithAbort and other types of MPC), or @MPC(alice, bob, ...) (requires some hosts, allows others)?