docs(security): land secret-types research note

CHANGELOG.adoc

@@ -34,6 +34,12 @@ the changelog records what is actually proved, not what is aspired to.
   A fixity declaration only; no definition changed.
 * New documentation: `docs/applications/rapidnj-q-criterion.adoc`, plus README,
   documentation-index, proof-status and machine-readable state updates.
+* Added `docs/secret-types.adoc` as an in-repository research note for the
+  security-polarity direction (issue #29). It corrects the preserved draft's
+  scope against the current APIs, makes no security-implementation claim, and
+  sets out staged proof and runtime obligations. README and documentation
+  index link to the note; no Agda API changed and the retired `AUDIT.adoc` was
+  not restored.
 
 [[fixed--2026-09-07]]
 ==== Fixed — 2026-09-07

README.adoc

@@ -202,6 +202,9 @@ This is a prototype, not a complete epistemic logic. The following are **intenti
   transport that would lift the integer certificate to rational input
 * Cross-iteration reuse of a skip bound, and the row-insertion update that
   maintains the scan invariants (`Applications.RapidNJSkip.WeakeningObligation`)
+* Confidentiality labels, secret types, declassification, and noninterference;
+  see link:docs/secret-types.adoc[the security-polarity research note] for the
+  current scope and proposed route
 
 == Build
 
@@ -223,6 +226,7 @@ agda --no-libraries -i src src/EpistemicTypes/All.agda
 * link:docs/continuity-foundations.adoc[Continuity foundations] — store coherence, retained information, bounds, and next obligations
 * link:docs/proof-transport.adoc[Proof transport] — semantic verification across boundaries
 * link:docs/applications/rapidnj-q-criterion.adoc[Applications: the RapidNJ Q-criterion] — the bound, the skip warrant, the exact-arithmetic obligation
+* link:docs/secret-types.adoc[Secret types] — a scoped research direction and staged route to a future security model
 
 == License
 

docs/README.adoc

@@ -34,6 +34,11 @@ authority.
   downgrades a sender's `Proof` to a receiver's `Receipt`, how `verify` upgrades
   `Data` to `Proof` only with the receiver's own checker plus evidence, and the
   public / designated / receipt distinctions.
+
+| `docs/secret-types.adoc`
+| A scoped research direction for security-polarity / secret types: what the
+  current epistemic, warrant, and Echo interfaces do and do not establish, plus
+  a staged route to an in-repository security model.
 |===
 
 == Continuity foundations

docs/secret-types.adoc

@@ -0,0 +1,177 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Secret Types: a security-polarity research direction
+:toc: macro
+:toclevels: 3
+:icons: font
+:revdate: 2026-09-27
+
+[abstract]
+This note keeps the secret-types direction inside `epistemic-types` and sets out
+a cautious route from the current epistemic interfaces to a possible formal
+information-flow model. It is a design note, not an implemented security API:
+there is no `Secret` type, security-label lattice, declassification mechanism, or
+noninterference result in this repository today.
+
+toc::[]
+
+== Decision and scope
+
+The land-or-retire decision recorded in issue #29 is to **land this research
+direction in this repository**, rather than create a new repository. The
+preserved note is reworked here against the current source and proof boundaries.
+It is a research connection to the existing epistemic core, not evidence that a
+security model is already implemented or proved.
+
+This file is therefore a roadmap and an explicitly unformalized research note.
+It does not change the public Agda API, promise a particular design, or make a
+security guarantee about a program or runtime. The retired `AUDIT.adoc` is not
+part of this decision and is not restored.
+
+== What the repository currently provides
+
+The current code offers concepts that may be useful when designing a security
+model, but their present meanings are narrower:
+
+* `Modality` in `src/EpistemicTypes/Base.agda` is an indexed family `E κ A`
+  with a mapping operation. It does not assign confidentiality labels or
+  restrict who can observe a value.
+* `Access.Preorder` and `AccessibleModality.increase` in
+  `src/EpistemicTypes/Access.agda` let an instance interpret an order and
+  transport `E κ A` along it. The example reading is epistemic access from a
+  less-informed to a more-informed standpoint. The generic preorder does not
+  specify a security policy or a clearance lattice.
+* `BeliefModality` omits a `reflect` field. This says that the generic record
+  interface does not provide a factivity operation. It does **not** hide a
+  concrete representation, prevent pattern matching, stop a client from
+  exposing data through another operation, or establish confidentiality.
+* `FactiveModality.reflect : E κ A -> A` is an epistemic factivity interface.
+  It is not a declassification policy. Conversely, omitting `reflect` is not,
+  by itself, an information-flow proof.
+* `Warrant` separates evidence tokens from an explicit soundness map, and
+  `ProofTransport` proves claims relative to a caller-supplied meaning and
+  checker. Neither module models secrecy, identity, cryptography, or a physical
+  access-control system.
+* `Echo` certificates relate a residue to an observation under a supplied
+  contract. `BoundedEcho` bounds a supplied residue measure. Its grade is not
+  inherently a number of leaked bits, entropy, or a declassification budget;
+  such a meaning would need its own measure and theorem. See
+  link:continuity-foundations.adoc[continuity foundations].
+
+At this revision, the proof gate recursively checks the Agda modules under
+`src/EpistemicTypes/` (17 source modules) using `--safe --without-K`, with no
+standard-library dependency. These proofs establish only the propositions
+encoded in those modules. Safe type-checking is not a general security
+certification, and it does not supply missing security semantics.
+
+== A possible security interpretation
+
+A future model could reuse the idea of indexing a value by a standpoint, but it
+must state a security policy rather than silently identify it with the existing
+epistemic preorder. One possible convention is:
+
+* labels form an ordered set with `ℓ ⊑ ℓ'` meaning that `ℓ'` is at least as
+  restrictive as `ℓ`;
+* `⊥` is public and higher labels require greater clearance;
+* a value classified at `ℓ` can be read at clearance `c` only when there is an
+  explicit witness of `ℓ ⊑ c`;
+* raising a label from `ℓ` to `ℓ'` when `ℓ ⊑ ℓ'` is safe classification (taint
+  moves upward); combining values uses a join so the result is no less
+  restrictive than either input.
+
+Under that convention, schematic signatures (not compile-ready Agda) might
+resemble:
+
+[source,text]
+----
+Secret       : Label -> Set -> Set
+raise        : ℓ ⊑ ℓ' -> Secret ℓ A -> Secret ℓ' A
+combine      : Secret ℓ A -> Secret m B -> Secret (ℓ ⊔ m) (A × B)
+readAt       : ℓ ⊑ clearance -> Secret ℓ A -> A
+----
+
+This is only a sketch. It leaves open how values are represented, how the
+constructor is hidden, what a clearance witness means, how a runtime enforces
+it, and which observations an attacker can make. In particular, a proof of
+`ℓ ⊑ clearance` is meaningful only relative to a correctly specified label
+model and trusted construction of its witnesses. The order direction is a
+design choice that must be documented consistently in code and examples.
+
+Declassification would need a separate, explicit policy boundary. It should
+not be modelled as an unrestricted `reflect` or as an ordinary safe label raise:
+a release rule needs to say who may release what, under which evidence or
+capability, and what property is preserved by that release. The initial model
+could instead omit declassification entirely.
+
+== What is not claimed
+
+This note does not claim that the following exist or have been proved here:
+
+* a `SecurityLattice`, `Secret`, `classify`, `declassify`, or clearance API;
+* a confidentiality or information-flow policy, or a proof that forbidden
+  flows cannot occur;
+* noninterference, quantitative leakage, secure erasure, zeroization, or
+  resistance to timing, cache, storage, network, or other side channels;
+* linear or single-use handling of secret values;
+* a connection from `EchoBridge.Grade` to bits, entropy, or a security budget;
+* a transfer of proof from another repository's algebra, type checker, or
+  runtime into this Agda development.
+
+The preserved draft proposed links to neighbouring formal and runtime projects.
+Those may be useful inputs, but they are not dependencies of this repository and
+their results are not reproduced by its current CI. Any future integration must
+name exact source revisions, state the compatibility claim, and add a
+reproducible check before the project relies on it.
+
+== Route forward
+
+The route below is staged so that prose, a type-level discipline, and a runtime
+security claim are not conflated. Later stages depend on earlier decisions; this
+list is a proposal, not a commitment to implement every stage.
+
+. **Specify the model and threat boundary.** Choose a concrete use case, label
+  order and its direction, principals and clearances, observable outputs,
+  attacker capabilities, permitted flows, and whether declassification is in
+  scope. State the security property to prove (for example, a clearly defined
+  noninterference relation) before choosing type constructors.
+. **Add the smallest in-repository Agda interface.** If the specification
+  warrants it, introduce a `SecurityLattice` and an abstract secret wrapper in
+  a focused module (a possible location is
+  `src/EpistemicTypes/Secret.agda`). Decide explicitly whether the existing
+  `Preorder` is reusable or whether security needs a distinct interface. Define
+  only the operations justified by the model: safe label raising, combination
+  at a join, and reading under a proved clearance. Keep declassification out
+  until its policy is specified.
+. **Add positive and negative proof controls.** Prove the permitted operations
+  under `--safe --without-K --no-libraries`; add regression fixtures showing
+  that a lower-clearance read, an implicit downgrade, and an unauthorized
+  release are rejected. The recursive proof gate must include every new module
+  and the expected-rejection gate must distinguish a real policy failure from
+  a broken import or tool invocation.
+. **Prove the semantic security property.** Give the labels and program
+  observations an explicit semantics. Prove a policy-appropriate theorem such
+  as noninterference, with any permitted declassification reflected in the
+  theorem's assumptions and conclusion. Type-level encapsulation alone is not
+  that theorem.
+. **Treat runtime guarantees as a separate integration.** Only after the model
+  and theorem are clear should a concrete runtime, linearity discipline,
+  resource/leakage measure, or external grade algebra be connected. State and
+  check the representation and runtime correspondence; keep erasure and
+  side-channel claims outside the formal result unless they are separately
+  modelled and verified.
+
+The next actionable step is the first one: agree the use case, order convention,
+and threat boundary. That specification determines whether the useful first
+implementation is an access-controlled wrapper, a lattice-indexed information-
+flow API, or a different abstraction altogether.
+
+== Related documentation
+
+* link:../README.adoc[Project overview] — current interfaces and deliberately
+  unformalized commitments.
+* link:what-epistemic-is.adoc[What epistemic-types is] — the project's
+  mathematical scope and contribution boundary.
+* link:continuity-foundations.adoc[Continuity foundations] — certified
+  residues and the distinct resource-bound axis.
+* link:proof-transport.adoc[Proof transport] — verification relative to an
+  explicit meaning, with its own trust boundary.