Skip to content

Commit

Permalink
refactor: uint module (#75)
Browse files Browse the repository at this point in the history 
* confirm const across file impl

* implement try from cell_id's to uint

* add test for uint from cell ids

* add documentation

* document N_OPERAND_CELLS constant

* wip

* test cell repacking

* add documentation

* update packing test, ensure remaining values are 0s

* add more uint instantiation methods

* add test placeholders

* sketch base plan for cmp

* implement and test pad cells

* modify from_range and from_bytes to use cell padding

* extract logic for uint from arbitrary cell_width to make from_range and from_bytes easier

* add compile time evaluated min function

* introduce new constant  cleans up uint_from*

* update uint from cell id test to test greater than N_OPERANDS

* add test for uint from different sized cells

* implement add_unsafe

* add functions sketch

* wip

* all func

* building

* test compiling

* use range checker

* refactor constants second pass

* document cmp

* wip

* arithmetic second pass

* delete old uint

* refactor arithmetic

* fix documentation

* add test for add

* test add constant unsafe

* add test for add_small_unsafe

* implement handle borrow

* test sub_unsafe

* rename add_small to add_cell

* wip

* change uint mod management

* setup structure for namespacing constants

* refactor counter vector implementation

* move add specific constants to AddSub block

* fix comment arithmetic precedence

* wip

* use range cells instead of range cells no overflow

* add optimization comment

* wip

* rename witness extractors
  • Loading branch information
@iammadab @yczhangsjtu
iammadab authored and yczhangsjtu committed Aug 12, 2024
1 parent ab8ccd0 commit 8b27871
Show file tree
Hide file tree
Showing 39 changed files with 1,655 additions and 1,078 deletions.
2 changes: 1 addition & 1 deletion singer-pro/src/basic_block.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -536,7 +536,7 @@ mod test {
LayerWitness::default(),
LayerWitness::default(),
LayerWitness {
instances: random_matrix(n_instances, PCUInt::N_OPRAND_CELLS),
instances: random_matrix(n_instances, PCUInt::N_OPERAND_CELLS),
},
LayerWitness::default(),
LayerWitness::default(),
Expand Down
12 changes: 6 additions & 6 deletions singer-pro/src/basic_block/bb_final.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ use gkr::structs::Circuit;
use itertools::Itertools;
use paste::paste;
use simple_frontend::structs::{CircuitBuilder, MixedCell};
use singer_utils::uint::constants::AddSubConstants;
use singer_utils::{
chip_handler::{
GlobalStateChipOperations, OAMOperations, ROMOperations, RangeChipOperations,
Expand All @@ -12,7 +13,6 @@ use singer_utils::{
chips::IntoEnumIterator,
register_witness,
structs::{ChipChallenges, InstOutChipType, PCUInt, RAMHandler, ROMHandler, StackUInt, TSUInt},
uint::UIntAddSub,
};
use std::sync::Arc;

Expand All @@ -28,7 +28,7 @@ pub struct BasicBlockFinal;

register_witness!(BasicBlockFinal, phase0 {
// State in related
stack_ts_add => UIntAddSub::<TSUInt>::N_NO_OVERFLOW_WITNESS_CELLS
stack_ts_add => AddSubConstants::<TSUInt>::N_WITNESS_CELLS_NO_CARRY_OVERFLOW
});

impl BasicBlockFinal {
Expand All @@ -49,12 +49,12 @@ impl BasicBlockFinal {
let (phase0_wire_id, phase0) = circuit_builder.create_witness_in(Self::phase0_size());

// From BB start
let (stack_ts_id, stack_ts) = circuit_builder.create_witness_in(TSUInt::N_OPRAND_CELLS);
let (stack_ts_id, stack_ts) = circuit_builder.create_witness_in(TSUInt::N_OPERAND_CELLS);
let (stack_top_id, stack_top) = circuit_builder.create_witness_in(1);
let (clk_id, clk) = circuit_builder.create_witness_in(1);

// From inst pc.
let (next_pc_id, next_pc) = circuit_builder.create_witness_in(PCUInt::N_OPRAND_CELLS);
let (next_pc_id, next_pc) = circuit_builder.create_witness_in(PCUInt::N_OPERAND_CELLS);

let mut ram_handler = RAMHandler::new(&challenges);
let mut rom_handler = ROMHandler::new(&challenges);
Expand All @@ -68,7 +68,7 @@ impl BasicBlockFinal {
stack_ts_add_witness,
)?;

let (memory_ts_id, memory_ts) = circuit_builder.create_witness_in(TSUInt::N_OPRAND_CELLS);
let (memory_ts_id, memory_ts) = circuit_builder.create_witness_in(TSUInt::N_OPERAND_CELLS);
let stack_top_expr = MixedCell::Cell(stack_top[0]);
let clk_expr = MixedCell::Cell(clk[0]);
ram_handler.state_out(
Expand All @@ -92,7 +92,7 @@ impl BasicBlockFinal {
.iter()
.map(|offset| {
let (stack_from_insts_id, stack_from_insts) =
circuit_builder.create_witness_in(StackUInt::N_OPRAND_CELLS);
circuit_builder.create_witness_in(StackUInt::N_OPERAND_CELLS);
ram_handler.stack_push(
&mut circuit_builder,
stack_top_expr.add(i64_to_base_field::<E>(*offset)),
Expand Down
16 changes: 8 additions & 8 deletions singer-pro/src/basic_block/bb_ret.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ impl BasicBlockReturn {
let n_stack_items = stack_top_offsets.len();

// From BB Start
let (stack_ts_id, stack_ts) = circuit_builder.create_witness_in(TSUInt::N_OPRAND_CELLS);
let (stack_ts_id, stack_ts) = circuit_builder.create_witness_in(TSUInt::N_OPERAND_CELLS);
let (stack_top_id, stack_top) = circuit_builder.create_witness_in(1);
let (clk_id, _) = circuit_builder.create_witness_in(1);

Expand All @@ -62,7 +62,7 @@ impl BasicBlockReturn {
rom_handler.range_check_stack_top(&mut circuit_builder, stack_top_r)?;

// From predesessor instruction
let (memory_ts_id, _) = circuit_builder.create_witness_in(TSUInt::N_OPRAND_CELLS);
let (memory_ts_id, _) = circuit_builder.create_witness_in(TSUInt::N_OPERAND_CELLS);
let stack_operand_ids = stack_top_offsets
.iter()
.map(|offset| {
Expand Down Expand Up @@ -113,8 +113,8 @@ register_witness!(
BBReturnRestMemLoad,
phase0 {
mem_byte => 1,
old_memory_ts => TSUInt::N_OPRAND_CELLS,
offset => StackUInt::N_OPRAND_CELLS
old_memory_ts => TSUInt::N_OPERAND_CELLS,
offset => StackUInt::N_OPERAND_CELLS
}
);

Expand Down Expand Up @@ -160,7 +160,7 @@ register_witness!(
BBReturnRestMemStore,
phase0 {
mem_byte => 1,
offset => StackUInt::N_OPRAND_CELLS
offset => StackUInt::N_OPERAND_CELLS
}
);

Expand All @@ -176,7 +176,7 @@ impl BBReturnRestMemStore {
let offset = &phase0[Self::phase0_offset()];
let mem_byte = phase0[Self::phase0_mem_byte().start];
// memory_ts is zero.
let memory_ts = circuit_builder.create_cells(StackUInt::N_OPRAND_CELLS);
let memory_ts = circuit_builder.create_cells(StackUInt::N_OPERAND_CELLS);
ram_handler.oam_store(&mut circuit_builder, offset, &memory_ts, &[mem_byte]);

let (ram_load_id, ram_store_id) = ram_handler.finalize(&mut circuit_builder);
Expand Down Expand Up @@ -206,8 +206,8 @@ pub struct BBReturnRestStackPop;
register_witness!(
BBReturnRestStackPop,
phase0 {
old_stack_ts => TSUInt::N_OPRAND_CELLS,
stack_values => StackUInt::N_OPRAND_CELLS
old_stack_ts => TSUInt::N_OPERAND_CELLS,
stack_values => StackUInt::N_OPERAND_CELLS
}
);

Expand Down
22 changes: 11 additions & 11 deletions singer-pro/src/basic_block/bb_start.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ use ff_ext::ExtensionField;
use gkr::structs::Circuit;
use paste::paste;
use simple_frontend::structs::{CircuitBuilder, MixedCell};
use singer_utils::uint::constants::AddSubConstants;
use singer_utils::{
chip_handler::{
GlobalStateChipOperations, OAMOperations, ROMOperations, RangeChipOperations,
Expand All @@ -11,7 +12,6 @@ use singer_utils::{
chips::IntoEnumIterator,
register_multi_witness,
structs::{ChipChallenges, InstOutChipType, PCUInt, RAMHandler, ROMHandler, StackUInt, TSUInt},
uint::UIntCmp,
};
use std::sync::Arc;

Expand All @@ -27,16 +27,16 @@ pub(crate) struct BasicBlockStart;

register_multi_witness!(BasicBlockStart, phase0(n_stack_items) {
// State in related
pc => PCUInt::N_OPRAND_CELLS,
stack_ts => TSUInt::N_OPRAND_CELLS,
memory_ts => TSUInt::N_OPRAND_CELLS,
pc => PCUInt::N_OPERAND_CELLS,
stack_ts => TSUInt::N_OPERAND_CELLS,
memory_ts => TSUInt::N_OPERAND_CELLS,
stack_top => 1,
clk => 1,

// Stack values
old_stack_values(n_stack_items) => StackUInt::N_OPRAND_CELLS,
old_stack_ts(n_stack_items) => TSUInt::N_OPRAND_CELLS,
old_stack_ts_lt(n_stack_items) => UIntCmp::<TSUInt>::N_NO_OVERFLOW_WITNESS_CELLS
old_stack_values(n_stack_items) => StackUInt::N_OPERAND_CELLS,
old_stack_ts(n_stack_items) => TSUInt::N_OPERAND_CELLS,
old_stack_ts_lt(n_stack_items) => AddSubConstants::<TSUInt>::N_WITNESS_CELLS_NO_CARRY_OVERFLOW
});

impl BasicBlockStart {
Expand Down Expand Up @@ -83,7 +83,7 @@ impl BasicBlockStart {
for (i, offset) in stack_top_offsets.iter().enumerate() {
let old_stack_ts =
TSUInt::try_from(&phase0[Self::phase0_old_stack_ts(i, n_stack_items)])?;
UIntCmp::<TSUInt>::assert_lt(
TSUInt::assert_lt(
&mut circuit_builder,
&mut rom_handler,
&old_stack_ts,
Expand All @@ -102,9 +102,9 @@ impl BasicBlockStart {
let mut stack_result_ids = Vec::with_capacity(n_stack_items);
for i in 0..n_stack_items {
let (stack_operand_id, stack_operand) =
circuit_builder.create_witness_out(StackUInt::N_OPRAND_CELLS);
circuit_builder.create_witness_out(StackUInt::N_OPERAND_CELLS);
let old_stack = &phase0[Self::phase0_old_stack_values(i, n_stack_items)];
for j in 0..StackUInt::N_OPRAND_CELLS {
for j in 0..StackUInt::N_OPERAND_CELLS {
circuit_builder.add(stack_operand[j], old_stack[j], E::BaseField::ONE);
}
stack_result_ids.push(stack_operand_id);
Expand All @@ -114,7 +114,7 @@ impl BasicBlockStart {

// To BB final
let (out_stack_ts_id, out_stack_ts) =
circuit_builder.create_witness_out(TSUInt::N_OPRAND_CELLS);
circuit_builder.create_witness_out(TSUInt::N_OPERAND_CELLS);
add_assign_each_cell(&mut circuit_builder, &out_stack_ts, stack_ts.values());
let (out_stack_top_id, out_stack_top) = circuit_builder.create_witness_out(1);
circuit_builder.add(out_stack_top[0], stack_top, E::BaseField::ONE);
Expand Down
14 changes: 7 additions & 7 deletions singer-pro/src/instructions/add.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,13 @@ use ff_ext::ExtensionField;
use gkr::structs::Circuit;
use paste::paste;
use simple_frontend::structs::CircuitBuilder;
use singer_utils::uint::constants::AddSubConstants;
use singer_utils::{
chip_handler::ROMOperations,
chips::IntoEnumIterator,
constants::OpcodeType,
register_witness,
structs::{ChipChallenges, InstOutChipType, ROMHandler, StackUInt, TSUInt},
uint::UIntAddSub,
};
use std::sync::Arc;

Expand All @@ -30,7 +30,7 @@ register_witness!(
AddInstruction,
phase0 {
// Witness for addend_0 + addend_1
instruction_add => UIntAddSub::<StackUInt>::N_WITNESS_CELLS
instruction_add => AddSubConstants::<StackUInt>::N_WITNESS_CELLS
}
);

Expand All @@ -44,16 +44,16 @@ impl<E: ExtensionField> Instruction<E> for AddInstruction {
let (phase0_wire_id, phase0) = circuit_builder.create_witness_in(Self::phase0_size());

// From predesessor instruction
let (memory_ts_id, memory_ts) = circuit_builder.create_witness_in(TSUInt::N_OPRAND_CELLS);
let (addend_0_id, addend_0) = circuit_builder.create_witness_in(StackUInt::N_OPRAND_CELLS);
let (addend_1_id, addend_1) = circuit_builder.create_witness_in(StackUInt::N_OPRAND_CELLS);
let (memory_ts_id, memory_ts) = circuit_builder.create_witness_in(TSUInt::N_OPERAND_CELLS);
let (addend_0_id, addend_0) = circuit_builder.create_witness_in(StackUInt::N_OPERAND_CELLS);
let (addend_1_id, addend_1) = circuit_builder.create_witness_in(StackUInt::N_OPERAND_CELLS);

let mut rom_handler = ROMHandler::new(&challenges);

// Execution result = addend0 + addend1, with carry.
let addend_0 = addend_0.try_into()?;
let addend_1 = addend_1.try_into()?;
let result = UIntAddSub::<StackUInt>::add(
let result = StackUInt::add(
&mut circuit_builder,
&mut rom_handler,
&addend_0,
Expand All @@ -63,7 +63,7 @@ impl<E: ExtensionField> Instruction<E> for AddInstruction {
// To successor instruction
let stack_result_id = circuit_builder.create_witness_out_from_cells(result.values());
let (next_memory_ts_id, next_memory_ts) =
circuit_builder.create_witness_out(TSUInt::N_OPRAND_CELLS);
circuit_builder.create_witness_out(TSUInt::N_OPERAND_CELLS);
add_assign_each_cell(&mut circuit_builder, &next_memory_ts, &memory_ts);

// To chips
Expand Down
8 changes: 4 additions & 4 deletions singer-pro/src/instructions/calldataload.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ pub struct CalldataloadInstruction;
register_witness!(
CalldataloadInstruction,
phase0 {
data => StackUInt::N_OPRAND_CELLS
data => StackUInt::N_OPERAND_CELLS
}
);

Expand All @@ -41,8 +41,8 @@ impl<E: ExtensionField> Instruction<E> for CalldataloadInstruction {
// From witness
let (phase0_wire_id, phase0) = circuit_builder.create_witness_in(Self::phase0_size());
// From predesessor instruction
let (memory_ts_id, memory_ts) = circuit_builder.create_witness_in(TSUInt::N_OPRAND_CELLS);
let (offset_id, offset) = circuit_builder.create_witness_in(UInt64::N_OPRAND_CELLS);
let (memory_ts_id, memory_ts) = circuit_builder.create_witness_in(TSUInt::N_OPERAND_CELLS);
let (offset_id, offset) = circuit_builder.create_witness_in(UInt64::N_OPERAND_CELLS);

let mut rom_handler = ROMHandler::new(&challenges);

Expand All @@ -54,7 +54,7 @@ impl<E: ExtensionField> Instruction<E> for CalldataloadInstruction {
let (data_copy_id, data_copy) = circuit_builder.create_witness_out(data.len());
add_assign_each_cell(&mut circuit_builder, &data_copy, &data);
let (next_memory_ts_id, next_memory_ts) =
circuit_builder.create_witness_out(TSUInt::N_OPRAND_CELLS);
circuit_builder.create_witness_out(TSUInt::N_OPERAND_CELLS);
add_assign_each_cell(&mut circuit_builder, &next_memory_ts, &memory_ts);

// To chips
Expand Down
16 changes: 8 additions & 8 deletions singer-pro/src/instructions/gt.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,13 @@ use ff_ext::ExtensionField;
use gkr::structs::Circuit;
use paste::paste;
use simple_frontend::structs::CircuitBuilder;
use singer_utils::uint::constants::AddSubConstants;
use singer_utils::{
chip_handler::ROMOperations,
chips::IntoEnumIterator,
constants::OpcodeType,
register_witness,
structs::{ChipChallenges, InstOutChipType, ROMHandler, StackUInt, TSUInt},
uint::UIntCmp,
};
use std::sync::Arc;

Expand All @@ -28,7 +28,7 @@ register_witness!(
GtInstruction,
phase0 {
// Witness for operand_0 > operand_1
instruction_gt => UIntCmp::<StackUInt>::N_WITNESS_CELLS
instruction_gt => AddSubConstants::<StackUInt>::N_WITNESS_CELLS
}
);

Expand All @@ -42,18 +42,18 @@ impl<E: ExtensionField> Instruction<E> for GtInstruction {
let (phase0_wire_id, phase0) = circuit_builder.create_witness_in(Self::phase0_size());

// From predesessor instruction
let (memory_ts_id, memory_ts) = circuit_builder.create_witness_in(TSUInt::N_OPRAND_CELLS);
let (memory_ts_id, memory_ts) = circuit_builder.create_witness_in(TSUInt::N_OPERAND_CELLS);
let (operand_0_id, operand_0) =
circuit_builder.create_witness_in(StackUInt::N_OPRAND_CELLS);
circuit_builder.create_witness_in(StackUInt::N_OPERAND_CELLS);
let (operand_1_id, operand_1) =
circuit_builder.create_witness_in(StackUInt::N_OPRAND_CELLS);
circuit_builder.create_witness_in(StackUInt::N_OPERAND_CELLS);

let mut rom_handler = ROMHandler::new(&challenges);

// Execution operand_1 > operand_0.
let operand_0 = operand_0.try_into()?;
let operand_1 = operand_1.try_into()?;
let (result, _) = UIntCmp::<StackUInt>::lt(
let (result, _) = StackUInt::lt(
&mut circuit_builder,
&mut rom_handler,
&operand_0,
Expand All @@ -62,13 +62,13 @@ impl<E: ExtensionField> Instruction<E> for GtInstruction {
)?;
let result = [
vec![result],
circuit_builder.create_cells(StackUInt::N_OPRAND_CELLS - 1),
circuit_builder.create_cells(StackUInt::N_OPERAND_CELLS - 1),
]
.concat();
// To successor instruction
let stack_result_id = circuit_builder.create_witness_out_from_cells(&result);
let (next_memory_ts_id, next_memory_ts) =
circuit_builder.create_witness_out(TSUInt::N_OPRAND_CELLS);
circuit_builder.create_witness_out(TSUInt::N_OPERAND_CELLS);
add_assign_each_cell(&mut circuit_builder, &next_memory_ts, &memory_ts);

// To chips
Expand Down
6 changes: 3 additions & 3 deletions singer-pro/src/instructions/jump.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,16 +27,16 @@ impl<E: ExtensionField> Instruction<E> for JumpInstruction {
fn construct_circuit(_: ChipChallenges) -> Result<InstCircuit<E>, ZKVMError> {
let mut circuit_builder = CircuitBuilder::new();
// From predesessor instruction
let (memory_ts_id, memory_ts) = circuit_builder.create_witness_in(TSUInt::N_OPRAND_CELLS);
let (next_pc_id, next_pc) = circuit_builder.create_witness_in(StackUInt::N_OPRAND_CELLS);
let (memory_ts_id, memory_ts) = circuit_builder.create_witness_in(TSUInt::N_OPERAND_CELLS);
let (next_pc_id, next_pc) = circuit_builder.create_witness_in(StackUInt::N_OPERAND_CELLS);

// To BB final
let (next_pc_copy_id, next_pc_copy) = circuit_builder.create_witness_out(next_pc.len());
add_assign_each_cell(&mut circuit_builder, &next_pc_copy, &next_pc);

// To Succesor instruction
let (next_memory_ts_id, next_memory_ts) =
circuit_builder.create_witness_out(TSUInt::N_OPRAND_CELLS);
circuit_builder.create_witness_out(TSUInt::N_OPERAND_CELLS);
add_assign_each_cell(&mut circuit_builder, &next_memory_ts, &memory_ts);

// To chips
Expand Down
Loading

0 comments on commit 8b27871

Please sign in to comment.