generic labels and functions

[rolph-recto]

To make functions more reusable, we would like to support label polymorphism.

fun gcd{a,b}(x: int{a}, y: int{b}, ret: out int{a || b}) {
  if (y == 0) {
    ret = a;

  } else {
    gcd{b, a || b}(y, x % y);
  }
}

We can have two calls to GCD that compile to different protocols. This call will compile into a local computation for Alice:

int{A} x, y;
int{A} z = gcd{A}(x, y);

While this call compiles into an MPC protocol:

int{A & B<-} x;
int{B & A<-} y;
int{A & B} z = gcd{A & B<-, B & A<-}(x, y);

Label Parameter Constraints

Sometimes we would like to have restrictions how label parameters get instantiated; for example, though we want to be generic over the label parameters of inputs, we also want to guarantee that the inputs satisfy specific constraints. We allow a form of bounded polymorphism by introducing label parameter constraints with where blocks.

fun gcd{a,b}(x: int{a}, y: int{b}, ret: out int{a && b})
    where {a-> !=> b->}, {b-> !=> a->}
{ ... }

!=> is the "does not flow to" operator.

During typechecking, these constraints will be present to ensure that the function body respects them.

Monomorphization

We can only perform protocol selection to functions with instantiated label parameters. To support this, we must perform monomorphization and create function copies ("function instances") where labels are instantiated and do not contain label parameters. There are an infinite number of possible instantiations of label parameters; we only monomorphize to instances that occur in function calls.

Monomorphization occurs in four steps.

1. Compute map from function callers to function callees

First, we generate a map from functions and to other functions it calls, while preserving the relationship between the label parameters of the caller and the label parameters of the callee. This will later allow us to compute all function calls with their instantiated labels.

For example, the function body of gcd

gcd{a,b} ---> gcd{b, a || b}

2. Compute set of all function calls with unique instantiated labels

Next, we compute the set of all function calls with unique instantiated labels. We do this by substituting label parameters with actual labels in the initial function call and creating new function calls according to the map in (1), repeating this process until we reach a fixpoint.

Calling gcd where a=A and b=B, we get the chain of calls with instantiated labels:

gcd{A, B} ---> gcd{B, A || B} ---> gcd{A || B, A || B}

Alternatively, calling gcd where a=A & B<- and b=B & A<-, we get the chain:

gcd{A & B<-, B & A<-} ---> gcd{B & A<-, A & B} ---> gcd{A & B, A & B}

3. Create function instances and rename function calls as appropriate.

Given the set of function calls with instantiated labels, we create copies of the original function where label parameters have been instantiated. Assuming we compile the call gcd{A,B}, we generate the following copies:

fun gcd1(x: int{A}, y: int{B}, ret: out int{A || B}) {
  if (y == 0) {
    ret = x

  } else {
    gcd2(y, x % y, ret)
  }
}

fun gcd2(x: int{B}, y: int{A || B}, ret: out int{A || B}) {
  if (y == 0) {
    ret = x

  } else {
    gcd3(y, x % y, ret)
  }
}

fun gcd3(x: int{A || B}, y: int{A || B}, ret: out int{A || B}) {
  if (y == 0) {
    ret = x

  } else {
    gcd3(y, x % y, ret)
  }
}

4. Synthesize protocols for bodies of instantiated functions

We then synthesize protocols for the bodies of these monomorphized functions. This process remains the same as before.

[rolph-recto]

closed by #81