soft3/zheng/docs/explanation.md

zheng explanations

zheng is a polynomial proof system. these documents explain the concepts, design decisions, and historical context.

for formal definitions, see specs/ (soundness per component: specs/soundness.md). for the hash primitive, see hemera. for the VM whose traces we prove, see nox.

reading path

                              ╭──────── vision ────────╮
                              │                        │
                     why-zheng                the-name
                              │
                              │
                    ╭──────── foundations ────────╮
                    │            │               │
                 stark          CCS         landscape
                    │            │               │
                    ╰────────────┼───────────────╯
                                 │
                   ╭──────── protocols ────────╮
                   │             │             │
              sumcheck    poly-commits    fri-to-whir
                   │             │             │
                   ╰─────────────┼─────────────╯
                                 │
                                 │
                        superspartan
                                 │
                                 │
                           whirlaway
                                 │
                                 │
                        trace-to-proof
                                 │
                                 │
                    ╭──────── powers ──────────╮
                    │       │        │         │
              recursion  security  performance  bbg-integration

pages

vision

page topic
why-zheng why a custom proof system — what zheng enables and why existing systems fall short
the-name 証 etymology — proof as evidence, verification as witnessing

foundations

page topic
stark STARK systems — arithmetization (AIR, R1CS, CCS), univariate vs multilinear, heritage; zheng proofs are not STARKs
CCS Customizable Constraint Systems — why unified constraints matter for zheng and accumulation
landscape proof system taxonomy — trusted setup vs transparent, pre-quantum vs post-quantum, SNARKs vs STARKs vs multilinear STARKs

core protocols

page topic
sumcheck the heart of the system — reducing exponential verification to logarithmic via the sumcheck protocol
polynomial-commitments the trust anchor — commit to data, prove evaluations, bind the prover to a single polynomial
fri-to-whir the PCS evolution — FRI to STIR to WHIR, each generation's insight and what it unlocks
whir the shipped commitment of the succinct profile — protocol, parameters, measured figures
recursive-brakedown a retired design: what it was and why it was unsound

architecture

page topic
superspartan CCS as universal constraint system — why AIR matters for nox and how SuperSpartan unifies them
whirlaway the architecture of the succinct profile — how sumcheck protocol, WHIR and SuperSpartan compose
trace-to-proof from a nox program to a zheng proof: the compiled relation, the machine trace, and the retired register trace
zheng-vs-starks zheng proofs and STARK systems — shared trust model, different IOP and commitment, measured figures

powers

page topic
recursion accumulation, IVC and wrap — how a nox run of any length becomes one proof of constant size
security hash-based assumptions — post-quantum guarantees, the soundness ledger explained, no trusted setup
performance measured proof sizes and verification times per profile, against the goal
bbg-integration how a proof reads BBG state — state roots, evidence, the QueryProof migration

tooling

page topic
zippel eniac/zippel as a checker for zheng's IOPs — derived transcripts, completeness and special-soundness analyses; what it cannot cover and the first experiment

see also

  • nebu — the Goldilocks field underlying all arithmetic
  • hemera — the hash primitive used in every Merkle tree and commitment
  • nox — the VM whose execution traces zheng proves
  • BBG — the state database whose integrity proofs zheng generates

Folder

Homonyms

cyberia/explanation
explanation
neural/rs/docs/explanation
explanation
soft3/foculus/docs/explanation
explanation
soft3/nox/docs/explanation
nox explanations conceptual documentation — why nox works the way it does, the design choices behind it, and the consequences that emerge. these pages illuminate the architecture. for formal definitions, see reference/. for task-oriented instructions, see docs/guides/ (when available). pages | page…
soft3/hemera/docs/explanation
why Hemera works the way it does design decisions behind the Hemera hash primitive. philosophy why-hemera — eight design principles: permanence, the tree, endofunction, self-reference, identity, unity, beauty, the name the-name — etymology: Hemera in the Protogenoi, genealogy of hash names…
soft3/radio/docs/explanation
explanation
soft3/bbg/docs/explanation
explanation
soft3/tru/docs/explanation
explanation why tru works the way it does — narrative, derivations, and background. the normative contracts live in [specs/](/soft3/tru/specs); these pages explain and motivate them, they never restate them. start here [overview](/soft3/tru/docs/explanation/overview) — what tru computes and why it…
warriors/trisha/docs/explanation
explanation why trisha works the way it does. architecture — how trisha fits in the soft3 stack gpu-backend — seven shaders, one pipeline, Metal/Vulkan/DX12 proof-file-format — TOML envelope + bincode proof bytes patching — vendor patching strategy: no fork, one script
neural/rune/docs/explanation
explanation
neural/trident/docs/explanation
💡 Trident Explanation [← Documentation Index](/neural/trident/docs/readme) Understanding-oriented. Deep dives into why Trident works the way it does, for readers who want the full picture. 🏗️ Core Architecture | Document | Description | |----------|-------------| |…
soft3/strata/genies/docs/explanation
isogeny group action arithmetic an encyclopedia of the mathematics behind genies — supersingular isogenies, class group actions, and the CSIDH construction. every concept connects back to the central operation: the commutative group action of cl(O) on supersingular elliptic curves over F_q.…
soft3/strata/kuro/docs/explanation
binary field arithmetic an encyclopedia of the mathematics behind kuro's F₂ tower — from first principles to applications. every concept is grounded in the tower we implement: F₂ → F₂² → F₂⁴ → F₂⁸ → F₂¹⁶ → F₂³² → F₂⁶⁴ → F₂¹²⁸. foundations binary-fields — field axioms in characteristic 2, GF(2) as…
cyb/honeycrisp/unimem/docs/explanation
unimem: How and Why The problem in one picture Every inference framework on macOS does this: Four buffers. Three copies. Each copy burns ~5 GB/s of memory bandwidth and adds latency. On a machine with 200 GB/s total bandwidth, three copies of a 7B model's weights eat 15% of available bandwidth…
cyb/honeycrisp/rane/docs/explanation
explanation
soft3/strata/nebu/docs/explanation
finite field arithmetic an encyclopedia of the mathematics behind the Goldilocks field — from first principles to applications. every concept is grounded in the field we implement: p = 2⁶⁴ − 2³² + 1. foundations finite-fields — field axioms, existence and uniqueness, GF(p), characteristic, the…
soft3/strata/jali/docs/explanation
polynomial ring arithmetic an encyclopedia of the mathematics behind jali's polynomial ring R_q = F_p[x]/(x^n+1) — from first principles to applications. every concept is grounded in the ring we implement: structured vectors of Goldilocks field elements with negacyclic convolution. foundations…
soft3/strata/trop/docs/explanation
tropical semiring arithmetic an encyclopedia of the mathematics behind trop's (min, +) algebra — from first principles to applications. every concept is grounded in the semiring we implement: tropical addition is min, tropical multiplication is ordinary addition, and shortest paths are matrix…

Graph