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

bugfix: fix the cell type to support larger memory accessing range #247

Merged
merged 4 commits into from
Apr 14, 2024
Merged
Show file tree
Hide file tree
Changes from 2 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
1 change: 1 addition & 0 deletions Cargo.lock

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

12 changes: 3 additions & 9 deletions crates/cli/src/config.rs
Original file line number Diff line number Diff line change
Expand Up @@ -260,14 +260,6 @@ impl Config {
result
};

if cfg!(not(feature = "continuation")) {
if result.tables.execution_tables.etable.len() != 1 {
return Err(anyhow::anyhow!(
"Only support single slice for non-continuation mode.\nYou could increase K or enable continuation feature."
));
}
}

{
if let Some(context_output_filename) = context_output_filename {
let context_output_path = output_dir.join(context_output_filename);
Expand Down Expand Up @@ -318,8 +310,10 @@ impl Config {

let progress_bar = ProgressBar::new(result.tables.execution_tables.etable.len() as u64);

let mut slices = loader.slice(result).into_iter().enumerate().peekable();
let mut slices = loader.slice(result)?.into_iter().enumerate().peekable();
while let Some((index, circuit)) = slices.next() {
let circuit = circuit?;

let _is_finalized_circuit = slices.peek().is_none();

if mock_test {
Expand Down
1 change: 1 addition & 0 deletions crates/zkwasm/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ strum = "0.24.1"
strum_macros = "0.24.1"
serde = { version = "1.0", features = ["derive"] }
serde_json = "1.0"
thiserror = "1.0.58"
ff = "0.12"
sha2 = "0.10.6"
anyhow.workspace = true
Expand Down
8 changes: 4 additions & 4 deletions crates/zkwasm/src/circuits/etable/allocator.rs
Original file line number Diff line number Diff line change
Expand Up @@ -185,17 +185,17 @@ pub(crate) enum EventTableCellType {
const BIT_COLUMNS: usize = 12;
const U8_COLUMNS: usize = 1;
const U32_CELLS: usize = if cfg!(feature = "continuation") {
10
12
} else {
0
2
};
const U64_CELLS: usize = 5;
const U16_COLUMNS: usize = U64_CELLS + (U32_CELLS / 2);
const COMMON_RANGE_COLUMNS: usize = if cfg!(feature = "continuation") { 5 } else { 7 };
const COMMON_RANGE_COLUMNS: usize = if cfg!(feature = "continuation") { 4 } else { 6 };
const UNLIMITED_COLUMNS: usize = if cfg!(feature = "continuation") {
10
} else {
7
8
};
const MEMORY_TABLE_LOOKUP_COLUMNS: usize = 2;
const JUMP_TABLE_LOOKUP_COLUMNS: usize = 1;
Expand Down
26 changes: 13 additions & 13 deletions crates/zkwasm/src/circuits/etable/op_configure/op_load.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,10 +33,10 @@ use specs::step::StepInfo;

pub struct LoadConfig<F: FieldExt> {
// offset in opcode
opcode_load_offset: AllocatedCommonRangeCell<F>,
opcode_load_offset: AllocatedU32Cell<F>,

// which heap offset to load
load_block_index: AllocatedCommonRangeCell<F>,
load_block_index: AllocatedU32Cell<F>,
load_inner_pos: AllocatedU8Cell<F>,
/// helper to prove load_inner_pos < WASM_BLOCK_BYTE_SIZE
load_inner_pos_diff: AllocatedU8Cell<F>,
Expand Down Expand Up @@ -65,7 +65,7 @@ pub struct LoadConfig<F: FieldExt> {
is_two_bytes: AllocatedBitCell<F>,
is_four_bytes: AllocatedBitCell<F>,
is_eight_bytes: AllocatedBitCell<F>,
len: AllocatedUnlimitedCell<F>,
bytes: AllocatedUnlimitedCell<F>,
len_modulus: AllocatedUnlimitedCell<F>,

is_sign: AllocatedBitCell<F>,
Expand All @@ -92,10 +92,10 @@ impl<F: FieldExt> EventTableOpcodeConfigBuilder<F> for LoadConfigBuilder {
allocator: &mut EventTableCellAllocator<F>,
constraint_builder: &mut ConstraintBuilder<F>,
) -> Box<dyn EventTableOpcodeConfig<F>> {
let opcode_load_offset = allocator.alloc_common_range_cell();
let opcode_load_offset = allocator.alloc_u32_cell();

// which heap offset to load
let load_block_index = allocator.alloc_common_range_cell();
let load_block_index = allocator.alloc_u32_cell();
let load_inner_pos = allocator.alloc_u8_cell();
let load_inner_pos_diff = allocator.alloc_u8_cell();
let is_cross_block = allocator.alloc_bit_cell();
Expand All @@ -106,7 +106,7 @@ impl<F: FieldExt> EventTableOpcodeConfigBuilder<F> for LoadConfigBuilder {
let is_two_bytes = allocator.alloc_bit_cell();
let is_four_bytes = allocator.alloc_bit_cell();
let is_eight_bytes = allocator.alloc_bit_cell();
let len = allocator.alloc_unlimited_cell();
let bytes = allocator.alloc_unlimited_cell();
let len_modulus = allocator.alloc_unlimited_cell();

let load_tailing = allocator.alloc_u64_cell();
Expand Down Expand Up @@ -197,10 +197,10 @@ impl<F: FieldExt> EventTableOpcodeConfigBuilder<F> for LoadConfigBuilder {
);

constraint_builder.push(
"op_load len",
"op_load bytes",
Box::new(move |meta| {
vec![
len.expr(meta)
bytes.expr(meta)
- constant_from!(1)
- is_two_bytes.expr(meta)
- constant_from!(3) * is_four_bytes.expr(meta)
Expand Down Expand Up @@ -229,7 +229,7 @@ impl<F: FieldExt> EventTableOpcodeConfigBuilder<F> for LoadConfigBuilder {
is_cross_block.expr(meta) * constant_from!(WASM_BLOCK_BYTE_SIZE)
+ cross_block_rem.expr(meta)
- load_inner_pos.expr(meta)
- len.expr(meta)
- bytes.expr(meta)
+ constant_from!(1),
cross_block_rem.expr(meta) + cross_block_rem_diff.expr(meta)
- constant_from!(WASM_BLOCK_BYTE_SIZE - 1),
Expand Down Expand Up @@ -389,7 +389,7 @@ impl<F: FieldExt> EventTableOpcodeConfigBuilder<F> for LoadConfigBuilder {
is_two_bytes,
is_four_bytes,
is_eight_bytes,
len,
bytes,
len_modulus,
is_sign,
is_i32,
Expand Down Expand Up @@ -442,12 +442,12 @@ impl<F: FieldExt> EventTableOpcodeConfig<F> for LoadConfig<F> {
} => {
let len = load_size.byte_size();

self.opcode_load_offset.assign_u32(ctx, offset)?;
self.opcode_load_offset.assign(ctx, offset)?;

let inner_byte_index = byte_offset_from_address(effective_address);
let block_start_index = block_from_address(effective_address);

self.load_block_index.assign_u32(ctx, block_start_index)?;
self.load_block_index.assign(ctx, block_start_index)?;
self.load_inner_pos.assign_u32(ctx, inner_byte_index)?;
self.load_inner_pos_diff
.assign_u32(ctx, WASM_BLOCK_BYTE_SIZE - 1 - inner_byte_index)?;
Expand Down Expand Up @@ -519,7 +519,7 @@ impl<F: FieldExt> EventTableOpcodeConfig<F> for LoadConfig<F> {
self.is_two_bytes.assign_bool(ctx, len == 2)?;
self.is_four_bytes.assign_bool(ctx, len == 4)?;
self.is_eight_bytes.assign_bool(ctx, len == 8)?;
self.len.assign(ctx, (len as u64).into())?;
self.bytes.assign(ctx, (len as u64).into())?;
self.len_modulus
.assign_bn(ctx, &(BigUint::from(1u64) << (len * 8)))?;

Expand Down
26 changes: 13 additions & 13 deletions crates/zkwasm/src/circuits/etable/op_configure/op_store.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,10 +33,10 @@ use specs::step::StepInfo;

pub struct StoreConfig<F: FieldExt> {
// offset in opcode
opcode_store_offset: AllocatedCommonRangeCell<F>,
opcode_store_offset: AllocatedU32Cell<F>,

// which heap offset to load
load_block_index: AllocatedCommonRangeCell<F>,
load_block_index: AllocatedU32Cell<F>,
load_block_inner_pos_bits: [AllocatedBitCell<F>; 3],
/// helper to prove load_inner_pos < WASM_BLOCK_BYTE_SIZE
load_block_inner_pos: AllocatedUnlimitedCell<F>,
Expand All @@ -53,7 +53,7 @@ pub struct StoreConfig<F: FieldExt> {
load_picked_byte_proof: AllocatedU8Cell<F>,

unchanged_value: AllocatedUnlimitedCell<F>,
len: AllocatedUnlimitedCell<F>,
bytes: AllocatedUnlimitedCell<F>,
len_modulus: AllocatedUnlimitedCell<F>,

store_value: AllocatedU64Cell<F>,
Expand Down Expand Up @@ -88,17 +88,17 @@ impl<F: FieldExt> EventTableOpcodeConfigBuilder<F> for StoreConfigBuilder {
allocator: &mut EventTableCellAllocator<F>,
constraint_builder: &mut ConstraintBuilder<F>,
) -> Box<dyn EventTableOpcodeConfig<F>> {
let opcode_store_offset = allocator.alloc_common_range_cell();
let opcode_store_offset = allocator.alloc_u32_cell();

// which heap offset to load
let load_block_index = allocator.alloc_common_range_cell();
let load_block_index = allocator.alloc_u32_cell();
let load_block_inner_pos_bits = [0; 3].map(|_| allocator.alloc_bit_cell());
let load_block_inner_pos = allocator.alloc_unlimited_cell();
let is_cross_block = allocator.alloc_bit_cell();
let cross_block_rem = allocator.alloc_common_range_cell();
let cross_block_rem_diff = allocator.alloc_common_range_cell();

let len = allocator.alloc_unlimited_cell();
let bytes = allocator.alloc_unlimited_cell();
let len_modulus = allocator.alloc_unlimited_cell();

let load_tailing = allocator.alloc_u64_cell();
Expand Down Expand Up @@ -210,10 +210,10 @@ impl<F: FieldExt> EventTableOpcodeConfigBuilder<F> for StoreConfigBuilder {
);

constraint_builder.push(
"op_store len",
"op_store bytes",
Box::new(move |meta| {
vec![
len.expr(meta)
bytes.expr(meta)
- constant_from!(1)
- is_two_bytes.expr(meta)
- constant_from!(3) * is_four_bytes.expr(meta)
Expand Down Expand Up @@ -245,7 +245,7 @@ impl<F: FieldExt> EventTableOpcodeConfigBuilder<F> for StoreConfigBuilder {
is_cross_block.expr(meta) * constant_from!(WASM_BLOCK_BYTE_SIZE)
+ cross_block_rem.expr(meta)
- load_block_inner_pos.expr(meta)
- len.expr(meta)
- bytes.expr(meta)
+ constant_from!(1),
cross_block_rem.expr(meta) + cross_block_rem_diff.expr(meta)
- constant_from!(WASM_BLOCK_BYTE_SIZE - 1),
Expand Down Expand Up @@ -426,7 +426,7 @@ impl<F: FieldExt> EventTableOpcodeConfigBuilder<F> for StoreConfigBuilder {
lookup_pow_modulus,
address_within_allocated_pages_helper,
load_tailing_diff,
len,
bytes,
len_modulus,
})
}
Expand Down Expand Up @@ -468,12 +468,12 @@ impl<F: FieldExt> EventTableOpcodeConfig<F> for StoreConfig<F> {
} => {
let len = store_size.byte_size() as u32;

self.opcode_store_offset.assign_u32(ctx, offset)?;
self.opcode_store_offset.assign(ctx, offset)?;

let inner_byte_index = byte_offset_from_address(effective_address);
let block_start_index = block_from_address(effective_address);

self.load_block_index.assign_u32(ctx, block_start_index)?;
self.load_block_index.assign(ctx, block_start_index)?;
self.load_block_inner_pos
.assign_u32(ctx, inner_byte_index)?;
self.load_block_inner_pos_bits[0].assign_bool(ctx, inner_byte_index & 1 != 0)?;
Expand Down Expand Up @@ -545,7 +545,7 @@ impl<F: FieldExt> EventTableOpcodeConfig<F> for StoreConfig<F> {
self.is_two_bytes.assign_bool(ctx, len == 2)?;
self.is_four_bytes.assign_bool(ctx, len == 4)?;
self.is_eight_bytes.assign_bool(ctx, len == 8)?;
self.len.assign(ctx, (len as u64).into())?;
self.bytes.assign(ctx, (len as u64).into())?;
self.is_i32.assign_bool(ctx, vtype == VarType::I32)?;

self.address_within_allocated_pages_helper.assign_u32(
Expand Down
2 changes: 1 addition & 1 deletion crates/zkwasm/src/circuits/image_table/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,10 +7,10 @@ use halo2_proofs::plonk::Fixed;
use halo2_proofs::plonk::VirtualCells;
use std::marker::PhantomData;

use super::zkwasm_circuit::RESERVE_ROWS;
use super::utils::image_table::GLOBAL_CAPABILITY;
use super::utils::image_table::INIT_MEMORY_ENTRIES_OFFSET;
use super::utils::image_table::STACK_CAPABILITY;
use super::zkwasm_circuit::RESERVE_ROWS;

mod assign;
mod configure;
Expand Down
51 changes: 46 additions & 5 deletions crates/zkwasm/src/circuits/mod.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
use crate::circuits::utils::Context;
use crate::error::BuildingCircuitError;

use halo2_proofs::arithmetic::FieldExt;
use halo2_proofs::plonk::ConstraintSystem;
Expand All @@ -8,6 +9,10 @@ use num_bigint::BigUint;
use specs::slice::Slice;
use std::marker::PhantomData;

use self::etable::EVENT_TABLE_ENTRY_ROWS;
use self::image_table::compute_maximal_pages;
use self::zkwasm_circuit::RESERVE_ROWS;

pub(crate) mod cell;
pub(crate) mod etable;

Expand All @@ -34,19 +39,55 @@ pub mod zkwasm_circuit;
pub type CompilationTable = specs::CompilationTable;
pub type ExecutionTable = specs::ExecutionTable;

pub(crate) fn compute_slice_capability(k: u32) -> u32 {
((1 << k) - RESERVE_ROWS as u32 - 1024) / EVENT_TABLE_ENTRY_ROWS as u32
}

pub struct ZkWasmCircuit<F: FieldExt> {
pub k: u32,
pub slice: Slice,
pub slice_capability: usize,
_data: PhantomData<F>,
}

impl<F: FieldExt> ZkWasmCircuit<F> {
pub fn new(slice: Slice, slice_capability: usize) -> Self {
ZkWasmCircuit {
pub fn new(k: u32, slice: Slice) -> Result<Self, BuildingCircuitError> {
{
// entries is empty when called by without_witness
let allocated_memory_pages = slice
.etable
.entries()
.last()
.map(|entry| entry.allocated_memory_pages);
let maximal_pages = compute_maximal_pages(k);
if let Some(allocated_memory_pages) = allocated_memory_pages {
if allocated_memory_pages > maximal_pages {
return Err(BuildingCircuitError::PagesExceedLimit(
allocated_memory_pages,
maximal_pages,
k,
));
}
}
}

{
let etable_entires = slice.etable.entries().len() as u32;
let etable_capacity = compute_slice_capability(k);

if etable_entires > etable_capacity {
return Err(BuildingCircuitError::EtableEntriesExceedLimit(
etable_entires as u32,
etable_capacity as u32,
k,
));
}
}

Ok(ZkWasmCircuit {
k,
slice,
slice_capability,
_data: PhantomData,
}
})
}
}

Expand Down
8 changes: 5 additions & 3 deletions crates/zkwasm/src/circuits/zkwasm_circuit/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ use specs::slice::Slice;
use crate::circuits::bit_table::BitTableChip;
use crate::circuits::bit_table::BitTableConfig;
use crate::circuits::bit_table::BitTableTrait;
use crate::circuits::compute_slice_capability;
use crate::circuits::etable::EventTableChip;
use crate::circuits::etable::EventTableConfig;
use crate::circuits::external_host_call_table::ExternalHostCallChip;
Expand Down Expand Up @@ -61,7 +62,7 @@ use super::post_image_table::PostImageTableConfig;
pub const VAR_COLUMNS: usize = if cfg!(feature = "continuation") {
60
} else {
50
51
};

// Reserve a few rows to keep usable rows away from blind rows.
Expand Down Expand Up @@ -108,6 +109,7 @@ impl<F: FieldExt> Circuit<F> for ZkWasmCircuit<F> {

fn without_witnesses(&self) -> Self {
ZkWasmCircuit::new(
self.k,
// fill slice like circuit_without_witness
Slice {
itable: self.slice.itable.clone(),
Expand All @@ -127,8 +129,8 @@ impl<F: FieldExt> Circuit<F> for ZkWasmCircuit<F> {

is_last_slice: self.slice.is_last_slice,
},
self.slice_capability,
)
.unwrap()
}

fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
Expand Down Expand Up @@ -231,7 +233,7 @@ impl<F: FieldExt> Circuit<F> for ZkWasmCircuit<F> {
let frame_table_chip = JumpTableChip::new(config.jtable, config.max_available_rows);
let echip = EventTableChip::new(
config.etable,
self.slice_capability,
compute_slice_capability(self.k) as usize,
config.max_available_rows,
);
let bit_chip = BitTableChip::new(config.bit_table, config.max_available_rows);
Expand Down
Loading
Loading