Skip to content

Commit

Permalink
fix: bug in chiplet bus
Browse files Browse the repository at this point in the history
fix how `DYN` is handled

changelog
  • Loading branch information
Al-Kindi-0 committed Oct 1, 2024
1 parent 880d95a commit d7765ca
Show file tree
Hide file tree
Showing 6 changed files with 46 additions and 19 deletions.
1 change: 1 addition & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@
- Fixed the construction of the block hash table (#1506)
- Fixed a bug in the block stack table (#1511)
- Fixed the construction of the chiplets virtual table (#1514)
- Fixed the construction of the chiplets bus (#1516)

#### Fixes

Expand Down
46 changes: 36 additions & 10 deletions processor/src/chiplets/aux_trace/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@ use miden_air::{
use vm_core::{
Word, ONE, OPCODE_CALL, OPCODE_DYN, OPCODE_END, OPCODE_HPERM, OPCODE_JOIN, OPCODE_LOOP,
OPCODE_MLOAD, OPCODE_MLOADW, OPCODE_MPVERIFY, OPCODE_MRUPDATE, OPCODE_MSTORE, OPCODE_MSTOREW,
OPCODE_MSTREAM, OPCODE_RCOMBBASE, OPCODE_RESPAN, OPCODE_SPAN, OPCODE_SPLIT, OPCODE_SYSCALL,
OPCODE_U32AND, OPCODE_U32XOR, ZERO,
OPCODE_MSTREAM, OPCODE_PIPE, OPCODE_RCOMBBASE, OPCODE_RESPAN, OPCODE_SPAN, OPCODE_SPLIT,
OPCODE_SYSCALL, OPCODE_U32AND, OPCODE_U32XOR, ZERO,
};

use super::{super::trace::AuxColumnBuilder, Felt, FieldElement};
Expand Down Expand Up @@ -55,6 +55,7 @@ impl AuxTraceBuilder {
let b_chip = bus_col_builder.build_aux_column(main_trace, rand_elements);

debug_assert_eq!(*t_chip.last().unwrap(), E::ONE);
debug_assert_eq!(*b_chip.last().unwrap(), E::ONE);
vec![t_chip, b_chip]
}
}
Expand Down Expand Up @@ -258,6 +259,7 @@ impl<E: FieldElement<BaseField = Felt>> AuxColumnBuilder<E> for BusColumnBuilder
OPCODE_HPERM => build_hperm_request(main_trace, alphas, row),
OPCODE_MPVERIFY => build_mpverify_request(main_trace, alphas, row),
OPCODE_MRUPDATE => build_mrupdate_request(main_trace, alphas, row),
OPCODE_PIPE => build_pipe_request(main_trace, alphas, row),
_ => E::ONE,
}
}
Expand Down Expand Up @@ -340,7 +342,6 @@ fn build_span_block_request<E: FieldElement<BaseField = Felt>>(
alphas[0] + alphas[1].mul_base(Felt::from(transition_label)) + alphas[2].mul_base(addr_nxt);

let state = main_trace.decoder_hasher_state(row);

header + build_value(&alphas[8..16], &state)
}

Expand All @@ -361,10 +362,9 @@ fn build_respan_block_request<E: FieldElement<BaseField = Felt>>(
+ alphas[2].mul_base(addr_nxt - ONE)
+ alphas[3].mul_base(ZERO);

let state = &main_trace.chiplet_hasher_state(row - 2)[CAPACITY_LEN..];
let state_nxt = &main_trace.chiplet_hasher_state(row - 1)[CAPACITY_LEN..];
let state = main_trace.decoder_hasher_state(row);

header + build_value(&alphas[8..16], state_nxt) - build_value(&alphas[8..16], state)
header + build_value(&alphas[8..16], &state)
}

/// Builds requests made to the hasher chiplet at the end of a block.
Expand Down Expand Up @@ -471,6 +471,33 @@ fn build_mstream_request<E: FieldElement<BaseField = Felt>>(
factor1 * factor2
}

/// Builds `PIPE` requests made to the memory chiplet.
fn build_pipe_request<E: FieldElement<BaseField = Felt>>(
main_trace: &MainTrace,
alphas: &[E],
row: RowIndex,
) -> E {
let word1 = [
main_trace.stack_element(7, row + 1),
main_trace.stack_element(6, row + 1),
main_trace.stack_element(5, row + 1),
main_trace.stack_element(4, row + 1),
];
let word2 = [
main_trace.stack_element(3, row + 1),
main_trace.stack_element(2, row + 1),
main_trace.stack_element(1, row + 1),
main_trace.stack_element(0, row + 1),
];
let addr = main_trace.stack_element(12, row);
let op_label = MEMORY_WRITE_LABEL;

let factor1 = compute_memory_request(main_trace, op_label, alphas, row, addr, word1);
let factor2 = compute_memory_request(main_trace, op_label, alphas, row, addr + ONE, word2);

factor1 * factor2
}

/// Builds `RCOMBBASE` requests made to the memory chiplet.
fn build_rcomb_base_request<E: FieldElement<BaseField = Felt>>(
main_trace: &MainTrace,
Expand Down Expand Up @@ -827,13 +854,12 @@ where

let state_nxt = main_trace.chiplet_hasher_state(row + 1);

// build the value from the difference of the hasher state's just before and right
// after the absorption of new elements.
// build the value from the hasher state's just right after the absorption of new
// elements.
let next_state_value =
build_value(&alphas_state[CAPACITY_LEN..], &state_nxt[CAPACITY_LEN..]);
let state_value = build_value(&alphas_state[CAPACITY_LEN..], &state[CAPACITY_LEN..]);

multiplicand = header + next_state_value - state_value;
multiplicand = header + next_state_value;
}
}
multiplicand
Expand Down
8 changes: 4 additions & 4 deletions processor/src/decoder/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -292,15 +292,15 @@ where
// --------------------------------------------------------------------------------------------

/// Starts decoding of a DYN node.
pub(super) fn start_dyn_node(&mut self, callee_hash: Word) -> Result<(), ExecutionError> {
pub(super) fn start_dyn_node(&mut self) -> Result<(), ExecutionError> {
let addr = self.chiplets.hash_control_block(
EMPTY_WORD,
EMPTY_WORD,
DynNode::DOMAIN,
DynNode::default().digest(),
);

self.decoder.start_dyn(callee_hash, addr);
self.decoder.start_dyn(addr);
self.execute_op(Operation::Noop)
}

Expand Down Expand Up @@ -534,10 +534,10 @@ impl Decoder {
///
/// This pushes a block with ID=addr onto the block stack and appends execution of a DYN
/// operation to the trace.
pub fn start_dyn(&mut self, dyn_hash: Word, addr: Felt) {
pub fn start_dyn(&mut self, addr: Felt) {
// push DYN block info onto the block stack and append a DYN row to the execution trace
let parent_addr = self.block_stack.push(addr, BlockType::Dyn, None);
self.trace.append_block_start(parent_addr, Operation::Dyn, dyn_hash, [ZERO; 4]);
self.trace.append_block_start(parent_addr, Operation::Dyn, [ZERO; 4], [ZERO; 4]);

self.debug_info.append_operation(Operation::Dyn);
}
Expand Down
4 changes: 2 additions & 2 deletions processor/src/decoder/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1277,9 +1277,9 @@ fn dyn_block() {
assert_eq!(join_hash, get_hasher_state1(&trace, 8));
assert_eq!([ZERO, ZERO, ZERO, ZERO], get_hasher_state2(&trace, 8));

// at the start of the DYN block, the hasher state is set to the hash of its child (foo span)
// at the start of the DYN block, the hasher state is set to ZERO
let foo_hash: Word = foo_root_node.digest().into();
assert_eq!(foo_hash, get_hasher_state1(&trace, 9));
assert_eq!([ZERO, ZERO, ZERO, ZERO], get_hasher_state1(&trace, 9));
assert_eq!([ZERO, ZERO, ZERO, ZERO], get_hasher_state2(&trace, 9));

// at the end of the DYN SPAN, the hasher state is set to the hash of the foo span
Expand Down
3 changes: 2 additions & 1 deletion processor/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -410,9 +410,10 @@ where
/// expected to be either in the current `program` or in the host.
#[inline(always)]
fn execute_dyn_node(&mut self, program: &MastForest) -> Result<(), ExecutionError> {
self.start_dyn_node()?;

// get target hash from the stack
let callee_hash = self.stack.get_word(0);
self.start_dyn_node(callee_hash)?;

// if the callee is not in the program's MAST forest, try to find a MAST forest for it in
// the host (corresponding to an external library loaded in the host); if none are
Expand Down
3 changes: 1 addition & 2 deletions processor/src/trace/tests/chiplets/hasher.rs
Original file line number Diff line number Diff line change
Expand Up @@ -810,9 +810,8 @@ fn build_expected(
// include the entire state (words a, b, c)
value += build_value(&alphas[4..16], &state);
} else if label == LINEAR_HASH_LABEL {
// include the delta between the next and current rate elements (words b and c)
// include the next rate elements
value += build_value(&alphas[8..16], &next_state[CAPACITY_LEN..]);
value -= build_value(&alphas[8..16], &state[CAPACITY_LEN..]);
} else if label == RETURN_HASH_LABEL {
// include the digest (word b)
value += build_value(&alphas[8..12], &state[DIGEST_RANGE]);
Expand Down

0 comments on commit d7765ca

Please sign in to comment.