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.

Sign up for GitHub

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

chore(core): ALU tables verifies pc control flow #1808

Closed
wants to merge 20 commits into from
+620 −815
Closed

chore(core): ALU tables verifies pc control flow #1808

Show file tree
Hide file tree
Changes from 17 commits
Commits
Show all changes
20 commits
Select commit Hold shift + click to select a range
3bb111b
dummy columns
kevjue Nov 20, 2024
bc34538
checkpoint
kevjue Nov 21, 2024
50acb86
changes for the executor
kevjue Nov 21, 2024
692f3be
got shard from public values
kevjue Nov 21, 2024
01b996b
remove shard
kevjue Nov 21, 2024
e0e5836
added a comment
kevjue Nov 21, 2024
9c43f66
Revert "dummy columns"
kevjue Nov 21, 2024
f50ccc1
fixed types
kevjue Nov 21, 2024
e559b4c
reverted memory table
kevjue Nov 21, 2024
836fc88
removed shard
kevjue Nov 22, 2024
63bd940
merged dev
kevjue Nov 22, 2024
c55fe19
changes
kevjue Nov 22, 2024
1bf08ac
put back shard column into cpu table
kevjue Nov 22, 2024
617d962
fix
kevjue Nov 22, 2024
84deca2
fix
kevjue Nov 22, 2024
8681a56
revert p3 dependencies
kevjue Nov 22, 2024
5d6f56c
finishing touches
kevjue Nov 22, 2024
a2268a5
Update crates/core/machine/src/alu/add_sub/mod.rs
kevjue Nov 22, 2024
cc2b9db
more intuitive code
kevjue Nov 22, 2024
73f3abc
fixed conflict
kevjue Nov 22, 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
36 changes: 18 additions & 18 deletions Cargo.lock
View file
Open in desktop

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

78 changes: 31 additions & 47 deletions crates/core/executor/src/dependencies.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,13 +1,12 @@
use crate::{
events::AluEvent,
events::InstrEvent,
utils::{get_msb, get_quotient_and_remainder, is_signed_operation},
Executor, Opcode,
Executor, Opcode, UNUSED_PC,
};

/// Emits the dependencies for division and remainder operations.
#[allow(clippy::too_many_lines)]
pub fn emit_divrem_dependencies(executor: &mut Executor, event: AluEvent) {
let shard = executor.shard();
pub fn emit_divrem_dependencies(executor: &mut Executor, event: InstrEvent) {
let (quotient, remainder) = get_quotient_and_remainder(event.b, event.c, event.opcode);
let c_msb = get_msb(event.c);
let rem_msb = get_msb(remainder);
Expand All @@ -21,10 +20,9 @@ pub fn emit_divrem_dependencies(executor: &mut Executor, event: AluEvent) {

if c_neg == 1 {
let ids = executor.record.create_lookup_ids();
executor.record.add_events.push(AluEvent {
executor.record.add_events.push(InstrEvent {
pc: UNUSED_PC,
lookup_id: event.sub_lookups[4],
shard,
clk: event.clk,
opcode: Opcode::ADD,
a: 0,
b: event.c,
Expand All @@ -34,10 +32,9 @@ pub fn emit_divrem_dependencies(executor: &mut Executor, event: AluEvent) {
}
if rem_neg == 1 {
let ids = executor.record.create_lookup_ids();
executor.record.add_events.push(AluEvent {
executor.record.add_events.push(InstrEvent {
pc: UNUSED_PC,
lookup_id: event.sub_lookups[5],
shard,
clk: event.clk,
opcode: Opcode::ADD,
a: 0,
b: remainder,
Expand All @@ -56,10 +53,9 @@ pub fn emit_divrem_dependencies(executor: &mut Executor, event: AluEvent) {
let lower_word = u32::from_le_bytes(c_times_quotient[0..4].try_into().unwrap());
let upper_word = u32::from_le_bytes(c_times_quotient[4..8].try_into().unwrap());

let lower_multiplication = AluEvent {
let lower_multiplication = InstrEvent {
pc: UNUSED_PC,
lookup_id: event.sub_lookups[0],
shard,
clk: event.clk,
opcode: Opcode::MUL,
a: lower_word,
c: event.c,
Expand All @@ -68,10 +64,9 @@ pub fn emit_divrem_dependencies(executor: &mut Executor, event: AluEvent) {
};
executor.record.mul_events.push(lower_multiplication);

let upper_multiplication = AluEvent {
let upper_multiplication = InstrEvent {
pc: UNUSED_PC,
lookup_id: event.sub_lookups[1],
shard,
clk: event.clk,
opcode: {
if is_signed_operation {
Opcode::MULH
Expand All @@ -87,25 +82,23 @@ pub fn emit_divrem_dependencies(executor: &mut Executor, event: AluEvent) {
executor.record.mul_events.push(upper_multiplication);

let lt_event = if is_signed_operation {
AluEvent {
InstrEvent {
pc: UNUSED_PC,
lookup_id: event.sub_lookups[2],
shard,
opcode: Opcode::SLTU,
a: 1,
b: (remainder as i32).unsigned_abs(),
c: u32::max(1, (event.c as i32).unsigned_abs()),
clk: event.clk,
sub_lookups: executor.record.create_lookup_ids(),
}
} else {
AluEvent {
InstrEvent {
pc: UNUSED_PC,
lookup_id: event.sub_lookups[3],
shard,
opcode: Opcode::SLTU,
a: 1,
b: remainder,
c: u32::max(1, event.c),
clk: event.clk,
sub_lookups: executor.record.create_lookup_ids(),
}
};
Expand All @@ -119,7 +112,6 @@ pub fn emit_divrem_dependencies(executor: &mut Executor, event: AluEvent) {
#[allow(clippy::too_many_lines)]
pub fn emit_cpu_dependencies(executor: &mut Executor, index: usize) {
let event = executor.record.cpu_events[index];
let shard = executor.shard();
let instruction = &executor.program.fetch(event.pc);
if matches!(
instruction.opcode,
Expand All @@ -134,10 +126,9 @@ pub fn emit_cpu_dependencies(executor: &mut Executor, index: usize) {
) {
let memory_addr = event.b.wrapping_add(event.c);
// Add event to ALU check to check that addr == b + c
let add_event = AluEvent {
let add_event = InstrEvent {
pc: UNUSED_PC,
lookup_id: event.memory_add_lookup_id,
shard,
clk: event.clk,
opcode: Opcode::ADD,
a: memory_addr,
b: event.b,
Expand Down Expand Up @@ -169,10 +160,9 @@ pub fn emit_cpu_dependencies(executor: &mut Executor, index: usize) {
};

if most_sig_mem_value_byte >> 7 & 0x01 == 1 {
let sub_event = AluEvent {
let sub_event = InstrEvent {
pc: UNUSED_PC,
lookup_id: event.memory_sub_lookup_id,
shard,
clk: event.clk,
opcode: Opcode::SUB,
a: event.a,
b: unsigned_mem_val,
Expand Down Expand Up @@ -200,20 +190,18 @@ pub fn emit_cpu_dependencies(executor: &mut Executor, index: usize) {

let alu_op_code = if use_signed_comparison { Opcode::SLT } else { Opcode::SLTU };
// Add the ALU events for the comparisons
let lt_comp_event = AluEvent {
let lt_comp_event = InstrEvent {
pc: UNUSED_PC,
lookup_id: event.branch_lt_lookup_id,
shard,
clk: event.clk,
opcode: alu_op_code,
a: a_lt_b as u32,
b: event.a,
c: event.b,
sub_lookups: executor.record.create_lookup_ids(),
};
let gt_comp_event = AluEvent {
let gt_comp_event = InstrEvent {
pc: UNUSED_PC,
lookup_id: event.branch_gt_lookup_id,
shard,
clk: event.clk,
opcode: alu_op_code,
a: a_gt_b as u32,
b: event.b,
Expand All @@ -231,10 +219,9 @@ pub fn emit_cpu_dependencies(executor: &mut Executor, index: usize) {
};
if branching {
let next_pc = event.pc.wrapping_add(event.c);
let add_event = AluEvent {
let add_event = InstrEvent {
pc: UNUSED_PC,
lookup_id: event.branch_add_lookup_id,
shard,
clk: event.clk,
opcode: Opcode::ADD,
a: next_pc,
b: event.pc,
Expand All @@ -249,10 +236,9 @@ pub fn emit_cpu_dependencies(executor: &mut Executor, index: usize) {
match instruction.opcode {
Opcode::JAL => {
let next_pc = event.pc.wrapping_add(event.b);
let add_event = AluEvent {
let add_event = InstrEvent {
pc: UNUSED_PC,
lookup_id: event.jump_jal_lookup_id,
shard,
clk: event.clk,
opcode: Opcode::ADD,
a: next_pc,
b: event.pc,
Expand All @@ -263,10 +249,9 @@ pub fn emit_cpu_dependencies(executor: &mut Executor, index: usize) {
}
Opcode::JALR => {
let next_pc = event.b.wrapping_add(event.c);
let add_event = AluEvent {
let add_event = InstrEvent {
pc: UNUSED_PC,
lookup_id: event.jump_jalr_lookup_id,
shard,
clk: event.clk,
opcode: Opcode::ADD,
a: next_pc,
b: event.b,
Expand All @@ -280,10 +265,9 @@ pub fn emit_cpu_dependencies(executor: &mut Executor, index: usize) {
}

if matches!(instruction.opcode, Opcode::AUIPC) {
let add_event = AluEvent {
let add_event = InstrEvent {
pc: UNUSED_PC,
lookup_id: event.auipc_lookup_id,
shard,
clk: event.clk,
opcode: Opcode::ADD,
a: event.a,
b: event.pc,
Expand Down
Loading
Loading