Skip to content

Commit

Permalink
Merge branch 'next' of github.com:0xPolygonMiden/miden-vm into leviat…
Browse files Browse the repository at this point in the history
…hanbeak/migrate_to_clap_from_next
  • Loading branch information
leviathanbeak committed Aug 16, 2023
2 parents 820cb01 + 518ed44 commit 51ec1f6
Show file tree
Hide file tree
Showing 39 changed files with 2,274 additions and 668 deletions.
4 changes: 4 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,13 @@
- Added ability to attach doc comments to re-exported procedures (#994).
- Added support for nested modules (#992).
- Added support for the arithmetic expressions in constant values (#1026).
- Added support for module aliases (#1037).
- Added `adv.insert_hperm` decorator (#1042).

#### VM Internals
- Simplified range checker and removed 1 main and 1 auxiliary trace column (#949).
- Migrated range checker lookups to use LogUp and reduced the number of trace columns to 2 main and
1 auxiliary (#1027).
- Added `get_mapped_values()` and `get_store_subset()` methods to the `AdviceProvider` trait (#987).
- [BREAKING] Added options to specify maximum number of cycles and expected number of cycles for a program (#998).
- Improved handling of invalid/incomplete parameters in `StackOutputs` constructors (#1010).
Expand Down
29 changes: 0 additions & 29 deletions air/src/constraints/chiplets/memory/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -355,32 +355,3 @@ impl<E: FieldElement> EvaluationFrameExt<E> for &EvaluationFrame<E> {
self.selector_next(1)
}
}

// EXTERNAL ACCESSORS
// ================================================================================================
/// Trait to allow other processors to easily access the memory column values they need for
/// constraint calculations.
pub trait MemoryFrameExt<E: FieldElement> {
// --- Column accessors -----------------------------------------------------------------------

/// The value of the lower 16-bits of the delta value being tracked between two consecutive
/// context IDs, addresses, or clock cycles in the current row.
fn memory_d0(&self) -> E;
/// The value of the upper 16-bits of the delta value being tracked between two consecutive
/// context IDs, addresses, or clock cycles in the current row.
fn memory_d1(&self) -> E;
}

impl<E: FieldElement> MemoryFrameExt<E> for &EvaluationFrame<E> {
// --- Column accessors -----------------------------------------------------------------------

#[inline(always)]
fn memory_d0(&self) -> E {
self.current()[MEMORY_D0_COL_IDX]
}

#[inline(always)]
fn memory_d1(&self) -> E {
self.current()[MEMORY_D1_COL_IDX]
}
}
1 change: 0 additions & 1 deletion air/src/constraints/chiplets/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ use crate::utils::{are_equal, binary_not, is_binary};
mod bitwise;
mod hasher;
mod memory;
pub use memory::MemoryFrameExt;

// CONSTANTS
// ================================================================================================
Expand Down
103 changes: 103 additions & 0 deletions air/src/constraints/mod.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,106 @@
use super::{EvaluationFrame, ExtensionOf, Felt, FieldElement};
use crate::trace::{
chiplets::{MEMORY_D0_COL_IDX, MEMORY_D1_COL_IDX},
decoder::{DECODER_OP_BITS_OFFSET, DECODER_USER_OP_HELPERS_OFFSET},
};
use crate::utils::binary_not;

pub mod chiplets;
pub mod range;
pub mod stack;

// ACCESSORS
// ================================================================================================
/// Trait to allow other processors to easily access the column values they need for constraint
/// calculations.
pub trait MainFrameExt<F, E>
where
F: FieldElement<BaseField = Felt>,
E: FieldElement<BaseField = Felt> + ExtensionOf<F>,
{
/// Returns true when a u32 stack operation that requires range checks is being performed.
fn u32_rc_op(&self) -> F;

// --- Range check lookup accessors -----------------------------------------------------------------------

/// The value required for the first memory lookup when the memory chiplet requests range
/// checks. The value returned is the denominator used for including the value into the LogUp
/// lookup: (alpha - d0). The value d0 which is being range-checked is the lower 16-bits of the
/// delta value being tracked between two consecutive context IDs, addresses, or clock cycles in
/// the current row.
fn lookup_mv0(&self, alpha: E) -> E;
/// The value required for the second memory lookup when the memory chiplet requests range
/// checks. The value returned is the denominator used for including the value into the LogUp
/// lookup: (alpha - d1). The value d1 which is being range-checked is the upper 16-bits of the
/// delta value being tracked between two consecutive context IDs, addresses, or clock cycles in
/// the current row.
fn lookup_mv1(&self, alpha: E) -> E;
/// The value required for the first stack lookup when the stack requests range checks. The
/// value returned is the denominator used for including the value into the LogUp lookup:
/// (alpha - h0). The value h0 which is being range checked by the stack operation is stored in
/// the helper columns of the decoder section of the trace.
fn lookup_sv0(&self, alpha: E) -> E;
/// The value required for the second stack lookup when the stack requests range checks. The
/// value returned is the denominator used for including the value into the LogUp lookup:
/// (alpha - h1). The value h1 which is being range checked by the stack operation is stored in
/// the helper columns of the decoder section of the trace.
fn lookup_sv1(&self, alpha: E) -> E;
/// The value required for the third stack lookup when the stack requests range checks. The
/// value returned is the denominator used for including the value into the LogUp lookup:
/// (alpha - h2). The value h2 which is being range checked by the stack operation is stored in
/// the helper columns of the decoder section of the trace.
fn lookup_sv2(&self, alpha: E) -> E;
/// The value required for the fourth stack lookup when the stack requests range checks. The
/// value returned is the denominator used for including the value into the LogUp lookup:
/// (alpha - h3). The value h3 which is being range checked by the stack operation is stored in
/// the helper columns of the decoder section of the trace.
fn lookup_sv3(&self, alpha: E) -> E;
}

impl<F, E> MainFrameExt<F, E> for EvaluationFrame<F>
where
F: FieldElement<BaseField = Felt>,
E: FieldElement<BaseField = Felt> + ExtensionOf<F>,
{
/// Returns true when the stack operation is a u32 operation that requires range checks.
/// TODO: this is also defined in the op flags. It's redefined here to avoid computing all of
/// the op flags when this is the only one needed, but ideally this should only be defined once.
#[inline(always)]
fn u32_rc_op(&self) -> F {
let not_4 = binary_not(self.current()[DECODER_OP_BITS_OFFSET + 4]);
let not_5 = binary_not(self.current()[DECODER_OP_BITS_OFFSET + 5]);
self.current()[DECODER_OP_BITS_OFFSET + 6].mul(not_5).mul(not_4)
}

// --- Intermediate values for LogUp lookups --------------------------------------------------

#[inline(always)]
fn lookup_mv0(&self, alpha: E) -> E {
alpha - self.current()[MEMORY_D0_COL_IDX].into()
}

#[inline(always)]
fn lookup_mv1(&self, alpha: E) -> E {
alpha - self.current()[MEMORY_D1_COL_IDX].into()
}

#[inline(always)]
fn lookup_sv0(&self, alpha: E) -> E {
alpha - self.current()[DECODER_USER_OP_HELPERS_OFFSET].into()
}

#[inline(always)]
fn lookup_sv1(&self, alpha: E) -> E {
alpha - self.current()[DECODER_USER_OP_HELPERS_OFFSET + 1].into()
}

#[inline(always)]
fn lookup_sv2(&self, alpha: E) -> E {
alpha - self.current()[DECODER_USER_OP_HELPERS_OFFSET + 2].into()
}

#[inline(always)]
fn lookup_sv3(&self, alpha: E) -> E {
alpha - self.current()[DECODER_USER_OP_HELPERS_OFFSET + 3].into()
}
}
Loading

0 comments on commit 51ec1f6

Please sign in to comment.