diff --git a/.machine_readable/descriptiles/META.a2ml b/.machine_readable/descriptiles/META.a2ml index 2d064d8..552e79c 100644 --- a/.machine_readable/descriptiles/META.a2ml +++ b/.machine_readable/descriptiles/META.a2ml @@ -73,8 +73,8 @@ consequence = "No-smuggling holds structurally rather than by side-condition. Th title = "Secret types and information-flow control are specified outside this repository" status = "accepted" context = "Issue #29 preserved a secret-types research note here; issue #32 then proposed an in-repository security model. On 2026-10-04 the owner ruled that hyperpolymath/secret-types is the standalone home, with D153 (a secret type is a value whose flow is constrained by a confidentiality label with explicit declassification, registered in the type-family map on that boundary) and D154 (reuse an existing lattice, two-point first then general; prove noninterference; declassify only at explicit audited points)." -decision = "This repository adds no Secret API and no information-flow implementation. docs/secret-types.adoc is retained as the boundary/history note; the specification itself, lattice reuse, the noninterference theorem, and audited declassification belong to hyperpolymath/secret-types." -consequence = "The epistemic core keeps its scope: no confidentiality claim attaches to BeliefModality, Echo grades, or Access. epistemic-types#29 stays closed; the move of issue #32 must not be duplicated." +decision = "This repository adds no Secret API and no information-flow implementation. docs/secret-types.adoc is retained as the boundary/history note; the specification itself (canonical text in hyperpolymath/secret-types docs/secret-types.adoc; placement in docs/decisions/0004-standalone-repo-and-scope.adoc, PR #4 d1122d8), lattice reuse, the noninterference theorem, and audited declassification belong to hyperpolymath/secret-types." +consequence = "The epistemic core keeps its scope: no confidentiality claim attaches to BeliefModality, Echo grades, or Access. epistemic-types#29 stays closed. Issue #32 stays in this repository and stays open as the origin/decision record - no transfer and no duplicate - until the standalone specification's review checklist is completed item by item (docs/secret-types.adoc, docs/secret-types-transition-review-2026-10-05.adoc)." [development-practices] build-tool = "just" diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index b8720a9..4a37b81 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -1,7 +1,7 @@ [metadata] project = "epistemic-types" version = "0.1.0" -last-updated = "2026-10-04" +last-updated = "2026-10-05" status = "prototype" # prototype | active | paused | archived [project-context] @@ -20,7 +20,7 @@ discipline = "Constructive. Compiles under {-# OPTIONS --safe --without-K #-}. N honesty-rule = "Laws appear as explicit fields when not derivable; lawful instances are added only after proving or explicitly assuming the laws. No smuggling." [boundaries] -secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153: label-constrained flow with explicit declassification and type-family-map registration; D154: reuse an existing lattice two-point-first, prove noninterference, declassify only at explicit audited points). This repository adds no Secret API and no information-flow implementation; docs/secret-types.adoc is retained as the boundary/history note. epistemic-types#29 is resolved and stays closed; the transfer of epistemic-types#32 to secret-types is pending GitHub issue-write access and must not be duplicated." +secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153: label-constrained flow with explicit declassification and type-family-map registration; D154: reuse an existing lattice two-point-first, prove noninterference, declassify only at explicit audited points). This repository adds no Secret API and no information-flow implementation; docs/secret-types.adoc is retained as the boundary/history note. epistemic-types#29 is resolved and stays closed; epistemic-types#32 stays in this repository and stays open as the origin/decision record (no transfer) and must not be duplicated. It closes only after the standalone specification's review checklist is completed item by item; see docs/secret-types.adoc and docs/secret-types-transition-review-2026-10-05.adoc." [build] checker = "Agda 2.6.4.3 (CI-matched)" diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 0501a06..953ca4c 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -41,7 +41,7 @@ agda-options = "{-# OPTIONS --safe --without-K #-} ; no postulates; no Agda stan agda-version = "2.6.4.3" echo-distinction = "Do not collapse Echo C y and E κ A. Echo retains certified residues; epistemic types are standpoint/warrant/access modalities. Their composition is meaningful; they are not the same modality." ci = "Proof and security workflows configured; required merge checks are described in docs/ci-safety.adoc" -secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153/D154). Do not add a Secret API or information-flow implementation here; docs/secret-types.adoc is the boundary/history note. epistemic-types#29 stays closed." +secret-types = "Owner decision 2026-10-04: hyperpolymath/secret-types is the standalone home for secret types (D153/D154). Do not add a Secret API or information-flow implementation here; docs/secret-types.adoc is the boundary/history note. epistemic-types#29 stays closed; issue #32 stays open here as the origin/decision record (no transfer) until the standalone specification's review checklist completes." [first-run] dev-container = ".devcontainer/ — Debian 13 pinned to the same base image digest as CI, agda-bin=2.6.4.3-1+b2; postCreateCommand runs 'just check'." @@ -107,7 +107,7 @@ rules = [ "Keep a2ml / Nickel / k9 files under .machine_readable/ only.", "License and SPDX changes are owner-manual; do not add LICENSE files or SPDX headers.", "Maintain owner-authorized proof and security CI; do not bypass failing checks.", - "Secret types and information-flow control stay outside this repository (D153/D154, docs/secret-types.adoc); do not duplicate the move of issue #32.", + "Secret types and information-flow control stay outside this repository (D153/D154; canonical specification in hyperpolymath/secret-types). Issue #32 stays in this repository, open, as the origin/decision record: do not transfer it, close it, or duplicate it, and treat closure as pending the standalone specification's review checklist (docs/secret-types.adoc, docs/secret-types-transition-review-2026-10-05.adoc).", ] [ecosystem] diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index dd8bddd..b0d979b 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -12,6 +12,22 @@ the changelog records what is actually proved, not what is aspired to. === https://github.com/hyperpolymath/epistemic-types/compare/v0.1.0...HEAD[Unreleased] +[[changed--2026-10-05]] +==== Changed — 2026-10-05 + +* Cross-reference review of the Secret Types transition. `docs/secret-types.adoc` + now records that issue #32 **stays in this repository, open**, as the + origin/decision record: the specification moved to + `hyperpolymath/secret-types` (canonical spec and ADR 0004, PR #4 `d1122d8`, + 2026-10-04), but no issue transfer occurs, and closure waits on the standalone + specification's own review checklist. The provenance blob (`583017cfd5fa…`, + the PR #33 revision) was verified, the stale downstream cross-references were + recorded, and the exact proposed issue update (prepared, not posted) is in + `docs/secret-types-transition-review-2026-10-05.adoc`. `README`, the + documentation index, `STATE.a2ml`, `META.a2ml` (ADR-007) and + `0-AI-MANIFEST.a2ml` were corrected where they described a pending transfer of + issue #32. No Agda source changed. + [[changed--2026-10-04]] ==== Changed — 2026-10-04 diff --git a/README.adoc b/README.adoc index e44a3c2..96df244 100644 --- a/README.adoc +++ b/README.adoc @@ -206,7 +206,10 @@ This is a prototype, not a complete epistemic logic. The following are **intenti out of scope for this repository. The standalone home is link:https://github.com/hyperpolymath/secret-types[`hyperpolymath/secret-types`] (D153/D154); link:docs/secret-types.adoc[the boundary/history note] records - the decision and the pointer. No `Secret` API exists here. + the decision and the pointer. No `Secret` API exists here. Issue #32 stays + open in this repository as the origin/decision record (no transfer); + link:docs/secret-types-transition-review-2026-10-05.adoc[the transition + review] records the cross-references. == Build diff --git a/docs/README.adoc b/docs/README.adoc index 8a21174..4574e9b 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -40,7 +40,14 @@ authority. `hyperpolymath/secret-types` is the standalone home (D153/D154), the retained two-level information-flow proposal (label order, attacker and observation boundary, noninterference target), and the reason no `Secret` API or security - theorem exists in this repository. + theorem exists in this repository. Issue #32 stays open here as the + origin/decision record (no transfer). + +| `docs/secret-types-transition-review-2026-10-05.adoc` +| Cross-reference review of the Secret Types transition: the evidence and + verified provenance of `secret-types` PR #4, the ownership split (what moved, + what remains here, where follow-up belongs), the stale downstream trackers, + and the exact proposed issue #32 update (prepared, not posted). |=== == Continuity foundations diff --git a/docs/secret-types-transition-review-2026-10-05.adoc b/docs/secret-types-transition-review-2026-10-05.adoc new file mode 100644 index 0000000..1d043f9 --- /dev/null +++ b/docs/secret-types-transition-review-2026-10-05.adoc @@ -0,0 +1,263 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += Secret Types transition: cross-reference review — 2026-10-05 +:toc: macro +:toclevels: 3 +:icons: font +:revdate: 2026-10-05 + +[abstract] +Review of the Secret Types transition — the standalone migration recorded by +`hyperpolymath/secret-types` PR #4 (commit `d1122d8`, merged 2026-10-04) — +against this repository's current documentation and tracked work. It records +what has moved, what remains owned here, and where follow-up work belongs. It +changes no issue state: issue #32 stays in this repository and stays open, no +issue ownership is transferred, and nothing is deleted or moved. The exact +proposed update for issue #32 is prepared at the end of this document; it is +*not posted*. + +toc::[] + +== Scope and constraint + +The review was commissioned on 2026-10-05 with three constraints, all applied: + +* preserve history — retained notes keep their text, and superseded text is + marked, not rewritten or deleted; +* do not move or delete work, transfer issue ownership, or close + `epistemic-types#32` merely because `hyperpolymath/secret-types` exists; +* update or close tracking only after the transition is evidenced and any + required review is complete. + +This record is proposed for review in PR #38. Checked against `main` at +`eb810d4` (`docs/secret-types.adoc` blob +`01dd2c24bd7d11249ce39917a246925ae4808ce5`), the GitHub API for both +repositories, and the destination repositories named below. + +== The transition, as evidenced + +[cols="1,2,2",options="header"] +|=== +| Source | Evidence (checked 2026-10-05) | What it establishes + +| Migration change +| `hyperpolymath/secret-types` PR #4, commit + `d1122d8474f3e2f389d494473aac51164f1747bc`, merged 2026-10-04T09:07:42Z; + changes `README.adoc`, `docs/secret-types.adoc`, + `docs/decisions/0004-standalone-repo-and-scope.adoc` +| The standalone repository owns the canonical specification and the placement + decision. No `Secret` type, IFC calculus, theorem, or cross-repository import + is claimed there. + +| Owner confirmation +| 2026-10-04, recorded in `secret-types` ADR 0004 and PR #4; D153 comment on + `secret-types#2` (2026-09-30T14:14Z); D154 comment on `epistemic-types#32` + (2026-09-30T14:15Z, surface: + https://github.com/hyperpolymath/standards/issues/787#issuecomment-5912989503) +| The standalone repository is the home of the *work*; the "fold it into + `epistemic-types#32`" placement alternative is superseded. The rulings say + nothing about transferring the issue itself. + +| Provenance +| `secret-types` `docs/secret-types.adoc` names blob `583017cfd5fa…`; the full + blob `583017cfd5fab189ca17128d01c7eddb494d8476` (19,326 bytes) is the + `docs/secret-types.adoc` revision at `epistemic-types` PR #33 (`d97ecaab`, + 2026-09-27) +| Verified accurate: the adopted text is the PR #33 revision — not the initial + PR #31 draft (`cf0a152e…`, 9,436 bytes) and not the 2026-10-04 boundary + revision (PR #37, `eb810d4`). + +| Boundary record here +| `epistemic-types` PR #37 (`eb810d4`, merged 2026-10-04) retains + `docs/secret-types.adoc` as the boundary/history note; `#29` was closed + 2026-09-27 and stays closed +| The origin record is retained here, as the current docs already state. + +| Review state +| `secret-types` `docs/secret-types.adoc` § "Review checklist before + implementation" states that the checklist "has not yet been completed item by + item"; `epistemic-types` PR #37 carries an unresolved review finding + (CodeRabbit, `CHANGES_REQUESTED`) about the issue-#32 open-state wording +| The required review is **not** complete. Issue #32 must not be closed, and the + specification must not be described as accepted. +|=== + +== Findings + +. **Issue #32 is not obsolete, and it was not transferred.** This repository's + note said the issue "is obsolete as titled" and that "the replacement issue is + the transferred #32 itself". No transfer occurred (issue write access was + documented as denied with `403` in the migration commit message), and no + ruling makes the issue obsolete: the placement decision moves the *work*, not + the issue. The note now says #32 stays here and stays open. Corrected in + `docs/secret-types.adoc`. +. **`STATE.a2ml` described a pending transfer.** It read "the transfer of + epistemic-types#32 to secret-types is pending GitHub issue-write access and + must not be duplicated". There is no transfer to wait for; corrected to + "issue #32 stays in this repository and stays open (no transfer)". +. **`META.a2ml` ADR-007 and `0-AI-MANIFEST.a2ml` used "move" language** ("the + move of issue #32 must not be duplicated"). The non-duplication intent is + kept; the transfer implication is removed. +. **The four "ready-to-post" coordination texts named in `secret-types` PR #4 + were never persisted to any repository** (`secret-types#2`, + `nextgen-typing#118`, `valence-shell#210`, and the transferred-issue + provenance note). Only this review's proposed update for `epistemic-types#32` + is prepared in text. Recorded here as a process gap, not as a claim about the + other repositories. +. **Downstream trackers are stale; ownership stays with them.** + `nextgen-typing` `docs/TYPE-CONNECTIONS.adoc` (245 lines, checked 2026-10-05) + carries no secret-types row, although D153 and `nextgen-typing#118` both + require family-map registration. `valence-shell` `docs/THEORY-FEED.adoc` + (merged via PR #211) still describes `secret-types` as un-minted, records + "mint it … or fold it into epistemic-types#32" as an open owner call, and + grades its feed `?`/`?`; `valence-shell#92` remains unselected as a consumer. + Anytype#15 remains open for the grade-instance neighbour comparison; SystemET + PR #17 is still merged at `a11c98774c8c4a1b35c1e3bd9145a191dffb3840` + (2026-07-21). These repositories own their own corrections. +. **The statements about this repository's interfaces stay here.** The + standalone specification explicitly says the origin note's statements about + `Access.Preorder`, `BeliefModality`, `Warrant`, `EchoBridge.Grade` "remain + statements about *that* repository's narrower interfaces. They are not + re-homed here, and none of them is a confidentiality guarantee." Nothing in + the transition weakens them. + +== Ownership split + +[cols="1,2",options="header"] +|=== +| Area | Owner after the transition + +| Canonical specification: question, boundary, two-level `Public ⊑ Secret` + baseline, low-observer attacker, noninterference target, review checklist +| `hyperpolymath/secret-types` (`docs/secret-types.adoc`) + +| Placement decision +| `hyperpolymath/secret-types` (`docs/decisions/0004-standalone-repo-and-scope.adoc`) + +| Future formal work: module with expected-rejection fixtures, noninterference + theorem, audited declassification, runtime correspondence +| `hyperpolymath/secret-types` (each stage separately reviewed) + +| Family-map registration (D153) +| `nextgen-typing#118` / `docs/TYPE-CONNECTIONS.adoc` + +| Boundary/history note and origin of the question +| `epistemic-types` (`docs/secret-types.adoc`, retained) + +| Origin/decision-record issue +| `epistemic-types#32` — **open, no transfer**; closure only after the standalone + review checklist is completed item by item + +| Non-claims about `Access.Preorder`, `BeliefModality`, `Warrant`, + `EchoBridge.Grade`, and the `--safe --without-K` proof gate +| `epistemic-types` + +| Consumption/feeder selection, including any RMO claim +| `valence-shell` (`docs/THEORY-FEED.adoc`, `#210`); `#92` is unselected + +| Scaffolding/mint (RSR template sweep) +| `secret-types#2` +|=== + +== Prepared update for issue #32 — not posted + +The exact proposed comment follows. It is **prepared and not posted**: the +tracking gate ("only update or close tracking after the transition is evidenced +and any required review is complete") is not met, because the standalone +specification's own review checklist is incomplete and PR #37's review finding +is unresolved. The credential state for issue writes was documented as +unavailable (`403`) on 2026-10-04 in `secret-types` PR #4 and was not +re-verified here. Nothing in this document should be read as posted. + +[source,markdown] +---- +**Cross-reference review — Secret Types transition (2026-10-05)** + +*Prepared update for this issue. It is not posted yet; see the note at the end.* + +Status of this issue: **open, and remaining open in `epistemic-types`.** This is +a tracking review, not a closure, and it does not transfer the issue. + +Evidenced state (checked 2026-10-05): + +* `hyperpolymath/secret-types` holds the canonical specification and the + placement decision: `docs/secret-types.adoc` (scope statement, two-level + `Public ⊑ Secret` model, low-observer attacker, noninterference target, + explicit non-claims, review checklist) and + `docs/decisions/0004-standalone-repo-and-scope.adoc`, landed by secret-types + PR #4 (`d1122d8`, merged 2026-10-04). +* Provenance verified: the adopted text is this repository's + `docs/secret-types.adoc` at blob + `583017cfd5fab189ca17128d01c7eddb494d8476` — the PR #33 revision of + 2026-09-27 (19,326 bytes) — not the initial PR #31 draft (`cf0a152e…`) and + not the 2026-10-04 boundary revision (PR #37, `eb810d4`). +* D153 (`secret-types#2`) and D154 (this issue's comment, 2026-09-30) stand. + The 2026-10-04 owner confirmation, recorded in secret-types ADR 0004 and + PR #4, selects the standalone repository as the home of the work; it + supersedes the "fold it into `epistemic-types`#32" placement alternative + only. + +What has moved: the specification text and its review checklist; label/lattice +reuse (two-point first); the noninterference theorem; audited declassification; +the future module with expected-rejection fixtures; any runtime correspondence +argument. + +What remains owned here: this issue as the origin/decision record; +`docs/secret-types.adoc` in this repository as the boundary/history note; the +statements about this repository's interfaces (`Access.Preorder`, +`BeliefModality`, `Warrant`, `EchoBridge.Grade`), which the standalone +specification explicitly states are not re-homed and are not confidentiality +guarantees; and the Agda `--safe --without-K` proof gate. + +Where follow-up belongs: + +* `secret-types#2` — mint/scaffolding and the handoff record. +* `nextgen-typing#118` and `docs/TYPE-CONNECTIONS.adoc` — the family-map row + required by D153; as of 2026-10-05 the map (245 lines) carries no + secret-types row. +* `valence-shell#210` / `docs/THEORY-FEED.adoc` — the secret-types section + still describes the project as un-minted and records "mint it … or fold it + into epistemic-types#32" as an open owner call with a `?`/`?` feed grade; + that text is stale. `valence-shell#92` remains unselected as a consumer. +* `occupancy-types` — its own ULTRAPLAN no-import fence; no action evidenced. +* Anytype#15 — the grade-instance neighbour comparison remains open; SystemET + PR #17 (`a11c987…`, 2026-07-21) is still the merged MECH-2 reference. + +Why this issue does not close or transfer: + +* The standalone specification's "Review checklist before implementation" + states, in the merged text, that it "has not yet been completed item by + item". Its item 5 (placement) is decided; items 1–4 and 6 are not. +* PR #37 in this repository carries an unresolved review finding about this + issue's open-state wording; that wording is superseded by this review and by + the repository updates in the same change. +* Nothing in the 2026-10-04 placement decision requires transferring this + issue. No transfer has occurred, and no issue-write operation has ever been + performed for it. + +Review record: `epistemic-types` +`docs/secret-types-transition-review-2026-10-05.adoc` (PR #38 +(`arena/01a10aaf-epistemic-types`); pending review). +---- + +== What would unblock the tracking update + +* The standalone specification's "Review checklist before implementation" is + completed item by item, or the owner explicitly accepts the baseline; and +* the unresolved PR #37 review finding is superseded or resolved (this review + supersedes its wording); and +* an issue-write credential is available, or the owner posts the prepared text. + +Until then: #32 open, in this repository; nothing moved; nothing closed. + +== References + +* `secret-types` `docs/secret-types.adoc` and + `docs/decisions/0004-standalone-repo-and-scope.adoc` (PR #4, `d1122d8`). +* `epistemic-types` `docs/secret-types.adoc` (PR #37, `eb810d4`; history: + PR #31 `c71cc257`, PR #33 `d97ecaab`). +* `epistemic-types#32` (D154 comment, 2026-09-30) and `epistemic-types#29` + (closed 2026-09-27). +* `nextgen-typing#118` and `docs/TYPE-CONNECTIONS.adoc`; `valence-shell#210`, + PR #211, `docs/THEORY-FEED.adoc`, `#92`; `secret-types#2`; Anytype#15; + SystemET PR #17. diff --git a/docs/secret-types.adoc b/docs/secret-types.adoc index 01dd2c2..eec16be 100644 --- a/docs/secret-types.adoc +++ b/docs/secret-types.adoc @@ -4,7 +4,7 @@ :toc: macro :toclevels: 3 :icons: font -:revdate: 2026-09-27 +:revdate: 2026-10-05 [abstract] This note records a concrete first model for issue #32: a two-level, @@ -47,14 +47,58 @@ Status of the related issues: * `epistemic-types#29` (preservation of the original note) is resolved and stays closed. * `epistemic-types#32` ("Specify an in-repository security model for secret - types") is obsolete as titled: the work moves to `hyperpolymath/secret-types` - (D153/D154). Until that transfer lands, this note and issue #32 remain the - record; the replacement issue is the transferred #32 itself, not a duplicate. + types") **stays in this repository and stays open.** The specification work + moved to `hyperpolymath/secret-types` (D153/D154), but the issue is the + origin/decision record here: no transfer of the issue has occurred or is + required by the 2026-10-04 placement decision, and it must not be closed + merely because the standalone repository exists. Closure waits on the + standalone specification's review checklist being completed item by item + (`secret-types` `docs/secret-types.adoc` § "Review checklist before + implementation"), which is not complete as of 2026-10-05. + +[[transition_review]] +== Cross-reference review — 2026-10-05 + +The Secret Types transition — the migration recorded by +link:https://github.com/hyperpolymath/secret-types/pull/4[`secret-types` PR #4], +commit `d1122d8474f3e2f389d494473aac51164f1747bc`, merged 2026-10-04 — was +reviewed against this repository's docs and tracked work. The full record is in +link:secret-types-transition-review-2026-10-05.adoc[the transition review]; the +conclusions: + +* **The canonical specification is standalone.** `hyperpolymath/secret-types` + `docs/secret-types.adoc` (scope statement, two-level `Public ⊑ Secret` model, + low-observer attacker, noninterference target, non-claims, review checklist) + plus `docs/decisions/0004-standalone-repo-and-scope.adoc`. Provenance was + verified: the adopted text is this note at blob + `583017cfd5fab189ca17128d01c7eddb494d8476` — the PR #33 revision of + 2026-09-27 — not the initial PR #31 draft. +* **Moved:** the specification and its item-by-item review; all follow-on formal + work (lattice reuse, the noninterference theorem, audited declassification, + module and rejection fixtures, any runtime correspondence argument); the + scaffolding/mint (`secret-types#2`); and the family-map registration (D153, + owned by `nextgen-typing#118` / `docs/TYPE-CONNECTIONS.adoc`). +* **Remains here:** this boundary/history note; issue #32 as the origin/decision + record (**open, no transfer**); the statements about this repository's + interfaces (`Access.Preorder`, `BeliefModality`, `Warrant`, + `EchoBridge.Grade`), which the standalone specification explicitly does not + re-home and does not treat as confidentiality guarantees; and the Agda + `--safe --without-K` proof gate. +* **Follow-up belongs elsewhere:** the family-map row (`nextgen-typing#118`; no + secret-types row exists in `TYPE-CONNECTIONS.adoc` as of 2026-10-05); the + stale "mint it or fold it into `epistemic-types#32`" text and the RMO + inference in `valence-shell` `docs/THEORY-FEED.adoc` (under + `valence-shell#210`; `valence-shell#92` remains unselected as a consumer); and + the grade-instance neighbour comparison (Anytype#15, still open). + +Nothing was moved or deleted by this review, no issue ownership was +transferred, and the tracking update for #32 is prepared but not posted (the +standalone review checklist is incomplete; see the review record). == Decision offered for issue #32 -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 +PR #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: * **Accept as a distinct research target:** static confidentiality / information @@ -73,8 +117,12 @@ following decisions for review: <> sets the early repository gate. 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. +implementation. Keep issue #32 open **in this repository**: the baseline's +item-by-item acceptance is now the review checklist of the standalone +specification (`secret-types` `docs/secret-types.adoc` § "Review checklist +before implementation"), which is not yet complete; no issue transfer is +required or planned. Do not close or transfer this issue merely because +`hyperpolymath/secret-types` exists. == What this repository currently provides @@ -320,6 +368,16 @@ 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. +Re-checked 2026-10-05: SystemET PR #17 is still merged at +`a11c98774c8c4a1b35c1e3bd9145a191dffb3840` (2026-07-21); Anytype#15 is still +open (retitled "ET-5: only 2 of the named grade disciplines have instances"); +the standalone specification landed as `secret-types` PR #4 (`d1122d8`, +2026-10-04); `nextgen-typing` `docs/TYPE-CONNECTIONS.adoc` still carries no +secret-types row, and `valence-shell` `docs/THEORY-FEED.adoc` still records the +pre-2026-10-04 "mint it or fold it" alternative. None of these is a dependency +or a proof. See <> above and +link:secret-types-transition-review-2026-10-05.adoc[the transition review]. + === Placement decision for the next step [NOTE] @@ -327,7 +385,9 @@ link:https://github.com/hyperpolymath/echo-types/blob/main/docs/adjacency/inform ==== This section records the 2026-09-27 recommendation ("no new repository yet"). The owner decided on 2026-10-04 that `hyperpolymath/secret-types` is the -standalone home; see <> above. +standalone home (recorded in `secret-types` ADR +`docs/decisions/0004-standalone-repo-and-scope.adoc`, landed by PR #4, +`d1122d8`); see <> above. ==== **Do not create a new repository from issue #32 alone, and do not add a @@ -377,6 +437,15 @@ before this project relies on it. == Review checklist before implementation +[NOTE] +==== +The live checklist is now the standalone specification's "Review checklist +before implementation" (`secret-types` `docs/secret-types.adoc`). The list below +is retained as the origin record; its item 5 (placement) was decided on +2026-10-04 — a standalone calculus repository — and items 1–4 and 6 await the +standalone review. This list is not an agreement already reached here. +==== + Issue #32's first-stage acceptance should require agreement on all of the following, not just agreement on the name `Secret`: @@ -406,3 +475,9 @@ prose-specification step. residues and the distinct resource-bound axis. * link:proof-transport.adoc[Proof transport] — verification relative to an explicit meaning, with its own trust boundary. +* link:secret-types-transition-review-2026-10-05.adoc[Secret Types transition + review] — the cross-reference review, the ownership split, and the prepared + (not posted) update for issue #32. +* link:https://github.com/hyperpolymath/secret-types/blob/main/docs/secret-types.adoc[`secret-types` canonical specification] + and link:https://github.com/hyperpolymath/secret-types/blob/main/docs/decisions/0004-standalone-repo-and-scope.adoc[ADR 0004] + — the standalone work; not imported here.