Skip to content

Commit

Permalink
Remove all preinit memory (#1610)
Browse files Browse the repository at this point in the history
  • Loading branch information
spiral-ladder authored May 8, 2024
1 parent 22f4f18 commit e5007e9
Show file tree
Hide file tree
Showing 31 changed files with 473 additions and 988 deletions.
3 changes: 3 additions & 0 deletions circuits/src/cpu/columns.rs
Original file line number Diff line number Diff line change
Expand Up @@ -178,6 +178,7 @@ pub struct CpuState<T> {
pub is_event_tape: T,
pub is_events_commitment_tape: T,
pub is_cast_list_commitment_tape: T,
pub is_self_prog_id_tape: T,
pub is_halt: T,
pub is_poseidon2: T,
}
Expand Down Expand Up @@ -330,6 +331,7 @@ pub fn lookup_for_storage_tables() -> TableWithTypedOutput<StorageDeviceCtl<Colu
CPU.is_event_tape,
CPU.is_events_commitment_tape,
CPU.is_cast_list_commitment_tape,
CPU.is_self_prog_id_tape,
]),
clk: CPU.clk,
addr: CPU.io_addr,
Expand All @@ -342,6 +344,7 @@ pub fn lookup_for_storage_tables() -> TableWithTypedOutput<StorageDeviceCtl<Colu
CPU.is_event_tape,
CPU.is_events_commitment_tape,
CPU.is_cast_list_commitment_tape,
CPU.is_self_prog_id_tape,
]
.iter()
.sum(),
Expand Down
3 changes: 3 additions & 0 deletions circuits/src/cpu/ecall.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ pub(crate) fn constraints<'a, P: Copy>(
cb.always(lv.is_event_tape.is_binary());
cb.always(lv.is_events_commitment_tape.is_binary());
cb.always(lv.is_cast_list_commitment_tape.is_binary());
cb.always(lv.is_self_prog_id_tape.is_binary());
cb.always(
lv.inst.ops.ecall
- (lv.is_halt
Expand All @@ -32,6 +33,7 @@ pub(crate) fn constraints<'a, P: Copy>(
+ lv.is_event_tape
+ lv.is_events_commitment_tape
+ lv.is_cast_list_commitment_tape
+ lv.is_self_prog_id_tape
+ lv.is_poseidon2),
);
halt_constraints(lv, nv, cb);
Expand Down Expand Up @@ -86,6 +88,7 @@ pub(crate) fn storage_device_constraints<'a, P: Copy>(
lv.is_cast_list_commitment_tape
* (lv.op1_value - i64::from(ecall::CAST_LIST_COMMITMENT_TAPE)),
);
cb.always(lv.is_self_prog_id_tape * (lv.op1_value - i64::from(ecall::SELF_PROG_ID_TAPE)));
}

pub(crate) fn poseidon2_constraints<'a, P: Copy>(
Expand Down
4 changes: 4 additions & 0 deletions circuits/src/generation/cpu.rs
Original file line number Diff line number Diff line change
Expand Up @@ -104,6 +104,10 @@ pub fn generate_cpu_trace<F: RichField>(record: &ExecutionRecord<F>) -> Vec<CpuS
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreCastListCommitmentTape)
)),
is_self_prog_id_tape: F::from_bool(matches!(
(inst.op, io.op),
(Op::ECALL, StorageDeviceOpcode::StoreSelfProgIdTape)
)),
is_halt: F::from_bool(matches!(
(inst.op, state.registers[usize::from(REG_A0)]),
(Op::ECALL, ecall::HALT)
Expand Down
4 changes: 3 additions & 1 deletion circuits/src/generation/fullword_memory.rs
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ mod tests {
use crate::generation::storage_device::{
generate_call_tape_trace, generate_cast_list_commitment_tape_trace,
generate_event_tape_trace, generate_events_commitment_tape_trace,
generate_private_tape_trace, generate_public_tape_trace,
generate_private_tape_trace, generate_public_tape_trace, generate_self_prog_id_tape_trace,
};
use crate::poseidon2_output_bytes::generation::generate_poseidon2_output_bytes_trace;
use crate::poseidon2_sponge::generation::generate_poseidon2_sponge_trace;
Expand Down Expand Up @@ -179,6 +179,7 @@ mod tests {
let events_commitment_tape_rows = generate_events_commitment_tape_trace(&record.executed);
let cast_list_commitment_tape_rows =
generate_cast_list_commitment_tape_trace(&record.executed);
let self_prog_id_tape_rows = generate_self_prog_id_tape_trace(&record.executed);
let poseidon2_rows = generate_poseidon2_sponge_trace(&record.executed);
let poseidon2_output_bytes = generate_poseidon2_output_bytes_trace(&poseidon2_rows);
let trace = generate_memory_trace::<GoldilocksField>(
Expand All @@ -193,6 +194,7 @@ mod tests {
&event_tape_rows,
&events_commitment_tape_rows,
&cast_list_commitment_tape_rows,
&self_prog_id_tape_rows,
&poseidon2_rows,
&poseidon2_output_bytes,
);
Expand Down
4 changes: 3 additions & 1 deletion circuits/src/generation/halfword_memory.rs
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ mod tests {
use crate::generation::storage_device::{
generate_call_tape_trace, generate_cast_list_commitment_tape_trace,
generate_event_tape_trace, generate_events_commitment_tape_trace,
generate_private_tape_trace, generate_public_tape_trace,
generate_private_tape_trace, generate_public_tape_trace, generate_self_prog_id_tape_trace,
};
use crate::poseidon2_sponge::generation::generate_poseidon2_sponge_trace;
use crate::test_utils::prep_table;
Expand Down Expand Up @@ -170,6 +170,7 @@ mod tests {
let events_commitment_tape_rows = generate_events_commitment_tape_trace(&record.executed);
let cast_list_commitment_tape_rows =
generate_cast_list_commitment_tape_trace(&record.executed);
let self_prog_id_tape_rows = generate_self_prog_id_tape_trace(&record.executed);
let poseidon2_sponge_rows = generate_poseidon2_sponge_trace(&record.executed);
let poseidon2_output_bytes = generate_poseidon2_output_bytes_trace(&poseidon2_sponge_rows);

Expand All @@ -185,6 +186,7 @@ mod tests {
&event_tape_rows,
&events_commitment_tape_rows,
&cast_list_commitment_tape_rows,
&self_prog_id_tape_rows,
&poseidon2_sponge_rows,
&poseidon2_output_bytes,
);
Expand Down
8 changes: 7 additions & 1 deletion circuits/src/generation/memory.rs
Original file line number Diff line number Diff line change
Expand Up @@ -160,6 +160,7 @@ pub fn generate_memory_trace<F: RichField>(
event_tape_rows: &[StorageDevice<F>],
events_commitment_tape_rows: &[StorageDevice<F>],
castlist_commitment_tape_rows: &[StorageDevice<F>],
self_prog_id_tape_rows: &[StorageDevice<F>],
poseidon2_sponge_rows: &[Poseidon2Sponge<F>],
poseidon2_output_bytes_rows: &[Poseidon2OutputBytes<F>],
) -> Vec<Memory<F>> {
Expand All @@ -178,6 +179,7 @@ pub fn generate_memory_trace<F: RichField>(
transform_storage(event_tape_rows),
transform_storage(events_commitment_tape_rows),
transform_storage(castlist_commitment_tape_rows),
transform_storage(self_prog_id_tape_rows),
transform_poseidon2_sponge(poseidon2_sponge_rows),
transform_poseidon2_output_bytes(poseidon2_output_bytes_rows,),
)
Expand Down Expand Up @@ -220,7 +222,7 @@ mod tests {
use crate::generation::storage_device::{
generate_call_tape_trace, generate_cast_list_commitment_tape_trace,
generate_event_tape_trace, generate_events_commitment_tape_trace,
generate_private_tape_trace, generate_public_tape_trace,
generate_private_tape_trace, generate_public_tape_trace, generate_self_prog_id_tape_trace,
};
use crate::memory::columns::Memory;
use crate::memory::stark::MemoryStark;
Expand Down Expand Up @@ -288,6 +290,7 @@ mod tests {
let event_tape_rows = generate_event_tape_trace(&record.executed);
let events_commitment_tape_rows = generate_events_commitment_tape_trace(&record.executed);
let cast_list_commitment_tape_rows = generate_cast_list_commitment_tape_trace(&record.executed);
let self_prog_id_tape_rows = generate_self_prog_id_tape_trace(&record.executed);
let poseidon2_sponge_trace = generate_poseidon2_sponge_trace(&record.executed);
let poseidon2_output_bytes = generate_poseidon2_output_bytes_trace(&poseidon2_sponge_trace);

Expand All @@ -303,6 +306,7 @@ mod tests {
&event_tape_rows,
&events_commitment_tape_rows,
&cast_list_commitment_tape_rows,
&self_prog_id_tape_rows,
&poseidon2_sponge_trace,
&poseidon2_output_bytes,
);
Expand Down Expand Up @@ -378,6 +382,7 @@ mod tests {
let events_commitment_tape_rows = generate_events_commitment_tape_trace(&[]);
let cast_list_commitment_tape_rows =
generate_cast_list_commitment_tape_trace(&[]);
let self_prog_id_tape_rows = generate_self_prog_id_tape_trace(&[]);
let poseidon2_trace = generate_poseidon2_sponge_trace(&[]);
let poseidon2_output_bytes = generate_poseidon2_output_bytes_trace(&poseidon2_trace);
let trace = super::generate_memory_trace::<F>(
Expand All @@ -392,6 +397,7 @@ mod tests {
&event_tape_rows,
&events_commitment_tape_rows,
&cast_list_commitment_tape_rows,
&self_prog_id_tape_rows,
&poseidon2_trace,
&poseidon2_output_bytes,
);
Expand Down
100 changes: 0 additions & 100 deletions circuits/src/generation/memoryinit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,6 @@ use crate::utils::pad_trace_with_default;
pub fn generate_memory_init_trace<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
let mut memory_inits: Vec<MemoryInit<F>> = chain! {
elf_memory_init(program),
mozak_memory_init(program),
call_tape_init(program),
private_tape_init(program),
public_tape_init(program),
event_tape_init(program),
}
.collect();

Expand All @@ -37,101 +32,6 @@ where
pad_trace_with_default(memory_inits)
}

/// Generates a mozak memory init ROM trace
#[must_use]
pub fn generate_mozak_memory_init_trace<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
let trace = generate_init_trace(program, mozak_memory_init);
log::trace!("MozakMemoryInit trace {:?}", trace);
trace
}

#[must_use]
pub fn mozak_memory_init<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
program
.mozak_ro_memory
.iter()
.flat_map(|mozak_ro_memory| {
chain! {
mozak_ro_memory.self_prog_id.data.clone(),
mozak_ro_memory.cast_list.data.clone(),
}
})
.map(MemoryInit::new_readonly)
.collect_vec()
}

#[must_use]
pub fn call_tape_init<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
program
.mozak_ro_memory
.iter()
.flat_map(|mozak_ro_memory| mozak_ro_memory.call_tape.data.clone())
.map(MemoryInit::new_readonly)
.collect_vec()
}

/// Generates a call tape memory init ROM trace
#[must_use]
pub fn generate_call_tape_init_trace<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
let trace = generate_init_trace(program, call_tape_init);
log::trace!("CallTapeInit trace {:?}", trace);
trace
}

#[must_use]
pub fn private_tape_init<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
program
.mozak_ro_memory
.iter()
.flat_map(|mozak_ro_memory| mozak_ro_memory.private_tape.data.clone())
.map(MemoryInit::new_readonly)
.collect_vec()
}

/// Generates a private tape memory init ROM trace
#[must_use]
pub fn generate_private_tape_init_trace<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
let trace = generate_init_trace(program, private_tape_init);
log::trace!("PrivateTapeInit trace {:?}", trace);
trace
}

#[must_use]
pub fn public_tape_init<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
program
.mozak_ro_memory
.iter()
.flat_map(|mozak_ro_memory| mozak_ro_memory.public_tape.data.clone())
.map(MemoryInit::new_readonly)
.collect_vec()
}

/// Generates a public tape memory init ROM trace
#[must_use]
pub fn generate_public_tape_init_trace<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
let trace = generate_init_trace(program, public_tape_init);
log::trace!("PublicTapeInit trace {:?}", trace);
trace
}

#[must_use]
pub fn event_tape_init<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
program
.mozak_ro_memory
.iter()
.flat_map(|mozak_ro_memory| mozak_ro_memory.event_tape.data.clone())
.map(MemoryInit::new_readonly)
.collect_vec()
}

/// Generates a event tape memory init ROM trace
#[must_use]
pub fn generate_event_tape_init_trace<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
let trace = generate_init_trace(program, event_tape_init);
log::trace!("EventTapeInit trace {:?}", trace);
trace
}

#[must_use]
pub fn elf_memory_init<F: RichField>(program: &Program) -> Vec<MemoryInit<F>> {
[(F::ZERO, &program.ro_memory), (F::ONE, &program.rw_memory)]
Expand Down
27 changes: 8 additions & 19 deletions circuits/src/generation/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -32,21 +32,16 @@ use self::cpu::{generate_cpu_trace, generate_program_mult_trace};
use self::fullword_memory::generate_fullword_memory_trace;
use self::halfword_memory::generate_halfword_memory_trace;
use self::memory::generate_memory_trace;
use self::memoryinit::{
generate_call_tape_init_trace, generate_event_tape_init_trace, generate_memory_init_trace,
generate_private_tape_init_trace, generate_public_tape_init_trace,
};
use self::memoryinit::generate_memory_init_trace;
use self::storage_device::{
generate_call_tape_trace, generate_cast_list_commitment_tape_trace, generate_event_tape_trace,
generate_events_commitment_tape_trace,
generate_events_commitment_tape_trace, generate_private_tape_trace, generate_public_tape_trace,
generate_self_prog_id_tape_trace,
};
use self::xor::generate_xor_trace;
use crate::columns_view::HasNamedColumns;
use crate::generation::memory_zeroinit::generate_memory_zero_init_trace;
use crate::generation::memoryinit::{
generate_elf_memory_init_trace, generate_mozak_memory_init_trace,
};
use crate::generation::storage_device::{generate_private_tape_trace, generate_public_tape_trace};
use crate::generation::memoryinit::generate_elf_memory_init_trace;
use crate::poseidon2::generation::generate_poseidon2_trace;
use crate::poseidon2_output_bytes::generation::generate_poseidon2_output_bytes_trace;
use crate::poseidon2_sponge::generation::generate_poseidon2_sponge_trace;
Expand Down Expand Up @@ -82,11 +77,6 @@ pub fn generate_traces<F: RichField + Extendable<D>, const D: usize>(

let memory_init = generate_memory_init_trace(program);
let elf_memory_init_rows = generate_elf_memory_init_trace(program);
let mozak_memory_init_rows = generate_mozak_memory_init_trace(program);
let call_tape_init_rows = generate_call_tape_init_trace(program);
let private_tape_init_rows = generate_private_tape_init_trace(program);
let public_tape_init_rows = generate_public_tape_init_trace(program);
let event_tape_init_rows = generate_event_tape_init_trace(program);

let memory_zeroinit_rows = generate_memory_zero_init_trace(&record.executed, program);

Expand All @@ -98,6 +88,7 @@ pub fn generate_traces<F: RichField + Extendable<D>, const D: usize>(
let event_tape_rows = generate_event_tape_trace(&record.executed);
let events_commitment_tape_rows = generate_events_commitment_tape_trace(&record.executed);
let cast_list_commitment_tape_rows = generate_cast_list_commitment_tape_trace(&record.executed);
let self_prog_id_tape_rows = generate_self_prog_id_tape_trace(&record.executed);
let poseiden2_sponge_rows = generate_poseidon2_sponge_trace(&record.executed);
let poseidon2_output_bytes_rows = generate_poseidon2_output_bytes_trace(&poseiden2_sponge_rows);
let poseidon2_rows = generate_poseidon2_trace(&record.executed);
Expand All @@ -114,6 +105,7 @@ pub fn generate_traces<F: RichField + Extendable<D>, const D: usize>(
&event_tape_rows,
&events_commitment_tape_rows,
&cast_list_commitment_tape_rows,
&self_prog_id_tape_rows,
&poseiden2_sponge_rows,
&poseidon2_output_bytes_rows,
);
Expand All @@ -129,6 +121,7 @@ pub fn generate_traces<F: RichField + Extendable<D>, const D: usize>(
&event_tape_rows,
&events_commitment_tape_rows,
&cast_list_commitment_tape_rows,
&self_prog_id_tape_rows,
&register_init_rows,
);
// Generate rows for the looking values with their multiplicities.
Expand All @@ -147,11 +140,6 @@ pub fn generate_traces<F: RichField + Extendable<D>, const D: usize>(
program_mult_stark: trace_rows_to_poly_values(program_mult_rows),
memory_stark: trace_rows_to_poly_values(memory_rows),
elf_memory_init_stark: trace_rows_to_poly_values(elf_memory_init_rows),
mozak_memory_init_stark: trace_rows_to_poly_values(mozak_memory_init_rows),
call_tape_init_stark: trace_rows_to_poly_values(call_tape_init_rows),
private_tape_init_stark: trace_rows_to_poly_values(private_tape_init_rows),
public_tape_init_stark: trace_rows_to_poly_values(public_tape_init_rows),
event_tape_init_stark: trace_rows_to_poly_values(event_tape_init_rows),
memory_zeroinit_stark: trace_rows_to_poly_values(memory_zeroinit_rows),
rangecheck_u8_stark: trace_rows_to_poly_values(rangecheck_u8_rows),
halfword_memory_stark: trace_rows_to_poly_values(halfword_memory_rows),
Expand All @@ -162,6 +150,7 @@ pub fn generate_traces<F: RichField + Extendable<D>, const D: usize>(
event_tape_stark: trace_rows_to_poly_values(event_tape_rows),
events_commitment_tape_stark: trace_rows_to_poly_values(events_commitment_tape_rows),
cast_list_commitment_tape_stark: trace_rows_to_poly_values(cast_list_commitment_tape_rows),
self_prog_id_tape_stark: trace_rows_to_poly_values(self_prog_id_tape_rows),
register_init_stark: trace_rows_to_poly_values(register_init_rows),
register_stark: trace_rows_to_poly_values(register_rows),
register_zero_read_stark: trace_rows_to_poly_values(register_zero_read_rows),
Expand Down
8 changes: 8 additions & 0 deletions circuits/src/generation/storage_device.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ fn is_storage_device_opcode<F: RichField>(op: StorageDeviceOpcode) -> F {
| StorageDeviceOpcode::StoreEventTape
| StorageDeviceOpcode::StoreEventsCommitmentTape
| StorageDeviceOpcode::StoreCastListCommitmentTape
| StorageDeviceOpcode::StoreSelfProgIdTape
))
}

Expand Down Expand Up @@ -119,3 +120,10 @@ pub fn generate_cast_list_commitment_tape_trace<F: RichField>(
) -> Vec<StorageDevice<F>> {
generate_storage_trace(step_rows, StorageDeviceOpcode::StoreCastListCommitmentTape)
}

#[must_use]
pub fn generate_self_prog_id_tape_trace<F: RichField>(
step_rows: &[Row<F>],
) -> Vec<StorageDevice<F>> {
generate_storage_trace(step_rows, StorageDeviceOpcode::StoreSelfProgIdTape)
}
Loading

0 comments on commit e5007e9

Please sign in to comment.