Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix bug in chiplet bus #1516

Merged
merged 2 commits into from
Oct 1, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
Loading