From 906e110ff7ba23b51409f53a028d1c9e8b9c6a2b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 4 Oct 2026 09:52:13 +0100 Subject: [PATCH] docs: mint scope statement and canonical spec for the standalone repo Owner confirmation 2026-10-04: secret-types is the standalone home of the confidentiality-label / information-flow work (supersedes the fold-into-epistemic-types#32 alternative and resolves the origin note's `no new repository yet` gate). - docs/secret-types.adoc: canonical scope statement -- question, boundary, decision record (D153, D154, 2026-10-04), first two-level Public/Secret model, explicit non-claims, consumers/neighbours. Ported with provenance from epistemic-types docs/secret-types.adoc (blob 583017cfd5fa). - README.adoc: real project README (question, boundary, honest status). - docs/decisions/0004-standalone-repo-and-scope.adoc: the placement decision. Honesty notes: specification only (no code, no proofs, no import, no CI proof gate); no consumer or frontier item selected (the RMO key-provisioning / disclosure use stays an inference, not a claim); RSR placeholder sweep (just repo-init) not yet run -- tracked in #2. Commit created through the GitHub API so it is GitHub-signed (Require-Signed-Commits ruleset). --- README.adoc | 155 +++------ .../0004-standalone-repo-and-scope.adoc | 69 ++++ docs/secret-types.adoc | 317 ++++++++++++++++++ 3 files changed, 434 insertions(+), 107 deletions(-) create mode 100644 docs/decisions/0004-standalone-repo-and-scope.adoc create mode 100644 docs/secret-types.adoc diff --git a/README.adoc b/README.adoc index 23a053b..ed5fcac 100644 --- a/README.adoc +++ b/README.adoc @@ -1,127 +1,68 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell -// SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) -= {{PROJECT_NAME}} +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += Secret Types :toc: :toc-placement: preamble // ── Licensing ─────────────────────────────────────────────────────────────── image:https://img.shields.io/badge/Code-MPL--2.0-blue.svg?logo=mozilla[Code licence: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"] image:https://img.shields.io/badge/Docs-CC--BY--SA--4.0-blue.svg?logo=creativecommons[Docs licence: CC-BY-SA-4.0,link="https://creativecommons.org/licenses/by-sa/4.0/"] -image:https://img.shields.io/badge/Provenance-Quantum--Safe-blueviolet[Quantum-Safe Provenance,link="docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt"] -// ── Standard & quality gates ──────────────────────────────────────────────── +// ── Status ────────────────────────────────────────────────────────────────── +image:https://img.shields.io/badge/Stage-specification--only-orange[Specification only: no code, no proofs] image:https://img.shields.io/badge/RSR-Rhodium_Standard-9C27B0[Rhodium Standard Repository,link="https://github.com/hyperpolymath/rhodium-standard-repositories"] -image:https://www.bestpractices.dev/projects/{{OPENSSF_BP_ID}}/badge[OpenSSF Best Practices,link="https://www.bestpractices.dev/projects/{{OPENSSF_BP_ID}}"] -image:https://api.scorecard.dev/projects/github.com/{{OWNER}}/{{REPO}}/badge[OpenSSF Scorecard,link="https://scorecard.dev/viewer/?uri=github.com/{{OWNER}}/{{REPO}}"] -image:https://sonarcloud.io/api/project_badges/measure?project={{OWNER}}_{{REPO}}&metric=alert_status[SonarQube Quality Gate,link="https://sonarcloud.io/summary/new_code?id={{OWNER}}_{{REPO}}"] -image:https://archive.softwareheritage.org/badge/origin/https://{{FORGE}}/{{OWNER}}/{{REPO}}/[Archived in Software Heritage,link="https://archive.softwareheritage.org/browse/origin/?origin_url=https://{{FORGE}}/{{OWNER}}/{{REPO}}"] -// ── Provenance & ecosystem ────────────────────────────────────────────────── -image:https://img.shields.io/badge/Idris-Inside-5E5086?logo=idris&logoColor=white[Idris Inside,link="https://github.com/hyperpolymath/proven"] -image:https://img.shields.io/badge/Zig-Zero--overhead-F7A41D?logo=zig&logoColor=black[Zig Zero-overhead FFI,link="https://github.com/hyperpolymath/typed-wasm"] -image:https://api.thegreenwebfoundation.org/greencheckimage/{{FORGE}}[Green Web,link="https://www.thegreenwebfoundation.org/green-web-check/?url={{FORGE}}"] - -{{PROJECT_DESCRIPTION}} - -[IMPORTANT] -==== -*This file is a template.* You are reading `README.adoc` from the *RSR template repo* -(or a freshly-cloned copy of it). Run `just repo-init` to replace every `{{PLACEHOLDER}}` -token with your project's details, then delete this admonition. Until you do, the -`{{...}}` markers below are intentional placeholders, not content. -==== +Confidentiality labels that constrain value flow, with declassification only at +explicit audited points: a standalone information-flow typing project. == What this is -A new repository scaffolded from the *Rhodium Standard Repository (RSR)* template: -a batteries-included starting point that ships with CI/CD, machine-readable project -metadata, an AI-agent gatekeeper protocol, a formally-typed ABI/FFI seam -(Idris2 + Zig), container and reproducible-build scaffolding, and governance -infrastructure — all wired and passing the RSR validators on day one. - -Replace this section with a description of *your* project once initialised. - -== Quick start - -[source,bash] ----- -# 1. Create a repo from this template (or clone it), then from the repo root: -just repo-init # interactive bootstrap: fills every {{PLACEHOLDER}} - -# 2. See the available tasks: -just # lists all phases (build, test, validate, audit, ...) - -# 3. Check the repo still satisfies the RSR shape: -just validate # structure + metadata checks ----- - -`just repo-init` prompts for the project name, owner, author, licence contact, and the -other values listed in `.machine_readable/ai/PLACEHOLDERS.adoc`, substitutes them -across the tree, validates the result, and (if available) runs the `k9-svc` checks. - -== AI-Assisted Installation - -If you are an AI agent installing this project, read -link:docs/AI_INSTALLATION_GUIDE.adoc[the AI installation guide] first — it gives -the orientation order, the full prompt sequence, and the privacy notice. - -The one trap worth stating up front: **do not set `RSR_NON_INTERACTIVE=1`**. It -stubs the shell builtin `read`, which also disables the loops that perform token -substitution — the run never terminates and substitutes nothing. Pipe answers to -stdin instead. - -== What you get - -* *Machine-readable metadata* (`.machine_readable/descriptiles/`) — `STATE`, `META`, - `ECOSYSTEM`, `PLAYBOOK`, `AGENTIC`, `NEUROSYM`, `CLADE`, and `anchors/ANCHOR`, - in deed, so tools and agents can read the project's state and boundaries. -* *AI gatekeeper protocol* — `rsr-template-repo_chora.deed` (the repo deed) is the - universal entry point that tells an AI agent how to work in this repo before it - touches anything; it carries the AI allocation policy and the ply directory tree. -* *Typed ABI/FFI seam* — `src/interface/Abi/` (Idris2 type + layout proofs) over - `src/interface/ffi/` (Zig implementation), with generated C headers. -* *CI/CD* — GitHub Actions for quality, security (CodeQL, Scorecard, secret - scanning), multi-forge mirroring, and RSR anti-pattern enforcement. -* *Supply-chain & reproducibility* — container layering (stapeln), Guix shells, - SBOM, and signing hooks. -* *Governance* — `GOVERNANCE.adoc`, `MAINTAINERS.adoc`, `.github/` community health - files, and a release `AUDIT.adoc` gate. - -== Repository map - -The authoritative map is generated, so it cannot drift from the tree: -link:docs/architecture/REPOSITORY-MAP.adoc[docs/architecture/REPOSITORY-MAP.adoc] -(regenerate with `just repo-map`; CI fails if it is stale). - -The short version: - -[cols="1,3"] -|=== -| Path | What lives there - -| `README.adoc`, `CLAUDE.md` | Start here - humans and AI agents respectively. -| `src/`, `tests/` | The code and its tests. -| `docs/` | Human documentation, including the full map above. -| `.machine_readable/` | Manifests, contractiles and policies that tools read. -| `build/`, `Justfile` | Every task runs through `just`; phases live in `build/just/`. -| `ci/`, `.github/` | CI configuration; GitHub reads `.github/` and no other path. -|=== - -== Where to go next - -* link:docs/architecture/REPOSITORY-MAP.adoc[The repository map] — generated; what every directory is for. -* link:docs/EXPLAINME.adoc[EXPLAINME] — the engineering deep-dive: how the pieces actually work. -* link:docs/AFFIRMATION.adoc[AFFIRMATION] — the dated, signed honesty snapshot of the repo's true state. -* link:docs/AUDIT.adoc[AUDIT] — the release audit gate. -* link:docs/AI_INSTALLATION_GUIDE.adoc[AI installation guide] — for agents instantiating this template. -* link:.machine_readable/ai/PLACEHOLDERS.adoc[PLACEHOLDERS] — the full placeholder reference. +*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 link:docs/secret-types.adoc[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. + +== Status + +* *Specification only.* There is no `Secret` type, no information-flow + calculus, no declassification rule, no noninterference theorem and no + cross-repository import in this project. +* *Minted 2026-10-04 in scope, not yet in scaffolding.* The scope statement and + this README are real project content. The RSR template placeholder sweep + (`just repo-init`) has not been run across the tree yet, so other files still + carry `{{TOKEN}}` template text; that sweep is tracked in + link:https://github.com/hyperpolymath/secret-types/issues/2[issue #2]. +* *No progress grade claimed.* A documentation link is not a mechanised + dependency; an integration may only be claimed once a real import builds in + CI. + +== Where things belong + +* This repository owns the confidentiality-label definitions, the typing and + observation semantics, and its own proof evidence. +* link:https://github.com/hyperpolymath/nextgen-typing/blob/main/docs/TYPE-CONNECTIONS.adoc[TYPE-CONNECTIONS] + is the shared family map; this family's row is proposed in + link:https://github.com/hyperpolymath/nextgen-typing/issues/118[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. == Licence Code, configuration and scripts are link:LICENSE[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. -The GitHub-detected licence is MPL-2.0 (the root `LICENSE`). Long-term -attribution uses Quantum-Safe Provenance — see -link:docs/legal/EXHIBIT-B-QUANTUM-SAFE.txt[the Quantum-Safe Provenance exhibit]. diff --git a/docs/decisions/0004-standalone-repo-and-scope.adoc b/docs/decisions/0004-standalone-repo-and-scope.adoc new file mode 100644 index 0000000..542181d --- /dev/null +++ b/docs/decisions/0004-standalone-repo-and-scope.adoc @@ -0,0 +1,69 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Architecture Decision Record: 0004-standalone-repo-and-scope + +== 4. Secret Types is a standalone information-flow project, scoped by docs/secret-types.adoc + +Date: 2026-10-04 + +=== Status + +Accepted (owner confirmation 2026-10-04, relayed to the coordinating session; +recorded publicly in link:https://github.com/hyperpolymath/secret-types/issues/2[secret-types#2]) + +=== Context + +The secret-types question began inside `epistemic-types` (`docs/secret-types.adoc`, +landed for `epistemic-types`#32) with an explicit early gate: + +* "Do not create a new repository from issue #32 alone, and do not add a `Secret` + module under `EpistemicTypes`." +* Placement options were (a) a grade instance inside SystemET/Anytype, or + (b) a standalone IFC calculus repository — the split to be made *before* + growing an API or runtime prototype. + +Two owner rulings followed on 2026-09-30: + +* *D153:* a secret type = a value whose flow is constrained by a confidentiality + label with explicit declassification, registered in the type-family map on + that boundary. +* *D154:* reuse an existing lattice (two-point first, then general), prove + noninterference, and allow declassification only at explicit audited points. + +valence-shell's direction doc (`docs/THEORY-FEED.adoc`) then carried the +placement as an owner call — "mint it with a scope statement ... Alternatively, +fold it into epistemic-types#32" — and graded secret-types' fit for the +RMO key-provisioning and disclosure story (`#92`) as an inference from the +repository name. + +=== Decision + +1. The standalone `secret-types` repository is the home of the work (owner + confirmation 2026-10-04). The "fold into `epistemic-types`#32" alternative is + superseded. +2. `docs/secret-types.adoc` in this repository is the canonical scope statement: + the two-level `Public ⊑ Secret` baseline, the low-observer model, the + noninterference target, and the explicit non-claims. +3. No consumer and no frontier item is selected. In particular, the possible + RMO key-provisioning / disclosure use is *not* adopted as a claim; the + nearest frontier item by name (`valence-shell`#92) is not selected as a + consumer of this project. +4. Progress claims stay graded: this decision creates no mechanised dependency. + The TYPE-CONNECTIONS row is a documentation link at most, and an integration + may only be claimed after a real import builds in CI. + +=== Consequences + +* This repository needs the scope statement reviewed like any other proposal; + the review checklist is in `docs/secret-types.adoc`. The model is not yet + accepted item by item, and there is no code. +* The RSR template placeholder sweep (`just repo-init`) still has to run across + the tree; until it does, the repository is minted in scope but not in + scaffolding. Tracked in `secret-types#2`. +* Cross-links that still describe the old alternatives need updating: + `epistemic-types`#32 (the specification issue), `nextgen-typing`#118 / + `TYPE-CONNECTIONS` (the family row), and valence-shell `docs/THEORY-FEED.adoc` + (the "mint vs fold" sentence and the RMO inference cell). +* The SystemET/Anytype grade-instance option remains a neighbour comparison for + any future grade-based realisation; it is not selected and no mapping is + claimed. diff --git a/docs/secret-types.adoc b/docs/secret-types.adoc new file mode 100644 index 0000000..88434d0 --- /dev/null +++ b/docs/secret-types.adoc @@ -0,0 +1,317 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += Secret Types: scope statement and first information-flow model +:toc: macro +:toclevels: 3 +:icons: font +:revdate: 2026-10-04 + +[abstract] +This is the canonical scope statement for the standalone `secret-types` +repository: a confidentiality-label / information-flow research project. It +records the owner's decision of 2026-10-04 to keep this as its own repository +(which supersedes the earlier "mint it or fold it into `epistemic-types`#32" +alternative), the ruling of 2026-09-30 on the model direction, and a first +specification proposal for a two-level, confidentiality-oriented +information-flow discipline over pure, deterministic, total programs. + +*This is a specification, not an implementation and not a security guarantee.* +There is no `Secret` type, no information-flow calculus, no declassification +rule and no noninterference theorem in this repository. No other repository +imports any artefact from this project, and no consumer or frontier item has +been selected for it. + +toc::[] + +== Scope statement + +*Question.* Which value flows does a confidentiality label permit, and what may +a lower (less cleared) 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, does not authenticate a +principal, does not enforce runtime access control, and does not hide timing, +storage, network or other side channels. The baseline below declassifies +nothing: an ordinary `Secret`-to-`Public` flow is outside the discipline, and +any release needs a separate policy and theorem. A security label is also not +an epistemic availability index (`κ`); the two share the shape of an order and +nothing else. As of 2026-10-04 *no consumer and no frontier item is selected* +for this project: the possible RMO key-provisioning / disclosure use is an +inference recorded in valence-shell's direction doc, not a claim made here +(see <>). + +== Decision record + +* *D153 (2026-09-30, owner).* A secret type = a value whose flow is constrained + by a confidentiality label with explicit declassification, registered in the + type-family map on that boundary. +* *D154 (2026-09-30, owner).* Reuse an existing lattice (two-point first, then + general), prove noninterference, and allow declassification only at explicit + audited points. +* *Owner confirmation (2026-10-04).* The standalone repository is the chosen + home. This supersedes the alternative recorded in valence-shell's direction + doc of folding the work into `epistemic-types`#32, and it resolves the "no new + repository yet" gate in the origin note (link:https://github.com/hyperpolymath/epistemic-types/blob/main/docs/secret-types.adoc[`epistemic-types` + `docs/secret-types.adoc`]). + +The alternatives considered and *not* selected: + +* *Fold into `epistemic-types`* — rejected by the 2026-10-04 confirmation. + `epistemic-types` remains the correct home of the decision record that started + this question; it is not the home of a `Secret` API. +* *A grade instance inside SystemET / Anytype* — a candidate for a grade-only + realisation, still open as a neighbour comparison (SystemET's L2 grade + algebra, Anytype#15). Not selected here: it would conflate resource-use + grades with confidentiality propagation unless a mapping is proved, and no + such mapping exists. See <>. + +This section records decisions; it does not claim that any implementation work +has started. + +== First model (specification proposal) + +The material in this section is adopted from the origin note +(`epistemic-types` `docs/secret-types.adoc`, blob `583017cfd5fa`, 2026-09-27) so +that the standalone repository owns its specification. It is a proposal at the +boundary set by D154, and the review checklist at the end of this document has +not yet been completed item by item. + +=== 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. 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, 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. `Public` is the bottom, an +ordinary flow may raise sensitivity but may not lower it, and combining +dependencies uses the least upper bound (`Public ⊔ Secret = Secret`, etc.). + +A clearance is also a label: a value at `ℓ` is within clearance `c` exactly +when there is a witness of `ℓ ⊑ c`. A `Secret` clearance is permitted to +observe either label *inside the model*. A witness states a policy relation; it +does not prove a person's identity, authenticate a credential, or enforce +access control at runtime. + +The two-point lattice is the baseline, not a claim that a general +`SecurityLattice` interface is justified. General labels should be added only +after the two-point model establishes which operations and laws the typing +rules actually require. + +=== 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, not properties established by any proof. +Because 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 them later requires +a new semantics and threat analysis. + +=== Permitted and forbidden flows + +Permitted: explicitly trusted public inputs may remain public or be raised to +`Secret`; secret inputs remain secret; values with multiple dependencies take +their join label. + +Forbidden: an ordinary `Secret`-to-`Public` flow, including 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 condition is a dependency. If commands or effects are added +later, the program-counter (or equivalent control-dependence) discipline must +be specified as well. + +There is *no declassification in this baseline*: no downgrade operation, no +release budget, no trusted declassifier, no authorization policy. A deliberate +release remains a forbidden flow until a separate policy states who may release +which information, under what evidence or capability, and which security +theorem is preserved. + +=== Target semantic property + +Let a machine state be a pair of public and secret inputs; call two states +low-equivalent when their public components are equal, with no constraint on +their secret components. Let `run c s` evaluate program `c` in state `s` and +`observePublic` select exactly the output visible to a `Public` observer. +Because only total programs are admitted, there is no separate termination +observation; the noninterference target is: + +[source,text] +---- +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 a two-level, termination-insensitive noninterference property for the +specified pure language. It is a theorem future typing rules must prove — not +an axiom, a field, or a consequence of having a `Secret ℓ A` wrapper. The +required controls follow: a well-typed public result 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. + +=== Candidate type shape, and its limit + +A future value-level surface could include schematic signatures resembling: + +[source,text] +---- +Secret : Label -> Set -> Set +raise : ℓ ⊑ ℓ' -> Secret ℓ A -> Secret ℓ' A +combine : Secret ℓ A -> Secret m B -> Secret (ℓ ⊔ m) (A × B) +---- + +These 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. + +== What this repository does *not* provide + +This project does not claim that any of the following exist or have been +proved here: + +* a `SecurityLattice`, `Secret`, `classify`, `declassify` or clearance API; +* 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; +* key provisioning, key rotation or key revocation semantics, and therefore no + RMO (GDPR/obliteration) key-lifecycle or disclosure guarantee; +* any transfer of proof or code from another repository's algebra, type + checker or runtime into this project. + +The origin note's statements about `epistemic-types` modules +(`Access.Preorder`, `BeliefModality`, `Warrant`, `EchoBridge.Grade` and the +rest) remain statements about *that* repository's narrower interfaces. They are +not re-homed here, and none of them is a confidentiality guarantee. + +== Consumers and neighbours + +=== Consumers + +No consumer and no valence-shell frontier item is selected as of 2026-10-04. + +The nearest frontier item *by name only* is +link:https://github.com/hyperpolymath/valence-shell/issues/92[valence-shell#92] +(GDPR / RMO completeness theory, Frontier 4). The suggested use of this project +for "RMO key-provisioning and disclosure" appears in valence-shell +`docs/THEORY-FEED.adoc` explicitly as an inference from the repository name, +not as a selected feeder link; `secret-types` is not selected as a feeder for +#92, and this document makes no claim about obliteration keys or disclosure. +Any future selection must name the frontier item, state the exact artefact to +be consumed, and keep the progress grade honest: a documentation link is not a +mechanised dependency, and an integration may only be claimed after a real +import builds in CI. + +=== Neighbours + +[cols="1,2,2",options="header"] +|=== +| Project | Existing responsibility | Relevance and limit for this proposal + +| `epistemic-types` +| Standpoint-indexed modalities, warrants and proof transport. +| Origin of the decision note; not the home of a confidentiality API. Possessing + evidence is not possessing a secret, and an epistemic index is not a security + label. + +| `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#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. + +| `echo-types` +| Proof-relevant fibres / 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 formalised relational-IFC comparison and leaves type-theoretic IFC open, so + any novelty claim for a new calculus needs 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. +|=== + +== Review checklist before implementation + +The specification issue (filed as `epistemic-types`#32; its handoff to this +repository is tracked in secret-types#2) asks for the first semantic boundary, +not for a proof module. Agreement is required on all of the following, not just +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, runtime enforcement and 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. +. Confirm the placement: a standalone calculus repository (decided 2026-10-04). +. Only then specify syntax, typing rules, and positive/negative proof controls. + +The follow-on stages remain separate work, each requiring its own review: a +focused formal module with expected-rejection fixtures; the semantic +noninterference proof; and, only if required, a runtime correspondence +argument. None is part of this prose-specification step. + +== Provenance and status + +* Ported and adopted 2026-10-04 from `epistemic-types` + `docs/secret-types.adoc` (blob `583017cfd5fa`, landed via PR #33 for #32 on + 2026-09-27, CC-BY-SA-4.0). The origin note remains the record of why the + question arose there; its placement section ("no new repository yet") is + superseded by the 2026-10-04 owner confirmation. +* Status: specification only. No source module, no proof, no CI proof gate and + no cross-repository import exists. The RSR template placeholder sweep for this + repository is not yet complete; see secret-types#2. +* Family map: the `nextgen-typing` TYPE-CONNECTIONS row for this family is + proposed in + link:https://github.com/hyperpolymath/nextgen-typing/issues/118[nextgen-typing#118]; + a proposed row is not a landed row, and a documentation link is not a + mechanised dependency.