Reference
Every reference document, rendered verbatim from the markdown in the repository. The files here are the same ones an implementer reads — the specification is normative, and the rest explain why it says what it says.
Protocol
The specification
The normative kernel spec: identity encoding, the gate, verdicts, the journal, signed publication, namespace authority, licence evaluation, and conformance. This is the document a second implementation is written against.
Releases
Release notes for each version, stating identity stability first — whether artifact hashes moved is the only question that matters when upgrading a content-addressed system.
Publishing
The practical path: get a key, reserve a namespace, publish under it, delegate publication to CI, and propose an addition to the standard library.
The authority model
Why authority is a principal, why reservations are explicit while exact-name ownership is inferred, why retention beats denial, and what a third party can check from the journal alone.
Licensing
Licensing as an evidence domain: publishers assert signed terms, the registry derives what a composition permits, and UNSTATED is never permission.
Effects and capabilities
The capability model: what a definition may touch, and how confinement is checked.
Model
Discovery
Finding proven code by property content-hash rather than by name — and the invariant that discovery never touches identity.
Generics
Dictionary passing: a type class is a capability record, and combinators are proven over all dictionaries.
Floats
IEEE-754 binary64 identity: bit-identity, canonical NaN, and why == is Leibniz equality.
Integers
Int is ℤ — arbitrary precision, no overflow, and what that costs.
Strings
Str as an inductive datatype rather than a primitive, and why the string primitives were deleted.
Sets and maps
Set and Map compiled to native hash maps, differentially gated against the structural definitions.
Refinement types
Design only: why refinement identity is syntactic, and why logically-equal refinements are related by discovery rather than by identity.
Semantic canonicalization
Body-equivalence via AC-normalization, type-directed — the e-graph behind find --equiv.
Operating a registry
Registry authentication
Signatures as principals, capability-limited bearer tokens, and why both exist.
Verification workers
Proving require_proven names out of band, in dependency order, gated on a proof-state fingerprint.
The team store
The hosted layer: authenticated principals, repoint policy, and what a blocked submission records.
Store drivers
The backend seam: filesystem, in-memory, and the GCS-objects plus Postgres-index cloud driver.
Corpus and registry
Why the committed corpus and the live registry are different objects, and the declared policy that accounts for every name rather than forcing them equal.
Deploying a registry
The GCP walkthrough: keyless deploy from CI, custom domain, managed TLS.