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.

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.