marlin_marlin.markdown

This document makes explicit what is hinted at in the Halo paper, which is a technique for taking two AHIOPs that have efficient "incremental verification" and "gluing them together" to obtain one recursive proof system.

More specifically, if we have

• An AHIOP $S_0$ for verifying $\F_p$ arithmetic
• An AHIOP $S_1$ for verifying $\F_q$ arithmetic
• A polynomial commitment scheme $C_0$ for polynomials in $\F_p[x]$ and whose proofs can be efficiently "incrementally verified" using $\F_q$ arithmetic.
• A polynomial commitment scheme $C_1$ for polynomials in $\F_q[x]$ and whose proofs can be efficiently "incrementally verified" using $\F_p$ arithmetic.

Then we obtain an efficient incrementally verifiable computation system (or PCD system etc.) for say $\F_p$ arithmetic. This IVC system has the following efficiency properties

• Verifier time is equal to the "finalizing verifier time" of $C_0$ plus the "finalizing verifier time" of $C_1$, with each $C_i$ verifying a commitment to a polynomial whose degree is the max degree of a polynomial in the argument $S_{1 - i}$
• Incremental prover time is equal to the prover time in $S_0$ instantiated with $C_0$, plus a constant factor overhead which is proportional to the complexity of $S_1$'s incremental verifier (when verifying a statement encoding $S_0$'s incremental verifier).

A concrete instantiation

It's complicated to explain the general technique, so I will describe a good concrete instantiation based on gluing together two versions of Marlin using a half-pairing-friendly cycle.

Say the pairing-friendly curve $G_0$ is defined over $\F_q$ and has scalar field $\F_p$ and the non-pairing-friendly Curve $G_1$ is defined over $\F_p$ and has scalar field $\F_q$.

$S_0$ will be Marlin instantiated using the Kate PCS scheme, which is itself instantiated using $G_0$.

$S_1$ will be Marlin instantiated using the DLog-based PCS scheme (described in the Halo paper) which is itself built out of a inner-product argument described in the Bulletproofs paper. (We will use the inner-product argument directly for an optimizations later.)

Say the computation we are incrementally verifying is a transition function $\textsf{transition_function} \colon \F_p^s \times \F_p^t \to \F_p^s$. We have to describe two SNARK circuits which will recursively verify each other. Here is how it looks.

let n = something
let k = log2 n

let b (u : f_q array) (x : f_q) : f_q =
  let x_to_pow2s =
    let res = Array.create k x in
    for i = 1 to k - 1 do
      res.(i) <- square (res.(i - 1))
    done
  in
  product k (fun i -> u.(i) + 1 / u.(i) * x_to_pow2s.(i))

(* Inside here we have F_q arithmetic, so we can incrementally check
   the polynomial commitments from the pairing-based Marlin *)
let dlog_main
    app_state (* F_p based (passed through) *)

    pairing_marlin_vk (* F_q based *)
    next_pairing_marlin_acc (* F_q based *)

    dlog_marlin_vk (* F_p based (passed through) *)
    g_old (* F_p based (passed through) *)

    x_old (* F_q based *)
    u_old (* F_q based *)
    b_u_x_old (* F_q based *)

    prev_dlog_marlin_acc (* F_p based *)
    prev_deferred_fp_arithmetic (* F_p based *)
  =
  let prev_pairing_marlin_acc = exists Pairing_marlin_acc
  and prev_deferred_fq_arithmetic = exists Deferred_fq_arithmetic
  in
  List.iter prev_deferred_fq_arithmetic ~f:(fun a ->
      perform a);
  (* This is kind of a special case of deferred fq arithmetic. *)
  assert (b u_old x_old = b_u_x_old);

  let updated_pairing_marlin_acc, deferred_fp_arithmetic =
    let prev_marlin_proof = exists Prev_pairing_marlin_proof in
    (* This performs the marlin verifier, does the incremental update of
       the polynomial commitment verification but does not perform all the
       F_p arithmetic equality checks. *)
    Pairing_marlin.incrementally_verify_openings
      pairing_marlin_vk
      prev_marlin_proof
      ~public_input:[
        pairing_marlin_vk; (* This may need to be passed in using the hashing trick. It could be hashed together with prev_pairing_marlin_acc since they're both just passed through anyway.  *)
        prev_pairing_marlin_acc;
        dlog_marlin_vk;
        g_old;

        prev_dlog_marlin_acc;

        prev_deferred_fq_arithmetic;
      ]
  in
  assert (updated_pairing_marlin_macc = next_pairing_marlin_acc);
  assert (prev_deferred_fp_arithmetic = deferred_fp_arithmetic);

(* Inside here we have F_p arithmetic so we can incrementally check the
   polynomial commitments from the DLog-based marlin *)
let pairing_main
    app_state
    pairing_marlin_vk
    prev_pairing_marlin_acc
    dlog_marlin_vk
    g_new
    u_new
    x_new
    next_dlog_marlin_acc
    next_deferred_fq_arithmetic
    =
    (* The actual computation *)
    let prev_app_state = exists Prev_app_state in
    let transition = exists Transition in
    assert (transition_function prev_app_state transition = app_state);

    let prev_dlog_marlin_acc = exists Dlog_marlin_acc
    and prev_deferred_fp_arithmetic = exists Deferred_fp_arithmetic in
    List.iter prev_deferred_fp_arithmetic ~f:perform;
    let (actual_g_new, actual_u_new), deferred_fq_arithmetic =
      let g_old, x_old, u_old, b_u_old = exists G_old in
      let updated_dlog_marlin_acc, deferred_fq_arithmetic, polynomial_evaluation_checks =
        let prev_dlog_marlin_proof = exists Prev_dlog_marlin_proof in
        Dlog_marlin.incrementally_execute_protocol
          dlog_marlin_vk
          prev_dlog_marlin_proof
          ~public_input:[
            prev_app_state;
            pairing_marlin_vk;
            prev_pairing_marlin_acc;
            dlog_marlin_vk;
            g_old;
            x_old;
            u_old;
            b_u_old_x;
            prev_dlog_marlin_acc;
            prev_deferred_fp_arithmetic;
          ]
      in
      let g_new_u_new =
        batched_inner_product_argument
          ((g_old, x_old, b_u_old_x) :: polynomial_evaluation_checks)
      in
      g_new_u_new, deferred_fq_arithmetic
    in
    (* This should be sampled using the hash state at the end of 
        "Dlog_marlin.incrementally_execute_protocol" *)
    let x_new = sample () in
    assert (actual_g_new = g_new);
    assert (actual_u_new = u_new);
    assert (actual_x_new = x_new)