package octez-libs
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=dbc3b675aee59c2c574e5d0a771193a2ecfca31e7a5bc5aed66598080596ce1c
sha512=b97ed762b9d24744305c358af0d20f394376b64bfdd758dd4a81775326caf445caa57c4f6445da3dd6468ff492de18e4c14af6f374dfcbb7e4d64b7b720e5e2a
doc/octez-libs.plompiler/Plompiler/Gadget/Sha512/argument-1-L/Num/index.html
Module L.Num
type scalar = scalarElement of the native scalar field.
type 'a repr = 'a reprRepresentation of values.
type 'a t = 'a tPlompiler program.
val constant : Csir.Scalar.t -> scalar repr tconstant s returns the constant value s.
range_check ~nb_bits s asserts that s is in the range [0, 2^nb_bits).
val custom :
?qc:Csir.Scalar.t ->
?ql:Csir.Scalar.t ->
?qr:Csir.Scalar.t ->
?qo:Csir.Scalar.t ->
?qm:Csir.Scalar.t ->
?qx2b:Csir.Scalar.t ->
?qx5a:Csir.Scalar.t ->
scalar repr ->
scalar repr ->
scalar repr tcustom ~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.
val 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 tassert_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.
val add :
?qc:Csir.Scalar.t ->
?ql:Csir.Scalar.t ->
?qr:Csir.Scalar.t ->
scalar repr ->
scalar repr ->
scalar repr tadd ~qc ~ql ~qr a b returns a value c such that ql * a + qr * b + qc = c.
val add_constant :
?ql:Csir.Scalar.t ->
Csir.Scalar.t ->
scalar repr ->
scalar repr tadd_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.
is_zero a returns a boolean c representing whether a is zero.
pow b e_bits returns the value b^e where e is the number represented by the binary decomposition e_bits.
val add_list :
?qc:Csir.Scalar.t ->
?coeffs:Csir.Scalar.t list ->
scalar list repr ->
scalar repr tadd_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.
val is_eq_const : scalar repr -> Csir.Scalar.t -> bool repr tis_eq_const a k returns whether a is equal to k.
val assert_eq_const : scalar repr -> Csir.Scalar.t -> unit repr tassert_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.