diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 0819d33bda..c0d8d530fc 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -171,3 +171,20 @@ jobs: tool: cargo-hack - name: Check all feature combinations run: make check-features + + check-user-doc-cycles: + name: check user doc cycle counts + runs-on: warp-ubuntu-latest-x64-8x + steps: + - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1 + with: + persist-credentials: false + - name: Cleanup large tools for build space + uses: ./.github/actions/cleanup-runner + - uses: WarpBuilds/rust-cache@9d0cc3090d9c87de74ea67617b246e978735b1a1 # v2.9.1 + with: + save-if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/next' }} + - name: Install rust + run: rustup update --no-self-update + - name: Check user doc cycle counts + run: make check-user-doc-cycles diff --git a/CHANGELOG.md b/CHANGELOG.md index a83f485742..a4d49ff8f6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -143,6 +143,7 @@ - Added a Blake3 pure execution benchmark axis and reduced processor benchmark compile time by relaxing forced inlining in execution helpers ([#3289](https://github.com/0xMiden/miden-vm/pull/3289)). - Documented that `smt::peek` is a fast, untrusted advice lookup, and that caller code must verify the returned value before relying on it ([#3297](https://github.com/0xMiden/miden-vm/pull/3297)). +- Added `scripts/check-user-doc-cycles.sh` to verify user-facing core library and assembly instruction cycle counts against generated MASM docs and measured `clk` fixtures ([#3111](https://github.com/0xMiden/miden-vm/issues/3111)). - Clarified MAST node equality coverage by using structural `PartialEq` directly in merge tests ([#3298](https://github.com/0xMiden/miden-vm/pull/3298)). - Documented the `sorted_array` lookup sortedness contract and added linear assertion helpers for proving word, key, and half-key ordering ([#3308](https://github.com/0xMiden/miden-vm/pull/3308)). - Tightened LogUp lookup AIR docs and comments, removed unused operation-flag accessors, and added block-hash/op-group selector coverage ([#3309](https://github.com/0xMiden/miden-vm/pull/3309)). diff --git a/Cargo.lock b/Cargo.lock index 32d7a5ac07..8cc639aa47 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2563,6 +2563,7 @@ dependencies = [ "rstest", "thiserror", "tokio", + "toml", "tracing", "tracing-subscriber", ] diff --git a/Makefile b/Makefile index 87617eaa40..a46d2954b3 100644 --- a/Makefile +++ b/Makefile @@ -26,7 +26,8 @@ help: @printf " make test-air test=\"some_test\" # Test specific function\n" @printf " make test-fast # Fast tests (no proptests/CLI)\n" @printf " make test-skip-proptests # All tests except proptests\n" - @printf " make check-features # Check all feature combinations with cargo-hack\n\n" + @printf " make check-features # Check all feature combinations with cargo-hack\n" + @printf " make check-user-doc-cycles # Check user doc cycle counts against core-lib docs\n\n" # -- environment toggles -------------------------------------------------------------------------- @@ -223,6 +224,10 @@ check: ## Checks all targets and features for errors without code generation check-features: ## Checks all feature combinations compile without warnings using cargo-hack @scripts/check-features.sh +.PHONY: check-user-doc-cycles +check-user-doc-cycles: ## Checks user doc cycle counts against generated core-lib docs + @bash scripts/check-user-doc-cycles.sh + # --- building ------------------------------------------------------------------------------------ .PHONY: build diff --git a/crates/assembly/src/instruction/u32_ops.rs b/crates/assembly/src/instruction/u32_ops.rs index 9bb91c82d8..0c76e22bd8 100644 --- a/crates/assembly/src/instruction/u32_ops.rs +++ b/crates/assembly/src/instruction/u32_ops.rs @@ -357,7 +357,7 @@ pub fn u32rotr( /// Translates u32popcnt assembly instructions to VM operations. /// -/// This operation takes 32 cycles. +/// This operation takes 38 VM cycles. pub fn u32popcnt(span_builder: &mut BasicBlockBuilder) { #[rustfmt::skip] let ops = [ diff --git a/docs/src/user_docs/assembly/instruction_reference.md b/docs/src/user_docs/assembly/instruction_reference.md index 854a25b62b..dfef324e35 100644 --- a/docs/src/user_docs/assembly/instruction_reference.md +++ b/docs/src/user_docs/assembly/instruction_reference.md @@ -114,7 +114,7 @@ _Note: Assertions can be parameterized with an error message (e.g., assert.err=" | `u32shr`
`u32shr.b` | `[b, a, ...]` | `[c, ...]` | 20
5 | $c = \lfloor a / 2^b \rfloor$. Undefined if $a \geq 2^{32}$ or $b > 31$. | | `u32rotl`
`u32rotl.b` | `[b, a, ...]` | `[c, ...]` | 18
3 | Rotate left. Undefined if $a \geq 2^{32}$ or $b > 31$. | | `u32rotr`
`u32rotr.b` | `[b, a, ...]` | `[c, ...]` | 22
3 | Rotate right. Undefined if $a \geq 2^{32}$ or $b > 31$. | -| `u32popcnt` | `[a, ...]` | `[b, ...]` | 32 | Population count (Hamming weight). Undefined if $a \geq 2^{32}$. | +| `u32popcnt` | `[a, ...]` | `[b, ...]` | 38 | Population count (Hamming weight). Undefined if $a \geq 2^{32}$. | | `u32clz` | `[a, ...]` | `[b, ...]` | 48 | Count leading zeros. Undefined if $a \geq 2^{32}$. | | `u32ctz` | `[a, ...]` | `[b, ...]` | 34 | Count trailing zeros. Undefined if $a \geq 2^{32}$. | | `u32clo` | `[a, ...]` | `[b, ...]` | 40 | Count leading ones. Undefined if $a \geq 2^{32}$. | diff --git a/docs/src/user_docs/assembly/u32_operations.md b/docs/src/user_docs/assembly/u32_operations.md index fbf77a900e..f4ce884705 100644 --- a/docs/src/user_docs/assembly/u32_operations.md +++ b/docs/src/user_docs/assembly/u32_operations.md @@ -111,7 +111,7 @@ The message is hashed and turned into a field element. If the error code is omit | u32shr
- *(20 cycles)*
u32shr.*b*
- *(5 cycles)* | [b, a, ...] | [c, ...] | $c \leftarrow \lfloor a/2^b \rfloor$
Undefined if $a \ge 2^{32}$ or $b > 31$ | | u32rotl
- *(18 cycles)*
u32rotl.*b*
- *(3 cycles)* | [b, a, ...] | [c, ...] | Computes $c$ by rotating a 32-bit representation of $a$ to the left by $b$ bits.
Undefined if $a \ge 2^{32}$ or $b > 31$ | | u32rotr
- *(22 cycles)*
u32rotr.*b*
- *(3 cycles)* | [b, a, ...] | [c, ...] | Computes $c$ by rotating a 32-bit representation of $a$ to the right by $b$ bits.
Undefined if $a \ge 2^{32}$ or $b > 31$ | -| u32popcnt
- *(32 cycles)* | [a, ...] | [b, ...] | Computes $b$ by counting the number of set bits in $a$ (hamming weight of $a$).
Undefined if $a \ge 2^{32}$ | +| u32popcnt
- *(38 cycles)* | [a, ...] | [b, ...] | Computes $b$ by counting the number of set bits in $a$ (hamming weight of $a$).
Undefined if $a \ge 2^{32}$ | | u32clz
- *(48 cycles)* | [a, ...] | [b, ...] | Computes $b$ as a number of leading zeros of $a$.
Undefined if $a \ge 2^{32}$ | | u32ctz
- *(34 cycles)* | [a, ...] | [b, ...] | Computes $b$ as a number of trailing zeros of $a$.
Undefined if $a \ge 2^{32}$ | | u32clo
- *(40 cycles)* | [a, ...] | [b, ...] | Computes $b$ as a number of leading ones of $a$.
Undefined if $a \ge 2^{32}$ | diff --git a/docs/src/user_docs/core_lib/collections.md b/docs/src/user_docs/core_lib/collections.md index aeec62e80e..89ef67897b 100644 --- a/docs/src/user_docs/core_lib/collections.md +++ b/docs/src/user_docs/core_lib/collections.md @@ -19,9 +19,9 @@ The following procedures are available to read data from and make updates to a M | ---------------------------- | ------------- | | get | Loads the element at the absolute position `pos` in the MMR onto the stack. Valid range for `pos` is between $0$ and $2^{32} - 1$ (both inclusive), and `pos` must refer to an existing leaf: `pos < num_leaves`, where `num_leaves` is stored at `mmr_ptr[0]`. The procedure fails instead of returning an empty or sentinel word when `pos` is outside the current MMR. Inputs: `[pos, mmr_ptr, ...]`. Output: `[EL, ...]`. Where `EL` is the element loaded from the MMR whose memory location starts at `mmr_ptr`. | | add | Adds a new element to the MMR. This will update the MMR peaks in the VM's memory and the advice provider with any merged nodes. Inputs: `[EL, mmr_ptr, ...]`. Outputs: `[...]`. Where `EL` is the element added to the MMR whose memory location starts at `mmr_ptr`.

Cycles: `145 + 39 * peak_merges` | -| pack | Computes a commitment to the given MMR and copies the MMR to the Advice Map using the commitment as a key. Inputs: `[mmr_ptr, ...]`. Outputs: `[HASH, ...]`.

Cycles: `128 + 3 * num_peaks` | -| unpack | Writes the MMR whose peaks hash to `HASH` to the memory location pointed to by `mmr_ptr`. Inputs: `[HASH, mmr_ptr, ...]`. Outputs: `[...]`. Where: `HASH` is the MMR peak hash, the hash is expected to be padded to an even length and to have a minimum size of 16 elements. The advice map must contain a key with `HASH`, and its value is `[num_leaves, 0, 0, 0] \|\| hash_data`, and hash_data is the data used to compute `HASH`. `mmr_ptr` is the memory location where the MMR data will be written, starting with the MMR forest (the total count of its leaves) followed by its peaks. The memory location must be word-aligned.

Cycles: `162 + 9 * extra_peak_pair` | -| num_leaves_to_num_peaks | Given the number of leaves in an MMR, computes the number of peaks (i.e. the number of set bits in `num_leaves`).

Inputs: `[num_leaves, ...]`
Outputs: `[num_peaks, ...]`

Cycles: 67 | +| pack | Computes a commitment to the given MMR and copies the MMR to the Advice Map using the commitment as a key. Inputs: `[mmr_ptr, ...]`. Outputs: `[HASH, ...]`.

Cycles: `198 + 6 * extra_peak_pair cycles` where `extra_peak_pair` is the number of peak pairs in addition to the first 16 peaks, i.e. `round_up((num_of_peaks - 16) / 2)` | +| unpack | Writes the MMR whose preimage hashes to `HASH` to the memory location pointed to by `mmr_ptr`. Inputs: `[HASH, mmr_ptr, ...]`. Outputs: `[...]`. Where: `HASH` is the hash of `[num_leaves, 0, 0, 0] \|\| padded_peaks`. The advice map must contain a key with `HASH`, and its value is `[num_leaves, 0, 0, 0] \|\| padded_peaks`. `mmr_ptr` is the memory location where the MMR data will be written, starting with the MMR forest (the total count of its leaves) followed by its peaks. The memory location must be word-aligned.

Cycles: `215 + 9 * extra_peak_pair cycles` where `extra_peak_pair` is the number of peak pairs in addition to the first 16 peaks, i.e. `round_up((num_of_peaks - 16) / 2)` | +| num_leaves_to_num_peaks | Given the number of leaves in an MMR, computes the number of peaks (i.e. the number of set bits in `num_leaves`).

Inputs: `[num_leaves, ...]`
Outputs: `[num_peaks, ...]`

Cycles: 32 | | num_peaks_to_message_size | Given the number of peaks, computes the size of the hashing message used when computing the MMR commitment (rounded up to the next even length, with a minimum of 16).

Inputs: `[num_peaks, ...]`
Outputs: `[message_size, ...]`

Cycles: 19 | `mmr_ptr` is a pointer to the `mmr` data structure, which is defined as: @@ -49,6 +49,6 @@ The following procedures are available: | Procedure | Description | |--------------------|-------------| -| find_word | Finds a value in a sorted array of words.

**Inputs:** `[VALUE, start_ptr, end_ptr, ...]`
**Outputs:** `[is_value_found, value_ptr, start_ptr, end_ptr, ...]`

Where `VALUE` is the word to search for, `start_ptr` and `end_ptr` define the array bounds (word-aligned), `is_value_found` is 1 if found and 0 otherwise, and `value_ptr` points to the found value or the insertion point.

**Requirements:**
- Words must be sorted in non-decreasing order
- `start_ptr` and `end_ptr` must be word-aligned
- `start_ptr <= end_ptr`

**Cycles:** 25-286 depending on case | +| find_word | Finds a value in a sorted array of words.

**Inputs:** `[VALUE, start_ptr, end_ptr, ...]`
**Outputs:** `[is_value_found, value_ptr, start_ptr, end_ptr, ...]`

Where `VALUE` is the word to search for, `start_ptr` and `end_ptr` define the array bounds (word-aligned), `is_value_found` is 1 if found and 0 otherwise, and `value_ptr` points to the found value or the insertion point.

**Requirements:**
- Words must be sorted in non-decreasing order
- `start_ptr` and `end_ptr` must be word-aligned
- `start_ptr <= end_ptr`

**Cycles:**
Value exists: 46 cycles
Value doesn't exist and the array is empty: 25 cycles
Value doesn't exist and is smaller than all elements: 151 cycles
Value doesn't exist and is larger than all elements: 149 cycles
Value doesn't exist: 286 cycles | | find_key_value | Finds a key in a sorted array of (key, value) word tuples.

**Inputs:** `[KEY, start_ptr, end_ptr, ...]`
**Outputs:** `[is_key_found, key_ptr, start_ptr, end_ptr, ...]`

Where `KEY` is the 4-element key to search for. The array contains pairs of words where each pair is (key, value).

**Requirements:**
- Keys must be sorted in non-decreasing order
- `start_ptr` must be word-aligned
- `(end_ptr - start_ptr)` must be divisible by 8 (double-word aligned)
- `start_ptr <= end_ptr`

**Cycles:** 25-322 depending on case | | find_half_key_value | Finds a half-key in a sorted array of (key, value) word tuples. Only the two most significant elements of the key need to match.

**Inputs:** `[key_suffix, key_prefix, start_ptr, end_ptr, ...]`
**Outputs:** `[is_key_found, key_ptr, start_ptr, end_ptr, ...]`

Where `key_prefix` is the most significant element and `key_suffix` is the second most significant element of the key to match.

Same requirements as `find_key_value`. | diff --git a/docs/src/user_docs/core_lib/crypto/aead.md b/docs/src/user_docs/core_lib/crypto/aead.md index 1aeddc90b8..a4b4427847 100644 --- a/docs/src/user_docs/core_lib/crypto/aead.md +++ b/docs/src/user_docs/core_lib/crypto/aead.md @@ -64,7 +64,7 @@ The padding block is automatically added and encrypted. The tag is stored right - Blocks must be stored contiguously in memory - `src_ptr` and `dst_ptr` **must be different** (in-place encryption not supported) -**Cycles:** ~77 + 2 * n, where n = number of field elements encrypted (includes the final padding block) +**Cycles:** ~77 + 2 * n, where n = number of field elements encrypted (includes the final padding block). For num_blocks data blocks: n = 8 * (num_blocks + 1). ### decrypt @@ -112,4 +112,4 @@ Length: `num_blocks * 8` elements. The padding block is authenticated but **not* - Execution halts with assertion failure if tag verification fails - If execution completes successfully, the plaintext at `dst_ptr` is authenticated -**Cycles:** ~177 + 3.5 * n, where n = number of field elements in the plaintext (excludes padding block) +**Cycles:** ~209 + 5 * n, where n = number of field elements in the plaintext (excludes the padding block). For `num_blocks` data blocks: n = 8 * num_blocks. diff --git a/docs/src/user_docs/core_lib/crypto/hashes.md b/docs/src/user_docs/core_lib/crypto/hashes.md index 06c09ea5f3..8b1c530dd5 100644 --- a/docs/src/user_docs/core_lib/crypto/hashes.md +++ b/docs/src/user_docs/core_lib/crypto/hashes.md @@ -51,11 +51,11 @@ Module `miden::core::crypto::hashes::poseidon2` contains procedures for computin | copy_digest | Copies the digest (R0) to the top of the stack.

It is expected to have the hasher state at the top of the stack at the beginning of the procedure execution.

**Inputs:** `[R0, R1, C, ...]`
**Outputs:** `[DIGEST, R0, R1, C, ...]`

Where:
Cycles: 4 | | absorb_double_words_from_memory | Hashes the memory `start_addr` to `end_addr` given a Poseidon2 state specified by 3 words.

This requires that `end_addr = start_addr + 8n` where n = 0, 1, 2, ..., otherwise the procedure will enter an infinite loop.

**Inputs:** `[R0, R1, C, start_addr, end_addr, ...]`
**Outputs:** `[R0', R1', C', end_addr, end_addr ...]`

Where:
Cycles: 4 + 3 * words, where `words` is the `start_addr - end_addr` | | hash_double_words | Hashes the pairs of words in the memory from `start_addr` to `end_addr`.

This procedure requires that `end_addr = start_addr + 8n` where $n = \{0, 1, 2 ...\}$ (i.e. we must always hash some number of double words), otherwise the procedure will enter an infinite loop.

**Inputs:** `[start_addr, end_addr, ...]`
**Outputs:** `[HASH, ...]`

Where:
Cycles: 37 + 3 * words, where `words` is the `start_addr - end_addr` | -| hash_words | Hashes the memory `start_addr` to `end_addr`, handles odd number of elements.

Requires `start_addr < end_addr`, `end_addr` is not inclusive.

**Inputs:** `[start_addr, end_addr, ...]`
**Outputs:** `[H, ...]`

Cycles: | +| hash_words | Hashes the memory `start_addr` to `end_addr`, handles odd number of elements.

Requires `start_addr ≤ end_addr`, `end_addr` is not inclusive. Requires `start_addr` and `end_addr` to be word-aligned.

**Inputs:** `[start_addr, end_addr, ...]`
**Outputs:** `[H, ...]`

Cycles:where `words` is `(end_addr - start_addr) / 4`. | | prepare_hasher_state | Computes the hasher state required for the `hash_elements_with_state` procedure.

Depending on the provided `pad_inputs_flag`, this procedure instantiates the hasher state using different values for capacity element:
- If `pad_inputs_flag` equals $1$ the capacity element will be assigned to $0$. This will essentially "pad" the hashing values with zeroes to the next multiple of $8$.
- If `pad_inputs_flag` equals $0$ the capacity element will be assigned to the remainder of the division of elements number by $8$ ($num\_elements\%8$).

Inputs: `[ptr, num_elements, pad_inputs_flag]`
Outputs: `[R0, R1, C, ptr, end_pairs_addr, num_elements%8]`

Where R0, R1, C are three words representing the hasher state (R0 on top). | | hash_elements_with_state | Computes hash of `Felt` values starting at the specified memory address using the provided hasher state.

This procedure divides the hashing process into two parts: hashing pairs of words using `absorb_double_words_from_memory` procedure and hashing the remaining values using the `hperm` instruction.

Inputs: `[R0, R1, C, ptr, end_pairs_addr, num_elements%8]`
Outputs: `[HASH]`

Where R0, R1, C are three words representing the hasher state (R0 on top). | -| hash_elements | Computes hash of `Felt` values starting at the specified memory address.

Notice that this procedure does not pad the elements to hash to the next multiple of 8.

This procedure divides the hashing process into two parts: hashing pairs of words using
`absorb_double_words_from_memory` procedure and hashing the remaining values using the `hperm`
instruction.

**Inputs:** `[ptr, num_elements]`
**Outputs:** `[HASH]`

Where:
Cycles:
Panics if: | -| pad_and_hash_elements | Computes hash of `Felt` values starting at the specified memory address.

Notice that this procedure essentially pads the elements to be hashed to the next multiple of 8 by setting the capacity element to 0.

This procedure divides the hashing process into two parts: hashing pairs of words using
`absorb_double_words_from_memory` procedure and hashing the remaining values using the `hperm`
instruction.

**Inputs:** `[ptr, num_elements]`
**Outputs:** `[HASH]`

Where:
Cycles:
Panics if: | +| hash_elements | Computes hash of `Felt` values starting at the specified memory address.

Notice that this procedure does not pad the elements to hash to the next multiple of 8.

This procedure divides the hashing process into two parts: hashing pairs of words using
`absorb_double_words_from_memory` procedure and hashing the remaining values using the `hperm`
instruction.

**Inputs:** `[ptr, num_elements]`
**Outputs:** `[HASH]`

Where:
Cycles:where `words` is the number of quads of input values.
Panics if: | +| pad_and_hash_elements | Computes hash of `Felt` values starting at the specified memory address.

Notice that this procedure essentially pads the elements to be hashed to the next multiple of 8 by setting the capacity element to 0.

This procedure divides the hashing process into two parts: hashing pairs of words using
`absorb_double_words_from_memory` procedure and hashing the remaining values using the `hperm`
instruction.

**Inputs:** `[ptr, num_elements]`
**Outputs:** `[HASH]`

Where:
Cycles:where `words` is the number of quads of input values.
Panics if: | | hash | Computes Poseidon2 hash of a single 256-bit input (1 word = 4 field elements).

**Inputs:** `[A]`
**Outputs:** `[B]`

Where:
Cycles: 19 | | merge | Merges two words (256-bit digests) via Poseidon2 hash.

**Inputs:** `[A, B]`
**Outputs:** `[C]`

Where:
Cycles: 16 | | permute | Performs Poseidon2 permutation on the hasher state.

**Inputs:** `[R0, R1, C]`
**Outputs:** `[R0', R1', C']`

Where:
Cycles: 1 | diff --git a/docs/src/user_docs/core_lib/sys.md b/docs/src/user_docs/core_lib/sys.md index 1c9cf8d3e8..37d86ddca9 100644 --- a/docs/src/user_docs/core_lib/sys.md +++ b/docs/src/user_docs/core_lib/sys.md @@ -6,7 +6,8 @@ sidebar_position: 7 # System procedures Module `miden::core::sys` contains a set of system-level utility procedures. -| Procedure | Description | -| -------------- | ------------- | -| truncate_stack | Removes elements deep in the stack until the depth of the stack is exactly 16. The elements are removed in such a way that the top 16 elements of the stack remain unchanged. If the stack would otherwise contain more than 16 elements at the end of execution, then adding a call to this function at the end will reduce the size of the public inputs that are shared with the verifier.
Input: Stack with 16 or more elements.
Output: Stack with only the original top 16 elements.

Cycles: `17 + 11 * overflow_words`, where `overflow_words` is the number of words to drop. | -| drop_stack_top | Drops the top 16 values from the stack.

Input: Stack with 16 or more elements.
Output: Stack with the top 16 elements removed. | +| Procedure | Description | +| ---------------------- | ------------- | +| truncate_stack | Removes elements deep in the stack until the depth of the stack is exactly 16. The elements are removed in such a way that the top 16 elements of the stack remain unchanged. If the stack would otherwise contain more than 16 elements at the end of execution, then adding a call to this function at the end will reduce the size of the public inputs that are shared with the verifier.
Input: Stack with 16 or more elements.
Output: Stack with only the original top 16 elements.

Cycles: `17 + 11 * overflow_words`, where `overflow_words` is the number of words needed to drop. | +| drop_stack_top | Drops the top 16 values from the stack.

Input: Stack with 16 or more elements.
Output: Stack with the top 16 elements removed. | +| log_precompile_request | Logs a precompile commitment and removes the helper words produced by the underlying `log_precompile` instruction.

Input: `[COMM, TAG, ...]`
Output: `[...]` (top three helper words `R0`, `R1`, `CAP_NEXT` are dropped internally)

Cycles: 1 (plus cost of the underlying `log_precompile` instruction). | diff --git a/processor/Cargo.toml b/processor/Cargo.toml index 118bf2da9e..768799d51b 100644 --- a/processor/Cargo.toml +++ b/processor/Cargo.toml @@ -56,6 +56,7 @@ miden-assembly = { workspace = true, features = ["testing"] } tracing = { workspace = true, features = ["std"] } tracing-subscriber.workspace = true miden-utils-testing.workspace = true +toml = { workspace = true, features = ["parse"] } insta.workspace = true pretty_assertions = { workspace = true, features = ["std"] } proptest.workspace = true diff --git a/processor/src/tests/assembly-cycle-fixtures.toml b/processor/src/tests/assembly-cycle-fixtures.toml new file mode 100644 index 0000000000..f2f12d26c9 --- /dev/null +++ b/processor/src/tests/assembly-cycle-fixtures.toml @@ -0,0 +1,19 @@ +# Assembly instruction cycle fixtures measured with clk. +# Source of truth for assembly cycle fixtures (shared by processor tests and scripts/check_user_doc_cycles.py). +# See processor::tests::user_doc_assembly_cycle_fixtures_match_documentation and issue #3111. + +[[case]] +id = "u32popcnt" +doc = "docs/src/user_docs/assembly/u32_operations.md" +marker = "u32popcnt" +program = "clk push.7 u32popcnt drop clk swap sub" +baseline_program = "clk push.7 drop clk swap sub" +expected = "38 cycles" + +[[case]] +id = "u32popcnt-instruction-reference" +doc = "docs/src/user_docs/assembly/instruction_reference.md" +marker = "u32popcnt" +program = "clk push.7 u32popcnt drop clk swap sub" +baseline_program = "clk push.7 drop clk swap sub" +expected = "38" diff --git a/processor/src/tests/mod.rs b/processor/src/tests/mod.rs index 31f42a4663..93093b1710 100644 --- a/processor/src/tests/mod.rs +++ b/processor/src/tests/mod.rs @@ -1,4 +1,9 @@ -use alloc::{boxed::Box, string::ToString, sync::Arc, vec::Vec}; +use alloc::{ + boxed::Box, + string::{String, ToString}, + sync::Arc, + vec::Vec, +}; use miden_assembly::{ Assembler, DefaultSourceManager, Path, PathBuf, @@ -1504,3 +1509,101 @@ fn test_assert_message_without_debug_info_reports_error_code() { "non-debug execution should not recover package debug assertion messages:\n{diagnostic}" ); } + +/// Verifies assembly instruction cycle fixtures referenced by user docs. +#[test] +fn user_doc_assembly_cycle_fixtures_match_documentation() { + for case in load_assembly_cycle_fixtures() { + let measured = measure_program_cycles(&case.program); + let baseline = measure_program_cycles(&case.baseline_program); + let delta = measured.saturating_sub(baseline); + assert_eq!( + delta, case.expected_cycles, + "fixture {}: program should measure {} cycles (measured {measured}, baseline {baseline})", + case.id, case.expected_cycles, + ); + } +} + +struct AssemblyCycleFixture { + id: String, + program: String, + baseline_program: String, + expected_cycles: u32, +} + +fn load_assembly_cycle_fixtures() -> Vec { + // Packaged with the crate so `cargo test -p miden-processor` works outside the workspace. + const FIXTURES: &str = include_str!("assembly-cycle-fixtures.toml"); + + let table: toml::Table = + FIXTURES.parse().expect("assembly cycle fixtures should be valid TOML"); + let cases = table + .get("case") + .and_then(toml::Value::as_array) + .expect("assembly-cycle-fixtures.toml should contain a [[case]] array"); + + cases + .iter() + .map(|case| { + let case = case.as_table().expect("each [[case]] entry should be a table"); + let expected = case + .get("expected") + .and_then(toml::Value::as_str) + .expect("fixture should declare expected cycle text"); + let expected_cycles = expected + .split_whitespace() + .next() + .and_then(|value| value.parse().ok()) + .unwrap_or_else(|| panic!("could not parse cycle count from {expected:?}")); + + AssemblyCycleFixture { + id: case.get("id").and_then(toml::Value::as_str).expect("id").to_string(), + program: case + .get("program") + .and_then(toml::Value::as_str) + .expect("program") + .to_string(), + baseline_program: case + .get("baseline_program") + .and_then(toml::Value::as_str) + .expect("baseline_program") + .to_string(), + expected_cycles, + } + }) + .collect() +} + +fn measure_program_cycles(program: &str) -> u32 { + use miden_utils_testing::Test; + + const TRUNCATE_STACK: &str = r"@locals(4) +proc truncate_stack + loc_storew_be.0 dropw movupw.3 + sdepth neq.16 + while.true + dropw movupw.3 + sdepth neq.16 + end + loc_loadw_be.0 +end +"; + + let body = program.trim(); + let source = format!( + "{TRUNCATE_STACK}begin +{body} +exec.truncate_stack +end" + ); + + let test = Test::new("program", &source, false); + let outputs = test.get_last_stack_state(); + let measured = outputs + .iter() + .next() + .expect("program should leave a cycle delta on the stack") + .as_canonical_u64(); + u32::try_from(measured).expect("measured cycle count should fit in u32") +} diff --git a/scripts/check-user-doc-cycles.sh b/scripts/check-user-doc-cycles.sh new file mode 100755 index 0000000000..05674d39b9 --- /dev/null +++ b/scripts/check-user-doc-cycles.sh @@ -0,0 +1,27 @@ +#!/bin/bash +set -euo pipefail + +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "${ROOT}" + +echo "Regenerating core library docs..." +MIDEN_BUILD_LIB_DOCS=1 cargo check -p miden-core-lib + +echo "Checking user doc cycle counts..." +if command -v python3.12 >/dev/null 2>&1; then + PYTHON=python3.12 +elif command -v python3.11 >/dev/null 2>&1; then + PYTHON=python3.11 +else + PYTHON=python3 +fi +if ! "$PYTHON" -c 'import tomllib' 2>/dev/null; then + echo "error: Python 3.11+ required (tomllib). Use python3.11 or python3.12." >&2 + exit 1 +fi +"$PYTHON" scripts/check_user_doc_cycles.py + +echo "Checking assembly cycle fixtures..." +# Processor VM tests need a larger stack than the default test thread stack (see Makefile TEST_RUST_MIN_STACK). +RUST_MIN_STACK="${TEST_RUST_MIN_STACK:-16777216}" \ + cargo test -p miden-processor --lib tests::user_doc_assembly_cycle_fixtures_match_documentation -- --exact diff --git a/scripts/check_user_doc_cycles.py b/scripts/check_user_doc_cycles.py new file mode 100644 index 0000000000..eb027cb03f --- /dev/null +++ b/scripts/check_user_doc_cycles.py @@ -0,0 +1,222 @@ +#!/usr/bin/env python3 +"""Check user doc cycle counts against generated core-lib docs and assembly fixtures.""" + +from __future__ import annotations + +import html +import re +import sys +import tomllib +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +MAPPINGS = Path(__file__).resolve().parent / "user-doc-cycle-mappings.toml" +ASSEMBLY_FIXTURES = ROOT / "processor/src/tests/assembly-cycle-fixtures.toml" + + +def extract_cycles_from_description(description: str) -> str: + description = html.unescape(description) + matches = list( + re.finditer(r"\bCycles(?:\s*\((estimate)\))?\s*:?\s*(.*)", description, re.DOTALL) + ) + if not matches: + return "" + + match = matches[-1] + is_estimate = match.group(1) is not None + block = match.group(2).strip() + block = re.split( + r"(?:#?\s*panics\b|security:|note:)", + block, + maxsplit=1, + flags=re.IGNORECASE, + )[0] + block = re.sub(r"", "\n", block, flags=re.IGNORECASE) + block = re.sub(r"", "\n", block, flags=re.IGNORECASE) + block = re.sub(r"", "", block, flags=re.IGNORECASE) + block = re.sub(r"]+>", "", block) + block = block.replace("`", "") + block = re.sub(r"\*\*", "", block) + block = re.sub(r"\$([^$]+)\$", r"\1", block) + # Preserve estimate markers (~ or Cycles (estimate)) in the normalized text. + if "~" in block: + is_estimate = True + block = block.replace("~", "") + block = re.sub(r"(?m)^\s*-\s+", "", block) + block = re.sub(r"where:\s*", "where ", block, flags=re.IGNORECASE) + block = re.sub(r"[,.\:;]", " ", block) + block = re.sub(r"\s+", " ", block.lower()).strip() + if is_estimate: + return f"estimate {block}" + return block + +def slice_section(content: str, section: str | None) -> str: + if not section: + return content + + heading = re.escape(section) + pattern = re.compile(rf"^#{{2,3}}\s+{heading}\s*$", re.MULTILINE) + match = pattern.search(content) + if not match: + raise KeyError(f"section not found: {section!r}") + + start = match.end() + next_heading = re.search(r"^#{2,3}\s+", content[start:], re.MULTILINE) + end = start + next_heading.start() if next_heading else len(content) + return content[start:end] + + +def extract_table_row_description(line: str, procedure: str) -> str | None: + if not line.startswith("|") or line.startswith("| ---"): + return None + + parts = line.split("|", 2) + if len(parts) < 3: + return None + + name = parts[1].split("<", 1)[0].strip() + if name != procedure: + return None + + description = parts[2].rstrip() + if description.endswith("|"): + description = description[:-1].rstrip() + return description + + +def extract_user_procedure_cycles(content: str, section: str | None, procedure: str) -> str: + scoped = slice_section(content, section) + + subsection = section or procedure + if re.search(rf"^###\s+{re.escape(subsection)}\s*$", content, re.MULTILINE): + for line in scoped.splitlines(): + if re.search(r"cycles", line, re.IGNORECASE): + return extract_cycles_from_description(line) + raise KeyError(f"no cycle text in subsection: {subsection!r}") + + for line in scoped.splitlines(): + description = extract_table_row_description(line, procedure) + if description is not None: + return extract_cycles_from_description(description) + + raise KeyError(f"procedure row not found: {procedure!r}") + + +def extract_generated_procedure_cycles(path: Path, procedure: str) -> str: + content = path.read_text(encoding="utf-8") + for line in content.splitlines(): + description = extract_table_row_description(line, procedure) + if description is not None: + return extract_cycles_from_description(description) + + raise KeyError(f"generated procedure not found: {procedure!r} in {path}") + + +def check_core_lib_mappings() -> list[str]: + entries = tomllib.loads(MAPPINGS.read_text(encoding="utf-8"))["entry"] + errors: list[str] = [] + + for entry in entries: + user_path = ROOT / entry["user_doc"] + generated_path = ROOT / entry["generated_doc"] + section = entry.get("section") + procedure = entry["procedure"] + + try: + user_content = user_path.read_text(encoding="utf-8") + user_cycles = extract_user_procedure_cycles(user_content, section, procedure) + generated_cycles = extract_generated_procedure_cycles(generated_path, procedure) + except KeyError as err: + errors.append( + f"{user_path}: {procedure}: {err} " + f"(generated: {generated_path}, procedure: {procedure})" + ) + continue + + if user_cycles != generated_cycles: + errors.append( + f"{user_path}: {procedure}\n" + f" expected (generated): {generated_cycles!r}\n" + f" actual (user doc): {user_cycles!r}" + ) + + return errors + + +def _normalize_table_cell(cell: str) -> str: + text = html.unescape(cell) + text = re.sub(r"", " ", text, flags=re.IGNORECASE) + text = re.sub(r"]+>", "", text) + text = text.replace("`", "") + text = re.sub(r"\s+", " ", text).strip() + return text + + +def extract_cycle_cell_from_row(row: str) -> str | None: + """Return the cycle cell text from a marked markdown table row. + + Prefer a dedicated Cycles column (instruction_reference style). Fall back to + an embedded `*(N cycles)*` fragment in the instruction cell (u32_operations). + """ + cells = [c.strip() for c in row.strip().strip("|").split("|")] + for cell in cells: + text = _normalize_table_cell(cell) + if re.fullmatch(r"\d+(?: cycles?)?", text, re.IGNORECASE): + return text.lower() + if re.fullmatch(r"\d+(?: \d+)+", text): + return text.lower() + for cell in cells: + match = re.search(r"\*\(\s*(\d+\s+cycles?)\s*\)\*", cell, re.IGNORECASE) + if match: + return re.sub(r"\s+", " ", match.group(1).lower()) + return None + + +def check_assembly_fixtures() -> list[str]: + cases = tomllib.loads(ASSEMBLY_FIXTURES.read_text(encoding="utf-8"))["case"] + errors: list[str] = [] + + for case in cases: + case_id = case["id"] + doc_path = ROOT / case["doc"] + marker = f"" + expected = case["expected"].strip().lower() + + content = doc_path.read_text(encoding="utf-8") + if marker not in content: + errors.append(f"{doc_path}: missing marker {marker!r}") + continue + + marker_at = content.index(marker) + row_start = content.rfind("\n", 0, marker_at) + 1 + row_end = content.find("\n", marker_at) + if row_end == -1: + row_end = len(content) + row = content[row_start:row_end] + actual = extract_cycle_cell_from_row(row) + if actual is None: + errors.append( + f"{doc_path}: marker {case_id!r} row has no cycle cell matching {expected!r}" + ) + elif actual != expected: + errors.append( + f"{doc_path}: marker {case_id!r} cycle cell is {actual!r}, expected {expected!r}" + ) + + return errors +def main() -> int: + errors = check_core_lib_mappings() + errors.extend(check_assembly_fixtures()) + + if errors: + print("User doc cycle check failed:\n", file=sys.stderr) + for error in errors: + print(f"- {error}\n", file=sys.stderr) + return 1 + + print("User doc cycle counts are in sync.") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/user-doc-cycle-mappings.toml b/scripts/user-doc-cycle-mappings.toml new file mode 100644 index 0000000000..527206289b --- /dev/null +++ b/scripts/user-doc-cycle-mappings.toml @@ -0,0 +1,172 @@ +# Maps user-facing core library docs to generated MASM docs (source of truth for cycles). +# See scripts/check_user_doc_cycles.py and issue #3111. + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/collections.md" +section = "Merkle Mountain Range" +procedure = "add" +generated_doc = "crates/lib/core/docs/collections/mmr.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/collections.md" +section = "Merkle Mountain Range" +procedure = "pack" +generated_doc = "crates/lib/core/docs/collections/mmr.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/collections.md" +section = "Merkle Mountain Range" +procedure = "unpack" +generated_doc = "crates/lib/core/docs/collections/mmr.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/collections.md" +section = "Merkle Mountain Range" +procedure = "num_leaves_to_num_peaks" +generated_doc = "crates/lib/core/docs/collections/mmr.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/collections.md" +section = "Merkle Mountain Range" +procedure = "num_peaks_to_message_size" +generated_doc = "crates/lib/core/docs/collections/mmr.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/collections.md" +section = "Sorted Array" +procedure = "find_word" +generated_doc = "crates/lib/core/docs/collections/sorted_array.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/word.md" +procedure = "reverse" +generated_doc = "crates/lib/core/docs/word.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/word.md" +procedure = "store_word_u32s_le" +generated_doc = "crates/lib/core/docs/word.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/word.md" +procedure = "eqz" +generated_doc = "crates/lib/core/docs/word.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/word.md" +procedure = "testz" +generated_doc = "crates/lib/core/docs/word.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/word.md" +procedure = "gt" +generated_doc = "crates/lib/core/docs/word.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/word.md" +procedure = "gte" +generated_doc = "crates/lib/core/docs/word.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/word.md" +procedure = "lt" +generated_doc = "crates/lib/core/docs/word.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/word.md" +procedure = "lte" +generated_doc = "crates/lib/core/docs/word.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/word.md" +procedure = "eq" +generated_doc = "crates/lib/core/docs/word.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/word.md" +procedure = "test_eq" +generated_doc = "crates/lib/core/docs/word.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/sys.md" +procedure = "truncate_stack" +generated_doc = "crates/lib/core/docs/sys.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/hashes.md" +section = "Poseidon2" +procedure = "init_no_padding" +generated_doc = "crates/lib/core/docs/crypto/hashes/poseidon2.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/hashes.md" +section = "Poseidon2" +procedure = "squeeze_digest" +generated_doc = "crates/lib/core/docs/crypto/hashes/poseidon2.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/hashes.md" +section = "Poseidon2" +procedure = "copy_digest" +generated_doc = "crates/lib/core/docs/crypto/hashes/poseidon2.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/hashes.md" +section = "Poseidon2" +procedure = "absorb_double_words_from_memory" +generated_doc = "crates/lib/core/docs/crypto/hashes/poseidon2.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/hashes.md" +section = "Poseidon2" +procedure = "hash_double_words" +generated_doc = "crates/lib/core/docs/crypto/hashes/poseidon2.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/hashes.md" +section = "Poseidon2" +procedure = "hash_words" +generated_doc = "crates/lib/core/docs/crypto/hashes/poseidon2.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/hashes.md" +section = "Poseidon2" +procedure = "hash_elements" +generated_doc = "crates/lib/core/docs/crypto/hashes/poseidon2.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/hashes.md" +section = "Poseidon2" +procedure = "pad_and_hash_elements" +generated_doc = "crates/lib/core/docs/crypto/hashes/poseidon2.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/hashes.md" +section = "Poseidon2" +procedure = "hash" +generated_doc = "crates/lib/core/docs/crypto/hashes/poseidon2.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/hashes.md" +section = "Poseidon2" +procedure = "merge" +generated_doc = "crates/lib/core/docs/crypto/hashes/poseidon2.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/hashes.md" +section = "Poseidon2" +procedure = "permute" +generated_doc = "crates/lib/core/docs/crypto/hashes/poseidon2.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/aead.md" +section = "encrypt" +procedure = "encrypt" +generated_doc = "crates/lib/core/docs/crypto/aead.md" + +[[entry]] +user_doc = "docs/src/user_docs/core_lib/crypto/aead.md" +section = "decrypt" +procedure = "decrypt" +generated_doc = "crates/lib/core/docs/crypto/aead.md" +