Skip to content

Commit 840135f

Browse files
Avaneesh-axiomAvaneesh-axiom
committed
Update docs
1 parent 5562893 commit 840135f

File tree

4 files changed

+17
-24
lines changed

4 files changed

+17
-24
lines changed

‎docs/specs/ISA.md

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -672,8 +672,7 @@ The elliptic curve extension supports arithmetic over elliptic curves `C` in the
672672

673673
We note that
674674
the definitions of the curve arithmetic operations for short Weierstrass curves do not depend on `C::B`. The VM configuration will specify a list of supported curves. For
675-
each curve `C` (of either form) there will be associated configuration parameters `C::COORD_SIZE` and `C::BLOCK_SIZE` (
676-
defined below). The extension operates on address spaces `1` and `2`, meaning all memory cells are constrained to be
675+
each curve `C` (of either form) there will be associated configuration parameters `C::COORD_SIZE` and `C::BLOCK_SIZE` (defined below). The extension operates on address spaces `1` and `2`, meaning all memory cells are constrained to be
677676
bytes.
678677

679678
An affine curve point `EcPoint(x, y)` is a pair of `x,y` where each element is an array of `C::COORD_SIZE` elements each
@@ -691,6 +690,8 @@ r32_ec_point(a) -> EcPoint {
691690
}
692691
```
693692

693+
The instructions that have prefix `SW_` perform short Weierstrass curve operations, and those with prefix `TE_` perform twisted Edwards curve operations.
694+
694695
| Name | Operands | Description |
695696
| -------------------- | ----------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
696697
| SW_ADD_NE\<C\> | `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. |
@@ -706,9 +707,10 @@ The elliptic curve extension defines the following phantom sub-instructions.
706707

707708
| Name | Discriminant | Operands | Description |
708709
| -------------- | ------------ | ------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
709-
| SwHintDecompress | 0x40 | `a,b,c_upper` | Uses `c_upper = C::IDX` to determine the index of the curve `C`, from the list of enabled curves. Assumes the `C::IDX`th curve is a short Weierstrass curve. Read from memory `x = [r32{0}(a): C::COORD_SIZE]_2` for an element in the coordinate field of `C`. Let `rec_id = [r32{0}(b)]_2` be a byte in memory for the recovery id, where the lowest bit is 1 if and only if the `y` coordinate of the corresponding point is odd. If there exists a unique `y` such that `(x, y)` is a point on `C` and `y` has the same parity as `rec_id`, then the sub-instruction resets the hint stream to `[1, 0, 0, 0]` followed by `y: [_; C::COORD_SIZE]`. Otherwise, it resets the hint stream to `[0, 0, 0, 0]` followed by `sqrt: [_; C::COORD_SIZE]` where `sqrt * sqrt == (x^3 + ax + b) * non_qr` (`non_qr` is a quadratic nonresidue of `C::Fp`). |
710-
| TeHintDecompress | 0x40 | `a,b,c_upper` | Uses `c_upper = C::IDX` to determine the index of the curve `C`, from the list of enabled curves. Assumes the `C::IDX`th curve is a twisted Edwards curve. Read from memory `y = [r32{0}(a): C::COORD_SIZE]_2` for an element in the coordinate field of `C`. Let `rec_id = [r32{0}(b)]_2` be a byte in memory for the recovery id, where the lowest bit is 1 if and only if the `x` coordinate of the corresponding point is odd. If there exists a unique `x` such that `(x, y)` is a point on `C` and `x` has the same parity as `rec_id`, then the sub-instruction resets the hint stream to `[1, 0, 0, 0]` followed by `x: [_; C::COORD_SIZE]`. Otherwise, TODO |
711-
| HintNonQr | 0x41 | `_,_,c_upper` | Reset the hint stream to equal `non_qr: [_; C::COORD_SIZE]` where `non_qr` is a quadratic nonresidue of `C::Fp`. |
710+
| SwHintDecompress | 0x40 | `a,b,c_upper` | Use `c_upper = C::IDX` to determine the index of the curve `C`, from the list of enabled short Weierstrass curves. Read from memory `x = [r32{0}(a): C::COORD_SIZE]_2` for an element in the coordinate field of `C`. Let `rec_id = [r32{0}(b)]_2` be a byte in memory for the recovery id, where the lowest bit is 1 if and only if the `y` coordinate of the corresponding point is odd. If there exists a unique `y` such that `(x, y)` is a point on `C` and `y` has the same parity as `rec_id`, then the sub-instruction resets the hint stream to `[1, 0, 0, 0]` followed by `y: [_; C::COORD_SIZE]`. Otherwise, it resets the hint stream to `[0, 0, 0, 0]` followed by `sqrt: [_; C::COORD_SIZE]` where `sqrt * sqrt == (x^3 + ax + b) * non_qr` where `non_qr` is a quadratic nonresidue of `C::Fp` that is fixed for the curve. |
711+
| SwHintNonQr | 0x41 | `_,_,c_upper` | Reset the hint stream to equal `non_qr: [_; C::COORD_SIZE]` where `non_qr` is a quadratic nonresidue of `C::Fp`. This element is fixed for the curve during VM instantiation so multiple calls to this instruction will always return the same hint. |
712+
| TeHintDecompress | 0x42 | `a,b,c_upper` | Use `c_upper = C::IDX` to determine the index of the curve `C`, from the list of enabled twisted Edwards curves. Read from memory `y = [r32{0}(a): C::COORD_SIZE]_2` for an element in the coordinate field of `C`. Let `rec_id = [r32{0}(b)]_2` be a byte in memory for the recovery id, where the lowest bit is 1 if and only if the `x` coordinate of the corresponding point is odd. If there exists a unique `x` such that `(x, y)` is a point on `C` and `x` has the same parity as `rec_id`, then the sub-instruction resets the hint stream to `[1, 0, 0, 0]` followed by `x: [_; C::COORD_SIZE]`. Otherwise, it resets the hint stream to `[0, 0, 0, 0]` followed by `sqrt: [_; C::COORD_SIZE]` where `sqrt * sqrt = (y^2 - 1) / (C::D * y^2 - C::A) * non_qr` where `non_qr` is a quadratic nonresidue of `C::Fp` that is fixed for the curve. |
713+
| TeHintNonQr | 0x43 | `_,_,c_upper` | Reset the hint stream to equal `non_qr: [_; C::COORD_SIZE]` where `non_qr` is a quadratic nonresidue of `C::Fp`. This element is fixed for the curve during VM instantiation so multiple calls to this instruction will always return the same hint. |
712714

713715
### Pairing Extension
714716

‎docs/specs/RISCV.md

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -163,18 +163,19 @@ Complex extension field arithmetic over `Fp2` depends on `Fp` where `-1` is not
163163

164164
## Elliptic Curve Extension
165165

166-
The elliptic curve extension supports arithmetic over short Weierstrass curves and twisted Edwards curves, which requires specification of the elliptic curve `C`. The extension must be configured to support a fixed ordered list of supported curves. There is one list for each type of curves (short Weierstrass and twisted Edwards). We use `config.curve_idx(C)` to denote the index of `C` in the appropriate list. In the list below, `idx` denotes `config.curve_idx(C)`.
166+
The elliptic curve extension supports arithmetic over short Weierstrass curves and twisted Edwards curves, which requires specification of the elliptic curve `C`. The extension must be configured to support two fixed ordered lists of supported curves: one list of short Weierstrass curves and one list of twisted Edwards curves. Instructions prefixed with `sw_` are for short Weierstrass curves and instructions prefixed with `te_` are for twisted Edwards curves. We use `config.curve_idx(C)` to denote the index of `C` in the appropriate list. In the list below, `idx` denotes `config.curve_idx(C)`.
167167

168168
| RISC-V Inst | FMT | opcode[6:0] | funct3 | funct7 | RISC-V description and notes |
169169
| --------------- | --- | ----------- | ------ | --------- | -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
170170
| sw_add_ne\<C\> | 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. |
171171
| sw_double\<C\> | 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`. |
172172
| sw_setup\<C\> | R | 0101011 | 001 | `idx*8+2` | `assert([rs1: 2*C::COORD_SIZE]_2 == [C::MODULUS, CURVE_A])` in the chip defined by the register index of `rs2`. For the sake of implementation convenience it also writes an unconstrained value 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` |
173-
| sw_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`. If there exists a unique `y: C::Fp` such that `(x, y)` is a point on `C` and `y` has the same parity as `rec_id`, then reset the hint stream to `[1u8, 0u8, 0u8, 0u8]` concatenated with the limbs representing `y` in little-endian order; otherwise, reset it to `[0u8; 4]` concatenated the limbs representing `sqrt` where `sqrt * sqrt == (x^3 + ax + b) * non_qr` (`non_qr` is a quadratic nonresidue of `C::Fp`). `rd` should be `x0`. |
173+
| sw_hint_decompress\<C\> | R | 0101011 | 001 | `idx*8+3` | Read `x: C::Fp` from `[rs1: C::COORD_SIZE]_2` and `rec_id: u8` from `[rs2]_2`. If there exists a unique `y: C::Fp` such that `(x, y)` is a point on `C` and `y` has the same parity as `rec_id`, then reset the hint stream to `[1u8, 0u8, 0u8, 0u8]` concatenated with the limbs representing `y` in little-endian order; otherwise, reset it to `[0u8; 4]` concatenated the limbs representing `sqrt` where `sqrt * sqrt == (x^3 + ax + b) * non_qr` where `non_qr` is a quadratic nonresidue of `C::Fp` that is fixed for the curve. `rd` should be `x0`. |
174+
| sw_hint_non_qr\<C\> | R | 0101011 | 001 | `idx*8+4` | Reset the hint stream to equal `non_qr` where `non_qr` is a quadratic nonresidue of `C::Fp`. This element is fixed for the curve during VM instantiation so multiple calls to this instruction will always return the same hint. `rd`, `rs1`, and `rs2` should be `x0`. |
174175
| te_add\<C\> | R | 0101011 | 100 | `idx*8` | `EcPoint([rd:2*C::COORD_SIZE]_2) = EcPoint([rs1:2*C::COORD_SIZE]_2) + EcPoint([rs2:2*C::COORD_SIZE]_2)`. |
175-
| te_setup\<C\> | R | 0101011 | 100 | `idx*8+2` | `assert([rs1: 2*C::COORD_SIZE]_2 == [C::MODULUS, C::CURVE_A] && [rs2: C::COORD_SIZE]_2 == C::CURVE_D])`. For the sake of implementation convenience it also writes an unconstrained value into `[rd: 2*C::COORD_SIZE]_2`. |
176-
| te_hint_decompress | R | 0101011 | 100 | `idx*8+3` | Read `y: C::Fp` from `[rs1: C::COORD_SIZE]_2` and `rec_id: u8` from `[rs2]_2`. Reset the hint stream to equal the unique `x: C::Fp` such that `(x, y)` is a point on `C` and `x` has the same parity as `rec_id`, if it exists. Otherwise reset hint stream to arbitrary `C::Fp`. `rd` should be `x0`. |
177-
| hint_non_qr | R | 0101011 | 001 | `idx*8+4` | Reset the hint stream to equal `non_qr` where `non_qr` is a quadratic nonresidue of `C::Fp`. `rd`, `rs1`, and `rs2` should be `x0`. |
176+
| te_setup\<C\> | R | 0101011 | 100 | `idx*8+1` | `assert([rs1: 2*C::COORD_SIZE]_2 == [C::MODULUS, C::CURVE_A] && [rs2: C::COORD_SIZE]_2 == C::CURVE_D])`. For the sake of implementation convenience it also writes an unconstrained value into `[rd: 2*C::COORD_SIZE]_2`. |
177+
| te_hint_decompress\<C\> | R | 0101011 | 100 | `idx*8+2` | Read `y: C::Fp` from `[rs1: C::COORD_SIZE]_2` and `rec_id: u8` from `[rs2]_2`. If there exists a unique `x: C::Fp` such that `(x, y)` is a point on `C` and `x` has the same parity as `rec_id`, then reset the hint stream to `[1u8, 0u8, 0u8, 0u8]` concatenated with the limbs representing `x` in little-endian order; otherwise, reset it to `[0u8; 4]` concatenated the limbs representing `sqrt` where `sqrt * sqrt == (y^2 - 1) / (C::D * y^2 - C::A) * non_qr` where `non_qr` is a quadratic nonresidue of `C::Fp` that is fixed for the curve. `rd` should be `x0`. |
178+
| te_hint_non_qr\<C\> | R | 0101011 | 100 | `idx*8+3` | Reset the hint stream to equal `non_qr` where `non_qr` is a quadratic nonresidue of `C::Fp`. This element is fixed for the curve during VM instantiation so multiple calls to this instruction will always return the same hint. `rd`, `rs1`, and `rs2` should be `x0`. |
178179

179180

180181
Since `funct7` is 7-bits, up to 16 curves can be supported simultaneously. We use `idx*8` to leave some room for future expansion.

‎docs/specs/transpiler.md

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -204,11 +204,12 @@ Each VM extension's behavior is specified below.
204204
| sw_add_ne\<C\> | EC_ADD_NE_RV32\<C\> `ind(rd), ind(rs1), ind(rs2), 1, 2` |
205205
| sw_double\<C\> | EC_DOUBLE_RV32\<C\> `ind(rd), ind(rs1), 0, 1, 2` |
206206
| sw_setup\<C\> | SETUP_EC_ADD_NE_RV32\<C\> `ind(rd), ind(rs1), ind(rs2), 1, 2` if `ind(rs2) != 0`, SETUP_EC_DOUBLE_RV32\<C\> `ind(rd), ind(rs1), ind(rs2), 1, 2` if `ind(rs2) = 0` |
207-
| sw_hint_decompress | PHANTOM `ind(rs1), ind(rs2), phantom_c(curve_idx, HintDecompress)` |
207+
| sw_hint_decompress\<C\> | PHANTOM `ind(rs1), ind(rs2), phantom_c(curve_idx, SwHintDecompress)` |
208+
| sw_hint_non_qr\<C\> | PHANTOM `0, 0, phantom_c(curve_idx, SwHintNonQr)` |
208209
| te_add\<C\> | TE_ADD_RV32\<C\> `ind(rd), ind(rs1), ind(rs2), 1, 2` |
209210
| te_setup\<C\> | SETUP_TE_ADD_RV32\<C\> `ind(rd), ind(rs1), ind(rs2), 1, 2` |
210-
| te_hint_decompress| PHANTOM `ind(rd), ind(rs1), phantom_c(curve_idx, HintDecompress)` |
211-
| hint_non_qr | PHANTOM `0, 0, phantom_c(curve_idx, HintNonQr)` |
211+
| te_hint_decompress\<C\> | PHANTOM `ind(rd), ind(rs1), phantom_c(curve_idx, TeHintDecompress)` |
212+
| te_hint_non_qr\<C\> | PHANTOM `0, 0, phantom_c(curve_idx, TeHintNonQr)` |
212213

213214
### Pairing Extension
214215

‎extensions/ecc/circuit/src/ecc_extension.rs

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -515,17 +515,12 @@ pub(crate) mod phantom {
515515
y_limbs.push(limb.as_canonical_u32() as u8);
516516
}
517517
let y = BigUint::from_bytes_le(&y_limbs);
518-
println!("y: {:?}", &y);
519518
let rs2 = unsafe_read_rv32_register(memory, b);
520519
let rec_id = memory.unsafe_read_cell(
521520
F::from_canonical_u32(RV32_MEMORY_AS),
522521
F::from_canonical_u32(rs2),
523522
);
524523
let hint = self.decompress_point(y, rec_id.as_canonical_u32() & 1 == 1, c_idx);
525-
println!(
526-
"hint.sqrt: {:?}, hint.possible: {}",
527-
hint.sqrt, hint.possible
528-
);
529524
let hint_bytes = once(F::from_bool(hint.possible))
530525
.chain(repeat(F::ZERO))
531526
.take(4)
@@ -557,16 +552,10 @@ pub(crate) mod phantom {
557552
curve_idx: usize,
558553
) -> DecompressionHint<BigUint> {
559554
let curve = &self.supported_curves[curve_idx];
560-
println!("y: {:?}", &y);
561-
println!("curve.modulus: {:?}", &curve.modulus);
562555
let numerator = (&y * &y + &curve.modulus - 1u8) % &curve.modulus;
563556
let denominator =
564557
(&curve.coeffs.d * &y * &y + &curve.modulus - &curve.coeffs.a) % &curve.modulus;
565-
println!("numerator: {:?}", &numerator);
566558
let rhs = numerator * denominator.modinv(&curve.modulus).unwrap() % &curve.modulus;
567-
println!("denominator: {:?}", &denominator);
568-
println!("rhs: {:?}", &rhs);
569-
println!("non_qr: {:?}", &self.non_qrs[curve_idx]);
570559
match mod_sqrt(&rhs, &curve.modulus, &self.non_qrs[curve_idx]) {
571560
Some(x) => {
572561
if is_x_odd == x.is_odd() {

0 commit comments

Comments
 (0)