Astrea Tech / PixelVM
The manifold's engine

Runs once.
Proves itself.

PixelVM is the engine room of the proof manifold. A typed claim fixes exactly what is being proved, one deterministic run records the work, and a compact zero-knowledge receipt binds the result to that claim — so verifiers check receipts instead of repeating computation.

typed claimscheduled executionstructured traceCHARK proofCHASM streamNeoFold compositionNeoFold/UM-QFNA compressioncompact receiptverification
01 · two separate jobs

Consensus orders the history. PixelVM proves the work

The manifold separates decisions that require shared authority from the computation behind them. Consensus chooses the authoritative history: which accepted actions count, and in what order. PixelVM handles a different question: did a registered computation follow the rules attached to its claim?

A useful picture

Consensus is the clerk who establishes the official order of forms. PixelVM is the sealed calculation sheet attached to a form. The sheet can show that the calculation followed its rules, but it does not decide where the form belongs in the official history.

Consensus authority

Validates accepted objects, chooses graph-final order, and binds that history to checkpoint evidence.

PixelVM execution proof

Turns a declared computation into deterministic traces and a verifier-facing proof artifact.

This separation keeps expensive execution and proof generation away from the consensus hot path. A verifier receives a bounded public interface instead of an invitation to trust an unstructured computation.

02 · say exactly what is proved

Typed claims make the statement explicit

A verifier needs to know exactly what a proof establishes. PixelVM starts with a typed claim: a registered object that identifies the operation, its public context, the program and schedule it uses, and the outputs it promises to establish.

Typed objects also use canonical bytes. That means one logical object has one accepted byte representation. Two machines cannot give the same claim different identities merely by changing field order, optional formatting, or another encoding choice.

Why the type matters

A blank receipt that says “correct” is nearly useless. A typed receipt says what was checked, which rules were used, and which public result belongs to that check. Canonical bytes make sure every participant is talking about the same receipt.

Registered meaning

The operation and its claim shape come from a fail-closed registry. It accepts known, well-formed claim types and rejects everything else.

Declared resources

The program carries a schedule and fuel boundary. Those declared limits keep the job's resource shape fixed while it runs.

Public boundary

The claim distinguishes verifier-visible context from declared private content. A proof can establish the public statement without making every input public.

A worked example: proving a Zcash deposit

In the bridge, crediting a deposit is a typed claim. Its registered meaning is "this shielded note pays the bridge's address, sits in Zcash's note-commitment tree at this anchor, and that anchor lies on a chain of valid headers with this much work at this confirmation depth." Its declared resources bound the header checks, the Merkle path, and the note decryption. Its public boundary names the imported Zcash root, the confirmation depth, the amount class, and the memo's commitment to an Astrea account; the note, the viewing key, and the account behind the commitment stay on the private side. Validators verify the receipt without learning whose deposit it was. The same shape proves an Ethereum finalized checkpoint and a contract slot beneath it.

CHL stands for Claim/Handoff Layer, and the name describes the job. The claim half fixes meaning, representation, and resource shape before proof work begins; the handoff half defines the exact typed package every later stage receives, so execution, proving, and verification all consume one unambiguous object instead of renegotiating what the operation means.

03 · deterministic work

A fixed schedule keeps workers in sync

PixelVM uses a small slot-scheduled runtime. A slot is a declared place for one kind of operation in the execution schedule. The compiler places work into deterministic buckets, and the runtime emits separate ordered trace streams for the parts a proof system needs to inspect.

PixelVM uses a purpose-built execution surface instead of reproducing every quirk of an ordinary processor. Its smaller instruction set is easier to schedule deterministically, turn into constraints, and connect to a stable verification interface.

01

Validate

Check the typed claim, registry entry, program, and declared bounds.

02

Schedule

Place each operation into its canonical slot and execution order.

03

Execute

Run the fixed schedule with explicit fuel and memory rules.

04

Trace

Record ordered streams that bind the claim, state, and operation results.

Heavy operations use registered coprocessors

Some operations fit a specialized component better than a long expansion into tiny generic steps. PixelVM calls these components coprocessors. Each one has a registered interface and declared trace behavior, so its result remains part of the checkable execution record.

Boundary

PixelVM is a purpose-built execution-and-proof architecture for registered deterministic computation. Generic CPU emulation, a generic zkEVM, and one normative high-level guest language sit outside this interface.

04 · from trace to receipt

Bounded chunks keep proof generation streamable

The trace describes what the runtime did. The next layer translates that record into constraints: checkable relationships that must hold when the execution is valid. PixelVM then lowers the work into bounded chunks so proof generation can proceed as a stream.

Why streaming matters

A long file can be checked in numbered blocks without loading every byte at once. PixelVM applies the same resource idea to proof work: each chunk has a bounded shape, and neighboring chunks carry the continuity needed to reassemble one statement.

ONE TYPED OPERATION · CANONICAL PROOF FLOW
claim → receipt
DECLARED STATEMENT AND SCHEDULE FIX THE MEANING Typed claim statement + public context Scheduled execution fixed slots, fuel, order Structured trace ordered subsystem streams CHARK chunks bounded proof relationships CHASM stream one ordered package NeoFold neighboring intervals compose NeoFold/UM-QFNA final compression Compact receipt bounded public interface Final verification algebraic accept or reject WORKERS MAY CHANGE · CANONICAL INTERVAL ORDER AND THE FINAL STATEMENT DO NOT
The operation moves through distinct, named stages. Streaming changes how much work a prover holds at once; ordered composition and final compression preserve the typed statement that the receipt carries.
05

Constrain

Translate the typed trace into the relationships valid execution must satisfy.

06

Chunk

Lower the trace into bounded intervals with authenticated coordinates.

07

Compose

Combine neighboring intervals in canonical order, independent of worker assignment.

08

Compress

Reduce the composed proof material to a compact public package.

09

Verify

Check the receipt against the registered claim and public context.

Canonical order fixes the final statement

Workers may take different chunks, and the reduction tree may group neighboring chunks in different ways. Each interval has a canonical position, so composition preserves one final statement. This is ordered proof reduction. Application concurrency uses a separate semantic-independence rule.

Ordered reduction many workers

Proof chunks combine by their canonical neighboring intervals. Assignment may vary; interval order and the final claim do not.

Proof compression one interface

Composed proof material becomes a smaller verifier-facing package. Compression is a separate stage with its own checks.

The product names for these layers are CHARK for the proof architecture, CHASM for its streaming accumulator, NeoFold for canonical interval composition, and NeoFold/UM-QFNA, shortened to NFUM, for final compression.

CHL · typed claims CHARK · proof architecture CHASM · streaming accumulator NeoFold · ordered composition NeoFold/UM-QFNA · final compression
05 · cryptography built for the workload

A proof stack designed as one system

The receipts that power the manifold come from a stack designed as one system. PixelVM does not bolt a general-purpose virtual machine onto an unrelated proof backend: its execution schedule, proof architecture, streaming layer, compression system, and post-quantum signature path are designed to fit together.

Why this matters

Imagine a factory where the workbench, inspection line, packing station, and shipping label were designed together. Work can move in bounded pieces, different stations can help at the same time, and the package at the end still describes one exact job.

zkCHARKContinuous-Hypercube Argument of Knowledge

CHARK proves the registered relationships in an execution. It organizes the job as packetized subsystem claims rather than one monolithic processor trace. Its multilinear, streaming architecture is distinct from the polynomial-coding pipeline commonly associated with zkSTARKs.

CHARK is transparent, so it needs no trusted setup. Inside PixelVM it replaces a STARK-style backend with an architecture shaped around slot-scheduled programs and parallel proof production; that is a system-specific design choice, not a claim that every STARK should be replaced.

GraniteProof-oriented cryptographic primitive

Astrea developed a field-native cryptographic hash-and-sampling primitive for the arithmetic CHARK already uses. That lets proof work stay in its natural arithmetic domain instead of repeatedly translating a conventional hash into proof constraints.

Granite is designed for efficient proof generation; no public benchmark or universal speed comparison is implied. Its values are bound into the proof transcript, while a standard cSHAKE seal remains the acceptance-critical cryptographic boundary.

zkCHASMContinuous Hypercube Accumulator for Streaming Multilinears

CHASM keeps CHARK streamable. It binds bounded chunks, their authenticated positions, and their continuity into one end-of-operation package. Workers can process different intervals without changing the order or meaning of the final statement.

NeoFold / NFUMOrdered composition and final compression

NeoFold combines neighboring proof intervals in canonical order. After that composition, NeoFold/UM-QFNA (NFUM) compresses the result into PixelVM's bounded verifier-facing receipt. Compression changes the amount a verifier handles, not the claim being proved.

ResonanceNative post-quantum signatures

Resonance is Astrea's signature family for post-quantum authorization at large scale. It is designed for the high-volume role that aggregate-signature systems usually serve. Signature batches enter PixelVM as typed statements, so the complete acceptance path proves the batch through CHARK and CHASM instead of trusting a native aggregate check as the final word.

Privacy evidence

The zero-knowledge simulator

The simulator rebuilds the verifier-visible transcript surface from public inputs and its own randomness, without receiving the private witness. Matching that surface is evidence for the declared zero-knowledge privacy boundary.

Correctness evidence

The algebraic verifier

The final verifier checks that the proof's mathematical relationships hold for the registered claim. Simulation cannot replace this check: privacy and correctness answer different questions.

PRIVACY EVIDENCE AND CORRECTNESS VERIFICATION
two separate questions
PRIVACY QUESTION CAN THE VISIBLE SURFACE BE REBUILT WITHOUT THE WITNESS? Public inputs no private witness ZK simulator rebuilds the visible surface Privacy evidence declared surface matches NO SUBSTITUTION BETWEEN THESE LANES CORRECTNESS QUESTION DOES THE PROOF ESTABLISH THE REGISTERED CLAIM? Proof receipt claim + public context Algebraic verifier checks proof relationships Accept or reject correctness decision
The simulator supports the declared privacy claim by reproducing the verifier-visible surface from public information. Correctness still requires the final algebraic verifier to check the proof against its registered claim.
06 · the verifier interface

One compact receipt carries the claim

A PixelVM receipt binds the registered claim, its public context, the execution statement, and the proof material needed by the selected verification profile, while declared private content stays out of the public verification input. The interface is deliberately bounded: consensus and other verifiers should not need an unstructured copy of the full execution trace.

Claim binding

The receipt identifies the typed statement and the canonical public material it covers.

Trace binding

Authenticated roots connect the public package to the scheduled execution and its ordered streams.

Policy gate

The verifier rejects an unsupported profile, malformed package, mismatched root, or out-of-policy public input.

Receipt size follows the declared proof profile and program bounds. “Compact” means the verifier receives a bounded artifact for that profile; arbitrary programs do not share one universal receipt size.

Receipt boundary

The PixelVM verifier contract requires final algebraic acceptance for the declared profile. Structural bindings, root checks, simulator evidence, and aggregate replay are safeguards within that path; none substitutes for the final proof required by the profile.

07 · security and privacy

Strong security profiles with explicit boundaries

PixelVM lets a claim declare which content is public and which content is private. The verifier can check the declared public result without receiving the private content itself. Public context and the shape of memory access can remain visible. General oblivious memory, which would hide every access pattern, lies outside this privacy claim.

Primary profile post-quantum

Astrea is engineered for 160-bit post-quantum security in its primary profile.

Absolute floor supported profiles

No supported profile falls below an absolute 128-bit post-quantum floor.

Those security statements are conditional on the declared construction, parameters, assumptions, implementation, and deployment boundary. The commitment applies to the named profile rather than every surrounding layer.

PixelVM's mathematical statements and adversarial tests have their own scopes. Astrea's machine-checked consensus theorem remains a consensus result. The proof evidence guide explains how to read both boundaries.