Module type Snark_intf.Field_checked_intf

type field
type field_var
type scale_field
type _ checked
type boolean_var

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 : field_var -> field_var checked

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.

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.

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

If x is 0, this raises a Failure.

val is_square : field_var -> boolean_var checked

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

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

val sqrt_check : field_var -> (field_var * boolean_var) checked

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.

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 : field_var -> length:int -> boolean_var list checked

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 : field_var -> length:int -> (boolean_var list * [ `Success of boolean_var ]) checked

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 -> field_var -> boolean_var checked

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 : field_var -> length:int -> boolean_var list checked

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 -> field_var -> field_var -> comparison_result checked

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_:field_var -> else_:field_var -> field_var checked

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

Infix notations for the basic field operations.

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

Assertions