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.

Aller à l'installation

Informations de source

Dépôt
starkware-libs/proving
Dernière activité de la source
23 juillet 2026 à 10:00
Langue détectée de SKILL.md
anglais
Étoiles
3
Forks
4

Options d'installation

Le prompt qui vérifie d'abord la source est sélectionné par défaut. Vous pouvez passer à une commande directe ou télécharger une copie locale.

Vérifiez les fichiers source

Lisez SKILL.md et les fichiers associés affichés par SkillsMP avant de décider de l'installer.

Affichage de SKILL.md

SKILL.md
Instructions source · Aperçu en lecture seule
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
Voir sur GitHub