marlin_marlin.ml

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)