package octez-libs

  1. Overview
  2. Docs
package octez-libs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file cq.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
(*****************************************************************************)
(*                                                                           *)
(* MIT License                                                               *)
(* Copyright (c) 2023 Nomadic Labs <contact@nomadic-labs.com>                *)
(*                                                                           *)
(* Permission is hereby granted, free of charge, to any person obtaining a   *)
(* copy of this software and associated documentation files (the "Software"),*)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense,  *)
(* and/or sell copies of the Software, and to permit persons to whom the     *)
(* Software is furnished to do so, subject to the following conditions:      *)
(*                                                                           *)
(* The above copyright notice and this permission notice shall be included   *)
(* in all copies or substantial portions of the Software.                    *)
(*                                                                           *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR*)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,  *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL   *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER*)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING   *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER       *)
(* DEALINGS IN THE SOFTWARE.                                                 *)
(*                                                                           *)
(*****************************************************************************)

(* This file implements Cq, a lookup protocol described in
   https://eprint.iacr.org/2022/1763.pdf, in which the prover work is
   independant of the size of the table

   In the code, we call n the size of the table (N), & k the size of the wire
   to check (n).

   TODO https://gitlab.com/tezos/tezos/-/issues/6070
          - the setup is currently computed in O(N²) while it could be computed
            in O(NlogN) with Kate amortized
          - be able to select the wire’s value to lookup
          - integrate to PlonK
          - integrate to aPlonK
*)

open Kzg.Bls
open Identities
open Kzg.Utils
module Degree_check = Kzg.Degree_check.G1_proof

module type Cq_sig = sig
  exception Entry_not_in_table

  type prover_public_parameters

  type verifier_public_parameters

  type proof

  val setup :
    srs:Srs_g1.t * Srs_g2.t ->
    wire_size:int ->
    table:S.t array list ->
    prover_public_parameters * verifier_public_parameters

  val prove :
    prover_public_parameters ->
    Transcript.t ->
    S.t array SMap.t list ->
    proof * Transcript.t

  val verify :
    verifier_public_parameters -> Transcript.t -> proof -> bool * Transcript.t
end

module Internal = struct
  open Utils
  module PC = Kzg.Polynomial_commitment
  module ISet = Set.Make (Int)
  module IMap = Map.Make (Int)

  exception Entry_not_in_table

  type transcript = bytes

  type prover_public_parameters = {
    (* size of the table (= N in the paper) *)
    n : int;
    (* precomputed domain for the wires of the size of the wires *)
    domain_k : Domain.t;
    (* domain twice as large as the previous one (for poly multiplication) *)
    domain_2k : Domain.t;
    (* the table as a list of scalar_maps to be more efficient for searching in
       the prover *)
    table : ISet.t Scalar_map.t list;
    (* N kzg commitments for lagrange polynomials L_i *)
    cms_lagrange : G1.t array;
    (* N kzg commitments for (Li - Li(0))/X *)
    cms_lagrange_0 : G1.t array;
    (* N kzg commitments for Qi = (Li × (T - ti)) / X^N - 1 *)
    q : G1.t array list;
    (* prover public parameters for commitment *)
    pc : PC.Public_parameters.prover;
  }

  type verifier_public_parameters = {
    (* size of the table (= N in the paper) *)
    n : int;
    (* size of the wires (= k in the paper) *)
    k : int;
    (* first element of the SRS_2 *)
    srs2_0 : G2.t;
    (* sencond element of the SRS_2 *)
    srs2_1 : G2.t;
    (* (N-1-k+2) of the SRS_2 *)
    srs2_N_1_k_2 : G2.t;
    (* commitment of the table *)
    cm_table : G2.t list;
    (* commitment of the polynomial X^N - 1 *)
    cm_zv : G2.t;
    (* verifier public parameters for commitment *)
    pc : PC.Public_parameters.verifier;
  }

  type proof = {
    (* commitments *)
    cm_f : PC.Commitment.t;
    cm_f_agg : PC.Commitment.t;
    cm_a : PC.Commitment.t;
    cm_b0 : PC.Commitment.t;
    cm_qa : PC.Commitment.t;
    cm_m : PC.Commitment.t;
    cm_p : Degree_check.Proof.t;
    cm_b0_qb_f : PC.Commitment.t;
    (* evaluations *)
    a0 : Scalar.t list;
    b0y : Scalar.t SMap.t;
    fy : Scalar.t SMap.t;
    fy_agg : Scalar.t SMap.t;
    (* proofs *)
    pc : PC.proof;
    cm_a0 : G1.t;
  }

  (* Wires polynomial *)
  let f_name = "f"

  (* m polynomial : i-th coefficient is the number of occurences of t_i in the
     corresponding wire *)
  let m_name = "m"

  (* A polynomial : i-th coefficient is m_i/(t_i + β) *)
  let a_name = "a"

  (* Q_A polynomial : (A×(T+β) - m)/(X^N - 1) *)
  let qa_name = "qa"

  (* B₀ polynomial : (B(X) - B(0))/X, where B polynomial has i-th coefficient 1/(fi + β) *)
  let b0_name = "b0"

  (* Q_B polynomial : (B×(f+β) - 1)/(X^k - 1) (with k = n in the paper) *)
  let qb_name = "qb"

  (* P polynomial : B₀×X^(N-1-(k-2)) *)
  let p_name = "p"

  (* Wire aggregation polynomial : f₀ + αf₁ + α²f₂ + … *)
  let f_agg_name = "f_agg"

  (* This function is used to aggregate commitments for different proofs *)
  let aggregate_cm cm etas =
    Kzg.Commitment.Commit.with_affine_array_1
      (PC.Commitment.to_map cm |> SMap.values |> Array.of_list)
      etas

  (* We don’t need the generator because we don’t evaluate at gX *)
  let get_pc_query gamma =
    List.map (convert_eval_points ~generator:Scalar.zero ~x:gamma) [[X]]

  (* We use PC’s function to commit our polynomials *)
  let commit1 srs =
    PC.(Commitment.commit_single (Public_parameters.get_commit_parameters srs))

  (* [open_at_0 p] returns (p - p(0))/X *)
  let open_at_0 p =
    let q, r =
      Poly.(division_xn (p - constant (evaluate p Scalar.zero)) 1 Scalar.zero)
    in
    assert (Poly.is_zero r) ;
    q

  (* This function avoid some lines of code duplication *)
  let compute_and_commit f list =
    let m, l = List.map f list |> Array.of_list |> Array.split in
    (m, Kzg.Commitment.Commit.with_affine_array_1 l m)

  let setup_prover (n, domain) k (table_arrays, table_polys) pc =
    let domain_k = Domain.build k in
    let domain_2k = Domain.build (2 * k) in

    (* Map that binds scalar to the set of its indices in the table ;
       converting it to a map allow more efficient research in the table *)
    let table =
      List.map
        (fun t ->
          fst
          @@ Array.fold_left
               (fun (acc, i) fi ->
                 ( Scalar_map.update
                     fi
                     (function
                       | None -> Some (ISet.singleton i)
                       | Some sk -> Some (ISet.add i sk))
                     acc,
                   i + 1 ))
               (Scalar_map.empty, 0)
               t)
        table_arrays
    in

    let lagrange =
      Array.init n (fun i ->
          Evaluations.init ~degree:(n - 1) n (fun j ->
              if j = i then Scalar.one else Scalar.zero)
          |> Evaluations.interpolation_fft domain)
    in
    let cms_lagrange = Array.map (commit1 pc) lagrange in
    let cms_lagrange_0 =
      Array.map (fun p -> commit1 pc @@ open_at_0 p) lagrange
    in

    let q =
      List.map2
        (fun t_poly t_array ->
          Array.init n (fun i ->
              let q, r =
                Poly.(
                  division_xn
                    (lagrange.(i) * (t_poly - constant t_array.(i)))
                    n
                    Scalar.(negate one))
              in
              if not (Poly.is_zero r) then
                failwith "Cq.setup_prover : division error." ;
              commit1 pc q))
        table_polys
        table_arrays
    in

    {n; domain_k; domain_2k; table; q; cms_lagrange; cms_lagrange_0; pc}

  let setup_verifier (_srs1, srs2) n k table_poly pc =
    (* cm (X^n - 1) *)
    let cm_zv =
      try G2.(add (Srs_g2.get srs2 n) (negate one))
      with Invalid_argument _ ->
        raise
          (Kzg.Commitment.SRS_too_short
             (Printf.sprintf
                "Cq.setup_verifier : SRS_2 of size at least (%d + 1) expected \
                 (size %d received)."
                n
                (Srs_g2.size srs2)))
    in

    let cm_table = List.map (Kzg.Commitment.Commit.with_srs2 srs2) table_poly in

    let srs2_0 = Srs_g2.get srs2 0 in
    let srs2_1 = Srs_g2.get srs2 1 in
    let srs2_N_1_k_2 = Srs_g2.get srs2 (n - 1 - (k - 2)) in

    {n; k; srs2_0; srs2_1; srs2_N_1_k_2; cm_table; cm_zv; pc}

  let setup ~srs ~wire_size ~table =
    let len_t = Array.length (List.hd table) in
    let n = 1 lsl Z.(log2up (of_int len_t)) in
    (* If the table length is not a power of two we pad until n with the first element of the table *)
    let table =
      if n = len_t then table
      else
        List.map
          (fun t ->
            if Array.length t <> len_t then
              raise (Invalid_argument "Table columns have different lengths.") ;
            Array.(append t (init (n - len_t) (Fun.const t.(0)))))
          table
    in
    if wire_size > n then
      raise
        (Invalid_argument
           (Printf.sprintf
              "Wire (size = %d) greater than table (size = %d)."
              wire_size
              n)) ;
    let domain = Domain.build n in
    let table_polys = List.map (Evaluations.interpolation_fft2 domain) table in
    let pc_prv, pc_vrf, _ = PC.Public_parameters.setup 0 (srs, srs) in
    let prv = setup_prover (n, domain) wire_size (table, table_polys) pc_prv in
    let vrf = setup_verifier srs n wire_size table_polys pc_vrf in
    (prv, vrf)

  let compute_m_and_t_sparse pp f_arrays f_agg =
    let f_arrays = SMap.values f_arrays in
    (* Returns [(i, mi, ti)], where mi is the number of occurences of ti (aggregated version) in f ;
       returning lists is ok because we will just iterate on them & they are sparse *)
    let m_and_t_sparse =
      Array.fold_left
        (fun (m_map, i) f_agg ->
          (* Index in the table of the i-th line of f_arrays *)
          let idx, _ =
            (* For each value of the i-th line, we search it in the table and
               return its indices in the corresponding column of the table
               the index of the line will be the intersection of the indices
               for all the values of the line *)
            List.fold_left2
              (fun (acc, first) f t ->
                match Scalar_map.find_opt f.(i) t with
                | None -> raise Entry_not_in_table
                | Some idx ->
                    ((if first then idx else ISet.inter acc idx), false))
              (ISet.empty, true)
              f_arrays
              pp.table
          in
          (* If the set is empty it means that the line is not in the table ;
             if there is more than one index it means that there is duplication
             in the table, so we just keep one *)
          let idx =
            try ISet.choose idx with Not_found -> raise Entry_not_in_table
          in
          (* Note that we add f_agg here to keep track of the aggregated value
             at each index (what was called ti before) ; we will need it later
             to compute a ; we use f_agg to avoid recomputation *)
          ( IMap.update
              idx
              (function
                | None -> Some (1, f_agg) | Some (nb, _) -> Some (nb + 1, f_agg))
              m_map,
            i + 1 ))
        (IMap.empty, 0)
        f_agg
      |> fst |> IMap.to_seq |> List.of_seq
      |> List.map (fun (i, (m, t)) -> (i, Scalar.of_int m, t))
    in
    let _, cm_m =
      compute_and_commit
        (fun (i, m, _) -> (m, pp.cms_lagrange.(i)))
        m_and_t_sparse
    in
    (m_and_t_sparse, cm_m)

  let compute_a pp beta m_and_t =
    let a, cm_a =
      compute_and_commit
        Scalar.(fun (i, mi, ti) -> (mi / (ti + beta), pp.cms_lagrange.(i)))
        m_and_t
    in
    (List.map2 (fun (i, _, _) a -> (i, a)) m_and_t (Array.to_list a), cm_a)

  let compute_cm_qa alphas pp a =
    snd
    @@ compute_and_commit
         (fun (i, ai) ->
           ( ai,
             fst
             @@ List.fold_left
                  (fun (acc, j) q ->
                    (G1.(add acc (mul q.(i) alphas.(j))), j + 1))
                  (G1.zero, 0)
                  pp.q ))
         a

  let compute_b beta k domain f =
    Evaluations.init ~degree:(k - 1) k (fun i ->
        Scalar.(inverse_exn (f.(i) + beta)))
    |> Evaluations.interpolation_fft domain

  let compute_qb pp beta k b f =
    let f = Evaluations.evaluation_fft pp.domain_2k f in
    let b = Evaluations.evaluation_fft pp.domain_2k b in
    let f_beta = Evaluations.linear_c ~evaluations:[f] ~add_constant:beta () in
    let bf = Evaluations.mul_c ~evaluations:[b; f_beta] () in
    let bf_1 =
      Poly.(Evaluations.interpolation_fft pp.domain_2k bf - constant Scalar.one)
    in
    let q, r = Poly.division_xn bf_1 k Scalar.(negate one) in
    if Poly.is_zero r then q else raise Entry_not_in_table

  let compute_p (pp : prover_public_parameters) transcript k b0 =
    Degree_check.prove_multi
      ~max_commit:(pp.n - 1)
      ~max_degree:(k - 2)
      (PC.Public_parameters.get_commit_parameters pp.pc)
      transcript
      b0

  (* as written p. 13, N × a₀ = ΣA_i for i < N ; since A is sparse, it’s fine *)
  let compute_a0 n a =
    Scalar.(List.fold_left (fun acc (_, a) -> acc + a) zero a / of_int n)

  let compute_cm_a0 pp etas a =
    (* since cm_a0 is a kzg proof, we can batch every a polynomials into one *)
    let a_agg =
      List.fold_left
        (fun (global_acc, k) a ->
          ( List.fold_left
              (fun acc (i, ai) ->
                IMap.update
                  i
                  (function
                    | None -> Some Scalar.(etas.(k) * ai)
                    | Some a -> Some Scalar.(a + (etas.(k) * ai)))
                  acc)
              global_acc
              a,
            k + 1 ))
        (IMap.empty, 0)
        a
      |> fst |> IMap.to_seq |> List.of_seq
    in
    snd @@ compute_and_commit (fun (i, a) -> (a, pp.cms_lagrange_0.(i))) a_agg

  (* produces a kzg proof for steps 3.5 & 3.6 *)
  let kzg_prove (pp : prover_public_parameters) transcript n
      ((cm_f, f_aux), (cm_f_agg, f_agg_aux)) (b0_map, f, f_agg, qb) =
    let qb_map = SMap.Aggregation.of_list ~n "" qb_name qb in
    let f_map = SMap.union_disjoint_list [f; f_agg; b0_map; qb_map] in
    let cm_b0, b0_aux = PC.commit pp.pc b0_map in
    let cm_qb, qb_aux = PC.commit pp.pc qb_map in
    (* Does this must be in lexicographic order ? *)
    let cm_map = PC.Commitment.(recombine [cm_b0; cm_f; cm_f_agg; cm_qb]) in
    let aux =
      PC.Commitment.(recombine_prover_aux [b0_aux; f_aux; f_agg_aux; qb_aux])
    in
    (* 3.1 *)
    let transcript = Transcript.expand PC.Commitment.t cm_map transcript in
    let gamma, transcript = Fr_generation.random_fr transcript in
    (* 3.2 *)
    let b0y = SMap.map (fun p -> Poly.evaluate p gamma) b0_map in
    let qby = SMap.map (fun p -> Poly.evaluate p gamma) qb_map in
    let fy = SMap.map (fun p -> Poly.evaluate p gamma) f in
    let fy_agg = SMap.map (fun p -> Poly.evaluate p gamma) f_agg in
    let query = get_pc_query gamma in
    let secret = [f_map] in
    let cm_aux = [aux] in
    let answers =
      [SMap.singleton "x" (SMap.union_disjoint_list [b0y; fy; fy_agg; qby])]
    in
    let proof, transcript =
      PC.prove pp.pc transcript secret cm_aux query answers
    in
    (b0y, fy, fy_agg, cm_map, cm_b0, proof, transcript)

  (* verify the values provided by kzg_prove *)
  let kzg_verify pp transcript proof k beta =
    (* 3.1 *)
    let transcript =
      Transcript.expand PC.Commitment.t proof.cm_b0_qb_f transcript
    in
    let gamma, transcript = Fr_generation.random_fr transcript in
    (* 3.4 *)
    let n = List.length proof.a0 in
    let b0 =
      List.mapi
        (fun i a0 ->
          ( SMap.Aggregation.add_prefix ~n ~i "" b0_name,
            Scalar.(of_int pp.n * a0 / of_int pp.k) ))
        proof.a0
    in
    (* 3.5, 3.6.a *)
    let zhy = Scalar.((gamma ** Z.of_int k) + negate one) in
    let by =
      List.map2
        (fun b0y (_, b0) -> Scalar.((b0y * gamma) + b0))
        (SMap.values proof.b0y)
        b0
    in
    let qby =
      let i = ref (-1) in
      SMap.of_list
      @@ List.map2
           (fun by fy ->
             i := !i + 1 ;
             ( SMap.Aggregation.add_prefix ~n ~i:!i "" qb_name,
               Scalar.(((by * (fy + beta)) + negate one) / zhy) ))
           by
           (SMap.values proof.fy_agg)
    in
    let cm = [proof.cm_b0_qb_f] in
    let query = get_pc_query gamma in
    let answers =
      [
        SMap.singleton
          "x"
          (SMap.union_disjoint_list [proof.b0y; proof.fy; proof.fy_agg; qby]);
      ]
    in
    PC.verify pp.pc transcript cm query answers proof.pc

  (* Checks that f_agg(γ) = f₀(γ) + αf₁(γ) + α²f₂(γ) *)
  let verify_f_agg alphas proof =
    let nb_wires = Array.length alphas in
    (* format proof.fy as [[f₀, f₁, …] ; [f₀, f₁, …] ; …] *)
    let formatted_fy =
      let (rev_formatted, last), _ =
        SMap.fold
          (fun _ f ((acc_global, acc), count) ->
            (* if count = nb_wires, it means we went accross every wires for
               this proof & the current wire is for a new proof *)
            if count = nb_wires - 1 then ((List.rev acc :: acc_global, [f]), 0)
            else ((acc_global, f :: acc), count + 1))
          proof.fy
          (([], []), -1)
      in
      List.rev (List.rev last :: rev_formatted)
    in
    (* Check equality for all proofs *)
    List.for_all2
      (fun fs f_agg ->
        let sum_fs, _ =
          List.fold_left
            (fun (acc, i) fy -> (Scalar.(acc + (fy * alphas.(i))), i + 1))
            (Scalar.zero, 0)
            fs
        in
        Scalar.eq sum_fs f_agg)
      formatted_fy
      (SMap.values proof.fy_agg)

  (* each f must be a power of two & of the same size *)
  let prove pp transcript f_map_list =
    let k = Array.length (snd @@ SMap.choose (List.hd f_map_list)) in
    (* n = nb_proofs *)
    let n = List.length f_map_list in
    (* The map of all wires polynomials *)
    let f_map =
      SMap.union_disjoint_list
      @@ List.mapi
           (fun i f_map ->
             SMap.map
               (fun f ->
                 Evaluations.(
                   interpolation_fft pp.domain_k (of_array (k - 1, f))))
               f_map
             |> SMap.Aggregation.prefix_map ~n ~i "")
           f_map_list
    in
    let cm_f, f_aux = PC.commit pp.pc f_map in
    let transcript = Transcript.expand PC.Commitment.t cm_f transcript in
    (* α will be used to aggregate wires & table’s columns *)
    let alpha, transcript = Fr_generation.random_fr transcript in
    let alphas = Fr_generation.powers (SMap.cardinal f_map) alpha in
    let f_agg_arrays_list =
      List.map
        (fun f_map ->
          Array.init k (fun i ->
              fst
              @@ SMap.fold
                   (fun _ f (acc, j) ->
                     (Scalar.(acc + (alphas.(j) * f.(i))), j + 1))
                   f_map
                   (Scalar.zero, 0)))
        f_map_list
    in
    let f_agg_list =
      List.map
        (fun f ->
          Evaluations.(interpolation_fft pp.domain_k (of_array (k - 1, f))))
        f_agg_arrays_list
    in
    let f_agg_map = SMap.Aggregation.of_list ~n "" f_agg_name f_agg_list in
    let cm_f_agg, f_agg_aux = PC.commit pp.pc f_agg_map in

    (* 1.1, 1.2 *)
    let m_and_t, cm_m =
      List.map2 (compute_m_and_t_sparse pp) f_map_list f_agg_arrays_list
      |> List.split
    in
    let cm_m, _ = PC.Commitment.of_list pp.pc ~name:m_name cm_m in

    (* 2.1 *)
    let transcript =
      Transcript.list_expand PC.Commitment.t [cm_f_agg; cm_m] transcript
    in
    let beta, transcript = Fr_generation.random_fr transcript in

    (* 2.2, 2.3 *)
    let a, cm_a = List.map (compute_a pp beta) m_and_t |> List.split in
    let cm_a, _ = PC.Commitment.of_list pp.pc ~name:a_name cm_a in
    (* 2.4 *)
    let cm_qa, _ =
      List.map (compute_cm_qa alphas pp) a
      |> PC.Commitment.of_list pp.pc ~name:qa_name
    in

    (* 2.5 *)
    let b = List.map (compute_b beta k pp.domain_k) f_agg_arrays_list in
    (* 2.6 *)
    let b0 =
      SMap.of_list
      @@ List.mapi
           (fun i b ->
             (SMap.Aggregation.add_prefix ~n ~i "" b0_name, open_at_0 b))
           b
    in
    (* 2.8, 2.9 *)
    let qb = List.map2 (compute_qb pp beta k) b (SMap.values f_agg_map) in

    let transcript =
      Transcript.list_expand PC.Commitment.t [cm_a; cm_qa] transcript
    in
    (* 3.6.b *)
    let b0y, fy, fy_agg, cm_b0_qb_f, cm_b0, pc, transcript =
      kzg_prove
        pp
        transcript
        n
        ((cm_f, f_aux), (cm_f_agg, f_agg_aux))
        (b0, f_map, f_agg_map, qb)
    in

    (* 2.10 *)
    let cm_p, transcript =
      Degree_check.prove_multi
        ~max_commit:(pp.n - 1)
        ~max_degree:(k - 2)
        (PC.Public_parameters.get_commit_parameters pp.pc)
        transcript
        cm_b0
        b0
    in

    let transcript = Transcript.expand Degree_check.Proof.t cm_p transcript in

    (* 3.3 *)
    let a0 = List.map (compute_a0 pp.n) a in

    (* 3.6.a *)
    let transcript = Transcript.list_expand Scalar.t a0 transcript in
    let eta, transcript = Fr_generation.random_fr transcript in
    (* 3.7.a *)
    let cm_a0 = compute_cm_a0 pp (Fr_generation.powers n eta) a in

    ( {
        cm_f;
        cm_f_agg;
        cm_a;
        cm_a0;
        cm_b0;
        cm_qa;
        cm_m;
        cm_p;
        a0;
        b0y;
        fy;
        fy_agg;
        pc;
        cm_b0_qb_f;
      },
      transcript )

  let verify pp transcript proof =
    let transcript = Transcript.expand PC.Commitment.t proof.cm_f transcript in
    (* α will be used to aggregate wires & table’s columns *)
    let alpha, transcript = Fr_generation.random_fr transcript in
    let alphas = Fr_generation.powers (List.length pp.cm_table) alpha in
    (* 2.1 *)
    let transcript =
      Transcript.list_expand
        PC.Commitment.t
        [proof.cm_f_agg; proof.cm_m]
        transcript
    in
    let beta, transcript = Fr_generation.random_fr transcript in
    (* 3.1 *)
    let transcript =
      Transcript.list_expand
        PC.Commitment.t
        [proof.cm_a; proof.cm_qa]
        transcript
    in

    let f_agg_verif = verify_f_agg alphas proof in

    (* 3.5, 3.6.a *)
    let kzg_verif, transcript = kzg_verify pp transcript proof pp.k beta in

    (* 2.12 *)
    (* At this point, b0 already has been added to the transcript, & it is
       added again in Degree_check *)
    let check_b0, transcript =
      Degree_check.verify_multi
        pp.srs2_N_1_k_2
        transcript
        proof.cm_b0
        proof.cm_p
    in

    let transcript =
      Transcript.expand Degree_check.Proof.t proof.cm_p transcript
    in

    (* 3.6.a *)
    let transcript = Transcript.list_expand Scalar.t proof.a0 transcript in
    let eta, transcript = Fr_generation.random_fr transcript in
    let etas =
      Fr_generation.powers
        (PC.Commitment.to_map proof.cm_a |> SMap.cardinal)
        eta
    in

    let cm_a = aggregate_cm proof.cm_a etas in
    let cm_qa = aggregate_cm proof.cm_qa etas in
    let cm_m = aggregate_cm proof.cm_m etas in

    let a0 =
      List.fold_left
        Scalar.(fun acc a -> (acc * eta) + a)
        Scalar.zero
        (List.rev proof.a0)
    in

    (* 2.11 *)
    let check_a =
      let table, _ =
        List.fold_left
          (fun (acc, i) c -> G2.(add acc (mul c alphas.(i)), i + 1))
          (G2.zero, 0)
          pp.cm_table
      in
      Pairing.pairing_check
        G1.
          [
            (negate cm_a, table);
            (cm_qa, pp.cm_zv);
            (add cm_m (negate (mul cm_a beta)), pp.srs2_0);
          ]
    in

    (* 3.6.b *)
    let check_a0 =
      Pairing.pairing_check
        G1.
          [
            (add cm_a (negate (mul one a0)), pp.srs2_0);
            (negate proof.cm_a0, pp.srs2_1);
          ]
    in

    (f_agg_verif && kzg_verif && check_a && check_b0 && check_a0, transcript)
end

include (Internal : Cq_sig)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct