Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: increase cycle limit #2037

Closed
wants to merge 16 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions crates/core/executor/src/artifacts/rv32im_costs.json
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
"KeccakPermute": 93720,
"Program": 31,
"MemoryLocal": 100,
"Global": 428,
"Global": 434,
"Secp256k1AddAssign": 4461,
"AddSub": 47,
"Jump": 50,
Expand All @@ -40,7 +40,7 @@
"SyscallCore": 22,
"Bn254Fp2AddSubAssign": 1454,
"Bls12381FpOpAssign": 1098,
"Cpu": 109,
"Cpu": 110,
"ShaCompress": 40480,
"MemoryInstrs": 93,
"Secp256k1DoubleAssign": 4564
Expand Down
2 changes: 1 addition & 1 deletion crates/core/executor/src/program.rs
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ impl<F: PrimeField32> MachineProgram<F> for Program {
.par_bridge()
.map(|(&addr, &word)| {
let values = [
(InteractionKind::Memory as u32) << 16,
(InteractionKind::Memory as u32) << 24,
0,
addr,
word & 255,
Expand Down
36 changes: 25 additions & 11 deletions crates/core/machine/src/cpu/air/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use core::borrow::Borrow;
use p3_air::{Air, AirBuilder, AirBuilderWithPublicValues, BaseAir};
use p3_field::AbstractField;
use p3_matrix::Matrix;
use sp1_core_executor::{ByteOpcode, DEFAULT_PC_INC};
use sp1_core_executor::DEFAULT_PC_INC;
use sp1_stark::{
air::{BaseAirBuilder, PublicValues, SP1AirBuilder, SP1_PROOF_NUM_PV_ELTS},
Word,
Expand Down Expand Up @@ -40,21 +40,26 @@ where
let clk =
AB::Expr::from_canonical_u32(1u32 << 16) * local.clk_8bit_limb + local.clk_16bit_limb;

// We represent the `shard` with a 16 bit limb and a 8 bit limb.
// The range checks for these limbs are done in `eval_shard_clk`.
let shard = AB::Expr::from_canonical_u32(1u32 << 16) * local.shard_8bit_limb
+ local.shard_16bit_limb;

// Program constraints.
// SAFETY: `local.is_real` is checked to be boolean in `eval_is_real`.
// The `pc` and `instruction` is taken from the `ProgramChip`, where these are preprocessed.
builder.send_program(local.pc, local.instruction, local.is_real);

// Register constraints.
self.eval_registers::<AB>(builder, local, clk.clone());
self.eval_registers::<AB>(builder, local, shard.clone(), clk.clone());

// Assert the shard and clk to send. Only the memory and syscall instructions need the
// actual shard and clk values for memory access evals.
// SAFETY: The usage of `builder.if_else` requires `is_memory + is_syscall` to be boolean.
// The correctness of `is_memory` and `is_syscall` will be checked in the opcode specific chips.
// In these correct cases, `is_memory + is_syscall` will be always boolean.
let expected_shard_to_send =
builder.if_else(local.is_memory + local.is_syscall, local.shard, AB::Expr::zero());
builder.if_else(local.is_memory + local.is_syscall, shard.clone(), AB::Expr::zero());
let expected_clk_to_send =
builder.if_else(local.is_memory + local.is_syscall, clk.clone(), AB::Expr::zero());
builder.when(local.is_real).assert_eq(local.shard_to_send, expected_shard_to_send);
Expand Down Expand Up @@ -90,7 +95,7 @@ where
);

// Check that the shard and clk is updated correctly.
self.eval_shard_clk(builder, local, next, public_values, clk.clone());
self.eval_shard_clk(builder, local, next, public_values, shard.clone(), clk.clone());

// Check that the pc is updated correctly.
self.eval_pc(builder, local, next, public_values);
Expand Down Expand Up @@ -120,21 +125,30 @@ impl CpuChip {
local: &CpuCols<AB::Var>,
next: &CpuCols<AB::Var>,
public_values: &PublicValues<Word<AB::PublicVar>, AB::PublicVar>,
shard: AB::Expr,
clk: AB::Expr,
) {
// Verify the public value's shard.
builder.when(local.is_real).assert_eq(public_values.execution_shard, local.shard);
builder.when(local.is_real).assert_eq(public_values.execution_shard, shard.clone());

// Verify that all shard values are the same.
builder.when_transition().when(next.is_real).assert_eq(local.shard, next.shard);
let next_shard =
AB::Expr::from_canonical_u32(1u32 << 16) * next.shard_8bit_limb + next.shard_16bit_limb;
builder.when_transition().when(next.is_real).assert_eq(shard.clone(), next_shard);

// Verify that the shard value is within 16 bits.
// SAFETY: `local.is_real` is checked to be boolean in `eval_is_real`.
builder.send_byte(
AB::Expr::from_canonical_u8(ByteOpcode::U16Range as u8),
local.shard,
AB::Expr::zero(),
AB::Expr::zero(),
// builder.send_byte(
// AB::Expr::from_canonical_u8(ByteOpcode::U16Range as u8),
// local.shard,
// AB::Expr::zero(),
// AB::Expr::zero(),
// local.is_real,
// );
builder.eval_range_check_24bits(
shard,
local.shard_16bit_limb,
local.shard_8bit_limb,
local.is_real,
);

Expand Down
7 changes: 4 additions & 3 deletions crates/core/machine/src/cpu/air/register.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ impl CpuChip {
&self,
builder: &mut AB,
local: &CpuCols<AB::Var>,
shard: AB::Expr,
clk: AB::Expr,
) {
// Load immediates into b and c, if the immediate flags are on.
Expand All @@ -26,15 +27,15 @@ impl CpuChip {

// If they are not immediates, read `b` and `c` from memory.
builder.eval_memory_access(
local.shard,
shard.clone(),
clk.clone() + AB::F::from_canonical_u32(MemoryAccessPosition::B as u32),
local.instruction.op_b[0],
&local.op_b_access,
AB::Expr::one() - local.instruction.imm_b,
);

builder.eval_memory_access(
local.shard,
shard.clone(),
clk.clone() + AB::F::from_canonical_u32(MemoryAccessPosition::C as u32),
local.instruction.op_c[0],
&local.op_c_access,
Expand All @@ -52,7 +53,7 @@ impl CpuChip {
// receviers of the interaction to witness the value. It will be wasteful to put that column
// in all other instruction chips.
builder.eval_memory_access(
local.shard,
shard.clone(),
clk + AB::F::from_canonical_u32(MemoryAccessPosition::A as u32),
local.instruction.op_a,
&local.op_a_access,
Expand Down
6 changes: 4 additions & 2 deletions crates/core/machine/src/cpu/columns/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,10 @@ pub const CPU_COL_MAP: CpuCols<usize> = make_col_map();
#[derive(AlignedBorrow, Default, Debug, Clone, Copy)]
#[repr(C)]
pub struct CpuCols<T: Copy> {
/// The current shard.
pub shard: T,
/// The least significant 16 bit limb of the current shard.
pub shard_16bit_limb: T,
/// The most significant 16 bit limb of the current shard.
pub shard_8bit_limb: T,

/// The least significant 16 bit limb of clk.
pub clk_16bit_limb: T,
Expand Down
16 changes: 13 additions & 3 deletions crates/core/machine/src/cpu/trace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -143,7 +143,7 @@ impl CpuChip {
|| instruction.is_memory_store_instruction()
|| instruction.is_ecall_instruction()
{
cols.shard
F::from_canonical_u32(shard)
} else {
F::zero()
};
Expand Down Expand Up @@ -218,14 +218,24 @@ impl CpuChip {
blu_events: &mut impl ByteRecord,
shard: u32,
) {
cols.shard = F::from_canonical_u32(shard);
let shard_16bit_limb = (shard & 0xffff) as u16;
let shard_8bit_limb = ((shard >> 16) & 0xff) as u8;
cols.shard_16bit_limb = F::from_canonical_u16(shard_16bit_limb);
cols.shard_8bit_limb = F::from_canonical_u8(shard_8bit_limb);

let clk_16bit_limb = (event.clk & 0xffff) as u16;
let clk_8bit_limb = ((event.clk >> 16) & 0xff) as u8;
cols.clk_16bit_limb = F::from_canonical_u16(clk_16bit_limb);
cols.clk_8bit_limb = F::from_canonical_u8(clk_8bit_limb);

blu_events.add_byte_lookup_event(ByteLookupEvent::new(U16Range, shard as u16, 0, 0, 0));
blu_events.add_byte_lookup_event(ByteLookupEvent::new(U16Range, shard_16bit_limb, 0, 0, 0));
blu_events.add_byte_lookup_event(ByteLookupEvent::new(
ByteOpcode::U8Range,
0,
0,
0,
shard_8bit_limb as u8,
));
blu_events.add_byte_lookup_event(ByteLookupEvent::new(U16Range, clk_16bit_limb, 0, 0, 0));
blu_events.add_byte_lookup_event(ByteLookupEvent::new(
ByteOpcode::U8Range,
Expand Down
14 changes: 12 additions & 2 deletions crates/core/machine/src/global/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ const GLOBAL_COL_MAP: GlobalCols<usize> = make_col_map();

pub const GLOBAL_INITIAL_DIGEST_POS: usize = GLOBAL_COL_MAP.accumulation.initial_digest[0].0[0];

pub const GLOBAL_INITIAL_DIGEST_POS_COPY: usize = 377;
pub const GLOBAL_INITIAL_DIGEST_POS_COPY: usize = 379;

#[repr(C)]
pub struct Ghost {
Expand All @@ -54,6 +54,8 @@ pub struct GlobalChip;
pub struct GlobalCols<T: Copy> {
pub message: [T; 7],
pub kind: T,
pub shard_16bit_limb: T,
pub shard_8bit_limb: T,
pub interaction: GlobalInteractionOperation<T>,
pub is_receive: T,
pub is_send: T,
Expand Down Expand Up @@ -82,7 +84,10 @@ impl<F: PrimeField32> MachineAir<F> for GlobalChip {
.map(|events| {
let mut blu: Vec<ByteLookupEvent> = Vec::new();
events.iter().for_each(|event| {
blu.add_u16_range_check(event.message[0].try_into().unwrap());
let message0_16bit_limb = (event.message[0] & 0xffff) as u16;
let message0_8bit_limb = ((event.message[0] >> 16) & 0xff) as u8;
blu.add_u16_range_check(message0_16bit_limb);
blu.add_u8_range_check(0, message0_8bit_limb);
});
blu
})
Expand Down Expand Up @@ -137,6 +142,10 @@ impl<F: PrimeField32> MachineAir<F> for GlobalChip {
} else {
cols.is_send = F::one();
}
cols.shard_16bit_limb =
F::from_canonical_u16((event.message[0] & 0xffff) as u16);
cols.shard_8bit_limb =
F::from_canonical_u8(((event.message[0] >> 16) & 0xff) as u8);
point_chunks.push(SepticCurveComplete::Affine(SepticCurve {
x: SepticExtension(cols.interaction.x_coordinate.0),
y: SepticExtension(cols.interaction.y_coordinate.0),
Expand Down Expand Up @@ -246,6 +255,7 @@ where
local.is_send.into(),
local.is_real,
local.kind,
[local.shard_16bit_limb.into(), local.shard_8bit_limb.into()],
);

// Evaluate the accumulation.
Expand Down
17 changes: 9 additions & 8 deletions crates/core/machine/src/operations/global_interaction.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,13 @@
air::{eval_external_round, eval_internal_rounds},
NUM_EXTERNAL_ROUNDS,
};
use crate::air::MemoryAirBuilder;
use p3_air::AirBuilder;
use p3_field::AbstractExtensionField;
use p3_field::AbstractField;
use p3_field::Field;
use p3_field::PrimeField32;
use sp1_core_executor::ByteOpcode;

use sp1_derive::AlignedBorrow;
use sp1_stark::{
air::SP1AirBuilder,
Expand All @@ -37,7 +38,7 @@
kind: u8,
) -> (SepticCurve<F>, u8, [F; 16], [F; 16]) {
let x_start = SepticExtension::<F>::from_base_fn(|i| F::from_canonical_u32(values.0[i]))
+ SepticExtension::from_base(F::from_canonical_u32((kind as u32) << 16));
+ SepticExtension::from_base(F::from_canonical_u32((kind as u32) << 24));
let (point, offset, m_trial, m_hash) = SepticCurve::<F>::lift_x(x_start);
if !is_receive {
return (point.neg(), offset, m_trial, m_hash);
Expand Down Expand Up @@ -102,7 +103,7 @@

impl<F: Field> GlobalInteractionOperation<F> {
/// Constrain that the elliptic curve point for the global interaction is correctly derived.
pub fn eval_single_digest<AB: SP1AirBuilder + p3_air::PairBuilder>(

Check failure on line 106 in crates/core/machine/src/operations/global_interaction.rs

View workflow job for this annotation

GitHub Actions / Formatting & Clippy

this function has too many arguments (8/7)
builder: &mut AB,
values: [AB::Expr; 7],
cols: GlobalInteractionOperation<AB::Var>,
Expand All @@ -110,6 +111,7 @@
is_send: AB::Expr,
is_real: AB::Var,
kind: AB::Var,
shard_limbs: [AB::Expr; 2],
) {
// Constrain that the `is_real` is boolean.
builder.assert_bool(is_real);
Expand All @@ -121,19 +123,18 @@
offset = offset.clone() + cols.offset_bits[i] * AB::F::from_canonical_u32(1 << i);
}

// Range check the first element in the message to be a u16 so that we can encode the interaction kind in the upper 8 bits.
builder.send_byte(
AB::Expr::from_canonical_u8(ByteOpcode::U16Range as u8),
// Range check the first element in the message to be a u24 so that we can encode the interaction kind in the upper 8 bits.
builder.eval_range_check_24bits(
values[0].clone(),
AB::Expr::zero(),
AB::Expr::zero(),
shard_limbs[0].clone(),
shard_limbs[1].clone(),
is_real,
);

// Turn the message into a hash input. Only the first 8 elements are non-zero, as the rate of the Poseidon2 hash is 8.
// Combining `values[0]` with `kind` is safe, as `values[0]` is range checked to be u16, and `kind` is known to be u8.
let m_trial = [
values[0].clone() + AB::Expr::from_canonical_u32(1 << 16) * kind,
values[0].clone() + AB::Expr::from_canonical_u32(1 << 24) * kind,
values[1].clone(),
values[2].clone(),
values[3].clone(),
Expand Down
2 changes: 1 addition & 1 deletion crates/core/machine/src/riscv/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ pub(crate) mod riscv_chips {
}

/// The maximum log number of shards in core.
pub const MAX_LOG_NUMBER_OF_SHARDS: usize = 16;
pub const MAX_LOG_NUMBER_OF_SHARDS: usize = 24;

/// The maximum number of shards in core.
pub const MAX_NUMBER_OF_SHARDS: usize = 1 << MAX_LOG_NUMBER_OF_SHARDS;
Expand Down
2 changes: 1 addition & 1 deletion crates/prover/src/verify.rs
Original file line number Diff line number Diff line change
Expand Up @@ -278,7 +278,7 @@ impl<C: SP1ProverComponents> SP1Prover<C> {
}

// Verify that the number of shards is not too large.
if proof.0.len() > 1 << 16 {
if proof.0.len() > 1 << 24 {
return Err(MachineVerificationError::TooManyShards);
}

Expand Down
Loading
Loading