docs(security): specify secret-type model boundary (#32)

CHANGELOG.adoc

@@ -40,6 +40,13 @@ the changelog records what is actually proved, not what is aspired to.
   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.
+* Expanded `docs/secret-types.adoc` for issue #32 with a proposed two-level
+  confidentiality lattice, pure/total use case, low-observer threat boundary,
+  explicit noninterference target, and a distinction between epistemic access,
+  Echo residues, resource grades, and information-flow control. The placement
+  decision rejects an `EpistemicTypes.Secret` API, defers a new repository
+  pending review against SystemET/Anytype and Echo Types, and leaves all Agda
+  implementation and theorem work as separate follow-ups.
 
 [[fixed--2026-09-07]]
 ==== Fixed — 2026-09-07

README.adoc

@@ -203,8 +203,8 @@ This is a prototype, not a complete epistemic logic. The following are **intenti
 * 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
+  see link:docs/secret-types.adoc[the information-flow proposal] for the
+  two-level baseline, non-claims, and repository boundary
 
 == Build
 
@@ -226,7 +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
+* link:docs/secret-types.adoc[Secret types] — a proposed two-level information-flow model, its noninterference target, and the repository boundary; no API is implemented
 
 == License
 

docs/README.adoc

@@ -36,9 +36,10 @@ authority.
   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.
+| Issue #32's proposed two-level information-flow model: label order, attacker
+  and observation boundary, target noninterference property, distinction from
+  existing interfaces, and an early repository-placement decision. No API or
+  security theorem is implemented.
 |===
 
 == Continuity foundations