Confidentiality labels that constrain value flow, with declassification only at explicit audited points: a standalone information-flow typing project.
Question. Which value flows does a confidentiality label permit, and what may
a lower observer learn from an output? A value type Secret ℓ A classifies a
value at a label ℓ; the first model uses a two-level Public ⊑ Secret label
order over a pure, total calculus, and the target property is
termination-insensitive noninterference between secret inputs and public
observations.
Boundary. A label is not cryptography and not an epistemic standpoint. A
Secret ℓ A does not make a value unreadable, authenticate a principal, enforce
runtime access control, or hide timing, storage or network side channels. The
baseline declassifies nothing: an ordinary Secret-to-Public flow is outside
the discipline, and any release requires a separate policy and theorem. As of
2026-10-04 no consumer and no frontier item is selected for this project.
That decision is about selection, not about existence, and the difference is
worth stating because it was measured on 2026-11-01:
metadatastician/lintel imports
SecretTypes.{Prelude,Vars,Lattice.Record,Lang,Noninterference.Generic}, defines
reader-sets : Lattice, and opens the generic TINI at it, so the estate does
have a mechanised consumer of this calculus. It is pinned at ee01db4; Lintel’s
own gate was run against this repository’s HEAD on 2026-11-01 and passes, so the
lattice re-representation described in the
proof-debt record is non-breaking for it. Recording a consumer that exists is
not a change to the 2026-10-04 decision, which stands: no consumer is selected,
and nothing here is designed around Lintel’s requirements.
The canonical statement is docs/secret-types.adoc. It records the owner decisions (D153, D154, and the 2026-10-04 confirmation of this standalone home), the first model, and the explicit non-claims.
Core theorem PROVEN (2026-10-12): termination-insensitive noninterference
for the two-point lattice, src/SecretTypes/Noninterference.agda
(tini), with the explicit and implicit flows refused by the type system
and shown to leak by computation (tests/reject/, Witness.agda). Since
2026-10-19 that theorem is an instance: typing and TINI are stated over a
Lattice record and any down-closed observer
(src/SecretTypes/Noninterference/Generic.agda), and the laws the proof
uses are certified (scripts/minimal-laws.sh) and each shown necessary
(Countermodels.agda). The fragment is a while language with fuel
semantics over any variables with decidable equality (two, lo and hi,
in the two-point development); see PROOF-STATUS.adoc. Termination is
the channel the theorem leaves open, by name.
Conjecture (not claimed): for a well-typed program, the public observer’s
Echo fibre over its outputs does not separate secret inputs — the Echo
reading of noninterference, and the first candidate connection
Secret → Echo for nextgen-typing/docs/TYPE-CONNECTIONS.adoc.
Grade. The proved claims are mathesis Grade 3 and no higher: they
type-check in Agda under the estate’s canonical strict flags
(scripts/proof-flags.sh) and have not been translated to an independent
foundational system. The Rocq and Lean recheck legs that PROOF-POLICY.adoc §2
requires for Grade 2 do not exist; they are recorded unavailable, not skipped
silently. Per-claim evidence is in the Proof
Ledger, the machine record is
verification/receipts/agda-grade3.a2ml
(checked in CI), and proof debt is empty in all four
dispositions. This paragraph states no grade the ledger does not support.
-
This repository owns the confidentiality-label definitions, the typing and observation semantics, and its own proof evidence.
-
TYPE-CONNECTIONS is the shared family map. This family’s row landed on 2026-10-05 and nextgen-typing#118 is closed, which satisfies D153’s registration requirement. A row is not a dependency: no import exists in either direction.
-
Neighbours and their limits (
epistemic-types,systemet/anytype,echo-types,tropical-types) are covered in the canonical spec. None is a dependency. They are also not one another: a confidentiality label, an epistemic standpoint, a resource grade and an Echo residue are four distinct structures, and the spec says why they stay distinct. -
The origin record stays with
epistemic-types— its boundary/history note — and it is a record, not a dependency: that repository proves no confidentiality or noninterference theorem and hosts noSecretAPI. Its issue #32 was closed by the owner on 2026-10-05T06:37Z as delivered here, with no transfer and none required; its successor guard #39 closed on 2026-10-25. Nothing is to be reopened. The transition review records the verified cross-references, keeps its 2026-10-05 text as history, and carries a 2026-11-01 reconciliation addendum.
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.