HCPS: Cryptographic Foundations and Verification Status
By DEOS Team
Hash Chain Proof System (HCPS) is DEOS's zero-knowledge proof system for verifiable computation. It allows proving that a sequence of state transitions occurred correctly without revealing the intermediate states.
This post explains what HCPS is built on, what we've formally verified, and what assumptions remain.
Cryptographic Foundations
HCPS is built on peer-reviewed, battle-tested primitives:
| Component | Foundation | Used By |
|---|---|---|
| Polynomial Commitments | KZG (Kate et al., 2010) | Ethereum, EIP-4844 |
| Hash Function | Poseidon (Grassi et al., 2019) | Polygon, zkSync, Filecoin |
| Non-interactivity | Fiat-Shamir Transform (1986) | All modern ZK systems |
| Trusted Setup | Powers of Tau Ceremony | Zcash, Ethereum |
Each has been analyzed by cryptographers, deployed in production systems, and tested with billions of dollars at stake.
Security Properties
Soundness: 128-bit security (same as Ethereum's blob commitments)
Soundness error: < 2^(-234) for 1 million execution steps
Curve: BN254 (Ethereum precompile compatible)
The soundness error means: for a computation with 1 million steps, the probability of a malicious prover creating a fake proof is less than 1 in 2^234. That's astronomically small—less likely than guessing a 256-bit private key.
Formal Verification
We've created a Lean 4 formalization of HCPS that structures what we prove and identifies our cryptographic assumptions.
Main Theorem
If HCPS verification passes, there exists a valid execution trace
with probability ≥ 1 - n/2^254.
In plain English: if the proof checks out, the computation happened correctly.
What the Formalization Shows
The formalization explicitly separates two categories:
Proven structure:
- Protocol logic follows from the mathematics
- Polynomial relations are correctly constructed
- Verification equations match the protocol specification
Cryptographic assumptions:
- KZG binding (based on q-SDH hardness)
- Poseidon collision resistance
- Fiat-Shamir security (random oracle model)
Why Some Things Can't Be "Proven"
The cryptographic assumptions above are not bugs or gaps—they're the nature of cryptography.
You cannot prove "breaking AES is hard" any more than you can prove P ≠ NP. What you can do is:
- Reduce security to well-studied problems
- Show that breaking the system requires breaking those problems
- Rely on decades of cryptanalysis that hasn't found efficient attacks
This is exactly what HCPS does. Breaking HCPS requires either:
- Solving the q-SDH problem (breaks all KZG-based systems including Ethereum)
- Finding Poseidon collisions (breaks Polygon, zkSync, Filecoin)
- Breaking Fiat-Shamir (breaks essentially all non-interactive ZK)
Comparison to Production Systems
| System | Formal Verification | Security Audits |
|---|---|---|
| Zcash (Groth16) | Partial Coq proofs | Multiple |
| Ethereum (KZG) | None (academic papers) | Multiple |
| HCPS (DEOS) | Lean 4 structural proof | Planned |
Most production ZK systems have less formal verification than HCPS. Ethereum's KZG—securing billions in blob commitments—relies on academic papers and audits, not machine-checked proofs.
We're not claiming HCPS is more secure than Ethereum. We're showing that HCPS meets the same standard of rigor as systems trusted with significant value.
What This Means
HCPS uses the same cryptographic building blocks as systems securing billions of dollars. Our Lean formalization provides transparency about exactly what we assume and what we prove—something few projects in this space offer.
For production deployments:
- The cryptographic foundations are solid
- The formal structure is verified
- Third-party security audit is pending