package octez-libs

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

Install

Dune Dependency

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

Authors

  1. T
    Tezos devteam

Maintainers

  1. C
    contact@tezos.com

Sources

octez-19.0.tar.gz
sha256=c6df840ebbf115e454db949028c595bec558a59a66cade73b52a6d099d6fa4d4
sha512=d8aee903b9fe130d73176bc8ec38b78c9ff65317da3cb4f3415f09af0c625b4384e7498201fdb61aa39086a7d5d409d0ab3423f9bc3ab989a680cf444a79bc13

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.

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