package octez-libs

  1. Overview
  2. Docs
A package that contains multiple base libraries used by the Octez suite

Install 

dune-project
 Dependency

www.tezos.com Readme Edit opam file Versions (5)

Authors

  1. T
    Tezos devteam

Maintainers

  1. C
    contact@tezos.com

Sources

tezos-18.0.tar.gz
sha256=dbc3b675aee59c2c574e5d0a771193a2ecfca31e7a5bc5aed66598080596ce1c
sha512=b97ed762b9d24744305c358af0d20f394376b64bfdd758dd4a81775326caf445caa57c4f6445da3dd6468ff492de18e4c14af6f374dfcbb7e4d64b7b720e5e2a

doc/octez-libs.plompiler/Plompiler/Solver/index.html

Module Plompiler.SolverSource

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.

Sourcemodule CS = Csir.CS
Sourcemodule Tables = Csir.Tables
Sourcetype wire =
  1. | W of int

Index of a wire

Sourcetype row =
  1. | R of int

Index of a row

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

Input/output tag for generic lookups.

Sourceval untag : 'a tagged -> 'a

untag t unwraps a tagged value.

Descriptors for core gates.

Sourcetype 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;
}
Sourcetype pow5_desc = {
  1. a : int;
  2. c : int;
}
Sourcetype wires_desc = int array
Sourcetype lookup_desc = {
  1. wires : int tagged array;
  2. table : string;
}
Sourcetype swap_desc = {
  1. b : int;
  2. x : int;
  3. y : int;
  4. u : int;
  5. v : int;
}
Sourcetype ws_desc = {
  1. x1 : int;
  2. y1 : int;
  3. x2 : int;
  4. y2 : int;
  5. x3 : int;
  6. y3 : int;
}
Sourcetype 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;
}
Sourcetype 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;
}
Sourcetype bits_desc = {
  1. nb_bits : int;
  2. shift : Z.t;
  3. l : int;
  4. bits : int list;
}
Sourcetype limbs_desc = {
  1. total_nb_bits : int;
  2. nb_bits : int;
  3. shift : Z.t;
  4. l : int;
  5. limbs : int list;
}
Sourcetype 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;
}
Sourcetype 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;
}
Sourcetype 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;
}
Sourcetype 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;
}
Sourcetype 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;
}
Sourcetype 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

Sourcetype 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

Sourceval mod_arith_is_zero_desc_t : mod_arith_is_zero_desc Repr.t
Sourcetype 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.

Sourcetype solvers

Collection of solver descriptors for a circuit.

Sourcetype 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.

Sourceval t : t Repr.t
Sourceval empty_solver : t

Empty solver.

Sourceval append_solver : solver_desc -> t -> t

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

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

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