Types

With the linkedproofs feature enabled, the original ZKP types are extended to include types that mirror their FHE counterparts.

How to link?

Before we enumerate those types, there are a few traits and attributes to be aware of that determine the ability to link an FHE ciphertext to a ZKP program.

Linking

The LinkWithZkp trait is implemented for FHE types (like Signed, Unsigned, etc.) that supporting linking the private encrypted values as inputs to a ZKP program. This trait uniquely defines the ZKP counterpart type; for example, the following impl

impl LinkWithZkp for sunscreen::types::bfv::Signed {
    type ZkpType<F: FieldSpec> = sunscreen::types::zkp::BfvSigned<F>;
}

indicates that when you link a Signed value, the corresponding type expected in your ZKP program signature is BfvSigned<F> (otherwise you will see a type error).

Decoding

Recall that plaintext values in FHE are actually polynomials, and to be cryptographically secure, when you link an FHE type to a ZKP program, it is actually this plaintext polynomial that is inserted into the ZKP circuit.

Of course, if you are linking this value to your ZKP program, you probably don't care about the actual encoding (i.e., the plaintext polynomial coefficients), but rather the underlying value being encoded, whether that's a signed, unsigned, or rational value. This is where the AsFieldElement trait comes in: given a linked_input, the trait method linked_input.into_field_elem() decodes the input into a native field element.

Specifying linked inputs

Linked inputs are handled specially with the #[linked] argument attribute. Such arguments are also inherently private, but they must be specified with the linked attribute rather than the #[private] attribute. In fact, we enforce that you can use the argument types below if and only if they are adorned with the #[linked] attribute; doing otherwise will result in a compile-time error.

Lastly, note that #[linked] arguments must be specified before all other argument types (private, public, and constant).

Signed

The counterpart of the FHE Signed type is BfvSigned:

#![allow(unused)]
fn main() {
use sunscreen::{
    types::zkp::{AsFieldElement, BfvSigned, ConstrainEq, Field, FieldSpec}, zkp_program
};
use std::ops::Neg;

#[zkp_program]
fn is_negation<F: FieldSpec>(#[linked] a: BfvSigned<F>, b: Field<F>) {
    a.into_field_elem().constrain_eq(b.neg());
}
}

Unsigned

The counterpart of the FHE Unsigned64 and Unsigned128 types are BfvUnsigned64 and BfvUnsigned128 respectively:¹

#![allow(unused)]
fn main() {
use sunscreen::{
    types::zkp::{AsFieldElement, BfvUnsigned64, BfvUnsigned128, ConstrainCmp, Field, FieldSpec}, zkp_program, zkp_var
};

#[zkp_program]
fn exceeds<F: FieldSpec>(#[linked] a: BfvUnsigned64<F>, #[linked] b: BfvUnsigned128<F>) {
    a.into_field_elem().constrain_le_bounded(zkp_var!(u64::MAX), 64);
    b.into_field_elem().constrain_le_bounded(zkp_var!(u128::MAX), 128);
}
}

Rational

The counterpart of the FHE Rational type is BfvRational. This one is a bit different from the others because the rational type actually encodes two signed integers, a numerator and a denominator. Consequently, the into_field_elem actually returns two field elements for this type:

#![allow(unused)]
fn main() {
use sunscreen::{
    types::zkp::{AsFieldElement, BfvRational, ConstrainCmp, Field, FieldSpec}, zkp_program
};

#[zkp_program]
fn compare_rational<F: FieldSpec>(#[linked] x: BfvRational<F>, #[linked] y: BfvRational<F>) {
    let (x_num, x_den) = x.into_field_elem();
    let (y_num, y_den) = y.into_field_elem();
    let x = x_num * y_den;
    let y = y_num * x_den;
    x.constrain_le_bounded(y, 128);
}
}