Skip to content

Commit

Permalink
fix: bug in chiplet bus (#1516)
Browse files Browse the repository at this point in the history
  • Loading branch information
Al-Kindi-0 authored Oct 1, 2024
1 parent f2b9161 commit 5085999
Show file tree
Hide file tree
Showing 7 changed files with 183 additions and 156 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
274 changes: 137 additions & 137 deletions miden/src/repl/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,141 +6,141 @@ use processor::ContextId;
use rustyline::{error::ReadlineError, DefaultEditor};
use stdlib::StdLibrary;

/// This work is in continuation to the amazing work done by team `Scribe`
/// [here](https://github.com/ControlCplusControlV/Scribe/blob/main/transpiler/src/repl.rs#L8)
///
/// The Miden Read–eval–print loop (REPL) is a Miden shell that allows for quick and easy debugging
/// of Miden assembly. To use the repl, simply type "miden repl" after building it with feature
/// "executable" (cargo build --release --feature executable) when in the miden home
/// crate and the repl will launch. After the REPL gets initialized, you can execute any Miden
/// instruction, undo executed instructions, check the state of the stack and memory at a given
/// point, and do many other useful things! When the REPL is exited, a `history.txt` file is saved.
/// One thing to note is that all the REPL native commands start with an `!` to differentiate them
/// from regular assembly instructions.
///
/// Miden Instructions
/// All Miden instructions mentioned in the
/// [Miden Assembly section](https://0xpolygonmiden.github.io/miden-vm/user_docs/assembly/main.html)
/// are valid.
/// One can either input instructions one by one or multiple instructions in one input.
/// For example, the below two commands will result in the same output.
/// >> push.1
/// >> push.2
/// >> push.3
///
/// >> push.1 push.2 push.3
///
/// In order to execute a control flow operation, one needs to write the entire flow operation in
/// a single line with spaces between individual operations.
/// Ex.
/// ```
/// repeat.20
/// pow2
/// end
/// ```
/// should be written as
/// `repeat.20 pow2 end`
///
/// To execute a control flow operation, one must write the entire statement in a single line with
/// spaces between individual operations.
/// ```
/// >> repeat.20
/// pow2
/// end
/// ```
///
/// The above example should be written as follows in the REPL tool:
/// >> repeat.20 pow2 end
///
/// `!stack`
/// The `!stack` command prints out the state of the stack at the last executed instruction. Since
/// the stack always contains at least 16 elements, 16 or more elements will be printed out (even
/// if all of them are zeros).
/// >> push.1 push.2 push.3 push.4 push.5
/// >> exp
/// >> u32wrapping_mul
/// >> swap
/// >> eq.2
/// >> assert
///
/// The `!stack` command will print out the following state of the stack:
/// ```
/// >> !stack
/// 3072 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
/// ```
///
/// `!undo`
/// The `!undo` command reverts to the previous state of the stack and memory by dropping off the
/// last executed assembly instruction from the program. One could use `!undo` as often as they want
/// to restore the state of a stack and memory $n$ instructions ago (provided there are $n$
/// instructions in the program). The `!undo` command will result in an error if no remaining
/// instructions are left in the miden program.
/// ```
/// >> push.1 push.2 push.3
/// >> push.4
/// >> !stack
/// 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0
/// >> push.5
/// >> !stack
/// 5 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0
/// >> !undo
/// 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0
/// >> !undo
/// 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0
/// ```
///
///`!program`
/// The `!program` command prints out the entire miden program getting executed. E.g., in the below
/// ```
/// scenario: >> push.1
/// >> push.2
/// >> push.3
/// >> add
/// >> add
/// >> !program
/// begin
/// push.1
/// push.2
/// push.3
/// add
/// add
/// end
/// ```
///
/// `!help`
/// The `!help` command prints out all the available commands in the REPL tool.
///
/// `!mem`
/// The `!mem` command prints out the contents of all initialized memory locations. For each such
/// location, the address, along with its memory values, is printed. Recall that four elements are
/// stored at each memory address.
/// If the memory has at least one value that has been initialized:
/// ```
/// >> !mem
/// 7: [1, 2, 0, 3]
/// 8: [5, 7, 3, 32]
/// 9: [9, 10, 2, 0]
/// ```
///
/// If the memory is not yet been initialized:
/// ```
/// >> !mem
/// The memory has not been initialized yet
/// ```
///
/// `!mem[addr]`
/// The `!mem[addr]` command prints out memory contents at the address specified by `addr`.
/// If the `addr` has been initialized:
/// ```
/// >> !mem[9]
/// 9: [9, 10, 2, 0]
/// ```
///
/// If the `addr` has not been initialized:
/// ```
/// >> !mem[87]
/// Memory at address 87 is empty
/// ```
// This work is in continuation to the amazing work done by team `Scribe`
// [here](https://github.com/ControlCplusControlV/Scribe/blob/main/transpiler/src/repl.rs#L8)
//
// The Miden Read–eval–print loop (REPL) is a Miden shell that allows for quick and easy debugging
// of Miden assembly. To use the repl, simply type "miden repl" after building it with feature
// "executable" (cargo build --release --feature executable) when in the miden home
// crate and the repl will launch. After the REPL gets initialized, you can execute any Miden
// instruction, undo executed instructions, check the state of the stack and memory at a given
// point, and do many other useful things! When the REPL is exited, a `history.txt` file is saved.
// One thing to note is that all the REPL native commands start with an `!` to differentiate them
// from regular assembly instructions.
//
// Miden Instructions
// All Miden instructions mentioned in the
// [Miden Assembly section](https://0xpolygonmiden.github.io/miden-vm/user_docs/assembly/main.html)
// are valid.
// One can either input instructions one by one or multiple instructions in one input.
// For example, the below two commands will result in the same output.
// >> push.1
// >> push.2
// >> push.3
//
// >> push.1 push.2 push.3
//
// In order to execute a control flow operation, one needs to write the entire flow operation in
// a single line with spaces between individual operations.
// Ex.
// ```
// repeat.20
// pow2
// end
// ```
// should be written as
// `repeat.20 pow2 end`
//
// To execute a control flow operation, one must write the entire statement in a single line with
// spaces between individual operations.
// ```
// >> repeat.20
// pow2
// end
// ```
//
// The above example should be written as follows in the REPL tool:
// >> repeat.20 pow2 end
//
// `!stack`
// The `!stack` command prints out the state of the stack at the last executed instruction. Since
// the stack always contains at least 16 elements, 16 or more elements will be printed out (even
// if all of them are zeros).
// >> push.1 push.2 push.3 push.4 push.5
// >> exp
// >> u32wrapping_mul
// >> swap
// >> eq.2
// >> assert
//
// The `!stack` command will print out the following state of the stack:
// ```
// >> !stack
// 3072 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
// ```
//
// `!undo`
// The `!undo` command reverts to the previous state of the stack and memory by dropping off the
// last executed assembly instruction from the program. One could use `!undo` as often as they want
// to restore the state of a stack and memory $n$ instructions ago (provided there are $n$
// instructions in the program). The `!undo` command will result in an error if no remaining
// instructions are left in the miden program.
// ```
// >> push.1 push.2 push.3
// >> push.4
// >> !stack
// 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0
// >> push.5
// >> !stack
// 5 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0
// >> !undo
// 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0
// >> !undo
// 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0
// ```
//
//`!program`
// The `!program` command prints out the entire miden program getting executed. E.g., in the below
// ```
// scenario: >> push.1
// >> push.2
// >> push.3
// >> add
// >> add
// >> !program
// begin
// push.1
// push.2
// push.3
// add
// add
// end
// ```
//
// `!help`
// The `!help` command prints out all the available commands in the REPL tool.
//
// `!mem`
// The `!mem` command prints out the contents of all initialized memory locations. For each such
// location, the address, along with its memory values, is printed. Recall that four elements are
// stored at each memory address.
// If the memory has at least one value that has been initialized:
// ```
// >> !mem
// 7: [1, 2, 0, 3]
// 8: [5, 7, 3, 32]
// 9: [9, 10, 2, 0]
// ```
//
// If the memory is not yet been initialized:
// ```
// >> !mem
// The memory has not been initialized yet
// ```
//
// `!mem[addr]`
// The `!mem[addr]` command prints out memory contents at the address specified by `addr`.
// If the `addr` has been initialized:
// ```
// >> !mem[9]
// 9: [9, 10, 2, 0]
// ```
//
// If the `addr` has not been initialized:
// ```
// >> !mem[87]
// Memory at address 87 is empty
// ```

/// Initiates the Miden Repl tool.
pub fn start_repl(library_paths: &Vec<PathBuf>, use_stdlib: bool) {
Expand Down Expand Up @@ -295,8 +295,8 @@ pub fn start_repl(library_paths: &Vec<PathBuf>, use_stdlib: bool) {
.expect("Couldn't dump the program into the history file");
}

/// HELPER METHODS
/// --------------------------------------------------------------------------------------------
// HELPER METHODS
// --------------------------------------------------------------------------------------------

/// Compiles and executes a compiled Miden program, returning the stack, memory and any Miden
/// errors. The program is passed in as a String, passed to the Miden Assembler, and then passed
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
Loading

0 comments on commit 5085999

Please sign in to comment.