Module BigInt

Function BigIntBlock_to_post


pub  fn BigIntBlock_to_post
[
N : Nat,
@D
]
(   x : BigIntBlock[N, $pre, @D] $pre @public
) 
-> BigIntBlock[N, $post, @D] $pre @public

where

  Field[N]

Conversion of a block of a BigInt object in the stage $pre to the stage $post.

Function BigIntBlock_to_pre


pub  fn BigIntBlock_to_pre
[
N : Nat,
@D
]
(   x : BigIntBlock[N, $post, @D] $pre @public
) 
-> BigIntBlock[N, $pre, @D] $pre @public

Conversion of a block of a BigInt object in the stage $post to the stage $pre.

Function BigInt_add


pub  fn BigInt_add
[
N : Nat,
$S,
@D
]
(   x : BigInt[N, $S, @D] $pre @public,
   y : BigInt[N, $S, @D] $pre @public
) 
-> BigInt[N, $S, @D] $pre @public

The sum of the given two BigInt objects. The result is not normalized. Fails if the numbers of bits per block differ in the given BigInt objects or the public bound of some block exceeds half of the modulus.

Function BigInt_assert_eq


pub  fn BigInt_assert_eq
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public,
   y : BigInt[N, $post, @D] $pre @public,
  ref sizeasserters : list[SizeAsserter[N, $post, @D] $pre @public] $pre @public
) 
-> () $pre @public

where

  Field[N]

Assertion that the given two BigInt objects have equal values. Fails if the given list does not contain a SizeAsserter object for the used number of bits per block.

Function BigInt_assert_le


pub  fn BigInt_assert_le
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public,
   y : BigInt[N, $post, @D] $pre @public,
  ref sizeasserters : list[SizeAsserter[N, $post, @D] $pre @public] $pre @public
) 
-> () $pre @public

where

  Field[N]

Assertion that the value of the first given BigInt object is less than or equal to that of the second one. Fails if the given list does not contain a SizeAsserter object for the used number of bits per block.

Function BigInt_assert_lt


pub  fn BigInt_assert_lt
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public,
   y : BigInt[N, $post, @D] $pre @public,
  ref sizeasserters : list[SizeAsserter[N, $post, @D] $pre @public] $pre @public
) 
-> () $pre @public

where

  Field[N]

Assertion that the value of the first given BigInt object is less than that of the second one. Fails if the given list does not contain a SizeAsserter object for the used number of bits per block.

Function BigInt_assert_nonneg


pub  fn BigInt_assert_nonneg
[
N : Nat,
@D
]
(   xn : BigInt[N, $post, @D] $pre @public,
  ref sizeasserters : list[SizeAsserter[N, $post, @D] $pre @public] $pre @public
) 
-> () $pre @public

where

  Field[N]

Assertion that the value of the given BigInt object is non-negative. Assumes that the given BigInt object is normalized. Fails if the given list does not contain a SizeAsserter object for the used number of bits per block.

Function BigInt_assert_normalization


pub  fn BigInt_assert_normalization
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public,
  ref sizeasserters : list[SizeAsserter[N, $post, @D] $pre @public] $pre @public
) 
-> () $pre @public

where

  Field[N]

Assertion that the given BigInt object in $post is normalized, i.e., the number in each block or its absolute value fits to the required number of bits. Fails if the given list does not contain a SizeAsserter object for that number of bits.

Function BigInt_assert_zero


pub  fn BigInt_assert_zero
[
N : Nat,
@D
]
(   xn : BigInt[N, $post, @D] $pre @public
) 
-> () $pre @public

where

  Field[N]

Assertion that the value of the given BigInt object is zero. Assumes that the given BigInt object is normalized.

Function BigInt_bit_width


pub  fn BigInt_bit_width
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public
) 
-> uint[18446744073709551616] $pre @public

The total number of bits in the given BigInt object.

Function BigInt_cast


pub  fn BigInt_cast
[
N : Nat,
$S,
@D1,
@D2
]
(   x : BigInt[N, $S, @D1] $pre @public
) 
-> BigInt[N, $S, @D2] $pre @public

where

  @D1 <= @D2

Conversion of a BigInt object to a higher domain.

Function BigInt_choose


pub  fn BigInt_choose
[
N : Nat,
$S,
@D
]
(   b : uint[N] $S @D,
   t : BigInt[N, $S, @D] $pre @public,
   f : BigInt[N, $S, @D] $pre @public
) 
-> BigInt[N, $S, @D] $pre @public

Oblivious choice according to the given boolean between the given two BigInt objects. The result is normalized, provided that the givens are normalized. Fails if the numbers of bits per block differ in the given BigInt objects.

Function BigInt_conditional_swap


pub  fn BigInt_conditional_swap
[
N : Nat,
$S,
@D
]
(   b : bool[N] $S @D,
   t : BigInt[N, $S, @D] $pre @public,
   f : BigInt[N, $S, @D] $pre @public
) 
-> tuple[BigInt[N, $S, @D] $pre @public, BigInt[N, $S, @D] $pre @public] $pre @public

Oblivious choice according to the given boolean between the pair of the given two BigInt objects and the pair with components swapped. The result is normalized, provided that the givens are normalized. The function can be used in the field cond_swap of the struct Waksman::ApplySwitchingNetworkInterface. Fails if the numbers of bits per block differ in the given BigInt objects.

Function BigInt_constmul


pub  fn BigInt_constmul
[
N : Nat,
@D
]
(   c : uint $pre @public,
   x : BigInt[N, $post, @D] $pre @public
) 
-> BigInt[N, $post, @D] $pre @public

where

  Field[N]

The product of the given constant in $pre and the given BigInt object in $post.

Function BigInt_eq


pub  fn BigInt_eq
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public,
   y : BigInt[N, $post, @D] $pre @public,
  ref sizeasserters : list[SizeAsserter[N, $post, @D] $pre @public] $pre @public
) 
-> bool[N] $post @D

where

  Field[N]

Test if the given two BigInt objects have equal values. Fails if the given list does not contain a SizeAsserter object for the used number of bits per block.

Function BigInt_from_bitarray


pub  fn BigInt_from_bitarray
[
N : Nat,
@D
]
(   bs : list[bool[N] $post @D] $pre @public,
   bpb : uint[18446744073709551616] $pre @public
) 
-> BigInt[N, $post, @D] $pre @public

where

  Field[N]

A new BigInt object whose value is represented by the given list of booleans (assuming little-endian representation), using the given number of bits per block.

Function BigInt_from_bool2_array


pub  fn BigInt_from_bool2_array
[
N : Nat,
@D
]
(   bs : list[bool[2] $post @D] $pre @public,
   bpb : uint[18446744073709551616] $pre @public
) 
-> BigInt[N, $post, @D] $pre @public

where

  Field[N],

  Convertible[2,N]

A new BigInt object whose value is represented by the given list of booleans (assuming little-endian representation), using the given number of bits per block.

Function BigInt_from_uint


pub  fn BigInt_from_uint
[
N : Nat,
@D
]
(   x : uint $pre @D,
   nblocks : uint[18446744073709551616] $pre @public,
   bpb : uint[18446744073709551616] $pre @public
) 
-> BigInt[N, $pre, @D] $pre @public

A new BigInt object with the given value and parameters (the number of blocks; the number of bits per block). If the allowed number of blocks is not enough to fit the number, the higher blocks are omitted.

Function BigInt_from_uint_select


pub  fn BigInt_from_uint_select
[
N : Nat,
@D
]
(   x : uint $pre @public,
   nblocks : uint[18446744073709551616] $pre @public,
   bpb : uint[18446744073709551616] $pre @public,
   sel : uint[N] $post @D
) 
-> BigInt[N, $post, @D] $pre @public

where

  Field[N]

A new BigInt object with the given value or zero value (depending on the fourth argument) and the given parameters (the number of blocks; the number of bits per block). Assumes that the fourth argument is either 0 or 1 (the first option forcing the result to be zero). If the allowed number of blocks is not enough to fit the number, the higher blocks are omitted.

Function BigInt_is_zero


pub  fn BigInt_is_zero
[
N : Nat,
@D
]
(   xn : BigInt[N, $post, @D] $pre @public
) 
-> bool[N] $post @D

where

  Field[N]

Test if the value of the given BigInt object is zero. Assumes that the given BigInt object is normalized.

Function BigInt_mod


pub  fn BigInt_mod
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public,
   y : BigInt[N, $post, @D] $pre @public,
  ref sizeasserters : list[SizeAsserter[N, $post, @D] $pre @public] $pre @public
) 
-> BigInt[N, $post, @D] $pre @public

where

  Field[N]

The remainder of the first given BigInt object upon division by the second one. Fails if the numbers of bits per block differ in the given BigInt objects or the given list does not contain a SizeAsserter object for the number of bits per block.

Function BigInt_mod_div


pub  fn BigInt_mod_div
[
N : Nat,
@D
]
(   y : BigInt[N, $post, @D] $pre @public,
   x : BigInt[N, $post, @D] $pre @public,
   p : uint $pre @public,
  ref sizeasserters : list[SizeAsserter[N, $post, @D] $pre @public] $pre @public
) 
-> BigInt[N, $post, @D] $pre @public

where

  Field[N]

Division of the first given BigInt object by the second given BigInt object in the residue class ring modulo the integer given as the third argument. The result is normalized but the integrity of normalization is not checked. Fails if the numbers of bits per block differ in the given BigInt objects.

Function BigInt_modconst


pub  fn BigInt_modconst
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public,
   y : uint $pre @public,
  ref sizeasserters : list[SizeAsserter[N, $post, @D] $pre @public] $pre @public
) 
-> BigInt[N, $post, @D] $pre @public

where

  Field[N]

The remainder of the value of the given BigInt object upon division by the given integer. The result is a normalized BigInt object. Fails if the given list does not contain a SizeAsserter object for the number of bits per block.

Function BigInt_mul


pub  fn BigInt_mul
[
N : Nat,
$S,
@D
]
(   x : BigInt[N, $S, @D] $pre @public,
   y : BigInt[N, $S, @D] $pre @public
) 
-> BigInt[N, $S, @D] $pre @public

The product of the given two BigInt objects. The result is not normalized. Fails if the numbers of bits per block differ in the given BigInt objects.

Function BigInt_mul_post


pub  fn BigInt_mul_post
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public,
   y : BigInt[N, $post, @D] $pre @public
) 
-> BigInt[N, $post, @D] $pre @public

where

  Field[N]

The product of the given two BigInt objects in $post. The result is not normalized. This computation is more efficient than that of BigInt_mul in $post.

Function BigInt_neg


pub  fn BigInt_neg
[
N : Nat,
$S,
@D
]
(   x : BigInt[N, $S, @D] $pre @public
) 
-> BigInt[N, $S, @D] $pre @public

Negation of the given BigInt object.

Function BigInt_normalize_post


pub  fn BigInt_normalize_post
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public,
  ref sizeasserters : list[SizeAsserter[N, $post, @D] $pre @public] $pre @public
) 
-> BigInt[N, $post, @D] $pre @public

where

  Field[N]

The normal form of the given BigInt object in $post. Fails if the given list does not contain a SizeAsserter object for the used number of bits per block.

Function BigInt_sub


pub  fn BigInt_sub
[
N : Nat,
$S,
@D
]
(   x : BigInt[N, $S, @D] $pre @public,
   y : BigInt[N, $S, @D] $pre @public
) 
-> BigInt[N, $S, @D] $pre @public

The difference of the given two BigInt objects. The result is not normalized. Fails if the numbers of bits per block differ in the given BigInt objects or the public bound of some block exceeds half of the modulus.

Function BigInt_to_bitarray


pub  fn BigInt_to_bitarray
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public
) 
-> list[bool[N] $post @D] $pre @public

where

  Field[N]

A little-endian representation of the value of the given BigInt object. Fails if the given BigInt object is not normalized or its value is negative.

Function BigInt_to_post


pub  fn BigInt_to_post
[
N : Nat,
@D
]
(   x : BigInt[N, $pre, @D] $pre @public
) 
-> BigInt[N, $post, @D] $pre @public

where

  Field[N]

Conversion of a BigInt object in the stage $pre to the stage $post.

Function BigInt_to_pre


pub  fn BigInt_to_pre
[
N : Nat,
@D
]
(   x : BigInt[N, $post, @D] $pre @public
) 
-> BigInt[N, $pre, @D] $pre @public

Conversion of a BigInt object in the stage $post to the stage $pre.

Function BigInt_to_string


pub  fn BigInt_to_string
[
N : Nat,
$S,
@D
]
(   x : BigInt[N, $S, @D] $pre @public
) 
-> string $pre @D

A string representation of the given BigInt object (for debugging).

Function BigInt_to_uint


pub  fn BigInt_to_uint
[
N : Nat,
$S,
@D
]
(   x : BigInt[N, $S, @D] $pre @public
) 
-> uint $pre @D

Conversion of the given BigInt object to an unsigned integer.