use miden_air::{
RowIndex,
trace::chiplets::{
MEMORY_CLK_COL_IDX, MEMORY_CTX_COL_IDX, MEMORY_IDX0_COL_IDX, MEMORY_IDX1_COL_IDX,
MEMORY_IS_READ_COL_IDX, MEMORY_IS_WORD_ACCESS_COL_IDX, MEMORY_V_COL_RANGE,
MEMORY_WORD_COL_IDX,
memory::{
MEMORY_ACCESS_ELEMENT, MEMORY_ACCESS_WORD, MEMORY_READ, MEMORY_READ_ELEMENT_LABEL,
MEMORY_READ_WORD_LABEL, MEMORY_WRITE, MEMORY_WRITE_ELEMENT_LABEL,
MEMORY_WRITE_WORD_LABEL,
},
},
};
use miden_core::WORD_SIZE;
use super::{
AUX_TRACE_RAND_ELEMENTS, CHIPLETS_BUS_AUX_TRACE_OFFSET, ExecutionTrace, Felt, FieldElement,
NUM_RAND_ROWS, ONE, Operation, Trace, Word, ZERO, build_trace_from_ops, rand_array,
};
#[test]
#[allow(clippy::needless_range_loop)]
fn b_chip_trace_mem() {
const FOUR: Felt = Felt::new(4);
let stack = [1, 2, 3, 4, 0];
let word = [ONE, Felt::new(2), Felt::new(3), Felt::new(4)];
let operations = vec![
Operation::MStoreW, Operation::Drop, Operation::Drop,
Operation::Drop,
Operation::Drop,
Operation::MLoad, Operation::MovDn5, Operation::MLoadW, Operation::Push(ONE), Operation::Push(FOUR), Operation::MStore, Operation::Drop, Operation::MStream, ];
let trace = build_trace_from_ops(operations, &stack);
let rand_elements = rand_array::<Felt, AUX_TRACE_RAND_ELEMENTS>();
let aux_columns = trace.build_aux_trace(&rand_elements).unwrap();
let b_chip = aux_columns.get_column(CHIPLETS_BUS_AUX_TRACE_OFFSET);
assert_eq!(trace.length(), b_chip.len());
assert_eq!(ONE, b_chip[0]);
assert_eq!(ONE, b_chip[1]);
let value = build_expected_bus_word_msg(
&rand_elements,
MEMORY_WRITE_WORD_LABEL,
ZERO,
ZERO,
ONE,
word.into(),
);
let mut expected = value.inv();
assert_eq!(expected, b_chip[2]);
for row in 3..7 {
assert_eq!(expected, b_chip[row]);
}
let value = build_expected_bus_element_msg(
&rand_elements,
MEMORY_READ_ELEMENT_LABEL,
ZERO,
ZERO,
Felt::new(6),
word[0],
);
expected *= value.inv();
assert_eq!(expected, b_chip[7]);
assert_ne!(expected, b_chip[8]);
let span_result = b_chip[8] * b_chip[7].inv();
expected = b_chip[8];
let value = build_expected_bus_word_msg(
&rand_elements,
MEMORY_READ_WORD_LABEL,
ZERO,
ZERO,
Felt::new(8),
word.into(),
);
expected *= value.inv();
expected *= build_expected_bus_msg_from_trace(&trace, &rand_elements, 8.into());
assert_eq!(expected, b_chip[9]);
expected *= build_expected_bus_msg_from_trace(&trace, &rand_elements, 9.into());
assert_eq!(expected, b_chip[10]);
expected *= build_expected_bus_msg_from_trace(&trace, &rand_elements, 10.into());
assert_eq!(expected, b_chip[11]);
let value = build_expected_bus_element_msg(
&rand_elements,
MEMORY_WRITE_ELEMENT_LABEL,
ZERO,
FOUR,
Felt::new(11),
ONE,
);
expected *= value.inv();
expected *= build_expected_bus_msg_from_trace(&trace, &rand_elements, 11.into());
assert_eq!(expected, b_chip[12]);
expected *= build_expected_bus_msg_from_trace(&trace, &rand_elements, 12.into());
assert_eq!(expected, b_chip[13]);
let value1 = build_expected_bus_word_msg(
&rand_elements,
MEMORY_READ_WORD_LABEL,
ZERO,
ZERO,
Felt::new(13),
word.into(),
);
let value2 = build_expected_bus_word_msg(
&rand_elements,
MEMORY_READ_WORD_LABEL,
ZERO,
Felt::new(4),
Felt::new(13),
[ONE, ZERO, ZERO, ZERO].into(),
);
expected *= (value1 * value2).inv();
expected *= build_expected_bus_msg_from_trace(&trace, &rand_elements, 13.into());
assert_eq!(expected, b_chip[14]);
assert_ne!(expected, b_chip[15]);
expected *= span_result.inv();
assert_eq!(expected, b_chip[15]);
for row in 15..trace.length() - NUM_RAND_ROWS {
assert_eq!(ONE, b_chip[row]);
}
}
fn build_expected_bus_element_msg(
alphas: &[Felt],
op_label: u8,
ctx: Felt,
addr: Felt,
clk: Felt,
value: Felt,
) -> Felt {
assert!(op_label == MEMORY_READ_ELEMENT_LABEL || op_label == MEMORY_WRITE_ELEMENT_LABEL);
alphas[0]
+ alphas[1] * Felt::from(op_label)
+ alphas[2] * ctx
+ alphas[3] * addr
+ alphas[4] * clk
+ alphas[5] * value
}
fn build_expected_bus_word_msg(
alphas: &[Felt],
op_label: u8,
ctx: Felt,
addr: Felt,
clk: Felt,
word: Word,
) -> Felt {
assert!(op_label == MEMORY_READ_WORD_LABEL || op_label == MEMORY_WRITE_WORD_LABEL);
alphas[0]
+ alphas[1] * Felt::from(op_label)
+ alphas[2] * ctx
+ alphas[3] * addr
+ alphas[4] * clk
+ alphas[5] * word[0]
+ alphas[6] * word[1]
+ alphas[7] * word[2]
+ alphas[8] * word[3]
}
fn build_expected_bus_msg_from_trace(
trace: &ExecutionTrace,
alphas: &[Felt],
row: RowIndex,
) -> Felt {
let read_write = trace.main_trace.get_column(MEMORY_IS_READ_COL_IDX)[row];
let element_or_word = trace.main_trace.get_column(MEMORY_IS_WORD_ACCESS_COL_IDX)[row];
let op_label = if read_write == MEMORY_WRITE {
if element_or_word == MEMORY_ACCESS_ELEMENT {
MEMORY_WRITE_ELEMENT_LABEL
} else {
MEMORY_WRITE_WORD_LABEL
}
} else if read_write == MEMORY_READ {
if element_or_word == MEMORY_ACCESS_ELEMENT {
MEMORY_READ_ELEMENT_LABEL
} else {
MEMORY_READ_WORD_LABEL
}
} else {
panic!("invalid read_write value: {read_write}");
};
let ctx = trace.main_trace.get_column(MEMORY_CTX_COL_IDX)[row];
let addr = {
let word = trace.main_trace.get_column(MEMORY_WORD_COL_IDX)[row];
let idx1 = trace.main_trace.get_column(MEMORY_IDX1_COL_IDX)[row];
let idx0 = trace.main_trace.get_column(MEMORY_IDX0_COL_IDX)[row];
word + idx1.mul_small(2) + idx0
};
let clk = trace.main_trace.get_column(MEMORY_CLK_COL_IDX)[row];
let mut word = [ZERO; WORD_SIZE];
for (i, element) in word.iter_mut().enumerate() {
*element = trace.main_trace.get_column(MEMORY_V_COL_RANGE.start + i)[row];
}
if element_or_word == MEMORY_ACCESS_ELEMENT {
let idx1 = trace.main_trace.get_column(MEMORY_IDX1_COL_IDX)[row].as_int();
let idx0 = trace.main_trace.get_column(MEMORY_IDX0_COL_IDX)[row].as_int();
let idx = idx1 * 2 + idx0;
build_expected_bus_element_msg(alphas, op_label, ctx, addr, clk, word[idx as usize])
} else if element_or_word == MEMORY_ACCESS_WORD {
build_expected_bus_word_msg(alphas, op_label, ctx, addr, clk, word.into())
} else {
panic!("invalid element_or_word value: {element_or_word}");
}
}