ZK-SecreC Documentation

2024.09

Module Inequalities

Function assert_ge

pub fn assert_ge [ N : Nat ] ( x : uint[N] $post @prover, y : uint[N] $post @prover, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first of the given two Prover’s values on wires is greater than or equal to the second one. Fails also if the numbers do not fit the number of bits given by the SizeAsserter object.

Function assert_ge’

pub fn assert_ge’ [ N : Nat ] ( xc : Checked[N, $post, @prover] $pre @public, yc : Checked[N, $post, @prover] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first of the given two checked Prover’s values on wires is greater than or equal to the second one. Assumes that the numbers have been checked to fit the number of bits given by the SizeAsserter object.

Function assert_gt

pub fn assert_gt [ N : Nat ] ( x : uint[N] $post @prover, y : uint[N] $post @prover, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first of the given two Prover’s values on wires is greater than the second one. Fails also if the numbers do not fit the number of bits given by the SizeAsserter object.

Function assert_gt’

pub fn assert_gt’ [ N : Nat ] ( xc : Checked[N, $post, @prover] $pre @public, yc : Checked[N, $post, @prover] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first of the given two checked Prover’s values on wires is greater than the second one. Assumes that the numbers have been checked to fit the number of bits given by the SizeAsserter object.

Function assert_le

pub fn assert_le [ N : Nat ] ( x : uint[N] $post @prover, y : uint[N] $post @prover, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first of the given two Prover’s values on wires is less than or equal to the second one. Fails also if the numbers do not fit the number of bits given by the SizeAsserter object.

Function assert_le’

pub fn assert_le’ [ N : Nat ] ( xc : Checked[N, $post, @prover] $pre @public, yc : Checked[N, $post, @prover] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first of the given two checked Prover’s values on wires is less than or equal to the second one. Assumes that the numbers have been checked to fit the number of bits given by the SizeAsserter object.

Function assert_lt

pub fn assert_lt [ N : Nat ] ( x : uint[N] $post @prover, y : uint[N] $post @prover, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first of the given two Prover’s values on wires is less than the second one. Fails also if the numbers do not fit the number of bits given by the SizeAsserter object.

Function assert_lt’

pub fn assert_lt’ [ N : Nat ] ( xc : Checked[N, $post, @prover] $pre @public, yc : Checked[N, $post, @prover] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the first of the given two checked Prover’s values on wires is less than the second one. Assumes that the numbers have been checked to fit the number of bits given by the SizeAsserter object.

Function assert_sorted

pub fn assert_sorted [ N : Nat ] ( xs : list[uint[N] $post @prover] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the list of Prover’s values on wires is non-decreasing. Fails also if not all the values fit into the number of bits given by the SizeAsserter object.

Function check_size

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

Assertion that the given integer fits into the number of bits given by the SizeAsserter object. Returns a Checked object for the given integer.

Function checked_prover

pub fn checked_prover [ N : Nat, $S, @D ] ( x : Checked[N, $S, @D] $pre @public ) -> Checked[N, $S, @prover] $pre @public

Conversion of the given Checked object to the Prover’s domain.

Function ge

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

Test if the first of the given two values in $pre is greater than or equal to the second one.

Function ge3

pub fn ge3 [ N : Nat, $S, @D ] ( x : uint[N] $S @D, y : uint[N] $S @D, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first of the given two values is greater than or equal to the second one. Triggers assertion failure if the numbers are in $post @prover and do not fit the number of bits given by the SizeAsserter object.

Function ge3’

pub fn ge3’ [ N : Nat ] ( xc : Checked[N, $post, @prover] $pre @public, yc : Checked[N, $post, @prover] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> bool[N] $post @prover
where
  Field[N]

Test if the first of the given two checked Prover’s values on wires is greater than or equal to the second one. Assumes that the numbers have been checked to fit the number of bits given by the SizeAsserter object.

Function gt

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

Test if the first of the given two values in $pre is greater than the second one.

Function gt3

pub fn gt3 [ N : Nat, $S, @D ] ( x : uint[N] $S @D, y : uint[N] $S @D, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first of the given two values is greater than the second one. Triggers assertion failure if the numbers are in $post @prover and do not fit the number of bits given by the SizeAsserter object.

Function gt3’

pub fn gt3’ [ N : Nat ] ( xc : Checked[N, $post, @prover] $pre @public, yc : Checked[N, $post, @prover] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> bool[N] $post @prover
where
  Field[N]

Test if the first of the given two checked Prover’s values on wires is greater than the second one. Assumes that the numbers have been checked to fit the number of bits given by the SizeAsserter object.

Function is_sorted

pub fn is_sorted [ N : Nat, @D ] ( xs : list[uint[N] $pre @D] $pre @public ) -> bool[N] $pre @D
where
  Field[N]

Test if the list of values in $pre is non-decreasing.

Function is_sorted3

pub fn is_sorted3 [ N : Nat, $S, @D ] ( xs : list[uint[N] $S @D] $pre @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the list of values is non-decreasing. Triggers assertion failure if the numbers are in $post @prover and not all of them fit into the number of bits given by the SizeAsserter object.

Function le

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

Test if the first of the given two values in $pre is less than or equal to the second one.

Function le3

pub fn le3 [ N : Nat, $S, @D ] ( x : uint[N] $S @D, y : uint[N] $S @D, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first of the given two values is less than or equal to the second one. Triggers assertion failure if the numbers are in $post @prover and do not fit the number of bits given by the SizeAsserter object.

Function le3’

pub fn le3’ [ N : Nat ] ( xc : Checked[N, $post, @prover] $pre @public, yc : Checked[N, $post, @prover] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> bool[N] $post @prover
where
  Field[N]

Test if the first of the given two checked Prover’s values on wires is less than or equal to the second one. Assumes that the numbers have been checked to fit the number of bits given by the SizeAsserter object.

Function lt

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

Test if the first of the given two values in $pre is less than the second one.

Function lt3

pub fn lt3 [ N : Nat, $S, @D ] ( x : uint[N] $S @D, y : uint[N] $S @D, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> bool[N] $S @D
where
  Field[N]

Test if the first of the given two values is less than the second one. Triggers assertion failure if the numbers are in $post @prover and do not fit the number of bits given by the SizeAsserter object.

Function lt3’

pub fn lt3’ [ N : Nat ] ( xc : Checked[N, $post, @prover] $pre @public, yc : Checked[N, $post, @prover] $pre @public, ref sizeasserter : SizeAsserter[N, $post, @prover] $pre @public ) -> bool[N] $post @prover
where
  Field[N]

Test if the first of the given two checked Prover’s values on wires is less than the second one. Assumes that the numbers have been checked to fit the number of bits given by the SizeAsserter object.

Function max

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

Maximum of the given two values in $pre.

Function max3

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

Maximum of the given two values. Triggers an assertion failure if the numbers are in $post @prover and not both of them fit into the number of bits given by the SizeAsserter object.

Function min

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

Minimum of the given two values in $pre.

Function min3

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

Minimum of the given two values. Triggers an assertion failure if the numbers are in $post @prover and not both of them fit into the number of bits given by the SizeAsserter object.

Function sizeasserter_new

pub fn sizeasserter_new [ N : Nat, $S, @D ] ( bw : uint[18446744073709551616] $pre @public ) -> SizeAsserter[N, $S, @D] $pre @public

A new SizeAsserter object for the given number of bits. The number of bits must be less than binary logarithm of half of the modulus.

Function sizeasserters_new

pub fn sizeasserters_new [ N : Nat, $S, @D ] ( bwlim : uint[18446744073709551616] $pre @public ) -> list[SizeAsserter[N, $S, @D] $pre @public] $pre @public

A list of new SizeAsserter objects, one for every number of bits less than the given limit. The limit must be less than binary logarithm of the modulus.