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.
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.
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
.
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.
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.
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.
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
.
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
.
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
.
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.
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.
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.