diff --git a/emulator/src/emu.rs b/emulator/src/emu.rs index b81a61d0..1c47d8ce 100644 --- a/emulator/src/emu.rs +++ b/emulator/src/emu.rs @@ -617,16 +617,21 @@ impl<'a> Emu<'a> { a_src_imm: F::from_bool(instruction.a_src == SRC_IMM), a_src_mem: F::from_bool(instruction.a_src == SRC_MEM), a_offset_imm0: F::from_canonical_u64(instruction.a_offset_imm0), + #[cfg(not(feature = "sp"))] + a_imm1: F::from_canonical_u64(instruction.a_use_sp_imm1), + #[cfg(feature = "sp")] sp: F::from_canonical_u64(self.ctx.inst_ctx.sp), #[cfg(feature = "sp")] a_src_sp: F::from_bool(instruction.a_src == SRC_SP), - #[cfg(not(feature = "sp"))] - a_src_sp: F::from_bool(false), + #[cfg(feature = "sp")] a_use_sp_imm1: F::from_canonical_u64(instruction.a_use_sp_imm1), a_src_step: F::from_bool(instruction.a_src == SRC_STEP), b_src_imm: F::from_bool(instruction.b_src == SRC_IMM), b_src_mem: F::from_bool(instruction.b_src == SRC_MEM), b_offset_imm0: F::from_canonical_u64(instruction.b_offset_imm0), + #[cfg(not(feature = "sp"))] + b_imm1: F::from_canonical_u64(instruction.a_use_sp_imm1), + #[cfg(feature = "sp")] b_use_sp_imm1: F::from_canonical_u64(instruction.b_use_sp_imm1), b_src_ind: F::from_bool(instruction.b_src == SRC_IND), ind_width: F::from_canonical_u64(instruction.ind_width), @@ -637,15 +642,12 @@ impl<'a> Emu<'a> { store_ind: F::from_bool(instruction.store == STORE_IND), store_offset: F::from_canonical_u64(instruction.store_offset as u64), set_pc: F::from_bool(instruction.set_pc), + #[cfg(feature = "sp")] store_use_sp: F::from_bool(instruction.store_use_sp), #[cfg(feature = "sp")] set_sp: F::from_bool(instruction.set_sp), - #[cfg(not(feature = "sp"))] - set_sp: F::from_bool(false), #[cfg(feature = "sp")] inc_sp: F::from_canonical_u64(instruction.inc_sp), - #[cfg(not(feature = "sp"))] - inc_sp: F::from_bool(false), jmp_offset1: F::from_canonical_u64(instruction.jmp_offset1 as u64), jmp_offset2: F::from_canonical_u64(instruction.jmp_offset2 as u64), main_segment: F::from_canonical_u64(0), diff --git a/pil/v0.1/src/pil_helpers/pilout.rs b/pil/v0.1/src/pil_helpers/pilout.rs index 69d8ad1c..8edeec19 100644 --- a/pil/v0.1/src/pil_helpers/pilout.rs +++ b/pil/v0.1/src/pil_helpers/pilout.rs @@ -32,21 +32,26 @@ pub struct Pilout; impl Pilout { pub fn pilout() -> WitnessPilout { - let mut pilout = WitnessPilout::new("Zisk", 1, PILOUT_HASH.to_vec()); + let mut pilout = WitnessPilout::new("Zisk", 2, PILOUT_HASH.to_vec()); let air_group = pilout.add_air_group(Some("Main")); + air_group.add_air(Some("Main"), 2097152); let air_group = pilout.add_air_group(Some("Binary")); + air_group.add_air(Some("Binary"), 2097152); let air_group = pilout.add_air_group(Some("BinaryTable")); + air_group.add_air(Some("BinaryTable"), 8388608); let air_group = pilout.add_air_group(Some("BinaryExtension")); + air_group.add_air(Some("BinaryExtension"), 2097152); let air_group = pilout.add_air_group(Some("BinaryExtensionTable")); + air_group.add_air(Some("BinaryExtensionTable"), 524288); pilout diff --git a/pil/v0.1/src/pil_helpers/traces.rs b/pil/v0.1/src/pil_helpers/traces.rs index a1dd2dc9..e532557d 100644 --- a/pil/v0.1/src/pil_helpers/traces.rs +++ b/pil/v0.1/src/pil_helpers/traces.rs @@ -4,7 +4,7 @@ use proofman_common as common; pub use proofman_macros::trace; trace!(Main0Row, Main0Trace { - main_first_segment: F, main_last_segment: F, main_segment: F, a: [F; 2], b: [F; 2], c: [F; 2], last_c: [F; 2], flag: F, pc: F, a_src_imm: F, a_src_mem: F, a_offset_imm0: F, sp: F, a_src_sp: F, a_use_sp_imm1: F, a_src_step: F, b_src_imm: F, b_src_mem: F, b_offset_imm0: F, b_use_sp_imm1: F, b_src_ind: F, ind_width: F, is_external_op: F, op: F, store_ra: F, store_mem: F, store_ind: F, store_offset: F, set_pc: F, store_use_sp: F, set_sp: F, inc_sp: F, jmp_offset1: F, jmp_offset2: F, end: F, m32: F, + main_first_segment: F, main_last_segment: F, main_segment: F, a: [F; 2], b: [F; 2], c: [F; 2], last_c: [F; 2], flag: F, pc: F, a_src_imm: F, a_src_mem: F, a_offset_imm0: F, a_imm1: F, a_src_step: F, b_src_imm: F, b_src_mem: F, b_offset_imm0: F, b_imm1: F, b_src_ind: F, ind_width: F, is_external_op: F, op: F, store_ra: F, store_mem: F, store_ind: F, store_offset: F, set_pc: F, jmp_offset1: F, jmp_offset2: F, end: F, m32: F, }); trace!(Binary0Row, Binary0Trace { diff --git a/state-machines/main/pil/main.pil b/state-machines/main/pil/main.pil index b8de1118..7941c6d1 100644 --- a/state-machines/main/pil/main.pil +++ b/state-machines/main/pil/main.pil @@ -5,7 +5,7 @@ const int BOOT_ADDR = 0x1000; -airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 1, const int operation_bus_id, int MAIN_CONTINUATION_ID = 1000) { +airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 0, const int operation_bus_id, int MAIN_CONTINUATION_ID = 1000) { col fixed SEGMENT_L1 = [1,0...]; col fixed SEGMENT_STEP = [0..(N-1)]; @@ -45,6 +45,14 @@ airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 1, const int ope // Instruction + // a_src_step + // a_src_mem + // a_src_imm + // a_src_sp + // b_src_mem + // b_src_imm + // b_src_ind + // Source A col witness a_src_imm; // Selector @@ -55,10 +63,10 @@ airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 1, const int ope col witness air.sp; col witness air.a_src_sp; col witness air.a_use_sp_imm1; - col witness air.a_src_step; } else { - col witness air.a_src_step_imm1; + col witness air.a_imm1; } + col witness a_src_step; // Source B @@ -68,11 +76,10 @@ airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 1, const int ope if (stack_enabled) { col witness air.b_use_sp_imm1; - col witness air.b_src_ind; } else { - col witness air.b_src_ind_imm1; + col witness air.b_imm1; } - + col witness b_src_ind; col witness ind_width; // 8 , 4, 2, 1 // Operations related @@ -112,15 +119,14 @@ airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 1, const int ope const expr sel_mem_b; const expr addr[3]; + sel_mem_b = b_src_mem + b_src_ind; if (stack_enabled) { - sel_mem_b = b_src_mem + b_src_ind; addr[0] = a_offset_imm0 + a_use_sp_imm1 * sp; addr[1] = b_offset_imm0 + b_src_ind * (a[0] + 2**32 * a[1]) + b_use_sp_imm1 * sp; addr[2] = store_offset + store_ind * a[0] + store_use_sp * sp; } else { - sel_mem_b = b_src_mem + b_src_ind_imm1; addr[0] = a_offset_imm0; - addr[1] = b_offset_imm0 + b_src_ind_imm1 * (a[0] + 2**32 * a[1]); + addr[1] = b_offset_imm0 + b_src_ind * (a[0] + 2**32 * a[1]); addr[2] = store_offset + store_ind * a[0]; } @@ -163,28 +169,23 @@ airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 1, const int ope a_imm[1] = a_use_sp_imm1; b_imm[1] = b_use_sp_imm1; } else { - a_src_c = 1 - a_src_step_imm1 - a_src_mem - a_src_imm; - b_src_c = 1 - b_src_mem - b_src_imm - b_src_ind_imm1; - a_imm[1] = a_src_step_imm1; - b_imm[1] = b_src_ind_imm1; + a_src_c = 1 - a_src_step - a_src_mem - a_src_imm; + b_src_c = 1 - b_src_mem - b_src_imm - b_src_ind; + a_imm[1] = a_imm1; + b_imm[1] = b_imm1; } for (int index = 0; index < RC; ++index) { if (stack_enabled) { // a_src_sp ===> set a = sp (only less significant index, rest must be 0) - a_src_sp*(a[index] - (index == 0 ? sp: 0 )) === 0; - - // a_src_step ===> set a = STEP (only less significant index, rest must be 0) - a_src_step *( a[index] - (index == 0 ? STEP : 0)) === 0; - } else { - a_src_step_imm1 *( a[index] - (index == 0 ? STEP : 0)) === 0; + a_src_sp * (a[index] - (index == 0 ? sp: 0 )) === 0; } + a_src_step * (a[index] - (index == 0 ? STEP : 0)) === 0; + a_src_c * (a[index] - last_c[index]) === 0; + b_src_c * (b[index] - last_c[index]) === 0; - a_src_c*(a[index] - last_c[index]) === 0; - b_src_c*(b[index] - last_c[index]) === 0; - - a_src_imm*(a[index] - a_imm[index]) === 0; - b_src_imm*(b[index] - b_imm[index]) === 0; + a_src_imm * (a[index] - a_imm[index]) === 0; + b_src_imm * (b[index] - b_imm[index]) === 0; // continuations_transition(last_c[index], c[index]); // last_c[index]' = c[index]; @@ -234,6 +235,7 @@ airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 1, const int ope flag * (1 - flag) === 0; + /* if (stack_enabled) { const expr rom_flags = a_src_imm + 2 * a_src_mem + 4 * b_src_imm + 8 * b_src_mem + 16 * store_ra + 32 * store_mem + 64 * store_ind + 128 * set_pc + 256 * m32 + 512 * end + 1024 * is_external_op + 2**11 * a_src_sp + 2**12 * a_use_sp_imm1 + 2**13 * a_src_step + 2**14 * b_src_ind + 2**15 * store_use_sp; @@ -242,4 +244,5 @@ airtemplate Main(int N = 2**21, int RC = 2, int stack_enabled = 1, const int ope const expr rom_flags = a_src_imm + 2 * a_src_mem + 4 * b_src_imm + 8 * b_src_mem + 16 * store_ra + 32 * store_mem + 64 * store_ind + 128 * set_pc + 256 * m32 + 512 * end + 1024 * is_external_op; // lookup_assumes(ROM_ID, cols: [pc, rom_flags, op, a_offset_imm0, b_offset_imm0, ind_width, store_offset, jmp_offset1, jmp_offset2, a_src_step_imm1, b_src_ind_imm1]); } + */ } \ No newline at end of file