Module Plompiler.Solver

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.