ZK-SecreC Documentation

2024.09

Module Builtin

Function !

pub fn ! [ N : Nat, $S, @D ] ( x1 : bool[N] $S @D ) -> bool[N] $S @D

The logical negation of the given boolean.

Function !=

pub fn != [ N : Nat, @D ] ( x1 : uint[N] $pre @D, x2 : uint[N] $pre @D ) -> bool[N] $pre @D

The boolean indicating if the given two integers are distinct.

Function %

pub fn % [ N : Nat, @D ] ( x1 : uint[N] $pre @D, x2 : uint[N] $pre @D ) -> uint[N] $pre @D

The remainder upon division of the first given integer by the second one.

Function &

pub fn & [ N : Nat, $S, @D ] ( x1 : bool[N] $S @D, x2 : bool[N] $S @D ) -> bool[N] $S @D

The logical and of the given two booleans.

Function *

pub fn * [ N : Nat, $S, @D ] ( x1 : uint[N] $S @D, x2 : uint[N] $S @D ) -> uint[N] $S @D

Modular multiplication of the given two integers.

Function +

pub fn + [ N : Nat, $S, @D ] ( x1 : uint[N] $S @D, x2 : uint[N] $S @D ) -> uint[N] $S @D

Modular addition of the given two integers.

Function -

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

Modular subtraction of the second given integer from the first one.

Function /

pub fn / [ N : Nat, @D ] ( x1 : uint[N] $pre @D, x2 : uint[N] $pre @D ) -> uint[N] $pre @D

Integral division of the first given integer by the second one.

Function <

pub fn < [ N : Nat, @D ] ( x1 : uint[N] $pre @D, x2 : uint[N] $pre @D ) -> bool[N] $pre @D

The boolean indicating if the first of the given two integers is less than the second one.

Function <=

pub fn <= [ N : Nat, @D ] ( x1 : uint[N] $pre @D, x2 : uint[N] $pre @D ) -> bool[N] $pre @D

The boolean indicating if the first of the given two integers is less than or equal to the second one.

Function ==

pub fn == [ N : Nat, @D ] ( x1 : uint[N] $pre @D, x2 : uint[N] $pre @D ) -> bool[N] $pre @D

The equality of the given two integers as a boolean.

Function >

pub fn > [ N : Nat, @D ] ( x1 : uint[N] $pre @D, x2 : uint[N] $pre @D ) -> bool[N] $pre @D

The boolean indicating if the first of the given two integers is greater than the second one.

Function >=

pub fn >= [ N : Nat, @D ] ( x1 : uint[N] $pre @D, x2 : uint[N] $pre @D ) -> bool[N] $pre @D

The boolean indicating if the first of the given two integers is greater than or equal to the second one.

Function ^

pub fn ^ [ N : Nat, $S, @D ] ( x1 : bool[N] $S @D, x2 : bool[N] $S @D ) -> bool[N] $S @D

The logical xor of the given two booleans. Synonym of xor.

Function __add

pub fn __add [ N : Nat, @D ] ( x1 : arr[uint[N] $post @D] $pre @public, x2 : arr[uint[N] $post @D] $pre @public ) -> arr[uint[N] $post @D] $pre @public
where
  Field[N],
  Vectors

Pointwise modular addition of the given two vectors. Makes use of the vectors plugin.

Function __add_scalar

pub fn __add_scalar [ N : Nat, @D ] ( x1 : arr[uint[N] $post @D] $pre @public, x2 : uint[N] $post @D ) -> arr[uint[N] $post @D] $pre @public
where
  Field[N],
  Vectors

Modular addition of the value x2 to every element of the vector x1. Makes use of the vectors plugin.

Function __addc

pub fn __addc [ N : Nat, @D ] ( x1 : arr[uint[N] $post @D] $pre @public, x2 : uint[N] $pre @public ) -> arr[uint[N] $post @D] $pre @public
where
  Field[N],
  Vectors

Modular addition of the constant x2 to every element of the vector x1. Makes use of the vectors plugin.

Function __assert_perm

pub fn __assert_perm [ N : Nat, @D ] ( x1 : arr[uint[N] $post @D] $pre @public, x2 : arr[uint[N] $post @D] $pre @public ) -> () $pre @public
where
  Field[N],
  PermutationCheck

Checking if the given two vectors are permutations of each other. If the check fails then the whole proof fails. Makes use of the permutation_check plugin.

Function __bitextract

pub fn __bitextract [ N : Nat, @D ] ( x1 : uint[N] $post @D ) -> arr[uint[N] $post @D] $pre @public
where
  Field[N],
  ExtendedArithmetic

The big endian binary representation of the given integer, with the minimal length that can accommodate all elements of the field. Makes use of the extended_arithmetic plugin.

Function __default_value

pub fn __default_value [ T : Unqualified, $S, @D ] ( x1 : () $pre @public ) -> T $S @D
where
  has-default-value[T $S @D]

The default value of given type. For integers the value is 0, for booleans the value is false, default containers are empty, and structured types are filled recursively with default values.

Function __div

pub fn __div [ N : Nat, @D ] ( x1 : uint[N] $post @D, x2 : uint[N] $post @D ) -> uint[N] $post @D
where
  Field[N],
  ExtendedArithmetic

Integral division of the first given integer by the second one. Makes use of the extended_arithmetic plugin.

Function __divmod

pub fn __divmod [ N : Nat, @D ] ( x1 : uint[N] $post @D, x2 : uint[N] $post @D ) -> tuple[uint[N] $post @D, uint[N] $post @D] $pre @public
where
  Field[N],
  ExtendedArithmetic

Integral division of the first given integer by the second one, producing the quotient and the remainder together in a pair. Makes use of the extended_arithmetic plugin.

Function __dotprod

pub fn __dotprod [ N : Nat, @D ] ( x1 : arr[uint[N] $post @D] $pre @public, x2 : arr[uint[N] $post @D] $pre @public ) -> uint[N] $post @D
where
  Field[N],
  Vectors

The scalar product of the given two vectors. Makes use of the vectors plugin.

Function __get_sorting_permutation

pub fn __get_sorting_permutation [ @D ] ( x1 : list[uint $pre @D] $pre @public ) -> list[uint[18446744073709551616] $pre @D] $pre @public

The permutation that sorts the input.

Function __le

pub fn __le [ N : Nat, @D ] ( x1 : uint[N] $post @D, x2 : uint[N] $post @D ) -> bool[N] $post @D
where
  Field[N],
  ExtendedArithmetic

The boolean indicating if the first of the given two integers is less than or equal to the second one. Makes use of the extended_arithmetic plugin.

Function __lt

pub fn __lt [ N : Nat, @D ] ( x1 : uint[N] $post @D, x2 : uint[N] $post @D ) -> bool[N] $post @D
where
  Field[N],
  ExtendedArithmetic

The boolean indicating if the first of the given two integers is less than the second one. Makes use of the extended_arithmetic plugin.

Function __make_waksman_network

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

Constructing a Waksman permutation network of the given order.

Function __mod_invert

pub fn __mod_invert [ @D ] ( x1 : uint $pre @D, x2 : uint $pre @D ) -> uint $pre @D

The inverse of x1 modulo x2.

Function __mul

pub fn __mul [ N : Nat, @D ] ( x1 : arr[uint[N] $post @D] $pre @public, x2 : arr[uint[N] $post @D] $pre @public ) -> arr[uint[N] $post @D] $pre @public
where
  Field[N],
  Vectors

Pointwise modular multiplication of the given two vectors. Makes use of the vectors plugin.

Function __mul_scalar

pub fn __mul_scalar [ N : Nat, @D ] ( x1 : arr[uint[N] $post @D] $pre @public, x2 : uint[N] $post @D ) -> arr[uint[N] $post @D] $pre @public
where
  Field[N],
  Vectors

Modular multiplication of every element of the vector x1 with the value x2. Makes use of the vectors plugin.

Function __mulc

pub fn __mulc [ N : Nat, @D ] ( x1 : arr[uint[N] $post @D] $pre @public, x2 : uint[N] $pre @public ) -> arr[uint[N] $post @D] $pre @public
where
  Field[N],
  Vectors

Modular multiplication of every element of the vector x1 with the constant x2. Makes use of the vectors plugin.

Function __permutation_switches

pub fn __permutation_switches [ @D ] ( x1 : list[uint[18446744073709551616] $pre @D] $pre @public ) -> list[bool $pre @D] $pre @public

Producing switches which, when input to the Waksman network of the order of the length of the given permutation, lead to the given permutation.

Function __prod

pub fn __prod [ N : Nat, @D ] ( x1 : arr[uint[N] $post @D] $pre @public ) -> uint[N] $post @D
where
  Field[N],
  Vectors

The product of all elements of the given vector. Makes use of the vectors plugin.

Function __sum

pub fn __sum [ N : Nat, @D ] ( x1 : arr[uint[N] $post @D] $pre @public ) -> uint[N] $post @D
where
  Field[N],
  Vectors

The sum of all elements of the given vector. Makes use of the vectors plugin.

Function array_to_post

pub fn array_to_post [ T : Unqualified, @D ] ( x1 : arr[T $pre @D] $pre @public ) -> arr[T $post @D] $pre @public
where
  Vectorization

Putting all elements of the given vector onto wires in a consecutive range.

Function array_to_prover

pub fn array_to_prover [ N : Nat ] ( x1 : arr[uint[N] $post @verifier] $pre @public ) -> arr[uint[N] $post @prover] $pre @public

Lifting all elements of the given vector to the prover’s domain.

Function assert

pub fn assert [ @D, N : Nat ] ( x1 : bool[N] $post @D ) -> () $pre @public
where
  Field[N]

Checking if the given boolean is true. If this check fails then the whole proof fails.

Function assert_eq

pub fn assert_eq [ @D, T1 : Unqualified, T2 : Unqualified ] ( x1 : T1 $post @D, x2 : T2 $post @D ) -> () $pre @public
where
  assert-eq[T1,T2]

Checking if the given two field elements are equal as integers. If this check fails then the whole proof fails.

Function assert_eq_uints_bools

pub fn assert_eq_uints_bools [ N1 : Nat, @D ] ( x1 : list[uint[N1] $post @D] $pre @public, x2 : list[bool[2] $post @D] $pre @public ) -> () $pre @public
where
  Field[N1],
  Field[2]

Checking if the given field element, represented as the singleton element of the given list of integers, equals the number represented by the given list of booleans. The latter binary representation is little-endian.

Function assert_zero

pub fn assert_zero [ @D, N : Nat ] ( x1 : uint[N] $post @D ) -> () $pre @public
where
  Field[N]

Checking if the given field element equals zero. If this check fails then the whole proof fails.

Function bitextract_pre_uint

pub fn bitextract_pre_uint [ N : Nat, @D ] ( x1 : uint[N] $pre @D, x2 : uint $pre @public ) -> list[uint[N] $pre @D] $pre @public

The little endian binary representation of the integer x1. The result list contains x2 elements. If this number of bits is not enough to represent x1 then a run time error occurs.

Function bitextract_vec_helper

pub fn bitextract_vec_helper [ N : Nat, @D ] ( x1 : list[uint[N] $post @D] $pre @public, x2 : uint[18446744073709551616] $pre @public ) -> list[arr[uint[N] $post @D] $pre @public] $pre @public
where
  Vectorization

The little endian binary representations of the integers in $pre in the list x1. The result list contains x2 elements. Every element in the resulting list is a vector that contains the corresponding bit in each representation. If any of the integers cannot be represented by the expected number of bits then a run time error occurs.

Function call

pub fn call [ N : Nat, $S, @D ] ( x1 : string $pre @public, x2 : list[list[bool[N] $S @D] $pre @public] $pre @public ) -> list[list[bool[N] $S @D] $pre @public] $pre @public

Calling a circuit x1 with x2 as input. The circuit search path can be specified via the --circuits argument when compiling the program. Each element in the outer list of x2 corresponds to one input in the circuit and the inner list corresponds to the bits of that input. The return value is a list of bit arrays corresponding to the outputs of the circuit.

Function callu

pub fn callu [ $S, @D ] ( x1 : string $pre @public, x2 : list[uint[18446744073709551616] $S @D] $pre @public ) -> list[uint[18446744073709551616] $S @D] $pre @public

Calling a circuit x1 with x2 as input. The circuit search path can be specified via the --circuits argument when compiling the program. This variant of the call function assumes the inputs as 64-bit integers and produces outputs in the same form.

Function challenge

pub fn challenge [ N : Nat ] ( x1 : uint $pre @public ) -> list[uint[N] $pre @verifier] $pre @public
where
  Field[N],
  Challenge[N]

Producing a list of random field elements.

Function dbg_print

pub fn dbg_print [ @D ] ( x1 : string $pre @D ) -> () $pre @public

Printing the given string to standard output.

Function field_bit_width

pub fn field_bit_width ( x1 : uint $pre @public ) -> uint[18446744073709551616] $pre @public

The number of bits required to represent the given integer.

Function flatten

pub fn flatten [ T : Unqualified, $S, @D, @DL ] ( x1 : arr[T $S @D] $pre @DL ) -> arr[T $S @D] $pre @DL
where
  Sized[T]

Converting a tensor to a one-dimensional vector.

Function freeze

pub fn freeze [ T : Unqualified, $S, @D, @DL ] ( x1 : list[T $S @D] $pre @DL ) -> arr[T $S @D] $pre @DL
where
  Sized[T],
  Vectorization

Converting a list to a vector of the same values in the same order.

Function get_instance

pub fn get_instance [ T : Unqualified, $S, @D ] ( x1 : string $pre @public ) -> T $S @D
where
  instance-input[T,$S,@D]

Loading a value from the instance json file. The instance file can be passed to the compiler via the --instance argument.

Function get_public

pub fn get_public [ T : Unqualified, $S, @D ] ( x1 : string $pre @public ) -> T $S @D
where
  public-input[T,$S,@D]

Loading a value from the public json file. The public file can be passed to the compiler via the --public argument.

Function get_witness

pub fn get_witness [ T : Unqualified, $S, @D ] ( x1 : string $pre @public ) -> T $S @D
where
  witness-input[T,$S,@D]

Loading a value from the witness json file. The witness file can be passed to the compiler via the --witness argument.

Function index_tensor

pub fn index_tensor [ T : Unqualified, $S, @D, @DL ] ( x1 : arr[T $S @D] $pre @DL, x2 : list[uint[18446744073709551616] $pre @DL] $pre @DL ) -> T $S @D
where
  Sized[T]

Lookup of an element at position x2 in the tensor x1.

Function index_tensor_1

pub fn index_tensor_1 [ T : Unqualified, $S, @D, @DL ] ( x1 : arr[T $S @D] $pre @DL, x2 : uint[18446744073709551616] $pre @DL ) -> arr[T $S @D] $pre @DL
where
  Sized[T]

Subtensor of the tensor x1 corresponding to the index value x2 of its first dimension.

Function length

pub fn length [ TC : Qualified -> Unqualified, T : Unqualified, $S, @D, @DL ] ( x1 : TC[T $S @D] $pre @DL ) -> uint[18446744073709551616] $pre @DL
where
  Array[TC]

The length of the list or vector.

Function make_not_unknown

pub fn make_not_unknown [ N : Nat, @D ] ( x1 : uint[N] $post @D, x2 : uint[N] $pre @D ) -> uint[N] $post @D

Associating a new $pre value, given in the second argument, to an unknown value given in the first argument.

Function make_unknown

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

Forgetting the $pre copy of the value in order to save memory and time.

Function mod_div

pub fn mod_div [ N : Nat, @D ] ( x1 : uint[N] $pre @D, x2 : uint[N] $pre @D ) -> uint[N] $pre @D
where
  Field[N]

Modular division of the first given integer by the second one.

Function size

pub fn size [ T : Unqualified, $S, @D, @DL ] ( x1 : arr[T $S @D] $pre @DL ) -> list[uint[18446744073709551616] $pre @DL] $pre @DL
where
  Sized[T]

The list of dimensions of the given tensor.

Function string_append

pub fn string_append [ @D ] ( x1 : string $pre @D, x2 : string $pre @D ) -> string $pre @D

Concatenating the given two strings.

Function thaw

pub fn thaw [ T : Unqualified, $S, @D, @DL ] ( x1 : arr[T $S @D] $pre @DL ) -> list[T $S @D] $pre @DL
where
  Sized[T],
  Vectorization

Converting a vector to a list of the same values in the same order.

Function to_string

pub fn to_string [ T : Unqualified, @D ] ( x1 : T $pre @D ) -> string $pre @D
where
  ToString[T]

A string representation of the value.

Function uint_n_pre_matrix_prod

pub fn uint_n_pre_matrix_prod [ N : Nat, @D ] ( x1 : list[list[uint[N] $pre @D] $pre @public] $pre @public, x2 : list[list[uint[N] $pre @D] $pre @public] $pre @public ) -> list[list[uint[N] $pre @D] $pre @public] $pre @public

Multiplying the matrix x1 with the transposed matrix x2.

Function unflatten

pub fn unflatten [ T : Unqualified, $S, @D, @DL ] ( x1 : arr[T $S @D] $pre @DL, x2 : list[uint[18446744073709551616] $pre @DL] $pre @DL ) -> arr[T $S @D] $pre @DL
where
  Sized[T]

Converting a given vector x1 to a tensor of dimensions given by the list x2.

Function unslice

pub fn unslice [ TC : Qualified -> Unqualified, T : Unqualified, $S, @D, @DL ] ( x1 : TC[T $S @D] $pre @DL ) -> TC[T $S @D] $pre @DL
where
  Array[TC]

Converting a slice of a list or vector to a new list or vector.

Function xor

pub fn xor [ N : Nat, $S, @D ] ( x1 : bool[N] $S @D, x2 : bool[N] $S @D ) -> bool[N] $S @D

The logical xor of the given two booleans.

Function |

pub fn | [ N : Nat, $S, @D ] ( x1 : bool[N] $S @D, x2 : bool[N] $S @D ) -> bool[N] $S @D

The logical or of the given two booleans.