Version 1.3 • August 10, 2025 • CrownThrive, LLC • Patent Pending
Confidential Technical Draft. Do not distribute without written permission from CrownThrive, LLC.
Table of Contents
- Methodology — What it means to “prove CHLOM works”
- System Model & Assumptions
- Target Properties (P1–P13)
- Contract Invariants (I1–I9)
- Theorems & Proof Sketches
- Mechanization Plan (TLA+ & Tests)
- Economic Calibration
- Stress Cases & Resolutions
- Security, Privacy & Threat Model
- Architecture Overview
- Governance & Dispute Flows
- Audit & Compliance Artifacts
- Implementation Checklist Appendices A–F (Formal statements, examples, TLA+ skeleton, pre/post conditions, risk register, change log)
1) Methodology — What it means to “prove CHLOM works”
We fix a formal model of entities, contracts, oracles, and a BFT ledger. We specify precise properties (safety, liveness, privacy, conservation, attribution, incentives), prove them under standard cryptographic and distributed-systems assumptions, and bind proofs to engineering artifacts (pre/post-conditions, TLA+ invariants, ZK constraints, slashing economics). The outcome is a specification auditors can model-check and developers can implement with property-based tests.
2) System Model & Assumptions
2.1 Cryptographic primitives
H : {0,1}* → {0,1}^k (collision‑resistant)
EUF‑CMA signature scheme (Sign, Verify)
ZK Proof system: soundness + zero‑knowledge
2.2 Ledger & time
A permissioned or permissionless BFT ledger with safety and liveness for f < n/3. Time is discrete by block height. “Finalized” means not revertible without violating BFT safety.
2.3 Entities & roles
Principals (creators, licensees, sublicensees, validators). Public DID Registry maps authorized public keys to public identifiers. DIDs are public-facing and used for authorization and attribution. Any internal device/person fingerprints, if used, remain private off‑chain and are not required by this proof.
2.4 Contracts & state
License contract with state {Draft, Active, Suspended, Revoked, Expired}, counters (used, cap), and a monotone nonce. Splitter with weights vector. Override Tree (rooted, acyclic). Registry (roles ↔ keys). Treasury (receipts + disbursements). Governance (state transitions from evidence and ZK verifications).
2.5 Compliance & privacy
A policy predicate C(x) over private usage data x. Holders present ZK proofs that C holds without revealing x. On‑chain verifier admits or rejects advancement.
2.6 Economics
Actors with enforcement power stake S with slashing factor s and are subject to detection probability p. Illicit gain G is upper‑bounded via modeling and calibration.
3) Target Properties (P1–P13)
P1 Value Conservation P2 Capacity Safety P3 Attribution Uniqueness P4 ZK‑Compliance Correctness & Privacy P5 Eventual Enforcement (Liveness) P6 Incentive‑Compatibility P7 Audit Immutability P8 Compositional Compliance P9 Batch‑Order Invariance (new) P10 Subtree‑Revocation Conservation (new) P11 Rounding‑Error Bound (new) P12 Collusion Thresholds (new) P13 Oracle Accountability (new)
4) Contract Invariants (I1–I9)
I1 Splitter Sum (weights sum to 1; non‑negative) I2 Capacity (0 ≤ used ≤ cap) I3 Nonce Monotonicity I4 Authorization (DID‑authorized signatures) I5 Audit Link Uniqueness I6 ZK Acceptance ⇒ Policy Holds I7 Override Graph is a Tree I8 Replay‑Resistance (nonce in tx) I9 Finality‑only Reads
5) Theorems & Proof Sketches
Theorems T1–T15 correspond to P1–P13 and rely on I1–I9 and the system assumptions. Sketches are preserved and tightened for clarity; full formalization is left to the TLA+/SMT stage.
T1 — Value Conservation (Splitter)
Σ_i w_i = 1 ⇒ Σ_i w_i B = B
Proof uses linearity and I1.
T2 — Override Correctness on a Tree Payouts follow unique path products in a rooted tree; telescoping sum ensures conservation.
T3 — Capacity Safety With finality, monotone nonce, and explicit guard, cap cannot be exceeded in finalized history.
T4 — Attribution Uniqueness (DID)
DID = H(pk ∥ salt)
Collision requires breaking H.
T5 — ZK Compliance Correctness & Privacy Soundness ensures truth; zero‑knowledge ensures no leakage beyond validity.
T6 — Eventual Enforcement (Liveness) BFT liveness implies bounded‑round finalization of valid enforcement.
T7 — Incentive‑Compatibility (Single Actor)
EU = G − p·s·S ⇒ S ≥ G/(p s) for non‑profitability
T8 — Audit Immutability Finalized events cannot be altered without violating BFT safety.
T9 — Compositional Compliance Conjunction of accepted ZK predicates implies all policies hold.
T10 — Batch‑Order Invariance (New) Addition associativity/commutativity renders totals independent of ordering/batching.
T11 — Subtree‑Revocation Conservation (New) Revoking a connected subtree disables future flows to it while preserving conservation for valid sales outside the subtree.
T12 — Rounding‑Error Bound (New)
w_i = a_i/D, Σ a_i = D, r = B − Σ ⌊a_i B / D⌋, 0 ≤ r ≤ m − 1
Conservation holds by design; residuals go to a deterministic sink.
T13 — Collusion Thresholds (New) Censorship requires ≥1/3; safety break ≥2/3; slashing economics calibrated so attacks are irrational.
T14 — Oracle Accountability (New)
p_detect · s_V · S_V ≥ benefit_of_successful_lie
T15 — Cross‑Chain Settlement Safety (Optional) Light‑client proof of finality lifts conservation and immutability across chains.
6) Mechanization Plan (TLA+ & Tests)
6.1 TLA+ module skeleton
------------------------------- MODULE CHLOM -------------------------------
EXTENDS Naturals, Sequences
CONSTANTS Roles, Keys, DIDs, Nodes
VARIABLES state, used, cap, nonce, weights, tree, ledger
Init == /\ Sum(weights) = 1 /\ used = 0 /\ nonce = 0 /\ Tree(tree)
Next == \E a \in Actions : Action(a)
InvSplitSumOne == Sum(weights) = 1
InvCapSafe == 0 <= used /\ used <= cap
InvNonceMonotone == nonce' = nonce + 1
InvAuthKey == Authorized(ledger, DIDs, Keys)
InvAuditLinkUnique == UniqueLinks(ledger)
InvZKImpliesPolicy == VerifyZK => PolicyHolds
InvTreeAcyclic == Tree(tree)
InvReplayResist == NonceFresh(ledger, nonce)
InvFinalityOnly == FinalityReads(ledger)
============================================================================
6.2 Property‑based & unit tests (Foundry/SMT)
Test families: split_sum_eq_1; cap_guard; rounding_residual_bound; batch_order_invariance; revoke_subtree_no_leakage; zk_gate_required; nonce_replay_reject; auth_required; audit_link_unique.
7) Economic Calibration
Calibrate S, s, p by actor role, with conservative G bounds. Use Monte‑Carlo to validate negative expected value for misbehavior; extend to coalitions.
S ≥ G/(p s)
Coalition: choose s such that for plausible G and S_c, G ≤ s·S_c is hard to satisfy.
Deterministic residual policy for rounding; publish parameter ranges and change controls.
8) Stress Cases & Resolutions
Simultaneous finalize near cap → only one succeeds; others revert (nonce + finality). Partial refunds & rounding → residual ≤ m − 1 and deterministic sink avoids disputes. Batch payouts & MEV → totals invariant; per‑tx receipts prevent micro‑level disputes. Revocation storms → subtree revocation guarantees no leakage; past payouts remain immutable. Oracle griefing → deposits and slashing make misreports negative EV.
9) Security, Privacy & Threat Model
Adversaries: rational participants seeking MEV, malicious oracles, validator coalitions, off‑chain data tampering, bridge forgeries. Mitigations: I1–I9; T7, T10, T13, T14, T15; receipts; audits; light‑client proofs; stake/slash.
Non‑goals: deanonymizing users; storing private fingerprints on‑chain; punitive slashing without evidence.
Privacy boundary: DIDs are public; any internal device/person fingerprints remain private off‑chain.
10) Architecture Overview
Actors: Creator/Owner, Licensee, Sublicensee, Validator, Oracles (A/V), Governance, Treasury. Core flow: License activation → ZK‑gated usage → capacity guard → payouts via Splitter and Override Tree → audit events → potential governance actions (slash/suspend/revoke).
11) Governance & Dispute Flows
Violations are submitted with deposits. Governance verifies evidence; on false reports, oracles are slashed; on true reports, violators are penalized, and reporters rewarded. Subtree revocation disables future flows to the affected branch without retroactive clawback of finalized payouts.
12) Audit & Compliance Artifacts
Event schema includes DID of actor, license ID, nonce, usage delta, proof verifier hash, payout vector hash, and override path hash. Receipts are per‑transaction, signed, and linked to finalized blocks.
13) Implementation Checklist
• Complete TLA+ model and TLC runs for I1–I9 and liveness. • Implement Foundry property tests listed in §6.2. • Deliver ZK circuits for representative predicates and verifier integration. • Publish economic parameter ranges and residual policy. • If bridging, integrate light‑client proofs and document bridge assumptions.
Appendix A — Formal Statements (raw)
Σ_i w_i = 1, w_i ≥ 0
0 ≤ used ≤ cap, nonce' = nonce + 1
DID = H(pk ∥ salt)
Verify(π, vk) ∈ {⊤, ⊥}
S ≥ G/(p s)
Appendix B — Worked Example (rounding bound)
D = 10^6, B = 1,234,567, a = [200000, 300000, 500000]
Pay_1 = ⌊200000 * B / D⌋ = 246,913
Pay_2 = ⌊300000 * B / D⌋ = 370,370
Pay_3 = ⌊500000 * B / D⌋ = 617,283
Σ Pay_i = 1,234,566; r = 1 ≤ m − 1
Appendix C — TLA+ invariant names (index)
InvSplitSumOne; InvCapSafe; InvNonceMonotone; InvAuthKey; InvAuditLinkUnique; InvZKImpliesPolicy; InvTreeAcyclic; InvReplayResist; InvFinalityOnly.
Appendix D — Example pre/post‑conditions (Solidity/Vyper style)
require(sum(w) == 1e18 && all(w_i ≥ 0))
require(used + Δ ≤ cap && nonce' == nonce + 1)
require(VerifyZK(π, vk))
Appendix E — Risk Register (excerpt)
MEV ordering games → totals invariant but micro‑allocation debates; mitigation: receipts + documented invariance. Oracle collusion → deposits + slashing + auditability. Bridge spoofing → light‑client proofs only. Parameter drift → governance‑controlled bounds + on‑chain registry of parameters.
Appendix G — TLA+ Quick Glossary & Primer (1‑page)
Purpose
This appendix equips auditors and engineers to read the CHLOM TLA+ spec quickly and interpret TLC results without ambiguity.
Core concepts
State and behaviors: a system run is a sequence of states; each step changes variables according to actions.
VARIABLES state, used, cap, nonce, weights, tree, ledger
Initialization: defines all legal starting states.
Init == /\ Sum(weights) = 1 /\ used = 0 /\ nonce = 0 /\ Tree(tree)
Next‑state relation: a disjunction of actions describing allowed transitions.
Next == \/ Advance
\/ RecordUsage
\/ Payout
\/ RevokeSubtree
\/ VerifyZK
Spec and stuttering: full behavior includes stuttering on unchanged variables.
Spec == Init /\ [][Next]_<<state, used, cap, nonce, weights, tree, ledger>>
Invariants (safety): properties that must hold in all reachable states.
InvCapSafe == 0 <= used /\ used <= cap
InvSplitSumOne == Sum(weights) = 1
InvTreeAcyclic == Tree(tree)
InvAuthKey == Authorized(ledger)
InvZKImpliesPolicy == VerifyZK => PolicyHolds
Temporal operators (TLA notation)
[] P \* "Always P" (safety)
<> P \* "Eventually P" (liveness)
P ~> Q \* "Leads‑to": whenever P, eventually Q
WF_v(A) \* Weak fairness: if A is continuously enabled, it eventually occurs
SF_v(A) \* Strong fairness: if A is enabled infinitely often, it occurs infinitely often
Liveness in CHLOM
We assert eventual inclusion/finality of valid enforcement actions.
EnforcementLiveness == [] (ValidReport => <> Finalized)
Parameters and bounds
Constants (e.g., max tree size, cap ranges) are set in the TLC model to bound the state space for exhaustive exploration.
TLC model checking workflow
- Choose constants/bounds; 2) list invariants and temporal properties; 3) run TLC; 4) inspect counterexample traces; 5) tighten guards or invariants and re‑run.
Reading TLC output
A failing invariant includes a shortest counterexample trace. Replay each step against the spec; the failing state violates the corresponding CHLOM guard. Keep failing traces as regression tests.
Mapping to CHLOM properties
P2 ↔ InvCapSafe; P1 ↔ InvSplitSumOne; P8 ↔ conjunction of ZK gates; P7 ↔ finality‑only reads; P5 ↔ EnforcementLiveness with fairness on inclusion actions.
Example minimal skeleton (for quick sanity checks)
------------------------------- MODULE CHLOM_MIN -------------------------------
EXTENDS Naturals
VARIABLES used, cap, nonce
Init == used = 0 /\ nonce = 0 /\ cap \in Nat
RecordUsage == /\ used' = used + 1 /\ used' <= cap /\ nonce' = nonce + 1 /\ cap' = cap
NoOp == used' = used /\ nonce' = nonce /\ cap' = cap
Next == RecordUsage \/ NoOp
Spec == Init /\ [][Next]_<<used, cap, nonce>>
InvCapSafe == 0 <= used /\ used <= cap
===============================================================================
Appendix H — DLA Quick Primer (Governance & Enforcement)
Purpose
This appendix explains the Decentralized Licensing Authority (DLA) used by CHLOM for governance, enforcement, and disputes.
Roles
DLA Council (governors). Validators. Oracles A/V. Reporter. Respondent (accused party). Treasury. Arbiter (optional advisory role).
Deposits, rewards, slashing
EV(misreport) = benefit_lie − p_detect · s_V · S_V
Set deposits S_V and slashing s_V so EV(misreport) < 0 under conservative p_detect. Reporters of valid violations receive rewards R from penalties; false reporters are slashed.
Core actions
FileViolation. AdmitOrDispute. EvidenceWindow. CouncilVote. Resolve. SlashOrReward. RevokeSubtree. Reinstate.
Quorum and thresholds
Define quorum q and decision threshold θ (e.g., θ = 2/3 of quorum). Emergency actions require higher θ and recorded rationale. All thresholds are published in the parameter registry.
Due process
Notice to respondent. Evidence access. Fixed response window. Right to appeal to a higher quorum. Time‑boxed stages to ensure liveness.
Evidence standards
Cryptographic proofs, signed attestations, finalized block references, ZK verifier hashes. Off‑chain materials must be hashed and time‑stamped.
Appendix I — DLA Governance State Machine (ASCII)
States and transitions at a glance.
[Clean] --(ViolationFiled + Deposit)--> [UnderInvestigation]
| |
| (NoEvidence / Timeout) | (SufficientEvidence)
v v
[Dismissed] <------------------------- [CouncilVote]
^ |
| (AppealGranted) | (Resolve: Slash/Reward)
| v
[Reinstated] <---(Remediation)--- [Suspended] --(NonRemedy/Timeout)--> [Revoked]
\
\--(RemedyComplete)--> [Reinstated]
Timeouts are enforced to guarantee liveness. Finalized states emit immutable audit events.
Appendix J — Event & Storage Schema (on‑chain and logs)
On‑chain structs and log shapes. Field names are canonical for audits.
struct License { bytes32 id; uint256 cap; uint256 used; uint64 nonce; uint8 state; bytes32 ownerDID; }
struct Splitter { bytes32 id; bytes32 licenseId; bytes32 weightsHash; }
struct Payout { bytes32 id; bytes32 licenseId; uint256 base; bytes32 weightsHash; bytes32 overridePathHash; bytes32 receiptId; }
struct Receipt { bytes32 id; bytes32 txHash; uint64 block; bytes32 verifierHash; bytes32 actorDID; }
struct Violation { bytes32 id; bytes32 licenseId; bytes32 reporter; bytes32 respondent; bytes32 evidenceHash; uint64 filedAt; }
struct OracleDeposit { address oracle; uint256 amount; uint64 lockedAt; }
struct Vote { bytes32 id; bytes32 caseId; address voter; uint8 decision; }
struct Revocation { bytes32 id; bytes32 subtreeRoot; uint64 when; }
Hashes are Merkle or keccak256 depending on chain. All receipts point to finalized blocks.
Appendix K — Foundry Test Matrix (coverage map)
Each test asserts an invariant or property with explicit pass criteria.
ID, Area, Property, Setup, Action, Expected
T01, Splitter, Σw=1, random weights sum, create, assert(sum==1e18)
T02, Splitter, Conservation, base B split, payout, Σpayouts+r == B
T03, Capacity, CapGuard, used≈cap, recordUsage(Δ), revert if used+Δ>cap
T04, Nonce, Monotone, any, replay tx, revert
T05, ZK, Gate, invalid proof, advance, revert
T06, ZK, Gate, valid proof, advance, succeed
T07, Override, PathProduct, simple tree, disburse, payouts match products
T08, Revocation, NoLeakage, subtree revoked, disburse, zero to revoked nodes
T09, Batch, OrderInvariant, permute txs, settle, totals equal
T10, Rounding, ResidualBound, random B,D,m, payout, residual ≤ m−1
T11, Oracle, Accountability, false report, resolve, slash reporter
T12, Liveness, EventualFinal, valid report, mine blocks, finalized within bound
Appendix L — Parameter Registry & Change Control
A versioned on‑chain registry records governance parameters: quorum q, threshold θ, deposits S_V, slashing s_V, reward R, appeal windows, residual policy, batch window. Changes require a formal proposal, council vote, and a freeze window before activation. Emergency changes are allowed with higher thresholds and immediate post‑mortem.
Appendix O — Recommended Parameter Defaults (CrownThrive baseline)
Purpose
These initial values are conservative, designed to make attacks economically irrational while keeping governance responsive. Tune per‑network.
Governance
q (quorum) = 9 θ (decision threshold) = 2/3 of q (rounded up) Emergency threshold θ_E = 4/5 of q Appeal window = 72 hours Evidence window = 48 hours Freeze window after parameter change = 24 hours
Economics
S_V (oracle deposit) = 5,000 units (native‑token) s_V (oracle slashing factor) = 0.6 R (reporter reward) = 0.35 × penalty collected S_validator (governance stake) = 25,000 units s_validator = 0.5 p_detect (effective detection probability) baseline = 0.65 (stacked detectors)
Settlement
Batch window = 5 minutes Residual policy = deterministic sink to creator Fixed‑point scale D = 10^6 for rounding proofs Weights scale ONE = 1e18 for Splitter math
Safety notes
Increase S_V and s_V if false‑positive griefing appears. For small networks, use higher θ_E and longer evidence windows until oracle reputation matures.
Appendix P — Downloadable Artifacts (TLC model & Foundry scaffold)
TLC model (minimal)
Use this as a starting point to stand up TLC and validate invariants.
File: CHLOM_TLC_Min.tla
Includes foundry.toml, src/ helpers, and test/CHLOMSpec.t.sol with basic property tests.
File: foundry_chlom_scaffold.zip
Integration tips
- Unzip the scaffold, run
- Wire your contracts to
- Extend tests to cover subtree revocation and order invariance in your settlement module.
A versioned on‑chain registry records governance parameters: quorum q, threshold θ, deposits S_V, slashing s_V, reward R, appeal windows, residual policy, batch window. Changes require a formal proposal, council vote, and a freeze window before activation. Emergency changes are allowed with higher thresholds and immediate post‑mortem.
Appendix M — Auditor Checklist (field guide)
- Verify invariants I1–I9 in TLC outputs.
- Confirm batch‑order invariance with randomized settlement traces.
- Check rounding residual logs never exceed m−1 and are conserved.
- Verify DID collisions are not observed in sampled registry (hash diversification via salt).
- Walk one violation case end‑to‑end: deposits, vote, resolution, events.
- Confirm parameter registry values match docs and change log.
Appendix N — Notation & Symbols
Plain‑text conventions and symbols used across the BlackPaper.
Σ sum; Π product; ⌊x⌋ floor; ⇒ implies; ↔ iff; ⊤/⊥ true/false
[]P always P; <>P eventually P; P ~> Q leads‑to; /\ and; \/ or
Appendix F — Change Log
v1.3 — Added DLA Quick Primer (Appendix H), Governance State Machine (Appendix I), Event & Storage Schema (Appendix J), Foundry Test Matrix (Appendix K), Parameter Registry & Change Control (Appendix L), Auditor Checklist (Appendix M), and Notation & Symbols (Appendix N). Updated header to v1.3. v1.2 — Added TLA+ glossary and one‑page primer (Appendix G) to aid auditors; tightened code‑block usage to formulas/code only. v1.1 — Reformatted for readability; prose moved out of code blocks; added ToC, governance/dispute flows, audit artifacts, and non‑goals/privacy boundary. v1.0 — Initial master BlackPaper draft.
Attachments
Legal & Protective Notice
This BlackPaper documents proprietary algorithms, state machines, and economic designs for CHLOM. Uniqueness stems from the composition of ZK compliance gates, override‑tree payouts with subtree revocation guarantees, batch‑order invariance, and calibrated staking/slashing proving negative EV for deviations.
All rights reserved. CrownThrive, LLC. Patent Pending.