diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index c9f7970..ecbc81b 100644
--- a/CHANGELOG.adoc
+++ b/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
diff --git a/README.adoc b/README.adoc
index c7b1a36..8863d67 100644
--- a/README.adoc
+++ b/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
 
diff --git a/docs/README.adoc b/docs/README.adoc
index 2da73d5..28a88c3 100644
--- a/docs/README.adoc
+++ b/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
diff --git a/docs/secret-types.adoc b/docs/secret-types.adoc
index cf0a152..583017c 100644
--- a/docs/secret-types.adoc
+++ b/docs/secret-types.adoc
@@ -1,34 +1,47 @@
 // 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
+= Secret Types: a scoped information-flow specification proposal
 :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.
+This note records a concrete first model for issue #32: a two-level,
+confidentiality-oriented information-flow discipline for pure, deterministic,
+total programs. It separates that model from the existing epistemic interfaces
+and from neighbouring type projects. This is a specification proposal, not an
+implemented API or security guarantee: there is no `Secret` type, IFC calculus,
+declassification rule, or noninterference theorem in this repository today.
 
 toc::[]
 
-== Decision and scope
+== Decision offered for issue #32
 
-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.
+Issue #31 landed this research direction here as documentation. Issue #32 asks
+for the first semantic boundary, not for an Agda module. This pass proposes the
+following decisions for review:
 
-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.
+* **Accept as a distinct research target:** static confidentiality / information
+  flow, with the minimal baseline specified below.
+* **Reject as an extension of the epistemic core:** do not identify a security
+  label with an epistemic standpoint `κ`, and do not add an
+  `EpistemicTypes.Secret` API on the strength of the current interfaces.
+* **Conditionally accept `Secret ℓ A` as a candidate value type:** it can
+  represent a value classified at security label `ℓ` inside a separately
+  specified IFC calculus; this does not accept it as a public API today.
+* **Reject a wrapper-only security claim:** `Secret ℓ A` alone does not define
+  program flows or prove noninterference. The calculus must include the rules
+  for dependencies and observations.
+* **No Agda API or new repository yet:** use this note as the decision record
+  while the exact calculus and the correct home for it are reviewed. Section
+  <<repository_boundary_and_exit_criteria>> sets the early repository gate.
 
-== What the repository currently provides
+These are proposed model decisions, not a claim that the project has accepted an
+implementation. Keep issue #32 open until the owner accepts or revises the
+baseline and placement decision.
+
+== What this repository currently provides
 
 The current code offers concepts that may be useful when designing a security
 model, but their present meanings are narrower:
@@ -40,7 +53,8 @@ model, but their present meanings are narrower:
   `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.
+  specify a security policy, a least element, joins, clearances, or program
+  flow rules.
 * `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
@@ -62,108 +76,282 @@ 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.
+certification, and it does not supply missing security semantics. The root
+`SECURITY.adoc` is the repository's vulnerability-reporting policy; it is not a
+program information-flow model.
+
+== Proposed baseline model
+
+=== Use case and trust boundary
+
+The first example domain is a pure, total policy/configuration function that
+receives a public request and a trusted private setting and returns an explicitly
+classified result. A public observer may choose and know the request, but must
+not learn anything about the private setting from public outputs. This is a
+small, concrete information-flow problem; it does not claim to model a deployed
+service.
+
+Source labels are trusted inputs to the model. The checker cannot infer from an
+arbitrary value whether it is genuinely public or private. In particular, any
+real application must justify the initial classification at its input boundary;
+a type annotation alone cannot authenticate that boundary.
+
+=== Labels, order, flows, and clearances
+
+For the first model, use exactly two labels:
+
+[source,text]
+----
+Label = { Public, Secret }
+Public ⊑ Public       Public ⊑ Secret       Secret ⊑ Secret
+                       (no proof of Secret ⊑ Public)
+⊥ = Public            ⊤ = Secret
+----
+
+Read `ℓ ⊑ ℓ'` as: data classified at source label `ℓ` may flow to a destination
+classified at `ℓ'` without becoming less protected. Thus `Public` is the bottom,
+`Secret` is more restrictive, and an ordinary flow may raise sensitivity but may
+not lower it. Combining dependencies uses the least upper bound:
 
-== A possible security interpretation
+[cols="1,2",options="header"]
+|===
+| Inputs | Resulting label
+| `Public ⊔ Public` | `Public`
+| `Public ⊔ Secret` | `Secret`
+| `Secret ⊔ Public` | `Secret`
+| `Secret ⊔ Secret` | `Secret`
+|===
 
-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:
+A clearance is also a label. A value at `ℓ` is within clearance `c` exactly when
+there is a witness of `ℓ ⊑ c`. A `Public` observer can therefore observe public
+values only; a `Secret` clearance is permitted to observe either label *inside
+the model*. Such a witness states a policy relation. It does not prove a person's
+identity, authenticate a credential, or enforce access control at runtime.
 
-* 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.
+The two-point lattice is the specification baseline, not a claim that a general
+`SecurityLattice` interface is already justified. General labels should be added
+only after the two-point model establishes which operations and laws the typing
+rules actually require. A bounded join-semilattice may suffice for upward
+combination; requiring meets or a richer lattice without a theorem would be
+premature.
 
-Under that convention, schematic signatures (not compile-ready Agda) might
-resemble:
+=== Attacker and observations
+
+The baseline attacker is a low-clearance observer who:
+
+* may choose and know all public inputs;
+* may observe the explicitly public projection of a program's result; and
+* may compare results from executions with the same public inputs and different
+  secret inputs.
+
+The model assumes that the attacker cannot inspect secret values directly,
+forge trusted source classifications, or obtain a privileged clearance witness.
+Those are assumptions of the model, not properties established by Agda. Since
+the initial language is pure, deterministic, and total, it has no I/O, mutable
+state, concurrency, exceptions, divergence, or observable termination. Timing,
+space, cache, storage, network, speculative-execution, and other side channels
+are outside the observation model. Adding any of these later requires a new
+semantics and threat analysis.
+
+=== Permitted and forbidden flows
+
+The baseline permits:
+
+* explicitly trusted public inputs to remain public or be raised to `Secret`;
+* secret inputs to remain secret; and
+* values with multiple dependencies to receive their join label.
+
+It forbids an ordinary `Secret`-to-`Public` flow. This includes implicit flow:
+if a secret condition selects between two different public results, that result
+must not be accepted as public merely because neither branch directly returns a
+secret value. The core expression rules must account for the condition as a
+dependency. If the language later adds commands or effects, its program-counter
+or equivalent control-dependence discipline must be specified as well.
+
+There is **no declassification** in this baseline: no downgrade operation,
+release budget, trusted declassifier, or authorization policy. A deliberate
+release is still a forbidden flow until a separate policy states who may release
+which information, under what evidence or capability, and which security theorem
+is preserved. An authorized-read judgement is not itself declassification, but
+an accessor exposed to untrusted program code could still create an output leak;
+its use must be included in the language semantics and proof.
+
+=== Target semantic property
+
+Let a machine state be a pair of public and secret inputs. Define two states to
+be low-equivalent when their public components are equal, with no constraint on
+their secret components. Let `run c s` be the result of evaluating program `c`
+in state `s`, and let `observePublic` select exactly the output visible to a
+`Public` observer.
+
+Because the model admits only total programs, there is no separate termination
+observation. The noninterference target is:
 
 [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
+For every program c well-typed to produce a Public output,
+for all public inputs p and secret inputs h₁, h₂:
+  observePublic (run c (p, h₁)) = observePublic (run c (p, h₂))
 ----
 
-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.
+This is a two-level, termination-insensitive noninterference property for the
+specified pure language: changing only secret input cannot change a public
+observation. It is a theorem the future typing rules must prove, not an axiom,
+field, or consequence of having a `Secret ℓ A` wrapper. If partiality or
+observable termination is introduced, the observation relation must be revised
+and the corresponding termination-sensitive or termination-insensitive claim
+stated explicitly.
 
-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.
+The required future positive/negative examples are consequently clear:
+well-typed public results whose value does not depend on the secret must be
+accepted; a direct secret return and a public result selected by a secret branch
+must be rejected. These controls test the intended flow rules, but do not replace
+the semantic theorem.
 
-== What is not claimed
+=== Candidate type shape, and its limit
 
-This note does not claim that the following exist or have been proved here:
+A future value-level surface could include signatures resembling the following;
+these are schematic, not Agda declarations or an accepted API:
+
+[source,text]
+----
+Secret   : Label -> Set -> Set
+raise    : ℓ ⊑ ℓ' -> Secret ℓ A -> Secret ℓ' A
+combine  : Secret ℓ A -> Secret m B -> Secret (ℓ ⊔ m) (A × B)
+----
+
+These operations express classification, safe upward propagation, and joining
+dependencies. They do not define the expression language, its control-flow
+rules, or the public observation function. An unrestricted
+`Secret ℓ A -> A`, whether called `reflect`, `reveal`, or `readAt`, is not part
+of the program interface. A future observer API would need a precise clearance
+semantics and a trusted boundary; it still would not authenticate an actual
+principal or prove noninterference on its own.
+
+== `Access.Preorder` is not the security interface
+
+The two domains share the *shape* of an order, but not its interpretation or
+required operations:
+
+[cols="1,2,2",options="header"]
+|===
+| | Epistemic access in this repository | Security flow in the proposed model
+| Index | Standpoint `κ` | Confidentiality label `ℓ`
+| Order reading | `κ ≤κ κ'`: `κ'` is at least as informed as `κ` | `ℓ ⊑ ℓ'`: information may flow from `ℓ` to no-less-restrictive `ℓ'`
+| Transport / use | `E κ A` transports to `E κ' A` | Data dependencies join; reading requires `ℓ ⊑ clearance`
+| Extra structure needed | Reflexivity and transitivity | The chosen label order, public bottom, join, clearance interpretation, source/flow typing, and low-equivalence semantics
+|===
+
+`Access.Preorder` supplies only reflexivity and transitivity. It has no label
+bottom, join, classification policy, low-equivalence relation, or noninterference
+semantics. Reusing it as the public security API would make the indices look
+interchangeable when they are not. The baseline therefore calls for a distinct
+security-label definition and relation. Shared proof lemmas for preorders could
+be considered later, but that would be code reuse only, not a semantic
+identification.
+
+[[repository_boundary_and_exit_criteria]]
+== Repository boundary and exit criteria
+
+There is a real **semantic** boundary: epistemic availability asks what is
+available at a standpoint; information-flow security asks whether changes in
+highly classified inputs can affect a lower observer. The common fact that both
+may be indexed by an order does not make one an extension of the other.
+
+The neighbouring projects narrow the repository decision:
+
+[cols="1,2,2",options="header"]
+|===
+| Project | Existing responsibility | Relevance and limit for this proposal
+| `epistemic-types`
+| Standpoint-indexed modalities, warrants, and proof transport
+| Correct home for this decision note because the research began here; not the home of an `E κ A`-based confidentiality API.
+| `systemet` / `anytype`
+| SystemET specifies an L2 ordered-semiring grade algebra; Anytype is its checker kernel.
+| SystemET's merged MECH-2 work proves a bounded-distributive-lattice grade instance, including the two-point `Low ≤ High` lattice. Anytype issue #15 remains open for porting the lattice/cost/product instances to the kernel. This is a promising home for the *grade algebra* part, not evidence of a program-level IFC or noninterference theorem. The grade operations' usage meaning must not be silently equated with confidentiality propagation.
+| `echo-types`
+| Proof-relevant fibers / residues and structured information loss
+| `EchoSecurity` proves a no-section / no-recovery property for a collapsing exit map; that is not low-observer noninterference. Its adjacency note records a formalized relational-IFC comparison and leaves comparison with type-theoretic IFC open, so novelty claims for a new calculus need that comparison.
+| `tropical-types`
+| Resource-grade algebras and worst-case bounds
+| Resource grades are not confidentiality labels; a resource bound is not a leakage bound without a separate measure and theorem.
+|===
+
+Status snapshot checked 2026-09-27: SystemET PR #17 merged on 2026-07-21
+at `a11c98774c8c4a1b35c1e3bd9145a191dffb3840`; Anytype issue #15 remained
+open. Current references: link:https://github.com/hyperpolymath/systemet/blob/main/docs/theory/03-l2-grades.adoc[SystemET L2 grade contract],
+link:https://github.com/hyperpolymath/systemet/pull/17[SystemET MECH-2],
+link:https://github.com/hyperpolymath/anytype/issues/15[Anytype issue #15],
+link:https://github.com/hyperpolymath/echo-types/blob/main/proofs/agda/EchoSecurity.agda[EchoSecurity], and
+link:https://github.com/hyperpolymath/echo-types/blob/main/docs/adjacency/information-flow.adoc[Echo Types' IFC adjacency note]. These are candidate neighbors, not dependencies or proofs imported into this repository.
+
+=== Placement decision for the next step
+
+**Do not create a new repository from issue #32 alone, and do not add a
+`Secret` module under `EpistemicTypes`.** Keep this specification here as the
+record of why the question arose. Before writing proof code, make one explicit
+cross-repository choice:
+
+. If the desired contribution is the lattice/grade instance within a graded
+  language, coordinate with SystemET/Anytype and prove the mapping from its L2
+  grade operations to this confidentiality interpretation.
+. If the desired contribution is a standalone IFC calculus—with its own
+  expression and control-flow rules, low-equivalence semantics, and
+  noninterference theorem—that cannot be hosted in SystemET without conflating
+  resource use with confidentiality or changing its theory, then a separate
+  repository is justified. Make that split **before** growing an API or runtime
+  prototype, and compare the calculus against the type-theoretic IFC literature
+  and Echo Types' open adjacency question.
+
+On the evidence checked for this note, the answer is: **separate from
+`epistemic-types` as a type/API; no new repository yet.** A candidate host for a
+grade-only realization already exists, while the independent-calculus case
+needs the owner to choose that larger deliverable and resolve the neighbor
+comparison. This is an early gate, not a commitment to keep security work in
+this repository indefinitely.
+
+== Explicit non-claims
+
+This proposal 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;
+* an implemented information-flow type system or a proof that forbidden flows
+  cannot occur;
+* the noninterference theorem above;
+* authenticated principals, runtime access control, cryptographic secrecy,
+  secure erasure, zeroization, or protection from 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.
+`--safe --without-K` establishes only the propositions actually encoded and
+checked by Agda. It does not validate the adequacy of this proposed attacker
+model or any external implementation. Any future integration must name exact
+source revisions, state the compatibility claim, and add a reproducible check
+before this project relies on it.
+
+== Review checklist before implementation
+
+Issue #32's first-stage acceptance should require agreement on all of the
+following, not just agreement on the name `Secret`:
+
+. Accept or revise the two-level public/secret labels and their order direction.
+. Confirm the pure, total policy/configuration use case and the low-observer
+  capability boundary.
+. Confirm that declassification and runtime/side-channel claims are out of
+  scope.
+. Accept the exact low-equivalence/noninterference statement and require a
+  future type-soundness proof for the chosen calculus.
+. Decide whether to target SystemET/Anytype as a grade instance or open a
+  standalone calculus repository before API work.
+. Only then specify syntax, typing rules, and positive/negative proof controls.
+
+The follow-on implementation stages remain separate: a focused formal module
+and expected-rejection fixtures; the semantic noninterference proof; and, only
+if required, a runtime correspondence argument. None is part of this issue's
+prose-specification step.
 
 == Related documentation