ZK-SecreC Documentation

2024.09

Module String

Function eval_string

pub fn eval_string [ $S, @D, N : Nat ] ( xs : String[$S, @D, N] $pre @public, r : uint[N] $S @D ) -> uint[N] $S @D
where
  Field[N]

The value of the given String object if interpreted as a big-endian representation on base given as the second argument. Only the characters within the declared length are taken into account.

Function string_assert_eq

pub fn string_assert_eq [ @D, N : Nat ] ( x : String[$post, @D, N] $pre @public, y : String[$post, @D, N] $pre @public, maxLen : uint[18446744073709551616] $pre @public ) -> () $pre @public
where
  Field[N]

Assertion that the String objects in $post given as the first two arguments have a common declared length and are equal within this length. The third argument is a public value that is assumed to be an upper bound of the common length and a lower bound of the actual lengths of the internal lists of characters.

Function string_eq

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

Test if the String objects given as the first two arguments have a common declared length and are equal within this length. The third argument is a public value that is assumed to be an upper bound of the common length and a lower bound of the actual lengths of the internal lists of characters if the String is in $post.

Function string_eq_up_to_len

pub fn string_eq_up_to_len [ N : Nat ] ( x : String[$post, @prover, N] $pre @public, y : String[$post, @prover, N] $pre @public, len : uint[N] $post @prover ) -> bool[N] $post @prover
where
  Field[N]

Test if the String objects in $post @prover given as the first two arguments are equal up to the number of characters given as the $post @prover value in the third argument. Assumes that the actual length of the internal list of characters of the first String object does not exceed that of the second String object.

Function string_substring

unchecked eff [[*],*] -> * -> * -> * -> [[*],*] ! <@public>
pub fn string_substring [ @D, N : Nat ] ( str : String[$pre, @D, N] $pre @public, start : uint[N] $pre @D, len : uint[N] $pre @D, maxLen : uint[18446744073709551616] $pre @public ) -> String[$pre, @D, N] $pre @public
where
  Field[N],
  Vectorization,
  PConTestChallenge[N]

The String object that consists of characters in the String object in $pre given as the first argument, starting from the position given as the second argument and having declared length given in the third argument. The fourth argument is a public upper bound of the lengths in use. Fails if the required substring extends over the declared length of the given string.

Function string_substring3

unchecked eff [[*],*] -> * -> * -> * -> [,,[*]] -> [[*],*] ! <@public>
pub fn string_substring3 [ $S, @D, N : Nat ] ( str : String[$S, @D, N] $pre @public, start : uint[N] $S @D, len : uint[N] $S @D, maxLen : uint[18446744073709551616] $pre @public, ref sizeasserter : SizeAsserter[N, $S, @D] $pre @public ) -> String[$S, @D, N] $pre @public
where
  Field[N],
  Vectorization,
  PConTestChallenge[N]

The String object that consists of characters in the String object given as the first argument, starting from the position given as the second argument and having declared length given in the third argument. The fourth argument is a public upper bound of the lengths in use and the fifth argument is a Sizeasserter object with a number of bits to fit all lengths if the String is in $post @prover. Fails if the required substring extends over the declared length of the given string.

Function string_to_post

pub fn string_to_post [ @D, N : Nat ] ( str : String[$pre, @D, N] $pre @public ) -> String[$post, @D, N] $pre @public
where
  Field[N]

Conversion of a String object in $pre to a String object in $post.

Function string_to_pre

pub fn string_to_pre [ $S, @D, N : Nat ] ( str : String[$S, @D, N] $pre @public ) -> String[$pre, @D, N] $pre @public

Conversion of any String object to a String object in $pre.

Function string_to_prover

pub fn string_to_prover [ $S, @D, N : Nat ] ( str : String[$S, @D, N] $pre @public ) -> String[$S, @prover, N] $pre @public

Conversion of any String object to a String object in the domain @prover.

Function string_to_uint

pub fn string_to_uint [ N : Nat, $S, @D ] ( s : String[$S, @D, N] $pre @public, l : uint[18446744073709551616] $pre @public ) -> uint[N] $S @D
where
  Field[N]

The value of the given String object if interpreted as a big-endian representation on base 256. The characters beyond the declared length are interpreted as zeros. The second argument is assumed to be a public upper bound of the declared length and a lower bound of the actual length of the internal character list.

Function string_with_native_len

unchecked eff [*] -> [[*],*] ! <$S>
pub fn string_with_native_len [ N : Nat, $S, @D ] ( bytes : list[uint[N] $S @D] $pre @public ) -> String[$S, @D, N] $pre @public
where
  Field[N]

The String object that consists of all characters in the given list, with the declared length being the actual length of the given list.

Function uint_to_string

pub fn uint_to_string [ N : Nat, $S, @D ] ( x : uint[N] $S @D, maxlen : uint[18446744073709551616] $pre @public ) -> String[$S, @D, N] $pre @public
where
  Field[N]

A String object whose value, when interpreted as a big-endian representation on base 256, is the number given as the first argument. The second argument becomes the actual length of the internal character list. The declared length excludes precisely the trailing zeros of the character list.