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.
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). The
fragment is one public and one secret variable with a while language and
fuel semantics; 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.
-
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 is proposed in nextgen-typing#118.
-
Neighbours and their limits (
epistemic-types,systemet/anytype,echo-types,tropical-types) are covered in the canonical spec. None is a dependency. -
The origin record stays with
epistemic-types: its boundary/history note and issue #32 remain open there, untransferred. The transition review records the verified cross-references and the prepared, unposted tracking updates.
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.