Linked proof user docs

sunscreen_docs/book.toml

@@ -1,5 +1,5 @@
 [book]
-authors = ["Rick Weber", "Ravital Solomon", "Sam Tay"]
+authors = ["Rick Weber", "Ravital Solomon", "Sam Tay", "Ryan Orendorff"]
 language = "en"
 multilingual = false
 src = "src"

sunscreen_docs/src/SUMMARY.md

@@ -15,6 +15,7 @@
 - [What's in an FHE program?](fhe/fhe_programs/fhe_programs.md)
   - [Types](fhe/fhe_programs/types/types.md)
     - [Signed](fhe/fhe_programs/types/signed.md)
+    - [Unsigned](fhe/fhe_programs/types/unsigned.md)
     - [Fractional](fhe/fhe_programs/types/fractional.md)
     - [Rational](fhe/fhe_programs/types/rational.md)
   - [How to write an FHE program](fhe/fhe_programs/writing_an_fhe_program/writing_an_fhe_program.md)
@@ -77,3 +78,23 @@
     - [Constant inputs](zkp/advanced/constant_inputs.md)
     - [Creating ZKP types](zkp/advanced/zkp_type.md)
   - [WASM support](zkp/advanced/wasm.md)
+
+# FHE + ZKP
+
+- [Introduction](linked/intro/intro.md)
+  - [How does this work?](linked/intro/how.md)
+- [What's in a Linked ZKP program?](linked/linked_programs/linked_programs.md)
+  - [Types](linked/linked_programs/types.md)
+  - [Limitations](linked/linked_programs/limitations.md)
+- [Compiling](linked/compiling/compiling.md)
+- [Runtime](linked/runtime/runtime.md)
+  - [Proving](linked/runtime/prove.md)
+  - [Verifying](linked/runtime/verify.md)
+  - [Serialization](linked/runtime/serialization.md)
+- [Applications](linked/applications/applications.md)
+  - [Private transactions](linked/applications/private_tx.md)
+- [FAQ](linked/faq/faq.md)
+- [Advanced topics](linked/advanced/advanced.md)
+  - [Plaintext modulus](linked/advanced/plain_modulus.md)
+  - [Custom bounds](linked/advanced/custom_bounds.md)
+  - [Short discrete log proof](linked/advanced/sdlp.md)

sunscreen_docs/src/fhe/fhe_programs/types/unsigned.md

@@ -0,0 +1,19 @@
+# Unsigned
+
+Our unsigned types actually come in a few different flavors, depending on the
+number of bits you need. Just like the [`crypto_bigint::Uint`](https://docs.rs/crypto-bigint/latest/crypto_bigint/struct.Uint.html) type, you can specify however many word-sized limbs you need for your computation:
+
+```rust,ignore
+struct Unsigned<const LIMBS: usize>;
+```
+
+and we provide a few type synonyms for common bit sizes (`Unsigned64`,
+`Unsigned128`, `Unsigned256`, and `Unsigned512`).
+
+These unsigned types allow you to perform integer arithmetic as follows (recall that at least one operand must be a ciphertext):
+
+operation | operand
+----------|------------------------------------------------------------
+add       | ciphertext, plaintext, `Uint<LIMBS>` literal, `u64` literal
+sub       | ciphertext, plaintext, `Uint<LIMBS>` literal, `u64` literal
+mul       | ciphertext, plaintext, `Uint<LIMBS>` literal, `u64` literal

sunscreen_docs/src/linked/advanced/advanced.md

@@ -0,0 +1,3 @@
+# Advanced topics
+
+Now that you've gotten the basics down, let's dive into some more complex topics.

sunscreen_docs/src/linked/advanced/custom_bounds.md

@@ -0,0 +1,59 @@
+# Custom bounds
+
+If you are comfortable with the math behind the [SDLP](/linked/intro.how.md),
+advanced users may wish to customize certain bounds in the secret `S`. Note that
+the correctness of linking types relies on the bounds we've used in our
+implementation (which varies among the FHE types but generally looks like a
+bound up to the plaintext modulus for coefficients under degree 256, and zero
+for greater coefficients). For this reason, we expressly discourage changing the
+bounds for any messages that are linked to ZKP programs. However, you may wish
+to change the bound on noise terms for computed ciphertexts; we use a liberal
+bound of $\Delta/2$ for each coefficient in the noise polynomial, which is the
+maximum noise permitted for a valid decryption. If you want to ensure that a
+computed ciphertext has much less noise, perhaps to use it as an input for
+further computation, you can lower this bound.
+
+To do this, first familiarize yourself with the [documentation](https://docs.rs/logproof/latest/logproof/bfv_statement/fn.generate_prover_knowledge.html) concerning the shape of `S`.
+Then you can modify its bounds with the code below.
+
+
+```rust,no_run
+{{#rustdoc_include ../basic_prog.rs:none}}
+use sunscreen::linked::Bounds;
+
+# fn main() -> Result<(), Error> {
+let app = Compiler::new()
+    .fhe_program(increase_by_factor)
+    .zkp_backend::<BulletproofsBackend>()
+    .zkp_program(is_greater_than_one)
+    .compile()?;
+let runtime = FheZkpRuntime::new(app.params(), &BulletproofsBackend::new())?;
+let (public_key, private_key) = runtime.generate_keys()?;
+# let existing_ct = runtime.encrypt(Signed::from(2), &public_key)?;
+
+let mut proof_builder = runtime.linkedproof_builder();
+
+// Assume existing ciphertext comes out of a computation
+let (pt, link) = proof_builder.decrypt_returning_link::<Signed>(&existing_ct, &private_key)?;
+
+// For a single decryption statement, S will have one column and four rows, with
+// the last entry containing the noise. Let's lower the bound on each
+// coefficient in the noise polynomial to 32 bits.
+let degree = app.params().lattice_dimension as usize;
+let proof = proof_builder
+    .add_custom_bounds(3, 0, Bounds(vec![32; degree]))
+    .zkp_program(app.get_zkp_program(is_greater_than_one).unwrap())?
+    .linked_input(link)
+    .build()?;
+
+let mut verify_builder = runtime.linkedproof_verification_builder();
+verify_builder.decrypt_returning_link::<Signed>(&existing_ct)?;
+// The verifier must specify the same bounds!
+verify_builder
+    .add_custom_bounds(3, 0, Bounds(vec![32; degree]))
+    .proof(proof)
+    .zkp_program(app.get_zkp_program(is_greater_than_one).unwrap())?
+    .verify()?;
+#     Ok(())
+# }
+```

sunscreen_docs/src/linked/advanced/plain_modulus.md

@@ -0,0 +1,15 @@
+# Plaintext modulus
+
+First, make sure you've read through the [previous chapter describing the
+plaintext modulus](/fhe/advanced/plain_modulus/plain_modulus.md). We mentioned
+that decreasing our default plaintext modulus can increase performance in FHE
+programs, and the same is true of linked ZKP programs. In fact, the size of the
+linked proof will also decrease with a lower plaintext modulus. If you are an
+advanced user looking to tune the proof size and prover/verifier times, you
+ought to consider whether or not your application can support a lower plaintext
+modulus.
+
+However, our current implementation requires that the plaintext modulus be a
+power of 2. If you specify a modulus that is not a power of two, your linked ZKP
+program will fail to compile. We may offer support for other plaintext modulus
+values in the future — reach out if you have a use case in mind!

sunscreen_docs/src/linked/advanced/sdlp.md

@@ -0,0 +1,27 @@
+# Short discrete log proof
+
+If you only have to prove that ciphertexts are well formed and within certain
+noise bounds, and you don't have any arbitrary properties to prove about the
+encrypted values, you can also use an `Sdlp` on its own, rather than a full
+`LinkedProof` and ZKP program.
+
+```rust
+{{#rustdoc_include ../basic_prog.rs:none}}
+# fn main() -> Result<(), Error> {
+let app = Compiler::new()
+    .fhe_program(increase_by_factor)
+    .compile()?;
+let runtime = FheRuntime::new(app.params())?;
+let (public_key, private_key) = runtime.generate_keys()?;
+
+let mut proof_builder = runtime.sdlp_builder();
+let ct = proof_builder.encrypt(&Signed::from(2), &public_key)?;
+let proof = proof_builder.build()?;
+
+let mut verify_builder = runtime.sdlp_verification_builder();
+verify_builder.encrypt(&ct, &public_key)?;
+verify_builder.proof(proof).verify()?;
+
+#     Ok(())
+# }
+```

sunscreen_docs/src/linked/applications/applications.md

@@ -0,0 +1,4 @@
+# Applications
+
+In this section, we'll take a look at a robust, private, and trustless system for private
+transactions in an environment with transparent computation.