PoC: Add experimental masm-lint CI and fix core MASM findings

.github/patches/masm-decompiler-swapdw-stack-effect.patch

@@ -0,0 +1,56 @@
+From 74aac0735c6035ff7089cae9b5c6452b0f19c5f9 Mon Sep 17 00:00:00 2001
+From: =?UTF-8?q?Fran=C3=A7ois=20Garillot?= <francois@garillot.net>
+Date: Sat, 25 Apr 2026 03:55:26 -0400
+Subject: [PATCH] Fix swapdw stack effect
+
+---
+ src/signature/effects.rs     | 10 +++++++++-
+ tests/signature_inference.rs |  4 ++--
+ 2 files changed, 11 insertions(+), 3 deletions(-)
+
+diff --git a/src/signature/effects.rs b/src/signature/effects.rs
+index ef4a665..fe34d51 100644
+--- a/src/signature/effects.rs
++++ b/src/signature/effects.rs
+@@ -248,7 +248,7 @@ impl From<&Instruction> for StackEffect {
+             SwapW1 => StackEffect::known(8, 8),
+             SwapW2 => StackEffect::known(12, 12),
+             SwapW3 => StackEffect::known(16, 16),
+-            SwapDw => StackEffect::known(8, 8),
++            SwapDw => StackEffect::known(16, 16),
+
+             CSwap => StackEffect::known(3, 2),
+             CSwapW => StackEffect::known(9, 8),
+@@ -451,6 +451,14 @@ mod tests {
+         );
+     }
+
++    #[test]
++    fn swapdw_swaps_four_words() {
++        assert_eq!(
++            StackEffect::from(&Instruction::SwapDw),
++            StackEffect::known(16, 16)
++        );
++    }
++
+     #[test]
+     fn then_push_then_drop_is_neutral() {
+         // push: (0, 1, 0) then drop: (1, 0, 1) = (0, 0, 0)
+diff --git a/tests/signature_inference.rs b/tests/signature_inference.rs
+index 583243d..1acbb8d 100644
+--- a/tests/signature_inference.rs
++++ b/tests/signature_inference.rs
+@@ -437,8 +437,8 @@ fn infers_correct_stack_effect_for_swapdw() {
+         ProcSignature::Known {
+             inputs, outputs, ..
+         } => {
+-            assert_eq!(*inputs, 8);
+-            assert_eq!(*outputs, 8);
++            assert_eq!(*inputs, 16);
++            assert_eq!(*outputs, 16);
+         }
+         ProcSignature::Unknown => panic!("expected known signature"),
+     }
+-- 
+2.50.1 (Apple Git-155)
+

.github/workflows/lint.yml

@@ -55,6 +55,58 @@ jobs:
       - name: Check workspace inheritance
         run: cargo workspace-inheritance-check --promotion-threshold 2 --promotion-failure
 
+  masm-lint:
+    name: masm-lint on ubuntu-latest
+    runs-on: ubuntu-latest
+    env:
+      MASM_LSP_REF: 0f7f54fed90aae59aaef241325e8f0d108b2d971
+      MASM_DECOMPILER_REF: a3d7aff5426e5e11556c73504782004de9edce07
+    steps:
+      - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4.3.1
+        with:
+          persist-credentials: false
+      - name: Cleanup large tools for build space
+        uses: ./.github/actions/cleanup-runner
+      - name: Install rust
+        run: rustup update --no-self-update
+      - name: Checkout masm-lsp sources
+        run: |
+          git init --quiet .tmp/masm-lsp
+          git -C .tmp/masm-lsp remote add origin https://github.com/trailofbits/masm-lsp
+          git -C .tmp/masm-lsp fetch --depth=1 origin "$MASM_LSP_REF"
+          git -C .tmp/masm-lsp checkout --detach FETCH_HEAD
+      - name: Checkout masm-decompiler sources
+        run: |
+          git init --quiet .tmp/masm-decompiler
+          git -C .tmp/masm-decompiler remote add origin https://github.com/trailofbits/masm-decompiler
+          git -C .tmp/masm-decompiler fetch --depth=1 origin "$MASM_DECOMPILER_REF"
+          git -C .tmp/masm-decompiler checkout --detach FETCH_HEAD
+      - name: Patch masm-decompiler stack effects
+        run: >
+          git -C .tmp/masm-decompiler apply
+          "$GITHUB_WORKSPACE/.github/patches/masm-decompiler-swapdw-stack-effect.patch"
+      - name: Use checked out masm-decompiler
+        run: |
+          python - <<'PY'
+          from pathlib import Path
+          cargo_toml = Path(".tmp/masm-lsp/Cargo.toml")
+          old = 'masm-decompiler = { version = "=0.6.1", git = "https://github.com/trailofbits/masm-decompiler", rev = "dac04e17dea54e7e025c48745705f4dc0433bc91" }'
+          new = 'masm-decompiler = { path = "../masm-decompiler" }'
+          text = cargo_toml.read_text()
+          if old not in text:
+              raise SystemExit("expected masm-decompiler workspace dependency not found")
+          cargo_toml.write_text(text.replace(old, new))
+          PY
+      - name: Install masm-lint
+        run: >
+          cargo install
+          --path .tmp/masm-lsp/crates/masm-lint
+      - name: Lint MASM core library
+        run: >
+          masm-lint --no-color
+          --library miden::core=crates/lib/core/asm
+          crates/lib/core/asm
+
   clippy:
     name: clippy nightly on ubuntu-latest
     runs-on: ubuntu-latest

CHANGELOG.md

@@ -21,6 +21,7 @@
 #### Changes
 
 - [BREAKING] Refactored MAST forest serialization around fixed-layout full, stripped, and hashless sections, and bumped the MAST wire format to `0.0.3` ([#2765](https://github.com/0xMiden/miden-vm/pull/2765)).
+- Added experimental `masm-lint` CI for the core MASM library, and fixed invalid signatures and missing `u32assert` checks it surfaced ([#3052](https://github.com/0xMiden/miden-vm/pull/3052)).
 - Documented sortedness precondition more prominently for sorted array operations ([#2832](https://github.com/0xMiden/miden-vm/pull/2832)).
 - [BREAKING] Updated the Miden crypto stack to `miden-crypto` and `miden-lifted-stark` v0.24, and switched digest-ordering code to `Word`'s native lexicographic ordering ([#3039](https://github.com/0xMiden/miden-vm/pull/3039)).
 - Borrowed operation slices in basic-block batching helpers to avoid cloning in the fingerprinting path ([#2994](https://github.com/0xMiden/miden-vm/pull/2994)).

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

@@ -41,7 +41,7 @@ pub proc find_word
         #=> [maybe_value_ptr, VALUE, start_ptr, end_ptr]
 
         # dereference maybe_value_ptr (8 cycles)
-        dup movdn.5 padw movup.4 mem_loadw_le
+        dup u32assert.err="maybe_value_ptr is not u32" movdn.5 padw movup.4 mem_loadw_le
         #=> [MAYBE_VALUE, VALUE, maybe_value_ptr, start_ptr, end_ptr]
 
         # check if it matches the requested VALUE (15 cycles)
@@ -78,7 +78,7 @@ pub proc find_word
                 #=> [VALUE, maybe_value_ptr, start_ptr, end_ptr]
 
                 # dereference maybe_value_ptr (7 cycles)
-                dup.4 padw movup.4 mem_loadw_le
+                dup.4 u32assert.err="start_ptr is not u32" padw movup.4 mem_loadw_le
                 #=> [FIRST_WORD, VALUE, maybe_value_ptr = start_ptr, start_ptr, end_ptr]
 
                 # there was no match, the first array element must be larger than VALUE
@@ -99,7 +99,7 @@ pub proc find_word
                 #=> [maybe_value_ptr = end_ptr, VALUE, start_ptr, end_ptr]
 
                 # fetch the last word in the array (10 cycles)
-                dup movdn.5 sub.4 padw movup.4 mem_loadw_le
+                dup movdn.5 sub.4 u32assert.err="end_ptr-4 is not u32" padw movup.4 mem_loadw_le
                 #=> [LAST_WORD, VALUE, maybe_value_ptr = end_ptr, start_ptr, end_ptr]
 
                 # there was no match, the last array element must be smaller than VALUE
@@ -122,15 +122,15 @@ pub proc find_word
                 #=> [VALUE, VALUE, maybe_value_ptr, start_ptr, end_ptr]
 
                 # dereference maybe_value_ptr (8 cycles)
-                padw dup.12 mem_loadw_le
+                padw dup.12 u32assert.err="maybe_value_ptr is not u32" mem_loadw_le
                 #=> [MAYBE_VALUE, VALUE, VALUE, maybe_value_ptr, start_ptr, end_ptr]
 
                 # there was no match, MAYBE_VALUE must be larger than VALUE (123 cycles)
                 exec.word::lt
                 assert.err="lowerbound_array invariant: *maybe_value_ptr not greater than VALUE"
 
                 # dereference `maybe_value_ptr-4` (11 cycles)
-                padw dup.8 sub.4 mem_loadw_le
+                padw dup.8 sub.4 u32assert.err="maybe_value_ptr-4 is not u32" mem_loadw_le
                 #=> [MAYBE_VALUE_PREV, VALUE, maybe_value_ptr, start_ptr, end_ptr]
 
                 # there was no match, MAYBE_VALUE_PREV must be smaller than VALUE (119 cycles)
@@ -254,11 +254,12 @@ proc find_partial_key_value
         #=> [maybe_key_ptr, KEY, start_ptr, end_ptr]
 
         # make sure maybe_key_ptr is pointing to a key, not value (10 cycles)
-        dup dup.6 sub u32mod.8 assertz.err="lowerbound_key_value invariant: key_ptr must be double-word aligned with start_ptr"
+        dup dup.6 sub u32assert.err="maybe_key_ptr-start_ptr is not u32"
+        u32mod.8 assertz.err="lowerbound_key_value invariant: key_ptr must be double-word aligned with start_ptr"
         #=> [maybe_key_ptr, KEY, start_ptr, end_ptr]
 
         # dereference maybe_key_ptr (22 cycles)
-        dup movdn.5
+        dup u32assert.err="maybe_key_ptr is not u32" movdn.5
         #=> [maybe_key_ptr, KEY, maybe_key_ptr, start_ptr, end_ptr]
 
         loc_load.0 exec.load_key
@@ -293,7 +294,7 @@ proc find_partial_key_value
                 #=> [maybe_key_ptr = start_ptr, KEY, start_ptr, end_ptr]
 
                 # load key (22 cycles)
-                dup movdn.5
+                dup u32assert.err="start_ptr is not u32" movdn.5
                 #=> [maybe_key_ptr, KEY, maybe_key_ptr, start_ptr, end_ptr]
 
                 loc_load.0 exec.load_key
@@ -317,7 +318,7 @@ proc find_partial_key_value
                 #=> [maybe_key_ptr = end_ptr, KEY, start_ptr, end_ptr]
 
                 # fetch the last key in the array (23 cycles)
-                dup movdn.5 sub.8
+                dup movdn.5 sub.8 u32assert.err="end_ptr-8 is not u32"
                 #=> [maybe_key_ptr-8, KEY, maybe_key_ptr, start_ptr, end_ptr]
 
                 loc_load.0 exec.load_key
@@ -400,4 +401,4 @@ proc load_key
 
     movup.4 drop
     # => [w0', w1', w2, w3]
-end
+end

crates/lib/core/asm/math/u256.masm

@@ -295,7 +295,7 @@ end
 #! Returns 1 if the top u256 value is zero; lower stack values are preserved.
 #! Stack transition looks as follows:
 #! [a0, a1, a2, a3, a4, a5, a6, a7, ...] -> [is_zero, ...].
-pub proc eqz(rhs: u256, lhs: u256) -> i1
+pub proc eqz(a: u256) -> i1
     eq.0
     repeat.7
         swap

crates/lib/core/asm/pcs/fri/frie2f4.masm

@@ -14,6 +14,7 @@ use miden::core::pcs::fri::helper
 @locals(16)
 pub proc preprocess
     adv_push.1
+    u32assert
     # => [num_queries, g, ...]
     exec.constants::fri_com_ptr
     # => [layer_ptr, num_queries, g, ...]
@@ -45,6 +46,7 @@ pub proc preprocess
     #=> [X, layer_ptr, layer_ptr, g]
 
     adv_push.1
+    u32assert
     mul.2
     sub.1
     movdn.4
@@ -72,6 +74,7 @@ pub proc preprocess
     #=> [X, remainder_poly_ptr, remainder_poly_ptr, layer_ptr, g]
 
     adv_push.1
+    u32assert
     dup mul.2 exec.constants::set_remainder_poly_size
 
     sub.1

crates/lib/core/asm/sys/mod.masm

@@ -31,7 +31,7 @@ pub proc truncate_stack()
 end
 
 #! Drop 16 values from the stack.
-pub proc drop_stack_top()
+pub proc drop_stack_top(top: word, upper_mid: word, lower_mid: word, bottom: word)
     dropw dropw dropw dropw
 end
 

crates/lib/core/tests/pcs/fri/mod.rs

@@ -8,6 +8,14 @@ pub(crate) mod verifier_fri_e2f4;
 use miden_core::Word;
 pub use verifier_fri_e2f4::*;
 
+const PREPROCESS_SOURCE: &str = "
+        use miden::core::pcs::fri::frie2f4
+
+        begin
+            exec.frie2f4::preprocess
+        end
+        ";
+
 #[test]
 fn fri_fold4_ext2_remainder64() {
     let source = "
@@ -104,6 +112,79 @@ fn fri_fold4_ext2_remainder128() {
     test.expect_stack(&[]);
 }
 
+#[test]
+fn fri_preprocess_rejects_non_u32_num_queries() {
+    let (domain_generator, mut advice_stack, num_layers_index, remainder_length_index) =
+        prepare_preprocess_inputs(14);
+    let invalid_u32 = u64::from(u32::MAX) + 1;
+
+    advice_stack[0] = invalid_u32;
+    // Keep later counters valid so this test isolates the first assertion.
+    advice_stack[num_layers_index] = 1;
+    advice_stack[remainder_length_index] = 1;
+
+    let test = build_test!(PREPROCESS_SOURCE, &[domain_generator], &advice_stack);
+    expect_assert_error_message!(test);
+}
+
+#[test]
+fn fri_preprocess_rejects_non_u32_num_layers() {
+    let (domain_generator, mut advice_stack, num_layers_index, remainder_length_index) =
+        prepare_preprocess_inputs(14);
+    let invalid_u32 = u64::from(u32::MAX) + 1;
+
+    advice_stack[num_layers_index] = invalid_u32;
+    advice_stack[remainder_length_index] = 1;
+
+    let test = build_test!(PREPROCESS_SOURCE, &[domain_generator], &advice_stack);
+    expect_assert_error_message!(test);
+}
+
+#[test]
+fn fri_preprocess_rejects_non_u32_remainder_length() {
+    let (domain_generator, mut advice_stack, _, remainder_length_index) =
+        prepare_preprocess_inputs(14);
+    let invalid_u32 = u64::from(u32::MAX) + 1;
+
+    advice_stack[remainder_length_index] = invalid_u32;
+
+    let test = build_test!(PREPROCESS_SOURCE, &[domain_generator], &advice_stack);
+    expect_assert_error_message!(test);
+}
+
+fn prepare_preprocess_inputs(trace_len_e: usize) -> (u64, Vec<u64>, usize, usize) {
+    let blowup_exp = 3;
+    let depth = trace_len_e + blowup_exp;
+    let domain_size = 1 << depth;
+
+    let FriResult {
+        positions,
+        alphas,
+        commitments,
+        remainder,
+        num_queries,
+        ..
+    } = fri_prove_verify_fold4_ext2(trace_len_e).unwrap();
+
+    let num_layers = (commitments.len() / 4) - 1;
+    let num_layers_index = 1 + positions.len();
+    let remainder_length_index = num_layers_index + 1 + (num_layers * 8);
+
+    let advice_stack = prepare_advice_stack(
+        depth,
+        domain_size,
+        num_queries,
+        positions,
+        alphas,
+        commitments,
+        remainder,
+    );
+
+    let domain_generator = Felt::get_root_of_unity(domain_size.ilog2()).as_canonical_u64();
+
+    (domain_generator, advice_stack, num_layers_index, remainder_length_index)
+}
+
 fn prepare_advice_stack(
     depth: usize,
     domain_size: u32,