ZK-SecreC Documentation

2024.09

Module FixedPoint

Function add_fixed

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

The sum of the given two fixed-point numbers in $pre. 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 sum does not fit to this number of bits.

Function add_fixed3

pub fn add_fixed3 [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public, ref sizeasserters : list[SizeAsserter[N, $S, @D] $pre @public] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

The sum of the given two fixed-point numbers. Assumes that they are correctly formed and the given list contains a SizeAsserter object for their number of bits. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers or the sum does not fit to this number of bits.

Function div_fixed

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

The ratio of the given two fixed-point numbers in $pre. 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 div_fixed3

pub fn div_fixed3 [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public, ref sizeasserters : list[SizeAsserter[N, $S, @D] $pre @public] $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 and the given list contains a SizeAsserter object for their number of bits. 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, @D ] ( coef : uint[N] $pre @D, len : uint[18446744073709551616] $pre @public, pplen : uint[18446744073709551616] $pre @public ) -> Fixed[N, $pre, @D] $pre @public
where
  Field[N]

A new fixed-point number in $pre with 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 fixed3

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

A new fixed-point number with given parameters (the integral value that ignores binary point; the number of bits; the number of bits following the binary point). The fourth argument must be a list of SizeAsserter objects as produced by Inequalities::sizeasserters_new. Fails if the integral value does not fit to the required number of bits or the list of SizeAsserter objects is too short to contain one with required number of bits.

Function fixed_cond

pub fn fixed_cond [ M : Nat, N : Nat, $S, @D ] ( b : bool[M] $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],
  Convertible[M,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_downcast

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

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

Function fixed_nonnegative

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

A new fixed-point number in $pre with 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_nonnegative3

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

A new fixed-point number with given parameters (the integral value that ignores binary point; the number of bits; the number of bits following the binary point). The fourth argument must be a list of SizeAsserter objects as produced by Inequalities::sizeasserters_new. Fails if the new fixed-point number would be negative, or if the integral value does not fit to the required number of bits or the list of SizeAsserter objects is too short to contain one with required number of bits.

Function fixed_pre

pub fn fixed_pre [ N : Nat, $S, @D ] ( x : 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

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 ] ( x : Fixed[N, $S, @D] $pre @public ) -> string $pre @D
where
  Field[N]

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

Function ge_fixed

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

Test if the first given fixed-point number in $pre 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 ge_fixed3

pub fn ge_fixed3 [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public, ref sizeasserters : list[SizeAsserter[N, $S, @D] $pre @public] $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 and the given list contains a SizeAsserter object for their number of bits. 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, @D ] ( x : Fixed[N, $pre, @D] $pre @public, y : Fixed[N, $pre, @D] $pre @public ) -> bool[N] $pre @D
where
  Field[N]

Test if the first given fixed-point number in $pre is greater 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 gt_fixed3

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

Test if the first given fixed-point number is greater than the second one. Assumes that they are correctly formed and the given list contains a SizeAsserter object for their number of bits. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers.

Function le_fixed

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

Test if the first given fixed-point number in $pre 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 le_fixed3

pub fn le_fixed3 [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public, ref sizeasserters : list[SizeAsserter[N, $S, @D] $pre @public] $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 and the given list contains a SizeAsserter object for their number of bits. 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, @D ] ( x : Fixed[N, $pre, @D] $pre @public, y : Fixed[N, $pre, @D] $pre @public ) -> bool[N] $pre @D
where
  Field[N]

Test if the first given fixed-point number in $pre 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_fixed3

pub fn lt_fixed3 [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public, ref sizeasserters : list[SizeAsserter[N, $S, @D] $pre @public] $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 and the given list contains a SizeAsserter object for their number of bits. 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, @D ] ( x : Fixed[N, $pre, @D] $pre @public, y : Fixed[N, $pre, @D] $pre @public ) -> Fixed[N, $pre, @D] $pre @public
where
  Field[N]

The product of the given two fixed-point numbers in $pre. 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 product does not fit to this number of bits.

Function mult_fixed3

pub fn mult_fixed3 [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public, ref sizeasserters : list[SizeAsserter[N, $S, @D] $pre @public] $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 and the given list contains a SizeAsserter object for their number of bits. 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 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. Fails if the given number is the smallest one representable within the number of bits and the number of bits after the binary point (the negation of this number would overflow these parameters).

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 sqrt_fixed

pub fn sqrt_fixed [ 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 sqrt_fixed3

pub fn sqrt_fixed3 [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, ref sizeasserters : list[SizeAsserter[N, $S, @D] $pre @public] $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 sub_fixed

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

The difference of the given two fixed-point numbers in $pre. 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 difference does not fit to this number of bits.

Function sub_fixed3

pub fn sub_fixed3 [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, y : Fixed[N, $S, @D] $pre @public, ref sizeasserters : list[SizeAsserter[N, $S, @D] $pre @public] $pre @public ) -> Fixed[N, $S, @D] $pre @public
where
  Field[N]

The difference of the given two fixed-point numbers. Assumes that they are correctly formed and the given list contains a SizeAsserter object for their number of bits. Fails if the numbers of bits or the numbers of bits after the binary point differ in the given fixed-point numbers or the difference does not fit to this number of bits.

Function uint_to_fixed

pub fn uint_to_fixed [ N : Nat, @D ] ( n : uint[N] $pre @D, len : uint[18446744073709551616] $pre @public, pplen : uint[18446744073709551616] $pre @public ) -> Fixed[N, $pre, @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.

Function uint_to_fixed3

pub fn uint_to_fixed3 [ N : Nat, $S, @D ] ( n : uint[N] $S @D, len : uint[18446744073709551616] $pre @public, pplen : uint[18446744073709551616] $pre @public, ref sizeasserters : list[SizeAsserter[N, $S, @D] $pre @public] $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. The fourth argument must be a list of SizeAsserter objects as produced by Inequalities::sizeasserters_new. Fails if the integral value (along with zeros after the binary point) does not fit to the required number of bits or the list of SizeAsserter objects is too short to contain one with required number of bits.