diff --git a/Cargo.toml b/Cargo.toml index c1bc061b8..aaed9a3cf 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -8,6 +8,7 @@ members = [ "air", "codegen/winterfell", "codegen/ace", + "constraints", ] resolver = "2" diff --git a/air-script/tests/codegen/winterfell.rs b/air-script/tests/codegen/winterfell.rs index 2fa96ccb8..efd1538d2 100644 --- a/air-script/tests/codegen/winterfell.rs +++ b/air-script/tests/codegen/winterfell.rs @@ -365,3 +365,30 @@ fn variables() { let expected = expect_file!["../variables/variables.rs"]; expected.assert_eq(&generated_air); } + +#[test] +fn cross_module_constants() { + // Test that constants used in comprehension iterables work across module boundaries + let generated_air = + Test::new("tests/cross_module_constants/cross_module_constants.air".to_string()) + .transpile(Target::Winterfell) + .unwrap(); + + let expected = expect_file!["../cross_module_constants/cross_mod_constants.rs"]; + expected.assert_eq(&generated_air); +} + +#[test] +fn comprehension_periodic_binding() { + // Test that comprehension bindings over periodic columns are typed as Local, not PeriodicColumn + // This pattern is used when iterating over a vector containing periodic column references + let generated_air = Test::new( + "tests/comprehension_periodic_binding/comprehension_periodic_binding.air".to_string(), + ) + .transpile(Target::Winterfell) + .unwrap(); + + let expected = + expect_file!["../comprehension_periodic_binding/comprehension_periodic_binding.rs"]; + expected.assert_eq(&generated_air); +} diff --git a/air-script/tests/comprehension_periodic_binding/comprehension_periodic_binding.air b/air-script/tests/comprehension_periodic_binding/comprehension_periodic_binding.air new file mode 100644 index 000000000..a21bbcbd5 --- /dev/null +++ b/air-script/tests/comprehension_periodic_binding/comprehension_periodic_binding.air @@ -0,0 +1,19 @@ +def ComprehensionPeriodicBindingTest + +use lib::test_comprehension; + +trace_columns { + main: [a, b], +} + +public_inputs { + stack_inputs: [1], +} + +boundary_constraints { + enf a.first = 0; +} + +integrity_constraints { + enf test_comprehension([a, b]); +} diff --git a/air-script/tests/comprehension_periodic_binding/comprehension_periodic_binding.rs b/air-script/tests/comprehension_periodic_binding/comprehension_periodic_binding.rs new file mode 100644 index 000000000..9e56fa9e2 --- /dev/null +++ b/air-script/tests/comprehension_periodic_binding/comprehension_periodic_binding.rs @@ -0,0 +1,97 @@ +use winter_air::{Air, AirContext, Assertion, AuxRandElements, EvaluationFrame, ProofOptions as WinterProofOptions, TransitionConstraintDegree, TraceInfo}; +use winter_math::fields::f64::BaseElement as Felt; +use winter_math::{ExtensionOf, FieldElement, ToElements}; +use winter_utils::{ByteWriter, Serializable}; + +pub struct PublicInputs { + stack_inputs: [Felt; 1], +} + +impl PublicInputs { + pub fn new(stack_inputs: [Felt; 1]) -> Self { + Self { stack_inputs } + } +} + +impl Serializable for PublicInputs { + fn write_into(&self, target: &mut W) { + self.stack_inputs.write_into(target); + } +} + +impl ToElements for PublicInputs { + fn to_elements(&self) -> Vec { + let mut elements = Vec::new(); + elements.extend_from_slice(&self.stack_inputs); + elements + } +} + +pub struct ComprehensionPeriodicBindingTest { + context: AirContext, + stack_inputs: [Felt; 1], +} + +impl ComprehensionPeriodicBindingTest { + pub fn last_step(&self) -> usize { + self.trace_length() - self.context().num_transition_exemptions() + } +} + +impl Air for ComprehensionPeriodicBindingTest { + type BaseField = Felt; + type PublicInputs = PublicInputs; + + fn context(&self) -> &AirContext { + &self.context + } + + fn new(trace_info: TraceInfo, public_inputs: PublicInputs, options: WinterProofOptions) -> Self { + let main_degrees = vec![TransitionConstraintDegree::with_cycles(1, vec![2, 2])]; + let aux_degrees = vec![]; + let num_main_assertions = 1; + let num_aux_assertions = 0; + + let context = AirContext::new_multi_segment( + trace_info, + main_degrees, + aux_degrees, + num_main_assertions, + num_aux_assertions, + options, + ) + .set_num_transition_exemptions(2); + Self { context, stack_inputs: public_inputs.stack_inputs } + } + + fn get_periodic_column_values(&self) -> Vec> { + vec![vec![Felt::ONE, Felt::new(2)], vec![Felt::new(3), Felt::new(4)]] + } + + fn get_assertions(&self) -> Vec> { + let mut result = Vec::new(); + result.push(Assertion::single(0, 0, Felt::ZERO)); + result + } + + fn get_aux_assertions>(&self, aux_rand_elements: &AuxRandElements) -> Vec> { + let mut result = Vec::new(); + result + } + + fn evaluate_transition>(&self, frame: &EvaluationFrame, periodic_values: &[E], result: &mut [E]) { + let main_current = frame.current(); + let main_next = frame.next(); + result[0] = main_next[0] - (main_current[0] * periodic_values[0] + main_current[1] * periodic_values[1]); + } + + fn evaluate_aux_transition(&self, main_frame: &EvaluationFrame, aux_frame: &EvaluationFrame, _periodic_values: &[F], aux_rand_elements: &AuxRandElements, result: &mut [E]) + where F: FieldElement, + E: FieldElement + ExtensionOf, + { + let main_current = main_frame.current(); + let main_next = main_frame.next(); + let aux_current = aux_frame.current(); + let aux_next = aux_frame.next(); + } +} \ No newline at end of file diff --git a/air-script/tests/comprehension_periodic_binding/lib.air b/air-script/tests/comprehension_periodic_binding/lib.air new file mode 100644 index 000000000..8667dc9ae --- /dev/null +++ b/air-script/tests/comprehension_periodic_binding/lib.air @@ -0,0 +1,16 @@ +mod lib + +periodic_columns { + k0: [1, 2], + k1: [3, 4], +} + +ev test_comprehension([a, b]) { + # Create local variable holding periodic column references + let cols = [k0, k1]; + let vals = [a, b]; + + # Iterate over the local variable - binding 'k' gets typed as PeriodicColumn + # but it's actually a local variable holding a value + enf a' = sum([x * k for (x, k) in (vals, cols)]); +} diff --git a/air-script/tests/comprehension_periodic_binding/mod.rs b/air-script/tests/comprehension_periodic_binding/mod.rs new file mode 100644 index 000000000..83244b98e --- /dev/null +++ b/air-script/tests/comprehension_periodic_binding/mod.rs @@ -0,0 +1,3 @@ +#[rustfmt::skip] +#[allow(clippy::all)] +mod comprehension_periodic_binding; diff --git a/air-script/tests/cross_module_constants/constants_lib.air b/air-script/tests/cross_module_constants/constants_lib.air new file mode 100644 index 000000000..25ef19270 --- /dev/null +++ b/air-script/tests/cross_module_constants/constants_lib.air @@ -0,0 +1,21 @@ +mod constants_lib + +# Constants used in comprehension iterables +const WEIGHTS = [1, 2, 3, 4]; + +# Pure function that uses constants in a comprehension +fn weighted_sum(values: felt[4]) -> felt { + return sum([v * w for (v, w) in (values, WEIGHTS)]); +} + +# Another function that calls the first +fn compute_result(a: felt, b: felt, c: felt, d: felt) -> felt { + let values = [a, b, c, d]; + return weighted_sum(values); +} + +# Evaluator that uses the chain of functions +ev apply_computation([cols[5]]) { + let result = compute_result(cols[0], cols[1], cols[2], cols[3]); + enf cols[4] = result; +} diff --git a/air-script/tests/cross_module_constants/cross_mod_constants.rs b/air-script/tests/cross_module_constants/cross_mod_constants.rs new file mode 100644 index 000000000..5de652283 --- /dev/null +++ b/air-script/tests/cross_module_constants/cross_mod_constants.rs @@ -0,0 +1,97 @@ +use winter_air::{Air, AirContext, Assertion, AuxRandElements, EvaluationFrame, ProofOptions as WinterProofOptions, TransitionConstraintDegree, TraceInfo}; +use winter_math::fields::f64::BaseElement as Felt; +use winter_math::{ExtensionOf, FieldElement, ToElements}; +use winter_utils::{ByteWriter, Serializable}; + +pub struct PublicInputs { + expected: [Felt; 1], +} + +impl PublicInputs { + pub fn new(expected: [Felt; 1]) -> Self { + Self { expected } + } +} + +impl Serializable for PublicInputs { + fn write_into(&self, target: &mut W) { + self.expected.write_into(target); + } +} + +impl ToElements for PublicInputs { + fn to_elements(&self) -> Vec { + let mut elements = Vec::new(); + elements.extend_from_slice(&self.expected); + elements + } +} + +pub struct CrossModuleConstantsTest { + context: AirContext, + expected: [Felt; 1], +} + +impl CrossModuleConstantsTest { + pub fn last_step(&self) -> usize { + self.trace_length() - self.context().num_transition_exemptions() + } +} + +impl Air for CrossModuleConstantsTest { + type BaseField = Felt; + type PublicInputs = PublicInputs; + + fn context(&self) -> &AirContext { + &self.context + } + + fn new(trace_info: TraceInfo, public_inputs: PublicInputs, options: WinterProofOptions) -> Self { + let main_degrees = vec![TransitionConstraintDegree::new(1)]; + let aux_degrees = vec![]; + let num_main_assertions = 1; + let num_aux_assertions = 0; + + let context = AirContext::new_multi_segment( + trace_info, + main_degrees, + aux_degrees, + num_main_assertions, + num_aux_assertions, + options, + ) + .set_num_transition_exemptions(2); + Self { context, expected: public_inputs.expected } + } + + fn get_periodic_column_values(&self) -> Vec> { + vec![] + } + + fn get_assertions(&self) -> Vec> { + let mut result = Vec::new(); + result.push(Assertion::single(0, 0, Felt::ZERO)); + result + } + + fn get_aux_assertions>(&self, aux_rand_elements: &AuxRandElements) -> Vec> { + let mut result = Vec::new(); + result + } + + fn evaluate_transition>(&self, frame: &EvaluationFrame, periodic_values: &[E], result: &mut [E]) { + let main_current = frame.current(); + let main_next = frame.next(); + result[0] = main_current[4] - (main_current[0] + main_current[1] * E::from(Felt::new(2_u64)) + main_current[2] * E::from(Felt::new(3_u64)) + main_current[3] * E::from(Felt::new(4_u64))); + } + + fn evaluate_aux_transition(&self, main_frame: &EvaluationFrame, aux_frame: &EvaluationFrame, _periodic_values: &[F], aux_rand_elements: &AuxRandElements, result: &mut [E]) + where F: FieldElement, + E: FieldElement + ExtensionOf, + { + let main_current = main_frame.current(); + let main_next = main_frame.next(); + let aux_current = aux_frame.current(); + let aux_next = aux_frame.next(); + } +} \ No newline at end of file diff --git a/air-script/tests/cross_module_constants/cross_module_constants.air b/air-script/tests/cross_module_constants/cross_module_constants.air new file mode 100644 index 000000000..87315ecd6 --- /dev/null +++ b/air-script/tests/cross_module_constants/cross_module_constants.air @@ -0,0 +1,21 @@ +def CrossModuleConstantsTest + +# Import evaluator that uses a chain: apply_computation -> compute_result -> weighted_sum -> WEIGHTS constant +use constants_lib::apply_computation; + +trace_columns { + main: [a, b, c, d, result], +} + +public_inputs { + expected: [1], +} + +boundary_constraints { + enf a.first = 0; +} + +integrity_constraints { + # Use imported evaluator that internally uses constants in comprehensions + enf apply_computation([a, b, c, d, result]); +} diff --git a/air-script/tests/cross_module_constants/mod.rs b/air-script/tests/cross_module_constants/mod.rs new file mode 100644 index 000000000..e10ee53c7 --- /dev/null +++ b/air-script/tests/cross_module_constants/mod.rs @@ -0,0 +1,3 @@ +#[rustfmt::skip] +#[allow(clippy::all)] +mod cross_mod_constants; diff --git a/air-script/tests/mod.rs b/air-script/tests/mod.rs index e96e603d8..e54fb7fdd 100644 --- a/air-script/tests/mod.rs +++ b/air-script/tests/mod.rs @@ -9,6 +9,8 @@ mod bitwise; #[allow(unused_variables, dead_code, unused_mut)] mod buses; #[allow(unused_variables, dead_code, unused_mut)] +mod comprehension_periodic_binding; +#[allow(unused_variables, dead_code, unused_mut)] mod computed_indices; #[allow(unused_variables, dead_code, unused_mut)] mod constant_in_range; @@ -17,6 +19,8 @@ mod constants; #[allow(unused_variables, dead_code, unused_mut)] mod constraint_comprehension; #[allow(unused_variables, dead_code, unused_mut)] +mod cross_module_constants; +#[allow(unused_variables, dead_code, unused_mut)] mod evaluators; #[allow(unused_variables, dead_code, unused_mut)] mod fibonacci; diff --git a/constraints/Cargo.toml b/constraints/Cargo.toml new file mode 100644 index 000000000..2263eadd9 --- /dev/null +++ b/constraints/Cargo.toml @@ -0,0 +1,23 @@ +[package] +name = "constraints" +version = "0.1.0" +edition = "2021" + +[dependencies] +air-ir = { path = "../air", version = "0.5" } +air-parser = { path = "../parser", version = "0.5" } +air-pass = { path = "../pass", version = "0.5" } +air-mir = { path = "../mir", version = "0.5" } +air-codegen-ace = { path = "../codegen/ace", version = "0.5" } +miden-diagnostics = { workspace = true } +miden-core = { package = "miden-core", version = "0.13", default-features = false } + +winter-air = { package = "winter-air", version = "0.12", default-features = false } +winter-math = { package = "winter-math", version = "0.12", default-features = false } +winter-utils = { package = "winter-utils", version = "0.12", default-features = false } +winter-prover = { package = "winter-prover", version = "0.12", default-features = false } +winter-verifier = { package = "winter-verifier", version = "0.12", default-features = false } +winterfell = { package = "winterfell", version = "0.12", default-features = false } + +[dev-dependencies] +anyhow = "1" \ No newline at end of file diff --git a/constraints/ace.air b/constraints/ace.air new file mode 100644 index 000000000..f822adbb3 --- /dev/null +++ b/constraints/ace.air @@ -0,0 +1,313 @@ +########################################################################################## +# ACE CHIPLET CONSTRAINTS MODULE +########################################################################################## +# +# The ACE (Arithmetic Circuit Evaluation) chiplet reduces the number of cycles required +# when recursively verifying a STARK proof in Miden assembly by evaluating arithmetic +# circuits and ensuring they evaluate to zero over given inputs. +# +# OVERVIEW: +# The ACE chiplet operates in two phases: +# 1. READ blocks: Load extension field elements from memory and assign node IDs +# 2. EVAL blocks: Execute arithmetic operations on previously loaded nodes +# +# Each section starts with READ operations to load inputs, followed by EVAL operations +# to compute intermediate and final results. The final result must evaluate to zero +# to represent a valid constraint satisfaction. +# +# ACE TRACE TABLE LAYOUT (16 columns): +# +# ┌─────────────┬────────────────────────────────────────────────────────────────────────────┐ +# │ Column │ Purpose │ +# ├─────────────┼────────────────────────────────────────────────────────────────────────────┤ +# │ sstart │ Section start flag (binary): 1 = first row of section, 0 = otherwise │ +# │ sblock │ Block selector (binary): 0 = READ block, 1 = EVAL block │ +# │ ctx │ Memory access context (constant throughout section) │ +# │ ptr │ Memory pointer: increments by +4 in READ, +1 in EVAL blocks │ +# │ clk │ Memory access clock cycle (constant within section) │ +# │ op │ Operation type (EVAL only): -1 = SUB, 0 = MUL, 1 = ADD │ +# │ id0 │ Result node ID: decrements by -2 in READ, -1 in EVAL │ +# │ v0_0 │ Result node value (extension field element, coefficient 0) │ +# │ v0_1 │ Result node value (extension field element, coefficient 1) │ +# │ id1 │ First operand node ID │ +# │ v1_0 │ First operand value (extension field element, coefficient 0) │ +# │ v1_1 │ First operand value (extension field element, coefficient 1) │ +# │ id2 / n_eval│ Dual use: 2nd operand node ID (EVAL) / #evaluations in section (READ) │ +# │ v2_0 │ Second operand value (extension field element, coefficient 0) │ +# │ v2_1 │ Second operand value (extension field element, coefficient 1) │ +# │ m0 │ Wire bus multiplicity (for node tracking, not yet implemented) │ +# └─────────────┴────────────────────────────────────────────────────────────────────────────┘ +# +# STATUS: Core constraints implemented, wire bus constraints not implemented +# +# REFERENCES: +# - ACE Design: https://0xmiden.github.io/miden-vm/design/chiplets/ace.html +########################################################################################## + +mod ace + +use chiplets::*; +use utils::*; + +########################################################################################## +# ACE CHIPLET CONSTRAINTS +########################################################################################## + +# Enforces constraints on all rows of ACE chiplet. +ev ace_chiplet_constraints_all_rows([s3, ace[16]]) { + let sstart = ace[0]; # Section start flag + let sblock = ace[1]; # Block selector (0=READ, 1=EVAL) + let ctx = ace[2]; # Memory access context + let ptr = ace[3]; # Memory pointer + let clk = ace[4]; # Memory access clock + let op = ace[5]; # Operation type (for EVAL block) + let id0 = ace[6]; # First node identifier + let v0_0 = ace[7]; # First node value (element 0) + let v0_1 = ace[8]; # First node value (element 1) + let id1 = ace[9]; # Second node identifier + let v1_0 = ace[10]; # Second node value (element 0) + let v1_1 = ace[11]; # Second node value (element 1) + let id2 = ace[12]; # Third node identifier (result node in EVAL) + let n_eval = ace[12]; # Total number of arithmetic operations + let v2_0 = ace[13]; # Third node value (element 0) + let v2_1 = ace[14]; # Third node value (element 1) + let m0 = ace[15]; # Multiplicity for wire bus operations + + let flag_ace_next = flag_ace_current_and_next(s3'); + let flag_ace_last = flag_ace_last(s3'); + + # Section and block flags constraints + enf section_block_flags_constraints([s3, sstart, sstart', sblock, id0, n_eval]); + + # Section general constraints + enf section_constraints([sstart, sblock, ctx, ptr, clk, id0]) when flag_ace_next; + + # Section specific constraints: READ block + enf enforce_read_block_constraints([sblock, id0, id1]); + + # Section specific constraints: EVAL block + enf enforce_eval_block_constraints([sblock, op, v0_0, v0_1, v1_0, v1_1, v2_0, v2_1]); + + # Finalization constraints + let f_end = binary_or(binary_and(flag_ace_next, sstart'), flag_ace_last); + enf finalization_constraints([id0, v0_0, v0_1]) when f_end; +} + +# Enforces that on the first row of ACE chiplet we should have sstart' = 1 +ev ace_chiplet_constraints_first_row([ace[16]]) { + let sstart = ace[0]; # Section start flag + + enf sstart' = 1; +} + +########################################################################################## +# CONSTRAINT EVALUATORS +########################################################################################## + +# Section and block flag management +# +# This evaluator enforces the proper sequencing of ACE chiplet operations: +# - Sections must start with READ blocks and end with EVAL blocks +# - Block transitions follow valid patterns (READ→EVAL within sections) +# - Section boundaries are correctly marked with sstart flags +# - READ→EVAL transition occurs when n_eval matches id0 +ev section_block_flags_constraints([s3, sstart, sstart_next, sblock, id0, n_eval]) { + let flag_ace_next = flag_ace_current_and_next(s3'); + let flag_ace_last = flag_ace_last(s3'); + + let section_flags = section_flags(s3', sstart, sstart_next); + let f_start = section_flags[0]; + let f_next = section_flags[1]; + let f_end = section_flags[2]; + + let block_flags = block_flags(sblock); + let block_flags_next = block_flags(sblock'); + let f_read = block_flags[0]; + let f_eval = block_flags[1]; + let f_read_next = block_flags_next[0]; + let f_eval_next = block_flags_next[1]; + + # Binary constraints for section and block flags + enf enforce_binary_columns([sstart, sblock]); + + # Last row of ACE chiplet cannot be section start + enf sstart = 0 when flag_ace_last; + + # Prevent consecutive section starts within ACE chiplet + enf binary_and(sstart, sstart') = 0 when flag_ace_next; + + # Sections must start with READ blocks (not EVAL) + enf f_eval = 0 when f_start; + + # EVAL blocks cannot be followed by READ blocks within same section + enf f_read_next = 0 when binary_and(f_next, f_eval); + + # Sections must end with EVAL blocks (not READ) + enf f_read = 0 when f_end; + + # In a READ block, n_eval stays constant. + # When transitioning to an EVAL block, the next id0 must equal n_eval - 1. + # This ensures proper sequencing: READ loads nodes with IDs, EVAL starts processing + # from the highest loaded node ID (n_eval - 1). + enf select(f_read_next, n_eval', id0' + 1) = n_eval when f_read; +} + +# Constrains binary columns for flags and selectors +ev enforce_binary_columns([sstart, sblock]) { + # Section start flag must be binary + enf is_binary([sstart]); + + # Block selector must be binary + enf is_binary([sblock]); +} + +# Section-level constraints (common to both READ and EVAL blocks) +# +# These constraints apply throughout an entire section regardless of block type: +# - Context (ctx) and clock (clk) remain constant within a section +# - Memory pointer (ptr) increments with fixed increments: +4 in READ, +1 in EVAL +# - Node identifiers (id0) decrement with fixed decrements: -2 in READ, -1 in EVAL +# +# Note: These constraints are active when the next row is NOT the start of a new section, +# i.e., all but the last rows of the section (intra-section transitions only). +ev section_constraints([sstart, sblock, ctx, ptr, clk, id0]) { + let flag_within_section = binary_not(sstart'); + let flag_read = !sblock; + let flag_eval = sblock; + + # Context consistency within a section + enf ctx' = ctx when flag_within_section; + + # Clock consistency within a section + enf clk' = clk when flag_within_section; + + # Memory pointer increases by 4 in READ blocks and by 1 in EVAL blocks + enf ptr' = ptr + 4 * flag_read + flag_eval when flag_within_section; + + # Node identifiers decrease by 2 in READ blocks and by 1 in EVAL blocks + enf id0 = id0' + 2 * flag_read + flag_eval when flag_within_section; +} + +# Finalization constraints (ensure final result is zero) +ev finalization_constraints([id0, v0_0, v0_1]) { + # The final result of the arithmetic circuit evaluation must be zero + # This ensures the circuit represents a valid constraint + enf v0_0 = 0; + enf v0_1 = 0; + + # Final node ID should be the root node + enf id0 = 0; +} + +# READ block operation constraints +# +# The only specific constraint to READ blocks is a constraint ensuring that the IDs of the two +# loaded extension field elements is consecutive. +ev enforce_read_block_constraints([sblock, id0, id1]) { + let is_read_block = binary_not(sblock); + + # In READ block, we read two extension field elements and assign node IDs + # The two node IDs should be consecutive. Note that the node IDs are decreasing. + enf id1 = id0 - 1 when is_read_block; +} + +# EVAL block operation constraints +# +# Enforces arithmetic circuit evaluation during EVAL operations: +# - Validates operation codes (op ∈ {-1, 0, 1} for SUB, MUL, ADD) +# - Performs extension field arithmetic on input nodes (v1, v2) +ev enforce_eval_block_constraints([sblock, op, v0_0, v0_1, v1_0, v1_1, v2_0, v2_1]) { + let is_eval_block = sblock; + + # In EVAL block, we decode instruction and perform arithmetic operation + # The 'op' column contains the operation type and must be equal to either -1, 0, or 1 + enf op * (op - 1) * (op + 1) = 0 when is_eval_block; + + # Arithmetic operation constraint based on op type + enf enforce_arithmetic_operation([op, v0_0, v0_1, v1_0, v1_1, v2_0, v2_1]) when is_eval_block; +} + + +# Arithmetic operation evaluation for EVAL block +# +# Performs extension field arithmetic based on operation code: +# - op = -1: Subtraction (v0 = v1 - v2) +# - op = 0: Multiplication (v0 = v1 × v2) +# - op = 1: Addition (v0 = v1 + v2) +# +# All arithmetic is in the quadratic extension field 𝔽ₚ[x]/(x² - x + 2) +ev enforce_arithmetic_operation([op, v0_0, v0_1, v1_0, v1_1, v2_0, v2_1]) { + # Decode operation and enforce arithmetic constraint for extension field elements + # Extension field elements are represented as (a_0, a_1) where element = a_0 + a_1 * α + + let linear_op = compute_linear_op(op, v1_0, v1_1, v2_0, v2_1); + let linear_op_0 = linear_op[0]; + let linear_op_1 = linear_op[1]; + + let non_linear_op = compute_non_linear_op(v1_0, v1_1, v2_0, v2_1); + let non_linear_op_0 = non_linear_op[0]; + let non_linear_op_1 = non_linear_op[1]; + + let op_square = op^2; + + enf op_square * (linear_op_0 - non_linear_op_0) + non_linear_op_0 = v0_0; + enf op_square * (linear_op_1 - non_linear_op_1) + non_linear_op_1 = v0_1; +} + +# Computes linear operations (addition and subtraction) in extension field +# - op = -1: Subtraction (v0 = v1 - v2) +# - op = 1: Addition (v0 = v1 + v2) +fn compute_linear_op(op: felt, v1_0: felt, v1_1: felt, v2_0: felt, v2_1: felt) -> felt[2] { + let res0 = v1_0 + op * v2_0; + let res1 = v1_1 + op * v2_1; + return [res0, res1]; +} + +# Multiplication in the quadratic extension field. +# +# The extension is 𝔽ₚ[x]/(x² - x + 2) +fn compute_non_linear_op(v1_0: felt, v1_1: felt, v2_0: felt, v2_1: felt) -> felt[2] { + let a0 = v1_0; + let a1 = v1_1; + let b0 = v2_0; + let b1 = v2_1; + + let res0 = a0 * b0 - 2 * a1 * b1; + let res1 = (b0 + b1) * (a0 + a1) - a0 * b0; + + return [res0, res1]; +} + +########################################################################################## +# HELPER FUNCTIONS +########################################################################################## + +# ACE chiplet active in current row and continuing to next row +fn flag_ace_current_and_next(s3_next: felt) -> felt { + return !s3_next; +} + +# ACE chiplet active in current row but transitioning out in next row +fn flag_ace_last(s3_next: felt) -> felt { + return s3_next; +} + +# Computes section-level flags: [f_start, f_next, f_end] +fn section_flags(s3_next: felt, s_start: felt, s_start_next: felt) -> felt[3] { + let f_ace_next = flag_ace_current_and_next(s3_next); + let f_ace_last = flag_ace_last(s3_next); + + let f_start = s_start; + let f_next = !s_start_next; + let f_end = binary_or(binary_and(f_ace_next, s_start_next), f_ace_last); + + return [f_start, f_next, f_end]; +} + +# Computes block-level flags: [f_read, f_eval] +fn block_flags(s_block: felt) -> felt[2] { + let f_read = !s_block; + let f_eval = s_block; + + return [f_read, f_eval]; +} \ No newline at end of file diff --git a/constraints/bitwise.air b/constraints/bitwise.air new file mode 100644 index 000000000..78efb50a6 --- /dev/null +++ b/constraints/bitwise.air @@ -0,0 +1,158 @@ +########################################################################################## +# BITWISE OPERATIONS CHIPLET +########################################################################################## +# +# The Bitwise chiplet handles bitwise logical operations (AND, XOR) on 32-bit values. +# It decomposes field elements into their binary representation and performs bit-level +# operations efficiently using field arithmetic. +# +# Each bitwise operation spans exactly 8 rows, with limbs processed in little-endian order. +# +# STATUS: Partially implemented (missing bus constraints) +# +# REFERENCES: +# - Bitwise Chiplet: https://0xmiden.github.io/miden-vm/design/chiplets/bitwise.html +########################################################################################## + +mod bitwise + +use utils::*; + +########################################################################################## +# BITWISE OPERATION CONSTANTS (Periodic Columns) +########################################################################################## +# +# Periodic constants contain values needed to switch various constraints on or off. +# +periodic_columns { + k_first: [1, 0, 0, 0, 0, 0, 0, 0], + k_transition: [1, 1, 1, 1, 1, 1, 1, 0], +} + +########################################################################################## +# BITWISE CHIPLET TRANSITION CONSTRAINTS +########################################################################################## +# +# The bitwise chiplet processes 32-bit integers by decomposing them into individual +# bits, applying bitwise operations, and recomposing the results. This approach +# enables verification of bitwise logic within the field arithmetic constraint system. + +# Enforces the constraints on the bitwise chiplet given its columns. +# +# Max constraint degree: 4 +ev bitwise_chiplet_constraints([op_flag, a, b, a_limb[4], b_limb[4], zp, z]) { + enf bitwise_op_flag([op_flag]); + enf input_decomposition([a, b, a_limb, b_limb]); + enf output_aggregation([op_flag, a, b, a_limb, b_limb, zp, z]); +} + +########################################################################################## +# BUS CONSTRAINTS +########################################################################################## +# +# The bitwise chiplet communicates with the stack component using the chiplets bus. +# +# MESSAGE FORMAT: +# +# Each bitwise operation message contains: +# - Operation type (AND/XOR) +# - Input operands (a, b) as 32-bit values +# - Expected result (c) +# +########################################################################################## + +########################################################################################## +# HELPERS +########################################################################################## + +### Helper evaluators ############################################################################# + +# Enforces that the bitwise operation flag is valid. +# +# Max constraint degree: 2 +ev bitwise_op_flag([op_flag]) { + # Enforce operation flag is binary (0 for AND, 1 for XOR). + # Constraint degree: 2 + enf is_binary([op_flag]); + + # Enforce operation flag should stay the same throughout the 8-row cycle. + # Constraint degree: 2 + enf op_flag' = op_flag when k_transition; +} + + +# Enforces that the input to the bitwise chiplet is decomposed into limbs correctly. +# +# Max constraint degree: 2 +ev input_decomposition([a, b, a_limb[4], b_limb[4]]) { + # Enforce that the input is decomposed into valid bits. + # Constraints degree: 2 + enf is_binary([a]) for a in a_limb; + enf is_binary([b]) for b in b_limb; + + # Enforce that the value in the first row of column `a` of the current 8-row cycle should be + # the aggregation of the decomposed bit columns `a_limb` (little-endian). + let a_aggr = aggregate_limbs(a_limb); + # Constraint degree: 2 + enf a = a_aggr when k_first; + + # Enforce that the value in the first row of column `b` of the current 8-row cycle should be + # the aggregation of the decomposed bit columns `b_limb` (little-endian). + let b_aggr = aggregate_limbs(b_limb); + # Constraint degree: 2 + enf b = b_aggr when k_first; + + # Enforce that for all rows in an 8-row cycle, except for the last one, the values in a and b + # columns are increased by the values contained in the individual bit columns a_limb and + # b_limb. + # Constraints degree: 2 + enf a' = a * 16 + a_aggr when k_transition; + enf b' = b * 16 + b_aggr when k_transition; +} + + +# Enforces that the output of the bitwise operation is aggregated correctly from the decomposed +# limbs. +# +# Max constraint degree: 3 +ev output_aggregation([op_flag, a, b, a_limb[4], b_limb[4], zp, z]) { + # Enforce that in the first row, the aggregated output value of the previous row should be 0. + # Constraint degree: 2 + enf zp = 0 when k_first; + + # Enforce that for each row except the last, the aggregated output value must equal the + # previous aggregated output value in the next row. + # Constraint degree: 2 + enf zp' = z when k_transition; + + # Enforce that for all rows the value in the z column is computed by multiplying the previous + # output value (from the zp column in the current row) by 16 and then adding it to the bitwise + # operation applied to the row's set of bits of a_limb and b_limb. The entire constraint must + # also be multiplied by the operation selector flag to ensure it is only applied for the + # appropriate operation. The constraint for AND is enforced when op_flag = 0 and the constraint for + # XOR is enforced when op_flag = 1. Because the selectors for the AND and XOR operations are mutually + # exclusive, the constraints for different operations can be aggregated into the same result + # indices. + # Constraints degree: 3 + let a_and_b = compute_limb_and(a_limb, b_limb); + let a_xor_b = compute_limb_xor(a_limb, b_limb); + + enf z = zp * 16 + op_flag * (a_xor_b - a_and_b) + a_and_b; +} + +### Helper functions ############################################################################## + +# Returns value aggregated from limbs in little-endian order. +fn aggregate_limbs(limbs: felt[4]) -> felt { + return sum([2^i * limb for (i, limb) in (0..4, limbs)]); +} + +# Computes AND operation result for a 4-bit limb using fold/reduce approach. +fn compute_limb_and(a_limb: felt[4], b_limb: felt[4]) -> felt { + return sum([2^i * binary_and(a_bit, b_bit) for (i, a_bit, b_bit) in (0..4, a_limb, b_limb)]); +} + +# Computes XOR operation result for a 4-bit limb using fold/reduce approach. +fn compute_limb_xor(a_limb: felt[4], b_limb: felt[4]) -> felt { + return sum([2^i * binary_xor(a_bit, b_bit) for (i, a_bit, b_bit) in (0..4, a_limb, b_limb)]); +} diff --git a/constraints/chiplets.air b/constraints/chiplets.air new file mode 100644 index 000000000..37d6a6b9b --- /dev/null +++ b/constraints/chiplets.air @@ -0,0 +1,173 @@ +########################################################################################## +# CHIPLETS CONSTRAINTS MODULE +########################################################################################## +# +# The Chiplets module contains specialized computation units that handle complex operations +# like cryptographic hashing, bitwise operations, and memory access. Each chiplet uses a +# hierarchical selector system to identify which operations are active. +# +# CHIPLETS COLUMN LAYOUT (20 columns): +# ┌─────────┬──────────────────────────────────────────────────────────────────────┐ +# │ Columns │ Purpose │ +# ├─────────┼──────────────────────────────────────────────────────────────────────┤ +# │ 0-4 │ s[5] - Hierarchical selector flags │ +# │ 5-19 │ Chiplet-specific data (hasher, bitwise ops, memory, ACE, kernel ROM) │ +# └─────────┴──────────────────────────────────────────────────────────────────────┘ +# +# STATUS: Not fully implemented +# +# REFERENCES: +# - Chiplets Design: https://0xmiden.github.io/miden-vm/design/chiplets/main.html +########################################################################################## + +mod chiplets + +use ace::ace_chiplet_constraints_all_rows; +use ace::ace_chiplet_constraints_first_row; + +use hasher::hash_chiplet; + +use bitwise::bitwise_chiplet_constraints; + +use memory::memory_chiplet_constraints_all_rows; +use memory::memory_chiplet_constraints_all_rows_except_last; +use memory::flag_memory_active_not_last_row; +use memory::flag_next_row_first_row_memory; +use memory::memory_chiplet_constraints_first_row; + +use kernel_rom::ker_rom_chiplet_constraints; +use kernel_rom::kernel_rom_chiplet_constraints_first_row; + +use utils::*; + +########################################################################################## +# CHIPLETS CONSTRAINTS +########################################################################################## + +ev chiplets_constraints([chiplets[20]]) { + # Chiplets' flag constraints + let s0 = chiplets[0]; + let s1 = chiplets[1]; + let s2 = chiplets[2]; + let s3 = chiplets[3]; + let s4 = chiplets[4]; + enf chiplet_selectors([s0, s1, s2, s3, s4]); + + # MAIN CHIPLET CONSTRAINT: + + # The chiplet system uses a hierarchical binary selector scheme where each selector + # bit (s0, s1, s2, s3, s4) determines which chiplet is active at any given row. + # + # This hierarchy ensures exactly one chiplet is active per row and provides + # deterministic transitions between chiplets based on selector state changes. + let hash_active = hasher_chiplet_flag(s0); # Active when: !s0 + let bitwise_active = bitwise_chiplet_flag(s0, s1); # Active when: s0 * !s1 + let memory_active = memory_chiplet_flag(s0, s1, s2); # Active when: s0 * s1 * !s2 + let ace_active = ace_chiplet_flag(s0, s1, s2, s3); # Active when: s0 * s1 * s2 * !s3 + let ker_rom_active = ker_rom_chiplet_flag(s0, s1, s2, s3, s4); # Active when: s0 * s1 * s2 * s3 * !s4 + + # Apply chiplet-specific constraints based on hierarchical selector state. + enf match { + case hash_active: hash_chiplet([chiplets[1..17]]), + case bitwise_active: bitwise_chiplet_constraints([chiplets[2..15]]), + case memory_active: memory_chiplet_constraints_all_rows([chiplets[3..18]]), + case ace_active: ace_chiplet_constraints_all_rows([chiplets[3..20]]), + case ker_rom_active: ker_rom_chiplet_constraints([chiplets[4..10]]), + }; + + # CHIPLET CONSTRAINTS REQUIRING SPECIAL HANDLING + + ## MEMORY + + ### The memory chiplet requires special handling for both initialization and transition constraints + ### to ensure proper memory access sequencing and state transitions. + let flag_next_row_first_row_memory = flag_next_row_first_row_memory(s0, s1, s2); # Transitioning into memory chiplet + let flag_memory_active_not_last_row = flag_memory_active_not_last_row(s0, s1, s2); # Active in memory, not exiting + + ### MEMORY INITIALIZATION CONSTRAINTS: + ### Apply specialized initialization constraints when first entering the memory chiplet. + enf memory_chiplet_constraints_first_row([chiplets[3..18]]) when flag_next_row_first_row_memory; + + ### MEMORY TRANSITION CONSTRAINTS ON ALL BUT LAST ROW: + ### Apply standard transition constraints while active in memory chiplet, excluding the final row. + enf memory_chiplet_constraints_all_rows_except_last([chiplets[3..18]]) when flag_memory_active_not_last_row; + + ## ACE + + ### Apply ACE chiplet initialization constraints at the transition point + let next_row_first_ace = binary_and(memory_active, s2'); # Transitioning into ACE chiplet + enf ace_chiplet_constraints_first_row([chiplets[4..20]]) when next_row_first_ace; + + ## KERNEL ROM + + ### The kernel ROM chiplet requires initialization constraints to ensure proper startup. + ### We force sfirst' = 1 on the first kernel ROM row, establishing proper digest initialization. + let next_row_first_kernel_rom = binary_and(ace_active, s3'); # Transitioning into kernel ROM chiplet + enf kernel_rom_chiplet_constraints_first_row([chiplets[4..10]]) when next_row_first_kernel_rom; + +} + +########################################################################################## +# CHIPLET SELECTOR SYSTEM +########################################################################################## + +# Hierarchical chiplet selector constraints +# +# CONSTRAINT DEGREE: 2 (quadratic due to binary constraints) +# +ev chiplet_selectors([s[5]]) { + #################################################################################### + # BINARY CONSTRAINTS - Ensure all selectors are valid binary values + #################################################################################### + + enf is_binary([s[0]]); + + enf is_binary([s[1]]) when s[0]; + enf is_binary([s[2]]) when s[0] & s[1]; + enf is_binary([s[3]]) when s[0] & s[1] & s[2]; + enf is_binary([s[4]]) when s[0] & s[1] & s[2] & s[3]; + + #################################################################################### + # STABILITY CONSTRAINTS - Prevent deactivation (forbids 1→0 transitions) + #################################################################################### + + # Once a selector level becomes active (1), it must remain active + # This ensures chiplet operations maintain consistent state throughout execution + enf s[0]' = s[0] when s[0]; + enf s[1]' = s[1] when s[0] & s[1]; + enf s[2]' = s[2] when s[0] & s[1] & s[2]; + enf s[3]' = s[3] when s[0] & s[1] & s[2] & s[3]; + enf s[4]' = s[4] when s[0] & s[1] & s[2] & s[3] & s[4]; +} + +########################################################################################## +# CHIPLET ACTIVATION FUNCTIONS +########################################################################################## + +# These functions decode the hierarchical selector pattern to identify active chiplets. +# Each chiplet activates when its selector pattern matches and the next level is inactive. + +# Hasher chiplet: Active when root selector is inactive +fn hasher_chiplet_flag(s_0: felt) -> felt { + return !s_0; +} + +# Bitwise chiplet: Active when s0=1, s1=0 +fn bitwise_chiplet_flag(s_0: felt, s_1: felt) -> felt { + return s_0 * !s_1; +} + +# Memory chiplet: Active when s0=1, s1=1, s2=0 +fn memory_chiplet_flag(s_0: felt, s_1: felt, s_2: felt) -> felt { + return s_0 * s_1 * !s_2; +} + +# ACE chiplet: Active when s0=1, s1=1, s2=1, s3=0 +fn ace_chiplet_flag(s_0: felt, s_1: felt, s_2: felt, s_3: felt) -> felt { + return s_0 * s_1 * s_2 * !s_3; +} + +# Kernel ROM chiplet: Active when s0=1, s1=1, s2=1, s3=1, s4=0 +fn ker_rom_chiplet_flag(s_0: felt, s_1: felt, s_2: felt, s_3: felt, s_4: felt) -> felt { + return s_0 * s_1 * s_2 * s_3 * !s_4; +} diff --git a/constraints/decoder.air b/constraints/decoder.air new file mode 100644 index 000000000..6a20ea287 --- /dev/null +++ b/constraints/decoder.air @@ -0,0 +1,14 @@ +########################################################################################## +# DECODER CONSTRAINTS +########################################################################################## +# +# Miden VM program decoder is responsible for ensuring that a program with a given MAST +# root is executed by the VM. +# +# STATUS: Not implemented +# +# REFERENCES: +# - Decoder Design: https://0xmiden.github.io/miden-vm/design/decoder/main.html +########################################################################################## + +mod decoder diff --git a/constraints/hasher.air b/constraints/hasher.air new file mode 100644 index 000000000..5d92137f4 --- /dev/null +++ b/constraints/hasher.air @@ -0,0 +1,257 @@ +########################################################################################## +# HASHER CONSTRAINTS MODULE +########################################################################################## +# +# The Hasher module is responsible for all hash-related operations, which includes: +# +# 1. A single permutation of Rescue Prime Optimized (RPO). +# 2. A simple 2-to-1 hash. +# 3. A linear hash of n field elements. +# 4. Merkle path verification. +# 5. Merkle root update. +# +# STATUS: Partially implemented (missing bus interactions) +# +# REFERENCES: +# - Hasher chiplet design: https://0xmiden.github.io/miden-vm/design/chiplets/hasher.html +########################################################################################## + +mod hasher + +use utils::*; +use rpo::enforce_rpo_round; + +########################################################################################## +# HASHER CHIPLET TRANSITION CONSTRAINTS +########################################################################################## + +# Enforces the constraints on the hash chiplet given its columns. +ev hash_chiplet([s[3], h[12], i]) { + # Selector columns constraints + enf selector_columns([s]); + + # Node index constraints + enf node_index([s, i]); + + # Hasher state constraints + enf hasher_state([s, h, i]); +} + +########################################################################################## +# HELPER EVALUATORS +########################################################################################## + +# Enforce selector columns constraints +ev selector_columns([s[3]]) { + # Enforce that selector columns are binary. + enf is_binary([selector]) for selector in s; + + # Compute relevant flags (passing periodic column values as parameters) + let f_abp = get_f_abp(s, cycle_row_7); + let f_mpa = get_f_mpa(s, cycle_row_7); + let f_mva = get_f_mva(s, cycle_row_7); + let f_mua = get_f_mua(s, cycle_row_7); + let f_out = get_f_out(s, cycle_row_7); + let f_out_next = get_f_out_next(s, cycle_row_6, s[0]', s[1]'); + + # Enforce that unless f_out = 1 or f_out' = 1, the values in columns s[1] and s[2] are copied + # over to the next row. + # This encodes the fact that we can change the op flags only at the end of a cycle in order + # to output a result, or at the start of a new cycle to initiate a new operation. + enf is_unchanged([s[1]]) when !f_out & !f_out_next; + enf is_unchanged([s[2]]) when !f_out & !f_out_next; + + # Flag that is true when the performed operation is one of the operations represented by flags + # f_abp, f_mpa, f_mva or f_mua + let f_comp = f_abp + f_mpa + f_mva + f_mua; + + # Enforce that if any of f_abp, f_mpa, f_mva, f_mua flags is set to 1, the next value of s[0] + # is 0. + # This basically enforces the exclusion of all op which initiate a new op (at the start of a new + # cycle). Note that f_comp is a flag that is set only on rows which are 1 less than a multiple of 8 + # and hence the following constrains the 0-th selector at the start of a new cycle. + enf s[0]' = 0 when f_comp; + + # Enforce that no invalid combinations of flags are allowed. + # This enforces that if s[0] is 0 then the either f_hout or f_sout is set. + enf s[1] = 0 when binary_and(cycle_row_7, binary_not(s[0])); +} + +# Enforce node index constraints +ev node_index([s[3], i]) { + # Compute relevant flags (passing periodic column values as parameters) + let f_mp = get_f_mp(s, cycle_row_0); + let f_mv = get_f_mv(s, cycle_row_0); + let f_mu = get_f_mu(s, cycle_row_0); + let f_mpa = get_f_mpa(s, cycle_row_7); + let f_mva = get_f_mva(s, cycle_row_7); + let f_mua = get_f_mua(s, cycle_row_7); + let f_out = get_f_out(s, cycle_row_7); + + # Flag indicating to enforce the constraint that b is binary only when a new node is absorbed into + # the hasher state (when the hash operation is either one of Merkle path verification or + # Merkle root update) + let f_an = f_mp + f_mv + f_mu + f_mpa + f_mva + f_mua; + + # b is the value of the bit which is discarded during shift by one bit to the right. + let b = i - 2 * i'; + + # Enforce that b is binary only when a new node is absorbed into the hasher state. + enf b^2 - b = 0 when f_an; + + # Enforce that when a computation is finished i = 0. + enf i = 0 when f_out; + + # Enforce that the value in i is copied over to the next row unless we are absorbing a new row + # or the computation is finished. + let not_absorbing_nor_comp_finished = 1 - (f_an + f_out); + enf is_unchanged([i]) when not_absorbing_nor_comp_finished; +} + +# Enforce hasher state constraints +ev hasher_state([s[3], h[12], i]) { + # Enforce the RPO permutation round constraints + enf enforce_rpo_round([h]) when !cycle_row_7; + + # Compute relevant flags (passing periodic column values as parameters) + let f_mp = get_f_mp(s, cycle_row_0); + let f_mv = get_f_mv(s, cycle_row_0); + let f_mu = get_f_mu(s, cycle_row_0); + let f_abp = get_f_abp(s, cycle_row_7); + + # Flag that is true when the performed operation includes absorbing the next node during Merkle + # path computation. + let f_absorb_node = f_mp + f_mv + f_mu; + + # b is the value of the bit which is discarded during shift by one bit to the right. + let b = i - 2 * i'; + + # Enforce that when absorbing the next set of elements into the state during linear hash + # computation (i.e. f_abp = 1) the first 4 elements (the capacity portion) are carried over to + # the next row. + enf f_abp * (h' - h) = 0 for h in h; + + # TODO: Double check the following and fix both docs and VM if there is a typo + # + # Enforce that when absorbing the next node during Merkle path computation + # (i.e. f_mp + f_mv + f_mu = 1), the result of the previous hash (h[4], ..., h[7]) are copied + # over either to (h[4]', ..., h[7]') or to (h[8]', ..., h[11]') depending on the value of b. + # + # TODO: uncomment when computed indices are supported + # enf match { + # !b & f_absorb_node: is_unchanged(h[j + 4]) for j in 0..4, + # b & f_absorb_node: h[j + 8]' = h[j + 4] for j in 0..4 + # } +} + +########################################################################################## +# HELPER FUNCTIONS +########################################################################################## + +########################################################################################## +# INSTRUCTION FLAGS - DETAILED DESCRIPTIONS +########################################################################################## +# +# The hasher chiplet uses selector columns s[0], s[1], s[2] to encode different operations: +# +# INITIALIZATION FLAGS (on rows which are multiples of 8 - cycle_row_0): +# • f_bp: (1,0,0) - Begin Permutation +# Initiates: single permutation, 2-to-1 hash, or linear hash computation +# • f_mp: (1,0,1) - Merkle Path verification +# Starts standard Merkle path verification computation +# • f_mv: (1,1,0) - Merkle path Verification for "old" node +# Begins verification for old leaf value during Merkle root update +# • f_mu: (1,1,1) - Merkle path verification for "new" node +# Starts verification for new leaf value during Merkle root update +# +# ABSORPTION FLAGS (on rows 1 less than multiple of 8 - cycle_row_7): +# • f_abp: (1,0,0) - Absorb elements for linear hash (continuing computation) +# Absorbs next set of elements into hasher state during linear hash +# • f_mpa: (1,0,1) - Merkle Path Absorb during standard verification +# Absorbs next Merkle path node during standard verification +# • f_mva: (1,1,0) - Merkle path absorb for "old" node verification +# Absorbs next node during "old" leaf verification (Merkle root update) +# • f_mua: (1,1,1) - Merkle path absorb for "new" node verification +# Absorbs next node during "new" leaf verification (Merkle root update) +# +# OUTPUT FLAGS (on rows 1 less than multiple of 8 - cycle_row_7): +# • f_hout: (0,0,0) - Hash Output +# Returns the result of the currently running hash computation +# • f_sout: (0,0,1) - State Output +# Returns the entire 12-element hasher state +# • f_out: Combined flag (f_hout | f_sout) - any output operation +# +########################################################################################## + +# f_mp: Merkle Path verification flag (1,0,1) on cycle_row_0 +# Initiates standard Merkle path verification computation. +fn get_f_mp(s: felt[3], row0: felt) -> felt { + return row0 & s[0] & binary_not(s[1]) & s[2]; +} + +# f_mv: Merkle path Verification for "old" node flag (1,1,0) on cycle_row_0 +# Begins verification for old leaf value during Merkle root update computation. +fn get_f_mv(s: felt[3], row0: felt) -> felt { + return row0 & s[0] & s[1] & binary_not(s[2]); +} + +# f_mu: Merkle path verification for "new" node flag (1,1,1) on cycle_row_0 +# Starts verification for new leaf value during Merkle root update computation. +fn get_f_mu(s: felt[3], row0: felt) -> felt { + return row0 & s[0] & s[1] & s[2]; +} + +# f_abp: Absorb elements for linear hash flag (1,0,0) on cycle_row_7 +# Absorbs next set of elements into hasher state during linear hash computation. +fn get_f_abp(s: felt[3], row7: felt) -> felt { + return row7 & s[0] & binary_not(s[1]) & binary_not(s[2]); +} + +# f_mpa: Merkle Path Absorb flag (1,0,1) on cycle_row_7 +# Absorbs next Merkle path node during standard verification computation. +fn get_f_mpa(s: felt[3], row7: felt) -> felt { + return row7 & s[0] & binary_not(s[1]) & s[2]; +} + +# f_mva: Merkle path absorb for "old" node flag (1,1,0) on cycle_row_7 +# Absorbs next node during "old" leaf verification (Merkle root update computation). +fn get_f_mva(s: felt[3], row7: felt) -> felt { + return row7 & s[0] & s[1] & binary_not(s[2]); +} + +# f_mua: Merkle path absorb for "new" node flag (1,1,1) on cycle_row_7 +# Absorbs next node during "new" leaf verification (Merkle root update computation). +fn get_f_mua(s: felt[3], row7: felt) -> felt { + return row7 & s[0] & s[1] & s[2]; +} + +# We can define two flags: +# 1. Flag f_hout = cycle_row_7 & binary_not(s[0]) & binary_not(s[1]) & binary_not(s[2]), +# which is set to 1 when selector flags are (0,0,0) on rows which are 1 less than a multiple +# of 8. This flag is for the instruction that returns the resulting digest of the currently +# running computation. +# 2. Flag f_sout = cycle_row_7 & binary_not(s[0]) & binary_not(s[1]) & s[2], which is set to 1 +# when selector flags are (0,0,1) on rows which are 1 less than a multiple of 8. This flag is +# for the instruction that returns the whole hasher state. +# +# Flag f_out is set to 1 when either f_hout = 1 or f_sout = 1 in the current row. +fn get_f_out(s: felt[3], row7: felt) -> felt { + return row7 & binary_not(s[0]) & binary_not(s[1]); +} + +# Flag f_out_next is set to 1 when either f_hout = 1 or f_sout = 1 in the next row. +fn get_f_out_next(s: felt[3], row6: felt, s0_next: felt, s1_next: felt) -> felt { + return row6 & binary_not(s0_next) & binary_not(s1_next); +} + +########################################################################################## +# PERIODIC COLUMNS +########################################################################################## +# +# There are 3 periodic columns used to help select the instruction executed at a given row +# +periodic_columns { + cycle_row_0: [1, 0, 0, 0, 0, 0, 0, 0], + cycle_row_6: [0, 0, 0, 0, 0, 0, 1, 0], + cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1], +} diff --git a/constraints/kernel_rom.air b/constraints/kernel_rom.air new file mode 100644 index 000000000..49b83f463 --- /dev/null +++ b/constraints/kernel_rom.air @@ -0,0 +1,77 @@ +########################################################################################## +# KERNEL ROM CHIPLET +########################################################################################## +# +# The Kernel ROM chiplet is responsible for tracking execution of kernel (system) calls. +# It maintains a record of all kernel procedure digests and ensures proper initialization +# of kernel procedures while preserving privacy about call frequency. +# +# The chiplet contains digest values for all kernel procedures and enforces contiguity +# constraints to ensure proper execution tracking. +# +# STATUS: Core constraints implemented, bus constraints not implemented +# +# REFERENCES: +# - Kernel ROM Chiplet: https://0xmiden.github.io/miden-vm/design/chiplets/kernel_rom.html +########################################################################################## + +mod kernel_rom + +use utils::*; + +########################################################################################## +# KERNEL ROM CHIPLET TRANSITION CONSTRAINTS +########################################################################################## + +# Enforces the constraints on the kernel ROM chiplet given its columns. +# +# Parameters: +# - s4: Chiplet selector flag +# - sfirst: Section first flag (1 = start of new digest block, 0 = continuation of a given block) +# - r[4]: Kernel procedure root/digest (4 field elements) +# +# Max constraint degree: 3 +ev ker_rom_chiplet_constraints([s4, sfirst, r[4]]) { + enf kernel_rom_selector([sfirst]); + enf kernel_rom_digest_contiguity([s4, sfirst, r]); +} + +# Enforces initialization constraints for the first row of kernel ROM chiplet execution. +# +# According to the official specification, the first row must have sfirst = 1 to ensure +# proper digest matching and initialization of kernel procedure tracking. +# +# Max constraint degree: 1 +ev kernel_rom_chiplet_constraints_first_row([s4, sfirst, r[4]]) { + # FIRST ROW INITIALIZATION CONSTRAINT: + # The first row of any kernel ROM chiplet execution must have sfirst' = 1 + # This ensures proper initialization of kernel procedure digest tracking. + # Without this, the chiplet could start in an invalid intermediate state. + enf sfirst' = 1; +} + +########################################################################################## +# HELPERS +########################################################################################## + +# Enforces that the kernel ROM selector is valid. +# +# Max constraint degree: 2 +ev kernel_rom_selector([sfirst]) { + # Enforce that sfirst is binary (0 or 1) + enf is_binary([sfirst]); +} + +# Enforces digest contiguity constraints for the kernel ROM. +# +# When sfirst' = 0 (not starting a new digest block), the digest values must remain +# unchanged from the current row to the next row. This ensures contiguous blocks of +# identical digest values for proper tracking of kernel procedure executions. +# +# Max constraint degree: 3 +ev kernel_rom_digest_contiguity([s4, sfirst, r[4]]) { + # Constraint is active when: + # - sfirst' = 0 (next row is not the start of a new digest block) + # - s4' = 0 (next row is still within the kernel ROM chiplet) + enf is_unchanged([r_i]) for r_i in r when binary_and(binary_not(s4'), binary_not(sfirst')); +} diff --git a/constraints/memory.air b/constraints/memory.air new file mode 100644 index 000000000..efb9579d4 --- /dev/null +++ b/constraints/memory.air @@ -0,0 +1,237 @@ +########################################################################################## +# MEMORY CONSTRAINTS MODULE +########################################################################################## +# +# The Memory chiplet provides linear read-write random access memory for the Miden VM. +# Memory is element-addressable with addresses in range [0, 2^32), supporting both individual +# element access and optimized word-aligned batch operations (4 elements per word). +# +# MEMORY TABLE LAYOUT: +# ┌─────────────────┬────────────────────────────────────────────────────────────────┐ +# │ Column │ Purpose │ +# ├─────────────────┼────────────────────────────────────────────────────────────────┤ +# │ is_read │ Read/write selector: 1=read, 0=write │ +# │ is_word_access │ Element/word access selector: 0=element, 1=word │ +# │ ctx │ Context ID for execution context separation │ +# │ addr │ Memory address (word-aligned for word access) │ +# │ idx0/1 │ Element index within word [0,3] - binary decomposition │ +# │ clk │ Clock cycle when operation occurred │ +# │ v0-v3 │ Four field elements stored in memory word │ +# │ d0/d1 │ Delta tracking columns for monotonicity verification │ +# │ d_inv │ Inverse delta column for consecutive transitions │ +# │ f_scw │ Same context/word flag for sequential access optimization │ +# └─────────────────┴────────────────────────────────────────────────────────────────┘ +# +# STATUS: Partially implemented (missing bus integration) +# +# REFERENCES: +# - Memory Design: https://0xmiden.github.io/miden-vm/design/chiplets/memory.html +########################################################################################## + +mod memory + +use utils::*; + +########################################################################################## +# MEMORY CHIPLET CONSTRAINTS +########################################################################################## + +# Enforces proper memory initialization when entering memory chiplet +ev memory_chiplet_constraints_first_row([memory[15]]) { + let is_read = memory[0]; # Read(1)/Write(0) selector + let is_word_access = memory[1]; # Element(0)/Word(1) access selector + let ctx = memory[2]; # Context ID + let addr = memory[3]; # Memory address + let idx0 = memory[4]; # Element index bit 0 + let idx1 = memory[5]; # Element index bit 1 + let v0 = memory[7]; # Memory value 0 + let v1 = memory[8]; # Memory value 1 + let v2 = memory[9]; # Memory value 2 + let v3 = memory[10]; # Memory value 3 + + let is_constrained_value = compute_element_access_flags(idx0', idx1', is_read', is_word_access'); + + # Enforce that when v'[i] is not written to, then v'[i] must be 0. + enf v0' = 0 when is_constrained_value[0]; + enf v1' = 0 when is_constrained_value[1]; + enf v2' = 0 when is_constrained_value[2]; + enf v3' = 0 when is_constrained_value[3]; +} + +# Enforces constraints that apply to every row in the memory chiplet +# These are basic validity constraints for selectors and indices +ev memory_chiplet_constraints_all_rows([memory[15]]) { + let is_read = memory[0]; # Read(1)/Write(0) selector + let is_word_access = memory[1]; # Element(0)/Word(1) access selector + let idx0 = memory[4]; # Element index bit 0 + let idx1 = memory[5]; # Element index bit 1 + + # Read/write selector must be binary + enf is_binary([is_read]); + + # Element/word access selector must be binary + enf is_binary([is_word_access]); + + # Index bit 0 must be binary + enf is_binary([idx0]); + + # Index bit 1 must be binary + enf is_binary([idx1]); +} + +# Enforces memory state transition constraints for all rows except the final row +# Includes monotonicity, value consistency, and proper read/write semantics +ev memory_chiplet_constraints_all_rows_except_last([memory[15]]) { + let is_read = memory[0]; # Read(1)/Write(0) selector + let is_word_access = memory[1]; # Element(0)/Word(1) access selector + let ctx = memory[2]; # Context ID + let addr = memory[3]; # Memory address + let idx0 = memory[4]; # Element index bit 0 + let idx1 = memory[5]; # Element index bit 1 + let clk = memory[6]; # Clock cycle + let v0 = memory[7]; # Memory value 0 + let v1 = memory[8]; # Memory value 1 + let v2 = memory[9]; # Memory value 2 + let v3 = memory[10]; # Memory value 3 + let d0 = memory[11]; # Context delta + let d1 = memory[12]; # Address delta + let d_inv = memory[13]; # Delta inverse + let f_scw = memory[14]; # Same context/word flag + + # Delta inverse constraints + enf enforce_d_inv([ctx, addr, clk, d0, d1, d_inv]); + + # Context/address/clock delta constraints + enf enforce_delta([ctx, addr, clk, d0, d1, d_inv]); + + # Same context/word flag constraints + enf enforce_flag_same_context_and_word([ctx, addr, d_inv, f_scw]); + + # Same context/word/addr/clock access constraints + enf enforce_same_context_word_addr_and_clock([is_read, clk, f_scw, d_inv]); + + # Memory value constraints + enf enforce_values_consistency([is_read, is_word_access, idx0, idx1, v0, v1, v2, v3, f_scw]); +} + +########################################################################################## +# HELPER EVALUATORS +########################################################################################## + +# Constrains the delta inverse column +ev enforce_d_inv([ctx, addr, clk, d0, d1, d_inv]) { + let ctx_delta = ctx' - ctx; + let addr_delta = addr' - addr; + let is_ctx_changed = ctx_delta * d_inv'; + let is_addr_changed = addr_delta * d_inv'; + + # is_ctx_changed is binary + enf binary_constraint(is_ctx_changed) = 0; + + # When context changes, is_ctx_changed must be 1 + enf ctx_delta = 0 when !is_ctx_changed; + + # When is_ctx_changed is 0 then is_addr_changed is binary + enf binary_constraint(is_addr_changed) = 0 when !is_ctx_changed; + + # When is_ctx_changed and is_addr_changed are both 0, then address must not change + enf addr_delta = 0 when binary_not(is_ctx_changed) * binary_not(is_addr_changed); +} + +# Enforces monotonicity constraints for context, address, and clock transitions +ev enforce_delta([ctx, addr, clk, d0, d1, d_inv]) { + let ctx_delta = ctx' - ctx; + let addr_delta = addr' - addr; + let clk_delta = clk' - clk; + let delta_next = d1' * 2^16 + d0'; + let is_ctx_changed = ctx_delta * d_inv'; + let is_addr_changed = addr_delta * d_inv'; + + enf is_ctx_changed * ctx_delta + binary_not(is_ctx_changed) * (is_addr_changed * addr_delta + binary_not(is_addr_changed) * clk_delta) = delta_next; +} + +# Enforces correct f_scw flag computation +ev enforce_flag_same_context_and_word([ctx, addr, d_inv, f_scw]) { + let ctx_delta = ctx' - ctx; + let addr_delta = addr' - addr; + let is_ctx_changed = ctx_delta * d_inv'; + let is_addr_changed = addr_delta * d_inv'; + + enf f_scw' = binary_not(is_ctx_changed) * binary_not(is_addr_changed); +} + +# Enforces that accesses to same context, word address, and clock must be reads +ev enforce_same_context_word_addr_and_clock([is_read, clk, f_scw, d_inv]) { + let clk_delta = clk' - clk; + let clk_no_change = binary_not(clk_delta * d_inv'); + + enf f_scw' * clk_no_change * binary_not(is_read) * binary_not(is_read') = 0; +} + +# Enforces memory value consistency, and proper read/write semantics +ev enforce_values_consistency([is_read, is_word_access, idx0, idx1, v0, v1, v2, v3, f_scw]) { + let is_constrained_value = compute_element_access_flags(idx0', idx1', is_read', is_word_access'); + + # Non-first row constraints: if v[i]' is not written to and, + # - (f_scw' = 1) then its value needs to be copied over from the previous row, + # - (f_scw' = 0) then its value needs to be set to 0. + enf f_scw' * (v0' - v0) + binary_not(f_scw') * v0' = 0 when is_constrained_value[0]; + enf f_scw' * (v1' - v1) + binary_not(f_scw') * v1' = 0 when is_constrained_value[1]; + enf f_scw' * (v2' - v2) + binary_not(f_scw') * v2' = 0 when is_constrained_value[2]; + enf f_scw' * (v3' - v3) + binary_not(f_scw') * v3' = 0 when is_constrained_value[3]; +} + +########################################################################################## +# HELPER FUNCTIONS +########################################################################################## + +# Memory chiplet active flag +fn flag_all_rows(s0: felt, s1: felt, s2: felt) -> felt { + return s0 * s1 * binary_not(s2); +} + +# Memory chiplet active flag for next row +fn flag_all_rows_next(s0: felt, s1: felt, s2: felt) -> felt { + return s0' * s1' * binary_not(s2'); +} + +# Memory chiplet active in current row and row is not the last one of the memory chiplet +fn flag_memory_active_not_last_row(s0: felt, s1: felt, s2: felt) -> felt { + return s0 * s1 * binary_not(s2'); +} + +# First row of memory chiplet (transitioning from bitwise to memory) +fn flag_next_row_first_row_memory(s0: felt, s1: felt, s2: felt) -> felt { + return (1 - s1) * flag_all_rows_next(s0, s1, s2); +} + +# Computes constraint flag: 1 if value needs to be constrained, 0 otherwise +fn compute_constrained_values(is_accessed_i: felt, is_read_next: felt, is_word_access_next: felt) -> felt { + let z_i = binary_not(is_word_access_next) * binary_not(is_accessed_i); + return is_read_next + binary_not(is_read_next) * z_i; +} + +# Computes which memory elements need to be constrained based on access pattern +# Returns array of 4 flags indicating whether each element (v0-v3) needs constraining +# +# is_constrainted_value_i is set to 1 when `v'[i]` is not written to, and 0 otherwise. +# +# In other words, is_constrainted_value_i is set to 1 when `v'[i]` needs to be constrained (to either 0 or `v[i]`). +# +# Note that `is_constrainted_value_i` only uses values in the "next" row. This is because it must be used to +# constrain the first row of the memory chiplet, where that row sits in the "next" position of +# the frame, and the "current" row belongs to the previous chiplet (and hence the "current" row +# must not be accessed). +# +# As a result, `is_constrainted_value_i` does not include the constraint of being in the memory chiplet, or in the +# same context and word - these must be enforced separately. +fn compute_element_access_flags(idx0_next: felt, idx1_next: felt, is_read_next: felt, is_word_access_next: felt) -> felt[4] { + # Element selection flags: is_accessed[i] = 1 when element index (2*idx1 + idx0) equals i + let is_accessed_0 = binary_not(idx1_next) * binary_not(idx0_next); + let is_accessed_1 = binary_not(idx1_next) * idx0_next; + let is_accessed_2 = idx1_next * binary_not(idx0_next); + let is_accessed_3 = idx1_next * idx0_next; + + let is_accessed = [is_accessed_0, is_accessed_1, is_accessed_2, is_accessed_3]; + return [compute_constrained_values(is_accessed_i, is_read_next, is_word_access_next) for is_accessed_i in is_accessed]; +} diff --git a/constraints/miden-vm-old/bitwise.air b/constraints/miden-vm-old/bitwise.air new file mode 100644 index 000000000..8c186367f --- /dev/null +++ b/constraints/miden-vm-old/bitwise.air @@ -0,0 +1,114 @@ +mod BitwiseAir + +### Constants and periodic columns ################################################################ + +periodic_columns { + k0: [1, 0, 0, 0, 0, 0, 0, 0] + k1: [1, 1, 1, 1, 1, 1, 1, 0] +} + + +### Helper functions ############################################################################## + +# Returns value aggregated from limbs. +fn aggregate(limb: vector[4]) -> scalar: + return sum([2^i * a for (i, a) in (0..4, limb)]) + + +### Helper evaluators ############################################################################# + +# Enforces that column must be binary. +# +# Constraint degree: 2 +ev is_binary([a]) { + enf a^2 = a +} + + +# Enforces that the bitwise selector is valid. +# +# Max constraint degree: 2 +ev bitwise_selector([s]) { + # Enforce that selector must be binary. + # Constraint degree: 2 + enf is_binary([s]) + + # Enforce that selector should stay the same throughout the cycle. + # Constraint degree: 2 + enf s' = s when k1 +} + + +# Enforces that the input to the bitwise chiplet is decomposed into limbs correctly. +# +# Max constraint degree: 2 +ev input_decomposition([a, b, a_limb[4], b_limb[4]]) { + # Enforce that the input is decomposed into valid bits. + # Constraints degree: 2 + enf is_binary([a]) for a in a_limb + enf is_binary([b]) for b in b_limb + + # Enforce that the value in the first row of column `a` of the current 8-row cycle should be + # the aggregation of the decomposed bit columns `a_limb`. + let a_aggr = aggregate(a_limb) + # Constraint degree: 2 + enf a = a_aggr when k0 + + # Enforce that the value in the first row of column `b` of the current 8-row cycle should be + # the aggregation of the decomposed bit columns `b_limb`. + let b_aggr = aggregate(b_limb) + # Constraint degree: 2 + enf b = b_aggr when k0 + + # Enforce that for all rows in an 8-row cycle, except for the last one, the values in a and b + # columns are increased by the values contained in the individual bit columns a_limb and + # b_limb. + # Constraints degree: 2 + enf a' = a * 16 + a_aggr when k1 + enf b' = b * 16 + b_aggr when k1 +} + + +# Enforces that the output of the bitwise operation is aggregated correctly from the decomposed +# limbs. +# +# Max constraint degree: 3 +ev output_aggregation([s, a, b, a_limb[4], b_limb[4], zp, z]) { + # Enforce that in the first row, the aggregated output value of the previous row should be 0. + # Constraint degree: 2 + enf zp = 0 when k0 + + # Enforce that for each row except the last, the aggregated output value must equal the + # previous aggregated output value in the next row. + # Constraint degree: 2 + enf zp' = z when k1 + + # Enforce that for all rows the value in the z column is computed by multiplying the previous + # output value (from the zp column in the current row) by 16 and then adding it to the bitwise + # operation applied to the row's set of bits of a_limb and b_limb. The entire constraint must + # also be multiplied by the operation selector flag to ensure it is only applied for the + # appropriate operation. The constraint for AND is enforced when s = 0 and the constraint for + # XOR is enforced when s = 1. Because the selectors for the AND and XOR operations are mutually + # exclusive, the constraints for different operations can be aggregated into the same result + # indices. + # Constraints degree: 3 + let a_and_b = sum([2^i * a * b for (i, a, b) in (0..4, a_limb, b_limb)]) + let a_xor_b = sum([2^i * (a + b - 2 * a * b) for (i, a, b) in (0..4, a_limb, b_limb)]) + match enf: + z = zp * 16 + a_xor_b when s + z = zp * 16 + a_and_b when !s +} + + +### Bitwise Chiplet Air Constraints ############################################################### + +# Enforces the constraints on the bitwise chiplet, given the columns of the bitwise execution +# trace. +# +# Max constraint degree: 4 +ev bitwise_chiplet([s, a, b, a_limb[4], b_limb[4], zp, z]) { + enf bitwise_selector([s]) + enf input_decomposition([a, b, a_limb, b_limb]) + enf output_aggregation([s, a, b, a_limb, b_limb, zp, z]) + # Bus constraint is implemented in a separate file +} diff --git a/constraints/miden-vm-old/chiplets.air b/constraints/miden-vm-old/chiplets.air new file mode 100644 index 000000000..2cc397ed2 --- /dev/null +++ b/constraints/miden-vm-old/chiplets.air @@ -0,0 +1,38 @@ +mod ChipletsConstraintsAir + +use bitwise::bitwise_chiplet +use hash::hash_chiplet +use memory::memory_chiplet + +### Helper evaluators ############################################################################# + +# Enforces that the provided columns must be binary. +ev is_binary([a]) { + enf a^2 = a +} + +# Enforces that the chiplet selector columns are set correctly. +ev chiplet_selectors([s[3]]) { + # Enforce that selectors are binary. + enf is_binary([s[0]]) + enf is_binary([s[1]]) when s[0] + enf is_binary([s[2]]) when s[0] & s[1] + + # Enforce that the chiplets are stacked correctly by restricting selector values so they can + # only change from 0 to 1. + enf s[0]' = s[0] when s[0] + enf s[1]' = s[1] when s[0] & s[1] + enf s[2]' = s[2] when s[0] & s[1] & s[2] +} + +### Chiplets Constraints ########################################################################## + +# Enforce the constraints on the hash, bitwise or memory chiplet, given the columns of the chiplet +# module trace. +ev chiplets([s[3], chiplet_columns[15]]) { + enf chiplet_selectors([s]) + match enf: + hash_chiplet([s[1], s[2], chiplet_columns]) when !s[0] + bitwise_chiplet([s[2], chiplet_columns]) when s[0] & !s[1] + memory_chiplet([chiplet_columns]) when s[0] & s[1] & !s[2]' +} \ No newline at end of file diff --git a/constraints/miden-vm-old/decoder.air b/constraints/miden-vm-old/decoder.air new file mode 100644 index 000000000..cdab70682 --- /dev/null +++ b/constraints/miden-vm-old/decoder.air @@ -0,0 +1,654 @@ +mod DecoderAir + +### Constants and periodic columns ################################################################ + +const HASHER_LINEAR_HASH = 3 +const HASHER_RETURN_HASH = 1 + +periodic_columns { + cycle_row_0: [1, 0, 0, 0, 0, 0, 0, 0] + cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1] +} + +### Helper functions ############################################################################## + +# Returns the f_join operation flag which is set when JOIN control operation is executed. +# +# Flag degree: 6 +fn get_f_join(b: vector[7]) -> scalar: + return b[6] & !b[5] & b[4] & b[3] & !b[2] & b[1] + + +# Returns the f_split operation flag which is set when SPLIT control operation is executed. +# +# Flag degree: 6 +fn get_f_split(b: vector[7]) -> scalar: + return b[6] & !b[5] & b[4] & b[3] & b[2] & !b[1] + + +# Returns the f_loop operation flag which is set when LOOP control operation is executed. +# +# Flag degree: 6 +fn get_f_loop(b: vector[7]) -> scalar: + return b[6] & !b[5] & b[4] & b[3] & b[2] & b[1] + + +# Returns the f_repeat operation flag which is set when REPEAT operation is executed. +# +# Flag degree: 4 +fn get_f_repeat(b: vector[7], extra: scalar) -> scalar: + return extra & b[4] & !b[3] & b[2] + + +# Returns the f_span operation flag which is set when SPAN operation is executed. +# +# Flag degree: 6 +fn get_f_span(b: vector[7]) -> scalar: + return b[6] & !b[5] & b[4] & b[3] & !b[2] & !b[1] + + +# Returns the f_respan operation flag which is set when RESPAN operation is executed. +# +# Flag degree: 4 +fn get_f_respan(b: vector[7], extra: scalar) -> scalar: + return extra & b[4] & b[3] & !b[2] + + +# Returns the f_call operation flag which is set when CALL control operation is executed. +# +# Flag degree: 4 +fn get_f_call(b: vector[7], extra: scalar) -> scalar: + return extra & !b[4] & b[3] & b[2] + + +# Returns the f_syscall operation flag which is set when SYSCALL control operation is executed. +# +# Flag degree: 4 +fn get_f_syscall(b: vector[7], extra: scalar) -> scalar: + return extra & !b[4] & b[3] & !b[2] + + +# Returns the f_end operation flag which is set when END operation is executed. +# +# Flag degree: 4 +fn get_f_end(b: vector[7], extra: scalar) -> scalar: + return extra & b[4] & !b[3] & !b[2] + + +# Returns the f_halt operation flag which is set when HALT operation is executed. +# +# Flag degree: 4 +fn get_f_halt(b: vector[7], extra: scalar) -> scalar: + return extra & b[4] & b[3] & b[2] + + +# Returns the f_push operation flag which is set when PUSH operation is executed. +# +# Flag degree: 4 +fn get_f_push(b: vector[7], extra: scalar) -> scalar: + return extra & !b[4] & !b[3] & b[2] + + +# Returns the f_ctrl flag which is set when any one of the control flow operations (JOIN, SPLIT, +# LOOP, REPEAT, SPAN, RESPAN, CALL, SYSCALL, END, HALT) is being executed. +# +# Flag degree: 4 +fn get_f_ctrl(b: vector[7], extra: scalar) -> scalar: + # flag for SPAN, JOIN, SPLIT, LOOP + let f_sjsl = b[6] & !b[5] & b[4] & b[3] + + # flag for END, REPEAT, RESPAN, HALT + let f_errh = b[6] & b[5] & b[4] + + return f_sjsl + f_errh + get_f_call(b, extra) + get_f_syscall(b, extra) + + +# Returns f_ctrli flag which is set to 1 when a control flow operation that signifies the +# initialization of a control block (JOIN, SPLIT, LOOP, CALL, SYSCALL) is being executed on the VM. +# +# Flag degree: 6 +fn get_f_ctrli(b: vector[7], extra: scalar) -> scalar: + return get_f_join(b) + get_f_split(b) + get_f_loop(b) + get_f_call(b, extra) + get_f_syscall(b, extra) + + +# Returns transition label, composed of the operation label and the periodic columns that uniquely +# identify each transition function. +fn get_transition_label(op_label: scalar) -> scalar: + return op_label + 2^4 * cycle_row_7 + 2^5 * cycle_row_0 + + +# Returns f_g8 flag which is set to 1 if there are 8 operation groups in the batch. +fn get_f_g8(op_batch_flags: vector[3]) -> scalar: + return op_batch_flags[0] + + +# Returns f_g4 flag which is set to 1 if there are 4 operation groups in the batch. +fn get_f_g4(op_batch_flags: vector[3]) -> scalar: + return !op_batch_flags[0] & op_batch_flags[1] & op_batch_flags[2] + + +# Returns f_g2 flag which is set to 1 if there are 2 operation groups in the batch. +fn get_f_g2(op_batch_flags: vector[3]) -> scalar: + return !op_batch_flags[0] & !op_batch_flags[1] & op_batch_flags[2] + + +# Returns f_g1 flag which is set to 1 if there are 1 operation groups in the batch. +fn get_f_g1(op_batch_flags: vector[3]) -> scalar: + return !op_batch_flags[0] & op_batch_flags[1] & !op_batch_flags[2] + + +### Helper evaluators ############################################################################# + +# Enforces that column must be binary. +# Constraint degree: 2 +ev is_binary([a]) { + enf a^2 = a +} + + +# Enforces that value in column is copied over to the next row. +# Constraint degree: 1 +ev is_unchanged([column]) { + enf column' = column +} + + +# Enforces decoder general constraints. +# +# Max constraint degree: 9 +ev general([addr, op_bits[7], hasher[8], in_span, s0, extra]) { + # Get flags required for the general constraints + let f_repeat = get_f_repeat(op_bits, extra) + let f_end = get_f_end(op_bits, extra) + let f_halt = get_f_halt(op_bits, extra) + + # Enforce that `extra` column is set to 1 when op_bits[6] = 1 and op_bits[5] = 1 + # Constraint degree: 3 + enf extra = 1 when op_bits[6] & op_bits[5] + + # Enforce that when SPLIT or LOOP operation is executed, the top of the operand stack must + # contain a binary value. + # Constraint degree: 8 + enf is_binary([s0]) when get_f_split(op_bits) | get_f_loop(op_bits) + + # Enforce that When REPEAT operation is executed, the value at the top of the operand stack + # must be 1. + # Constraint degree: 5 + enf s0 = 1 when f_repeat + + # Enforce that when REPEAT operation is executed, the value in hasher[4] column (the + # is_loop_body flag), must be set to 1. This ensures that REPEAT operation can be executed only + # inside a loop. + # Constraint degree: 5 + enf hasher[4] = 1 when f_repeat + + # Enforce that when RESPAN operation is executed, we need to make sure that the block ID is + # incremented by 8. + # Constraint degree: 5 + enf addr' = addr + 8 when f_respan(op_bits, extra) + + # Enforce that when END operation is executed and we are exiting a loop block (i.e., is_loop, + # value which is stored in hasher[5], is 1), the value at the top of the operand stack must be + # 0. + # Constraint degree: 6 + enf s0 = 0 when f_end & hasher[5] + + # Enforce that when END operation is executed and the next operation is REPEAT, values in + # hasher[0], ..., hasher[4] (the hash of the current block and the is_loop_body flag) must be + # copied to the next row. + # Constraint degree: 9 + enf is_unchanged([hasher[i]]) for i in 0..5 when f_end & get_f_repeat(op_bits', extra') + + # Enforce that a HALT instruction can be followed only by another HALT instruction. + # Constraint degree: 8 + enf f_halt * !get_f_halt(op_bits', extra') = 0 + + # Enforce that when a HALT operation is executed, block address column (addr) must be 0. + # Constraint degree: 5 + enf addr = 0 when f_halt + + # Enforce that values in op_bits columns must be binary. + # Constraint degree: 2 + enf is_binary([b]) for b in op_bits + + # Enforce that when the value in in_span column is set to 1, control flow operations cannot be + # executed on the VM, but when in_span flag is 0, only control flow operations can be executed + # on the VM. + # Constraint degree: 4 + enf 1 - in_span - get_f_ctrl(op_bits, extra) = 0 +} + + +# Enforces the constraint for computing block hashes. +# +# Max constraint degree: 8 +ev block_hash_computation([addr, op_bits[7], hasher[8], extra], [p[4]]) { + # Get flags required for the block hash computation constraint + let f_ctrli = get_f_ctrli(op_bits, extra) + let f_span = get_f_span(op_bits) + let f_respan = get_f_respan(op_bits, extra) + let f_end = get_f_end(op_bits, extra) + + # Label specifying that we are starting a new hash computation. + let m_bp = get_transition_label(HASHER_LINEAR_HASH) + + # Label specifying that we are absorbing the next sequence of 8 elements into an ongoing hash + # computation. + let m_abp = get_transition_label(HASHER_LINEAR_HASH) + + # Label specifying that we are reading the result of a hash computation. + let m_hout = get_transition_label(HASHER_RETURN_HASH) + + # `alpha` is the global random values array. + let rate_sum = sum([$alpha[i + 8] * hasher[i] for i in 0..8]) + let digest_sum = sum([$alpha[i + 8] * hasher[i] for i in 0..4]) + + # Variable for initiating a hasher with address addr' and absorbing 8 elements from the hasher + # state (hasher[0], ..., hasher[7]) into it. + let h_init = $alpha[0] + $alpha[1] * m_bp + $alpha[2] * addr' + rate_sum + + # Variable for the absorption. + let h_abp = $alpha[0] + $alpha[1] * m_abp + $alpha[2] * addr' + rate_sum + + # Variable for the result. + let h_res = $alpha[0] + $alpha[1] * m_hout + $alpha[2] * (addr + 7) + digest_sum + + # Opcode value of the opcode being executed on the virtual machine. + let opcode_value = sum([op_bits[i] * 2^i for i in 0..7]) + + # When a control block initializer operation (JOIN, SPLIT, LOOP, CALL, SYSCALL) is executed, a + # new hasher is initialized and the contents of hasher[0], ..., hasher[7] are absorbed into the + # hasher. + # + # Value degree: 7 + let u_ctrli = f_ctrli * (h_init + $alpha[5] * opcode_value) + + # When SPAN operation is executed, a new hasher is initialized and contents of + # hasher[0], ..., hasher[7] are absorbed into the hasher. + # + # Value degree: 7 + let u_span = f_span * h_init + + # When RESPAN operation is executed, contents of hasher[0], ..., hasher[7] (which contain the + # new operation batch) are absorbed into the hasher. + # + # Value degree: 5 + let u_respan = f_respan * h_abp + + # When END operation is executed, the hash result is copied into registers + # hasher[0], ..., hasher[3]. + # + # Value degree: 5 + let u_end = f_end * h_res + + # Enforce the block hash computation constraint. We need to add 1 and subtract the sum of the + # relevant operation flags to ensure that when none of the flags is set to 1, the above + # constraint reduces to p[0]' = p[0]. + # Constraint degree: 8 + enf p[0]' * (u_ctrli + u_span + u_respan + u_end + 1 - + (f_ctrli + f_span + f_respan + f_end)) = p[0] +} + + +# Enforces the constraint for updating the block stack table. +# +# Max constraint degree: 8 +ev block_stack_table([addr, op_bits[7], hasher[8], s0, extra], [p[4]]) { + # Get flags required for the block stack table constraint + let f_join = get_f_join(op_bits) + let f_split = get_f_split(op_bits) + let f_loop = get_f_loop(op_bits) + let f_span = get_f_span(op_bits) + let f_respan = get_f_respan(op_bits, extra) + let f_end = get_f_end(op_bits, extra) + + # When JOIN operation is executed, row (addr', addr, 0) is added to the block stack table. + # Value degree: 7 + let v_join = f_join * ($alpha[0] + $alpha[1] * addr' + $alpha[2] * addr) + + # When SPLIT operation is executed, row (addr', addr, 0) added to the block stack table. + # Value degree: 7 + let v_split = f_split * ($alpha[0] + $alpha[1] * addr' + $alpha[2] * addr) + + # When LOOP operation is executed, row (addr', addr, 1) is added to the block stack table if + # the value at the top of the operand stack is 1, and row (addr', addr, 0) is added to the + # block stack table if the value at the top of the operand stack is 0. + # Value degree: 7 + let v_loop = f_loop * ($alpha[0] + $alpha[1] * addr' + $alpha[2] * addr + $alpha[3] * s0) + + # When SPAN operation is executed, row (addr', addr, 0) is added to the block stack table. + # Value degree: 7 + let v_span = f_span * ($alpha[0] + $alpha[1] * addr' + $alpha[2] * addr) + + # When RESPAN operation is executed, row (addr, hasher[1]', 0) is removed from the block stack + # table, and row (addr', hasher[1]', 0) is added to the table. The prover sets the value of + # register hasher[1] at the next row to the ID of the parent block. + # Value degree: 5 + let u_respan = f_respan * ($alpha[0] + $alpha[1] * addr + $alpha[2] * hasher[1]') + # Value degree: 5 + let v_respan = f_respan * ($alpha[0] + $alpha[1] * addr' + $alpha[2] * hasher[1]') + + # When END operation is executed, row (addr, addr', hasher[5]) is removed from the block span + # table. Register hasher[5] contains the is_loop flag. + # Value degree: 5 + let u_end = f_end * + ($alpha[0] + $alpha[1] * addr + $alpha[2] * addr' + $alpha[3] * hasher[5]) + + # Enforce the block stack table constraint. We need to add 1 and subtract the sum of the + # relevant operation flags from each side to ensure that when none of the flags is set to 1, + # the above constraint reduces to p[1]' = p[1] + # Constraint degree: 8 + enf p[1]' * (u_end + u_respan + 1 - (f_end + f_respan)) = + p[1] * (v_join + v_split + v_loop + v_span + v_respan + 1 - + (f_join + f_split + f_loop + f_span + f_respan)) +} + + +# Enforces the constraint for updating the block hash table. +# +# Max constraint degree: 9 +ev block_hash_table([addr, op_bits[7], hasher[8], s0, extra], [p[4]]) { + # Get flags required for the block hash table constraint + let f_join = get_f_join(op_bits) + let f_split = get_f_split(op_bits) + let f_loop = get_f_loop(op_bits) + let f_end = get_f_end(op_bits, extra) + let f_repeat = get_f_repeat(op_bits, extra) + + # Values representing left and right children of a block. + # Value degree: 1 + let ch1 = $alpha[0] + $alpha[1] * addr' + sum([$alpha[i + 2] * hasher[i] for i in 0..4]) + # Value degree: 1 + let ch2 = $alpha[0] + $alpha[1] * addr' + sum([$alpha[i + 2] * hasher[i + 4] for i in 0..4]) + + # Value representing the result of hash computation. + # Value degree: 1 + let bh = $alpha[0] + $alpha[1] * addr + sum([$alpha[i + 2] * hasher[i]]) + $alpha[7] * hasher[4] + + # When JOIN operation is executed, hashes of both child nodes are added to the block hash + # table. We add alpha[6] term to the first child value to differentiate it from the second + # child (i.e., this sets is_first_child to 1). + # Value degree: 8 + let v_join = f_join * (ch1 + $alpha[6]) * ch2 + + # When SPLIT operation is executed and the top of the stack is 1, hash of the true branch is + # added to the block hash table, but when the top of the stack is 0, hash of the false branch + # is added to the block hash table. + # Value degree: 8 + let v_split = f_split * (s0 * ch1 + (1 - s0) * ch2) + + # When LOOP operation is executed and the top of the stack is 1, hash of loop body is added to + # the block hash table. We add alpha[7] term to indicate that the child is a body of a loop. + # The below also means that if the top of the stack is 0, nothing is added to the block hash + # table as the expression evaluates to 0. + # Value degree: 8 + let v_loop = f_loop * s0 * (ch1 + $alpha[7]) + + # When REPEAT operation is executed, hash of loop body is added to the block hash table. We add + # alpha[7] term to indicate that the child is a body of a loop. + # Value degree: 5 + let v_repeat = f_repeat * (ch1 + $alpha[7]) + + # When END operation is executed, hash of the completed block is removed from the block hash + # table. However, we also need to differentiate between removing the first and the second child + # of a join block. We do this by looking at the next operation. Specifically, if the next + # operation is neither END nor REPEAT we know that another block is about to be executed, and + # thus, we have just finished executing the first child of a join block. Thus, if the next + # operation is neither END nor REPEAT we need to set the term for alpha[6] coefficient to 1 as + # shown below. + # Value degree: 8 + let u_end = f_end * + (bh + $alpha[6] * (1 - (get_f_end(op_bits', extra') + get_f_repeat(op_bits', extra')))) + + # Enforce the block hash table constraint. We need to add 1 and subtract the sum of the + # relevant operation flags from each side to ensure that when none of the flags is set to 1, + # the above constraint reduces to p[2]' = p[2] + # Constraint degree: 9 + enf p[2]' * (u_end + 1 - f_end) = + p[2] * (v_join + v_split + v_loop + v_repeat + 1 - (f_join + f_split + f_loop + f_repeat)) + + # TODO: add boundary constraints to the p[2] column: + # 1. The first value in the column represents a row for the entire program. Specifically, the + # row tuple would be (0, program_hash, 0, 0). This row should be removed from the table + # when the last END operation is executed. + # 2. The last value in the column is 1 - i.e., the block hash table is empty. +} + + +# Enforce that values in in_span column, which is used to identify rows which execute non-control +# flow operations, are set correctly. +# +# Constraint degree: 7 +ev in_span_column([op_bits[7], in_span, extra]) { + # Get flags required for the inspan column constraint + let f_span = get_f_span(op_bits) + let f_respan = get_f_respan(op_bits, extra) + let f_respan_next = get_f_respan(op_bits', extra') + let f_end_next = get_f_end(op_bits', extra') + + # Enforce that when executing SPAN or RESPAN operation, the next value in in_span column must + # be set to 1. + # Constraint degree: 7 + enf in_span' = 1 when f_span | f_respan + + # Enforce that when the next operation is END or RESPAN, the next value in in_span column must + # be set to 0. + # Constraint degree: 5 + enf in_span' = 0 when f_end_next | f_respan_next + + # Enforce that in all other cases, the value in in_span column must be copied over to the next + # row. + # Constraint degree: 7 + enf is_unchanged(in_span) when !f_span & !f_respan & !f_end_next & !f_respan_next + + # TODO: add boundary constraint for in_span column: in_span.first = 0 +} + +# Enforce that when we are inside a span block, values in the block address column (denoted as addr) +# must remain the same. +# +# Constraint degree: 2 +ev block_address([addr, in_span]) { + enf is_unchanged(addr) when in_span +} + +# Enforce that values in group_count column, which is used to keep track of the number of operation +# groups which remains to be executed in a span block, are set correctly. +# +# Max constraint degree: 7 +ev group_count([op_bits[7], hasher[8], in_span, group_count, extra]) { + # Get value of the f_push flag + let f_push = get_f_push(op_bits, extra) + + # Enforce that inside a span block, group count can either stay the same or decrease by one. + # Constraint degree: 3 + enf (group_count' - group_count) * (group_count' - group_count - 1) = 0 when in_span + + # Enforce that when group count is decremented inside a span block, either hasher[0] must be 0 + # (we consumed all operations in a group) or we must be executing PUSH operation. + # Constraint degree: 7 + enf (1 - f_push) * hasher[0] = 0 when in_span & (group_count' - group_count) + + # Enforce that when executing a SPAN, a RESPAN, or a PUSH operation, group count must be + # decremented by 1. + # Constraint degree: 7 + enf group_count' - group_count = 1 when f_span(op_bits) | get_f_respan(op_bits, extra) | f_push + + # Enforce that if the next operation is either an END or a RESPAN, group count must remain the + # same. + # Constraint degree: 5 + enf is_unchanged(group_count) when get_f_end(op_bits', extra') | get_f_respan(op_bits', extra') + + # Enforce that when an END operation is executed, group count must be 0. + # Constraint degree: 5 + enf group_count = 0 when get_f_end(op_bits, extra) +} + +# Enforce that register hasher[0], which is used to keep track of operations to be executed in the +# current operation group, is set correctly. +# +# Max constraint degree: 7 +ev op_group_decoding([op_bits[7], in_span, group_count, extra]) { + # opcode value for the next row. + let op_next = sum([op_bits[i]' * 2^i for i in 0..7]) + + # Flag which is set to 1 when the group count within a span block does not change. We multiply + # it by sp' to make sure the flag is 0 when we are about to end decoding of an operation batch. + let f_sgc = in_span * in_span' * (1 - group_count' + group_count) + + # Enforce that when a SPAN, a RESPAN, or a PUSH operation is executed or when the group count + # does not change, the value in hasher[0] should be decremented by the value of the opcode in + # the next row. + # Constraint degree: 7 + enf hasher[0] - hasher[0]' * 2^7 - op_next = 0 + when f_span(op_bits) | get_f_respan(op_bits, extra) | get_f_push(op_bits, extra) | f_sgc + + # Enforce that when we are in a span block and the next operation is END or RESPAN, the current + # value in hasher[0] column must be 0. + # Constraint degree: 6 + enf (get_f_end(op_bits', extra') + get_f_respan(op_bits', extra')) * hasher[0] = 0 when in_span +} + +# Enforce that the values in op_index column, which tracks index of an operation within its +# operation group, are set correctly. +# +# Max constraint degree: 9 +ev op_index([op_bits[7], in_span, group_count, op_index, extra]) { + # ng is set to 1 when we are about to start executing a new operation group (i.e., group count + # is decremented but we did not execute a PUSH operation). + let ng = group_count' - group_count - get_f_push(op_bits, extra) + + # Enforce that when executing SPAN or RESPAN operations the next value of op_index must be set + # to 0. + # Constraint degree: 7 + enf op_index' = 0 when f_span(op_bits) | get_f_respan(op_bits, extra) + + # Enforce that when starting a new operation group inside a span block, the next value of + # op_index must be set to 0. + # Constraint degree: 6 + enf op_index' = 0 when in_span & ng + + # Enforce that when inside a span block but not starting a new operation group, op_index must + # be incremented by 1. + # Constraint degree: 7 + enf op_index' - op_index = 1 when in_span & in_span' & !ng + + # Enforce that values of op_index must be in the range [0, 8]. + # Constraint degree: 9 + enf prod([op_index - i for i in 0..9]) = 0 +} + +# Enforce that values in operation batch flag columns (denoted op_batch_flags[]), which are used to +# specify how many operation groups are present in an operation batch, are set correctly. +# +# Max constraint degree: 6 +ev op_batch_flags([op_bits[7], hasher[8], op_batch_flags[3], extra]) { + # Get flags required for the op batch flag constraints + let f_g1 = get_f_g1(op_batch_flags) + let f_g2 = get_f_g2(op_batch_flags) + let f_g4 = get_f_g4(op_batch_flags) + let f_g8 = get_f_g8(op_batch_flags) + + # Enforce that all batch flags are binary. + # Constraint degree: 2 + enf is_binary(bc) for bc in op_batch_flags + + # Enforce that when SPAN or RESPAN operations is executed, one of the batch flags must be set + # to 1. + # Constraint degree: 6 + enf f_g1 + f_g2 + f_g4 + f_g8 = 1 when f_span(op_bits) | get_f_respan(op_bits, extra) + + # Enforce that when we have at most 4 groups in a batch, registers h[4], ..., h[7] should be + # set to 0's. + # Constraint degree: 4 + enf hasher[i] = 0 for i in 4..8 when f_g1 | f_g2 | f_g4 + + # Enforce that When we have at most 2 groups in a batch, registers h[2] and h[3] should also be + # set to 0's. + # Constraint degree: 4 + enf hasher[i] = 0 for i in 2..4 when f_g1 | f_g2 + + # Enforce that when we have at most 1 group in a batch, register h[1] should also be set to 0. + # Constraint degree: 4 + enf hasher[1] = 0 when f_g1 +} + +# Enforce that all operation groups in a given batch are consumed before a new batch is started +# (i.e., via a RESPAN operation) or the execution of a span block is complete (i.e., via an END +# operation). +# +# Max constraint degree: 9 +ev op_group_table([addr, op_bits[7], hasher[8], in_span, group_count, op_index, op_batch_flags[3], s0, extra], [p[4]]) { + # Get value of the f_push flag + let f_push = get_f_push(op_bits, extra) + + # opcode value for the next row. + let op_next = sum([op_bits[i]' * 2^i for i in 0..7]) + + # Row value for group in hasher[1] to be added to the op group table when a SPAN or a RESPAN + # operation is executed. + # Value degree: 1 + let v_1 = $alpha[0] + $alpha[1] * addr' + $alpha[2] * (group_count - 1) + $alpha[3] * hasher[1] + + # Value degree: 1 + let prod_v_3 = prod([$alpha[0] + + $alpha[1] * addr' + + $alpha[2] * (group_count - i) + + $alpha[3] * hasher[i] for i in 1..4]) + + # Value degree: 1 + let prod_v_7 = prod([$alpha[0] + + $alpha[1] * addr' + + $alpha[2] * (group_count - i) + + $alpha[3] * hasher[i] for i in 1..8]) + + # The value of the row to be removed from the op group table. + # Value degree: 5 + let u = $alpha[0] + $alpha[1] * addr + $alpha[2] * group_count + $alpha[3] * + ((hasher[0]' * 2^7 + op_next) * (1 - f_push) + s0' * f_push) = 0 + + # A flag which is set to 1 when a group needs to be removed from the op group table. + let f_dg = in_span * (group_count' - group_count) + + # Enforce the constraint for updating op group table. The constraint specifies that when SPAN + # or RESPAN operations are executed, we add between 1 and 7 groups to the op group table, and + # when group count is decremented inside a span block, we remove a group from the op group + # table. + # Constraint degree: 9 + enf p[3]' * (f_dg * u + 1 - f_dg) = p[3] * (get_f_g2(op_batch_flags) * v_1 + + get_f_g4(op_batch_flags) * prod_v_3 + + get_f_g8(op_batch_flags) * prod_v_7 - 1 + + (f_span(op_bits) + get_f_respan(op_bits, extra))) +} + +# Enforce proper decoding of span blocks. +# +# Max constraint degree: 9 +ev span_block([addr, op_bits[7], hasher[8], in_span, group_count, op_index, op_batch_flags[3], s0, extra], [p[4]]) { + enf in_span_column([op_bits, in_span, extra]) + enf block_address([addr, in_span]) + enf group_count([op_bits, hasher, in_span, group_count, extra]) + enf op_group_decoding([op_bits, in_span, group_count, extra]) + enf op_index([op_bits, in_span, group_count, op_index, extra]) + enf op_batch_flags([op_bits, hasher, op_batch_flags, extra]) + enf op_group_table([addr, op_bits, hasher, in_span, group_count, op_index, op_batch_flags, s0, extra], [p]) +} + +### Decoder Air Constraints ####################################################################### + +# Enforces the constraints on the decoder. The register `s0` denotes the value at the top of the +# stack. `extra` denotes the register for degree reduction during flag computations, and p[4] +# columns denote multiset check columns. +# +# Max constraint degree: 9 +ev decoder_constraints([addr, op_bits[7], hasher[8], in_span, group_count, op_index, op_batch_flags[3], s0, extra], [p[4]]) { + enf general([addr, op_bits[7], hasher[8], in_span, s0, extra]) + + enf block_hash_computation([addr, op_bits[7], hasher[8], extra], [p[4]]) + + enf block_stack_table([addr, op_bits[7], hasher[8], s0, extra], [p[4]]) + + enf block_hash_table([addr, op_bits, hasher, s0, extra], [p[4]]) + + enf span_block([addr, op_bits[7], hasher[8], in_span, group_count, op_index, op_batch_flags[3], s0, extra], [p[4]]) +} \ No newline at end of file diff --git a/constraints/miden-vm-old/hash.air b/constraints/miden-vm-old/hash.air new file mode 100644 index 000000000..55165cd19 --- /dev/null +++ b/constraints/miden-vm-old/hash.air @@ -0,0 +1,208 @@ +mod HashChipletAir + +### Constants and periodic columns ################################################################ + +periodic_columns { + cycle_row_0: [1, 0, 0, 0, 0, 0, 0, 0] + cycle_row_6: [0, 0, 0, 0, 0, 0, 1, 0] + cycle_row_7: [0, 0, 0, 0, 0, 0, 0, 1] +} + +### Helper functions ############################################################################## + +# Returns binary negation of the value. +fn binary_not(value: scalar) -> scalar: + return 1 - value + + +# Set to 1 when selector flags are (1,0,1) on rows which are multiples of 8. This is flag of +# the instruction that initiates Merkle path verification computation. +fn get_f_mp(s: vector[3]) -> scalar: + return cycle_row_0 & s[0] & binary_not(s[1]) & s[2] + + +# Set to 1 when selector flags are (1,1,0) on rows which are multiples of 8. This is flag of +# the instruction that initiates Merkle path verification for the "old" node value during +# Merkle root update computation. +fn get_f_mv(s: vector[3]) -> scalar: + return cycle_row_0 & s[0] & s[1] & binary_not(s[2]) + + +# Set to 1 when selector flags are (1,1,1) on rows which are multiples of 8. This is flag of +# the instruction that initiates Merkle path verification for the "new" node value during +# Merkle root update computation. +fn get_f_mu(s: vector[3]) -> scalar: + return cycle_row_0 & s[0] & s[1] & s[2] + + +# Set to 1 when selector flags are (1,0,0) on rows which are 1 less than a multiple of 8. This +# is flag of the instruction that absorbs a new set of elements into the hasher state when +# computing a linear hash of many elements. +fn get_f_abp(s: vector[3]) -> scalar: + return cycle_row_7 & s[0] & binary_not(s[1]) & binary_not(s[2]) + + +# Set to 1 when selector flags are (1,0,1) on rows which are 1 less than a multiple of 8. This +# is flag of the instruction that absorbs the next Merkle path node into the hasher state +# during Merkle path verification computation. +fn get_f_mpa(s: vector[3]) -> scalar: + return cycle_row_7 & s[0] & binary_not(s[1]) & s[2] + + +# Set to 1 when selector flags are (1,1,0) on rows which are 1 less than a multiple of 8. This +# is flag of the instruction that absorbs the next Merkle path node into the hasher state +# during Merkle path verification for the "old" node value during Merkle root update +# computation. +fn get_f_mva(s: vector[3]) -> scalar: + return cycle_row_7 & s[0] & s[1] & binary_not(s[2]) + + +# Set to 1 when selector flags are (1,1,1) on rows which are 1 less than a multiple of 8. This +# is flag of the instruction that absorbs the next Merkle path node into the hasher state +# during Merkle path verification for the "new" node value during Merkle root update +# computation. +fn get_f_mua(s: vector[3]) -> scalar: + return cycle_row_7 & s[0] & s[1] & s[2] + + +# We can define two flags: +# 1. Flag f_hout = cycle_row_7 & binary_not(s[0]) & binary_not(s[1]) & binary_not(s[2]), +# which is set to 1 when selector flags are (0,0,0) on rows which are 1 less than a multiple +# of 8. This is flag of the instruction that returns the result of the currently running +# computation. +# 2. Flag f_sout = cycle_row_7 & binary_not(s[0]) & binary_not(s[1]) & s[2], which is set to 1 +# when selector flags are (0,0,1) on rows which are 1 less than a multiple of 8. This is flag +# of the instruction that returns the whole hasher state. +# +# Flag f_out is set to 1 when either f_hout = 1 or f_sout = 1 in the current row. +fn get_f_out(s: vector[3]) -> scalar: + return cycle_row_7 & binary_not(s[0]) & binary_not(s[1]) + + +# Flag f_out_next is set to 1 when either f_hout = 1 or f_sout = 1 in the next row. +fn get_f_out_next(s: vector[3]) -> scalar: + return cycle_row_6 & binary_not(s[0]') & binary_not(s[1]') + + +### Helper evaluators ############################################################################# + +# Enforces that column must be binary. +ev is_binary(main: [a]) { + enf a^2 = a +} + + +# Enforces that value in column is copied over to the next row. +ev is_unchanged(main: [column]) { + ev column' = column +} + + +# Enforce selector columns constraints +ev selector_columns(main: [s[3]]) { + let f_out = get_f_out(s) + let f_out_next = get_f_out_next(s) + let f_abp = get_f_abp(s) + let f_mpa = get_f_mpa(s) + let f_mva = get_f_mva(s) + let f_mua = get_f_mua(s) + + # Flag that is true when the performed operation is one of the represented by flags f_abp, + # f_mpa, f_mva or f_mua + let f_comp = f_abp + f_mpa + f_mva + f_mua + + # Enforce that selector columns are binary. + enf is_binary([selector]) for selector in s + + # Enforce that unless f_out = 1 or f_out' = 1, the values in columns s[1] and s[2] are copied + # over to the nex row. + enf is_unchanged([s[1]]) when !f_out & !f_out_next + enf is_unchanged([s[2]]) when !f_out & !f_out_next + + # Enforce that if any of f_abp, f_mpa, f_mva, f_mua flags is set to 1, the next value of s[0] + # is 0. + enf s[0]' * f_comp = 0 + + # Enforce that no invalid combinations of flags are allowed. + enf cycle_row_7 * binary_not(s[0]) * s[1] = 0 +} + +# Enforce node index constraints +ev node_index(main: [s[3], i]) { + let f_out = get_f_out(s) + let f_mp = get_f_mp(s) + let f_mv = get_f_mv(s) + let f_mu = get_f_mu(s) + let f_mpa = get_f_mpa(s) + let f_mva = get_f_mva(s) + let f_mua = get_f_mua(s) + + # b is the value of the bit which is discarded during shift by one bit to the right. + let b = i - 2 * i' + + # Flag that allows to enforce constraint that b is binary only when a new node is absorbed into + # the hasher state (when the hash operation is one of Merkle path verification operations or + # next Merkle path node absorption operations) + let f_an = f_mp + f_mv + f_mu + f_mpa + f_mva + f_mua + + # Enforce that b is binary only when a new node is absorbed into the hasher state. + enf f_an * (b^2 - b) = 0 + + # Enforce that when a computation is finished i = 0. + enf f_out * i = 0 + + # Enforce that the value in i is copied over to the next row unless we are absorbing a new row + # or the computation is finished. + let absorbing_or_comp_finished = 1 - f_an - f_out + enf is_unchanged([i]) when absorbing_or_comp_finished +} + +# Enforce hasher state constraints +ev hasher_state(main: [s[3], h[12], i]) { + let f_mp = get_f_mp(s) + let f_mv = get_f_mv(s) + let f_mu = get_f_mu(s) + let f_abp = get_f_abp(s) + + # Flag that is true when the performed operation includes absorbing the next node during Merkle + # path computation. + let f_absorb_node = f_mp + f_mv + f_mu + + # b is the value of the bit which is discarded during shift by one bit to the right. + let b = i - 2 * i' + + # Enforce that when absorbing the next set of elements into the state during linear hash + # computation (i.e. f_abp = 1) the first 4 elements (the capacity portion) are carried over to + # the next row. + enf f_abp * (h[j]' - h[j]) = 0 for j in 0..4 + + # Enforce that when absorbing the next node during Merkle path computation + # (i.e. f_mp + f_mv + f_mu = 1), the result of the previous hash (h[4], ..., h[7]) are copied + # over either to (h[4]', ..., h[7]') or to (h[8]', ..., h[11]') depending on the value of b. + match enf: + is_unchanged(h[j + 4]) for j in 0..4 when !b & f_absorb_node + h[j + 8]' = h[j + 4] for j in 0..4 when b & f_absorb_node +} + +### Hash Chiplet Air Constraints ################################################################## + +# Enforces the constraints on the hash chiplet, given the columns of the hash execution trace. +ev hash_chiplet(main: [s[3], r, h[12], i]) { + ## Row address constraint ## + # TODO: Apply row address constraints: + # 1. Boundary constraint `enf r.first = 1` + # 2. Transition constraint. It requires chiplets module's selector flag s0. + + ## Selector columns constraints ## + enf selector_columns([s]) + + ## Node index constraints ## + enf node_index([s, i]) + + ## Hasher state constraints ## + # TODO: apply RPO constraints to the hasher state + enf hasher_state([s, h, i]) + + # Multiset check constraints + # TODO: Apply multiset check constraints +} \ No newline at end of file diff --git a/constraints/miden-vm-old/memory.air b/constraints/miden-vm-old/memory.air new file mode 100644 index 000000000..17da938a5 --- /dev/null +++ b/constraints/miden-vm-old/memory.air @@ -0,0 +1,120 @@ +mod MemoryChipletAir + +### Helper functions ############################################################################## + +# Returns the n0 flag which is set to 1 when context changes and 0 otherwise. +fn get_n0(ctx: scalar, ctx_next: scalar, t_next: scalar) -> scalar: + return (ctx_next - ctx) * t_next + + +# Returns the n1 flag. If context remains the same, n1 = 1 when address changes and 0 otherwise. +fn get_n1(addr: scalar, addr_next: scalar, t_next: scalar) -> scalar: + return (addr_next - addr) * t_next + + +### Helper evaluators ############################################################################# + +# Enforces that column must be binary. +# Constraint degree: 2 +ev is_binary([a]) { + enf a^2 = a +} + + +# Enforces that value in column is copied over to the next row. +# Constraint degree: 1 +ev is_unchanged([column]) { + enf column' = column +} + + +# Enforces that the provided columns must be zero. +ev is_zero([column]) { + enf column = 0 +} + + +# Enforces that created flags have valid values during the program execution. +ev flags_validity([ctx, addr, t]) { + # n0 = 1 when context changes and 0 otherwise. + let n0 = get_n0(ctx, ctx', t') + + # if context remains the same, n1 = 1 when address changes and 0 otherwise. + let n1 = get_n1(addr, addr', t') + + # Enforce that n0 must be binary. + enf n0^2 = n0 + + # Enforce that when context changes, n0 = 1 (or when n0 = 0, context remains the same). + enf ctx' = ctx when !n0 + + # Enforce that n1 must be binary. An additional condition ensures that the check of n1 + # occurs only if the context does not change (n0 = 0). + enf n1^2 = n1 when !n0 + + # Enforce that if context remains the same, n1 = 1 when address changes and 0 otherwise. + enf addr' = addr when !n0 & !n1 +} + +# Enforces that selectors take the correct values under certain conditions. +ev enforce_selectors([s[2], ctx, addr, t]) { + # Enforce that values in the selectior columns must be binary. + # s[0] is set to 0 for write operations and to 1 for read operations. + enf is_binary([selector]) for selector in s + + # n0 = 1 when context changes and 0 otherwise. + let n0 = get_n0(ctx, ctx', t') + + # if context remains the same, n1 = 1 when address changes and 0 otherwise. + let n1 = get_n1(addr, addr', t') + + # Enforce that s[1]' = 1 when the operation is a read and `ctx` and `addr` columns are both + # unchanged. + enf s[1]' = 1 when !n0 & !n1 & s[0]' + + # Enforce that s[1]' = 0 when either the context changed, the address changed, or the operation + # is a write. + enf s[1]' = 0 when n0 | n1 | !s[0]' +} + +# Enforces that the delta between two consecutive contexts, addresses, or clock cycles is updated +# and decomposed into the `d1` and `d0` columns correctly. +ev enforce_delta([ctx, addr, clk, d[2], t]) { + # n0 = 1 when context changes and 0 otherwise. + let n0 = get_n0(ctx, ctx', t') + + # if context remains the same, n1 = 1 when address changes and 0 otherwise. + let n1 = get_n1(addr, addr', t') + + let d_next_agg = 2^16 * d[1]' + d[0]' + + # Enforce that values of context (`ctx`), address (`addr`), and clock cycle (`clk`) grow + # monotonically + match enf: + d_next_agg = ctx' - ctx when n0 + d_next_agg = addr' - addr when !n0 & n1 + d_next_agg = clk' - clk - 1 when !n0 & !n1 +} + +# Enforces that memory is initialized to zero when it is read before being written and that when +# existing memory values are read they remain unchanged. +ev enforce_values([s[2], v[4]]) { + # Enforce that values at a given memory address are always initialized to 0. + enf is_zero([v_i]) for v_i in v when s[0] & !s[1] + + # Enforce that for the same context/address combination, the v columns of the current row are + # equal to the corresponding v columns of the next row + enf is_unchanged([v_i]) for v_i in v when s[1] +} + +### Memory Chiplet Air Constraints ################################################################ + +# Enforces the constraints on the memory chiplet, given the columns of the memory execution trace. +ev memory_chiplet([s[2], ctx, addr, clk, v[4], d[2], t]) { + enf flags_validity([ctx, addr, t]) + enf enforce_selectors([s, ctx, addr, t]) + enf enforce_delta([ctx, addr, clk, d, t]) + # TODO: perform range checks for values in columns d[0] and d[1] + enf enforce_values([s, v]) + # Bus constraint is implemented in a separate file +} \ No newline at end of file diff --git a/constraints/miden-vm-old/range_checker.air b/constraints/miden-vm-old/range_checker.air new file mode 100644 index 000000000..f3581de8c --- /dev/null +++ b/constraints/miden-vm-old/range_checker.air @@ -0,0 +1,62 @@ +mod RangeCheckerAir + +### Helper functions ############################################################################## + +# Returns array of mutually exclusive multiplicity flags. +# f[0] set to 1 when we don't include the value into the running product. +# f[1] set to 1 when we include the value into the running product. +# f[2] set to 1 when we include two copies of the value into the running product. +# f[3] set to 1 when we include four copies of the value into the running product. +fn get_multiplicity_flags(s0: scalar, s1: scalar) -> vector[4]: + return [!s0 & !s1, s0 & !s1, !s0 & s1, s0 & s1] + + +### Helper evaluators ############################################################################# + +# Enforces that column must be binary. +ev is_binary([v]) { + enf v^2 = v +} + +# Enforces correct transition from 8-bit to 16-bit section of the table. +ev transition_8_to_16_bit([t, v]) { + # Ensure that values in column t can flip from 0 to 1 only once + enf t * !t' = 0 + + # Ensure that when column t flips, column v must equal 255 + enf v = 255 when t' & !t + + # Ensure that when column t flips, v' must be reset to 0 + enf v' = 0 when t' & !t +} + +# The virtual table enforces an 8-bit range check for each row transition in the 16-bit section of +# the range checker, which enforces its internal correctness. +ev virtual_table([t, s0, s1, v], [p0]) { + let val = $alpha[0] + v + let f = get_multiplicity_flags(s0, s1) + + # z represents how a row in the execution trace is reduced to a single value. + let z = val^4 * f[3] + val^2 * f[2] + val * f[1] + f[0] + enf p0' * (($alpha[0] + v' - v) * t - t + 1) = p0 * (z - z * t + t) + + # TODO: add boundary constraints p0.first = 1 and p0.last = 1 +} + +### Range checker Air Constraints ################################################################# + +ev range_checker([t, s0, s1, v], [p0]) { + # Check selector flags are binary. + let selectors = [t, s0, s1] + enf is_binary([s]) for s in selectors + + # Constrain the row transitions in the 8-bit section of the table so that as we move from one + # row to the next the value either stays the same or increases by 1. + enf (v' - v) * (v' - v - 1) = 0 when !t' + + # Constrain the transition from 8-bit to 16-bit section of the table. + enf transition_8_to_16_bit([t, v]) + + # Constrain the row transitions in the 16-bit section of the table. + enf virtual_table([t, s0, s1, v], [p0]) +} \ No newline at end of file diff --git a/constraints/miden_vm.air b/constraints/miden_vm.air new file mode 100644 index 000000000..c9a324409 --- /dev/null +++ b/constraints/miden_vm.air @@ -0,0 +1,184 @@ +########################################################################################## +# MIDEN VM - ALGEBRAIC INTERMEDIATE REPRESENTATION (AIR) CONSTRAINTS +########################################################################################## +# +# The Miden Virtual Machine is a STARK-based zero-knowledge virtual machine designed for +# efficient execution and proving of arbitrary computations. This AIR specification defines +# the arithmetic constraints that govern the VM's execution. +# +# STATUS: Not fully implemented +# +# REFERENCES: +# - Miden VM implementation: https://0xmiden.github.io/miden-vm/ +# - Miden VM documentation : https://0xmiden.github.io/miden-vm/intro/main.html +########################################################################################## + +def MidenVM + +use chiplets::chiplets_constraints; +use bitwise::*; +use hasher::*; +use range_checker::*; +use system::*; +use utils::*; + +########################################################################################## +# EXECUTION TRACE LAYOUT +########################################################################################## +# +# The execution trace captures the state of the VM at each cycle. The main trace consists +# of 80 columns organized into logical segments. +# +########################################################################################## + +trace_columns { + main: [system[8], decoder[24], stack[19], range_checker[2], chiplets[20], padding[7]], +} + +########################################################################################## +# PUBLIC INPUTS +########################################################################################## +# +# Public inputs define the interface between the prover and verifier, establishing +# the computation's inputs and expected outputs that must be verified. +# +# INPUT STRUCTURE: +# ┌───────────────┬─────────┬───────────────────────────────────────────────────┐ +# │ Field │ Size │ Description │ +# ├───────────────┼─────────┼───────────────────────────────────────────────────┤ +# │ stack_inputs │ 16 │ Initial operand stack state (top 16 elements) │ +# │ stack_outputs │ 16 │ Final operand stack state (top 16 elements) │ +# │program_digest │ 4 │ MAST root hash identifying the executed program │ +# │kernel_digests │ [[5]] │ Hashes of kernel procedures (dynamic array) │ +# └───────────────┴─────────┴───────────────────────────────────────────────────┘ +# +########################################################################################## + +public_inputs { + stack_inputs: [16], # Initial operand stack state (16 field elements) + stack_outputs: [16], # Final operand stack state (16 field elements) + program_digest: [4], # MAST root hash (4 field elements) + kernel_digests: [[5]], # Kernel procedure hashes plus an op label +} + +########################################################################################## +# BUS ARCHITECTURE +########################################################################################## +# +# Buses enable efficient communication between VM components using cryptographic +# protocols like multiset checks and LogUp. They ensure data integrity and consistency +# across different execution units. +# +########################################################################################## + +buses { + # Decoder buses + multiset bus_0_decoder_p1, + multiset bus_1_decoder_p2, + multiset bus_2_decoder_p3, + + # Stack overflow table + multiset bus_3_stack_p1, + + # Range checker bus + logup bus_4_range_checker, + + # Chiplet buses + multiset bus_5_v_table, # Chiplets virtual table + multiset bus_6_chiplets_bus, # Main chiplets communication bus + + # Wiring bus + logup bus_7_wiring_bus, # ACE (Algebraic Circuit Elements) wiring +} + +########################################################################################## +# BOUNDARY CONSTRAINTS +########################################################################################## +# +# Boundary constraints establish the initial and final states of the VM execution. +# They ensure proper initialization and define the expected state at program completion. +# +########################################################################################## + +boundary_constraints { + #################################################################################### + # MAIN TRACE BOUNDARIES + #################################################################################### + + # System clock must start at 0 (VM begins execution at cycle 0) + enf system[0].first = 0; + + #################################################################################### + # AUXILIARY COLUMN BOUNDARIES + #################################################################################### + + # Decoder buses + enf bus_0_decoder_p1.first = unconstrained; + enf bus_0_decoder_p1.last = unconstrained; + enf bus_1_decoder_p2.first = unconstrained; + enf bus_1_decoder_p2.last = unconstrained; + enf bus_2_decoder_p3.first = unconstrained; + enf bus_2_decoder_p3.last = unconstrained; + + # Stack overflow table + enf bus_3_stack_p1.first = unconstrained; + enf bus_3_stack_p1.last = unconstrained; + + # Range checker bus - LogUp protocol requires null initialization/finalization + enf bus_4_range_checker.first = null; + enf bus_4_range_checker.last = null; + + # Chiplets virtual table + enf bus_5_v_table.first = unconstrained; + enf bus_5_v_table.last = unconstrained; + + # Chiplets communication bus + # Initial state contains kernel procedure digests against which the program was compiled + enf bus_6_chiplets_bus.first = kernel_digests; + enf bus_6_chiplets_bus.last = unconstrained; + + # ACE (Algebraic Circuit Elements) wiring bus + enf bus_7_wiring_bus.first = unconstrained; + enf bus_7_wiring_bus.last = unconstrained; +} + +########################################################################################## +# INTEGRITY CONSTRAINTS +########################################################################################## +# +# Integrity constraints define the state transition rules that govern VM execution. +# These constraints ensure that each step of program execution is valid according +# to the Miden VM instruction set architecture. +# +########################################################################################## + +integrity_constraints { + #################################################################################### + # MAIN TRACE CONSTRAINTS + #################################################################################### + + # System state transitions + enf system_transition([system[0..8]]); + + # TODO: Decoder constraints - Program execution and MAST verification + # enf decoder_constraints([decoder]); + + # TODO: Stack constraints - Operand stack operations and overflow handling + # enf stack_constraints([stack]); + + # TODO: Chiplet constraints - Hash, bitwise, ACE, memory operations, and kernel ROM + enf chiplets_constraints([chiplets[0..20]]); + + #################################################################################### + # BUS CONSTRAINTS + #################################################################################### + + # Range checker bus protocol - Connects stack and chiplets for 16-bit range checks + enf range_checker_constraints([decoder[0..24], range_checker[0..2], chiplets[0..20]]); + + # TODO: Additional bus constraints for complete VM verification + # enf decoder_bus_constraints([decoder]); + # enf stack_bus_constraints([stack]); + # enf chiplet_bus_constraints([chiplets]); + # enf ace_bus_constraints([chiplets]) +} diff --git a/constraints/range_checker.air b/constraints/range_checker.air new file mode 100644 index 000000000..e18b2965b --- /dev/null +++ b/constraints/range_checker.air @@ -0,0 +1,86 @@ +########################################################################################## +# RANGE CHECKER CONSTRAINTS MODULE +########################################################################################## +# +# The Range Checker provides efficient 16-bit range checking for other VM components +# using the LogUp protocol with optimized gap handling to minimize the minimal +# trace length while supporting (practically) unlimited range checks. +# +# STATUS: Not fully implemented +# +# REFERENCES: +# - Range Checker Spec: https://0xmiden.github.io/miden-vm/design/range.html +# - LogUp Protocol: https://0xmiden.github.io/miden-vm/design/lookups/main.html +########################################################################################## + +mod range_checker + +use chiplets::*; +use utils::*; + +########################################################################################## +# RANGE CHECKER BUS CONSTRAINTS +########################################################################################## + + +ev range_checker_constraints([decoder[24], range_checker[2], chiplets[20]]) { + + #################################################################################### + # Components requesting range checks + #################################################################################### + + # Stack values requiring 16-bit range checks (from decoder trace) + # These correspond to the top 4 operand stack elements during u32 operations + let sv0 = decoder[10]; # Stack value 0 + let sv1 = decoder[11]; # Stack value 1 + let sv2 = decoder[12]; # Stack value 2 + let sv3 = decoder[13]; # Stack value 3 + + # Memory chiplet values requiring 16-bit range checks + let mv0 = chiplets[14]; # Memory value 0 + let mv1 = chiplets[15]; # Memory value 1 + + #################################################################################### + # RANGE CHECKER STATE + #################################################################################### + + # Core range checker table columns + let value = range_checker[1]; # v: Current 16-bit value [0, 65535] + let multiplicity = range_checker[0]; # m: Usage count (how many times v is range-checked) + + #################################################################################### + # OPERATION FLAGS - Determine when range checks are needed + #################################################################################### + + # U32 range check operation flag + # Identifies stack operations that require 16-bit range checking + let not_4 = binary_not(decoder[5]); + let not_5 = binary_not(decoder[6]); + let u32_rc_op = decoder[7] * not_4 * not_5; + + # Memory chiplet operation flag + # Identifies memory operations that require range checking + let s_0 = chiplets[0]; + let s_1 = chiplets[1]; + let s_2 = chiplets[2]; + let chiplets_memory_flag = memory_chiplet_flag(s_0, s_1, s_2); + + #################################################################################### + # RANGE CHECKER INTERACTIONS + #################################################################################### + + # Each cycle, we insert the current value with its multiplicity + bus_4_range_checker.insert(value) with multiplicity; + + # Memory-related range checks + # When memory operations occur, verify that memory values are 16-bit + bus_4_range_checker.remove(mv0) when chiplets_memory_flag; + bus_4_range_checker.remove(mv1) when chiplets_memory_flag; + + # Stack-related range checks + # When u32 operations occur, verify that all operand components are 16-bit + bus_4_range_checker.remove(sv0) when u32_rc_op; + bus_4_range_checker.remove(sv1) when u32_rc_op; + bus_4_range_checker.remove(sv2) when u32_rc_op; + bus_4_range_checker.remove(sv3) when u32_rc_op; +} diff --git a/constraints/rpo.air b/constraints/rpo.air new file mode 100644 index 000000000..5061e8188 --- /dev/null +++ b/constraints/rpo.air @@ -0,0 +1,110 @@ + +mod rpo + +########################################################################################## +# RPO PERMUTATION ROUND CONSTRAINTS +########################################################################################## + +ev enforce_rpo_round([h[12]]){ + let ark1 = [ark1_0, ark1_1, ark1_2, ark1_3, ark1_4, ark1_5, ark1_6, ark1_7, ark1_8, ark1_9, + ark1_10, ark1_11]; + + let ark2 = [ark2_0, ark2_1, ark2_2, ark2_3, ark2_4, ark2_5, ark2_6, ark2_7, ark2_8, ark2_9, + ark2_10, ark2_11]; + + # Compute the state that should result from applying the first 5 steps of an RPO round to + # the current hasher state. + + # 1. Apply mds + let step1_initial = apply_mds(h); + + # 2. Add constants + let step1_with_constants = [s + k for (s, k) in (step1_initial, ark1)]; + + # 3. Apply sbox + let step1_with_sbox = [s^7 for s in step1_with_constants]; + + # 4. Apply mds + let step1_with_mds = apply_mds(step1_with_sbox); + + # 5. Add constants + let step1 = [s + k for (s, k) in (step1_with_mds, ark2)]; + + # Compute the state that should result from applying the inverse of the last operation of the + # RPO round to the next step of the computation. + let step2 = [s'^7 for s in h]; + + # Make sure that the results are equal. + enf s1 = s2 for (s1, s2) in (step1, step2); +} + +########################################################################################## +# HELPER FUNCTIONS +########################################################################################## + +fn apply_mds(state: felt[12]) -> felt[12]{ + # Compute dot product of state vector with each MDS row + let result0 = sum([s * m for (s, m) in (state, MDSROWA)]); + let result1 = sum([s * m for (s, m) in (state, MDSROWB)]); + let result2 = sum([s * m for (s, m) in (state, MDSROWC)]); + let result3 = sum([s * m for (s, m) in (state, MDSROWD)]); + let result4 = sum([s * m for (s, m) in (state, MDSROWE)]); + let result5 = sum([s * m for (s, m) in (state, MDSROWF)]); + let result6 = sum([s * m for (s, m) in (state, MDSROWG)]); + let result7 = sum([s * m for (s, m) in (state, MDSROWH)]); + let result8 = sum([s * m for (s, m) in (state, MDSROWI)]); + let result9 = sum([s * m for (s, m) in (state, MDSROWJ)]); + let result10 = sum([s * m for (s, m) in (state, MDSROWK)]); + let result11 = sum([s * m for (s, m) in (state, MDSROWL)]); + + return [result0, result1, result2, result3, result4, result5, + result6, result7, result8, result9, result10, result11]; +} + +########################################################################################## +# CONSTANTS AND PERIODIC COLUMNS +########################################################################################## + +# MDS matrix rows used for computing the linear layer in a RPO round +const MDSROWA = [7, 23, 8, 26, 13, 10, 9, 7, 6, 22, 21, 8]; +const MDSROWB = [8, 7, 23, 8, 26, 13, 10, 9, 7, 6, 22, 21]; +const MDSROWC = [21, 8, 7, 23, 8, 26, 13, 10, 9, 7, 6, 22]; +const MDSROWD = [22, 21, 8, 7, 23, 8, 26, 13, 10, 9, 7, 6]; +const MDSROWE = [6, 22, 21, 8, 7, 23, 8, 26, 13, 10, 9, 7]; +const MDSROWF = [7, 6, 22, 21, 8, 7, 23, 8, 26, 13, 10, 9]; +const MDSROWG = [9, 7, 6, 22, 21, 8, 7, 23, 8, 26, 13, 10]; +const MDSROWH = [10, 9, 7, 6, 22, 21, 8, 7, 23, 8, 26, 13]; +const MDSROWI = [13, 10, 9, 7, 6, 22, 21, 8, 7, 23, 8, 26]; +const MDSROWJ = [26, 13, 10, 9, 7, 6, 22, 21, 8, 7, 23, 8]; +const MDSROWK = [8, 26, 13, 10, 9, 7, 6, 22, 21, 8, 7, 23]; +const MDSROWL = [23, 8, 26, 13, 10, 9, 7, 6, 22, 21, 8, 7]; + +periodic_columns{ + # Round constants added to the hasher state in the first half of the RPO round + ark1_0: [5789762306288267264, 12987190162843097088, 18072785500942327808, 5674685213610122240, 4887609836208846848, 16308865189192448000, 7123075680859040768, 0], + ark1_1: [6522564764413702144, 653957632802705280, 6200974112677013504, 5759084860419474432, 3027115137917284352, 11977192855656443904, 1034205548717903104, 0], + ark1_2: [17809893479458207744, 4441654670647621120, 17682092219085883392, 13943282657648898048, 9595098600469471232, 12532242556065779712, 7717824418247931904, 0], + ark1_3: [107145243989736512, 4038207883745915904, 10599526828986757120, 1352748651966375424, 10528569829048483840, 14594890931430969344, 3019070937878604288, 0], + ark1_4: [6388978042437517312, 5613464648874829824, 975003873302957312, 17110913224029904896, 7864689113198940160, 7291784239689209856, 11403792746066868224, 0], + ark1_5: [15844067734406017024, 13222989726778339328, 8264241093196931072, 1003883795902368384, 17533723827845969920, 5514718540551361536, 10280580802233112576, 0], + ark1_6: [9975000513555218432, 3037761201230264320, 10065763900435474432, 4141870621881018368, 5781638039037711360, 10025733853830934528, 337153209462421248, 0], + ark1_7: [3344984123768313344, 16683759727265179648, 2181131744534710272, 8121410972417424384, 17024078752430718976, 7293794580341021696, 13333398568519923712, 0], + ark1_8: [9959189626657347584, 8337364536491240448, 6317303992309419008, 14300518605864919040, 109659393484013504, 6728552937464861696, 3596153696935337472, 0], + ark1_9: [12960773468763564032, 3227397518293416448, 1401440938888741632, 13712227150607669248, 7158933660534805504, 6332385040983343104, 8104208463525993472, 0], + ark1_10: [9602914297752487936, 8110510111539675136, 8884468225181997056, 17021852944633065472, 2955076958026921984, 13277683694236792832, 14345062289456084992, 0], + ark1_11: [16657542370200465408, 2872078294163232256, 13066900325715521536, 6252096473787587584, 7433723648458773504, 2600778905124452864, 17036731477169661952, 0], + + # Round constants added to the hasher state in the second half of the RPO round + ark2_0: [6077062762357203968, 6202948458916100096, 8023374565629191168, 18389244934624493568, 6982293561042363392, 3736792340494631424, 17130398059294019584, 0], + ark2_1: [15277620170502010880, 17690140365333231616, 15013690343205953536, 16731736864863924224, 14065426295947720704, 577852220195055360, 519782857322262016, 0], + ark2_2: [5358738125714196480, 3595001575307484672, 4485500052507913216, 4440209734760478208, 16451845770444974080, 6689998335515780096, 9625384390925084672, 0], + ark2_3: [14233283787297595392, 373995945117666496, 12489737547229155328, 17208448209698889728, 7139138592091307008, 13886063479078012928, 1664893052631119104, 0], + ark2_4: [13792579614346651648, 1235734395091296000, 9500452585969031168, 8739495587021565952, 9012006439959783424, 14358505101923203072, 7629576092524553216, 0], + ark2_5: [11614812331536766976, 14172757457833930752, 2054001340201038848, 17000774922218162176, 14619614108529063936, 7744142531772273664, 3485239601103661568, 0], + ark2_6: [14871063686742261760, 707573103686350208, 12420704059284934656, 13533282547195531264, 1394813199588124416, 16135070735728404480, 9755891797164034048, 0], + ark2_7: [10148237148793042944, 15453217512188186624, 355990932618543744, 525402848358706240, 4635111139507788800, 12290902521256030208, 15218148195153268736, 0], + ark2_8: [4457428952329675776, 219777875004506016, 9071225051243524096, 16987541523062161408, 16217473952264204288, 12059913662657710080, 16460604813734957056, 0], + ark2_9: [15590786458219171840, 17876696346199468032, 12766199826003447808, 5466806524462796800, 10782018226466330624, 16456018495793752064, 9643968136937730048, 0], + ark2_10: [10063319113072093184, 17731621626449383424, 9045979173463557120, 14512769585918244864, 6844229992533661696, 4571485474751953408, 3611348709641382912, 0], + ark2_11: [14200078843431360512, 2897136237748376064, 12934431667190679552, 10973956031244050432, 7446486531695178752, 17200392109565784064, 18256379591337758720, 0], +} diff --git a/constraints/stack.air b/constraints/stack.air new file mode 100644 index 000000000..f2b0898d9 --- /dev/null +++ b/constraints/stack.air @@ -0,0 +1,15 @@ +########################################################################################## +# STACK CONSTRAINTS MODULE +########################################################################################## +# +# The Stack module manages Miden VM's operand stack which is practically of unlimited depth +# (up to 2³² items), though only the top 16 stack items are directly accessible, with deeper +# items stored in an overflow virtual table. +# +# STATUS: Not implemented +# +# REFERENCES: +# - Stack Design: https://0xmiden.github.io/miden-vm/design/stack/main.html +########################################################################################## + +mod stack diff --git a/constraints/system.air b/constraints/system.air new file mode 100644 index 000000000..2495ab34d --- /dev/null +++ b/constraints/system.air @@ -0,0 +1,56 @@ +########################################################################################## +# SYSTEM CONSTRAINTS MODULE +########################################################################################## +# +# System module is responsible for managing system data, including the current VM cycle +# (clk), the free memory pointer (fmp) used for specifying the region of memory available +# to procedure locals, and the current and parent execution contexts. +# +# SYSTEM COLUMN LAYOUT (8 columns): +# ┌─────────┬──────────────────────────────────────────────────────────────────────┐ +# │ Column │ Purpose │ +# ├─────────┼──────────────────────────────────────────────────────────────────────┤ +# │ 0 │ clk - VM execution clock (increments each cycle) │ +# │ 1 │ fmp - Free memory pointer (procedure local memory region) │ +# │ 2 │ ctx - Current execution context │ +# │ 3 │ in_syscall - System call execution flag │ +# │ 4-7 │ Function hash - Current/parent function digest (4 elements) │ +# └─────────┴──────────────────────────────────────────────────────────────────────┘ +# +# +# STATUS: Not fully implemented +# +# REFERENCES: +# - System Design: https://0xmiden.github.io/miden-vm/design/main.html +########################################################################################## + +mod system + +########################################################################################## +# SYSTEM CONSTRAINT IMPLEMENTATION +########################################################################################## + +# Main system constraint evaluator - ensures proper system state transitions +ev system_transition([system[8]]) { + # Clock progression constraint + enf system_clock_transition([system[0]]); + + # TODO: Free memory pointer constraints + # TODO: Execution context constraints + # TODO: System call flag constraints + # TODO: Function hash management constraints +} + +########################################################################################## +# CLOCK CONSTRAINT +########################################################################################## + +# Clock increment by 1 constraint +# +# +# CONSTRAINT DEGREE: 1 (linear) +# +# PURPOSE: Ensures VM execution cycles increase monotonically +ev system_clock_transition([clk]) { + enf clk' = clk + 1; +} diff --git a/constraints/tests/miden_vm.rs b/constraints/tests/miden_vm.rs new file mode 100644 index 000000000..8509937d1 --- /dev/null +++ b/constraints/tests/miden_vm.rs @@ -0,0 +1,45 @@ +use std::sync::Arc; + +use air_codegen_ace::{build_ace_circuit, AceCircuit, AceNode}; +use air_ir::{compile, Air}; +use miden_diagnostics::{ + term::termcolor::ColorChoice, CodeMap, DefaultEmitter, DiagnosticsHandler, +}; +use winter_math::FieldElement; + +fn generate_circuit(source: &str) -> (Air, AceCircuit, AceNode) { + let code_map = Arc::new(CodeMap::new()); + let emitter = Arc::new(DefaultEmitter::new(ColorChoice::Auto)); + let diagnostics = DiagnosticsHandler::new(Default::default(), code_map.clone(), emitter); + + let air = air_parser::parse(&diagnostics, code_map, source) + .map_err(air_ir::CompileError::Parse) + .and_then(|program| compile(&diagnostics, program)) + .expect("lowering failed"); + + let (root, circuit) = build_ace_circuit(&air).expect("codegen failed"); + + (air, circuit, root) +} + +/// Loads the MidenVM AIR example +pub fn load_miden_vm_air() -> std::io::Result { + let crate_dir = std::env::var("CARGO_MANIFEST_DIR").unwrap(); + let path = format!("{}/miden_vm.air", crate_dir); + let content = std::fs::read_to_string(path)?; + + Ok(content) +} + +#[test] +fn test_miden_vm_updated_air_randomized() { + let air_string = load_miden_vm_air().expect("unable to read MidenVM AIR"); + + let (_air, circuit, root_node) = generate_circuit(&air_string); + + // Provide dummy variable assignments since we are not generating valid ACE vars here + let dummy_inputs = vec![Default::default(); circuit.layout.num_inputs]; + let eval = circuit.eval(root_node, &dummy_inputs); + + assert_eq!(eval, <_ as FieldElement>::ZERO); +} diff --git a/constraints/utils.air b/constraints/utils.air new file mode 100644 index 000000000..5af593a2c --- /dev/null +++ b/constraints/utils.air @@ -0,0 +1,142 @@ +########################################################################################## +# UTILITY CONSTRAINTS MODULE +########################################################################################## +# +# The Utils module provides fundamental constraint patterns and helper functions used +# throughout the Miden VM constraint system. These utilities ensure consistency and +# reusability across all VM components. +# +########################################################################################## + +mod utils + +########################################################################################## +# BINARY CONSTRAINT EVALUATORS +########################################################################################## + +# Ensures value is either 0 or 1 +# +# CONSTRAINT DEGREE: 2 +# +# USAGE PATTERN: +# ```air +# let flag = column[i]; +# enf is_binary([flag]); // Ensures flag ∈ {0, 1} +# ``` +ev is_binary([a]) { + enf a^2 = a; +} + +########################################################################################## +# STATE CONSISTENCY EVALUATORS +########################################################################################## + +# State persistence constraint - ensures values remain constant across cycles +# +# INTUITION: +# +# Many VM components require certain values to remain stable during specific +# operations or phases. This constraint enforces immutability when needed. +# +# CONSTRAINT DEGREE: 1 +# +# USAGE PATTERN: +# ```air +# let stable_value = column[i]; +# enf is_unchanged([stable_value]) when operation_active; +# ``` +ev is_unchanged([column]) { + enf column' = column; +} + +########################################################################################## +# LOGICAL OPERATION HELPERS +########################################################################################## + +# Binary negation function - computes logical NOT in finite field +# +# This is usually combined with another constraint to ensure booleaness +# +# CONSTRAINT DEGREE: 1 +# +# USAGE EXAMPLES: +# ```air +# let not_flag = binary_not(flag); // Simple negation +# let condition = flag * binary_not(other); // AND NOT pattern +# ``` +fn binary_not(a: felt) -> felt { + return 1 - a; +} + +# Binary constraint helper - returns 0 if input is binary (0 or 1), non-zero otherwise +# +# This function computes flag² - flag, which equals: +# - 0 when flag = 0 (since 0² - 0 = 0) +# - 0 when flag = 1 (since 1² - 1 = 0) +# - non-zero for any other value +# +# Usage: enf binary_constraint(x) = 0; // constrains x to be 0 or 1 +fn binary_constraint(flag: felt) -> felt { + return flag^2 - flag; +} + +########################################################################################## +# BOOLEAN ALGEBRA OPERATIONS +########################################################################################## + +# Logical AND: returns 1 if both a and b are 1, else 0 +# +# CONSTRAINT DEGREE: 2 +# +# USAGE EXAMPLES: +# ```air +# let result = binary_and(flag_a, flag_b); +# ``` +fn binary_and(a: felt, b: felt) -> felt { + return a * b; +} + +# Logical OR: returns 1 if either a or b is 1, else 0 +# +# Uses inclusion-exclusion principle: |A ∪ B| = |A| + |B| - |A ∩ B| +# +# CONSTRAINT DEGREE: 2 +# +# USAGE EXAMPLES: +# ```air +# let result = binary_or(flag_a, flag_b); +# ``` +fn binary_or(a: felt, b: felt) -> felt { + return a + b - a * b; +} + +# Logical XOR: returns 1 if exactly one of a or b is 1, else 0 +# +# CONSTRAINT DEGREE: 2 +# +# USAGE EXAMPLES: +# ```air +# let result = binary_xor(flag_a, flag_b); +# ``` +fn binary_xor(a: felt, b: felt) -> felt { + let ab = a * b; + return a + b - (ab + ab); +} + +########################################################################################## +# CONDITIONAL OPERATIONS +########################################################################################## + +# Conditional selection: returns if_true when condition=1, if_false when condition=0 +# +# This is a multiplexer function that selects between two values based on condition +# +# CONSTRAINT DEGREE: 2 +# +# USAGE EXAMPLES: +# ```air +# let result = select(condition, true_value, false_value); +# ``` +fn select(condition: felt, if_true: felt, if_false: felt) -> felt { + return condition * (if_true - if_false) + if_false; +} diff --git a/mir/src/passes/translate.rs b/mir/src/passes/translate.rs index db342ecb7..e1e54acf9 100644 --- a/mir/src/passes/translate.rs +++ b/mir/src/passes/translate.rs @@ -695,7 +695,7 @@ impl<'a> MirBuilder<'a> { // At this point during compilation, fully-qualified identifiers can only possibly refer // to a periodic column, as all functions have been inlined, and constants propagated. ast::ResolvableIdentifier::Resolved(qual_ident) => { - if let Some(pc) = self.mir.periodic_columns.get(&qual_ident).cloned() { + if let Some(pc) = self.mir.periodic_columns.get(qual_ident).cloned() { let node = Value::builder() .value(SpannedMirValue { span: access.span(), @@ -706,7 +706,7 @@ impl<'a> MirBuilder<'a> { }) .build(); Ok(node) - } else if let Some(bus) = self.mir.constraint_graph().get_bus_link(&qual_ident) { + } else if let Some(bus) = self.mir.constraint_graph().get_bus_link(qual_ident) { let node = Value::builder() .value(SpannedMirValue { span: access.span(), @@ -714,6 +714,10 @@ impl<'a> MirBuilder<'a> { }) .build(); Ok(node) + } else if let Some(constant) = self.program.constants.get(qual_ident) { + // Handle qualified constant references that weren't inlined + // (e.g., constants used in comprehension iterables across modules) + self.translate_const(&constant.value, access.span()) } else { // This is a qualified reference that should have been eliminated // during inlining or constant propagation, but somehow slipped through. @@ -735,7 +739,7 @@ impl<'a> MirBuilder<'a> { }, // This must be one of public inputs or trace columns ast::ResolvableIdentifier::Global(ident) | ast::ResolvableIdentifier::Local(ident) => { - self.translate_symbol_access_global_or_local(&ident, access) + self.translate_symbol_access_global_or_local(ident, access) }, // These should have been eliminated by previous compiler passes ast::ResolvableIdentifier::Unresolved(_ident) => { @@ -1063,7 +1067,8 @@ impl<'a> MirBuilder<'a> { access: &'a ast::SymbolAccess, ) -> Option> { // If it's a slice access, we need to create a vector of MirAccessType::Index - if let AccessType::Slice(ast::RangeExpr { start, end, .. }) = &access.access_type { + if let AccessType::Slice(range) = &access.access_type { + let ast::RangeExpr { start, end, .. } = range.as_ref(); let ( ast::RangeBound::Const(Span { item: start, .. }), ast::RangeBound::Const(Span { item: end, .. }), diff --git a/parser/src/ast/expression.rs b/parser/src/ast/expression.rs index 97f26fa94..1ad12bb80 100644 --- a/parser/src/ast/expression.rs +++ b/parser/src/ast/expression.rs @@ -865,7 +865,7 @@ pub enum AccessType { #[default] Default, /// Access binds a sub-slice of a vector - Slice(RangeExpr), + Slice(Box), /// Access binds the value at a specific index of an aggregate value (i.e. vector or matrix) /// /// The result type may be either a scalar or a vector, depending on the type of the aggregate @@ -1073,7 +1073,7 @@ impl SymbolAccess { Err(InvalidAccessError::IndexOutOfBounds) }, Type::Vector(_) => Ok(Self { - access_type: AccessType::Slice(shifted), + access_type: AccessType::Slice(Box::new(shifted.clone())), ty: Some(Type::Vector(rlen)), ..self.clone() }), @@ -1081,7 +1081,7 @@ impl SymbolAccess { Err(InvalidAccessError::IndexOutOfBounds) }, Type::Matrix(_, cols) => Ok(Self { - access_type: AccessType::Slice(shifted), + access_type: AccessType::Slice(Box::new(shifted)), ty: Some(Type::Matrix(rlen, cols)), ..self.clone() }), diff --git a/parser/src/ast/trace.rs b/parser/src/ast/trace.rs index 5b26a05d0..71fab9071 100644 --- a/parser/src/ast/trace.rs +++ b/parser/src/ast/trace.rs @@ -287,7 +287,7 @@ impl TraceBinding { let range_expr1 = range_expr1.to_slice_range(); let combined_range = (range_expr.start + range_expr1.start)..(range_expr.end + range_expr1.end); - AccessType::Slice(combined_range.into()) + AccessType::Slice(Box::new(combined_range.into())) }, (AccessType::Slice(range_expr), AccessType::Index(index_expr)) => { let range_expr_usize = range_expr.to_slice_range(); diff --git a/parser/src/lexer/mod.rs b/parser/src/lexer/mod.rs index f354cf6f4..8265300ae 100644 --- a/parser/src/lexer/mod.rs +++ b/parser/src/lexer/mod.rs @@ -644,10 +644,9 @@ where match num.parse::() { Ok(i) => Token::Num(i), - Err(err) => Token::Error(LexicalError::InvalidInt { - span: self.span(), - reason: err.kind().clone(), - }), + Err(err) => { + Token::Error(LexicalError::InvalidInt { span: self.span(), reason: *err.kind() }) + }, } } } diff --git a/parser/src/parser/grammar.lalrpop b/parser/src/parser/grammar.lalrpop index b06578f68..e05958009 100644 --- a/parser/src/parser/grammar.lalrpop +++ b/parser/src/parser/grammar.lalrpop @@ -560,7 +560,7 @@ SymbolAccessBaseSpanned: Span<(Identifier, AccessType)> = { SymbolAccessBase: (Identifier, AccessType) = { => (ident, AccessType::Default), - "[" "]" => (ident, AccessType::Slice(range)), + "[" "]" => (ident, AccessType::Slice(Box::new(range))), => (ident, AccessType::Index(idx)), => (ident, AccessType::Matrix(row, col)), // accessing an identifier used in a section declaration, like a named trace segment, e.g. $main @@ -611,7 +611,7 @@ Iterables: Vec = { Iterable: Expr = { => Expr::SymbolAccess(SymbolAccess::new(ident.span(), ident, AccessType::Default, 0)), => Expr::Range(range), - "[" "]" => Expr::SymbolAccess(SymbolAccess::new(span!(l, r), ident, AccessType::Slice(range), 0)), + "[" "]" => Expr::SymbolAccess(SymbolAccess::new(span!(l, r), ident, AccessType::Slice(Box::new(range)), 0)), => if let ScalarExpr::Call(call) = function_call { Expr::Call(call) } else { diff --git a/parser/src/parser/tests/mod.rs b/parser/src/parser/tests/mod.rs index aa1a162e1..1b18c60fc 100644 --- a/parser/src/parser/tests/mod.rs +++ b/parser/src/parser/tests/mod.rs @@ -426,7 +426,7 @@ macro_rules! slice { ScalarExpr::SymbolAccess(SymbolAccess { span: miden_diagnostics::SourceSpan::UNKNOWN, name: ResolvableIdentifier::Unresolved(NamespacedIdentifier::Binding(ident!($name))), - access_type: AccessType::Slice($range.into()), + access_type: AccessType::Slice(Box::new($range.into())), offset: 0, ty: None, }) @@ -436,7 +436,7 @@ macro_rules! slice { ScalarExpr::SymbolAccess(SymbolAccess { span: miden_diagnostics::SourceSpan::UNKNOWN, name: ResolvableIdentifier::Local(ident!($name)), - access_type: AccessType::Slice($range.into()), + access_type: AccessType::Slice(Box::new($range.into())), offset: 0, ty: Some($ty), }) diff --git a/parser/src/sema/semantic_analysis.rs b/parser/src/sema/semantic_analysis.rs index 09d89426f..b4bf9597e 100644 --- a/parser/src/sema/semantic_analysis.rs +++ b/parser/src/sema/semantic_analysis.rs @@ -444,9 +444,9 @@ impl VisitMut for SemanticAnalysis<'_> { self.current_module.clone().unwrap(), NamespacedIdentifier::Function(function.name), ); - let current_item_node_index = self.deps_graph.add_node(current_item); - for (referenced_item, ref_type) in self.referenced.iter() { - let referenced_item_node_index = self.deps_graph.add_node(referenced_item.clone()); + let current_item_node_index = self.get_node_index_or_add(¤t_item); + for (referenced_item, ref_type) in self.referenced.clone().iter() { + let referenced_item_node_index = self.get_node_index_or_add(referenced_item); self.deps_graph.add_edge( current_item_node_index, referenced_item_node_index, @@ -633,6 +633,15 @@ impl VisitMut for SemanticAnalysis<'_> { 0, ))))) .expect("unexpected scalar iterable"); + // Comprehension bindings are local variables holding values, not direct + // references to module-level declarations like periodic columns or constants. + // Convert these to Local bindings to ensure proper scoping. + let binding_ty = match binding_ty { + BindingType::PeriodicColumn(_) | BindingType::Constant(_) => { + BindingType::Local(binding_ty.ty().unwrap_or(Type::Felt)) + }, + other => other, + }; binding_tys.push((binding, iterable.span(), Some(binding_ty))); }, Err(InvalidAccessError::InvalidBinding) => {