diff --git a/cranelift/codegen/src/isa/zkasm/inst.isle b/cranelift/codegen/src/isa/zkasm/inst.isle index bbd9d26f6f3e..0f3b8d0fbac7 100644 --- a/cranelift/codegen/src/isa/zkasm/inst.isle +++ b/cranelift/codegen/src/isa/zkasm/inst.isle @@ -46,6 +46,11 @@ (rs1 Reg) (rs2 Reg)) + (RemArith + (rd WritableReg) + (rs1 Reg) + (rs2 Reg)) + ;; An load (Load (rd WritableReg) @@ -707,6 +712,14 @@ (_ Unit (emit (MInst.DivArith dst rs1 rs2)))) dst)) +;; Helper for emitting the `rem` instruction. +;; rd ← rs1 % rs2 +(decl zk_rem (XReg XReg) XReg) +(rule (zk_rem rs1 rs2) + (let ((dst WritableXReg (temp_writable_xreg)) + (_ Unit (emit (MInst.RemArith dst rs1 rs2)))) + dst)) + ;; Helper for emitting the `divu` ("Divide Unsigned") instruction. ;; rd ← rs1 ÷ rs2 (decl rv_divu (XReg XReg) XReg) diff --git a/cranelift/codegen/src/isa/zkasm/inst/emit.rs b/cranelift/codegen/src/isa/zkasm/inst/emit.rs index 5b2e3ed788fb..1a9928ec00b1 100644 --- a/cranelift/codegen/src/isa/zkasm/inst/emit.rs +++ b/cranelift/codegen/src/isa/zkasm/inst/emit.rs @@ -438,7 +438,7 @@ impl MachInstEmit for Inst { } &Inst::LoadConst64 { rd, imm } => { let rd = allocs.next_writable(rd); - put_string(&format!("{imm} => {}\n", reg_name(rd.to_reg())), sink); + put_string(&format!("{imm}n => {}\n", reg_name(rd.to_reg())), sink); } &Inst::Unwind { ref inst } => { put_string(&format!("Unwind\n"), sink); @@ -489,9 +489,24 @@ impl MachInstEmit for Inst { let rd = allocs.next_writable(rd); // Same as in MulArith about D register put_string("0 => D\n", sink); - put_string("0 => C\n", sink); put_string("$${var _divArith = E / B}\n", sink); + put_string("$${var _remArith = E % B}\n", sink); + put_string("${_divArith} => A\n", sink); + put_string("${_remArith} => C\n", sink); + put_string("E:ARITH\n", sink); + } + &Inst::RemArith { rd, rs1, rs2 } => { + let rs1 = allocs.next(rs1); + let rs2 = allocs.next(rs2); + debug_assert_eq!(rs1, e0()); + debug_assert_eq!(rs2, b0()); + let rd = allocs.next_writable(rd); + // Same as in MulArith about D register + put_string("0 => D\n", sink); + put_string("$${var _divArith = E / B}\n", sink); + put_string("$${var _remArith = E % B}\n", sink); put_string("${_divArith} => A\n", sink); + put_string("${_remArith} => C\n", sink); put_string("E:ARITH\n", sink); } &Inst::AluRRR { diff --git a/cranelift/codegen/src/isa/zkasm/inst/mod.rs b/cranelift/codegen/src/isa/zkasm/inst/mod.rs index 70c88a703a0d..7aa637aa8611 100644 --- a/cranelift/codegen/src/isa/zkasm/inst/mod.rs +++ b/cranelift/codegen/src/isa/zkasm/inst/mod.rs @@ -288,6 +288,15 @@ fn zkasm_get_operands VReg>(inst: &Inst, collector: &mut OperandC collector.reg_clobbers(clobbered); collector.reg_fixed_def(rd, a0()); } + &Inst::RemArith { rd, rs1, rs2, .. } => { + collector.reg_fixed_use(rs1, e0()); + collector.reg_fixed_use(rs2, b0()); + let mut clobbered = PRegSet::empty(); + clobbered.add(a0().to_real_reg().unwrap().into()); + clobbered.add(d0().to_real_reg().unwrap().into()); + collector.reg_clobbers(clobbered); + collector.reg_fixed_def(rd, c0()); + } &Inst::Load { rd, from, .. } => { if let Some(r) = from.get_allocatable_register() { collector.reg_use(r); @@ -995,6 +1004,12 @@ impl Inst { let rd_s = format_reg(rd.to_reg(), allocs); format!("DivArith rd = {}, rs1 = {}, rs2 = {}", rd_s, rs1_s, rs2_s) } + &Inst::RemArith { rd, rs1, rs2 } => { + let rs1_s = format_reg(rs1, allocs); + let rs2_s = format_reg(rs2, allocs); + let rd_s = format_reg(rd.to_reg(), allocs); + format!("RemArith rd = {}, rs1 = {}, rs2 = {}", rd_s, rs1_s, rs2_s) + } Inst::AddImm32 { rd, src1, src2 } => { let rd = format_reg(rd.to_reg(), allocs); format!("{src1} + {src2} => {rd};") diff --git a/cranelift/codegen/src/isa/zkasm/lower.isle b/cranelift/codegen/src/isa/zkasm/lower.isle index 3ac6e53f091f..e2a116308985 100644 --- a/cranelift/codegen/src/isa/zkasm/lower.isle +++ b/cranelift/codegen/src/isa/zkasm/lower.isle @@ -126,23 +126,8 @@ ;;;; Rules for `rem` ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(rule -1 (lower (has_type (fits_in_16 ty) (urem x y))) - (let - ((y2 XReg (zext y ty $I64)) - (_ InstOutput (gen_div_by_zero y2))) - (rv_remuw (zext x ty $I64) y2))) - -(rule -1 (lower (has_type (fits_in_16 ty) (srem x y))) - (let - ((y2 XReg (sext y ty $I64)) - (_ InstOutput (gen_div_by_zero y2))) - (rv_remw (sext x ty $I64) y2))) - -(rule (lower (has_type $I32 (srem x y))) - (let - ((y2 XReg (sext y $I32 $I64)) - (_ InstOutput (gen_div_by_zero y2))) - (rv_remw x y2))) +(rule (lower (srem x y)) + (zk_rem x y)) (rule (lower (has_type $I32 (urem x y))) (let @@ -150,11 +135,6 @@ (_ InstOutput (gen_div_by_zero y2))) (rv_remuw x y2))) -(rule (lower (has_type $I64 (srem x y))) - (let - ((_ InstOutput (gen_div_by_zero y))) - (rv_rem x y))) - (rule (lower (has_type $I64 (urem x y))) (let ((_ InstOutput (gen_div_by_zero y))) diff --git a/cranelift/codegen/src/isa/zkasm/lower/isle.rs b/cranelift/codegen/src/isa/zkasm/lower/isle.rs index efd76e1d00db..ee44a85fa04c 100644 --- a/cranelift/codegen/src/isa/zkasm/lower/isle.rs +++ b/cranelift/codegen/src/isa/zkasm/lower/isle.rs @@ -249,7 +249,9 @@ impl generated_code::Context for ZkAsmIsleContext<'_, '_, MInst, ZkAsmBackend> { let insts = match ty { F32 => MInst::load_fp_constant32(tmp, val as u32, alloc_tmp), F64 => MInst::load_fp_constant64(tmp, val, alloc_tmp), - _ => MInst::load_constant_u64(tmp, val, alloc_tmp), + I32 => MInst::load_constant_u32(tmp, val, alloc_tmp), + I64 => MInst::load_constant_u64(tmp, val, alloc_tmp), + _ => panic!("Not implemented"), }; self.emit_list(&insts); tmp.to_reg() diff --git a/cranelift/filetests/filetests/isa/zkasm/add.clif b/cranelift/filetests/filetests/isa/zkasm/add.clif index 51052d32175c..3cf2e3cf7463 100644 --- a/cranelift/filetests/filetests/isa/zkasm/add.clif +++ b/cranelift/filetests/filetests/isa/zkasm/add.clif @@ -25,7 +25,7 @@ function u0:1(i32 vmctx) fast { ; block0: ; ; +999999999 + +1000000000 => A; -; auipc B,0; ld B,12(B); j 12; .8byte 0x773593ff +; auipc B,0; ld B,12(B); j 8; .4byte 0x773593ff ; call userextname0 ; j label1 ; block1: diff --git a/cranelift/filetests/src/test_zkasm.rs b/cranelift/filetests/src/test_zkasm.rs index 9fe41440b303..213a1337e363 100644 --- a/cranelift/filetests/src/test_zkasm.rs +++ b/cranelift/filetests/src/test_zkasm.rs @@ -209,5 +209,8 @@ mod tests { ne, nop, _should_fail_unreachable, + i32_const, + i64_const, + rem, } } diff --git a/cranelift/zkasm_data/div.wat b/cranelift/zkasm_data/div.wat index 4d38ac1c4899..d6675d649d0c 100644 --- a/cranelift/zkasm_data/div.wat +++ b/cranelift/zkasm_data/div.wat @@ -1,9 +1,9 @@ (module (import "env" "assert_eq" (func $assert_eq (param i32) (param i32))) (func $main - i32.const 1999999999 - i32.const 64516129 + i32.const 5 + i32.const 2 i32.div_s - i32.const 31 + i32.const 2 call $assert_eq) (start $main)) diff --git a/cranelift/zkasm_data/generated/div.zkasm b/cranelift/zkasm_data/generated/div.zkasm index 434feb1c1703..9bc5b44a5efb 100644 --- a/cranelift/zkasm_data/generated/div.zkasm +++ b/cranelift/zkasm_data/generated/div.zkasm @@ -10,14 +10,15 @@ function_1: D :MSTORE(SP - 2) E :MSTORE(SP - 3) B :MSTORE(SP - 4) - 1999999999 => E - 64516129 => B + 5 => E + 2 => B 0 => D - 0 => C $${var _divArith = E / B} + $${var _remArith = E % B} ${_divArith} => A + ${_remArith} => C E:ARITH - 31 => B + 2 => B B :ASSERT $ => C :MLOAD(SP - 1) $ => D :MLOAD(SP - 2) diff --git a/cranelift/zkasm_data/generated/i32_const.zkasm b/cranelift/zkasm_data/generated/i32_const.zkasm new file mode 100644 index 000000000000..7d533df3bd7c --- /dev/null +++ b/cranelift/zkasm_data/generated/i32_const.zkasm @@ -0,0 +1,20 @@ +start: + zkPC + 2 => RR + :JMP(function_1) + :JMP(finalizeExecution) +function_1: + SP + 1 => SP + RR :MSTORE(SP - 1) + SP + 2 => SP + B :MSTORE(SP - 1) + 4 => A + 4 => B + B :ASSERT + $ => B :MLOAD(SP - 1) + SP - 2 => SP + $ => RR :MLOAD(SP - 1) + SP - 1 => SP + :JMP(RR) +finalizeExecution: + ${beforeLast()} :JMPN(finalizeExecution) + :JMP(start) \ No newline at end of file diff --git a/cranelift/zkasm_data/generated/i64_const.zkasm b/cranelift/zkasm_data/generated/i64_const.zkasm new file mode 100644 index 000000000000..da5a20d9691d --- /dev/null +++ b/cranelift/zkasm_data/generated/i64_const.zkasm @@ -0,0 +1,20 @@ +start: + zkPC + 2 => RR + :JMP(function_1) + :JMP(finalizeExecution) +function_1: + SP + 1 => SP + RR :MSTORE(SP - 1) + SP + 2 => SP + B :MSTORE(SP - 1) + 9223372036854775807n => A + 9223372036854775807n => B + B :ASSERT + $ => B :MLOAD(SP - 1) + SP - 2 => SP + $ => RR :MLOAD(SP - 1) + SP - 1 => SP + :JMP(RR) +finalizeExecution: + ${beforeLast()} :JMPN(finalizeExecution) + :JMP(start) \ No newline at end of file diff --git a/cranelift/zkasm_data/generated/i64_div.zkasm b/cranelift/zkasm_data/generated/i64_div.zkasm index 4a6e68980614..f07410f68892 100644 --- a/cranelift/zkasm_data/generated/i64_div.zkasm +++ b/cranelift/zkasm_data/generated/i64_div.zkasm @@ -10,10 +10,10 @@ function_1: D :MSTORE(SP - 2) E :MSTORE(SP - 3) B :MSTORE(SP - 4) - 214748364 => A + 214748364n => A A => E - 107374183 => A - 2 => B + 107374183n => A + 2n => B 0 => D 0 => C $${var _mulArith = A * B} @@ -23,13 +23,14 @@ function_1: 0 => C $${var _mulArith = A * B} ${_mulArith} => E :ARITH - 214748364 => B + 214748364n => B 0 => D - 0 => C $${var _divArith = E / B} + $${var _remArith = E % B} ${_divArith} => A + ${_remArith} => C E:ARITH - 214748366 => B + 214748366n => B B :ASSERT $ => C :MLOAD(SP - 1) $ => D :MLOAD(SP - 2) diff --git a/cranelift/zkasm_data/generated/i64_mul.zkasm b/cranelift/zkasm_data/generated/i64_mul.zkasm index 27fce4b7a4a9..fdac5d818ccb 100644 --- a/cranelift/zkasm_data/generated/i64_mul.zkasm +++ b/cranelift/zkasm_data/generated/i64_mul.zkasm @@ -10,10 +10,10 @@ function_1: D :MSTORE(SP - 2) E :MSTORE(SP - 3) B :MSTORE(SP - 4) - 214748364 => A + 214748364n => A A => E - 107374183 => A - 2 => B + 107374183n => A + 2n => B 0 => D 0 => C $${var _mulArith = A * B} @@ -24,10 +24,10 @@ function_1: $${var _mulArith = A * B} ${_mulArith} => A :ARITH A => E - 107374182 => A + 107374182n => A A :MSTORE(SP) - 214748366 => A - 2 => B + 214748366n => A + 2n => B 0 => D 0 => C $${var _mulArith = A * B} diff --git a/cranelift/zkasm_data/generated/rem.zkasm b/cranelift/zkasm_data/generated/rem.zkasm new file mode 100644 index 000000000000..d05ce5adeea5 --- /dev/null +++ b/cranelift/zkasm_data/generated/rem.zkasm @@ -0,0 +1,45 @@ +start: + zkPC + 2 => RR + :JMP(function_1) + :JMP(finalizeExecution) +function_1: + SP + 1 => SP + RR :MSTORE(SP - 1) + SP + 4 => SP + C :MSTORE(SP - 1) + D :MSTORE(SP - 2) + E :MSTORE(SP - 3) + B :MSTORE(SP - 4) + 5 => E + 2 => B + 0 => D + $${var _divArith = E / B} + $${var _remArith = E % B} + ${_divArith} => A + ${_remArith} => C + E:ARITH + C => A + 1 => B + B :ASSERT + 8 => E + 3 => B + 0 => D + $${var _divArith = E / B} + $${var _remArith = E % B} + ${_divArith} => A + ${_remArith} => C + E:ARITH + C => A + 2 => B + B :ASSERT + $ => C :MLOAD(SP - 1) + $ => D :MLOAD(SP - 2) + $ => E :MLOAD(SP - 3) + $ => B :MLOAD(SP - 4) + SP - 4 => SP + $ => RR :MLOAD(SP - 1) + SP - 1 => SP + :JMP(RR) +finalizeExecution: + ${beforeLast()} :JMPN(finalizeExecution) + :JMP(start) \ No newline at end of file diff --git a/cranelift/zkasm_data/i32_const.wat b/cranelift/zkasm_data/i32_const.wat new file mode 100644 index 000000000000..7d6d678b2e64 --- /dev/null +++ b/cranelift/zkasm_data/i32_const.wat @@ -0,0 +1,7 @@ +(module + (import "env" "assert_eq" (func $assert_eq (param i32) (param i32))) + (func $main + i32.const 4 + i32.const 4 + call $assert_eq) + (start $main)) diff --git a/cranelift/zkasm_data/i64_const.wat b/cranelift/zkasm_data/i64_const.wat new file mode 100644 index 000000000000..2b6f7f5cc6d9 --- /dev/null +++ b/cranelift/zkasm_data/i64_const.wat @@ -0,0 +1,7 @@ +(module + (import "env" "assert_eq" (func $assert_eq (param i64) (param i64))) + (func $main + i64.const 9223372036854775807 + i64.const 9223372036854775807 + call $assert_eq) + (start $main)) diff --git a/cranelift/zkasm_data/rem.wat b/cranelift/zkasm_data/rem.wat new file mode 100644 index 000000000000..f41aa0442758 --- /dev/null +++ b/cranelift/zkasm_data/rem.wat @@ -0,0 +1,14 @@ +(module + (import "env" "assert_eq" (func $assert_eq (param i32) (param i32))) + (func $main + i32.const 5 + i32.const 2 + i32.rem_s + i32.const 1 + call $assert_eq + i32.const 8 + i32.const 3 + i32.rem_s + i32.const 2 + call $assert_eq) + (start $main))