From 6b877149655eab106264021d25adc61aa7f43f5b Mon Sep 17 00:00:00 2001 From: Lun-Kai Hsu Date: Fri, 13 Dec 2024 22:22:37 -0800 Subject: [PATCH] [docs] update ISA with setup opcodes (#1036) * update isa for setup opcodes * fix * Update docs/specs/vm/ISA.md Co-authored-by: Jonathan Wang <31040440+jonathanpwang@users.noreply.github.com> * Update docs/specs/vm/RISCV.md --------- Co-authored-by: Jonathan Wang <31040440+jonathanpwang@users.noreply.github.com> --- docs/specs/vm/ISA.md | 7 +++++++ docs/specs/vm/RISCV.md | 2 +- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/docs/specs/vm/ISA.md b/docs/specs/vm/ISA.md index 4464fc4687..ad8337ed1f 100644 --- a/docs/specs/vm/ISA.md +++ b/docs/specs/vm/ISA.md @@ -332,8 +332,10 @@ Each instruction performs block accesses with block size `4` in address space `1 | ---------------- | ----------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | ADDMOD_RV32\ | `a,b,c,1,2` | `[r32{0}(a): N::NUM_LIMBS]_2 = [r32{0}(b): N::NUM_LIMBS]_2 + [r32{0}(c): N::NUM_LIMBS]_2 (mod N)` | | SUBMOD_RV32\ | `a,b,c,1,2` | `[r32{0}(a): N::NUM_LIMBS]_2 = [r32{0}(b): N::NUM_LIMBS]_2 - [r32{0}(c): N::NUM_LIMBS]_2 (mod N)` | +| SETUP_ADDSUBMOD_RV32\ | `a,b,c,1,2` | `assert([r32{0}(b): N::NUM_LIMBS]_2 == N)` for the chip that handles add and sub. For the sake of implementation convenience it also writes something (can be anything) into `[r32{0}(a): N::NUM_LIMBS]_2` | | MULMOD_RV32\ | `a,b,c,1,2` | `[r32{0}(a): N::NUM_LIMBS]_2 = [r32{0}(b): N::NUM_LIMBS]_2 * [r32{0}(c): N::NUM_LIMBS]_2 (mod N)` | | DIVMOD_RV32\ | `a,b,c,1,2` | `[r32{0}(a): N::NUM_LIMBS]_2 = [r32{0}(b): N::NUM_LIMBS]_2 / [r32{0}(c): N::NUM_LIMBS]_2 (mod N)`. Undefined behavior if `gcd([r32{0}(c): N::NUM_LIMBS]_2, N) != 1`. | +| SETUP_MULDIVMOD_RV32\ | `a,b,c,1,2` | `assert([r32{0}(b): N::NUM_LIMBS]_2 == N)` for the chip that handles mul and div. For the sake of implementation convenience it also writes something (can be anything) into `[r32{0}(a): N::NUM_LIMBS]_2` | ### Modular Branching @@ -342,6 +344,7 @@ The configuration of `N` is the same as above. For each instruction, the input e | Name | Operands | Description | | ----------------- | ----------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | ISEQMOD_RV32\ | `a,b,c,1,2` | `[a:4]_1 = [r32{0}(b): N::NUM_LIMBS]_2 == [r32{0}(c): N::NUM_LIMBS]_2 (mod N) ? 1 : 0`. Enforces that `[r32{0}(b): N::NUM_LIMBS]_2, [r32{0}(c): N::NUM_LIMBS]_2` are less than `N` and then sets the register value of `[a:4]_1` to `1` or `0` depending on whether the two big integers are equal. | +| SETUP_ISEQMOD_RV32\ | `a,b,c,1,2` | `assert([r32{0}(b): N::NUM_LIMBS]_2 == N)` in the chip that handles modular equality. For the sake of implementation convenience it also writes something (can be anything) into register value of `[a:4]_1` ### Short Weierstrass Elliptic Curve Arithmetic @@ -362,7 +365,9 @@ r32_ec_point(a) -> EcPoint { | Name | Operands | Description | | -------------- | ----------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | | SW_ADD_NE\ | `a,b,c,1,2` | Set `r32_ec_point(a) = r32_ec_point(b) + r32_ec_point(c)` (curve addition). Assumes that `r32_ec_point(b), r32_ec_point(c)` both lie on the curve and are not the identity point. Further assumes that `r32_ec_point(b).x, r32_ec_point(c).x` are not equal in the coordinate field. | +| SETUP_SW_ADD_NE\ | `a,b,c,1,2` | `assert(r32_ec_point(b).x == C::MODULUS)` in the chip for EC ADD. For the sake of implementation convenience it also writes something (can be anything) into `[r32{0}(a): 2*C::COORD_SIZE]_2`. It is required for proper functionality that `assert(r32_ec_point(b).x != r32_ec_point(c).x)` | | SW_DOUBLE\ | `a,b,_,1,2` | Set `r32_ec_point(a) = 2 * r32_ec_point(b)`. This doubles the input point. Assumes that `r32_ec_point(b)` lies on the curve and is not the identity point. | +| SETUP_SW_DOUBLE\ | `a,b,_,1,2` | `assert(r32_ec_point(b).x == C::MODULUS)` in the chip for EC DOUBLE. For the sake of implementation convenience it also writes something (can be anything) into `[r32{0}(a): 2*C::COORD_SIZE]_2`. It is required for proper functionality that `assert(r32_ec_point(b).y != 0 mod C::MODULUS)` | ### Complex Extension Field @@ -386,8 +391,10 @@ r32_fp2(a) -> Fp2 { | ---------- | ----------- | ------------------------------------------ | | ADD\ | `a,b,c,1,2` | Set `r32_fp2(a) = r32_fp2(b) + r32_fp2(c)` | | SUB\ | `a,b,c,1,2` | Set `r32_fp2(a) = r32_fp2(b) - r32_fp2(c)` | +| SETUP_ADDSUB\ | `a,b,c,1,2` | `assert([r32_fp2(b).c0 == N)` for the chip that handles add and sub. For the sake of implementation convenience it also writes something (can be anything) into `r32_fp2(a)` | | MUL\ | `a,b,c,1,2` | Set `r32_fp2(a) = r32_fp2(b) * r32_fp2(c)` | | DIV\ | `a,b,c,1,2` | Set `r32_fp2(a) = r32_fp2(b) / r32_fp2(c)` | +| SETUP_MULDIV\ | `a,b,c,1,2` | `assert([r32_fp2(b).c0 == N)` for the chip that handles mul and div. For the sake of implementation convenience it also writes something (can be anything) into `r32_fp2(a)` | ### Optimal Ate Pairing diff --git a/docs/specs/vm/RISCV.md b/docs/specs/vm/RISCV.md index d083fcdf28..a07902885e 100644 --- a/docs/specs/vm/RISCV.md +++ b/docs/specs/vm/RISCV.md @@ -91,7 +91,7 @@ Short Weierstrass elliptic curve arithmetic depends on elliptic curve `C`. The i | --------------- | --- | ----------- | ------ | --------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | sw_add_ne\ | R | 0101011 | 001 | `idx*8` | `EcPoint([rd:2*C::COORD_SIZE]_2) = EcPoint([rs1:2*C::COORD_SIZE]_2) + EcPoint([rs2:2*C::COORD_SIZE]_2)`. Assumes that input affine points are not identity and do not have same x-coordinate. | | sw_double\ | R | 0101011 | 001 | `idx*8+1` | `EcPoint([rd:2*C::COORD_SIZE]_2) = 2 * EcPoint([rs1:2*C::COORD_SIZE]_2)`. Assumes that input affine point is not identity. `rs2` is unused and must be set to `x0`. | -| setup\ | R | 0101011 | 001 | `idx*8+2` | `assert([rs1: C::COORD_SIZE]_2 == C::MODULUS)` in the chip defined by the register index of `rs2`. For the sake of implementation convenience it also writes something (can be anything) into `[rd: 2*C::COORD_SIZE]_2`. It is required for proper functionality that `[rs1 + C::COORD_SIZE: C::COORD_SIZE]_2 != C::Fp::ZERO`. If `ind(rs2) != 0`, then this instruction is setup for `sw_add_ne`. Otherwise it is setup for `sw_double`. When `ind(rs2) != 0`, it is required that `[rs2: C::COORD_SIZE]_2 != C::MODULUS` and `[rs2 + C::COORD_SIZE: C::COORD_SIZE]_2 != C::Fp::ZERO`. | +| setup\ | R | 0101011 | 001 | `idx*8+2` | `assert([rs1: C::COORD_SIZE]_2 == C::MODULUS)` in the chip defined by the register index of `rs2`. For the sake of implementation convenience it also writes something (can be anything) into `[rd: 2*C::COORD_SIZE]_2`. If `ind(rs2) != 0`, then this instruction is setup for `sw_add_ne`. Otherwise it is setup for `sw_double`. When `ind(rs2) != 0` (add_ne), it is required for proper functionality that `[rs2: C::COORD_SIZE]_2 != [rs1: C::COORD_SIZE]_2`; otherwise (double), it is required that `[rs1 + C::COORD_SIZE: C::COORD_SIZE]_2 != C::Fp::ZERO` | | hint_decompress | R | 0101011 | 001 | `idx*8+3` | Read `x: C::Fp` from `[rs1: C::COORD_SIZE]_2` and `rec_id: u8` from `[rs2]_2`. Reset the hint stream to equal the unique `y: C::Fp` such that `(x, y)` is a point on `C` and `y` has the same parity as `rec_id`, if it exists. Otherwise reset hint stream to arbitrary `C::Fp`. `rd` should be `x0`. | Since `funct7` is 7-bits, up to 16 curves can be supported simultaneously. We use `idx*8` to leave some room for future expansion.