Module Field.Var

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.