Check user doc cycle counts against source of truth (#3111)

.github/workflows/test.yml

@@ -149,3 +149,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

CHANGELOG.md

@@ -6,6 +6,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)).

Makefile

@@ -25,7 +25,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 --------------------------------------------------------------------------
@@ -208,6 +209,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

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 = [

crates/lib/core/asm/collections/mmr.masm

@@ -129,7 +129,7 @@ end
 #!    The address is expected to be word-aligned.
 #!
 #! Cycles: 162 + 9 * extra_peak_pair cycles
-#!    where `extra_peak` is the number of peak pairs in addition to the first
+#!    where `extra_peak_pair` is the number of peak pairs in addition to the first
 #!    16, i.e. `round_up((num_of_peaks - 16) / 2)`
 pub proc unpack
   # load the num_leaves and peaks to the advice_stack (0 cycles)

crates/lib/core/docs/collections/mmr.md

@@ -5,6 +5,6 @@
 | get | Loads the leaf at the absolute `pos` in the MMR.<br /><br />This MMR implementation supports only u32 positions.<br /><br />The position must refer to an existing leaf: `pos < num_leaves`, where `num_leaves` is stored<br />at `mmr_ptr[0]`. The procedure fails instead of returning an empty or sentinel word when `pos`<br />is outside the current MMR.<br /><br />Stack transition:<br />Input: [pos, mmr_ptr, ...]<br />Output: [N, ...] where `N` is the leaf and `R` is the MMR peak that owns the leaf.<br /> |
 | num_leaves_to_num_peaks | Given the num_leaves of a MMR returns the num_peaks.<br /><br />Implemented as counting the number of "1" bits in `num_leaves`.<br /><br />Input: [num_leaves, ...]<br />Output: [num_peaks, ...]<br />Cycles: 67<br /> |
 | num_peaks_to_message_size | Given the num_peaks of a MMR, returns the hasher state size after accounting<br />for the required padding.<br /><br />Input: [num_peaks, ...]<br />Output: [len, ...]<br />Cycles: 19<br /> |
-| unpack | Writes the MMR who's peaks hash to `HASH` to the memory location pointed to by `mmr_ptr`.<br /><br />Input: [HASH, mmr_ptr, ...]<br />Output: [...]<br /><br />Where:<br />- HASH: is the MMR peak hash, the hash is expected to be padded to an even<br />length and to have a minimum size of 16 elements<br />- The advice map must contain a key with HASH, and its value is<br />`[num_leaves, 0, 0 , 0] \|\| hash_data`, and hash_data is the data used to computed `HASH`<br />- mmr_ptr: the memory location where the MMR data will be written to,<br />starting with the MMR forest (its total leaves count) followed by its peaks.<br />The address is expected to be word-aligned.<br /><br />Cycles: 162 + 9 * extra_peak_pair cycles<br />where `extra_peak` is the number of peak pairs in addition to the first<br />16, i.e. `round_up((num_of_peaks - 16) / 2)`<br /> |
+| unpack | Writes the MMR who's peaks hash to `HASH` to the memory location pointed to by `mmr_ptr`.<br /><br />Input: [HASH, mmr_ptr, ...]<br />Output: [...]<br /><br />Where:<br />- HASH: is the MMR peak hash, the hash is expected to be padded to an even<br />length and to have a minimum size of 16 elements<br />- The advice map must contain a key with HASH, and its value is<br />`[num_leaves, 0, 0 , 0] \|\| hash_data`, and hash_data is the data used to computed `HASH`<br />- mmr_ptr: the memory location where the MMR data will be written to,<br />starting with the MMR forest (its total leaves count) followed by its peaks.<br />The address is expected to be word-aligned.<br /><br />Cycles: 162 + 9 * extra_peak_pair cycles<br />where `extra_peak_pair` is the number of peak pairs in addition to the first<br />16, i.e. `round_up((num_of_peaks - 16) / 2)`<br /> |
 | pack | Computes the hash of the given MMR and copies it to the Advice Map using its hash as a key.<br /><br />Input: [mmr_ptr, ...]<br />Output: [HASH, ...]<br />Cycles: 128 + 3 * num_peaks<br /> |
 | add | Adds a new element to the MMR.<br /><br />This will update the MMR peaks in the VM's memory and the advice provider<br />with any merged nodes.<br /><br />Input: [EL, mmr_ptr, ...]<br />Output: [...]<br />Cycles: 145 + 39 * peak_merges<br /> |

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` <br /> `u32shr.b`   | `[b, a, ...]` | `[c, ...]`   | 20 <br /> 5 | $c = \lfloor a / 2^b \rfloor$. Undefined if $a \geq 2^{32}$ or $b > 31$.    |
 | `u32rotl` <br /> `u32rotl.b` | `[b, a, ...]` | `[c, ...]`   | 18 <br /> 3 | Rotate left. Undefined if $a \geq 2^{32}$ or $b > 31$.                      |
 | `u32rotr` <br /> `u32rotr.b` | `[b, a, ...]` | `[c, ...]`   | 22 <br /> 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` <!-- cycle-check: 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}$.                           |

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 <br /> - *(20 cycles)* <br /> u32shr.*b* <br /> - *(5 cycles)*   | [b, a, ...]    | [c, ...]      | $c \leftarrow \lfloor a/2^b \rfloor$ <br /> Undefined if $a \ge 2^{32}$ or $b > 31$                                              |
 | u32rotl <br /> - *(18 cycles)* <br /> u32rotl.*b* <br /> - *(3 cycles)* | [b, a, ...]    | [c, ...]      | Computes $c$ by rotating a 32-bit representation of $a$ to the left by $b$ bits. <br /> Undefined if $a \ge 2^{32}$ or $b > 31$  |
 | u32rotr <br /> - *(22 cycles)* <br /> u32rotr.*b* <br /> - *(3 cycles)* | [b, a, ...]    | [c, ...]      | Computes $c$ by rotating a 32-bit representation of $a$ to the right by $b$ bits. <br /> Undefined if $a \ge 2^{32}$ or $b > 31$ |
-| u32popcnt <br /> - *(32 cycles)*                                              | [a, ...]       | [b, ...]      | Computes $b$ by counting the number of set bits in $a$ (hamming weight of $a$). <br /> Undefined if $a \ge 2^{32}$               |
+| u32popcnt <!-- cycle-check: u32popcnt --> <br /> - *(38 cycles)*              | [a, ...]       | [b, ...]      | Computes $b$ by counting the number of set bits in $a$ (hamming weight of $a$). <br /> Undefined if $a \ge 2^{32}$               |
 | u32clz <br /> - *(48 cycles)*                                                     | [a, ...]    | [b, ...]      | Computes $b$ as a number of leading zeros of $a$. <br /> Undefined if $a \ge 2^{32}$               |
 | u32ctz <br /> - *(34 cycles)*                                                     | [a, ...]    | [b, ...]      | Computes $b$ as a number of trailing zeros of $a$. <br /> Undefined if $a \ge 2^{32}$               |
 | u32clo <br /> - *(40 cycles)*                                                     | [a, ...]    | [b, ...]      | Computes $b$ as a number of leading ones of $a$. <br /> Undefined if $a \ge 2^{32}$               |

docs/src/user_docs/core_lib/collections.md

@@ -20,7 +20,7 @@ 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`.<br /><br />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, ...]`.<br /><br />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.<br /><br />Cycles: `162 + 9 * extra_peak_pair` |
+| 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.<br /><br />Cycles: 162 + 9 * extra_peak_pair cycles<br />where `extra_peak_pair` is the number of peak pairs in addition to the first 16, 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`).<br /><br />Inputs: `[num_leaves, ...]`<br />Outputs: `[num_peaks, ...]`<br /><br />Cycles: 67 |
 | 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).<br /><br />Inputs: `[num_peaks, ...]`<br />Outputs: `[message_size, ...]`<br /><br />Cycles: 19 |
 
@@ -49,6 +49,6 @@ The following procedures are available:
 
 | Procedure          | Description |
 |--------------------|-------------|
-| find_word          | Finds a value in a sorted array of words.<br/><br/>**Inputs:** `[VALUE, start_ptr, end_ptr, ...]`<br/>**Outputs:** `[is_value_found, value_ptr, start_ptr, end_ptr, ...]`<br/><br/>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.<br/><br/>**Requirements:**<br/>- Words must be sorted in non-decreasing order<br/>- `start_ptr` and `end_ptr` must be word-aligned<br/>- `start_ptr <= end_ptr`<br/><br/>**Cycles:** 25-286 depending on case |
+| find_word          | Finds a value in a sorted array of words.<br/><br/>**Inputs:** `[VALUE, start_ptr, end_ptr, ...]`<br/>**Outputs:** `[is_value_found, value_ptr, start_ptr, end_ptr, ...]`<br/><br/>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.<br/><br/>**Requirements:**<br/>- Words must be sorted in non-decreasing order<br/>- `start_ptr` and `end_ptr` must be 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 |
 | find_key_value     | Finds a key in a sorted array of (key, value) word tuples.<br/><br/>**Inputs:** `[KEY, start_ptr, end_ptr, ...]`<br/>**Outputs:** `[is_key_found, key_ptr, start_ptr, end_ptr, ...]`<br/><br/>Where `KEY` is the 4-element key to search for. The array contains pairs of words where each pair is (key, value).<br/><br/>**Requirements:**<br/>- Keys must be sorted in non-decreasing order<br/>- `start_ptr` must be word-aligned<br/>- `(end_ptr - start_ptr)` must be divisible by 8 (double-word aligned)<br/>- `start_ptr <= end_ptr`<br/><br/>**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.<br/><br/>**Inputs:** `[key_suffix, key_prefix, start_ptr, end_ptr, ...]`<br/>**Outputs:** `[is_key_found, key_ptr, start_ptr, end_ptr, ...]`<br/><br/>Where `key_prefix` is the most significant element and `key_suffix` is the second most significant element of the key to match.<br/><br/>Same requirements as `find_key_value`. |

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.