Module Integer

Function div_signed


pub  fn div_signed
[
N : Nat,
@D
]
(   x : uint[N] $pre @D,
   y : uint[N] $pre @D
) 
-> uint[N] $pre @D

where

  Field[N]

Integral division, interpreting both given numbers as signed.

Function divide_modulo


unchecked eff * -> * -> * ! <$S>

pub  fn divide_modulo
[
$S,
@D,
N : Nat
]
(   x : uint[N] $S @D,
   y : uint[N] $S @D
) 
-> uint[N] $S @D

where

  Field[N]

Dividing the first given field element by the second one in the field.

Function eq


unchecked eff * -> * -> * ! <$S>

pub  fn eq
[
$S,
@D,
N : Nat
]
(   x : uint[N] $S @D,
   y : uint[N] $S @D
) 
-> bool[N] $S @D

where

  Field[N]

True iff the given two field elements are equal.

Function gcd


pub  fn gcd
[
N : Nat,
@D
]
(   x : uint[N] $pre @D,
   y : uint[N] $pre @D
) 
-> uint[N] $pre @D

The greatest common divisor of the given two arguments which are interpreted as unsigned integers. Computing is based on Euclid’s algorithm.

Function invert_modulo


pub  fn invert_modulo
[
$S,
@D,
N : Nat
]
(   x : uint[N] $S @D
) 
-> uint[N] $S @D

where

  Field[N]

The reciprocal of the given field element.

Function is_zero


unchecked eff * -> * ! <$S>

pub  fn is_zero
[
$S,
@D,
N : Nat
]
(   x : uint[N] $S @D
) 
-> bool[N] $S @D

where

  Field[N]

True iff the given field element equals zero.

Function log2


pub  fn log2
[
@D
]
(   x : uint $pre @D
) 
-> uint $pre @D

The floor of the binary logarithm of the given integer. Triggers assertion failure on non-positive arguments.

Function max_pre


pub  fn max_pre
[
@D,
N : Nat
]
(   x : uint[N] $pre @D,
   y : uint[N] $pre @D
) 
-> uint[N] $pre @D

The larger of the given two integers in $pre.

Function min_pre


pub  fn min_pre
[
@D,
N : Nat
]
(   x : uint[N] $pre @D,
   y : uint[N] $pre @D
) 
-> uint[N] $pre @D

The smaller of the given two integers in $pre.

Function neq


pub  fn neq
[
$S,
@D,
N : Nat
]
(   x : uint[N] $S @D,
   y : uint[N] $S @D
) 
-> bool[N] $S @D

where

  Field[N]

True iff the given two field elements are distinct.

Function pow_pre


unchecked eff * -> * -> * ! <$S>

pub  fn pow_pre
[
$S,
@D,
N : Nat,
M : Nat
]
(   a : uint[N] $S @D,
   m : uint[M] $pre @public
) 
-> uint[N] $S @D

where

  Field[N]

Raising a field element given as the first argument to the power of the second argument. The second argument is an integer in $pre. Computing uses the fast exponentiation algorithm.

Function pow_pre_inf


pub  fn pow_pre_inf
[
@D,
M : Nat
]
(   a : uint $pre @D,
   m : uint[M] $pre @public
) 
-> uint $pre @D

Raising an unbounded integer given as the first argument to the power of the second argument. Both arguments are in $pre. Computing uses the fast exponentiation algorithm.

Function sqr


pub  fn sqr
[
N : Nat,
$S,
@D
]
(   x : uint[N] $S @D
) 
-> uint[N] $S @D

The square of the given integer.

Function sqrt


pub  fn sqrt
[
@D
]
(   x : uint $pre @D
) 
-> uint $pre @D

The floor of the square root of the given integer. Fails if the argument is negative. Computation is based on Newton’s method.

Function uint_to_bool


unchecked eff * -> * ! <$S>

pub  fn uint_to_bool
[
$S,
@D,
N : Nat
]
(   x : uint[N] $S @D
) 
-> bool[N] $S @D

where

  Field[N]

Converting the given integer to boolean. Assumes that the argument is either 0 or 1.