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

Implement element-addressable memory #1598

Open
wants to merge 8 commits into
base: next
Choose a base branch
from
Open
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
3 changes: 3 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
# Changelog

#### Highlights
- [BREAKING] Memory is now memory addressable (#1598)

#### Changes
- [BREAKING] `Process` no longer takes ownership of the `Host` (#1571).
- [BREAKING] `ProcessState` was converted from a trait to a struct (#1571).
Expand Down
271 changes: 162 additions & 109 deletions air/src/constraints/chiplets/memory/mod.rs

Large diffs are not rendered by default.

109 changes: 59 additions & 50 deletions air/src/constraints/chiplets/memory/tests.rs
Original file line number Diff line number Diff line change
@@ -1,59 +1,49 @@
use alloc::vec::Vec;

use rand_utils::rand_value;
use vm_core::{Felt, FieldElement, WORD_SIZE};

use super::{
EvaluationFrame, MEMORY_ADDR_COL_IDX, MEMORY_CLK_COL_IDX, MEMORY_CTX_COL_IDX,
MEMORY_D0_COL_IDX, MEMORY_D1_COL_IDX, MEMORY_D_INV_COL_IDX, MEMORY_V_COL_RANGE, NUM_ELEMENTS,
EvaluationFrame, MEMORY_BATCH_COL_IDX, MEMORY_CLK_COL_IDX, MEMORY_CTX_COL_IDX,
MEMORY_D0_COL_IDX, MEMORY_D1_COL_IDX, MEMORY_D_INV_COL_IDX, MEMORY_V_COL_RANGE,
};
use crate::{
chiplets::memory,
trace::{
chiplets::{
memory::{Selectors, MEMORY_COPY_READ, MEMORY_INIT_READ, MEMORY_WRITE},
MEMORY_TRACE_OFFSET,
memory::{MEMORY_ACCESS_WORD, MEMORY_READ, MEMORY_WRITE},
MEMORY_ELEMENT_OR_WORD_COL_IDX, MEMORY_FLAG_SAME_BATCH_AND_CONTEXT,
MEMORY_IDX0_COL_IDX, MEMORY_IDX1_COL_IDX, MEMORY_READ_WRITE_COL_IDX,
},
TRACE_WIDTH,
},
Felt, FieldElement, ONE, ZERO,
ONE, ZERO,
};

// UNIT TESTS
// ================================================================================================

#[test]
fn test_memory_write() {
let expected = [ZERO; memory::NUM_CONSTRAINTS];
let expected_constraint_evals = [ZERO; memory::NUM_CONSTRAINTS];

let old_values = vec![0, 0, 0, 0];
let new_values = vec![1, 0, 0, 0];
let old_word = vec![0, 0, 0, 0];
let new_word = vec![1, 0, 0, 0];

// Write to a new context.
let result = get_constraint_evaluation(
MEMORY_WRITE,
MemoryTestDeltaType::Context,
&old_values,
&new_values,
);
assert_eq!(expected, result);
let result =
get_constraint_evaluation(MEMORY_WRITE, MemoryTestDeltaType::Context, &old_word, &new_word);
assert_eq!(expected_constraint_evals, result);

// Write to a new address in the same context.
let result = get_constraint_evaluation(
MEMORY_WRITE,
MemoryTestDeltaType::Address,
&old_values,
&new_values,
);
assert_eq!(expected, result);
let result =
get_constraint_evaluation(MEMORY_WRITE, MemoryTestDeltaType::Batch, &old_word, &new_word);
assert_eq!(expected_constraint_evals, result);

// Write to the same context and address at a new clock cycle.
let result = get_constraint_evaluation(
MEMORY_WRITE,
MemoryTestDeltaType::Clock,
&old_values,
&new_values,
);
assert_eq!(expected, result);
let result =
get_constraint_evaluation(MEMORY_WRITE, MemoryTestDeltaType::Clock, &old_word, &new_word);
assert_eq!(expected_constraint_evals, result);
}

#[test]
Expand All @@ -65,7 +55,7 @@ fn test_memory_read() {

// Read from a new context.
let result = get_constraint_evaluation(
MEMORY_INIT_READ,
MEMORY_READ,
MemoryTestDeltaType::Context,
&old_values,
&init_values,
Expand All @@ -74,16 +64,16 @@ fn test_memory_read() {

// Read from a new address in the same context.
let result = get_constraint_evaluation(
MEMORY_INIT_READ,
MemoryTestDeltaType::Address,
MEMORY_READ,
MemoryTestDeltaType::Batch,
&old_values,
&init_values,
);
assert_eq!(expected, result);

// Read from the same context and address at a new clock cycle.
let result = get_constraint_evaluation(
MEMORY_COPY_READ,
MEMORY_READ,
MemoryTestDeltaType::Clock,
&old_values,
&old_values,
Expand All @@ -100,7 +90,7 @@ fn test_memory_read() {
/// - Clock: when the delta occurs in the clock column, context and address must stay fixed.
enum MemoryTestDeltaType {
Context,
Address,
Batch,
Clock,
}

Expand All @@ -113,17 +103,17 @@ enum MemoryTestDeltaType {
/// - To test a valid read, the `delta_type` must be Clock and the `old_values` and `new_values`
/// must be equal.
fn get_constraint_evaluation(
selectors: Selectors,
read_write: Felt,
delta_type: MemoryTestDeltaType,
old_values: &[u32],
new_values: &[u32],
) -> [Felt; memory::NUM_CONSTRAINTS] {
let delta_row = get_test_delta_row(&delta_type);
let frame = get_test_frame(selectors, &delta_type, &delta_row, old_values, new_values);
let frame = get_test_frame(read_write, &delta_type, &delta_row, old_values, new_values);

let mut result = [ZERO; memory::NUM_CONSTRAINTS];

memory::enforce_constraints(&frame, &mut result, ONE);
memory::enforce_constraints(&frame, &mut result, ONE, ONE, ZERO);

result
}
Expand All @@ -141,7 +131,7 @@ fn get_constraint_evaluation(
/// row.
/// - `new_values`: specifies the new values, which are placed in the value columns of the next row.
fn get_test_frame(
selectors: Selectors,
read_write: Felt,
delta_type: &MemoryTestDeltaType,
delta_row: &[u64],
old_values: &[u32],
Expand All @@ -151,16 +141,16 @@ fn get_test_frame(
let mut next = vec![ZERO; TRACE_WIDTH];

// Set the operation in the next row.
next[MEMORY_TRACE_OFFSET] = selectors[0];
next[MEMORY_TRACE_OFFSET + 1] = selectors[1];
next[MEMORY_READ_WRITE_COL_IDX] = read_write;
next[MEMORY_ELEMENT_OR_WORD_COL_IDX] = MEMORY_ACCESS_WORD;

// Set the context, addr, and clock columns in the next row to the values in the delta row.
next[MEMORY_CTX_COL_IDX] = Felt::new(delta_row[0]);
next[MEMORY_ADDR_COL_IDX] = Felt::new(delta_row[1]);
next[MEMORY_BATCH_COL_IDX] = Felt::new(delta_row[1]);
next[MEMORY_CLK_COL_IDX] = Felt::new(delta_row[2]);

// Set the old and new values.
for idx in 0..NUM_ELEMENTS {
for idx in 0..WORD_SIZE {
let old_value = Felt::new(old_values[idx] as u64);
// Add a write for the old values to the current row.
current[MEMORY_V_COL_RANGE.start + idx] = old_value;
Expand All @@ -177,27 +167,40 @@ fn get_test_frame(
let delta: u64 = match delta_type {
MemoryTestDeltaType::Clock => delta_row[MemoryTestDeltaType::Clock as usize] - 1,
MemoryTestDeltaType::Context => delta_row[MemoryTestDeltaType::Context as usize],
MemoryTestDeltaType::Address => delta_row[MemoryTestDeltaType::Address as usize],
MemoryTestDeltaType::Batch => delta_row[MemoryTestDeltaType::Batch as usize],
};
next[MEMORY_D0_COL_IDX] = Felt::new(delta as u16 as u64);
next[MEMORY_D1_COL_IDX] = Felt::new(delta >> 16);
next[MEMORY_D_INV_COL_IDX] = (Felt::new(delta)).inv();

// since we're always writing a word, the idx0 and idx1 columns should be zero
next[MEMORY_IDX0_COL_IDX] = ZERO;
next[MEMORY_IDX1_COL_IDX] = ZERO;

// If the context or batch columns are changed, the same batch and context flag should be zero.
if delta_row[MemoryTestDeltaType::Batch as usize] > 0
|| delta_row[MemoryTestDeltaType::Context as usize] > 0
{
next[MEMORY_FLAG_SAME_BATCH_AND_CONTEXT] = ZERO;
} else {
next[MEMORY_FLAG_SAME_BATCH_AND_CONTEXT] = ONE;
}

EvaluationFrame::<Felt>::from_rows(current, next)
}

/// Generates a row of valid test values for the context, address, and clock columns according to
/// Generates a row of valid test values for the context, batch, and clock columns according to
/// the specified delta type, which determines the column over which the delta and delta inverse
/// values of the trace would be calculated.
///
/// - When the delta type is Context, the address and clock columns can be anything.
/// - When the delta type is Address, the context must remain unchanged but the clock can change.
/// - When the delta type is Batch, the context must remain unchanged but the clock can change.
/// - When the delta type is Clock, both the context and address columns must remain unchanged.
fn get_test_delta_row(delta_type: &MemoryTestDeltaType) -> Vec<u64> {
let delta_value = rand_value::<u32>() as u64;
let delta_value = word_aligned_rand_value() as u64;
let mut row = vec![0; 3];
let ctx_idx = MemoryTestDeltaType::Context as usize;
let addr_idx = MemoryTestDeltaType::Address as usize;
let batch_idx = MemoryTestDeltaType::Batch as usize;
let clk_idx = MemoryTestDeltaType::Clock as usize;

// Set the context, addr, and clock columns according to the specified delta type.
Expand All @@ -207,13 +210,13 @@ fn get_test_delta_row(delta_type: &MemoryTestDeltaType) -> Vec<u64> {
row[ctx_idx] = delta_value;

// Set addr and clock in the row column to random values.
row[addr_idx] = rand_value::<u32>() as u64;
row[batch_idx] = word_aligned_rand_value() as u64;
row[clk_idx] = rand_value::<u32>() as u64;
},
MemoryTestDeltaType::Address => {
MemoryTestDeltaType::Batch => {
// Keep the context value the same in current and row rows (leave it as ZERO).
// Set the row value for the address.
row[addr_idx] = delta_value;
row[batch_idx] = delta_value;

// Set clock in the row column to a random value.
row[clk_idx] = rand_value::<u32>() as u64;
Expand All @@ -227,3 +230,9 @@ fn get_test_delta_row(delta_type: &MemoryTestDeltaType) -> Vec<u64> {

row
}

/// Returns a random value that is aligned to a word boundary (i.e. divisible by 4).
fn word_aligned_rand_value() -> u32 {
let value = rand_value::<u32>();
value - (value % 4)
}
52 changes: 39 additions & 13 deletions air/src/constraints/chiplets/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -86,8 +86,15 @@ pub fn enforce_constraints<E: FieldElement<BaseField = Felt>>(
);
constraint_offset += bitwise::get_transition_constraint_count();

// TODO(plafer): refactor
// memory transition constraints
memory::enforce_constraints(frame, &mut result[constraint_offset..], frame.memory_flag(false));
memory::enforce_constraints(
frame,
&mut result[constraint_offset..],
frame.memory_flag(),
frame.memory_flag_no_last(),
frame.memory_flag_first_row(),
);
}

// TRANSITION CONSTRAINT HELPERS
Expand Down Expand Up @@ -144,11 +151,19 @@ trait EvaluationFrameExt<E: FieldElement> {
fn bitwise_flag(&self) -> E;

/// Flag to indicate whether the frame is in the memory portion of the Chiplets trace.
/// When `include_last_row` is true, the memory flag is true for every row where the memory
/// selectors are set. When false, the last row is excluded. When this flag is used for
/// transition constraints with `include_last_row = false`, they will not be applied to the
/// final row of the memory trace.
fn memory_flag(&self, include_last_row: bool) -> E;
fn memory_flag(&self) -> E;

/// Flag to indicate whether the frame is in the memory portion of the Chiplets trace, except
/// for the last memory chiplet row.
fn memory_flag_no_last(&self) -> E;

/// Flag to indicate whether the next row in the frame is in the memory portion of the Chiplets
/// trace.
fn memory_flag_next(&self) -> E;

/// Flag to indicate whether the frame is in the first row of the memory portion of the Chiplets
/// trace.
fn memory_flag_first_row(&self) -> E;
}

impl<E: FieldElement> EvaluationFrameExt<E> for &EvaluationFrame<E> {
Expand All @@ -175,12 +190,23 @@ impl<E: FieldElement> EvaluationFrameExt<E> for &EvaluationFrame<E> {
}

#[inline(always)]
fn memory_flag(&self, include_last_row: bool) -> E {
if include_last_row {
self.s(0) * self.s(1) * binary_not(self.s(2))
} else {
self.s(0) * self.s(1) * binary_not(self.s_next(2))
}
fn memory_flag(&self) -> E {
self.s(0) * self.s(1) * binary_not(self.s(2))
}

#[inline(always)]
fn memory_flag_no_last(&self) -> E {
self.s(0) * self.s(1) * binary_not(self.s_next(2))
}

#[inline(always)]
fn memory_flag_next(&self) -> E {
self.s_next(0) * self.s_next(1) * binary_not(self.s_next(2))
}

#[inline(always)]
fn memory_flag_first_row(&self) -> E {
self.hasher_flag() * self.memory_flag_next()
}
}

Expand All @@ -196,6 +222,6 @@ pub trait ChipletsFrameExt<E: FieldElement> {
impl<E: FieldElement> ChipletsFrameExt<E> for &EvaluationFrame<E> {
#[inline(always)]
fn chiplets_memory_flag(&self) -> E {
self.memory_flag(true)
self.memory_flag()
}
}
Loading
Loading