Module Field.Checked

val mul : Var.t -> Var.t -> Var.t Checked.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 : Var.t -> Var.t Checked.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 : Var.t -> Var.t -> Var.t Checked.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 : Var.t -> Var.t Checked.t

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

If x is 0, this raises a Failure.

val is_square : Var.t -> Boolean.var Checked.t

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

val sqrt : Var.t -> Var.t Checked.t

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

val sqrt_check : Var.t -> (Var.t * Boolean.var) Checked.t

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 : Var.t -> Var.t -> Boolean.var Checked.t

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 : Var.t -> length:int -> Boolean.var list Checked.t

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 : Var.t -> length:int -> (Boolean.var list * [ `Success of Boolean.var ]) Checked.t

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 -> Var.t -> Boolean.var Checked.t

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 : Var.t -> length:int -> Boolean.var list Checked.t

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 -> Var.t -> Var.t -> comparison_result Checked.t

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_:Var.t -> else_:Var.t -> Var.t Checked.t

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

Infix notations for the basic field operations.

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

Assertions