diff --git a/air/src/constraints/chiplets/mod.rs b/air/src/constraints/chiplets/mod.rs index 2f74ccd30..ebbfc80ef 100644 --- a/air/src/constraints/chiplets/mod.rs +++ b/air/src/constraints/chiplets/mod.rs @@ -5,7 +5,7 @@ use super::super::{ }; use crate::utils::{are_equal, binary_not, is_binary}; -mod bitwise; +pub mod bitwise; pub mod hasher; mod memory; diff --git a/air/src/logup_gkr/chiplets_bus.rs b/air/src/logup_gkr/chiplets_bus.rs new file mode 100644 index 000000000..2193fed75 --- /dev/null +++ b/air/src/logup_gkr/chiplets_bus.rs @@ -0,0 +1,495 @@ +use vm_core::{ExtensionOf, FieldElement}; + +use super::{inner_product, LogUpOpFlags}; +use crate::{ + decoder::{DECODER_HASHER_STATE_OFFSET, DECODER_USER_OP_HELPERS_OFFSET}, + trace::{ + chiplets::{ + kernel_rom::KERNEL_PROC_LABEL_RAW, + memory::{MEMORY_READ_LABEL, MEMORY_WRITE_LABEL}, + BITWISE_A_COL_IDX, BITWISE_B_COL_IDX, BITWISE_OUTPUT_COL_IDX, MEMORY_ADDR_COL_IDX, + MEMORY_CLK_COL_IDX, MEMORY_CTX_COL_IDX, MEMORY_V_COL_RANGE, + }, + stack::STACK_TOP_OFFSET, + }, + CHIPLETS_OFFSET, CLK_COL_IDX, CTX_COL_IDX, STACK_TRACE_OFFSET, +}; + +#[inline(always)] +pub fn bus( + query_current: &[F], + query_next: &[F], + bitwise_periodic_values: &[F], + op_flags: &LogUpOpFlags, + alphas: &[E], + numerator: &mut [E], + denominator: &mut [E], +) where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + let bitwise_reponse = + get_bitwise_chiplet_response(query_current, bitwise_periodic_values, alphas); + let [u32xor_request, u32and_request] = + get_u32andxor_requests(query_current, query_next, op_flags, alphas); + let kernel_chiplet_response = get_kernel_chiplet_response(query_current, alphas); + let syscall_kernel_request = get_syscall_kernel_request(query_current, op_flags, alphas); + let memory_chiplet_response = get_memory_chiplet_response(query_current, alphas); + let [mload_req, mstore_req] = + get_mload_mstore_requests(query_current, query_next, op_flags, alphas); + let [mloadw_req, mstorew_req] = + get_mloadw_mstorew_requests(query_current, query_next, op_flags, alphas); + let [pipe_req1, pipe_req2] = + get_pipe_memory_requests(query_current, query_next, op_flags, alphas); + let [mstream_req1, mstream_req2] = + get_mstream_memory_requests(query_current, query_next, op_flags, alphas); + let [rcombbase_req1, rcombbase_req2] = + get_rcombbase_memory_requests(query_current, op_flags, alphas); + + // bitwise chiplet + (numerator[0], denominator[0]) = bitwise_reponse; + (numerator[1], denominator[1]) = u32xor_request; + (numerator[2], denominator[2]) = u32and_request; + + // kernel chiplet + (numerator[3], denominator[3]) = kernel_chiplet_response; + (numerator[4], denominator[4]) = syscall_kernel_request; + + // memory chiplet + (numerator[5], denominator[5]) = memory_chiplet_response; + (numerator[6], denominator[6]) = mload_req; + (numerator[7], denominator[7]) = mstore_req; + (numerator[8], denominator[8]) = mloadw_req; + (numerator[9], denominator[9]) = mstorew_req; + (numerator[10], denominator[10]) = pipe_req1; + (numerator[11], denominator[11]) = pipe_req2; + (numerator[12], denominator[12]) = mstream_req1; + (numerator[13], denominator[13]) = mstream_req2; + (numerator[14], denominator[14]) = rcombbase_req1; + (numerator[15], denominator[15]) = rcombbase_req2; +} + +// RESPONSES +// =============================================================================================== + +#[inline(always)] +fn get_bitwise_chiplet_response( + query_current: &[F], + bitwise_periodic_values: &[F], + alphas: &[E], +) -> (E, E) +where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + let numerator = { + let f_is_bitwise_chiplet: E = { + let bitwise_selec0 = query_current[CHIPLETS_OFFSET]; + let bitwise_selec1 = F::ONE - query_current[CHIPLETS_OFFSET + 1]; + + (bitwise_selec0 * bitwise_selec1).into() + }; + let is_last_periodic_row: E = (F::ONE - bitwise_periodic_values[1]).into(); + + f_is_bitwise_chiplet * is_last_periodic_row + }; + let denominator = { + let is_xor = query_current[CHIPLETS_OFFSET + 2]; + let op_label_is_xor = get_op_label(F::ONE, F::ZERO, is_xor, F::ZERO); + let a = query_current[BITWISE_A_COL_IDX]; + let b = query_current[BITWISE_B_COL_IDX]; + let z = query_current[BITWISE_OUTPUT_COL_IDX]; + + alphas[0] + inner_product(&alphas[1..5], &[op_label_is_xor, a, b, z]) + }; + + (numerator, denominator) +} + +#[inline(always)] +fn get_kernel_chiplet_response(query_current: &[F], alphas: &[E]) -> (E, E) +where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + // numerator + let numerator = { + let is_kernel_chiplet = { + let selector0 = query_current[CHIPLETS_OFFSET]; + let selector1 = query_current[CHIPLETS_OFFSET + 1]; + let selector2 = query_current[CHIPLETS_OFFSET + 2]; + let selector3 = query_current[CHIPLETS_OFFSET + 3]; + + selector0 * selector1 * selector2 * (F::ONE - selector3) + }; + + let include_row_in_bus = query_current[CHIPLETS_OFFSET + 4]; + + E::from(is_kernel_chiplet * include_row_in_bus) + }; + + // denominator + let denominator = { + let root0 = query_current[CHIPLETS_OFFSET + 6]; + let root1 = query_current[CHIPLETS_OFFSET + 7]; + let root2 = query_current[CHIPLETS_OFFSET + 8]; + let root3 = query_current[CHIPLETS_OFFSET + 9]; + + alphas[0] + + inner_product( + &alphas[1..6], + &[KERNEL_PROC_LABEL_RAW.into(), root0, root1, root2, root3], + ) + }; + + (numerator, denominator) +} + +#[inline(always)] +fn get_memory_chiplet_response(query_current: &[F], alphas: &[E]) -> (E, E) +where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + let is_memory_chiplet = { + let selector0 = query_current[CHIPLETS_OFFSET]; + let selector1 = query_current[CHIPLETS_OFFSET + 1]; + let selector2 = query_current[CHIPLETS_OFFSET + 2]; + + selector0 * selector1 * (F::ONE - selector2) + }; + + let denominator = { + let op_label = { + let is_read = query_current[CHIPLETS_OFFSET + 3]; + get_op_label(F::ONE, F::ONE, F::ZERO, is_read) + }; + let ctx = query_current[MEMORY_CTX_COL_IDX]; + let clk = query_current[MEMORY_CLK_COL_IDX]; + let mem_addr = query_current[MEMORY_ADDR_COL_IDX]; + let mem_value = &query_current[MEMORY_V_COL_RANGE]; + + compute_memory_message(alphas, op_label, ctx, mem_addr, clk, mem_value) + }; + + (is_memory_chiplet.into(), denominator) +} + +// REQUESTS +// =============================================================================================== + +#[inline(always)] +fn get_u32andxor_requests( + query_current: &[F], + query_next: &[F], + op_flags: &LogUpOpFlags, + alphas: &[E], +) -> [(E, E); 2] +where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + // numerators + let u32xor_numerator = op_flags.f_u32_xor().into(); + let u32and_numerator = op_flags.f_u32_and().into(); + + // denominators + let op_label_is_xor = get_op_label(F::ONE, F::ZERO, F::ONE, F::ZERO); + let op_label_is_and = get_op_label(F::ONE, F::ZERO, F::ZERO, F::ZERO); + let a = query_current[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 1]; + let b = query_current[STACK_TRACE_OFFSET + STACK_TOP_OFFSET]; + let z = query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET]; + + let u32xor_denominator = + -(alphas[0] + inner_product(&alphas[1..5], &[op_label_is_xor, a, b, z])); + let u32and_denominator = + -(alphas[0] + inner_product(&alphas[1..5], &[op_label_is_and, a, b, z])); + + [(u32xor_numerator, u32xor_denominator), (u32and_numerator, u32and_denominator)] +} + +#[inline(always)] +fn get_syscall_kernel_request( + query_current: &[F], + op_flags: &LogUpOpFlags, + alphas: &[E], +) -> (E, E) +where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + let numerator: E = op_flags.f_syscall().into(); + + let denominator = { + let op_label: F = KERNEL_PROC_LABEL_RAW.into(); + let root0 = query_current[DECODER_HASHER_STATE_OFFSET]; + let root1 = query_current[DECODER_HASHER_STATE_OFFSET + 1]; + let root2 = query_current[DECODER_HASHER_STATE_OFFSET + 2]; + let root3 = query_current[DECODER_HASHER_STATE_OFFSET + 3]; + + -(alphas[0] + inner_product(&alphas[1..6], &[op_label, root0, root1, root2, root3])) + }; + + (numerator, denominator) +} + +/// Returns the memory request for `MLOAD` and `MSTORE`. +#[inline(always)] +fn get_mload_mstore_requests( + query_current: &[F], + query_next: &[F], + op_flags: &LogUpOpFlags, + alphas: &[E], +) -> [(E, E); 2] +where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + // the value read or written + let mem_value = [ + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET], + query_current[DECODER_USER_OP_HELPERS_OFFSET + 2], + query_current[DECODER_USER_OP_HELPERS_OFFSET + 1], + query_current[DECODER_USER_OP_HELPERS_OFFSET], + ]; + let mem_addr = query_current[STACK_TRACE_OFFSET + STACK_TOP_OFFSET]; + let ctx = query_current[CTX_COL_IDX]; + let clk = query_current[CLK_COL_IDX]; + + let mload_req = ( + op_flags.f_mload().into(), + -compute_memory_message(alphas, MEMORY_READ_LABEL.into(), ctx, mem_addr, clk, &mem_value), + ); + + let mstore_req = ( + op_flags.f_mstore().into(), + -compute_memory_message(alphas, MEMORY_WRITE_LABEL.into(), ctx, mem_addr, clk, &mem_value), + ); + + [mload_req, mstore_req] +} + +/// Returns the memory request for `MLOADW` and `MSTOREW`. +#[inline(always)] +fn get_mloadw_mstorew_requests( + query_current: &[F], + query_next: &[F], + op_flags: &LogUpOpFlags, + alphas: &[E], +) -> [(E, E); 2] +where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + // the value read or written + let mem_value = [ + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 3], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 2], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 1], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET], + ]; + let mem_addr = query_current[STACK_TRACE_OFFSET + STACK_TOP_OFFSET]; + let ctx = query_current[CTX_COL_IDX]; + let clk = query_current[CLK_COL_IDX]; + + let mloadw_req = ( + op_flags.f_mloadw().into(), + -compute_memory_message(alphas, MEMORY_READ_LABEL.into(), ctx, mem_addr, clk, &mem_value), + ); + + let mstorew_req = ( + op_flags.f_mstorew().into(), + -compute_memory_message(alphas, MEMORY_WRITE_LABEL.into(), ctx, mem_addr, clk, &mem_value), + ); + + [mloadw_req, mstorew_req] +} + +/// Returns the memory requests associated with the `PIPE` operation. +#[inline(always)] +fn get_pipe_memory_requests( + query_current: &[F], + query_next: &[F], + op_flags: &LogUpOpFlags, + alphas: &[E], +) -> [(E, E); 2] +where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + let f_pipe_flag: E = op_flags.f_pipe().into(); + let op_label: F = MEMORY_WRITE_LABEL.into(); + let ctx = query_current[CTX_COL_IDX]; + let clk = query_current[CLK_COL_IDX]; + + let req1 = { + let mem_value = [ + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 7], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 6], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 5], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 4], + ]; + let mem_addr = query_current[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 12]; + + ( + f_pipe_flag, + -compute_memory_message(alphas, op_label, ctx, mem_addr, clk, &mem_value), + ) + }; + let req2 = { + let mem_value = [ + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 3], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 2], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 1], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET], + ]; + let mem_addr = query_current[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 12] + F::ONE; + + ( + f_pipe_flag, + -compute_memory_message(alphas, op_label, ctx, mem_addr, clk, &mem_value), + ) + }; + + [req1, req2] +} + +/// Returns the memory requests associated with the `MSTREAM` operation. +#[inline(always)] +fn get_mstream_memory_requests( + query_current: &[F], + query_next: &[F], + op_flags: &LogUpOpFlags, + alphas: &[E], +) -> [(E, E); 2] +where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + let f_mstream_flag: E = op_flags.f_mstream().into(); + let op_label: F = MEMORY_READ_LABEL.into(); + let ctx = query_current[CTX_COL_IDX]; + let clk = query_current[CLK_COL_IDX]; + + let req1 = { + let mem_value = [ + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 7], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 6], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 5], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 4], + ]; + let mem_addr = query_current[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 12]; + + ( + f_mstream_flag, + -compute_memory_message(alphas, op_label, ctx, mem_addr, clk, &mem_value), + ) + }; + let req2 = { + let mem_value = [ + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 3], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 2], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 1], + query_next[STACK_TRACE_OFFSET + STACK_TOP_OFFSET], + ]; + let mem_addr = query_current[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 12] + F::ONE; + + ( + f_mstream_flag, + -compute_memory_message(alphas, op_label, ctx, mem_addr, clk, &mem_value), + ) + }; + + [req1, req2] +} + +/// Returns the memory requests associated with the `RCOMBBASE` operation. +#[inline(always)] +fn get_rcombbase_memory_requests( + query_current: &[F], + op_flags: &LogUpOpFlags, + alphas: &[E], +) -> [(E, E); 2] +where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + let f_rcombbase_flag: E = op_flags.f_rcombbase().into(); + let op_label: F = MEMORY_READ_LABEL.into(); + let ctx = query_current[CTX_COL_IDX]; + let clk = query_current[CLK_COL_IDX]; + + let req1 = { + let mem_value = { + let tz0 = query_current[DECODER_USER_OP_HELPERS_OFFSET]; + let tz1 = query_current[DECODER_USER_OP_HELPERS_OFFSET + 1]; + let tzg0 = query_current[DECODER_USER_OP_HELPERS_OFFSET + 2]; + let tzg1 = query_current[DECODER_USER_OP_HELPERS_OFFSET + 3]; + [tz0, tz1, tzg0, tzg1] + }; + let mem_addr = query_current[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 13]; + + ( + f_rcombbase_flag, + -compute_memory_message(alphas, op_label, ctx, mem_addr, clk, &mem_value), + ) + }; + + let req2 = { + let mem_value = { + let a0 = query_current[DECODER_USER_OP_HELPERS_OFFSET + 4]; + let a1 = query_current[DECODER_USER_OP_HELPERS_OFFSET + 5]; + + [a0, a1, F::ZERO, F::ZERO] + }; + let mem_addr = query_current[STACK_TRACE_OFFSET + STACK_TOP_OFFSET + 14]; + + ( + f_rcombbase_flag, + -compute_memory_message(alphas, op_label, ctx, mem_addr, clk, &mem_value), + ) + }; + + [req1, req2] +} + +// HELPERS +// ============================================================================================== + +/// Computes a memory message (request or response) given randomness `alphas`. +#[inline(always)] +fn compute_memory_message( + alphas: &[E], + op_label: F, + ctx: F, + mem_addr: F, + clk: F, + mem_value: &[F], +) -> E +where + F: FieldElement, + E: FieldElement + ExtensionOf, +{ + alphas[0] + + inner_product( + alphas, + &[ + op_label, + ctx, + mem_addr, + clk, + mem_value[0], + mem_value[1], + mem_value[2], + mem_value[3], + ], + ) +} + +/// Returns the operation unique label. +fn get_op_label(s0: F, s1: F, s2: F, s3: F) -> F +where + F: FieldElement, +{ + s3 * (1_u32 << 3).into() + s2 * (1_u32 << 2).into() + s1 * 2_u32.into() + s0 + F::ONE +} diff --git a/air/src/logup_gkr.rs b/air/src/logup_gkr/mod.rs similarity index 88% rename from air/src/logup_gkr.rs rename to air/src/logup_gkr/mod.rs index f028f47bc..cd02a966e 100644 --- a/air/src/logup_gkr.rs +++ b/air/src/logup_gkr/mod.rs @@ -5,7 +5,10 @@ use vm_core::{utils::range, ExtensionOf, Felt, FieldElement, StarkField}; use winter_air::{EvaluationFrame, LogUpGkrEvaluator, LogUpGkrOracle}; use crate::{ - constraints::chiplets::hasher::{HASH_K0_MASK, HASH_K1_MASK, HASH_K2_MASK}, + constraints::chiplets::{ + bitwise::{BITWISE_K0_MASK, BITWISE_K1_MASK}, + hasher::{HASH_K0_MASK, HASH_K1_MASK, HASH_K2_MASK}, + }, decoder::{ DECODER_ADDR_COL_IDX, DECODER_GROUP_COUNT_COL_IDX, DECODER_HASHER_STATE_OFFSET, DECODER_IN_SPAN_COL_IDX, DECODER_IS_CALL_FLAG_COL_IDX, DECODER_IS_LOOP_BODY_FLAG_COL_IDX, @@ -25,6 +28,8 @@ use crate::{ TRACE_WIDTH, }; +mod chiplets_bus; + // CONSTANTS // =============================================================================================== @@ -36,7 +41,7 @@ const fn const_max(a: usize, b: usize) -> usize { // Random values /// The number of random values used as offsets (alpha_0 is our docs) -pub const NUM_OFFSET_RAND_VALUES: usize = 6; +pub const NUM_OFFSET_RAND_VALUES: usize = 7; const RANGE_CHECKER_NUM_RAND_LINCOMB_VALUES: usize = 0; const OP_GROUP_TABLE_NUM_RAND_LINCOMB_VALUES: usize = 3; @@ -44,6 +49,7 @@ const BLOCK_HASH_TABLE_NUM_RAND_LINCOMB_VALUES: usize = 7; const BLOCK_STACK_TABLE_NUM_RAND_LINCOMB_VALUES: usize = 11; const HASHER_TABLE_NUM_RAND_LINCOMB_VALUES: usize = 15; const KERNEL_PROC_TABLE_NUM_RAND_LINCOMB_VALUES: usize = 5; +const CHIPLETS_BUS_NUM_RAND_LINCOMB_VALUES: usize = 16; /// The number of random values to generate to support all random linear combinations. /// @@ -54,16 +60,19 @@ pub const MAX_RAND_LINCOMB_VALUES: usize = const_max( const_max( const_max( const_max( - RANGE_CHECKER_NUM_RAND_LINCOMB_VALUES, - OP_GROUP_TABLE_NUM_RAND_LINCOMB_VALUES, + const_max( + RANGE_CHECKER_NUM_RAND_LINCOMB_VALUES, + OP_GROUP_TABLE_NUM_RAND_LINCOMB_VALUES, + ), + BLOCK_HASH_TABLE_NUM_RAND_LINCOMB_VALUES, ), - BLOCK_HASH_TABLE_NUM_RAND_LINCOMB_VALUES, + BLOCK_STACK_TABLE_NUM_RAND_LINCOMB_VALUES, ), - BLOCK_STACK_TABLE_NUM_RAND_LINCOMB_VALUES, + HASHER_TABLE_NUM_RAND_LINCOMB_VALUES, ), - HASHER_TABLE_NUM_RAND_LINCOMB_VALUES, + KERNEL_PROC_TABLE_NUM_RAND_LINCOMB_VALUES, ), - KERNEL_PROC_TABLE_NUM_RAND_LINCOMB_VALUES, + CHIPLETS_BUS_NUM_RAND_LINCOMB_VALUES, ); /// The total number of random values to generate @@ -94,8 +103,12 @@ pub const KERNEL_PROC_TABLE_FRACTIONS_OFFSET: usize = HASHER_TABLE_FRACTIONS_OFFSET + HASHER_TABLE_NUM_FRACTIONS; pub const KERNEL_PROC_TABLE_NUM_FRACTIONS: usize = 1; -pub const PADDING_FRACTIONS_OFFSET: usize = +pub const CHIPLETS_BUS_FRACTIONS_OFFSET: usize = KERNEL_PROC_TABLE_FRACTIONS_OFFSET + KERNEL_PROC_TABLE_NUM_FRACTIONS; +pub const CHIPLETS_BUS_NUM_FRACTIONS: usize = 16; + +pub const PADDING_FRACTIONS_OFFSET: usize = + CHIPLETS_BUS_FRACTIONS_OFFSET + CHIPLETS_BUS_NUM_FRACTIONS; pub const PADDING_NUM_FRACTIONS: usize = TOTAL_NUM_FRACTIONS - PADDING_FRACTIONS_OFFSET; pub const TOTAL_NUM_FRACTIONS: usize = 64; @@ -132,7 +145,13 @@ impl LogUpGkrEvaluator for MidenLogUpGkrEval { } fn get_periodic_column_values(&self) -> Vec> { - vec![HASH_K0_MASK.to_vec(), HASH_K1_MASK.to_vec(), HASH_K2_MASK.to_vec()] + vec![ + HASH_K0_MASK.to_vec(), + HASH_K1_MASK.to_vec(), + HASH_K2_MASK.to_vec(), + BITWISE_K0_MASK.to_vec(), + BITWISE_K1_MASK.to_vec(), + ] } fn get_num_rand_values(&self) -> usize { @@ -175,6 +194,9 @@ impl LogUpGkrEvaluator for MidenLogUpGkrEval { let query_current = &query[0..TRACE_WIDTH]; let query_next = &query[TRACE_WIDTH..]; + let hasher_periodic_values = &periodic_values[0..3]; + let bitwise_periodic_values = &periodic_values[3..5]; + let op_flags = LogUpOpFlags::new(query_current, query_next); let offset_rand_values = &rand_values[0..NUM_OFFSET_RAND_VALUES]; @@ -239,7 +261,7 @@ impl LogUpGkrEvaluator for MidenLogUpGkrEval { hasher_table( query_current, query_next, - periodic_values, + hasher_periodic_values, &alphas, &mut numerator[range(HASHER_TABLE_FRACTIONS_OFFSET, HASHER_TABLE_NUM_FRACTIONS)], &mut denominator[range(HASHER_TABLE_FRACTIONS_OFFSET, HASHER_TABLE_NUM_FRACTIONS)], @@ -257,6 +279,18 @@ impl LogUpGkrEvaluator for MidenLogUpGkrEval { [range(KERNEL_PROC_TABLE_FRACTIONS_OFFSET, KERNEL_PROC_TABLE_NUM_FRACTIONS)], ); } + { + alphas[0] = offset_rand_values[6]; + chiplets_bus::bus( + query_current, + query_next, + bitwise_periodic_values, + &op_flags, + &alphas, + &mut numerator[range(CHIPLETS_BUS_FRACTIONS_OFFSET, CHIPLETS_BUS_NUM_FRACTIONS)], + &mut denominator[range(CHIPLETS_BUS_FRACTIONS_OFFSET, CHIPLETS_BUS_NUM_FRACTIONS)], + ); + } padding( &mut numerator[range(PADDING_FRACTIONS_OFFSET, PADDING_NUM_FRACTIONS)], &mut denominator[range(PADDING_FRACTIONS_OFFSET, PADDING_NUM_FRACTIONS)], @@ -536,9 +570,8 @@ fn block_stack_table( + alphas[6].mul_base(parent_stack_depth) + alphas[7].mul_base(parent_next_overflow_addr) + inner_product(&alphas[8..12], parent_fn_hash); - let v_respan = alphas[0] - + alphas[1].mul_base(block_id) - + alphas[2].mul_base(parent_id_respan); + let v_respan = + alphas[0] + alphas[1].mul_base(block_id) + alphas[2].mul_base(parent_id_respan); let v_end = alphas[0] + alphas[1].mul_base(block_id) + alphas[2].mul_base(parent_id_end) @@ -674,8 +707,19 @@ where denominator.fill(E::ONE); } +// OP FLAGS +// =============================================================================================== + // TODO(plafer): save intermediary values between flags instead of recomputing struct LogUpOpFlags { + // degree 7 flags + f_u32_and: F, + f_u32_xor: F, + f_mload: F, + f_mstore: F, + f_mloadw: F, + f_mstorew: F, + // degree 5 flags f_push: F, f_emit: F, f_dyn: F, @@ -684,6 +728,10 @@ struct LogUpOpFlags { f_span: F, f_join: F, f_imm: F, + f_pipe: F, + f_mstream: F, + f_rcombbase: F, + // degree 4 flags f_repeat: F, f_end: F, f_syscall: F, @@ -710,15 +758,26 @@ impl LogUpOpFlags { let e0 = query_current[DECODER_OP_BITS_EXTRA_COLS_OFFSET]; let e1 = query_current[DECODER_OP_BITS_EXTRA_COLS_OFFSET + 1]; + // degree 7 flags + let f_u32_and = + (F::ONE - b6) * b5 * (F::ONE - b4) * (F::ONE - b3) * b2 * b1 * (F::ONE - b0); + let f_u32_xor = (F::ONE - b6) * b5 * (F::ONE - b4) * (F::ONE - b3) * b2 * b1 * b0; + let f_mload = (F::ONE - b6) * (F::ONE - b5) * (F::ONE - b4) * (F::ONE - b3) * b2 * b1 * b0; + let f_mstore = (F::ONE - b6) * b5 * (F::ONE - b4) * b3 * b2 * (F::ONE - b1) * b0; + let f_mloadw = (F::ONE - b6) * b5 * (F::ONE - b4) * b3 * b2 * (F::ONE - b1) * (F::ONE - b0); + let f_mstorew = (F::ONE - b6) * b5 * (F::ONE - b4) * b3 * b2 * b1 * (F::ONE - b0); + // degree 5 flags let e0_b3_nb2 = e0 * b3 * (F::ONE - b2); let e0_b3_nb2_b1 = e0_b3_nb2 * b1; let f_push = e0_b3_nb2_b1 * b0; let f_emit = e0_b3_nb2_b1 * (F::ONE - b0); - let e0_nb3_b2 = e0 * (F::ONE - b3) * b2; + let e0_nb3 = e0 * (F::ONE - b3); + let e0_nb3_b2 = e0_nb3 * b2; let e0_nb3_b2_b1 = e0_nb3_b2 * b1; let e0_nb3_b2_nb1 = e0_nb3_b2 * (F::ONE - b1); + let e0_nb3_nb2_b1 = e0 * (F::ONE - b3) * (F::ONE - b2) * b1; // degree 4 flags let e1_b4 = e1 * b4; @@ -741,6 +800,13 @@ impl LogUpOpFlags { let e1_b4_nb3_next = e1_b4_next * (F::ONE - b3_next); Self { + // degree 7 flags + f_u32_and, + f_u32_xor, + f_mload, + f_mstore, + f_mloadw, + f_mstorew, // degree 5 flags f_push, f_emit, @@ -750,6 +816,9 @@ impl LogUpOpFlags { f_loop: e0_nb3_b2_nb1 * b0, f_span: e0_nb3_b2_b1 * (F::ONE - b0), f_join: e0_nb3_b2_b1 * b0, + f_rcombbase: e0_b3_nb2 * (F::ONE - b1) * b0, + f_pipe: e0_nb3_nb2_b1 * (F::ONE - b0), + f_mstream: e0_nb3_nb2_b1 * b0, // degree 4 flags f_repeat: e1_b4_nb3 * b2, @@ -774,6 +843,31 @@ impl LogUpOpFlags { f_halt_next: e1_b4_next * b3_next * b2_next, } } + // flag degree 7 + + pub fn f_u32_and(&self) -> F { + self.f_u32_and + } + + pub fn f_u32_xor(&self) -> F { + self.f_u32_xor + } + + pub fn f_mload(&self) -> F { + self.f_mload + } + + pub fn f_mstore(&self) -> F { + self.f_mstore + } + + pub fn f_mloadw(&self) -> F { + self.f_mloadw + } + + pub fn f_mstorew(&self) -> F { + self.f_mstorew + } // flag degree 5 @@ -809,6 +903,18 @@ impl LogUpOpFlags { self.f_imm } + pub fn f_pipe(&self) -> F { + self.f_pipe + } + + pub fn f_mstream(&self) -> F { + self.f_mstream + } + + pub fn f_rcombbase(&self) -> F { + self.f_rcombbase + } + // degree 4 flags pub fn f_repeat(&self) -> F { diff --git a/air/src/trace/chiplets/kernel_rom.rs b/air/src/trace/chiplets/kernel_rom.rs index 94c9cc926..f39791d84 100644 --- a/air/src/trace/chiplets/kernel_rom.rs +++ b/air/src/trace/chiplets/kernel_rom.rs @@ -8,8 +8,9 @@ pub const TRACE_WIDTH: usize = 6; // --- OPERATION SELECTORS ------------------------------------------------------------------------ +pub const KERNEL_PROC_LABEL_RAW: u32 = 0b1000; /// Specifies a kernel procedure call operation to access a procedure in the kernel ROM. /// /// The unique operation label is computed as 1 plus the combined chiplet and internal selector /// with the bits reversed: kernel ROM selector=[1, 1, 1, 0] +1=[0, 0, 0, 1]. -pub const KERNEL_PROC_LABEL: Felt = Felt::new(0b1000); +pub const KERNEL_PROC_LABEL: Felt = Felt::new(KERNEL_PROC_LABEL_RAW as u64);