Scry Chambers

Chambers

Private worlds become partially computable without becoming public.

Why

Most of what matters is trapped behind privacy boundaries: who should meet, who should hire whom, which two labs hold techniques the other would pay for, what a decade of someone's notes actually says about them. None of it can be safely broadcast, so almost none of it is computed on. The default answer — upload everything and trust the platform — launders a lifetime of context into someone else's model.

A chamber is the other answer: a computation confined to the private worlds it has touched. Around it runs a market whose only tradable good is a bounded computation right, whose only deliverable is one symbol from a closed alphabet, whose price system is a lifetime exposure ledger, and whose settlement instrument is a court file. Nobody buys bits; people buy scoped rights and legible evidence.

Seven objects

  • Partya beneficial entity; identifiers are aliases, never the unit of governance
  • Chamberthe computation confined to the private worlds it has touched; no exit but release
  • Alphabetthe closed set of everything a counterparty can ever distinguish, failure modes included; capacity is derived, never declared
  • Contextaudience × purpose × alphabet; the disclosure state of every derivative
  • Rightthe traded good: one grant of algorithm, scope, purpose, alphabet, audience, review, and recourse — priced, revoked, audited as a unit
  • Accountthe lifetime source-by-reader exposure cell, exact integer millibits, hard ceiling
  • Court fileappend-only evidence of grants, crossings, charges, refusals, settlements — every outward claim compiles from it

Twelve axioms

Every law in canon is an axiom of this algebra, a one-line corollary, or a refusal the algebra records rather than resolves. The full statement, with its coverage map over all 146 law keys, is the Book.

  • A1 GrantAuthority moves only by an explicit ledgered grant; content, requests, and payments never carry it.
  • A2 JoinProvenance only joins; nothing shrinks a silo grade.
  • A3 AlphabetEverything a non-owner can distinguish — verdict, error, absence, timing, silence — belongs to an alphabet closed before the run, or the protocol is defective.
  • A4 PublicityAn operation is free exactly when it is computable from public values alone.
  • A5 ChargeA crossing is charged the capacity of its full outcome alphabet at the adversarial maximum.
  • A6 MeterEvery reading debits a lifetime account; a crossing that would pass the ceiling is blocked before it happens.
  • A7 ConsentA release exists only under unforgeable signatures from every party in its provenance grade, given before data enters.
  • A8 WideningA context only widens, only through a consented priced release, and never narrows back.
  • A9 LanesEvery claim carries its lane — proven, trusted, estimated, or unprovable — and estimates price, never gate.
  • A10 EvidenceEvery outward claim compiles from the court file and names its non-claims; what cannot compile cannot be said.
  • A11 RolesNo beneficial entity adjudicates a crossing it stands to gain from.
  • A12 OwnerContent crosses only on an affirmative human owner decision; exhaustion fails closed for disclosure.

Two theorems, fourteen refusals

Clearing: leakage to any observer coalition is at most the sum of charges on the crossings that reach it — provided every observable is enumerated and every schedule is fixed or public-computable. Clearing is a specification enforced by kernel and review; its soundness proof is a named open goal, not an assumption. Free post-processing: released symbols are public values; any function of them charges nothing.

The refusal register is load-bearing. No success-shaped privacy claims: a type may name an unsolved problem and record an honest "unprovable"; it may never assert the problem away with a boolean. The laws lean on named literatures — quantitative information flow and g-leakage, differential-privacy odometers, contextual integrity, Certificate Transparency, peer prediction, Shapley valuation — cited law by law in the repository. Among the fourteen refusals:

  • Identityuniqueness is unsolved; every per-entity key is Sybil-soft, the undercount visible, not prevented
  • Harmthe meter prices channel width, never damage; one bit can be a life
  • Trusted coreoperator, verifiers, reviewers, hardware roots: trusted and ledgered, not eliminated
  • Declared channelswhere no alphabet closes, the meter bounds the ledger, not the adversary — the seatbelt, not the car

The evidence floor

The accounting layer runs and is cross-verified. A Python reference and a Rust twin written from the spec alone agree bit-for-bit — 195/195 conformance decisions — because every float was exiled from the decision path. One author wrote both, with the reference sealed shut during the port; the first truly foreign twin is the standing invitation. The charge algebra's theorems (ceiling law, global cap under lease partition, settlement conservation, widening one-way-ness) are machine-checked in Lean 4, with golden traces from the reference replayed inside the proofs. All three floors verify in public CI.

python3 -m pytest -q                          # the whole floor
python3 -m chambers.pipeline.run_pipeline     # nine machines as one system
cd chambers/kernel/rust_ledger && cargo test  # the counterparty's verifier
cd chambers/lean && lake build                # the proof kernel

Status, honestly

This is a substrate and its evidence, not a hosted product. Operator-observed and reproducible-local assurance rungs are real; TEE attestation is named, not built. The soundness proof connecting the type system to quantitative information flow is a named open goal, not an assumption. The repository's IP manifest states exactly what the release gives and withholds.

Take it

The code, the Book, the specs, and the golden corpora are public at github.com/XyraSinclair/chambers under the Harvest License: use it, fork it, sell it — at most once a year the steward may ask what it has been worth to you, and any honest answer satisfies the license in full. Conformance divergences and spec ambiguities are first-class contributions; the first truly foreign reimplementation of the decision core is a standing invitation.