Module Snarky_integer.Integer

Positive integers as field elements.

These operations assert that the value of the field element does not exceed the largest element in the field -- ie. that the operations do not overflow.

Whenever possible, the bit representation is cached to avoid recomputing it.

module Interval : sig ... end
type 'f t = {
value : 'f Snarky_backendless.Cvar.t;
interval : Interval.t;
mutable bits : 'f Snarky_backendless.Cvar.t Snarky_backendless.Boolean.t list option;
}
val constant : ?length:int -> m:'f Snarky_backendless.Snark.m -> Bigint.t -> 'f t

Create an value representing the given constant value.

The bit representation of the constant is cached, and is padded to length when given.

val shift_left : m:'f Snarky_backendless.Snark.m -> 'f t -> int -> 'f t

shift_left ~m x k is equivalent to multiplying x by 2^k.

The result has a cached bit representation whenever the given x had a cached bit representation.

Create a value from the given bit string.

The given bit representation is cached.

Compute the bit representation of the given integer.

If the bit representation has already been cached, it is returned and no additional constraints are added. If the representation is computed, the value is updated to include the cache.

Return the cached bit representation, or raise an exception if the bit representation has not been cached.

Returns Some bs for bs the cached bit representation, or None if the bit representation has not been cached.

val div_mod : m:'f Snarky_backendless.Snark.m -> 'f t -> 'f t -> 'f t * 'f t

div_mod ~m a b = (q, r) such that a = q * b + r and r < b.

The bit representations of q and r are calculated and cached.

NOTE: This uses approximately log2(a) + 2 * log2(b) constraints.

val to_field : 'f t -> 'f Snarky_backendless.Cvar.t
val create : value:'f Snarky_backendless.Cvar.t -> upper_bound:Bigint.t -> 'f t
val min : m:'f Snarky_backendless.Snark.m -> 'f t -> 'f t -> 'f t

min ~m x y returns a value equal the lesser of x and y.

The result does not carry a cached bit representation.

val if_ : m:'f Snarky_backendless.Snark.m -> 'f Snarky_backendless.Cvar.t Snarky_backendless.Boolean.t -> then_:'f t -> else_:'f t -> 'f t
val succ : m:'f Snarky_backendless.Snark.m -> 'f t -> 'f t

succ ~m x computes the successor x+1 of x.

The result does not carry a cached bit representation.

succ_if ~m x b computes the integer x+1 if b is true, or x otherwise.

The result does not carry a cached bit representation.

val add : m:'f Snarky_backendless.Snark.m -> 'f t -> 'f t -> 'f t

add ~m x y computes x + y.

The result does not carry a cached bit representation.

val mul : m:'f Snarky_backendless.Snark.m -> 'f t -> 'f t -> 'f t

mul ~m x y computes x * y.

The result does not carry a cached bit representation.

val subtract_unpacking : m:'f Snarky_backendless.Snark.m -> 'f t -> 'f t -> 'f t

subtract_unpacking ~m x y computes x - y.

The bit representation is calculated to ensure that 0 <= x - y, and is cached in the result.

NOTE: This uses approximately log2(x) constraints.

val subtract_unpacking_or_zero : m:'f Snarky_backendless.Snark.m -> 'f t -> 'f t -> [ `Underflow of 'f Snarky_backendless.Cvar.t Snarky_backendless.Boolean.t ] * 'f t

subtract_unpacking_or_zero ~m x y computes x - y.

  • If the argument to `Underflow is true, x < y and the returned integer value is pinned to zero.
  • If the argument to `Underflow is false, x >= y and the returned integer value is equal to x - y.

The bit representation is calculated to check for underflow.

NOTE: This uses approximately log2(x) constraints.