ZK-SecreC Documentation

2024.09

Module Ratio

Function add_ratio

pub fn add_ratio [ N : Nat, @D ] ( xr : Ratio[N, $pre, @D] $pre @public, yr : Ratio[N, $pre, @D] $pre @public ) -> Ratio[N, $pre, @D] $pre @public
where
  Field[N]

The sum of the given two rational numbers in $pre. Fails if the numerator and the denominator of the result do not fit to the limit of the first summand.

Function add_ratio3

pub fn add_ratio3 [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public, yr : Ratio[N, $S, @D] $pre @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> Ratio[N, $S, @D] $pre @public
where
  Field[N]

The sum of the given two rational numbers. Fails if the numerator and the denominator of the result do not fit to the limit of the first summand. The given SizeAsserter object is used for checking this.

Function eq_ratio

pub fn eq_ratio [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public, yr : Ratio[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the given two rational numbers have the same value.

Function fixed_from_ratio

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

The closest lower approximation of the given rational number in $pre in the form of a fixed-point number, provided that the number of bits and the number of bits after the binary point are given as the second and the third parameter. Fails if the integral value does not fit to the required number of bits.

Function fixed_from_ratio3

pub fn fixed_from_ratio3 [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public, 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]

The closest lower approximation of the given rational number in the form of a fixed-point number, provided that the number of bits and the number of bits after the binary point are given as the second and the third parameter. 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_to_ratio

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

Conversion of the given fixed-point number in $pre to a rational number. Fails if the integral value of the fixed-point number does not fit to the limit given as the second argument.

Function fixed_to_ratio3

pub fn fixed_to_ratio3 [ N : Nat, $S, @D ] ( x : Fixed[N, $S, @D] $pre @public, lim : uint[N] $S @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> Ratio[N, $S, @D] $pre @public
where
  Field[N]

Conversion of the given fixed-point number to a rational number. Fails if the integral value of the fixed-point number does not fit to the limit given as the second argument. The given SizeAsserter object is used for checking this condition.

Function ge_ratio

pub fn ge_ratio [ N : Nat, @D ] ( xr : Ratio[N, $pre, @D] $pre @public, yr : Ratio[N, $pre, @D] $pre @public ) -> bool[N] $pre @D
where
  Field[N]

Test if the first given rational number in $pre is greater than or equal to the second one. Fails if the limits of the given two numbers differ.

Function ge_ratio3

pub fn ge_ratio3 [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public, yr : Ratio[N, $S, @D] $pre @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first given rational number is greater than or equal to the second one. Fails if the limits of the given two numbers differ. The given SizeAsserter object is used for comparison.

Function gt_ratio

pub fn gt_ratio [ N : Nat, @D ] ( xr : Ratio[N, $pre, @D] $pre @public, yr : Ratio[N, $pre, @D] $pre @public ) -> bool[N] $pre @D
where
  Field[N]

Test if the first given rational number in $pre is greater than the second one. Fails if the limits of the given two numbers differ.

Function gt_ratio3

pub fn gt_ratio3 [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public, yr : Ratio[N, $S, @D] $pre @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first given rational number is greater than the second one. Fails if the limits of the given two numbers differ. The given SizeAsserter object is used for comparison.

Function le_ratio

pub fn le_ratio [ N : Nat, @D ] ( xr : Ratio[N, $pre, @D] $pre @public, yr : Ratio[N, $pre, @D] $pre @public ) -> bool[N] $pre @D
where
  Field[N]

Test if the first given rational number in $pre is less than or equal to the second one. Fails if the limits of the given two numbers differ.

Function le_ratio3

pub fn le_ratio3 [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public, yr : Ratio[N, $S, @D] $pre @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first given rational number is less than or equal to the second one. Fails if the limits of the given two numbers differ. The given SizeAsserter object is used for comparison.

Function limit

pub fn limit [ N : Nat, $S ] () -> uint[N] $S @public
where
  Field[N]

A field element suitable for using as the value of lim in Ratio objects.

Function lt_ratio

pub fn lt_ratio [ N : Nat, @D ] ( xr : Ratio[N, $pre, @D] $pre @public, yr : Ratio[N, $pre, @D] $pre @public ) -> bool[N] $pre @D
where
  Field[N]

Test if the first given rational number in $pre is less than the second one. Fails if the limits of the given two numbers differ.

Function lt_ratio3

pub fn lt_ratio3 [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public, yr : Ratio[N, $S, @D] $pre @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first given rational number is less than the second one. Fails if the limits of the given two numbers differ. The given SizeAsserter object is used for comparison.

Function mult_ratio

pub fn mult_ratio [ N : Nat, @D ] ( xr : Ratio[N, $pre, @D] $pre @public, yr : Ratio[N, $pre, @D] $pre @public ) -> Ratio[N, $pre, @D] $pre @public
where
  Field[N]

The product of the given two rational numbers in $pre. Fails if the numerator and the denominator of the result do not fit to the limit of the first factor.

Function mult_ratio3

pub fn mult_ratio3 [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public, yr : Ratio[N, $S, @D] $pre @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> Ratio[N, $S, @D] $pre @public
where
  Field[N]

The product of the given two rational numbers. Fails if the numerator and the denominator of the result do not fit to the limit of the first factor. The given SizeAsserter object is used for checking this.

Function negate_ratio

pub fn negate_ratio [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public ) -> Ratio[N, $S, @D] $pre @public
where
  Field[N]

The additive inverse of the given rational number. Fails if the given rational number is the smallest one with its denominator fitting to the limit (then the additive inverse does not fit to the limit).

Function neq_ratio

pub fn neq_ratio [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public, yr : Ratio[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the given two rational numbers have distinct values.

Function ratio

pub fn ratio [ N : Nat, @D ] ( n : uint[N] $pre @D, m : uint[N] $pre @public, lim : uint[N] $pre @public ) -> Ratio[N, $pre, @D] $pre @public
where
  Field[N]

The rational number with the given numerator, denominator and limit in $pre. Fails if the numerator and denominator do not fit to the limit.

Function ratio3

pub fn ratio3 [ N : Nat, $S, @D ] ( n : uint[N] $S @D, m : uint[N] $pre @public, lim : uint[N] $S @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> Ratio[N, $S, @D] $pre @public
where
  Field[N]

The rational number with the given numerator, denominator and limit. Fails if the numerator and denominator do not fit to the limit. The given SizeAsserter object is used for checking this condition.

Function ratio_to_pre

pub fn ratio_to_pre [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public ) -> Ratio[N, $pre, @D] $pre @public

Conversion of the given rational number to the stage $pre.

Function ratio_to_string

pub fn ratio_to_string [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public ) -> string $pre @D

The string representation of the given rational number.

Function sub_ratio

pub fn sub_ratio [ N : Nat, @D ] ( xr : Ratio[N, $pre, @D] $pre @public, yr : Ratio[N, $pre, @D] $pre @public ) -> Ratio[N, $pre, @D] $pre @public
where
  Field[N]

The difference of the given two rational numbers in $pre. Fails if either the second addend is the smallest one with its denominator fitting to the limit or the numerator and the denominator of the result do not fit to the limit of the first summand.

Function sub_ratio3

pub fn sub_ratio3 [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public, yr : Ratio[N, $S, @D] $pre @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> Ratio[N, $S, @D] $pre @public
where
  Field[N]

The difference of the given two rational numbers. Fails if either the second addend is the smallest one with its denominator fitting to the limit or the numerator and the denominator of the result do not fit to the limit of the first summand. The given SizeAsserter object is used for checking the latter condition.

Function uint_to_ratio

pub fn uint_to_ratio [ N : Nat, @D ] ( n : uint[N] $pre @D, lim : uint[N] $pre @public ) -> Ratio[N, $pre, @D] $pre @public
where
  Field[N]

The rational number whose value equals the given integer in $pre, with the given limit in $pre. Fails if the value does not fit to the limit.

Function uint_to_ratio3

pub fn uint_to_ratio3 [ N : Nat, $S, @D ] ( n : uint[N] $S @D, lim : uint[N] $S @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> Ratio[N, $S, @D] $pre @public
where
  Field[N]

The rational number whose value equals the given integer, with the given limit. Fails if the value does not fit to the limit. The given SizeAsserter object is used for checking this.

Function with_denominator

pub fn with_denominator [ N : Nat, @D ] ( xr : Ratio[N, $pre, @D] $pre @public, n : uint[N] $pre @public ) -> Ratio[N, $pre, @D] $pre @public
where
  Field[N]

The closest lower approximation of the given rational number in $pre that has the given denominator. Fails if the numerator and the denominator of the result do not fit to the limit of the given rational number.

Function with_denominator3

pub fn with_denominator3 [ N : Nat, $S, @D ] ( xr : Ratio[N, $S, @D] $pre @public, n : uint[N] $pre @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> Ratio[N, $S, @D] $pre @public
where
  Field[N]

The closest lower approximation of the given rational number that has the given denominator. Fails if the numerator and the denominator of the result do not fit to the limit of the given rational number. The given SizeAsserter object is used for checking this.