Module Std

Function ++


pub  fn ++
[
@D
]
(   x : string $pre @D,
   y : string $pre @D
) 
-> string $pre @D

Synonym for string append.

Function all


pub  fn all
[
$S,
@D,
N : Nat
]
(   xs : list[bool[N] $S @D] $pre @public
) 
-> bool[N] $S @D

True iff all elements of the given list with boolean elements are true.

Function all_pre


pub  fn all_pre
[
@D,
@D1,
N : Nat
]
(   xs : list[bool[N] $pre @D] $pre @D1
) 
-> bool[N] $pre @D

where

  @D1 <= @D

True iff all elements of the given list with boolean elements in $pre are true.

Function any


pub  fn any
[
$S,
@D,
N : Nat
]
(   xs : list[bool[N] $S @D] $pre @public
) 
-> bool[N] $S @D

True iff at least one element of the given list with boolean elements is true.

Function any_pre


pub  fn any_pre
[
@D,
@D1,
N : Nat
]
(   xs : list[bool[N] $pre @D] $pre @D1
) 
-> bool[N] $pre @D

where

  @D1 <= @D

True iff at least one element of the given list with boolean elements in $pre is true.

Function append


pub  fn append
[
T : Qualified
]
(   x : list[T] $pre @public,
   y : list[T] $pre @public
) 
-> list[T] $pre @public

Concatenating of two lists.

Function bool_cond


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

pub  fn bool_cond
[
M : Nat,
N : Nat,
$S,
@D
]
(   b : bool[M] $S @D,
   x : bool[N] $S @D,
   y : bool[N] $S @D
) 
-> bool[N] $S @D

where

  Field[N],

  Convertible[M,N]

Choice between two booleans. Oblivious in $post @prover, evaluating both branches.

Function bool_downcast


unchecked eff * -> * ! <$S>

pub  fn bool_downcast
[
N : Nat,
$S,
@D
]
(   b : bool[N] $pre @D
) 
-> bool[N] $S @D

where

  Field[N]

Downcasting the elements of the given list of booleans in the stage $pre into the given stage. If the given stage is $pre then does nothing, otherwise applies wire.

Function bool_ensure_post


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

where

  Field[N]

Ensuring that the elements of the given list of booleans are in $post. If they are then does nothing, otherwise applies wire.

Function bool_list_to_post


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

where

  Field[N]

Putting the elements of the given list with boolean elements in $pre on wires.

Function bool_list_to_pre


pub  fn bool_list_to_pre
[
N : Nat,
$S,
@D
]
(   xs : list[bool[N] $S @D] $pre @public
) 
-> list[bool[N] $pre @D] $pre @public

Converting the elements of the given list of booleans to the stage $pre.

Function bool_list_to_prover


pub  fn bool_list_to_prover
[
N : Nat,
$S,
@D
]
(   xs : list[bool[N] $S @D] $pre @public
) 
-> list[bool[N] $S @prover] $pre @public

Converting the elements of the given list of booleans to the domain @prover.

Function bool_list_to_uint


pub  fn bool_list_to_uint
[
N : Nat,
$S,
@D
]
(   xs : list[bool[N] $S @D] $pre @public
) 
-> list[uint[N] $S @D] $pre @public

Converting the elements of the given list of booleans to integers.

Function concat


pub  fn concat
[
T : Qualified
]
(   xss : list[list[T] $pre @public] $pre @public
) 
-> list[T] $pre @public

Concatenating of all element lists of the given list of lists. Assumes that all element lists have the same length.

Function concat_non_rectangle


pub  fn concat_non_rectangle
[
T : Qualified
]
(   xss : list[list[T] $pre @public] $pre @public
) 
-> list[T] $pre @public

Concatenating of all element lists of the given list of lists.

Function conditional_assert


pub  fn conditional_assert
[
@D,
N : Nat
]
(   c : bool[N] $post @D,
   b : bool[N] $post @D
) 
-> () $pre @public

where

  Field[N]

Assertion, provided that the given condition is true.

Function conditional_assert_zero


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

where

  Field[N]

Assertion of equality to zero, provided that the given condition is true.

Function count


pub  fn count
[
$S,
@D,
X : Qualified,
N : Nat
]
(   l : list[X] $pre @public,
   p : X -> bool[N] $S @D
) 
-> uint[N] $S @D

The number of elements satisfying the given predicate in the given list.

Function count_pre


pub  fn count_pre
[
T : Unqualified,
N : Nat,
@D,
@D1
]
(   l : list[T $pre @D] $pre @D,
   p : T $pre @D -> bool[N] $pre @D1
) 
-> uint[N] $pre @D1

The number of elements satisfying the given predicate in the given list with elements in $pre.

Function duplicate_indices


pub  fn duplicate_indices
(   amounts : list[uint[18446744073709551616] $pre @public] $pre @public
) 
-> list[uint[18446744073709551616] $pre @public] $pre @public

Replacing of each element of the given list of numbers with the corresponding index replicated that many times.

Function equiv


pub  fn equiv
[
$S,
@D,
N : Nat
]
(   a : bool[N] $S @D,
   b : bool[N] $S @D
) 
-> bool[N] $S @D

Logical equivalence.

Function error


pub  fn error
[
@D
]
(   msg : string $pre @D
) 
-> () $pre @public

Halting immediately with an assertion failure.

Function foldl


pub  fn foldl
[
A : Qualified,
B : Qualified
]
(   f : B -> A -> B,
   x : B,
   xs : list[A] $pre @public
) 
-> B

The polymorphic left fold of the given list with the given operation and the given initial value.

Function foldl_pre


pub  fn foldl_pre
[
B : Unqualified,
$SB,
@DB,
T : Unqualified,
@D,
@D1
]
(   f : B $SB @DB -> T $pre @D -> B $SB @DB,
   x : B $SB @DB,
   xs : list[T $pre @D] $pre @D1
) 
-> B $SB @DB

where

  @D1 <= @D

The polymorphic left fold of list with elements in $pre.

Function foldr


pub  fn foldr
[
A : Qualified,
B : Qualified
]
(   f : A -> B -> B,
   x : B,
   xs : list[A] $pre @public
) 
-> B

The polymorphic right fold of the given list with the given operation and the given initial value.

Function foldr_pre


pub  fn foldr_pre
[
B : Qualified,
T : Unqualified,
@D,
@D1
]
(   f : T $pre @D -> B -> B,
   x : B,
   xs : list[T $pre @D] $pre @D1
) 
-> B

where

  @D1 <= @D

The polymorphic right fold of list with elements in $pre.

Function group


pub  fn group
[
T : Qualified
]
(   xs : list[T] $pre @public,
   l : uint[18446744073709551616] $pre @public
) 
-> list[list[T] $pre @public] $pre @public

Splitting of elements of the given list into groups of the given length.

Function id


pub  fn id
[
T : Qualified
]
(   x : T
) 
-> T

The polymorphic identity function.

Function impli


pub  fn impli
[
$S,
@D,
N : Nat
]
(   a : bool[N] $S @D,
   b : bool[N] $S @D
) 
-> bool[N] $S @D

Logical implication.

Function list_push


unchecked eff [*] -> * -> * ! <@D>

pub extern fn list_push
[
Q : Qualified,
@D
]
(  ref xs : list[Q] $pre @D,
   x : Q
) 
-> () $pre @public

Appending the given element to the end of the given list.

Function list_to_public_length


pub  fn list_to_public_length
[
T : Unqualified,
@D
]
(   xs : list[T $pre @D] $pre @D,
   n : uint[18446744073709551616] $pre @public
) 
-> list[T $pre @D] $pre @public

Truncating the given list at the given public length.

Function map


pub  fn map
[
T : Qualified,
U : Qualified
]
(   f : T -> U,
   l : list[T] $pre @public
) 
-> list[U] $pre @public

The polymorphic map of elements of the given list with the given function.

Function merge


pub  fn merge
[
N : Nat,
@D
]
(   xs : list[uint[N] $pre @D] $pre @public,
   ys : list[uint[N] $pre @D] $pre @public
) 
-> list[uint[N] $pre @D] $pre @public

Merging two lists that are assumed to be sorted into a new sorted list.

Function nonzero_challenge


unchecked eff * -> [*] ! <@public>

pub  fn nonzero_challenge
[
P : Nat
]
(   n : uint $pre @public
) 
-> list[uint[P] $pre @verifier] $pre @public

where

  Field[P],

  Challenge[P]

Generating a list of the given length and consisting of random non-zero field elements.

Function pre_uint_list_to_post_array


pub  fn pre_uint_list_to_post_array
[
N : Nat,
@D
]
(   xs : list[uint[N] $pre @D] $pre @D,
   n : uint[18446744073709551616] $pre @public
) 
-> arr[uint[N] $post @D] $pre @public

where

  Field[N],

  Vectorization

Truncating the given list with elements in $pre at the given public length and converting the result to a vector on wires.

Function prod


pub  fn prod
[
$S,
@D,
N : Nat,
A : Qualified -> Unqualified
]
(   xs : A[uint[N] $S @D] $pre @public
) 
-> uint[N] $S @D

where

  Array[A]

Product of all elements of the given list or vector.

Function prod_pre


pub  fn prod_pre
[
@D,
@D1,
N : Nat,
A : Qualified -> Unqualified
]
(   xs : A[uint[N] $pre @D] $pre @D1
) 
-> uint[N] $pre @D

where

  @D1 <= @D,

  Array[A]

Product of all elements of the given list or vector with elements in $pre.

Function reverse


pub  fn reverse
[
X : Qualified
]
(   l : list[X] $pre @public
) 
-> list[X] $pre @public

The given list reversed.

Function reverse_pre


pub  fn reverse_pre
[
T : Unqualified,
@D,
@D1
]
(   l : list[T $pre @D] $pre @D1
) 
-> list[T $pre @D] $pre @D1

where

  @D1 <= @D

The given list with elements in $pre reversed.

Function scalar_prod


pub  fn scalar_prod
[
$S,
@D,
N : Nat
]
(   xs : list[uint[N] $S @D] $pre @public,
   ys : list[uint[N] $S @D] $pre @public,
   lim : uint[18446744073709551616] $pre @public
) 
-> uint[N] $S @D

Scalar (dot) product of the initial parts of the given two lists up to the given position.

Function sort


pub  fn sort
[
@D,
N : Nat
]
(   xs : list[uint[N] $pre @D] $pre @public
) 
-> list[uint[N] $pre @D] $pre @public

Merge sort of the given list.

Function sq_sum


pub  fn sq_sum
[
$S,
@D,
N : Nat
]
(   xs : list[uint[N] $S @D] $pre @public
) 
-> uint[N] $S @D

Sum of squares of all elements of the given list.

Function sum


pub  fn sum
[
$S,
@D,
N : Nat,
A : Qualified -> Unqualified
]
(   xs : A[uint[N] $S @D] $pre @public
) 
-> uint[N] $S @D

where

  Array[A]

Sum of all elements of the given list or vector.

Function sum_pre


pub  fn sum_pre
[
@D,
@D1,
N : Nat,
A : Qualified -> Unqualified
]
(   xs : A[uint[N] $pre @D] $pre @D1
) 
-> uint[N] $pre @D

where

  @D1 <= @D,

  Array[A]

Sum of all elements of the given list or vector with elements in $pre.

Function uint_cond


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

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

where

  Field[N],

  Convertible[M,N]

Choice between two integers. Oblivious in $post @prover, evaluating both branches.

Function uint_downcast


unchecked eff * -> * ! <$S>

pub  fn uint_downcast
[
N : Nat,
$S,
@D
]
(   n : uint[N] $pre @D
) 
-> uint[N] $S @D

where

  Field[N]

Downcasting the elements of the given list of integers in the stage $pre into the given stage. If the given stage is $pre then does nothing, otherwise applies wire.

Function uint_ensure_post


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

where

  Field[N]

Ensuring that the elements of the given list of integers are in $post. If they are then does nothing, otherwise applies wire.

Function uint_list_to_post


pub  fn uint_list_to_post
[
N : Nat,
@D
]
(   xs : list[uint[N] $pre @D] $pre @public
) 
-> list[uint[N] $post @D] $pre @public

where

  Field[N]

Putting the elements of the given list with integral elements in $pre on wires.

Function uint_list_to_pre


pub  fn uint_list_to_pre
[
N : Nat,
$S,
@D
]
(   xs : list[uint[N] $S @D] $pre @public
) 
-> list[uint[N] $pre @D] $pre @public

Converting the elements of the given list of integers to the stage $pre.

Function uint_list_to_prover


pub  fn uint_list_to_prover
[
N : Nat,
$S,
@D
]
(   xs : list[uint[N] $S @D] $pre @public
) 
-> list[uint[N] $S @prover] $pre @public

Converting the elements of the given list of integers to the domain @prover.

Function undefined


pub  fn undefined
[
T : Unqualified,
$S,
@D
]
() 
-> T $S @D

An assertion failure along with an infinite loop.

Function univ_assert


unchecked eff * -> * ! <$S>

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

where

  Field[N]

Assertion that does not depend on stage.

Function univ_assert_zero


unchecked eff * -> * ! <$S>

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

where

  Field[N]

Assertion of equality to zero that does not depend on stage.

Function univ_conditional_assert


pub  fn univ_conditional_assert
[
@D,
$S,
N : Nat
]
(   c : bool[N] $S @D,
   b : bool[N] $S @D
) 
-> () $pre @public

where

  Field[N]

Assertion, provided that the given condition is true. Does not depend on stage.

Function univ_conditional_assert_zero


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

where

  Field[N]

Assertion of equality to zero, provided that the given condition is true. Does not depend on stage.

Function zip_with


pub  fn zip_with
[
T1 : Qualified,
T2 : Qualified,
T3 : Qualified,
@D
]
(   f : T1 -> T2 -> T3,
   xs : list[T1] $pre @D,
   ys : list[T2] $pre @D
) 
-> list[T3] $pre @D

The polymorphic zip of corresponding elements of two lists with the given operation. The lists must be of the same length.

Function zip_with_upto


pub  fn zip_with_upto
[
T1 : Qualified,
T2 : Qualified,
T3 : Qualified,
@D
]
(   f : T1 -> T2 -> T3,
   xs : list[T1] $pre @D,
   ys : list[T2] $pre @D,
   lim : uint[18446744073709551616] $pre @D
) 
-> list[T3] $pre @D

The polymorphic zip of corresponding elements of two lists with the given operation, up to the given position.