Skip to content

Commit

Permalink
Merge branch 'main' into next
Browse files Browse the repository at this point in the history
  • Loading branch information
bobbinth authored Sep 13, 2024
2 parents 492ce81 + fbce798 commit 19b5643
Show file tree
Hide file tree
Showing 10 changed files with 173 additions and 42 deletions.
8 changes: 8 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,14 @@

- Decorators are now allowed in empty basic blocks (#1466)


## 0.10.6 (2024-09-12) - `miden-processor` crate only.

#### Enhancements

- Added `PartialEq`, `Eq`, `Serialize` and `Deserialize` to `AdviceMap` and `AdviceInputs` structs (#1494).


## 0.10.5 (2024-08-21)

#### Enhancements
Expand Down
2 changes: 1 addition & 1 deletion Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

67 changes: 44 additions & 23 deletions air/src/constraints/stack/field_ops/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -99,8 +99,10 @@ pub fn enforce_constraints<E: FieldElement>(
// TRANSITION CONSTRAINT HELPERS
// ================================================================================================

/// Enforces constraints of the ADD operation. The ADD operation adds the first two elements
/// in the current trace. Therefore, the following constraints are enforced:
/// Enforces constraints of the ADD operation.
///
/// The ADD operation adds the first two elements in the current trace. Therefore, the following
/// constraints are enforced:
/// - The first element in the trace frame should be the addition of the first two elements in the
/// current trace. s0` - s0 - s1 = 0.
pub fn enforce_add_constraints<E: FieldElement>(
Expand All @@ -118,8 +120,10 @@ pub fn enforce_add_constraints<E: FieldElement>(
1
}

/// Enforces constraints of the NEG operation. The NEG operation updates the top element in the
/// stack with its inverse. Therefore, the following constraints are enforced:
/// Enforces constraints of the NEG operation.
///
/// The NEG operation updates the top element in the stack with its inverse. Therefore, the
/// following constraints are enforced:
/// - The first element in the next frame should be the negation of first element in the current
/// frame, therefore, their sum should be 0. s0` + s0 = 0.
pub fn enforce_neg_constraints<E: FieldElement>(
Expand All @@ -134,8 +138,10 @@ pub fn enforce_neg_constraints<E: FieldElement>(
1
}

/// Enforces constraints of the MUL operation. The MUL operation multiplies the first two elements
/// in the current trace. Therefore, the following constraints are enforced:
/// Enforces constraints of the MUL operation.
///
/// The MUL operation multiplies the first two elements in the current trace. Therefore, the
/// following constraints are enforced:
/// - The first element in the next frame should be the product of the first two elements in the
/// current frame. s0` - s0 * s1 = 0
pub fn enforce_mul_constraints<E: FieldElement>(
Expand All @@ -153,8 +159,10 @@ pub fn enforce_mul_constraints<E: FieldElement>(
1
}

/// Enforces constraints of the INV operation. The INV operation updates the top element
/// in the stack with its inverse. Therefore, the following constraints are enforced:
/// Enforces constraints of the INV operation.
///
/// The INV operation updates the top element in the stack with its inverse. Therefore, the
/// following constraints are enforced:
/// - The next element in the next frame should be the inverse of first element in the current
/// frame. s0` * s0 = 1.
pub fn enforce_inv_constraints<E: FieldElement>(
Expand All @@ -169,8 +177,10 @@ pub fn enforce_inv_constraints<E: FieldElement>(
1
}

/// Enforces constraints of the INCR operation. The INCR operation increments the
/// top element in the stack by 1. Therefore, the following constraints are enforced:
/// Enforces constraints of the INCR operation.
///
/// The INCR operation increments the top element in the stack by 1. Therefore, the following
/// constraints are enforced:
/// - The next element in the next frame should be equal to the addition of first element in the
/// current frame with 1. s0` - s0 - 1 = 0.
pub fn enforce_incr_constraints<E: FieldElement>(
Expand All @@ -184,9 +194,10 @@ pub fn enforce_incr_constraints<E: FieldElement>(
1
}

/// Enforces constraints of the NOT operation. The NOT operation updates the top element
/// in the stack with its bitwise not value. Therefore, the following constraints are
/// enforced:
/// Enforces constraints of the NOT operation.
///
/// The NOT operation updates the top element in the stack with its bitwise not value. Therefore,
/// the following constraints are enforced:
/// - The top element should be a binary. It is enforced as a general constraint.
/// - The first element of the next frame should be a binary not of the first element of the current
/// frame. s0` + s0 = 1.
Expand All @@ -205,8 +216,10 @@ pub fn enforce_not_constraints<E: FieldElement>(
1
}

/// Enforces constraints of the AND operation. The AND operation computes the bitwise and of the
/// first two elements in the current trace. Therefore, the following constraints are enforced:
/// Enforces constraints of the AND operation.
///
/// The AND operation computes the bitwise and of the first two elements in the current trace.
/// Therefore, the following constraints are enforced:
/// - The top two element in the current frame of the stack should be binary. s0^2 - s0 = 0, s1^2 -
/// s1 = 0. The top element is binary or not is enforced as a general constraint.
/// - The first element of the next frame should be a binary and of the first two elements in the
Expand All @@ -232,8 +245,10 @@ pub fn enforce_and_constraints<E: FieldElement>(
2
}

/// Enforces constraints of the OR operation. The OR operation computes the bitwise or of the
/// first two elements in the current trace. Therefore, the following constraints are enforced:
/// Enforces constraints of the OR operation.
///
/// The OR operation computes the bitwise or of the first two elements in the current trace.
/// Therefore, the following constraints are enforced:
/// - The top two element in the current frame of the stack should be binary. s0^2 - s0 = 0, s1^2 -
/// s1 = 0. The top element is binary or not is enforced as a general constraint.
/// - The first element of the next frame should be a binary or of the first two elements in the
Expand All @@ -259,8 +274,10 @@ pub fn enforce_or_constraints<E: FieldElement>(
2
}

/// Enforces constraints of the EQ operation. The EQ operation checks if the top two elements in the
/// current frame are equal or not. Therefore, the following constraints are enforced:
/// Enforces constraints of the EQ operation.
///
/// The EQ operation checks if the top two elements in the current frame are equal or not.
/// Therefore, the following constraints are enforced:
/// - (s0 - s1) * s0' = 0
/// - s0` - (1 - (s0 - s1) * h0) = 0
pub fn enforce_eq_constraints<E: FieldElement>(
Expand Down Expand Up @@ -291,8 +308,10 @@ pub fn enforce_eq_constraints<E: FieldElement>(
2
}

/// Enforces constraints of the EQZ operation. The EQZ operation checks if the top element in the
/// current frame is 0 or not. Therefore, the following constraints are enforced:
/// Enforces constraints of the EQZ operation.
///
/// The EQZ operation checks if the top element in the current frame is 0 or not. Therefore, the
/// following constraints are enforced:
/// - s0 * s0` = 0.
/// - s0` - (1 - h0 * s0) = 0.
pub fn enforce_eqz_constraints<E: FieldElement>(
Expand All @@ -319,8 +338,10 @@ pub fn enforce_eqz_constraints<E: FieldElement>(
2
}

/// Enforces constraints of the EXPACC operation. The EXPACC operation computes a single turn of
/// exponent accumulation for the given inputs. Therefore, the following constraints are enforced:
/// Enforces constraints of the EXPACC operation.
///
/// The EXPACC operation computes a single turn of exponent accumulation for the given inputs.
/// Therefore, the following constraints are enforced:
/// - The first element in the next frame should be a binary which is enforced as a general
/// constraint.
/// - The exp value in the next frame should be the square of exp value in the current frame.
Expand Down
12 changes: 8 additions & 4 deletions air/src/constraints/stack/stack_manipulation/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,8 +77,10 @@ pub fn enforce_constraints<E: FieldElement>(
// TRANSITION CONSTRAINT HELPERS
// ================================================================================================

/// Enforces constraints of the PAD operation. The PAD operation pushes a ZERO onto
/// the stack. Therefore, the following constraints are enforced:
/// Enforces constraints of the PAD operation.
///
/// The PAD operation pushes a ZERO onto the stack. Therefore, the following constraints are
/// enforced:
/// - The top element in the next frame should be ZERO. s0` = 0.
pub fn enforce_pad_constraints<E: FieldElement>(
frame: &EvaluationFrame<E>,
Expand Down Expand Up @@ -166,8 +168,10 @@ pub fn enforce_dup_movup_n_constraints<E: FieldElement>(
13
}

/// Enforces constraints of the SWAP operation. The SWAP operation swaps the first
/// two elements in the stack. Therefore, the following constraints are enforced:
/// Enforces constraints of the SWAP operation.
///
/// The SWAP operation swaps the first two elements in the stack. Therefore, the following
/// constraints are enforced:
/// - The first element in the current frame should be equal to the second element in the next
/// frame.
/// - The second element in the current frame should be equal to the first element in the next
Expand Down
12 changes: 8 additions & 4 deletions air/src/constraints/stack/system_ops/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -74,8 +74,10 @@ pub fn enforce_assert_constraints<E: FieldElement>(
1
}

/// Enforces unique constraints of the FMPADD operation. The FMPADD operation increments the top
/// element in the stack by `fmp` register value. Therefore, the following constraints are enforced:
/// Enforces unique constraints of the FMPADD operation.
///
/// The FMPADD operation increments the top element in the stack by `fmp` register value. Therefore,
/// the following constraints are enforced:
/// - The first element in the next frame should be equal to the addition of the first element in
/// the current frame and the fmp value. s0` - (s0 + fmp) = 0
pub fn enforce_fmpadd_constraints<E: FieldElement>(
Expand Down Expand Up @@ -106,8 +108,10 @@ pub fn enforce_fmpupdate_constraints<E: FieldElement>(
1
}

/// Enforces constraints of the CLK operation. The CLK operation pushes the current cycle number to
/// the stack. Therefore, the following constraints are enforced:
/// Enforces constraints of the CLK operation.
///
/// The CLK operation pushes the current cycle number to the stack. Therefore, the following
/// constraints are enforced:
/// - The first element in the next frame should be equal to the current cycle number. s0' - (cycle)
/// = 0.
pub fn enforce_clk_constraints<E: FieldElement>(
Expand Down
5 changes: 2 additions & 3 deletions air/src/trace/chiplets/kernel_rom.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ pub const TRACE_WIDTH: usize = 6;

/// Specifies a kernel procedure call operation to access a procedure in the kernel ROM.
///
/// The unique operation label is computed as 1 plus the combined chiplet and internal selector with
/// the bits reversed.
/// - kernel ROM selector=[1, 1, 1, 0] +1=[0, 0, 0, 1]
/// The unique operation label is computed as 1 plus the combined chiplet and internal selector
/// with the bits reversed: kernel ROM selector=[1, 1, 1, 0] +1=[0, 0, 0, 1].
pub const KERNEL_PROC_LABEL: Felt = Felt::new(0b1000);
4 changes: 2 additions & 2 deletions processor/Cargo.toml
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
[package]
name = "miden-processor"
version = "0.10.5"
version = "0.10.6"
description = "Miden VM processor"
documentation = "https://docs.rs/miden-processor/0.10.5"
documentation = "https://docs.rs/miden-processor/0.10.6"
readme = "README.md"
categories = ["emulators", "no-std"]
keywords = ["miden", "virtual-machine"]
Expand Down
59 changes: 56 additions & 3 deletions processor/src/host/advice/inputs.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
use alloc::vec::Vec;

use vm_core::crypto::hash::RpoDigest;
use vm_core::{
crypto::hash::RpoDigest,
utils::{ByteReader, ByteWriter, Deserializable, DeserializationError, Serializable},
};

use super::{AdviceMap, Felt, InnerNodeInfo, InputError, MerkleStore};

Expand All @@ -19,7 +22,7 @@ use super::{AdviceMap, Felt, InnerNodeInfo, InputError, MerkleStore};
/// 3. Merkle store, which is used to provide nondeterministic inputs for instructions that operates
/// with Merkle trees.
#[cfg(not(feature = "testing"))]
#[derive(Clone, Debug, Default)]
#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub struct AdviceInputs {
stack: Vec<Felt>,
map: AdviceMap,
Expand Down Expand Up @@ -132,13 +135,63 @@ impl AdviceInputs {
}
}

impl Serializable for AdviceInputs {
fn write_into<W: ByteWriter>(&self, target: &mut W) {
let Self { stack, map, store } = self;
stack.write_into(target);
map.write_into(target);
store.write_into(target);
}
}

impl Deserializable for AdviceInputs {
fn read_from<R: ByteReader>(source: &mut R) -> Result<Self, DeserializationError> {
let stack = Vec::<Felt>::read_from(source)?;
let map = AdviceMap::read_from(source)?;
let store = MerkleStore::read_from(source)?;
Ok(Self { stack, map, store })
}
}

// TESTING
// ================================================================================================

#[cfg(feature = "testing")]
#[derive(Clone, Debug, Default)]
#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub struct AdviceInputs {
pub stack: Vec<Felt>,
pub map: AdviceMap,
pub store: MerkleStore,
}

// TESTS
// ================================================================================================

#[cfg(test)]
mod tests {
use winter_utils::{Deserializable, Serializable};

use crate::AdviceInputs;

#[test]
fn test_advice_inputs_eq() {
let advice1 = AdviceInputs::default();
let advice2 = AdviceInputs::default();

assert_eq!(advice1, advice2);

let advice1 = AdviceInputs::default().with_stack_values([1, 2, 3].iter().copied()).unwrap();
let advice2 = AdviceInputs::default().with_stack_values([1, 2, 3].iter().copied()).unwrap();

assert_eq!(advice1, advice2);
}

#[test]
fn test_advice_inputs_serialization() {
let advice1 = AdviceInputs::default().with_stack_values([1, 2, 3].iter().copied()).unwrap();
let bytes = advice1.to_bytes();
let advice2 = AdviceInputs::read_from_bytes(&bytes).unwrap();

assert_eq!(advice1, advice2);
}
}
45 changes: 43 additions & 2 deletions processor/src/host/advice/map.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,10 @@ use alloc::{
vec::Vec,
};

use vm_core::crypto::hash::RpoDigest;
use vm_core::{
crypto::hash::RpoDigest,
utils::{ByteReader, ByteWriter, Deserializable, DeserializationError, Serializable},
};

use super::Felt;

Expand All @@ -15,7 +18,7 @@ use super::Felt;
/// Each key maps to one or more field element. To access the elements, the VM can move the values
/// associated with a given key onto the advice stack using `adv.push_mapval` instruction. The VM
/// can also insert new values into the advice map during execution.
#[derive(Debug, Clone, Default)]
#[derive(Debug, Clone, Default, PartialEq, Eq)]
pub struct AdviceMap(BTreeMap<RpoDigest, Vec<Felt>>);

impl AdviceMap {
Expand Down Expand Up @@ -60,3 +63,41 @@ impl Extend<(RpoDigest, Vec<Felt>)> for AdviceMap {
self.0.extend(iter)
}
}

impl Serializable for AdviceMap {
fn write_into<W: ByteWriter>(&self, target: &mut W) {
target.write_usize(self.0.len());
for (key, values) in self.0.iter() {
target.write((key, values));
}
}
}

impl Deserializable for AdviceMap {
fn read_from<R: ByteReader>(source: &mut R) -> Result<Self, DeserializationError> {
let mut map = BTreeMap::new();
let count = source.read_usize()?;
for _ in 0..count {
let (key, values) = source.read()?;
map.insert(key, values);
}
Ok(Self(map))
}
}

#[cfg(test)]
mod tests {
use super::*;

#[test]
fn test_advice_map_serialization() {
let mut map1 = AdviceMap::new();
map1.insert(RpoDigest::default(), vec![Felt::from(1u32), Felt::from(2u32)]);

let bytes = map1.to_bytes();

let map2 = AdviceMap::read_from_bytes(&bytes).unwrap();

assert_eq!(map1, map2);
}
}
1 change: 1 addition & 0 deletions test-utils/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -114,6 +114,7 @@ macro_rules! expect_exec_error {
};
}


/// Like [assembly::assert_diagnostic], but matches each non-empty line of the rendered output to a
/// corresponding pattern.
///
Expand Down

0 comments on commit 19b5643

Please sign in to comment.