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

Jump to bottom

Integrate new main.pil from zkronos with SP disabled #91

Closed
wants to merge 3 commits into from
Closed

Integrate new main.pil from zkronos with SP disabled #91

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
27a33dc
Integrate new main.pil from zkronos with SP disabled
fractasy Sep 23, 2024
5b14c2d
Fix wc cargo.toml
fractasy Sep 23, 2024
0ba3c1b
Fix a_imm1 and b_imm1 in Emu::step_slice()
fractasy Sep 23, 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
14 changes: 8 additions & 6 deletions emulator/src/emu.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -617,17 +617,22 @@
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),

Check failure on line 623 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Docker Risc Oficial Tests Check 

struct `Main0Row<F>` has no field named `sp`

Check failure on line 623 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Test on x86_64 

struct `Main0Row<F>` has no field named `sp`

Check failure on line 623 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Formatting & Clippy 

struct `zisk_pil::Main0Row<F>` has no field named `sp`
#[cfg(feature = "sp")]
a_src_sp: F::from_bool(instruction.a_src == SRC_SP),

Check failure on line 625 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Docker Risc Oficial Tests Check 

struct `Main0Row<F>` has no field named `a_src_sp`

Check failure on line 625 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Test on x86_64 

struct `Main0Row<F>` has no field named `a_src_sp`

Check failure on line 625 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Formatting & Clippy 

struct `zisk_pil::Main0Row<F>` has no field named `a_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),

Check failure on line 627 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Docker Risc Oficial Tests Check 

struct `Main0Row<F>` has no field named `a_use_sp_imm1`

Check failure on line 627 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Test on x86_64 

struct `Main0Row<F>` has no field named `a_use_sp_imm1`

Check failure on line 627 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Formatting & Clippy 

struct `zisk_pil::Main0Row<F>` has no field named `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),

Check failure on line 635 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Docker Risc Oficial Tests Check 

struct `Main0Row<F>` has no field named `b_use_sp_imm1`

Check failure on line 635 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Test on x86_64 

struct `Main0Row<F>` has no field named `b_use_sp_imm1`

Check failure on line 635 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Formatting & Clippy 

struct `zisk_pil::Main0Row<F>` has no field named `b_use_sp_imm1`
b_src_ind: F::from_bool(instruction.b_src == SRC_IND),
ind_width: F::from_canonical_u64(instruction.ind_width),
is_external_op: F::from_bool(instruction.is_external_op),
Expand All @@ -637,15 +642,12 @@
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),

Check failure on line 646 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Docker Risc Oficial Tests Check 

struct `Main0Row<F>` has no field named `store_use_sp`

Check failure on line 646 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Test on x86_64 

struct `Main0Row<F>` has no field named `store_use_sp`

Check failure on line 646 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Formatting & Clippy 

struct `zisk_pil::Main0Row<F>` has no field named `store_use_sp`
#[cfg(feature = "sp")]
set_sp: F::from_bool(instruction.set_sp),

Check failure on line 648 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Docker Risc Oficial Tests Check 

struct `Main0Row<F>` has no field named `set_sp`

Check failure on line 648 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Test on x86_64 

struct `Main0Row<F>` has no field named `set_sp`

Check failure on line 648 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Formatting & Clippy 

struct `zisk_pil::Main0Row<F>` has no field named `set_sp`
#[cfg(not(feature = "sp"))]
set_sp: F::from_bool(false),
#[cfg(feature = "sp")]
inc_sp: F::from_canonical_u64(instruction.inc_sp),

Check failure on line 650 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Docker Risc Oficial Tests Check 

struct `Main0Row<F>` has no field named `inc_sp`

Check failure on line 650 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Test on x86_64 

struct `Main0Row<F>` has no field named `inc_sp`

Check failure on line 650 in emulator/src/emu.rs

View workflow job for this annotation

GitHub Actions / Formatting & Clippy 

struct `zisk_pil::Main0Row<F>` has no field named `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),
Expand Down
7 changes: 6 additions & 1 deletion pil/v0.1/src/pil_helpers/pilout.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion pil/v0.1/src/pil_helpers/traces.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use proofman_common as common;
pub use proofman_macros::trace;

trace!(Main0Row, Main0Trace<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, 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<F> {
Expand Down
51 changes: 27 additions & 24 deletions state-machines/main/pil/main.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)];
Expand Down Expand Up @@ -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
Expand All @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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];
}

Expand Down Expand Up @@ -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];

Expand Down Expand Up @@ -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;
Expand All @@ -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]);
}
*/
}
Loading