From ae4b90f4131fc78f8ebe8845f4a9a7147ad23d70 Mon Sep 17 00:00:00 2001 From: Morgan Thomas Date: Mon, 1 Apr 2024 13:56:48 -0400 Subject: [PATCH] wip: static data chip: making the constraints pass --- cpu/src/lib.rs | 3 ++- memory/src/columns.rs | 3 +++ memory/src/lib.rs | 18 ++++++++++++------ static_data/src/lib.rs | 4 +++- 4 files changed, 20 insertions(+), 8 deletions(-) diff --git a/cpu/src/lib.rs b/cpu/src/lib.rs index 077918df..cbbcd892 100644 --- a/cpu/src/lib.rs +++ b/cpu/src/lib.rs @@ -96,9 +96,10 @@ where let is_read = VirtualPairCol::single_main(channel.is_read); let clk = VirtualPairCol::single_main(CPU_COL_MAP.clk); let addr = VirtualPairCol::single_main(channel.addr); + let is_static_initial = VirtualPairCol::constant(SC::Val::zero()); let value = channel.value.0.map(VirtualPairCol::single_main); - let mut fields = vec![is_read, clk, addr]; + let mut fields = vec![is_read, clk, addr, is_static_initial]; fields.extend(value); Interaction { diff --git a/memory/src/columns.rs b/memory/src/columns.rs index 73ef6f4d..cc3d2e8b 100644 --- a/memory/src/columns.rs +++ b/memory/src/columns.rs @@ -15,6 +15,9 @@ pub struct MemoryCols { /// Main CPU clock cycle pub clk: T, + /// Flag indicating if this is an initial static data value or not + pub is_static_initial: T, + /// Whether memory operation is a read pub is_read: T, diff --git a/memory/src/lib.rs b/memory/src/lib.rs index 8269e226..effbb888 100644 --- a/memory/src/lib.rs +++ b/memory/src/lib.rs @@ -129,13 +129,16 @@ where let mut rows = self.static_data .iter() - .map(|(addr, value)| self.static_data_to_row(*addr, *value)) + .enumerate() + .map(|(n, (addr, value))| self.static_data_to_row(n, *addr, *value)) .collect::>(); + let n0 = rows.len(); + let ops_rows = ops .par_iter() .enumerate() - .map(|(n, (clk, op))| self.op_to_row(n, *clk as usize, *op)) + .map(|(n, (clk, op))| self.op_to_row(n0+n, *clk as usize, *op)) .collect::>(); rows.extend(ops_rows); @@ -172,12 +175,14 @@ where } fn global_receives(&self, machine: &M) -> Vec> { + // return vec![]; // TODO let is_read: VirtualPairCol = VirtualPairCol::single_main(MEM_COL_MAP.is_read); let clk = VirtualPairCol::single_main(MEM_COL_MAP.clk); let addr = VirtualPairCol::single_main(MEM_COL_MAP.addr); + let is_static_initial = VirtualPairCol::single_main(MEM_COL_MAP.is_static_initial); let value = MEM_COL_MAP.value.0.map(VirtualPairCol::single_main); - let mut fields = vec![is_read, clk, addr]; + let mut fields = vec![is_read, clk, addr, is_static_initial]; fields.extend(value); let is_real = VirtualPairCol::sum_main(vec![MEM_COL_MAP.is_read, MEM_COL_MAP.is_write]); @@ -197,6 +202,7 @@ impl MemoryChip { cols.clk = F::from_canonical_usize(clk); cols.counter = F::from_canonical_usize(n); + cols.is_static_initial = F::zero(); match op { Operation::Read(addr, value) => { @@ -218,12 +224,12 @@ impl MemoryChip { row } - fn static_data_to_row(&self, addr: u32, value: Word) -> [F; NUM_MEM_COLS] { + fn static_data_to_row(&self, n: usize, addr: u32, value: Word) -> [F; NUM_MEM_COLS] { let mut row = [F::zero(); NUM_MEM_COLS]; let cols: &mut MemoryCols = unsafe { transmute(&mut row) }; - // TODO: maybe an is_static_data column? + cols.is_static_initial = F::one(); cols.clk = F::zero(); - cols.counter = F::zero(); + cols.counter = F::from_canonical_usize(n); cols.addr = F::from_canonical_u32(addr); cols.value = value.transform(F::from_canonical_u8); cols.is_write = F::one(); diff --git a/static_data/src/lib.rs b/static_data/src/lib.rs index e31b51c9..81eb39c5 100644 --- a/static_data/src/lib.rs +++ b/static_data/src/lib.rs @@ -66,12 +66,14 @@ where } fn global_sends(&self, machine: &M) -> Vec> { + // return vec![]; // TODO let addr = VirtualPairCol::single_main(STATIC_DATA_COL_MAP.addr); let value = STATIC_DATA_COL_MAP.value.0.map(VirtualPairCol::single_main); let is_read = VirtualPairCol::constant(SC::Val::zero()); let is_real = VirtualPairCol::single_main(STATIC_DATA_COL_MAP.is_real); + let is_static_initial = VirtualPairCol::constant(SC::Val::one()); let clk = VirtualPairCol::constant(SC::Val::zero()); - let mut fields = vec![is_read, clk, addr]; + let mut fields = vec![is_read, clk, addr, is_static_initial]; fields.extend(value); let send = Interaction { fields,