Papers With

← All papers
First page of Compact Shielded CSV: Post-Quantum, Private, Lightweight Client-Side Validation Blockchain

Compact Shielded CSV: Post-Quantum, Private, Lightweight Client-Side Validation Blockchain

Dragos I. Ilie, Uri Lee, Iain D. Stewart, Jonathan Zhu, Elliot Jones, William J. Knottenbelt

cs.CR Sep 25, 2026 · v1
verification cryptography
Read PDF arXiv abstract
TL;DR
Formalizes the Compact Shielded CSV blockchain protocol in Lean 4 with Mathlib, proving value preservation (safety), spendability (liveness), and no double spending.
Abstract
We propose Compact Shielded CSV, a private client-side validation blockchain for peer-to-peer payments designed for the postquantum era. Upgrading existing blockchains to quantum-resistant cryptography substantially increases on-chain overhead. By keeping all large cryptographic artifacts off-chain, Compact Shielded CSV keeps a minimal on-chain footprint independent of the size of the underlying cryptographic proofs and signatures. For a single input transaction, the onchain footprint is just 3 hashes (3x32 bytes): a nullifier, a degriefer, and a commitment to the transaction. We introduce the degriefer - a novel mechanism that enforces ownership and prevents double-spending using only hash commitments, eliminating the need for on-chain signatures entirely. These properties make Compact Shielded CSV a promising foundation for private, scalable, post-quantum digital payments.
Problem

Post-quantum signatures and proofs are much larger than classical ones, so upgrading blockchains to quantum-resistant cryptography greatly increases on-chain overhead. The goal is a private payment blockchain whose on-chain footprint does not depend on proof or signature size.

Approach

Compact Shielded CSV is a client-side validation design in which the chain acts only as a data-availability layer recording blobs of nullifiers, degriefers, and transaction commitments. A new mechanism, the degriefer, is a hash commitment binding a nullifier to the owner's secret key and the spending transaction. Off-chain validation uses it to pick the authorized spend among conflicting duplicates, so no signatures are posted on chain. The protocol rules are modeled in Lean 4 with Mathlib under abstractions such as collision-free hashing and a complete proof archive.

Results

A single-input transaction occupies 3 hashes on chain (2N+1 for N inputs). The Lean development proves invalidation soundness, value preservation, no double spending, constructive spendability, and payment progress. A correspondence table maps the paper's definitions to their Lean names.