Skip to content

Commit

Permalink
Merge branch 'next' into bobbin-arc-mast
Browse files Browse the repository at this point in the history
  • Loading branch information
plafer committed Aug 27, 2024
2 parents 0a339d6 + d7c8933 commit 296e75e
Show file tree
Hide file tree
Showing 18 changed files with 76 additions and 121 deletions.
2 changes: 2 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ A STARK-based virtual machine.

**WARNING:** This project is in an alpha stage. It has not been audited and may contain bugs and security flaws. This implementation is NOT ready for production use.

**WARNING:** For `no_std`, only the `wasm32-unknown-unknown` and `wasm32-wasip1` targets are officially supported.

## Overview

Miden VM is a zero-knowledge virtual machine written in Rust. For any program executed on Miden VM, a STARK-based proof of execution is automatically generated. This proof can then be used by anyone to verify that the program was executed correctly without the need for re-executing the program or even knowing the contents of the program.
Expand Down
8 changes: 5 additions & 3 deletions air/src/constraints/stack/field_ops/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -358,9 +358,11 @@ pub fn enforce_expacc_constraints<E: FieldElement>(
4
}

/// Enforces constraints of the EXT2MUL operation. The EXT2MUL operation computes the product of
/// two elements in the extension field of degree 2. Therefore, the following constraints are
/// enforced, assuming the first 4 elements of the stack in the current frame are a1, a0, b1, b0:
/// Enforces constraints of the EXT2MUL operation.
///
/// The EXT2MUL operation computes the product of two elements in the extension field of degree 2.
/// Therefore, the following constraints are enforced, assuming the first 4 elements of the stack in
/// the current frame are a1, a0, b1, b0:
/// - The first element in the next frame should be a1.
/// - The second element in the next frame should be a0.
/// - The third element in the next frame should be equal to (b0 + b1) * (a0 + a1) - b0 * a0.
Expand Down
18 changes: 10 additions & 8 deletions air/src/constraints/stack/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -35,14 +35,16 @@ pub const NUM_ASSERTIONS: usize = 2 * STACK_TOP_SIZE + 2;
/// The number of general constraints in the stack operations.
pub const NUM_GENERAL_CONSTRAINTS: usize = 17;

/// The degrees of constraints in the general stack operations. Each operation being executed
/// either shifts the stack to the left, right or doesn't effect it at all. Therefore, majority
/// of the general transitions of a stack item would be common across the operations and composite
/// flags were introduced to compute the individual stack item transition. A particular item lets
/// say at depth ith in the next stack frame can be transitioned into from ith depth (no shift op)
/// or (i+1)th depth(left shift) or (i-1)th depth(right shift) in the current frame. Therefore, the
/// VM would require only 16 general constraints to encompass all the 16 stack positions.
/// The last constraint checks if the top element in the stack is a binary or not.
/// The degrees of constraints in the general stack operations.
///
/// Each operation being executed either shifts the stack to the left, right or doesn't effect it at
/// all. Therefore, majority of the general transitions of a stack item would be common across the
/// operations and composite flags were introduced to compute the individual stack item transition.
/// A particular item lets say at depth ith in the next stack frame can be transitioned into from
/// ith depth (no shift op) or (i+1)th depth(left shift) or (i-1)th depth(right shift) in the
/// current frame. Therefore, the VM would require only 16 general constraints to encompass all the
/// 16 stack positions. The last constraint checks if the top element in the stack is a binary or
/// not.
pub const CONSTRAINT_DEGREES: [usize; NUM_GENERAL_CONSTRAINTS] = [
// Each degree are being multiplied with the respective composite flags which are of degree 7.
// Therefore, all the degree would incorporate 7 in their degree calculation.
Expand Down
8 changes: 5 additions & 3 deletions air/src/constraints/stack/stack_manipulation/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -91,9 +91,11 @@ pub fn enforce_pad_constraints<E: FieldElement>(
1
}

/// Enforces constraints of the DUPn and MOVUPn operations. The DUPn operation copies the element
/// at depth n in the stack and pushes the copy onto the stack, whereas MOVUPn opearation moves the
/// element at depth n to the top of the stack. Therefore, the following constraints are enforced:
/// Enforces constraints of the DUPn and MOVUPn operations.
///
/// The DUPn operation copies the element at depth n in the stack and pushes the copy onto the
/// stack, whereas MOVUPn opearation moves the element at depth n to the top of the stack.
/// Therefore, the following constraints are enforced:
/// - The top element in the next frame should be equal to the element at depth n in the current
/// frame. s0` - sn = 0.
pub fn enforce_dup_movup_n_constraints<E: FieldElement>(
Expand Down
7 changes: 4 additions & 3 deletions air/src/constraints/stack/system_ops/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -89,9 +89,10 @@ pub fn enforce_fmpadd_constraints<E: FieldElement>(
1
}

/// Enforces constraints of the FMPUPDATE operation. The FMPUPDATE operation increments the fmp
/// register value by the first element value in the current trace. Therefore, the following
/// constraints are enforced:
/// Enforces constraints of the FMPUPDATE operation.
///
/// The FMPUPDATE operation increments the fmp register value by the first element value in the
/// current trace. Therefore, the following constraints are enforced:
/// - The fmp register value in the next frame should be equal to the sum of the fmp register value
/// and the top stack element in the current frame. fmp` - (s0 + fmp) = 0.
pub fn enforce_fmpupdate_constraints<E: FieldElement>(
Expand Down
13 changes: 8 additions & 5 deletions air/src/constraints/stack/u32_ops/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -209,9 +209,10 @@ pub fn enforce_u32mul_constraints<E: FieldElement<BaseField = Felt>>(
1
}

/// Enforces constraints of the U32MADD operation. The U32MADD operation adds the third
/// element to the product of the first two elements in the current trace. Therefore, the
/// following constraints are enforced:
/// Enforces constraints of the U32MADD operation.
///
/// The U32MADD operation adds the third element to the product of the first two elements in the
/// current trace. Therefore, the following constraints are enforced:
/// - The aggregation of all the limbs in the helper registers is equal to the sum of the third
/// element with the product of the first two elements in the current trace.
pub fn enforce_u32madd_constraints<E: FieldElement<BaseField = Felt>>(
Expand All @@ -231,8 +232,10 @@ pub fn enforce_u32madd_constraints<E: FieldElement<BaseField = Felt>>(
1
}

/// Enforces constraints of the U32DIV operation. The U32DIV operation divides the second element
/// with the first element in the current trace. Therefore, the following constraints are enforced:
/// Enforces constraints of the U32DIV operation.
///
/// The U32DIV operation divides the second element with the first element in the current trace.
/// Therefore, the following constraints are enforced:
/// - The second element in the current trace should be equal to the sum of the first element in the
/// next trace with the product of the first element in the current trace and second element in
/// the next trace.
Expand Down
9 changes: 5 additions & 4 deletions air/src/trace/chiplets/kernel_rom.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,9 @@ pub const TRACE_WIDTH: usize = 6;

// --- OPERATION SELECTORS ------------------------------------------------------------------------

/// 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]
/// 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]
pub const KERNEL_PROC_LABEL: Felt = Felt::new(0b1000);
7 changes: 4 additions & 3 deletions air/src/trace/chiplets/memory.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,10 @@ pub const TRACE_WIDTH: usize = 12;
/// Number of selector columns in the trace.
pub const NUM_SELECTORS: usize = 2;

/// Type for Memory trace selectors. These selectors are used to define which operation and memory
/// state update (init & read / copy & read / write) is to be applied at a specific row of the
/// memory execution trace.
/// Type for Memory trace selectors.
///
/// These selectors are used to define which operation and memory state update (init & read / copy &
/// read / write) is to be applied at a specific row of the memory execution trace.
pub type Selectors = [Felt; NUM_SELECTORS];

// --- OPERATION SELECTORS ------------------------------------------------------------------------
Expand Down
27 changes: 7 additions & 20 deletions assembly/src/assembler/instruction/procedures.rs
Original file line number Diff line number Diff line change
Expand Up @@ -19,22 +19,20 @@ impl Assembler {
) -> Result<Option<MastNodeId>, AssemblyError> {
let span = callee.span();
let digest = self.resolve_target(kind, callee, proc_ctx, mast_forest_builder)?;
self.invoke_mast_root(kind, span, digest, proc_ctx, mast_forest_builder)
self.invoke_mast_root(kind, span, digest, mast_forest_builder)
}

fn invoke_mast_root(
&self,
kind: InvokeKind,
span: SourceSpan,
mast_root: RpoDigest,
proc_ctx: &mut ProcedureContext,
mast_forest_builder: &mut MastForestBuilder,
) -> Result<Option<MastNodeId>, AssemblyError> {
// Get the procedure from the assembler
let current_source_file = self.source_manager.get(span.source_id()).ok();

// If the procedure is cached, register the call to ensure the callset
// is updated correctly.
// If the procedure is cached and is a system call, ensure that the call is valid.
match mast_forest_builder.find_procedure(&mast_root) {
Some(proc) if matches!(kind, InvokeKind::SysCall) => {
// Verify if this is a syscall, that the callee is a kernel procedure
Expand Down Expand Up @@ -71,10 +69,8 @@ impl Assembler {
})
}
})?;
proc_ctx.register_external_call(proc, false)?;
},
Some(proc) => proc_ctx.register_external_call(proc, false)?,
None => (),
Some(_) | None => (),
}

let mast_root_node_id = {
Expand Down Expand Up @@ -150,34 +146,25 @@ impl Assembler {
&self,
callee: &InvocationTarget,
proc_ctx: &mut ProcedureContext,
span_builder: &mut BasicBlockBuilder,
basic_block_builder: &mut BasicBlockBuilder,
mast_forest_builder: &MastForestBuilder,
) -> Result<(), AssemblyError> {
let digest =
self.resolve_target(InvokeKind::ProcRef, callee, proc_ctx, mast_forest_builder)?;
self.procref_mast_root(digest, proc_ctx, span_builder, mast_forest_builder)
self.procref_mast_root(digest, basic_block_builder)
}

fn procref_mast_root(
&self,
mast_root: RpoDigest,
proc_ctx: &mut ProcedureContext,
span_builder: &mut BasicBlockBuilder,
mast_forest_builder: &MastForestBuilder,
basic_block_builder: &mut BasicBlockBuilder,
) -> Result<(), AssemblyError> {
// Add the root to the callset to be able to use dynamic instructions
// with the referenced procedure later

if let Some(proc) = mast_forest_builder.find_procedure(&mast_root) {
proc_ctx.register_external_call(proc, false)?;
}

// Create an array with `Push` operations containing root elements
let ops = mast_root
.iter()
.map(|elem| Operation::Push(*elem))
.collect::<SmallVec<[_; 4]>>();
span_builder.push_ops(ops);
basic_block_builder.push_ops(ops);
Ok(())
}
}
55 changes: 2 additions & 53 deletions assembly/src/assembler/procedure.rs
Original file line number Diff line number Diff line change
@@ -1,16 +1,14 @@
use alloc::{collections::BTreeSet, sync::Arc};
use alloc::sync::Arc;

use vm_core::mast::MastNodeId;

use super::GlobalProcedureIndex;
use crate::{
ast::{ProcedureName, QualifiedProcedureName, Visibility},
diagnostics::{SourceManager, SourceSpan, Spanned},
AssemblyError, LibraryPath, RpoDigest,
LibraryPath, RpoDigest,
};

pub type CallSet = BTreeSet<RpoDigest>;

// PROCEDURE CONTEXT
// ================================================================================================

Expand All @@ -23,7 +21,6 @@ pub struct ProcedureContext {
visibility: Visibility,
is_kernel: bool,
num_locals: u16,
callset: CallSet,
}

// ------------------------------------------------------------------------------------------------
Expand All @@ -44,7 +41,6 @@ impl ProcedureContext {
visibility,
is_kernel,
num_locals: 0,
callset: Default::default(),
}
}

Expand Down Expand Up @@ -93,38 +89,6 @@ impl ProcedureContext {
// ------------------------------------------------------------------------------------------------
/// State mutators
impl ProcedureContext {
pub fn insert_callee(&mut self, callee: RpoDigest) {
self.callset.insert(callee);
}

pub fn extend_callset<I>(&mut self, callees: I)
where
I: IntoIterator<Item = RpoDigest>,
{
self.callset.extend(callees);
}

/// Registers a call to an externally-defined procedure which we have previously compiled.
///
/// The call set of the callee is added to the call set of the procedure we are currently
/// compiling, to reflect that all of the code reachable from the callee is by extension
/// reachable by the caller.
pub fn register_external_call(
&mut self,
callee: &Procedure,
inlined: bool,
) -> Result<(), AssemblyError> {
// If we call the callee, it's callset is by extension part of our callset
self.extend_callset(callee.callset().iter().cloned());

// If the callee is not being inlined, add it to our callset
if !inlined {
self.insert_callee(callee.mast_root());
}

Ok(())
}

/// Transforms this procedure context into a [Procedure].
///
/// The passed-in `mast_root` defines the MAST root of the procedure's body while
Expand All @@ -140,7 +104,6 @@ impl ProcedureContext {
pub fn into_procedure(self, mast_root: RpoDigest, mast_node_id: MastNodeId) -> Procedure {
Procedure::new(self.name, self.visibility, self.num_locals as u32, mast_root, mast_node_id)
.with_span(self.span)
.with_callset(self.callset)
}
}

Expand Down Expand Up @@ -172,8 +135,6 @@ pub struct Procedure {
mast_root: RpoDigest,
/// The MAST node id which resolves to the above MAST root.
body_node_id: MastNodeId,
/// The set of MAST roots called by this procedure
callset: CallSet,
}

// ------------------------------------------------------------------------------------------------
Expand All @@ -193,19 +154,13 @@ impl Procedure {
num_locals,
mast_root,
body_node_id,
callset: Default::default(),
}
}

pub(crate) fn with_span(mut self, span: SourceSpan) -> Self {
self.span = span;
self
}

pub(crate) fn with_callset(mut self, callset: CallSet) -> Self {
self.callset = callset;
self
}
}

// ------------------------------------------------------------------------------------------------
Expand Down Expand Up @@ -246,12 +201,6 @@ impl Procedure {
pub fn body_node_id(&self) -> MastNodeId {
self.body_node_id
}

/// Returns a reference to a set of all procedures (identified by their MAST roots) which may
/// be called during the execution of this procedure.
pub fn callset(&self) -> &CallSet {
&self.callset
}
}

impl Spanned for Procedure {
Expand Down
10 changes: 5 additions & 5 deletions assembly/src/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -83,12 +83,12 @@ impl From<Label> for LabeledSpan {
// RELATED LABEL
// ================================================================================================

/// This type is used to associate a more complex label or set of labels with some other error. In
/// particular, it is used to reference related bits of source code distinct from that of the
/// original error.
/// This type is used to associate a more complex label or set of labels with some other error.
///
/// A related label can have a distinct severity, its own message, and its own sub-labels, and may
/// reference code in a completely different source file that the original error.
/// In particular, it is used to reference related bits of source code distinct from that of the
/// original error. A related label can have a distinct severity, its own message, and its own
/// sub-labels, and may reference code in a completely different source file that the original
/// error.
#[derive(Debug)]
pub struct RelatedLabel {
/// The severity for this related label
Expand Down
11 changes: 6 additions & 5 deletions assembly/src/testing.rs
Original file line number Diff line number Diff line change
Expand Up @@ -148,11 +148,12 @@ macro_rules! assert_diagnostic {
}};
}

/// Like [assert_diagnostic], but matches each non-empty line of the rendered output
/// to a corresponding pattern. So if the output has 3 lines, the second of which is
/// empty, and you provide 2 patterns, the assertion passes if the first line matches
/// the first pattern, and the third line matches the second pattern - the second
/// line is ignored because it is empty.
/// Like [assert_diagnostic], but matches each non-empty line of the rendered output to a
/// corresponding pattern.
///
/// So if the output has 3 lines, the second of which is empty, and you provide 2 patterns, the
/// assertion passes if the first line matches the first pattern, and the third line matches the
/// second pattern - the second line is ignored because it is empty.
#[macro_export]
macro_rules! assert_diagnostic_lines {
($diagnostic:expr, $($expected:expr),+) => {{
Expand Down
1 change: 1 addition & 0 deletions miden/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -308,6 +308,7 @@ Miden VM can be compiled with the following features:
- `executable` - required for building Miden VM binary as described above. Implies `std`.
- `metal` - enables [Metal](<https://en.wikipedia.org/wiki/Metal_(API)>)-based acceleration of proof generation (for recursive proofs) on supported platforms (e.g., Apple silicon).
- `no_std` does not rely on the Rust standard library and enables compilation to WebAssembly.
- Only the `wasm32-unknown-unknown` and `wasm32-wasip1` targets are officially supported.

To compile with `no_std`, disable default features via `--no-default-features` flag.

Expand Down
1 change: 1 addition & 0 deletions processor/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,7 @@ Miden processor can be compiled with the following features:

* `std` - enabled by default and relies on the Rust standard library.
* `no_std` does not rely on the Rust standard library and enables compilation to WebAssembly.
* Only the `wasm32-unknown-unknown` and `wasm32-wasip1` targets are officially supported.

To compile with `no_std`, disable default features via `--no-default-features` flag.

Expand Down
7 changes: 3 additions & 4 deletions processor/src/debug.rs
Original file line number Diff line number Diff line change
Expand Up @@ -47,10 +47,9 @@ impl fmt::Display for VmState {
}

/// Iterator that iterates through vm state at each step of the execution.
/// This allows debugging or replaying ability to view various process state
/// at each clock cycle.
/// If the execution returned an error, it returns that error on the clock cycle
/// it stopped.
///
/// This allows debugging or replaying ability to view various process state at each clock cycle. If
/// the execution returned an error, it returns that error on the clock cycle it stopped.
pub struct VmStateIterator {
chiplets: Chiplets,
decoder: Decoder,
Expand Down
Loading

0 comments on commit 296e75e

Please sign in to comment.