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 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. It holds for programs over the two fields and the client’s local state, not only for labels (L-6, L-7), under the non-collusion assumption A-1.

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' generic TINI needs hold here: ⊔-upper₁, ⊔-upper₂ and ⊑-trans (secret-types N-6, the certified census). The two-point laws of N-6’s earlier reading hold too.	PROVEN	⊔-upper₁/₂, ⊑-trans, packed as Lintel.Instance.reader-sets; earlier reading: ⊔-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, over three variables: addr (the address), qn (the query name) and local (the client’s local state, which the client alone reads), for each role’s observer and for any two roles observing together: secret-types' N-7 statement, agreement read at that observer.	PROVEN	src/Lintel/Instance.agda: reader-sets (an instance of secret-types' Lattice record, secret-types#9), fields (an instance of secret-types' Vars record), field-label, tini-per-role, tini-coalition (union observer ∪)
L-7	Self-defeating privacy compositions cannot be built as programs. A typed command writes a value depending on both fields, through its expression or through the guards around it, only into a variable that the client alone may read, for any variables and labelling. With Lintel’s variables that is the client’s local state alone, and a typed command can write the link there, so the refusal is of the destination, not of every composition.	PROVEN	src/Lintel/Composition.agda: writes-flow, link-written-to-client (any variables and labelling), link-written-to-local and link-writable (Lintel’s fields); tests/reject/ProgramLink.agda (explicit), tests/reject/ProgramLinkImplicit.agda (implicit), with positive controls tests/accept/ProgramField.agda, ProgramFieldGuarded.agda and ProgramLinkLocal.agda (the same sum as ProgramLink, written into local)
A-1	Non-collusion: no party holds both the proxy and the target role. TINI holds for coalitions too (L-6), but the confinement of the link (L-4, L-7) is per role: proxy and target together see the address and the query name, each by a permitted flow, and can join them outside any program. Coalition TINI is not determinism in disguise: the coalition does not see the client’s local state, so it relates stores that differ there, and says their runs end agreeing on the address and the query name.	ASSUMED	Non-collusion, as in proven-servers protocols/proven-odns (ODNS.Types.Role); the gap is proved: Lintel.Instance.collusion-gap; coalition TINI’s content: coalition-blind, with coalition-agrees and stores-differ (two such stores)

The Lattice record is defined once, in secret-types. Lintel proves the laws and supplies 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 with the flags of scripts/proof-flags.sh, the canonical --safe --without-K --cubical-compatible (PROOF-POLICY.adoc §2.1) and --no-libraries --ignore-interfaces --double-check -W error besides, secret-types pinned at 45046c2.

Grade. The PROVEN claims (L-1 to L-4, L-6, L-7) are at Proof Witness Grade PWG-2ii (PROOF-POLICY.adoc §8) and no higher. Each is also re-proved by hand in Rocq (Coq 8.18.0) and in Lean (4.24.0, no Mathlib), on top of secret-types' own legs at the same pin, with no axioms in either. The statements are compared in verification/legs/README.adoc; Claude Code wrote that comparison, and it is provisional until the owner reviews it. bash scripts/check-legs.sh checks both legs. Not PWG-1: no per-commit receipt captures each checker’s observed result yet. L-5 is a set of checked refusals and A-1 an assumption; neither is a theorem, so neither is graded. The machine record is verification/receipts/agda-pwg_praxis.deed, generated by scripts/grade-receipt.sh and checked in CI, and the per-claim record is docs/status/PROOF-STATUS.adoc.

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.