Module 1-Impl.Field

module Constant : sig ... end
include Snark_intf.Field_var_intf with type field := field and type boolean_var := Boolean.var
type t = field Cvar.t

The type that stores booleans as R1CS variables.

val length : t -> int

For debug purposes

val var_indices : t -> int list
val to_constant_and_terms : t -> field option * (field * int) list

Convert a t value to its constituent constant and a list of scaled R1CS variables.

val constant : field -> t

constant x creates a new R1CS variable containing the constant field element x.

val to_constant : t -> field option

to_constant x returns Some f if x holds only the constant field element f. Otherwise, it returns None.

val linear_combination : (field * t) list -> t

linear_combination [(f1, x1);...;(fn, xn)] returns the result of calculating f1 * x1 + f2 * x2 + ... + fn * xn. This does not add a new constraint; see Constraint.t for more information.

val sum : t list -> t

sum l returns the sum of all R1CS variables in l.

If the result would be greater than or equal to Field.size then the value will overflow to be less than Field.size.

val add : t -> t -> t

add x y returns the result of adding the R1CS variables x and y.

If the result would be greater than or equal to Field.size then the value will overflow to be less than Field.size.

val negate : t -> t

negate x returns the additive inverse of x as a field eleement

val sub : t -> t -> t

sub x y returns the result of subtracting the R1CS variables x and y.

If the result would be less than 0 then the value will underflow to be between 0 and Field.size.

val scale : t -> field -> t

scale x f returns the result of multiplying the R1CS variable x by the constant field element f.

If the result would be greater than or equal to Field.size then the value will overflow to be less than Field.size.

val project : Boolean.var list -> t

Convert a list of bits into a field element.

project [b1;...;bn] = b1 + 2*b2 + 4*b3 + ... + 2^(n-1) * bn

If the result would be greater than or equal to Field.size then the value will overflow to be less than Field.size.

val pack : Boolean.var list -> t

Convert a list of bits into a field element.

pack [b1;...;bn] = b1 + 2*b2 + 4*b3 + ... + 2^(n-1) * bn

This will raise an assertion error if the length of the list is not strictly less than number of bits in Field.size.

Use project if you know that the list represents a value less than Field.size but where the number of bits may be the maximum, or where overflow is appropriate.

include Snark_intf.Field_checked_intf with type field := field and type field_var := t and type scale_field := t and type 'a checked := 'a and type boolean_var := Boolean.var
val mul : t -> t -> t

mul x y returns the result of multiplying the R1CS variables x and y.

If the result would be greater than or equal to Field.size then the value will overflow to be less than Field.size.

val square : t -> t

square x returns the result of multiplying the R1CS variables x by itself.

If the result would be greater than or equal to Field.size then the value will overflow to be less than Field.size.

val div : t -> t -> t

div x y returns the result of dividing the R1CS variable x by y.

If x is not an integer multiple of y, the result could be any value; it is equivalent to computing mul x (inv y).

If y is 0, this raises a Failure.

val inv : t -> t

inv x returns the value such that mul x (inv x) = 1.

If x is 0, this raises a Failure.

val is_square : t -> Boolean.var

is_square x checks if x is a square in the field.

val sqrt : t -> t

sqrt x is the square root of x if x is a square. If not, this raises a Failure

val sqrt_check : t -> t * Boolean.var

If x is a square in the field and (y, b) = sqrt_check x, If b = true, then x is a square and y is sqrt(x) If b = false, then x is not a square y is a value which is not meaningful.

val equal : t -> t -> Boolean.var

equal x y returns a R1CS variable containing the value true if the R1CS variables x and y are equal, or false otherwise.

val unpack : t -> length:int -> Boolean.var list

unpack x ~length returns a list of R1CS variables containing the length lowest bits of x. If length is greater than the number of bits in Field.size then this raises a Failure.

For example,

  • unpack 8 ~length:4 = [0; 0; 0; 1]
  • unpack 9 ~length:3 = [1; 0; 0]
  • unpack 9 ~length:5 = [1; 0; 0; 1; 0]
val unpack_flagged : t -> length:int -> Boolean.var list * [ `Success of Boolean.var ]

unpack x ~length = (unpack x ~length, `Success success), where success is an R1CS variable containing true if the returned bits represent x, and false otherwise.

If length is greater than the number of bits in Field.size then this raises a Failure.

unpack x ~length returns a list of R1CS variables containing the bits of x.

val parity : ?length:int -> t -> Boolean.var

Get the least significant bit of a field element x. Pass a value for length if you know that x fits in length many bits.

val choose_preimage_var : t -> length:int -> Boolean.var list

unpack x ~length returns a list of R1CS variables containing the length lowest bits of x.

type comparison_result = {
less : Boolean.var;
less_or_equal : Boolean.var;
}

The type of results from checked comparisons, stored as boolean R1CS variables.

val compare : bit_length:int -> t -> t -> comparison_result

compare ~bit_length x y compares the bit_length lowest bits of x and y. bit_length must be <= size_in_bits - 2.

This requires converting an R1CS variable into a list of bits.

WARNING: x and y must be known to be less than 2^{bit_length} already, otherwise this function may not return the correct result.

val if_ : Boolean.var -> then_:t -> else_:t -> t

if_ b ~then_ ~else_ returns then_ if b is true, or else_ otherwise.

Infix notations for the basic field operations.

val (+) : t -> t -> t
val (-) : t -> t -> t
val (*) : t -> t -> t
module Unsafe : sig ... end
module Assert : sig ... end

Assertions

val size_in_bits : int
val size : Snarky_backendless__Snark_intf.Bignum_bigint.t
val of_int : int -> t
val one : t
val zero : t
val (/) : t -> t -> t
val typ : ( t, Constant.t ) Typ.t