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

zkasm: rem #68

Merged
merged 2 commits into from
Nov 6, 2023
Merged

zkasm: rem #68

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
87a848c
zkasm: i64.const
MCJOHN974 Nov 1, 2023
d67edda
zkasm: rem
MCJOHN974 Nov 6, 2023
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
13 changes: 13 additions & 0 deletions cranelift/codegen/src/isa/zkasm/inst.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,11 @@
(rs1 Reg)
(rs2 Reg))

(RemArith
(rd WritableReg)
(rs1 Reg)
(rs2 Reg))

;; An load
(Load
(rd WritableReg)
Expand Down Expand Up @@ -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)
Expand Down
19 changes: 17 additions & 2 deletions cranelift/codegen/src/isa/zkasm/inst/emit.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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 {
Expand Down
15 changes: 15 additions & 0 deletions cranelift/codegen/src/isa/zkasm/inst/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -288,6 +288,15 @@ fn zkasm_get_operands<F: Fn(VReg) -> 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);
Expand Down Expand Up @@ -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};")
Expand Down
24 changes: 2 additions & 22 deletions cranelift/codegen/src/isa/zkasm/lower.isle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,35 +126,15 @@

;;;; 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
((y2 XReg (zext y $I32 $I64))
(_ 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)))
Expand Down
4 changes: 3 additions & 1 deletion cranelift/codegen/src/isa/zkasm/lower/isle.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down
2 changes: 1 addition & 1 deletion cranelift/filetests/filetests/isa/zkasm/add.clif
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
3 changes: 3 additions & 0 deletions cranelift/filetests/src/test_zkasm.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -209,5 +209,8 @@ mod tests {
ne,
nop,
_should_fail_unreachable,
i32_const,
i64_const,
rem,
}
}
6 changes: 3 additions & 3 deletions cranelift/zkasm_data/div.wat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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))
9 changes: 5 additions & 4 deletions cranelift/zkasm_data/generated/div.zkasm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
20 changes: 20 additions & 0 deletions cranelift/zkasm_data/generated/i32_const.zkasm
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
20 changes: 20 additions & 0 deletions cranelift/zkasm_data/generated/i64_const.zkasm
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
13 changes: 7 additions & 6 deletions cranelift/zkasm_data/generated/i64_div.zkasm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -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)
Expand Down
12 changes: 6 additions & 6 deletions cranelift/zkasm_data/generated/i64_mul.zkasm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -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}
Expand Down
45 changes: 45 additions & 0 deletions cranelift/zkasm_data/generated/rem.zkasm
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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)
7 changes: 7 additions & 0 deletions cranelift/zkasm_data/i32_const.wat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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))
7 changes: 7 additions & 0 deletions cranelift/zkasm_data/i64_const.wat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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))
14 changes: 14 additions & 0 deletions cranelift/zkasm_data/rem.wat
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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))