Module LibCircuit.Num

Element of the native scalar field.

Representation of values.

Plompiler program.

constant s returns the constant value s.

zero returns the value 0.

one returns the value 1.

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.

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.

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.

div ~den_coeff a b asserts b is non-zero and returns a value c such that a / (b * den_coeff) = c.

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

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

is_not_zero a is the opposite of is_zero a.

assert_nonzero a asserts that a is not zero.

assert_bool a asserts that a is either zero or one.

square a returns the value a^2.

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

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.

mul_list l returns the product of the elements of l.

mul_by_constant k a returns the value k * a.

is_eq_const a k returns whether a is equal to k.

assert_eq_const a k asserts that a is equal to k.

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

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.

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