Skip to content

README.md

Latest commit

 

History

History
254 lines (179 loc) · 5.85 KB

README.md

File metadata and controls

254 lines (179 loc) · 5.85 KB

STARK-Proven sBPF Execution

This repository implements a STARK proving system from first principles that proves the correct execution of real Solana-style sBPF bytecode.

The system executes sBPF programs in a real VM, converts the execution trace into an algebraic representation, enforces correctness via AIR constraints, and produces a STARK proof verified using Fiat–Shamir, Merkle commitments, and FRI.

This is not a wrapper around an existing ZK library.

All cryptographic and algebraic components are implemented directly for learning, research, and systems understanding.

High-Level Architecture

sBPF bytecode
      ↓
Real sBPF VM execution
      ↓
Execution trace (PC, registers, opcodes)
      ↓
Algebraic trace (finite field columns)
      ↓
AIR constraints (execution correctness)
      ↓
Low-degree extension (NTT)
      ↓
Merkkle commitments
      ↓
FRI low-degree proof
      ↓
STARK proof
      ↓
Verifier (Fiat–Shamir + Merkle + AIR)

Repository Structure

.
├── bpf-tracer/          # Real sBPF execution + tracing
│   ├── src/
│   │   ├── vm.rs        # sBPF VM execution
│   │   └── trace.rs     # ExecutionTrace definition
│
├── zk-core/             # STARK system
│   ├── air/             # Algebraic Intermediate Representation
│   │   └── bpf_air.rs   # AIR for sBPF execution
│   │
│   ├── field/           # Finite field (BabyBear)
│   ├── poly/            # Polynomials + NTT
│   ├── merkle/          # Merkle trees and proofs
│   ├── fri/             # FRI low-degree protocol (skeleton)
│   ├── prover/          # Prover pipeline
│   ├── verifier/        # Verifier pipeline
│   └── crypto/          # Fiat–Shamir transcript
│
└── tests/               # Positive and negative tests

What Is Actually Implemented

1. Real sBPF Execution

  • Executes real Solana sBPF bytecode
  • Captures per-instruction state:
    • Program counter
    • Registers before and after
    • Decoded instruction metadata

This is not a toy VM.

2. Finite Field Arithmetic

Uses the BabyBear prime field:

  • p = 2^31 − 2^27 + 1 = 2013265921

Supported operations:

  • Addition
  • Subtraction
  • Multiplication
  • Inversion

Chosen for fast FFT/NTT via high 2-adicity.

3. Polynomial Arithmetic and NTT

Polynomials are represented by evaluations over a power-of-two domain.

Implemented:

  • Forward NTT (coefficients → evaluations)
  • Inverse NTT (evaluations → coefficients)
  • Correct low-degree extension (LDE):
    • Inverse NTT
    • Zero-padding
    • Forward NTT on a larger domain

This is critical for correctness.

4. AIR (Algebraic Intermediate Representation)

The AIR enforces:

  • Program counter increments correctly
  • Register values persist or update correctly
  • Instruction semantics (currently ADD)
  • Register continuity across rows
  • Boundary constraints (initial state)
  • Correct handling of padded rows via masks

If AIR constraints hold, the execution is provably correct.

5. Merkle Commitments

Commits to:

  • LDE trace columns
  • Constraint polynomials

Canonical Merkle tree:

  • Level-by-level hashing
  • Deterministic leaf layout

Supports:

  • Opening generation
  • Verification of Merkle proofs

6. Fiat–Shamir Transcript

  • Hash-based transcript
  • Deterministically derives verifier challenges
  • Ensures non-interactive soundness
  • Transcript ordering is strictly enforced

7. FRI (Low-Degree Testing)

  • Structurally correct FRI skeleton
  • Proves the combined constraint polynomial has low degree
  • Folding and commitment wiring are correct
  • Cryptographic strength is not yet optimized

8. Verifier

The verifier checks:

  • Fiat–Shamir transcript consistency
  • Merkle openings for trace and constraints
  • AIR constraint evaluations at queried rows
  • FRI low-degree proof

Both positive and negative tests are supported.

Tests and Guarantees

  • Positive Tests: Honest execution → proof verifies
  • Negative Tests: Tampered trace → verification fails

This establishes real soundness, not just compilation success.

What This Project Is (and Is Not)

This project is:

  • A correct, end-to-end STARK system
  • A real VM-level proving pipeline
  • A research-grade learning implementation
  • Architecturally aligned with real systems (Winterfell, Cairo VM, RISC-style ZK VMs)

This project is not:

  • Production-hardened
  • Optimized for performance
  • Using battle-tested cryptographic primitives
  • Suitable for mainnet deployment

Security Notes

This repository intentionally avoids external ZK libraries.

  • Hash functions and FRI parameters are simplified
  • Fiat–Shamir randomness is deterministic and minimal

Do not use in production.
This is for education, research, and systems understanding.

Current Limitations

  • Single verifier query (high soundness error)
  • Only one instruction (ADD)
  • No memory load/store AIR
  • Simplified FRI folding
  • No recursion or proof aggregation

All of these are deliberate.

Roadmap (Logical Next Steps)

  • Soundness amplification (multiple verifier queries)
  • Instruction generalization (selector-based opcode system)
  • Additional instructions: MOV, SUB, JMP
  • Memory AIR: load/store constraints
  • Performance optimizations
  • Recursive proof composition

Why This Matters

This project demonstrates a full understanding of:

  • VM execution semantics
  • Algebraic encoding of computation
  • Constraint-based correctness
  • Polynomial commitment schemes
  • STARK prover and verifier design

It is intended for engineers interested in:

  • ZK virtual machines
  • Blockchain execution layers
  • Solana core protocol research
  • Cryptographic systems engineering

Status

Correct, complete, and verified.

Further work is focused on security amplification and extensibility, not fixing correctness bugs.