Lintel

A privacy lattice for oblivious DNS (formerly oDNS), proved in Agda: per-field reader-set labels under which self-defeating privacy compositions are refused, built to instantiate secret-types' noninterference theorem.

Table of Contents

• What this is
• Quick start
• Repository scaffolding
• Repository map
• Where to go next
• Privacy lattice: proof status
• Licence

What this is

A Lintel label names the oblivious-DNS roles (client, proxy, target) that may observe a field, and combining fields intersects their readers. The client’s address may reach the proxy and the query name may reach the target, but the two together are the client’s alone. A composition that would show one non-client role both of them therefore needs a flow the lattice refuses. The proofs are in Agda (--safe --without-K). The noninterference theorem the lattice is built to instantiate comes from hyperpolymath/secret-types, consumed at a pinned commit.

Quick start

just            # lists every task (build, test, validate, audit, ...)
just validate   # structure + metadata checks

Repository scaffolding

Lintel was minted from rsr-template-repo, which supplies:

• Machine-readable metadata (.machine_readable/descriptiles/) — STATE, META, ECOSYSTEM, PLAYBOOK, AGENTIC, NEUROSYM, CLADE, and anchors/ANCHOR, in deed, so tools and agents can read the project’s state and boundaries.

• AI gatekeeper protocol — lintel_chora.deed (the repo deed) is the universal entry point that tells an AI agent how to work in this repo before it touches anything; it carries the AI allocation policy and the ply directory tree.

• Typed ABI/FFI seam — src/interface/Abi/ (Idris2 type + layout proofs) over src/interface/ffi/ (Zig implementation), with generated C headers.

• CI/CD — GitHub Actions for quality, security (CodeQL, Scorecard, secret scanning), multi-forge mirroring, and RSR anti-pattern enforcement.

• Supply-chain & reproducibility — container layering (stapeln), Guix shells, SBOM, and signing hooks.

• Governance — GOVERNANCE.adoc, MAINTAINERS.adoc, .github/ community health files, and a release AUDIT.adoc gate.

Repository map

The authoritative map is generated, so it cannot drift from the tree: docs/architecture/REPOSITORY-MAP.adoc (regenerate with just repo-map; CI fails if it is stale).

The short version:

Path	What lives there
README.adoc, CLAUDE.md	Start here - humans and AI agents respectively.
src/, tests/	The code and its tests.
docs/	Human documentation, including the full map above.
.machine_readable/	Manifests, contractiles and policies that tools read.
build/, Justfile	Every task runs through just; phases live in build/just/.
ci/, .github/	CI configuration; GitHub reads .github/ and no other path.

Where to go next

• The repository map — generated; what every directory is for.

• EXPLAINME — the engineering deep-dive: how the pieces actually work.

• AFFIRMATION — the dated, signed honesty snapshot of the repo’s true state.

• AUDIT — the release audit gate.

• PLACEHOLDERS — the full placeholder reference.

Privacy lattice: proof status

Lintel labels each field with the set of oblivious-DNS roles (client, proxy, target) allowed to observe it. Combining fields intersects their readers, so the client’s address (client and proxy) combined with the query name (client and target) is the client’s alone. The guarantee being built is secret-types' termination-insensitive noninterference (TINI) at this lattice, with one observer per role: two finishing runs that agree on what a role may observe end up agreeing on it. Until that instance typechecks, the claim that self-defeating privacy compositions cannot be built holds for labels, not yet for programs.

ID	Claim	Status	Artefact
L-1	A lattice, not just a poset. ⊑ is a decidable partial order, ⊔ and ⊓ are least upper and greatest lower bounds, anyone is least, and no-one is greatest and never flows down.	PROVEN	src/Lintel/Lattice.agda: ⊑-refl, ⊑-trans, ⊑-antisym, ⊔-upper₁/₂, ⊔-least, ⊓-lower₁/₂, ⊓-greatest, anyone-least, no-one-greatest, no-one-⋢-anyone, ⊑?
L-2	⊑ is reverse inclusion of reader sets. A role sees a label exactly when the label may flow to that role’s observer level.	PROVEN	⊑-readers, readers-⊑, observes-flow, flow-observes
L-3	The laws secret-types' TINI uses for its two-point lattice hold here.	PROVEN	⊔-anyone₁/₂ (⊔-L₁/₂), no-one-⊔ (H ⊔ y = H), anyone-⊔ (L ⊔ y = y)
L-4	Address and query name each reach their own role. Composed, only the client may observe them.	PROVEN	address-to-proxy, qname-to-target, link, link-confined
L-5	The typechecker refuses the self-defeating compositions and accepts the client’s.	TESTED	tests/reject/LinkToProxy.agda, tests/reject/LinkToTarget.agda, tests/accept/LinkToClient.agda, run by scripts/check.sh with a negative control
L-6	tini holds at this lattice for each role’s observer: secret-types' N-1 statement, with low-equivalence read at that observer.	OPEN	Waits on the parametric Lattice record, secret-types#9. Lintel then instantiates it at a pinned commit.
L-7	Self-defeating privacy compositions cannot be built (programs, not just labels).	DESIGNED	Follows from L-5 and L-6 once L-6 is PROVEN.
A-1	Each role is a separate observer. A party holding two roles is outside L-4 to L-7.	ASSUMED	Non-collusion, as in proven-servers protocols/proven-odns (ODNS.Types.Role)

The Lattice record is defined once, in secret-types. Lintel proves the laws and will supply the instance. just proof-check-lintel checks everything above (it runs scripts/fetch-siblings.sh then scripts/check.sh), and so does the Agda proofs workflow: Agda 2.6.4.3, --safe --without-K --no-libraries --double-check, secret-types pinned at 833715c.

Licence

Code, configuration and scripts are Mozilla Public License 2.0 (MPL-2.0); prose documentation is CC-BY-SA-4.0. Both texts live in LICENSES/, and per-file SPDX-License-Identifier headers are authoritative. The GitHub-detected licence is MPL-2.0 (the root LICENSE). Long-term attribution uses Quantum-Safe Provenance — see the Quantum-Safe Provenance exhibit.