partial evaluation for circuit-friendly protocols

[rolph-recto]

To compile to circuits that MPC libraries can execute, we need to make the protocols synthesized by Viaduct to be as straight-line programs as much as possible. To do this, we need to perform optimizations like loop unrolling.

We could have many optimizations that do one little thing at a time, but there is a general technique that would let us do all these things at once: partial evaluation. If loop sizes are statically known, then PE can unroll the loop automatically. PE will also perform constant prop/folding, inlining, etc.

PE would not be too hard to support, especially online PE (although we need to be careful here to avoid nontermination) --- we just need to modify the interpreter.

Example

To see the benefits of partial evaluation, consider the following program:

val a: int{A & B<-}[10];
val b: int{B & A<-}[10];
val c: int{A & B}[10];

for (val i: int = 0; i < 3; i++) {
  c[i] = endorse(a[i]) * endorse(b[i]);
}

val secret_sum: int{A & B} = 0;
for (val j: int = 0; j < 3; j++) {
  secret_sum += c[j]
}

val sum: int{A && B} = declassify(sum)

Before PE, the compiler synthesizes the following protocol:

process Local(A) {
  val a: int[];
  loop {
    tmp_guard <- recv int from Replicated(A,B)
    if (guard) {
      tmp_i <- recv int from Replicated(A,B)
      send a[tmp_i] to MPC(A,B)
    } else {
      break
    }
  }
}

process Local(B) {
  val b: int[];
  loop {
    tmp_guard <- recv int from Replicated(A,B)
    if (guard) {
      tmp_i <- recv int from Replicated(A,B)
      send b[tmp_i] to MPC(A,B)
    } else {
      break
    }
  }
}

process Replicated(A,B) {
  val i: int = 0;
  loop {
    let guard = i < 3
    send guard to Local(A), Local(B), MPC(A,B)
    if (guard) {
      send i to Local(A), Local(B), MPC(A,B)
      i++
    } else {
      break;
    }
  }
  
  val j: int = 0;
  loop {
    let guard = j < 3
    if (guard) {
      send j to MPC(A,B)
      j++
    } else {
      break
    }
  }
  
  val sum: int <- recv MPC(A,B)
}

process MPC(A,B) {
  val c: int[];
  loop {
    tmp_guard <- recv int from Replicated(A,B)
    if (tmp_guard) {
      tmp_ai <- recv Local(A)
      tmp_bi <- recv Local(B)
      tmp_i <- recv Replicated(A,B)
      c[tmp_i] = tmp_ai * tmp_bi
    
    } else {
      break
    }
  }
  
  val secret_sum: int = 0;
  loop {
    tmp_guard <- recv in from Replicated(A,B)
    if (tmp_guard) {
      tmp_j <- recv Replicated(A,B)
      secret_sum += c[tmp_j]
    } else {
      break
    }
  }
  
  send secret_sum to Replicated(A,B)
}

After PE, the protocol becomes:

process Local(A) {
  val a: int{A & B<-}[10];
  send a[0] to MPC(A,B);
  send a[1] to MPC(A,B);
  send a[2] to MPC(A,B);
}

process Local(B) {
  val b: int{B & A<-}[10];
  send b[0] to MPC(A,B);
  send b[1] to MPC(A,B);
  send b[2] to MPC(A,B);
}

process Replicated(A,B) {
  val sum: int <- recv MPC(A,B)
}

process MPC(A,B) {
  val c: int[10];
  tmp_ai_0 <- recv int from Local(A)
  tmp_bi_0 <- recv int from Local(B)
  c[0] = tmp_ai_0 * tmp_bi_0;
  tmp_ai_1 <- recv int from Local(A)
  tmp_bi_1 <- recv int from Local(B)
  c[1] = tmp_ai_1 * tmp_bi_1;
  tmp_ai_2 <- recv int from Local(A)
  tmp_bi_2 <- recv int from Local(B)
  c[2] = tmp_ai_2 * tmp_bi_2;
  
  val secret_sum: int = 0;
  secret_sum += c[0]
  secret_sum += c[1]
  secret_sum += c[2]
  send secret_sum to Replicated(A,B)
}

Notice that there is no control structures anymore---all processes just execute a straight-line program.

Of course there will tradeoffs with performing PE---the most obvious of which is the code size increase that occurs when we unroll loops.