miden-processor 0.23.0

Miden VM processor
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86

//! Stack overflow table bus test.
//!
//! Runs a PAD/DROP sequence and verifies that every interaction the stack-overflow bus emitter
//! fires at a right-shift (`PAD`) or left-shift-with-non-empty-overflow (`DROP`) row appears
//! somewhere in that row's bag of prover pushes. The test is column-blind — see
//! `processor/src/trace/tests/lookup_harness.rs` for the subset matcher.
//!
//! The DYNCALL branch of the bus is intentionally not exercised here; constructing a DYNCALL
//! with a non-empty overflow requires a full program around a host and fits better in an
//! integration test.

use alloc::vec::Vec;

use miden_air::logup::StackOverflowMsg;
use miden_core::{
    Felt,
    operations::{Operation, opcodes},
};

use super::{
    build_trace_from_ops,
    lookup_harness::{Expectations, InteractionLog},
};
use crate::RowIndex;

#[test]
fn stack_overflow_bus_emits_per_interaction_row() {
    // Mix of right-shifts (PAD) and left-shifts (DROP) around a couple of U32add no-shift ops,
    // ending with the overflow table empty.
    // Overflow depth before each op (determines whether DROP emits):
    //   U32add:0 Pad:0→1 Pad:1→2 U32add:2 Drop:2→1 Pad:1→2 Drop:2→1 Drop:1→0 Drop:0 Pad:0→1
    // Drop:1→0 Four of the five DROPs run against a non-empty table and emit; the fourth DROP
    // sees overflow=0 and is a no-op. All four PADs emit.
    let ops = vec![
        Operation::U32add, // no shift
        Operation::Pad,    // right shift
        Operation::Pad,    // right shift
        Operation::U32add, // no shift
        Operation::Drop,   // left shift (overflow=2 → remove)
        Operation::Pad,    // right shift
        Operation::Drop,   // left shift (overflow=2 → remove)
        Operation::Drop,   // left shift (overflow=1 → remove)
        Operation::Drop,   // left shift (overflow=0 → no interaction)
        Operation::Pad,    // right shift
        Operation::Drop,   // left shift (overflow=1 → remove)
    ];
    let init_stack = (1..17).rev().collect::<Vec<u64>>();
    let trace = build_trace_from_ops(ops, &init_stack);
    let log = InteractionLog::new(&trace);
    let main = trace.main_trace();

    let mut exp = Expectations::new(&log);
    for row in 0..main.num_rows() {
        let idx = RowIndex::from(row);
        let next = RowIndex::from(row + 1);
        let op = main.get_op_code(idx);

        if op == Felt::from_u8(opcodes::PAD) {
            // Right shift: `add (clk, s15, b1)`.
            exp.add(
                row,
                &StackOverflowMsg {
                    clk: main.clk(idx),
                    val: main.stack_element(15, idx),
                    prev: main.parent_overflow_address(idx),
                },
            );
        } else if op == Felt::from_u8(opcodes::DROP) && main.is_non_empty_overflow(idx) {
            // Left shift with non-empty overflow: `remove (b1, s15', b1')`.
            exp.remove(
                row,
                &StackOverflowMsg {
                    clk: main.parent_overflow_address(idx),
                    val: main.stack_element(15, next),
                    prev: main.parent_overflow_address(next),
                },
            );
        }
    }

    // 4 PADs and 4 DROPs-with-non-empty-overflow (only the lone DROP on an empty overflow
    // table emits nothing).
    assert_eq!(exp.count_adds(), 4, "expected one add per PAD");
    assert_eq!(exp.count_removes(), 4, "expected one remove per DROP with non-empty overflow");
    log.assert_contains(&exp);
}