package octez-libs

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

Module LibCircuit.NumSource

Sourcetype scalar = scalar

Element of the native scalar field.

Sourcetype 'a repr = 'a repr

Representation of values.

Sourcetype 'a t = 'a t

Plompiler program.

Sourceval constant : Csir.Scalar.t -> scalar repr t

constant s returns the constant value s.

Sourceval zero : scalar repr t

zero returns the value 0.

Sourceval one : scalar repr t

one returns the value 1.

Sourceval range_check : nb_bits:int -> scalar repr -> unit repr t

range_check ~nb_bits s asserts that s is in the range [0, 2^nb_bits).

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.

Sourceval assert_custom : ?qc:Csir.Scalar.t -> ?ql:Csir.Scalar.t -> ?qr:Csir.Scalar.t -> ?qo:Csir.Scalar.t -> ?qm:Csir.Scalar.t -> scalar repr -> scalar repr -> scalar repr -> unit 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.

add ~qc ~ql ~qr a b returns a value c such that ql * a + qr * b + qc = c.

Sourceval add_constant : ?ql:Csir.Scalar.t -> Csir.Scalar.t -> scalar repr -> scalar repr t

add_constant ~ql k a returns a value c such that ql * a + k = c.

mul ~qm a b returns a value c such that qm * a * b = c.

Sourceval div : ?den_coeff:Csir.Scalar.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.

Sourceval pow5 : scalar repr -> scalar repr t

pow5 a returns a value c such that a^5 = c.

Sourceval is_zero : scalar repr -> bool repr t

is_zero a returns a boolean c representing whether a is zero.

Sourceval is_not_zero : scalar repr -> bool repr t

is_not_zero a is the opposite of is_zero a.

Sourceval assert_nonzero : scalar repr -> unit repr t

assert_nonzero a asserts that a is not zero.

Sourceval assert_bool : scalar repr -> unit repr t

assert_bool a asserts that a is either zero or one.

Sourceval square : scalar repr -> scalar repr t

square a returns the value a^2.

Sourceval pow : scalar repr -> bool repr list -> scalar repr t

pow b e_bits returns the value b^e where e is the number represented by the binary decomposition e_bits.

Sourceval add_list : ?qc:Csir.Scalar.t -> ?coeffs:Csir.Scalar.t list -> scalar list repr -> scalar repr t

add_list ~qc ~coeffs l returns the sum of the elements of l weighted by coeffs.

Note: if coeffs is defined, it should be of the same length as l.

Sourceval mul_list : scalar list repr -> scalar repr t

mul_list l returns the product of the elements of l.

Sourceval mul_by_constant : Csir.Scalar.t -> scalar repr -> scalar repr t

mul_by_constant k a returns the value k * a.

Sourceval scalar_of_bytes : bool list repr -> scalar repr t
Sourceval is_eq_const : scalar repr -> Csir.Scalar.t -> bool repr t

is_eq_const a k returns whether a is equal to k.

Sourceval assert_eq_const : scalar repr -> Csir.Scalar.t -> unit repr t

assert_eq_const a k asserts that a is equal to k.

Sourceval is_upper_bounded : bound:Z.t -> scalar repr -> bool repr t

is_upper_bounded ~bound x returns whether the scalar x is strictly lower than bound when x is interpreted as an integer from 0 to p-1 (being p the scalar field order). This circuit is total (and more expensive than our version below).

Sourceval is_upper_bounded_unsafe : ?nb_bits:int -> bound:Z.t -> scalar repr -> bool repr t

Same as is_upper_bounded but cheaper and partial. is_upper_bounded_unsafe ~bound l is unsatisfiable if l cannot be represented in binary with Z.numbits bound bits.

Sourceval geq : (scalar repr * Z.t) -> (scalar repr * Z.t) -> bool repr t

geq (a, bound_a) (b, bound_b) returns the boolean wire representing a >= b. Pre-condition: a ∈ [0, bound_a) ∧ b ∈ [0, bound_b)

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