diff --git a/arithmetization/Makefile b/arithmetization/Makefile index cb14585af5..bedefaca48 100644 --- a/arithmetization/Makefile +++ b/arithmetization/Makefile @@ -11,7 +11,7 @@ REPO_ROOT := $(abspath $(MAKEFILE_DIR)/..) ZKC ?= $(REPO_ROOT)/zkc ZKC_REPO ?= https://github.com/LFDT-Lineth/zkc.git # Optional: pin a commit or branch (e.g. 763f30878e5fc260f0d88863c9883c904f8fc056). Leave empty for default branch. -ZKC_REF ?= v1.2.29 +ZKC_REF ?= v1.2.30 # Used to install Sail for ACT4 host builds. ACT4_RISCV_DIR ?= $(HOME)/riscv diff --git a/arithmetization/src/main/lib/keccak/impl.zkc b/arithmetization/src/main/lib/keccak/impl.zkc index 0af099a13f..0797a0bde6 100644 --- a/arithmetization/src/main/lib/keccak/impl.zkc +++ b/arithmetization/src/main/lib/keccak/impl.zkc @@ -193,7 +193,7 @@ fn kec_theta() { for i_minus_one:u5 = 0; i_minus_one<5; i_minus_one = i_minus_one + 1 { var i:u5 = i_minus_one + 1 - keccak_state[D + (mod5(i) as u7)] = keccak_state[C + (i_minus_one as u7)] ^ bit_rotl64(keccak_state[C + (mod5(i + 1) as u7)], 1) + keccak_state[D + (mod5[i] as u7)] = keccak_state[C + (i_minus_one as u7)] ^ bit_rotl64(keccak_state[C + (mod5[i + 1] as u7)], 1) } for j:u7 = 0; j<5; j = j + 1 { @@ -211,11 +211,11 @@ fn kec_theta() { fn kec_rho() { for j:u3 = 0; j<5; j = j + 1 { - keccak_state[ROW0 + (j as u7)] = bit_rotl64(keccak_state[ROW0 + (j as u7)], rot_offset(0, j)) - keccak_state[ROW1 + (j as u7)] = bit_rotl64(keccak_state[ROW1 + (j as u7)], rot_offset(1, j)) - keccak_state[ROW2 + (j as u7)] = bit_rotl64(keccak_state[ROW2 + (j as u7)], rot_offset(2, j)) - keccak_state[ROW3 + (j as u7)] = bit_rotl64(keccak_state[ROW3 + (j as u7)], rot_offset(3, j)) - keccak_state[ROW4 + (j as u7)] = bit_rotl64(keccak_state[ROW4 + (j as u7)], rot_offset(4, j)) + keccak_state[ROW0 + (j as u7)] = bit_rotl64(keccak_state[ROW0 + (j as u7)], rot_offset[0, j]) + keccak_state[ROW1 + (j as u7)] = bit_rotl64(keccak_state[ROW1 + (j as u7)], rot_offset[1, j]) + keccak_state[ROW2 + (j as u7)] = bit_rotl64(keccak_state[ROW2 + (j as u7)], rot_offset[2, j]) + keccak_state[ROW3 + (j as u7)] = bit_rotl64(keccak_state[ROW3 + (j as u7)], rot_offset[3, j]) + keccak_state[ROW4 + (j as u7)] = bit_rotl64(keccak_state[ROW4 + (j as u7)], rot_offset[4, j]) } } diff --git a/arithmetization/src/main/riscv/interpreter.zkc b/arithmetization/src/main/riscv/interpreter.zkc index 3a294a4253..55242ac91f 100644 --- a/arithmetization/src/main/riscv/interpreter.zkc +++ b/arithmetization/src/main/riscv/interpreter.zkc @@ -188,9 +188,27 @@ include "../lib/io/write_output.zkc" // The tiers above list explicit semantic opcodes (`*_WB`, branches, stores, // precompiles, …); anything not matched there eventually reaches the // `interpreter_c` default and behaves as a no-op. -// -fn interpreter(index:u64, pc:Address, output_write_address:OutputAddress) -> (new_pc:Address, new_output_write_address:OutputAddress) { +fn interpreter(clk:u32, base:Address, pc:Address, output_write_address:OutputAddress) -> ! { + var new_output_write_address:OutputAddress + var new_pc:Address + var index:u62 + var rem:u2 + // determine index of predecoded program + index::rem = pc - base + // + printf "\n----------------------------------------------------------------- PC=%d, clock cycle: %d\n", pc, clk + // Execute current instruction + new_pc, new_output_write_address = interpreter_a(index as u64, pc, output_write_address) + // Check for termination + if new_pc != MAX_UINT_64 { + // Execute next instruction + interpreter!(clk + 1, base, new_pc, new_output_write_address) + } + // Termination + done +} +fn interpreter_a(index:u64, pc:Address, output_write_address:OutputAddress) -> (new_pc:Address, new_output_write_address:OutputAddress) { var compute_op:ComputeOp var imm:DoubleWord var rs1:Register diff --git a/arithmetization/src/main/riscv/main.zkc b/arithmetization/src/main/riscv/main.zkc index 4585673eb1..740f2d87b8 100644 --- a/arithmetization/src/main/riscv/main.zkc +++ b/arithmetization/src/main/riscv/main.zkc @@ -76,43 +76,6 @@ fn main() { // -- PREDECODING SECTION END-- // -- NO PREDECODING -- - main_loop(entry_point, base) + interpreter!(0, base, entry_point, 0) // -- NO PREDECODING END-- -} - -// -- PREDECODING SECTION -- -// fn main_loop(entry_point:u64, base:u64, exec_end:u64) { -// -- PREDECODING SECTION END-- - -// -- NO PREDECODING -- -fn main_loop(entry_point:u64, base:u64) { - // -- NO PREDECODING END-- - var clock_cycle:u32 = 0 - var output_write_address:OutputAddress = 0 - var pc:Address = entry_point - - // We interpret pc == MAX_UINT_64 as the stop signal, which is set by the ecall instruction - while pc != MAX_UINT_64 { - var index:u62 - var rem:u2 - // rem is the remainder of pc - base divided by 4 - index::rem = pc - base - - // NOTE: This section pertains to the predecoding justification - // It is pending decision and is commented for now. - // Execution must stay inside the span justified by predecoding, at 4-byte - // aligned PCs, so decoded[(pc - base) / 4] matches the row checked at pc. - // if pc= exec_end || rem != 0 { - // printf "[ERROR] pc outside executable span (pc=%d base=%d exec_end=%d)\n", pc, base, exec_end - // fail - // } - - // clock cycle starts at 1 - clock_cycle = clock_cycle + 1 - printf "\n----------------------------------------------------------------- PC=%d, clock cycle: %d\n", pc, clock_cycle - - // update pc and output_write_address - pc, output_write_address = interpreter(index as u64, pc, output_write_address) - } -} - +} \ No newline at end of file