package octez-libs

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

This module defines a description format and interpretation of the programs needed to populate the PlonK witness for a Plompiler circuit given the initial inputs.

module CS = Csir.CS
module Tables = Csir.Tables
type wire =
  1. | W of int

Index of a wire

type row =
  1. | R of int

Index of a row

type 'a tagged =
  1. | Input of 'a
  2. | Output of 'a

Input/output tag for generic lookups.

val untag : 'a tagged -> 'a

untag t unwraps a tagged value.

Descriptors for core gates.

type arith_desc = {
  1. wires : row array;
  2. linear : Csir.Scalar.t array;
  3. qm : Csir.Scalar.t;
  4. qc : Csir.Scalar.t;
  5. qx5a : Csir.Scalar.t;
  6. qx2b : Csir.Scalar.t;
  7. to_solve : wire;
}
type pow5_desc = {
  1. a : int;
  2. c : int;
}
type wires_desc = int array
type lookup_desc = {
  1. wires : int tagged array;
  2. table : string;
}
type swap_desc = {
  1. b : int;
  2. x : int;
  3. y : int;
  4. u : int;
  5. v : int;
}
type ws_desc = {
  1. x1 : int;
  2. y1 : int;
  3. x2 : int;
  4. y2 : int;
  5. x3 : int;
  6. y3 : int;
}
type ed_desc = {
  1. a : Csir.Scalar.t;
  2. d : Csir.Scalar.t;
  3. x1 : int;
  4. y1 : int;
  5. x2 : int;
  6. y2 : int;
  7. x3 : int;
  8. y3 : int;
}
type ed_cond_desc = {
  1. a : Csir.Scalar.t;
  2. d : Csir.Scalar.t;
  3. x1 : int;
  4. y1 : int;
  5. x2 : int;
  6. y2 : int;
  7. bit : int;
  8. x3 : int;
  9. y3 : int;
}
type bits_desc = {
  1. nb_bits : int;
  2. shift : Z.t;
  3. l : int;
  4. bits : int list;
}
type limbs_desc = {
  1. total_nb_bits : int;
  2. nb_bits : int;
  3. shift : Z.t;
  4. l : int;
  5. limbs : int list;
}
type pos128full_desc = {
  1. x0 : int;
  2. y0 : int;
  3. x1 : int;
  4. y1 : int;
  5. x2 : int;
  6. y2 : int;
  7. k : Csir.Scalar.t array;
  8. matrix : Linear_algebra.Make_VectorSpace(Csir.Scalar).matrix;
}
type pos128partial_desc = {
  1. a : int;
  2. b : int;
  3. c : int;
  4. a_5 : int;
  5. b_5 : int;
  6. c_5 : int;
  7. x0 : int;
  8. y0 : int;
  9. x1 : int;
  10. y1 : int;
  11. x2 : int;
  12. y2 : int;
  13. k_cols : Linear_algebra.Make_VectorSpace(Csir.Scalar).matrix array;
  14. matrix : Linear_algebra.Make_VectorSpace(Csir.Scalar).matrix;
}
type anemoi_desc = {
  1. x0 : int;
  2. y0 : int;
  3. w : int;
  4. v : int;
  5. x1 : int;
  6. y1 : int;
  7. kx : Csir.Scalar.t;
  8. ky : Csir.Scalar.t;
}
type anemoi_double_desc = {
  1. x0 : int;
  2. y0 : int;
  3. w0 : int;
  4. w1 : int;
  5. y1 : int;
  6. x2 : int;
  7. y2 : int;
  8. kx1 : Csir.Scalar.t;
  9. ky1 : Csir.Scalar.t;
  10. kx2 : Csir.Scalar.t;
  11. ky2 : Csir.Scalar.t;
}
type anemoi_custom_desc = {
  1. x0 : int;
  2. y0 : int;
  3. x1 : int;
  4. y1 : int;
  5. x2 : int;
  6. y2 : int;
  7. kx1 : Csir.Scalar.t;
  8. ky1 : Csir.Scalar.t;
  9. kx2 : Csir.Scalar.t;
  10. ky2 : Csir.Scalar.t;
}
type mod_arith_desc = {
  1. modulus : Z.t;
  2. base : Z.t;
  3. nb_limbs : int;
  4. moduli : Z.t list;
  5. qm_bound : Z.t * Z.t;
  6. ts_bounds : (Z.t * Z.t) list;
  7. inverse : bool;
  8. inp1 : int list;
  9. inp2 : int list;
  10. out : int list;
  11. qm : int;
  12. ts : int list;
}

See lib_plompiler/gadget_mod_arith.ml for documentation on mod_arith

type mod_arith_is_zero_desc = {
  1. modulus : Z.t;
  2. base : Z.t;
  3. nb_limbs : int;
  4. inp : int list;
  5. aux : int list;
  6. out : int;
}

See lib_plompiler/gadget_mod_arith.ml for documentation on mod_arith

val mod_arith_is_zero_desc_t : mod_arith_is_zero_desc Repr.t
type solver_desc =
  1. | Arith of arith_desc
  2. | Pow5 of pow5_desc
  3. | IsZero of wires_desc
  4. | IsNotZero of wires_desc
  5. | Lookup of lookup_desc
  6. | Ecc_Ws of ws_desc
  7. | Ecc_Ed of ed_desc
  8. | Ecc_Cond_Ed of ed_cond_desc
  9. | Swap of swap_desc
  10. | Skip
  11. | BitsOfS of bits_desc
  12. | LimbsOfS of limbs_desc
  13. | Poseidon128Full of pos128full_desc
  14. | Poseidon128Partial of pos128partial_desc
  15. | AnemoiRound of anemoi_desc
  16. | AnemoiDoubleRound of anemoi_double_desc
  17. | AnemoiCustom of anemoi_custom_desc
  18. | Mod_Add of mod_arith_desc
  19. | Mod_Mul of mod_arith_desc
  20. | Mod_IsZero of mod_arith_is_zero_desc
  21. | Updater of Optimizer.trace_info

Solver description language. Each core gate has a descriptor holding the data needed to compute the part of the trace it determines.

type solvers

Collection of solver descriptors for a circuit.

type t = {
  1. solvers : solvers;
  2. initial_size : int;
  3. final_size : int;
}

A solver is formed by solver descriptors together with meta-data about the size of the initial inputs and final size of the witness.

val t : t Repr.t
val empty_solver : t

Empty solver.

val append_solver : solver_desc -> t -> t

append_solver sd s sdds a solver descriptor sd to a solver s.

val solve : t -> Csir.Scalar.t array -> Csir.Scalar.t array

solve s inital computes the witness using solver s and the initial inputs.

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