package octez-libs

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

Source file lang_core.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
(*****************************************************************************)
(*                                                                           *)
(* MIT License                                                               *)
(* Copyright (c) 2022 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.                                                 *)
(*                                                                           *)
(*****************************************************************************)

module S = Csir.Scalar

(** Plompiler core language.

    The {!COMMON} module type defines the set of primitives needed to interpret
    a Plompiler program.
    This module type provides the monadic interface needed to deal with
    Plompier computations, and a number of sub-modules to handle inputs
    and basic types.
*)

(** Numeric operations over the native field. *)
module type NUM = sig
  (** Element of the native scalar field. *)
  type scalar

  (** Representation of values. *)
  type 'a repr

  (** Plompiler program. *)
  type 'a t

  (** [constant s] returns the constant value [s]. *)
  val constant : S.t -> scalar repr t

  (** [zero] returns the value 0. *)
  val zero : scalar repr t

  (** [one] returns the value 1. *)
  val one : scalar repr t

  (** [range_check ~nb_bits s] asserts that [s] is in the
     range \[0, 2^nb_bits). *)
  val range_check : nb_bits:int -> scalar repr -> unit repr t

  (** [custom ~qc ~ql ~qr ~qo ~qm ~qx2b ~qx5a a b] returns a value [c]
      for which the following arithmetic constraint is added:
      [qc + ql * a + qr * b + qo * c + qm * a * b +
       qx2b * b^2 + qx5a * a^5 = 0]

      Manually adding constraints can be error-prone. Handle with care.
  *)
  val custom :
    ?qc:S.t ->
    ?ql:S.t ->
    ?qr:S.t ->
    ?qo:S.t ->
    ?qm:S.t ->
    ?qx2b:S.t ->
    ?qx5a:S.t ->
    scalar repr ->
    scalar repr ->
    scalar repr t

  (** [assert_custom ~qc ~ql ~qr ~qo ~qm a b c] asserts the
      following arithmetic constraint:
      [qc + ql * a + qr * b + qo * c + qm * a * b +
       qx2b * b^2 + qx5a * a^5 = 0]

      Manually adding constraints can be error-prone. Handle with care.
  *)
  val assert_custom :
    ?qc:S.t ->
    ?ql:S.t ->
    ?qr:S.t ->
    ?qo:S.t ->
    ?qm:S.t ->
    scalar repr ->
    scalar repr ->
    scalar repr ->
    unit repr t

  (** [add ~qc ~ql ~qr a b] returns a value [c] such that
      [ql * a + qr * b + qc = c].
  *)
  val add :
    ?qc:S.t -> ?ql:S.t -> ?qr:S.t -> scalar repr -> scalar repr -> scalar repr t

  (** [add_constant ~ql k a] returns a value [c] such that
      [ql * a + k = c].
  *)
  val add_constant : ?ql:S.t -> S.t -> scalar repr -> scalar repr t

  (** [mul ~qm a b] returns a value [c] such that
      [qm * a * b = c].
  *)
  val mul : ?qm:S.t -> scalar repr -> scalar repr -> scalar repr t

  (** [div ~den_coeff a b] asserts [b] is non-zero and returns a
      value [c] such that [a / (b * den_coeff) = c].
  *)
  val div : ?den_coeff:S.t -> scalar repr -> scalar repr -> scalar repr t

  (** [pow5 a] returns a value [c] such that [a^5 = c]. *)
  val pow5 : scalar repr -> scalar repr t

  (** [is_zero a] returns a boolean [c] representing whether [a] is zero. *)
  val is_zero : scalar repr -> bool repr t

  (** [is_not_zero a] is the opposite of [is_zero a]. *)
  val is_not_zero : scalar repr -> bool repr t

  (** [assert_nonzero a] asserts that [a] is not zero. *)
  val assert_nonzero : scalar repr -> unit repr t

  (** [assert_bool a] asserts that [a] is either zero or one. *)
  val assert_bool : scalar repr -> unit repr t
end

module type BOOL = sig
  (** Element of the native scalar field. *)
  type scalar

  (** Representation of values. *)
  type 'a repr

  (** Plompiler program. *)
  type 'a t

  (** [band a b] returns the conjunction of [a] and [b]. *)
  val band : bool repr -> bool repr -> bool repr t

  (** [xor a b] returns the exclusive disjunction of [a] and [b]. *)
  val xor : bool repr -> bool repr -> bool repr t

  (** [bor a b] returns the disjunction of [a] and [b]. *)
  val bor : bool repr -> bool repr -> bool repr t

  (** [bnot a] returns the negation of [a]. *)
  val bnot : bool repr -> bool repr t

  (** [ifthenelse c t e] returns [t] if [c] is true and [e] otherwise. *)
  val ifthenelse : bool repr -> 'a repr -> 'a repr -> 'a repr t

  (** [swap c a b] returns the pair [(b, a)] if [c] is true and
      [(a, b)] otherwise. *)
  val swap : bool repr -> 'a repr -> 'a repr -> ('a * 'a) repr t

  (** [assert_true a] asserts that [a] is true. *)
  val assert_true : bool repr -> unit repr t

  (** [assert_false a] asserts that [a] is false. *)
  val assert_false : bool repr -> unit repr t

  (** [constant kb] returns the constant [kb] as a Plompiler value. *)
  val constant : bool -> bool repr t

  (** [band_list bs] returns the conjunction of the list of booleans
      [bs]. *)
  val band_list : bool repr list -> bool repr t

  module Internal : sig
    val bor_lookup : bool repr -> bool repr -> bool repr t

    val xor_lookup : bool repr -> bool repr -> bool repr t

    val band_lookup : bool repr -> bool repr -> bool repr t

    val bnot_lookup : bool repr -> bool repr t
  end
end

module type COMMON = sig
  (** Element of the native scalar field. *)
  type scalar

  (** Inputs to a plompiler program have three kinds:
      {ul
        {li Public: known by both the prover and verifier.}
        {li Private: known only by the prover.}
        {li InputCom: part of an Input Commitment.
            See {!Lib_plonk.Input_commitment}.}
      }
  *)
  type input_kind = [`InputCom | `Public | `Private]

  (** The trace is the sequence of scalar values used in a Plompiler
      program. It includes the inputs and the intermediary variables.
      Inputs have to be a prefix of the trace, and public inputs come
      before private ones.
  *)
  type trace_kind = [input_kind | `NoInput]

  (** Representation of values. *)
  type 'a repr

  (** Plompiler program. *)
  type 'a t

  (** Monadic return. *)
  val ret : 'a -> 'a t

  (** Monadic bind. *)
  val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t

  (** Monadic sequence operator. *)
  val ( >* ) : unit repr t -> 'a t -> 'a t

  (** Infix map operator. *)
  val ( <$> ) : 'a t -> ('a -> 'b) -> 'b t

  (* Add a boolean check *)

  (** [with_bool_check c] adds an implicit boolean check computed by [c]
      to the circuit.
      The computation of this check is delayed until the end of the circuit
      construction, which is useful for defining complex conditions while
      still processing inputs.
  *)
  val with_bool_check : bool repr t -> unit repr t

  (** [get_checks_wire] retrieves the boolean representing the conjunction
      of all previous implicit checks.

      WARNING: This will "reset" the implicit check accumulator.
  *)
  val get_checks_wire : bool repr t

  (** Module for describing inputs to Plompiler circuits. *)
  module Input : sig
    (** Input of type ['a] to a Plompiler program.
        These hold a value of type ['a] with some additional structure used
        for constructing the circuit.
        Often, after implementing a Plompiler program, one is left with a
        function of the shape:

        [val prog : 'a input -> 'b input -> unit repr t].

        If the user only wants to execute the program in order to compute
        the corresponding circuit, but without producing a proof, then
        the [input]s can be set to dummy values, as they will be ignored.
        That is, only the structure of the [input] is used for building
        the circuit.
    *)
    type 'a input

    (** [scalar s] describes a scalar input holding the value [s]. *)
    val scalar : S.t -> scalar input

    (** [to_scalar i] retrieves the value from a scalar input. *)
    val to_scalar : scalar input -> S.t

    (** [bool b] describes a boolean input holding the value [b]. *)
    val bool : bool -> bool input

    (** [to_bool i] retrieves the value from a boolean input. *)
    val to_bool : bool input -> bool

    (** [unit] describes a unit input. *)
    val unit : unit input

    (** [pair a b] describes the input tuple [(a, b)] made out
        of inputs [a] and [b]. *)
    val pair : 'a input -> 'b input -> ('a * 'b) input

    (** [to_pair p] retrieves the inputs [(a, b)] that make
        up the input tuple [p]. *)
    val to_pair : ('a * 'b) input -> 'a input * 'b input

    (** [list l] turns a list of inputs [l] into an list input. *)
    val list : 'a input list -> 'a list input

    (** [to_list li] turns a list input [li]  into a list of inputs. *)
    val to_list : 'a list input -> 'a input list

    (** [with_implicit_bool_check bc i] attaches an implicit bool
        check [bc] to the input [i]. *)
    val with_implicit_bool_check :
      ('a repr -> bool repr t) -> 'a input -> 'a input

    (** [with_assertion assrtn i] attaches an assertion [assrtn]
        to the input [i]. *)
    val with_assertion : ('a repr -> unit repr t) -> 'a input -> 'a input

    type 'a t = 'a input
  end

  (** Type that describes an open input commitment. *)
  type 'b open_input_com

  (** [serialize i] returns the array of scalars corresponding to its values. *)
  val serialize : 'a Input.t -> S.t array

  (** [input ~kind i] declares an input of a given [kind] to the Plompiler
      program. It returns a Plompiler representation of the inputted value. *)
  val input : ?kind:input_kind -> 'a Input.t -> 'a repr t

  (** [begin_input_com builder] starts a new input commitment.
      [builder] is a function that takes the inputs to be committed one
      by one and returns the composite commitment.

      An example of usage is

      {[
        let* x1, x2 =
          begin_input_com (fun a b -> (a, b))
          |: Input.scalar x1 |: Input.scalar x2 |> end_input_com
        in
      ]}
  *)
  val begin_input_com : 'b -> 'b open_input_com

  (** [ic |: i] adds [i] to the input commitment [ic]  *)
  val ( |: ) : ('c repr -> 'd) open_input_com -> 'c Input.t -> 'd open_input_com

  (** [end_input_com ic] ends the declaration of an input commitment. *)
  val end_input_com : 'a open_input_com -> 'a t

  (** [eq a b] returns the physical equality of [a] and [b].
      Handle with care. *)
  val eq : 'a repr -> 'a repr -> bool

  (** Monadic fold over a list. *)
  val foldM : ('a -> 'b -> 'a t) -> 'a -> 'b list -> 'a t

  (** [pair x y] makes a pair value out of two values. *)
  val pair : 'a repr -> 'b repr -> ('a * 'b) repr

  (** [of_pair p] retrieves the values out of a pair value. *)
  val of_pair : ('a * 'b) repr -> 'a repr * 'b repr

  (** [to_list l] makes a list value out of a list of values. *)
  val to_list : 'a repr list -> 'a list repr

  (** [of_list v] retrieves a list of Plompiler values out of
      a list value. *)
  val of_list : 'a list repr -> 'a repr list

  (** [hd l] returns the head of list [l] *)
  val hd : 'a list repr -> 'a repr t

  (** [unit] is the unit value. *)
  val unit : unit repr

  (** [scalar_of_bool b] converts a boolean value into a scalar. *)
  val scalar_of_bool : bool repr -> scalar repr

  (** [unsafe_bool_of_scalar s] converts a scalar value into a bool.

      WARNING: [s] is expected to hold the values 0 or 1, but this
      is not checked. *)
  val unsafe_bool_of_scalar : scalar repr -> bool repr

  (** Assertion that two values are (structurally) equal. *)
  val assert_equal : 'a repr -> 'a repr -> unit repr t

  (** [equal a b] computes the structural equality between [a] and [b]. *)
  val equal : 'a repr -> 'a repr -> bool repr t

  val scalar_of_limbs : nb_bits:int -> scalar list repr -> scalar repr t

  (** Returns a list of Boolean variables representing the little endian
      bit decomposition of the given scalar (with the least significant bit
      on the head). *)
  val bits_of_scalar :
    ?shift:Z.t -> nb_bits:int -> scalar repr -> bool list repr t

  val limbs_of_scalar :
    ?shift:Z.t ->
    total_nb_bits:int ->
    nb_bits:int ->
    scalar repr ->
    scalar list repr t

  (** [with_label ~label c] adds a [label] to the Plompiler computation
      [c]. Useful for debugging and flamegraphs. *)
  val with_label : label:string -> 'a t -> 'a t

  (** Prints on stdout the prefix string and the repr. It works only when
      running the Result interpreter, it has no effect in the Circuit
      interpreter. *)
  val debug : string -> 'a repr -> unit repr t

  module Num :
    NUM
      with type scalar = scalar
       and type 'a repr = 'a repr
       and type 'a t = 'a t

  module Bool :
    BOOL
      with type scalar = scalar
       and type 'a repr = 'a repr
       and type 'a t = 'a t

  (** Module for describing operations over fixed size integers *)
  module Limb (N : sig
    val nb_bits : int
  end) : sig
    (** [xor_lookup a b] returns the exclusive disjunction of [a] and [b].
      This primitive uses a precomputed lookup table called "xor" ^ [nb_bits].
    *)
    val xor_lookup : scalar repr -> scalar repr -> scalar repr t

    (** [band_lookup a b] returns the conjunction of [a] and [b].
      This primitive uses a precomputed lookup table called "band" ^ [nb_bits].
    *)
    val band_lookup : scalar repr -> scalar repr -> scalar repr t

    (** [bnot_lookup b] returns the negation of [b].
      This primitive uses a precomputed lookup table called "bnot" ^ [nb_bits].
    *)
    val bnot_lookup : scalar repr -> scalar repr t

    (** [rotate_right_lookup x y i] returns the low [nb_bits] of
      [rotate_right (x + y * 2 ^ nb_bits) i] where [0 < i < nb_bits].
      This primitive uses a precomputed lookup table called
      "rotate_right" ^ [nb_bits] ^ "_" ^ [i].
    *)
    val rotate_right_lookup : scalar repr -> scalar repr -> int -> scalar repr t
  end

  (** Addition on ECC curves. *)
  module Ecc : sig
    (** [weierstrass_add (px, py) (qx, qy)] returns a pair [(rx, ry)]
        representing point addition over the Jubjub curve in Weierstrass
        coordinates of the given input points. Namely, it enforces constraints
        [rx = λ² - (px + qx)] and [ry = λ * (px - rx) - py],
        where [λ := (qy - py) / (qx - px)].
    *)
    val weierstrass_add :
      (scalar * scalar) repr ->
      (scalar * scalar) repr ->
      (scalar * scalar) repr t

    (** [edwards_add (px, py) (qx, qy)] returns a pair [(rx, ry)]
        representing point addition over the Jubjub curve in Edwards
        coordinates of the given input points. Namely, it enforces constraints
        [rx = (px * qy + qx * py) / (1 + d * px * py * qx * qy)] and
        [ry = (py * qy - a * px * qx) / (1 - d * px * py * qx * qy)]
        where [a := -1] and [d] are fixed parameters of the Jubjub curve
        in this representation. See {!Lib_plonk.Ecc_gates}.
    *)
    val edwards_add :
      (scalar * scalar) repr ->
      (scalar * scalar) repr ->
      (scalar * scalar) repr t

    (** [edwards_cond_add p q b] returns [edwards_add p q] if [b] is true and
        [p] otherwise.
    *)
    val edwards_cond_add :
      (scalar * scalar) repr ->
      (scalar * scalar) repr ->
      bool repr ->
      (scalar * scalar) repr t
  end

  (* See [lib_plompiler/gadget_mod_arith.ml] for documentation on mod_arith *)
  module Mod_arith : sig
    val add :
      ?subtraction:bool ->
      label:string ->
      modulus:Z.t ->
      nb_limbs:int ->
      base:Z.t ->
      moduli:Z.t list ->
      qm_bound:Z.t * Z.t ->
      ts_bounds:(Z.t * Z.t) list ->
      scalar list repr ->
      scalar list repr ->
      scalar list repr t

    val mul :
      ?division:bool ->
      label:string ->
      modulus:Z.t ->
      nb_limbs:int ->
      base:Z.t ->
      moduli:Z.t list ->
      qm_bound:Z.t * Z.t ->
      ts_bounds:(Z.t * Z.t) list ->
      scalar list repr ->
      scalar list repr ->
      scalar list repr t

    val assert_non_zero :
      label:string ->
      modulus:Z.t ->
      is_prime:bool ->
      nb_limbs:int ->
      base:Z.t ->
      moduli:Z.t list ->
      qm_bound:Z.t * Z.t ->
      ts_bounds:(Z.t * Z.t) list ->
      scalar list repr ->
      unit repr t

    val is_zero :
      label:string ->
      modulus:Z.t ->
      is_prime:bool ->
      nb_limbs:int ->
      base:Z.t ->
      moduli:Z.t list ->
      qm_bound:Z.t * Z.t ->
      ts_bounds:(Z.t * Z.t) list ->
      scalar list repr ->
      bool repr t
  end

  (** Helper functions for the Poseidon Hash defined over the scalar
      field of the BLS12-381 curve, using S-box function [x -> x^5]. *)
  module Poseidon : sig
    (** [poseidon128_full_round ~matrix ~k (x0, y0, z0)] returns
        [\[x1; y1; z1\]] where [(x1, y1, z1)] is the result of applying
        a (shifted) Poseidon full round (parametrized by [matrix] and [k]) to
        the 3-registers state [(x0, y0, z0)].

        Here, [matrix] is a 3 x 3 matrix and [k] is a vector of 3 elements.
        Note that this is a shifted round, that is, the S-box is applied first,
        followed by the linear layer. Namely:
        [(x1, y1, z1) = matrix * (x0^5, y0^5, z0^5) + k].
    *)
    val poseidon128_full_round :
      matrix:S.t array array ->
      k:S.t array ->
      scalar repr * scalar repr * scalar repr ->
      scalar list repr t

    (** [poseidon128_four_partial_rounds ~matrix ~k (x0, y0, z0)] returns
        [\[x4; y4; z4\]] where [(x4, y4, z4)] is the result of applying
        four (shifted) Poseidon partial round (parametrized by [matrix] and
        [ks]) to the 3-registers state [(x0, y0, z0)].

        Here, [matrix] is a 3 x 3 matrix and [ks] is an array of 4 vectors of
        3 elements each (one vector for each of the 4 rounds).

        In particular, for i = 1,...,4:
        [(xi, yi, zi) = matrix * (x_{i-1}, y_{i-1}, z_{i-1}^5) + ki].
    *)
    val poseidon128_four_partial_rounds :
      matrix:S.t array array ->
      ks:S.t array array ->
      scalar repr * scalar repr * scalar repr ->
      scalar list repr t
  end

  (** Helper functions for the Anemoi Hash defined over the scalar
      field of the BLS12-381 curve. *)
  module Anemoi : sig
    (** [anemoi_round ~kx ~ky (x0, y0)] returns [(x1, y1)], the result of
        applying an Anemoi round (parametrized by [kx] and [ky]) to the
        2-registers state [(x0, y0)].

        In particular,
        [x1 = u + kx + 7 * (v + ky)] and [y1 = 7 * (u + kx) + 50 * (v + ky)]
        where [(u, v) = S-BOX(x0, y0)] defined as:
        [u := t + beta * (y0 - t^(1/5))^2 + delta] and [v := y0 - t^(1/5)]
        where [t := x0 - beta * y0^2 - gamma] and [beta], [gamma], [delta]
        are system parameters.
    *)
    val anemoi_round :
      kx:S.t -> ky:S.t -> scalar repr * scalar repr -> (scalar * scalar) repr t

    (** [anemoi_double_round ~kx1 ~ky1 ~kx2 ~ky2 (x0, y0)] returns [(x2, y2)],
        the result of applying two Anemoi rounds.

        In particular, it is equivalent to
        [anemoi_round ~kx:kx2 ~ky:ky2 (anemoi_round ~kx:kx1 ~ky:ky1 (x0, y0))],
        but models the necessary constraints with 5 PlonK rows instead of 8.

        (Note that [anemoi_round] requires 4 PlonK rows.)
    *)
    val anemoi_double_round :
      kx1:S.t ->
      ky1:S.t ->
      kx2:S.t ->
      ky2:S.t ->
      scalar repr * scalar repr ->
      (scalar * scalar) repr t

    (** [anemoi_custom ~kx1 ~ky1 ~kx2 ~ky2 (x0, y0)] returns [(x2, y2)], the
        result of applying two Anemoi rounds.

        In particular, it is equivalent to
        [anemoi_round ~kx:kx2 ~ky:ky2 (anemoi_round ~kx:kx1 ~ky:ky1 (x0, y0))],
        but models the necessary constraints with 2 Plonk rows.

        This is possible thanks to our custom gate for Anemoi double rounds.

        See {!Lib_plonk.Hash_gates}. Furthermore, the second row is "compatible"
        with the one after if another Anemoi round follows this one.
        (Our optimizer would combine such rows in that case).
    *)
    val anemoi_custom :
      kx1:S.t ->
      ky1:S.t ->
      kx2:S.t ->
      ky2:S.t ->
      scalar repr * scalar repr ->
      (scalar * scalar) repr t
  end
end
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