ZK-SecreC Documentation

2024.09

Module FastFixedPoint

Function add_fixed

pub fn add_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

The sum of the given two fixed-point numbers. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers. Does not check that the sum fits to this number of bits. Use check_fixed to check it manually when necessary.

Function check_fixed

pub fn check_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public ) -> () $pre @public
where
  Field[N]

Check that a fixed-point number fits in its required number of bits. Can be used after an operation or a series of operations that do not do this check. Some operations (e.g. add_fixed, sub_fixed, negate_fixed) have left out this check for efficiency, so that several such operations can be done in row before calling check_fixed. This is safe if the intermediate results do not overflow the modulus (but they do not have to fit into len bits). For example, three fixed-point numbers can be added together by {let w = add_fixed(x, add_fixed(y, z)); check_fixed(w); w}, calling check_fixed only once rather than twice. This is safe if 3*(2^len - 1) < N.

Function coef_div_pre

pub fn coef_div_pre [ N : Nat, @D ] ( x : uint[N] $pre @D, y : uint[N] $pre @D, pplen : uint[18446744073709551616] $pre @public ) -> uint[N] $pre @D

A helper function used to implement division in both FastFixedPoint and FastFixedPointVec modules. Intended for standard library programmers only.

Function div_fixed

pub fn div_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

The ratio of the given two fixed-point numbers. Assumes that they are correctly formed. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers or the ratio does not fit to this number of bits. Also fails if the second operand is zero.

Function eq_fixed

pub fn eq_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the given two fixed-point numbers are equal. Assumes that they are correctly formed. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers.

Function fixed

pub fn fixed [ N : Nat, $S, @D ] ( coef : uint[N] $S @D, len : uint[18446744073709551616] $pre @public, pplen : uint[18446744073709551616] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

A new fixed-point number with the given parameters (the integral value that ignores binary point; the number of bits; the number of bits following the binary point). Fails if the integral value does not fit to the required number of bits.

Function fixed_cond

pub fn fixed_cond [ N : Nat, $S, @D ] ( b : bool[N] $S @D, x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

Oblivious choice according to the given boolean between the given two fixed-point numbers. Assumes that the numbers are correctly formed. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers.

Function fixed_nonnegative

pub fn fixed_nonnegative [ N : Nat, $S, @D ] ( coef : uint[N] $S @D, len : uint[18446744073709551616] $pre @public, pplen : uint[18446744073709551616] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

A new fixed-point number with the given parameters (the integral value that ignores binary point; the number of bits; the number of bits following the binary point). Fails if the new fixed-point number would be negative, or if the integral value does not fit to the required number of bits.

Function fixed_post

pub fn fixed_post [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $post, @D] $pre @public
where
  Field[N]

Conversion of the given fixed-point number to the stage $post, putting it on a wire if it is in $pre.

Function fixed_pre

pub fn fixed_pre [ N : Nat, $S, @D ] ( f : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $pre, @D] $pre @public

Conversion of the given fixed-point number to the stage $pre.

Function fixed_prover

pub fn fixed_prover [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @prover] $pre @public
where
  Field[N]

Conversion of the given fixed-point number to the domain @prover.

Function fixed_to_bitstring

pub fn fixed_to_bitstring [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public ) -> string $pre @D
where
  Field[N]

Representing the given fixed-point number as a bit string (for testing purposes).

Function fixed_to_string

pub fn fixed_to_string [ N : Nat, $S, @D ] ( f : Fixed[N, $S, @D] $pre @public ) -> string $pre @D
where
  Field[N]

Representing the given fixed-point number in decimal (for testing purposes).

Function fixed_verifier

pub fn fixed_verifier [ N : Nat, $S ] ( x : Fixed[N, $S, @public] $pre @public ) -> Fixed[N, $S, @verifier] $pre @public
where
  Field[N]

Conversion of the given fixed-point number from the domain @public to the domain @verifier.

Function ge_fixed

pub fn ge_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first given fixed-point number is greater than or equal to the second one. Assumes that they are correctly formed. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers.

Function gt_fixed

pub fn gt_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first given fixed-point number is less than the second one. Assumes that they are correctly formed. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers.

Function increase_len_fixed

pub fn increase_len_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, new_len : uint[18446744073709551616] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

Increases the number of bits of a fixed-point number, without changing its value. Fails if the new len is less than the old len. Does not check that the new len fits in the modulus.

Function le_fixed

pub fn le_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first given fixed-point number is less than or equal to the second one. Assumes that they are correctly formed. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers.

Function lt_fixed

pub fn lt_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first given fixed-point number is less than the second one. Assumes that they are correctly formed. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers.

Function lt_signed

pub fn lt_signed [ $S, @D, N : Nat ] ( x : uint[N] $S @D, y : uint[N] $S @D, bw : uint[18446744073709551616] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Signed comparison of two integers in uint[N], i.e. x and y are interpreted as bw-bit signed integers in the range -2^(bw-1) .. 2^(bw-1)-1. Tests if x is less than y.

Function max_fixed

pub fn max_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

Find the maximum of two fixed-point numbers. Assumes that they are correctly formed. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers.

Function min_fixed

pub fn min_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

Find the minimum of two fixed-point numbers. Assumes that they are correctly formed. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers.

Function mult_fixed

pub fn mult_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

The product of the given two fixed-point numbers. Assumes that they are correctly formed. The result is rounded to the same number of bits after the binary point as the arguments. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers or the product does not fit to this number of bits.

Function mult_fixed_alternative

pub fn mult_fixed_alternative [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

An alternative implementation of mult_fixed, using mult_fixed_exact, followed by round_down_fixed. Should have same semantics and similar performance.

Function mult_fixed_exact

pub fn mult_fixed_exact [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

The product of the given two fixed-point numbers. Does not round the result, instead the len and pplen of the result are the sum of the len and pplen of the arguments, respectively. This is much faster than mult_fixed. If the modulus is not large enough to fit numbers with new len bits then it fails. If the inputs are correctly formed (fit in the required number of bits) then the result is as well.

Function negate_fixed

pub fn negate_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

Negation of the given fixed-point number. If the given number is the smallest one representable within the number of bits and the number of bits after the binary point, then overflow will occur which is not checked. Use check_fixed to check it manually when necessary.

Function neq_fixed

pub fn neq_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the given two fixed-point numbers are distinct. Assumes that they are correctly formed. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers.

Function round_down_fixed

pub fn round_down_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, new_len : uint[18446744073709551616] $pre @public, new_pplen : uint[18446744073709551616] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

Reduces pplen by rounding towards minus infinity. The arguments specify both a new len and a new pplen. Fails if the new pplen is greater than the old one or if the rounded result does not fit in the new len bits or if adding the rounded-down bits back to the new len would overflow the modulus. The input fixed-point number does not have to fit in its len bits.

Function round_down_fixed_to_int

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

Rounds a fixed-point number down to the nearest integer less than or equal to it, i.e. it takes the floor of the fixed-point number. Fails if the input does not fit into its len bits.

Function round_fixed_to_nearest_int

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

Rounds a fixed-point number to the nearest integer, either up or down whichever is closer. n + 0.5, for an integer n, is rounded to n + 1, even for negative n. Fails if the output does not fit into its len bits, which can also occur for correctly formed inputs that are so close to the maximum allowed value that rounding up to an integer overflows the required number of bits. If the input is slightly below the minimum allowed value but after rounding up fits in the required number of bits then it does not fail.

Function round_up_fixed_to_int

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

Rounds a fixed-point number up to the nearest integer greater than or equal to it, i.e. it takes the ceiling of the fixed-point number. Fails if the output does not fit into its len bits, which can also occur for correctly formed inputs that are so close to the maximum allowed value that rounding up to an integer overflows the required number of bits. If the input is slightly below the minimum allowed value but after rounding up fits in the required number of bits then it does not fail.

Function signed_uintN_to_uint

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

Convert a uint[N] integer in $pre into a uint, interpreting the uint[N] as a value in the range -N/2 .. N-N/2-1 instead of 0 .. N-1. E.g. N-1 is converted to -1, etc.

Function sqrt_fixed

unchecked eff [,,*] -> [,,*] ! <$S>
pub fn sqrt_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

Square root of the given fixed-point number. Assumes that the number is correctly formed. Fails if the given fixed-point number is negative.

Function sqrt_fixed_pre

pub fn sqrt_fixed_pre [ N : Nat, @D ] ( x : Fixed[N, $pre, @D] $pre @public ) -> Fixed[N, $pre, @D] $pre @public
where
  Field[N]

Square root of the given fixed-point number in $pre. Assumes that the number is correctly formed. Fails if the given fixed-point number is negative.

Function sub_fixed

pub fn sub_fixed [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

The difference of the given two fixed-point numbers. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers. Does not check that the sum fits to this number of bits. Use check_fixed to check it manually when necessary.

Function uint_to_fixed

pub fn uint_to_fixed [ N : Nat, $S, @D ] ( n : uint[N] $S @D, len : uint[18446744073709551616] $pre @public, pplen : uint[18446744073709551616] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

A new fixed-point number whose value is the integer given as the first argument, with the number of bits and the number of bits after the binary point given as the second and the third arguments. Fails if the integral value (along with zeros after the binary point) does not fit to the required number of bits but does not check that it fits into the modulus (if overflowing the modulus wraps it around to a value that fits in the number of bits then it is not detected).