ZK-SecreC Documentation

2024.09

Module Vec

Function abs_uv

pub fn abs_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

The absolute values of the elements in the given vector on wires, all values being considered as signed integers with the number of bits given as the second argument.

Function add_preuint_uv

pub fn add_preuint_uv [ N : Nat ] ( c : uint[N] $pre @public, xs : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Adding the constant in $pre to all elements of the vector on wires.

Function add_uint_uv

pub fn add_uint_uv [ N : Nat ] ( c : uint[N] $post @prover, xs : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Vectorization

Adding the fixed value on wire to all elements of the vector on wires.

Function and_uv

pub fn and_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Pointwise logical conjunction of given two vectors on wires, 1 meaning true and 0 meaning false.

Function assert_eq_uv

pub fn assert_eq_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public ) -> () $pre @public
where
  Field[N],
  Vectorization

Assertion of terms in each pair of corresponding elements of two given vectors on wires being equal.

Function assert_lt_uv

pub fn assert_lt_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> () $pre @public
where
  Field[N],
  Vectorization

Assertion of every element in the first vector on wires being less than the corresponding element in the second vector on wire. All values are considered as unsigned integers with the number of bits given as the third argument.

Function assert_one_uv

pub fn assert_one_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public ) -> () $pre @public
where
  Field[N],
  Vectorization

Assertion of all elements of given vector on wires being equal to one.

Function assert_zero_uv

pub fn assert_zero_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public ) -> () $pre @public
where
  Field[N],
  Vectorization

Assertion of all elements of given vector on wires being zeros.

Function bitextract_uv

pub fn bitextract_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> list[arr[uint[N] $post @prover] $pre @public] $pre @public
where
  Field[N],
  Vectorization

The little endian binary representations of the integers in the given vector on wires. The second argument is the public length of the resulting list of vectors on wires. Every vector in the resulting list 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 check_bit_uv

pub fn check_bit_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public ) -> () $pre @public
where
  Field[N],
  Vectorization

Assertion that all elements of the given vector on wires are bits (either 0 or 1).

Function ge_uv

pub fn ge_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Pointwise greater-than-or-equal-to relation of two vectors on wires, all values being considered as unsigned integers with the number of bits given as the third argument. In the result, 1 means true (in relation), 0 means false (not in relation).

Function ge_uv_uint

pub fn ge_uv_uint [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, y : uint[N] $post @prover, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Greater-than-or-equal-to relation applied to each element of the given vector on wires and the fixed value on wire. All values are considered as unsigned integers with the number of bits given as the third argument. In the result, 1 means true (in relation), 0 means false (not in relation).

Function gt_uv

pub fn gt_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Pointwise greater-than relation of two vectors on wires, all values being considered as unsigned integers with the number of bits given as the third argument. In the result, 1 means true (in relation), 0 means false (not in relation).

Function gt_uv_uint

pub fn gt_uv_uint [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, y : uint[N] $post @prover, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Greater-than relation applied to each element of the given vector on wires and the fixed value on wire. All values are considered as unsigned integers with the number of bits given as the third argument. In the result, 1 means true (in relation), 0 means false (not in relation).

Function is_nonnegative_uv

pub fn is_nonnegative_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

The signs of the elements in the given vector on wires, all considered as signed integers with the number of bits given as the second argument. In the result, 1 means non-negative and 0 means negative.

Function le_uv

pub fn le_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Pointwise less-than-or-equal-to relation of two vectors on wires, all values being considered as unsigned integers with the number of bits given as the third argument. In the result, 1 means true (in relation), 0 means false (not in relation).

Function le_uv_uint

pub fn le_uv_uint [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, y : uint[N] $post @prover, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Less-than-or-equal-to relation applied to each element of the given vector on wires and the fixed value on wire. All values are considered as unsigned integers with the number of bits given as the third argument. In the result, 1 means true (in relation), 0 means false (not in relation).

Function lt_uv

pub fn lt_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Pointwise less-than relation of two vectors on wires, all values being considered as unsigned integers with the number of bits given as the third argument. In the result, 1 means true (in relation), 0 means false (not in relation).

Function lt_uv_uint

pub fn lt_uv_uint [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, y : uint[N] $post @prover, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Less-than relation applied to each element of the given vector on wires and the fixed value on wire. All values are considered as unsigned integers with the number of bits given as the third argument. In the result, 1 means true (in relation), 0 means false (not in relation).

Function max_uint_uv

pub fn max_uint_uv [ N : Nat ] ( x : uint[N] $post @prover, ys : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Maximum of each element of the given vector on wires with the fixed value on wire. All values are considered as unsigned integers with the number of bits given as the third argument.

Function max_uv

pub fn max_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Pointwise maximum of two vectors on wires, all values being considered as unsigned integers with the number of bits given as the third argument.

Function min_uint_uv

pub fn min_uint_uv [ N : Nat ] ( x : uint[N] $post @prover, ys : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Minimum of each element of the given vector on wires with the fixed value on wire. All values are considered as unsigned integers with the number of bits given as the third argument.

Function min_uv

pub fn min_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Pointwise minimum of two vectors on wires, all values being considered as unsigned integers with the number of bits given as the third argument.

Function mul_preuint_uv

pub fn mul_preuint_uv [ N : Nat ] ( c : uint[N] $pre @public, xs : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Multiplying all elements of the vector on wires with the constant in $pre.

Function mul_uint_uv

pub fn mul_uint_uv [ N : Nat ] ( c : uint[N] $post @prover, xs : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Vectorization

Multiplying all elements of the vector on wires with the fixed value on wire.

Function negate_uv

pub fn negate_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Negating all elements of the vector on wires.

Function not_uv

pub fn not_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Pointwise logical negation of given vector on wires, 1 meaning true and 0 meaning false.

Function or_uv

pub fn or_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Pointwise logical disjunction of given two vectors on wires, 1 meaning true and 0 meaning false.

Function prod_uv

unchecked eff [*] -> * ! <$post>
pub fn prod_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public ) -> uint[N] $post @prover
where
  Vectorization

The product of all elements of a vector on wires.

Function scalar_prod_uv

pub fn scalar_prod_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public ) -> uint[N] $post @prover
where
  Vectorization

The scalar (dot) product of two vectors on wires.

Function sub_preuint_uv

pub fn sub_preuint_uv [ N : Nat ] ( c : uint[N] $pre @public, xs : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Subtracting all elements of a vector on wires from a constant in $pre.

Function sub_uint_uv

pub fn sub_uint_uv [ N : Nat ] ( c : uint[N] $post @prover, xs : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Subtracting all elements of a vector on wires from a fixed value on wire.

Function sub_uv

pub fn sub_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Subtracting the second vector on wires from the first one pointwise. More efficient than vectorized subtraction due to negation being done via multiplying by constant -1 in $pre.

Function sum_uv

unchecked eff [*] -> * ! <$post>
pub fn sum_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public ) -> uint[N] $post @prover
where
  Vectorization

The sum of all elements of a vector on wires.

Function vectorized_bitextracts

pub fn vectorized_bitextracts [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, len : uint[18446744073709551616] $pre @public ) -> list[arr[uint[N] $post @prover] $pre @public] $pre @public
where
  Field[N],
  Vectorization

A synonym of bitextract_uv.

Function xor_uv

pub fn xor_uv [ N : Nat ] ( xs : arr[uint[N] $post @prover] $pre @public, ys : arr[uint[N] $post @prover] $pre @public ) -> arr[uint[N] $post @prover] $pre @public
where
  Field[N],
  Vectorization

Pointwise xor of given two vectors on wires, 1 meaning true and 0 meaning false.