SOUNDNESS: Invalid transactions rejected with probability ≥ 1 - 2^(-128) PRIVACY: Cannot distinguish transactions with same public structure CONSERVATION: Σ(energy) = initial + minted - burned (mathematically enforced) QUANTUM RESIST: Hash-based security only, ~128-bit post-quantum (Grover limit)
## attack surface
Attack │ Defense ────────────────┼───────────────────────────────────────────── Double Spend │ Nullifier set prevents reuse Inflation │ Circuit enforces conservation Front-Running │ Privacy hides transaction contents Sybil │ Focus proportional to stake DoS │ Focus-based metering limits computation Eclipse │ Namespace completeness proofs Replay │ Nonces and nullifiers ensure uniqueness Forgery │ ZK proofs unforgeable without witness
## formal properties
### Turing completeness
Theorem: nox is Turing-complete.
Proof: Construct encoding of arbitrary Turing machine M via patterns 0-4, 9. ∎
### confluence
Theorem: nox is confluent.
Proof: Orthogonal rewrite system by Huet-Levy (1980). ∎
### cost determinism
Theorem: Cost is identical across all reduction orders and implementations.
Proof: By structural induction on formula. ∎
### focus conservation
Theorem: $\sum_i \text{focus}(i) = 1$ for all valid states.
Proof: All operations preserve sum; invalid transitions rejected by verification. ∎
### privacy soundness
Theorem: A valid ZK proof implies all circuit constraints are satisfied with probability $\geq 1 - 2^{-128}$.
Proof: By stark/Plonky2 soundness. ∎
### double-spend prevention
Theorem: Same record cannot be spent twice.
Proof:
1. Each record has unique (nonce, owner_secret) pair
2. Nullifier = H(nonce, owner_secret) is deterministic
3. Same record → same nullifier
4. Nullifier set is append-only
5. Transaction rejected if nullifier already in set ∎
## complexity comparison
┌─────────────────────┬───────────────┬───────────────┬───────────────┬───────────────┐ │ Operation │ Traditional │ Blockchain │ Database │ nox │ │ │ (RAM model) │ (Ethereum) │ (SQL/NoSQL) │ │ ├─────────────────────┼───────────────┼───────────────┼───────────────┼───────────────┤ │ Equality check │ O(n) compare │ O(n) compare │ O(n) compare │ O(1) hash │ │ Membership proof │ O(n) scan │ O(log n) MPT │ O(log n) index│ O(log² n) poly│ │ Completeness proof │ impossible │ impossible │ impossible │ O(log² n) poly│ │ Computation verify │ O(n) re-exec │ O(n) re-exec │ N/A │ O(log n) stark│ │ Recursive verify │ O(n) re-exec │ O(n) re-exec │ N/A │ O(1) composed │ │ Privacy + verify │ incompatible │ incompatible │ incompatible │ O(1) ZK proof │ ├─────────────────────┼───────────────┼───────────────┼───────────────┼───────────────┤ │ Cost determinism │ ✗ cache-dep │ ~ gas approx │ ✗ query-dep │ ✓ structural │ │ Parallel safety │ ✗ explicit │ ✗ sequential │ ✗ locks │ ✓ confluent │ └─────────────────────┴───────────────┴───────────────┴───────────────┴───────────────┘
see nox for the execution model, bbg for the ZK privacy architecture, zheng for proof verification