miden-core-lib 0.25.3

Miden VM core library
Documentation
1
2
3
4
5
6
7
8
9
10

## miden::core::collections::sorted_array
| Procedure | Description |
| ----------- | ------------- |
| find_word | Finds a value in a sorted array of words.<br /><br />**Proof-side contract:** the input array must already be sorted in non-decreasing<br />lexicographic order before this procedure is called.<br /><br />This procedure does not prove that the full memory range is sorted. It uses host-provided<br />lower-bound advice and verifies only that the returned lower-bound witness is locally consistent<br />with the returned pointer. If malicious advice is used on an unsorted range, the local witness can<br />be consistent while the global lookup result is false.<br /><br />Caller code must prove sortedness before relying on this result, unless the range was already<br />authenticated by another proof-side invariant that implies sortedness. Use `assert_sorted_words`<br />when caller code needs to establish this precondition directly.<br /><br />Input:  [VALUE, start_ptr, end_ptr]<br />Output: [is_value_found, value_ptr, start_ptr, end_ptr]<br /><br /># Panics<br /><br />Panics if:<br />- start_ptr, end_ptr are not word-aligned<br />- `start_ptr > end_ptr`<br /><br />Cycles:<br />Value exists: 46 cycles<br />Value doesn't exist and the array is empty: 25 cycles<br />Value doesn't exist and is smaller than all elements: 151 cycles<br />Value doesn't exist and is larger than all elements: 149 cycles<br />Value doesn't exist: 286 cycles<br /> |
| assert_sorted_words | Asserts that an array of words is sorted in non-decreasing lexicographic order.<br /><br />This is a full linear proof-side check over the memory range. It does not use advice. Call this<br />before `find_word` when sortedness is not already implied by another proof-side invariant.<br /><br />Input:  [start_ptr, end_ptr, ...]<br />Output: [start_ptr, end_ptr, ...]<br /><br />Panics if:<br />- start_ptr or end_ptr is not a u32 value.<br />- start_ptr, end_ptr are not word-aligned<br />- `start_ptr > end_ptr`<br />- any adjacent word pair is out of order.<br /> |
| find_key_value | Finds a key in a sorted array of (key, value) word tuples.<br /><br />**Proof-side contract:** the keys in the array must already be sorted in non-decreasing<br />lexicographic order before this procedure is called.<br /><br />This procedure does not prove that the full memory range is sorted. It uses host-provided<br />lower-bound advice and verifies only that the returned lower-bound witness is locally consistent<br />with the returned pointer. If malicious advice is used on an unsorted range, the local witness can<br />be consistent while the global lookup result is false.<br /><br />Caller code must prove key sortedness before relying on this result, unless the range was already<br />authenticated by another proof-side invariant that implies sortedness. Use `assert_sorted_keys`<br />when caller code needs to establish this precondition directly.<br /><br />Inputs:  [KEY, start_ptr, end_ptr]<br />Outputs: [is_key_found, key_ptr, start_ptr, end_ptr]<br /><br /># Panics<br /><br />Panics if:<br />- start_ptr is not word-aligned<br />- end_ptr is not double-word-aligned with the start_ptr:<br />- `(end_ptr - start_ptr)` must be divisible by 8<br />- `start_ptr > end_ptr`<br /> |
| find_half_key_value | Finds a half-key in a sorted array of (key, value) word tuples.<br /><br />Half-key means that, out of the keys in the array, only half of the key - the most significant<br />element (prefix) and the second most significant element (suffix) - need to match.<br /><br />**Proof-side contract:** the half-keys in the array must already be sorted in non-decreasing<br />lexicographic order before this procedure is called.<br /><br />This procedure does not prove that the full memory range is sorted. It uses host-provided<br />lower-bound advice and verifies only that the returned lower-bound witness is locally consistent<br />with the returned pointer. If malicious advice is used on an unsorted range, the local witness can<br />be consistent while the global lookup result is false.<br /><br />Caller code must prove half-key sortedness before relying on this result, unless the range was<br />already authenticated by another proof-side invariant that implies sortedness. Use<br />`assert_sorted_half_keys` when caller code needs to establish this precondition directly.<br /><br />Inputs: [key_suffix, key_prefix, start_ptr, end_ptr]<br />Output: [is_key_found, key_ptr, start_ptr, end_ptr]<br /><br /># Panics<br /><br />Panics if:<br />- start_ptr is not word-aligned<br />- end_ptr is not double-word-aligned with the start_ptr:<br />- `(end_ptr - start_ptr)` must be divisible by 8<br />- `start_ptr > end_ptr`<br /> |
| assert_sorted_keys | Asserts that keys in an array of (key, value) word tuples are sorted in non-decreasing<br />lexicographic order.<br /><br />This is a full linear proof-side check over the memory range. It does not use advice. Call this<br />before `find_key_value` when key sortedness is not already implied by another proof-side invariant.<br /><br />Input:  [start_ptr, end_ptr, ...]<br />Output: [start_ptr, end_ptr, ...]<br /><br />Panics if:<br />- start_ptr or end_ptr is not a u32 value.<br />- start_ptr is not word-aligned<br />- end_ptr is not double-word-aligned with start_ptr<br />- `start_ptr > end_ptr`<br />- any adjacent key pair is out of order.<br /> |
| assert_sorted_half_keys | Asserts that half-keys in an array of (key, value) word tuples are sorted in non-decreasing<br />lexicographic order.<br /><br />A half-key comparison ignores the two least significant key elements, matching<br />`find_half_key_value`.<br /><br />This is a full linear proof-side check over the memory range. It does not use advice. Call this<br />before `find_half_key_value` when half-key sortedness is not already implied by another proof-side<br />invariant.<br /><br />Input:  [start_ptr, end_ptr, ...]<br />Output: [start_ptr, end_ptr, ...]<br /><br />Panics if:<br />- start_ptr or end_ptr is not a u32 value.<br />- start_ptr is not word-aligned<br />- end_ptr is not double-word-aligned with start_ptr<br />- `start_ptr > end_ptr`<br />- any adjacent half-key pair is out of order.<br /> |