Constructor-Theoretic Crypto Program
The Central Question
Can cryptographic security be derived from the laws of physics rather than from computational hardness assumptions? Constructor Theory says yes: if cloning the full quantum state is physically impossible, then eavesdropping is physically impossible — regardless of the adversary's computational power. This makes QKD security immune to algorithmic breakthroughs, including quantum computers.
Original Researchers
Scientific Context
Traditional cryptographic security relies on computational hardness: "breaking this requires solving a problem believed to be hard." Constructor Theory provides a fundamentally stronger guarantee: security from physical impossibility. The adversary doesn't just lack an efficient algorithm — the required operation violates physical law.
The core chain: Kochen-Specker contextuality → no hidden variables → physical impossibility of global sections → superinformation (X clonable, Y clonable, XY NOT clonable) → eavesdropping requires cloning XY → eavesdropping is physically impossible.
What formalization provides: Every step in this chain is machine-checked. The CHSH inequality proves no local hidden variable model can produce quantum correlations. The Tsirelson bound establishes the quantum limit. BB84 and E91 are proved secure as instantiations of the general superinformation security theorem. Composable security ensures protocols remain safe when used as subroutines.
Project Phases
Complete formalization across 92 modules: CT core framework, constructive hardness, BB84/E91 QKD protocols, CHSH/Tsirelson bounds, composable security, QEC, entropy/privacy amplification, and photoemission physics bridge.
- ▸chsh_inequality: |S| ≤ 2 for LHV models
- ▸tsirelson_bound: |S| ≤ 2√2 for quantum strategies
- ▸bb84_secure + e91_secure: eavesdropping CT-impossible
- ▸superinfo_secure_against_eavesdropping: core theorem
Faithful translation to verified C (gcc -Wall -Wextra -Werror: 0 warnings) and safe Rust (cargo test: 13/13 pass). CT core, CHSH bounds, and QKD security proofs translated.
- ▸gcc -std=c11 -Wall -Wextra -Werror: PASS
- ▸cargo build: 0 warnings
- ▸cargo test: 13/13 pass
- ▸All 16 deterministic LHV states verified bounded
All artifacts content-addressed and pinned to IPFS. Lean proofs, verified C, safe Rust archives with CIDv1 identifiers.
- ▸Lean archive: 10 key files (7.9KB)
- ▸C archive: 3 translation units (3.1KB)
- ▸Rust archive: 5 source files + Cargo.toml (3.2KB)
- ▸SHA-256 content hashes for all archives