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

refactor: uint module #75

Merged
merged 55 commits into from
Jun 28, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
55 commits
Select commit Hold shift + click to select a range
cba09be
confirm const across file impl
iammadab May 29, 2024
11949a4
Merge branch 'master' into feat/refactor-uint
iammadab May 29, 2024
210d714
Merge branch 'master' into feat/refactor-uint
iammadab May 29, 2024
a9093ff
Merge branch 'master' into feat/refactor-uint
iammadab May 29, 2024
7b6c70b
implement try from cell_id's to uint
iammadab May 29, 2024
18cfcac
add test for uint from cell ids
iammadab May 29, 2024
a2b39d6
add documentation
iammadab May 29, 2024
9bd42ed
document N_OPERAND_CELLS constant
iammadab May 29, 2024
3818103
wip
iammadab May 30, 2024
74516f3
test cell repacking
iammadab May 31, 2024
31a51c1
add documentation
iammadab May 31, 2024
c3e24e9
update packing test, ensure remaining values are 0s
iammadab May 31, 2024
e94e1e5
add more uint instantiation methods
iammadab Jun 3, 2024
97676c8
add test placeholders
iammadab Jun 3, 2024
a283f77
sketch base plan for cmp
iammadab Jun 3, 2024
65af7b5
implement and test pad cells
iammadab Jun 3, 2024
3a89440
modify from_range and from_bytes to use cell padding
iammadab Jun 3, 2024
eff16cf
extract logic for uint from arbitrary cell_width to make from_range a…
iammadab Jun 3, 2024
e9d2a41
add compile time evaluated min function
iammadab Jun 3, 2024
ffe140e
introduce new constant cleans up uint_from*
iammadab Jun 3, 2024
3bf521a
update uint from cell id test to test greater than N_OPERANDS
iammadab Jun 3, 2024
2c4a0ab
add test for uint from different sized cells
iammadab Jun 3, 2024
957ba24
implement add_unsafe
iammadab Jun 10, 2024
d49f31a
add functions sketch
iammadab Jun 11, 2024
632820f
wip
iammadab Jun 13, 2024
5b298c4
all func
iammadab Jun 13, 2024
e5403e4
building
iammadab Jun 13, 2024
5dce9db
test compiling
iammadab Jun 13, 2024
e810356
use range checker
iammadab Jun 13, 2024
17a63aa
refactor constants second pass
iammadab Jun 13, 2024
2033535
document cmp
iammadab Jun 13, 2024
9ca2e42
wip
iammadab Jun 13, 2024
14d0254
arithmetic second pass
iammadab Jun 13, 2024
c2ccb5e
delete old uint
iammadab Jun 13, 2024
4b0604f
Merge branch 'master' into feat/refactor-uint
iammadab Jun 13, 2024
8977106
refactor arithmetic
iammadab Jun 14, 2024
6dfaf71
fix documentation
iammadab Jun 14, 2024
08813e2
add test for add
iammadab Jun 14, 2024
d031363
test add constant unsafe
iammadab Jun 14, 2024
97f3945
add test for add_small_unsafe
iammadab Jun 14, 2024
8787912
implement handle borrow
iammadab Jun 14, 2024
8937ab0
test sub_unsafe
iammadab Jun 14, 2024
4c23282
merge with master
iammadab Jun 17, 2024
4d95615
rename add_small to add_cell
iammadab Jun 17, 2024
640541e
wip
iammadab Jun 17, 2024
aec94b2
change uint mod management
iammadab Jun 17, 2024
3c61078
setup structure for namespacing constants
iammadab Jun 17, 2024
02bbaee
refactor counter vector implementation
iammadab Jun 18, 2024
55519da
move add specific constants to AddSub block
iammadab Jun 25, 2024
d8aa67d
fix comment arithmetic precedence
iammadab Jun 26, 2024
834783f
wip
iammadab Jun 26, 2024
ca607d2
use range cells instead of range cells no overflow
iammadab Jun 27, 2024
d0e1d06
add optimization comment
iammadab Jun 27, 2024
fff6549
wip
iammadab Jun 27, 2024
3e74ec7
rename witness extractors
iammadab Jun 27, 2024
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
2 changes: 1 addition & 1 deletion singer-pro/src/basic_block.rs
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
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
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
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
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
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
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
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
Loading