Skip to main content

circle-stark-mathematics

Circle-group-specific mathematics for STWO: circle points, cosets, domains, circle FFT, circle polynomials, twin cosets, vanishing polynomials, and the M31 circle group structure. Use when modifying any code involving these concepts, which form the non-standard foundation distinguishing STWO from traditional multiplicative-subgroup STARKs.

Ir a la instalación

Datos de origen

Repositorio
starkware-libs/proving
Última actividad en el origen
23 de julio de 2026 a las 10:00
Idioma detectado de SKILL.md
inglés
Estrellas
3
Forks
4

Opciones de instalación

De forma predeterminada está seleccionado el prompt que primero revisa el origen. Puedes cambiar a un comando directo o descargar una copia local.

Revisa los archivos de origen

Lee SKILL.md y los archivos complementarios que muestra SkillsMP antes de decidir si quieres instalarlo.

Mostrando SKILL.md

SKILL.md
Instrucciones de origen · Vista previa de solo lectura
name
circle-stark-mathematics
description
Circle-group-specific mathematics for STWO: circle points, cosets, domains, circle FFT, circle polynomials, twin cosets, vanishing polynomials, and the M31 circle group structure. Use when modifying any code involving these concepts, which form the non-standard foundation distinguishing STWO from traditional multiplicative-subgroup STARKs.
# Circle STARK Mathematics ## Canonical Theory Sources - `.agents/papers/llm/INDEX.llm.md` — notation and invariant map - `.agents/papers/llm/Circle_STARKs.llm.md` — primary source for circle group/FFT/FRI math - `.agents/papers/llm/Stwo_Whitepaper.llm.md` — implementation-side protocol constraints ## The Circle Group ### Definition The circle curve over F_p is: ``` C: x^2 + y^2 = 1 (over F_p) ``` For p = 2^31 - 1 (Mersenne prime), the group has: - |C(F_p)| = p + 1 = 2^31 - Group is cyclic of order 2^31 - Group law: (x0,y0) * (x1,y1) = (x0*x1 - y0*y1, x0*y1 + y0*x1) - Identity: (1, 0) - Inverse (conjugate): (x, y)^{-1} = (x, -y) **Source**: `.agents/papers/llm/Circle_STARKs.llm.md` (`s:circle:curve`) **Implementation**: - `crates/stwo/src/core/circle.rs` — `CirclePoint<F>` struct, `Add` impl (group law), `Neg` impl (conjugate = inverse) ### Generator ``` M31_CIRCLE_GEN = (2, 1268011823) order = 2^31 ``` **Implementation**: `crates/stwo/src/core/circle.rs` — `M31_CIRCLE_GEN` constant ### Key Maps | Map | Formula | Code | |-----|---------|------| | Squaring (pi) | pi(x,y) = (2x^2 - 1, 2xy) | `CirclePoint::double()` via `Add` self+self | | x-doubling | double_x(x) = 2x^2 - 1 | `CirclePoint::double_x()` | | Conjugate (J) | J(x,y) = (x, -y) | `CirclePoint::conjugate()` | | Antipode | ant(x,y) = (-x, -y) | `CirclePoint::antipode()` | **Critical property**: pi and J commute: pi(J(P)) = J(pi(P)). ## Cosets and Domains ### Subgroups G_k = subgroup of order 2^k, generated by M31_CIRCLE_GEN^{2^{31-k}}. ### Canonic Cosets A canonic coset of size 2^k is Q_{k+1} * G_k, where Q_{k+1} has order 2^{k+1}. This is the standard trace/evaluation domain. **Implementation**: `crates/stwo/src/core/poly/circle/canonic.rs` — `CanonicCoset` ### Twin Cosets A twin coset of size N = 2^n is: D = Q*G_{n-1} union Q^{-1}*G_{n-1} Properties: - J-invariant (closed under conjugation) - Every J-orbit has exactly 2 points - pi maps a twin coset of size 2^n to one of size 2^{n-1} - This gives the domain chain for the FFT: D_n -> D_{n-1} -> ... -> D_1 **Source**: `.agents/papers/llm/Circle_STARKs.llm.md` (`def:standard:twin:coset`, `lem:twincosets:images`) **Implementation**: `crates/stwo/src/core/poly/circle/domain.rs` — `CircleDomain` ### Coset Type **Implementation**: `crates/stwo/src/core/circle.rs` — `CirclePointIndex`, `Coset` structs ## Circle FFT ### FFT Basis For j with binary representation (j_0, ..., j_{n-1}): ``` b_j(x,y) = y^{j_0} * v_1(x)^{j_1} * v_2(x)^{j_2} * ... * v_{n-1}(x)^{j_{n-1}} ``` Where v_k are the iterated x-doubling maps: - v_1(x) = x - v_2(x) = 2x^2 - 1 - v_3(x) = 2(2x^2-1)^2 - 1 = 8x^4 - 8x^2 + 1 **Source**: `.agents/papers/llm/Circle_STARKs.llm.md` (`def:FFT:basis`) ### Algorithm The circle FFT is a divide-and-conquer algorithm: 1. **Layer 1 (J-split)**: f(x,y) = f_0(x) + y*f_1(x) - f_0(x) = (f(x,y) + f(x,-y)) / 2 - f_1(x) = (f(x,y) - f(x,-y)) / (2y) 2. **Layers 2..n (pi-split)**: g(x) = g_0(pi(x)) + x*g_1(pi(x)) - g_0(pi(x)) = (g(x) + g(-x)) / 2 - g_1(pi(x)) = (g(x) - g(-x)) / (2x) **Complexity**: N*(n/2) multiplications + N*n additions **Source**: `.agents/papers/llm/Circle_STARKs.llm.md` (`thm:FFT`) **Implementation**: - Butterfly: `crates/stwo/src/core/fft.rs` — `butterfly()`, `ibutterfly()` - CPU FFT: `crates/stwo/src/prover/backend/cpu/circle.rs` - SIMD FFT: `crates/stwo/src/prover/backend/simd/fft/rfft.rs`, `ifft.rs` - Circle ops: `crates/stwo/src/prover/backend/simd/circle.rs` ### FFT Space L'_N(F) = { p_0(x) + y*p_1(x) : deg(p_i) <= N/2 - 1 } This has dimension N. The full space L_N(F) has dimension N+1. The gap: L_N(F) = L'_N(F) + span(v_n). This "dimension gap" is unique to circle STARKs and has implications for FRI (see DIVERGENCE-001 in the divergence log). **Source**: `.agents/papers/llm/Circle_STARKs.llm.md` (`prop:LN:properties`, `lem:FFT:space:monomial:basis`, Section "8. Implementation-Critical Invariants") ## Vanishing Polynomials For a canonic coset of size 2^k: ``` v_coset(p) = v_k(x_p) ``` Where v_k is the k-fold iterated x-doubling applied to the rotated point. **Source**: `.agents/papers/llm/Circle_STARKs.llm.md` (Section "12. Source Anchor Map" -> vanishing/quotients) **Implementation**: `crates/stwo/src/core/constraints.rs` — `coset_vanishing()` The formal derivative is: ``` v'_coset(p) = 4^{k-1} * prod_{i=1}^{k-1} v_i(x_p) ``` **Source**: `.agents/papers/llm/Circle_STARKs.llm.md` (Section "12. Source Anchor Map" -> vanishing/quotients) **Implementation**: `crates/stwo/src/core/constraints.rs` — `coset_vanishing_derivative()` ## Secure Field Circle Group The circle group extends to QM31: ``` SECURE_FIELD_CIRCLE_GEN = ((1, 0, 478637715, 513582971), (992285211, 649143431, 740191619, 1186584352)) SECURE_FIELD_CIRCLE_ORDER = P4 - 1 (where P4 = (2^31-1)^4) ``` The OODS point is sampled from C(QM31) \ C(M31) using the rational parametrization: t -> ((1-t^2)/(1+t^2), 2t/(1+t^2)). **Implementation**: `crates/stwo/src/core/circle.rs` — `get_random_point()` ## Security Invariants INVARIANT-CIRCLE-1: Circle point addition must satisfy x^2 + y^2 = 1. Verify: after any CirclePoint operation, the result lies on the circle. INVARIANT-CIRCLE-2: The FFT and inverse FFT must be exact inverses. Verify: interpolate(evaluate(poly)) == poly for all circle polynomials. INVARIANT-CIRCLE-3: Coset vanishing polynomials must vanish on exactly the coset points and nowhere else on the evaluation domain. INVARIANT-CIRCLE-4: The OODS point must NOT lie in the commitment domain or trace domain. It must be in C(QM31) \ C(M31). ## Forbidden Actions In this domain, agents must NEVER: - Modify the circle group law (Add impl for CirclePoint) — this is the mathematical foundation of the entire system - Change the generator constants without re-deriving group order - Modify the FFT butterfly operations without verifying invertibility - Change coset construction without verifying vanishing polynomial properties - Use a base-field (M31) point as an OODS point — must use secure field
Ver en GitHub