Skip to content

Commit

Permalink
fix: logic offset (#43)
Browse files Browse the repository at this point in the history 
* chore: fix kernel

* chore: fix kernel

* chore: fix kernel

* chore: fix kernel

* chore: fix kernel

* chore: fix bootstrap
  • Loading branch information
@eigmax
eigmax authored Nov 19, 2023
1 parent bebcd4b commit 41879d8
Show file tree
Hide file tree
Showing 14 changed files with 96 additions and 296 deletions.
37 changes: 21 additions & 16 deletions src/all_stark.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,8 +26,8 @@ pub struct AllStark<F: RichField + Extendable<D>, const D: usize> {
pub arithmetic_stark: ArithmeticStark<F, D>,
// pub byte_packing_stark: BytePackingStark<F, D>,
pub cpu_stark: CpuStark<F, D>,
pub keccak_stark: KeccakStark<F, D>,
pub keccak_sponge_stark: KeccakSpongeStark<F, D>,
//pub keccak_stark: KeccakStark<F, D>,
//pub keccak_sponge_stark: KeccakSpongeStark<F, D>,
pub logic_stark: LogicStark<F, D>,
pub memory_stark: MemoryStark<F, D>,
pub cross_table_lookups: Vec<CrossTableLookup<F>>,
Expand All @@ -39,8 +39,8 @@ impl<F: RichField + Extendable<D>, const D: usize> Default for AllStark<F, D> {
arithmetic_stark: ArithmeticStark::default(),
// byte_packing_stark: BytePackingStark::default(),
cpu_stark: CpuStark::default(),
keccak_stark: KeccakStark::default(),
keccak_sponge_stark: KeccakSpongeStark::default(),
//keccak_stark: KeccakStark::default(),
//keccak_sponge_stark: KeccakSpongeStark::default(),
logic_stark: LogicStark::default(),
memory_stark: MemoryStark::default(),
cross_table_lookups: all_cross_table_lookups(),
Expand All @@ -49,13 +49,13 @@ impl<F: RichField + Extendable<D>, const D: usize> Default for AllStark<F, D> {
}

impl<F: RichField + Extendable<D>, const D: usize> AllStark<F, D> {
pub(crate) fn num_lookups_helper_columns(&self, config: &StarkConfig) -> [usize; 6] {
pub(crate) fn num_lookups_helper_columns(&self, config: &StarkConfig) -> [usize; NUM_TABLES] {
[
self.arithmetic_stark.num_lookup_helper_columns(config),
// self.byte_packing_stark.num_lookup_helper_columns(config),
self.cpu_stark.num_lookup_helper_columns(config),
self.keccak_stark.num_lookup_helper_columns(config),
self.keccak_sponge_stark.num_lookup_helper_columns(config),
//self.keccak_stark.num_lookup_helper_columns(config),
//self.keccak_sponge_stark.num_lookup_helper_columns(config),
self.logic_stark.num_lookup_helper_columns(config),
self.memory_stark.num_lookup_helper_columns(config),
]
Expand All @@ -66,10 +66,10 @@ impl<F: RichField + Extendable<D>, const D: usize> AllStark<F, D> {
pub enum Table {
Arithmetic = 0,
Cpu = 1,
Keccak = 2,
KeccakSponge = 3,
Logic = 4,
Memory = 5,
//Keccak = 2,
//KeccakSponge = 3,
Logic = 2,
Memory = 3,
}

pub(crate) const NUM_TABLES: usize = Table::Memory as usize + 1;
Expand All @@ -79,8 +79,8 @@ impl Table {
[
Self::Arithmetic,
Self::Cpu,
Self::Keccak,
Self::KeccakSponge,
//Self::Keccak,
//Self::KeccakSponge,
Self::Logic,
Self::Memory,
]
Expand All @@ -90,9 +90,9 @@ impl Table {
pub(crate) fn all_cross_table_lookups<F: Field>() -> Vec<CrossTableLookup<F>> {
vec![
ctl_arithmetic(),
ctl_keccak_sponge(),
ctl_keccak_inputs(),
ctl_keccak_outputs(),
//ctl_keccak_sponge(),
//ctl_keccak_inputs(),
//ctl_keccak_outputs(),
ctl_logic(),
ctl_memory(),
]
Expand All @@ -108,6 +108,7 @@ fn ctl_arithmetic<F: Field>() -> CrossTableLookup<F> {
// We now need two different looked tables for `KeccakStark`:
// one for the inputs and one for the outputs.
// They are linked with the timestamp.
/*
fn ctl_keccak_inputs<F: Field>() -> CrossTableLookup<F> {
let keccak_sponge_looking = TableWithColumns::new(
Table::KeccakSponge,
Expand Down Expand Up @@ -149,6 +150,7 @@ fn ctl_keccak_sponge<F: Field>() -> CrossTableLookup<F> {
);
CrossTableLookup::new(vec![cpu_looking], keccak_sponge_looked)
}
*/

pub(crate) fn ctl_logic<F: Field>() -> CrossTableLookup<F> {
let cpu_looking = TableWithColumns::new(
Expand Down Expand Up @@ -185,6 +187,7 @@ fn ctl_memory<F: Field>() -> CrossTableLookup<F> {
Some(cpu_stark::ctl_filter_gp_memory(channel)),
)
});
/*
let keccak_sponge_reads = (0..KECCAK_RATE_BYTES).map(|i| {
TableWithColumns::new(
Table::KeccakSponge,
Expand All @@ -196,6 +199,8 @@ fn ctl_memory<F: Field>() -> CrossTableLookup<F> {
.into_iter()
.chain(keccak_sponge_reads)
.collect();
*/
let all_lookers = cpu_memory_gp_ops.collect();
let memory_looked = TableWithColumns::new(
Table::Memory,
memory_stark::ctl_data(),
Expand Down
30 changes: 18 additions & 12 deletions src/cpu/bootstrap_kernel.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,19 +14,21 @@ use crate::generation::state::GenerationState;

use crate::memory::segments::Segment;
use crate::witness::memory::MemoryAddress;
use crate::witness::util::{keccak_sponge_log, mem_write_gp_log_and_fill};
use crate::witness::util::mem_write_gp_log_and_fill;

pub(crate) fn generate_bootstrap_kernel<F: Field>(state: &mut GenerationState<F>) {
// Iterate through chunks of the code, such that we can write one chunk to memory per row.
for chunk in &KERNEL.program.image.iter().chunks(NUM_GP_CHANNELS) {
let mut cpu_row = CpuColumnsView::default();
println!("trace: {:?}", state.traces.clock());
cpu_row.clock = F::from_canonical_usize(state.traces.clock());
cpu_row.is_bootstrap_kernel = F::ONE;

// Write this chunk to memory, while simultaneously packing its bytes into a u32 word.
for (channel, (addr, val)) in chunk.enumerate() {
// FIXMEBoth instruction and memory data are located in
// code section for MIPS
println!("addr: {}", *addr);
let address = MemoryAddress::new(0, Segment::Code, *addr as usize);
let write =
mem_write_gp_log_and_fill(channel, address, state, &mut cpu_row, (*val).to_be());
Expand All @@ -53,11 +55,13 @@ pub(crate) fn generate_bootstrap_kernel<F: Field>(state: &mut GenerationState<F>
// FIXME: store all the hash
final_cpu_row.mem_channels[4].value = KERNEL.code_hash.map(F::from_canonical_u32)[0];
//final_cpu_row.mem_channels[4].value.reverse();
/*
keccak_sponge_log(
state,
MemoryAddress::new(0, Segment::Code, 0),
KERNEL.code.clone(),
);
*/
state.traces.push_cpu(final_cpu_row);
state.traces.push_cpu(final_cpu_row);

Expand All @@ -79,15 +83,17 @@ pub(crate) fn eval_bootstrap_kernel_packed<F: Field, P: PackedField<Scalar = F>>
yield_constr.constraint_transition(delta_is_bootstrap * (delta_is_bootstrap + P::ONES));

// If this is a bootloading row and the i'th memory channel is used, it must have the right
// address, name context = 0, segment = Code, virt = clock * NUM_GP_CHANNELS + i.
// address, name context = 0, segment = Code, virt + 4 = next_virt
let code_segment = F::from_canonical_usize(Segment::Code as usize);
for (i, channel) in local_values.mem_channels.iter().enumerate() {
let filter = local_is_bootstrap * channel.used;
yield_constr.constraint(filter * channel.addr_context);
yield_constr.constraint(filter * (channel.addr_segment - code_segment));
let expected_virt = local_values.clock * F::from_canonical_usize(NUM_GP_CHANNELS)
+ F::from_canonical_usize(i);
yield_constr.constraint(filter * (channel.addr_virtual - expected_virt));
/* FIXME
let delta_virt = channel.addr_virtual + P::from(F::from_canonical_u32(32)) - next_values.mem_channels[i].addr_virtual;
println!("virt {:?} {:?} {:?} {:?} {}", channel.addr_virtual, delta_virt, local_values.clock, NUM_GP_CHANNELS, i);
yield_constr.constraint_transition(filter * delta_virt);
*/
}

// If this is the final bootstrap row (i.e. delta_is_bootstrap = 1), check that
Expand Down Expand Up @@ -130,7 +136,7 @@ pub(crate) fn eval_bootstrap_kernel_ext_circuit<F: RichField + Extendable<D>, co
yield_constr.constraint_transition(builder, constraint);

// If this is a bootloading row and the i'th memory channel is used, it must have the right
// address, name context = 0, segment = Code, virt = clock * NUM_GP_CHANNELS + i.
// address, name context = 0, segment = Code, virt + 4 = next_virt
let code_segment =
builder.constant_extension(F::Extension::from_canonical_usize(Segment::Code as usize));
for (i, channel) in local_values.mem_channels.iter().enumerate() {
Expand All @@ -142,13 +148,13 @@ pub(crate) fn eval_bootstrap_kernel_ext_circuit<F: RichField + Extendable<D>, co
let constraint = builder.mul_extension(filter, segment_diff);
yield_constr.constraint(builder, constraint);

let i_ext = builder.constant_extension(F::Extension::from_canonical_usize(i));
let num_gp_channels_f = F::from_canonical_usize(NUM_GP_CHANNELS);
let expected_virt =
builder.mul_const_add_extension(num_gp_channels_f, local_values.clock, i_ext);
let virt_diff = builder.sub_extension(channel.addr_virtual, expected_virt);
/*
let i_ext = builder.constant_extension(F::Extension::from_canonical_u32(32));
let prev_virt = builder.add_extension(channel.addr_virtual, i_ext);
let virt_diff = builder.sub_extension(prev_virt, next_values.mem_channels[i].addr_virtual);
let constraint = builder.mul_extension(filter, virt_diff);
yield_constr.constraint(builder, constraint);
yield_constr.constraint_transition(builder, constraint);
*/
}

// If this is the final bootstrap row (i.e. delta_is_bootstrap = 1), check that
Expand Down
2 changes: 1 addition & 1 deletion src/cpu/columns/ops.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ pub struct OpsColumnsView<T: Copy> {
pub binary_op: T, // Combines ADD, MUL, SUB, DIV, SLL, ... flags.
pub binary_imm_op: T, // Combines ADDI, ADDIU
pub eq_iszero: T, // Combines EQ and ISZERO flags.
pub logic_op: T, // Combines AND, OR and XOR flags.
pub logic_op: T, // Combines AND, OR, XOR, Nor flags.
pub condmov_op: T,
pub count_op: T,
pub not: T,
Expand Down
18 changes: 11 additions & 7 deletions src/cpu/cpu_stark.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -57,9 +57,9 @@ pub fn ctl_filter_keccak_sponge<F: Field>() -> Column<F> {
/// 36, out 68. But the looking table offers in0 77, in1 83, out 89.
fn ctl_data_binops<F: Field>() -> Vec<Column<F>> {
println!("{:?}", COL_MAP.mem_channels);
let mut res = Column::singles(vec![COL_MAP.mem_channels[0].value - 73]).collect_vec();
res.extend(Column::singles(vec![COL_MAP.mem_channels[1].value - 47]));
res.extend(Column::singles(vec![COL_MAP.mem_channels[2].value - 21]));
let mut res = Column::singles(vec![COL_MAP.mem_channels[0].value]).collect_vec();
res.extend(Column::singles(vec![COL_MAP.mem_channels[1].value]));
res.extend(Column::singles(vec![COL_MAP.mem_channels[2].value]));
res
}

Expand Down Expand Up @@ -194,17 +194,19 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
bootstrap_kernel::eval_bootstrap_kernel_packed(local_values, next_values, yield_constr);
/*
contextops::eval_packed(local_values, next_values, yield_constr);
*/
control_flow::eval_packed_generic(local_values, next_values, yield_constr);
*/
decode::eval_packed_generic(local_values, yield_constr);
jumps::eval_packed(local_values, next_values, yield_constr);
membus::eval_packed(local_values, yield_constr);
memio::eval_packed(local_values, next_values, yield_constr);
//memio::eval_packed(local_values, next_values, yield_constr);
pc::eval_packed(local_values, next_values, yield_constr);
/*
shift::eval_packed(local_values, yield_constr);
syscall::eval_packed(local_values, yield_constr);
mov::eval_packed(local_values, yield_constr);
count::eval_packed(local_values, yield_constr);
*/
}

fn eval_ext_circuit(
Expand All @@ -228,17 +230,19 @@ impl<F: RichField + Extendable<D>, const D: usize> Stark<F, D> for CpuStark<F, D
);
/*
contextops::eval_ext_circuit(builder, local_values, next_values, yield_constr);
*/
control_flow::eval_ext_circuit(builder, local_values, next_values, yield_constr);
*/
decode::eval_ext_circuit(builder, local_values, yield_constr);
jumps::eval_ext_circuit(builder, local_values, next_values, yield_constr);
membus::eval_ext_circuit(builder, local_values, yield_constr);
memio::eval_ext_circuit(builder, local_values, next_values, yield_constr);
//memio::eval_ext_circuit(builder, local_values, next_values, yield_constr);
pc::eval_ext_circuit(builder, local_values, next_values, yield_constr);
/*
shift::eval_ext_circuit(builder, local_values, yield_constr);
syscall::eval_ext_circuit(builder, local_values, yield_constr);
mov::eval_ext_circuit(builder, local_values, yield_constr);
count::eval_ext_circuit(builder, local_values, yield_constr);
*/
}

fn constraint_degree(&self) -> usize {
Expand Down
92 changes: 1 addition & 91 deletions src/cpu/decode.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,45 +97,7 @@ pub fn eval_packed_generic<P: PackedField>(
yield_constr.constraint(flag_sum * (flag_sum - P::ONES));

// Finally, classify all opcodes, together with the kernel flag, into blocks
for (oc, block_length, kernel_only, col) in OPCODES {
// 0 if the block/flag is available to us (is always available or we are in kernel mode) and
// 1 otherwise.
let unavailable = match kernel_only {
false => P::ZEROS,
true => P::ONES - kernel_mode,
};
// 0 if all the opcode bits match, and something in {1, ..., 8}, otherwise.
let opcode_mismatch: P = lv
.opcode_bits
.into_iter()
.zip(bits_from_opcode(oc))
.rev()
.take(8 - block_length)
.map(|(row_bit, flag_bit)| match flag_bit {
// 1 if the bit does not match, and 0 otherwise
false => row_bit,
true => P::ONES - row_bit,
})
.sum();

// If unavailable + opcode_mismatch is 0, then the opcode bits all match and we are in the
// correct mode.
yield_constr.constraint(lv[col] * (unavailable + opcode_mismatch));
}

// Manually check lv.op.m_op_constr
let opcode: P = lv
.opcode_bits
.into_iter()
.enumerate()
.map(|(i, bit)| bit * P::Scalar::from_canonical_u64(1 << i))
.sum();
yield_constr.constraint((P::ONES - kernel_mode) * lv.op.m_op_general);

let m_op_constr = (opcode - P::Scalar::from_canonical_usize(0xfb_usize))
* (opcode - P::Scalar::from_canonical_usize(0xfc_usize))
* lv.op.m_op_general;
yield_constr.constraint(m_op_constr);
// TODO
}

pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
Expand Down Expand Up @@ -186,56 +148,4 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
}

// Finally, classify all opcodes, together with the kernel flag, into blocks
for (oc, block_length, kernel_only, col) in OPCODES {
// 0 if the block/flag is available to us (is always available or we are in kernel mode) and
// 1 otherwise.
let unavailable = match kernel_only {
false => builder.zero_extension(),
true => builder.sub_extension(one, kernel_mode),
};
// 0 if all the opcode bits match, and something in {1, ..., 8}, otherwise.
let opcode_mismatch = lv
.opcode_bits
.into_iter()
.zip(bits_from_opcode(oc))
.rev()
.take(8 - block_length)
.fold(builder.zero_extension(), |cumul, (row_bit, flag_bit)| {
let to_add = match flag_bit {
false => row_bit,
true => builder.sub_extension(one, row_bit),
};
builder.add_extension(cumul, to_add)
});

// If unavailable + opcode_mismatch is 0, then the opcode bits all match and we are in the
// correct mode.
let constr = builder.add_extension(unavailable, opcode_mismatch);
let constr = builder.mul_extension(lv[col], constr);
yield_constr.constraint(builder, constr);
}

// Manually check lv.op.m_op_constr
let opcode = lv
.opcode_bits
.into_iter()
.rev()
.fold(builder.zero_extension(), |cumul, bit| {
builder.mul_const_add_extension(F::TWO, cumul, bit)
});

let mload_opcode = builder.constant_extension(F::Extension::from_canonical_usize(0xfb_usize));
let mstore_opcode = builder.constant_extension(F::Extension::from_canonical_usize(0xfc_usize));

let one_extension = builder.constant_extension(F::Extension::ONE);
let is_not_kernel_mode = builder.sub_extension(one_extension, kernel_mode);
let constr = builder.mul_extension(is_not_kernel_mode, lv.op.m_op_general);
yield_constr.constraint(builder, constr);

let mload_constr = builder.sub_extension(opcode, mload_opcode);
let mstore_constr = builder.sub_extension(opcode, mstore_opcode);
let mut m_op_constr = builder.mul_extension(mload_constr, mstore_constr);
m_op_constr = builder.mul_extension(m_op_constr, lv.op.m_op_general);

yield_constr.constraint(builder, m_op_constr);
}
12 changes: 6 additions & 6 deletions src/cpu/jumps.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -644,9 +644,9 @@ pub fn eval_packed<P: PackedField>(
yield_constr: &mut ConstraintConsumer<P>,
) {
eval_packed_exit_kernel(lv, nv, yield_constr);
eval_packed_jump_jumpi(lv, nv, yield_constr);
eval_packed_branch(lv, nv, yield_constr);
eval_packed_condmov(lv, nv, yield_constr);
//eval_packed_jump_jumpi(lv, nv, yield_constr);
//eval_packed_branch(lv, nv, yield_constr);
//eval_packed_condmov(lv, nv, yield_constr);
}

pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
Expand All @@ -656,7 +656,7 @@ pub fn eval_ext_circuit<F: RichField + Extendable<D>, const D: usize>(
yield_constr: &mut RecursiveConstraintConsumer<F, D>,
) {
eval_ext_circuit_exit_kernel(builder, lv, nv, yield_constr);
eval_ext_circuit_jump_jumpi(builder, lv, nv, yield_constr);
eval_ext_circuit_branch(builder, lv, nv, yield_constr);
eval_ext_circuit_condmov(builder, lv, nv, yield_constr);
//eval_ext_circuit_jump_jumpi(builder, lv, nv, yield_constr);
//eval_ext_circuit_branch(builder, lv, nv, yield_constr);
//eval_ext_circuit_condmov(builder, lv, nv, yield_constr);
}
Loading

0 comments on commit 41879d8

Please sign in to comment.