diff --git a/.machine_readable/descriptiles/META.a2ml b/.machine_readable/descriptiles/META.a2ml index 552e79c..6e97d15 100644 --- a/.machine_readable/descriptiles/META.a2ml +++ b/.machine_readable/descriptiles/META.a2ml @@ -74,7 +74,7 @@ title = "Secret types and information-flow control are specified outside this re 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 (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)." +consequence = "The epistemic core keeps its scope: no confidentiality claim attaches to BeliefModality, Echo grades, or Access. epistemic-types#29 stays closed. Issue #32 was closed on 2026-10-05 as delivered here - no transfer and no duplicate; do not reopen it. Its successor guard is epistemic-types#39. The standalone repository is no longer specification-only: at ccdcb3ec42792337a9ab6047e1f99de9d20a4f96 (2026-10-19) TINI at the two-point lattice and over a Lattice record are PROVEN and its proof gate is green; declassification is not yet implemented. See docs/secret-types.adoc section Status update 2026-10-25." [development-practices] build-tool = "just" diff --git a/.machine_readable/descriptiles/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml index 4a37b81..574218e 100644 --- a/.machine_readable/descriptiles/STATE.a2ml +++ b/.machine_readable/descriptiles/STATE.a2ml @@ -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; 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." +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 was closed on 2026-10-05 as delivered here, with no transfer (none required); do not reopen it, transfer it, or duplicate it - the successor guard is epistemic-types#39. The standalone repository is no longer specification-only: at ccdcb3ec42792337a9ab6047e1f99de9d20a4f96 (2026-10-19) its proof gate is green, TINI at the two-point lattice and over a Lattice record are PROVEN, and declassification is not yet implemented. Pointers: docs/secret-types.adoc section Status update 2026-10-25, and docs/secret-types-transition-review-2026-10-05.adoc kept as history." [build] checker = "Agda 2.6.4.3 (CI-matched)" diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 953ca4c..3d9f0ba 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; issue #32 stays open here as the origin/decision record (no transfer) until the standalone specification's review checklist completes." +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 was closed on 2026-10-05 as delivered here (no transfer); do not reopen, transfer, or duplicate it - the successor guard is #39. The standalone repository now carries a proved noninterference theorem (ccdcb3ec42792337a9ab6047e1f99de9d20a4f96, 2026-10-19); see docs/secret-types.adoc section Status update 2026-10-25." [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; 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).", + "Secret types and information-flow control stay outside this repository (D153/D154; canonical specification in hyperpolymath/secret-types). Issue #32 is closed (2026-10-05, delivered here; no transfer): do not reopen, transfer, or duplicate it, and use the successor guard #39 for pointer updates (docs/secret-types.adoc section Status update 2026-10-25).", ] [ecosystem] diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index b0d979b..575e01c 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -12,6 +12,36 @@ 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-25]] +==== Changed — 2026-10-25 + +* Secret-types pointer sync (issue #39, items 1 and 3). `epistemic-types#32` was + **closed on 2026-10-05T06:37Z** by the owner as delivered here, with no + transfer ("no transfer of this issue occurred or is required, and none should + be attempted"); the successor guard is `#39`. The previous text — that #32 + stays open here and must not be closed — was accurate on 2026-10-05 and is now + false, so `docs/secret-types.adoc` (new section *Status update — 2026-10-25* + plus corrected boundary, transition-review and decision paragraphs), + `docs/secret-types-transition-review-2026-10-05.adoc` (kept as history, with + dated supersession notes), `README.adoc`, `docs/README.adoc`, `STATE.a2ml`, + `META.a2ml` (ADR-007) and `0-AI-MANIFEST.a2ml` were corrected. The + machine-readable agent instruction that said "do not close #32" now says it is + closed and must not be reopened. +* Recorded the standalone repository's current state at + `hyperpolymath/secret-types` `main` + `ccdcb3ec42792337a9ab6047e1f99de9d20a4f96` (2026-10-19, proof gate green in + run 39305922644): N-1, N-2, N-3 and N-7 PROVEN (TINI at the two-point lattice + and over an arbitrary `Lattice` record, public-expression agreement, + confinement), N-4/N-5/N-6 TESTED, N-8 PROVEN (countermodels). The fragment has + no declassification, so D154's audited-declassification requirement is not yet + implemented. +* Recorded that D153's family-map row landed in `nextgen-typing` + `docs/TYPE-CONNECTIONS.adoc` on 2026-10-05 and `nextgen-typing#118` is closed + (that map's explanatory note still claims no noninterference theorem exists), + and that `valence-shell` `docs/THEORY-FEED.adoc` remains stale under `#210` + with `#92` unselected. Those corrections belong to their own repositories. +* No Agda source changed; the proof gates are unaffected. + [[changed--2026-10-05]] ==== Changed — 2026-10-05 diff --git a/README.adoc b/README.adoc index 486d585..7d3f06f 100644 --- a/README.adoc +++ b/README.adoc @@ -211,10 +211,13 @@ 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. Issue #32 stays - open in this repository as the origin/decision record (no transfer); + the decision and the pointer. No `Secret` API exists here. Issue #32 was + closed on 2026-10-05 as delivered here (no transfer; the successor guard is + link:https://github.com/hyperpolymath/epistemic-types/issues/39[#39]); link:docs/secret-types-transition-review-2026-10-05.adoc[the transition - review] records the cross-references. + review] records the cross-references, and the boundary note's 2026-10-25 + status update records the standalone repository's proved noninterference + theorem. == Build diff --git a/docs/README.adoc b/docs/README.adoc index 4574e9b..444eb03 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -40,14 +40,17 @@ 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. Issue #32 stays open here as the - origin/decision record (no transfer). + theorem exists in this repository. Issue #32 was closed on 2026-10-05 as + delivered here (no transfer; successor guard #39), and the note's 2026-10-25 + status update records the standalone repository's proved noninterference + theorem. | `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). + and the exact proposed issue #32 update (prepared, never posted — the owner + posted a different closing comment on 2026-10-05). Kept as history. |=== == Continuity foundations diff --git a/docs/secret-types-transition-review-2026-10-05.adoc b/docs/secret-types-transition-review-2026-10-05.adoc index 1d043f9..05a2929 100644 --- a/docs/secret-types-transition-review-2026-10-05.adoc +++ b/docs/secret-types-transition-review-2026-10-05.adoc @@ -16,6 +16,17 @@ 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*. +[NOTE] +==== +**Historical record — 2026-10-05.** The text above and throughout this document +is kept as written on 2026-10-05. It was superseded in part the same day: the +owner closed `epistemic-types#32` at 06:37Z as delivered here, without a +transfer, and opened `#39` as the successor guard. See +link:secret-types.adoc#status_2026_10_25[the 2026-10-25 status update] in +`docs/secret-types.adoc` for the current state, including the standalone +repository's proved noninterference theorem. Do not reopen #32. +==== + toc::[] == Scope and constraint @@ -78,8 +89,10 @@ repositories, and the destination repositories named below. 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. +| *2026-10-05 assessment, now historical:* the required review was judged + incomplete, so #32 was not to be closed and the specification was not to be + described as accepted. The owner closed #32 later that day (06:37Z); the + specification is still not described as accepted. |=== == Findings @@ -145,8 +158,9 @@ repositories, and the destination repositories named below. | `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 +| `epistemic-types#32` — as of 2026-10-05, open with no transfer; **closed + 2026-10-05T06:37Z as delivered here** (no transfer), with `#39` as the + successor guard | Non-claims about `Access.Preorder`, `BeliefModality`, `Warrant`, `EchoBridge.Grade`, and the `--safe --without-K` proof gate @@ -159,15 +173,18 @@ repositories, and the destination repositories named below. | `secret-types#2` |=== -== Prepared update for issue #32 — not posted +== Prepared update for issue #32 — never posted -The exact proposed comment follows. It is **prepared and not posted**: the +The exact proposed comment follows. It is **prepared and never 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. +and any required review is complete") was judged unmet on 2026-10-05, because +the standalone specification's own review checklist was incomplete and PR #37's +review finding was unresolved. The credential state for issue writes was +documented as unavailable (`403`) on 2026-10-04 in `secret-types` PR #4. + +The owner instead posted a different closing comment on 2026-10-05T06:37Z and +closed the issue. The prepared text below is retained unmodified as the record +of what this review proposed; nothing in it should be read as posted. [source,markdown] ---- @@ -240,7 +257,7 @@ Review record: `epistemic-types` (`arena/01a10aaf-epistemic-types`); pending review). ---- -== What would unblock the tracking update +== What would unblock the tracking update — historical (2026-10-05) * The standalone specification's "Review checklist before implementation" is completed item by item, or the owner explicitly accepts the baseline; and @@ -248,7 +265,33 @@ Review record: `epistemic-types` 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. +As written on 2026-10-05: "Until then: #32 open, in this repository; nothing +moved; nothing closed." The owner resolved the question the same day by closing +#32 (06:37Z) and opening #39 as the guard; see <>. + +[[status_2026_10_25]] +== Status update — 2026-10-25 + +* `epistemic-types#32` — **closed** 2026-10-05T06:37Z as delivered here, with + no transfer (and none required); `#39` is the successor guard. +* `epistemic-types#29` — remains closed. +* `secret-types` `main` `ccdcb3ec42792337a9ab6047e1f99de9d20a4f96` + (2026-10-19): proof gate green + (link:https://github.com/hyperpolymath/secret-types/actions/runs/39305922644[run 39305922644]); + reported status: N-1, N-2, N-3, N-7 and N-8 are **PROVEN**; N-4, N-5 and + N-6 are **TESTED**. **D154's audited-declassification requirement is not + implemented**: the fragment contains no declassification, and procedures, + concurrency and timing are likewise outside it. +* Family map: the `nextgen-typing` row landed 2026-10-05 and `#118` is closed; + its explanatory note still says no noninterference theorem exists, which the + proofs supersede. +* `valence-shell` `docs/THEORY-FEED.adoc` remains stale (un-minted wording, + `?` feed grade, "fold it into epistemic-types#32"); `#210` and `#92` remain + open. +* The live specification checklist and status text are owned by + `secret-types`; reconciling them is that repository's work, not this one's. + +Nothing moved, nothing was deleted, and no `Secret`/IFC claim is added here. == References diff --git a/docs/secret-types.adoc b/docs/secret-types.adoc index eec16be..40e37af 100644 --- a/docs/secret-types.adoc +++ b/docs/secret-types.adoc @@ -47,14 +47,71 @@ 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") **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. + types"). *Recorded 2026-10-04, superseded 2026-10-05:* the issue was to stay + in this repository and to stay open as the origin/decision record, with no + transfer of the issue required by the 2026-10-04 placement decision and + closure waiting on the standalone specification's review checklist. The owner + **closed #32** on 2026-10-05T06:37Z as delivered here; see + <>. Do not reopen it: model work belongs in the standalone + repository, and the guard that keeps this pointer accurate is + link:https://github.com/hyperpolymath/epistemic-types/issues/39[issue #39]. + +[[status_2026_10_25]] +== Status update — 2026-10-25 + +This section records the current state and supersedes the present-tense +statements about issue #32 elsewhere in this note and in +link:secret-types-transition-review-2026-10-05.adoc[the 2026-10-05 transition +review]. Those records keep their 2026-10-05 text as history, per issue #39. + +**The issue.** `epistemic-types#32` was **closed** on 2026-10-05T06:37Z by the +owner as "delivered here; the model's acceptance now lives in +`hyperpolymath/secret-types`". The closing comment states that no transfer of +the issue occurred or is required and that none should be attempted. The +successor guard is +link:https://github.com/hyperpolymath/epistemic-types/issues/39[issue #39] +("keep the pointer accurate, keep claims out"). Do not reopen #32. + +**The standalone repository.** `hyperpolymath/secret-types` is no longer +specification-only. At `main` `ccdcb3ec42792337a9ab6047e1f99de9d20a4f96` +(2026-10-19, PR #10) its proof gate is green +(link:https://github.com/hyperpolymath/secret-types/actions/runs/39305922644[run 39305922644]), +and its `PROOF-STATUS.adoc` records, all under `--safe --without-K` with no +postulates: + +* N-1 termination-insensitive noninterference at the two-point lattice — + **PROVEN**; +* N-2 public expressions read the same in low-equivalent stores — **PROVEN**; +* N-3 confinement under a secret program counter, loops included — **PROVEN**; +* N-7 TINI over an arbitrary `Lattice` record and down-closed observer — + **PROVEN**; +* N-4 explicit and implicit flows refused, and shown to leak by computation — + **TESTED**; +* N-5 termination-insensitivity is real, not vacuous — **TESTED**; +* N-6 the laws census (exactly three laws used) — **TESTED**; +* N-8 the necessity of each census law — **PROVEN** (countermodels). + +The fragment is two variables, with no declassification, procedures, +concurrency, or timing. **D154's "declassify only at explicit audited points" +is therefore not yet implemented**; the baseline declassifies nothing. + +**D153 registration.** The family row landed in `nextgen-typing` +`docs/TYPE-CONNECTIONS.adoc` on 2026-10-05 and `nextgen-typing#118` is closed, +so the type-family-map requirement of D153 is satisfied. That map's +explanatory note still says the scope statement records that no noninterference +theorem exists yet, which the proofs above supersede; the correction belongs to +`nextgen-typing`. + +**Still stale elsewhere (recorded, not edited here).** `valence-shell` +`docs/THEORY-FEED.adoc` still grades the family `?`, records "mint it … or fold +it into epistemic-types#32" as an open owner call, and describes +`secret-types` as un-minted (`valence-shell#210` remains open; `#92` remains +unselected as a consumer). `secret-types#2` — mint and family-map registration +— remains open, as do that repository's own review checklist and its +"specification only" status text. + +Nothing in this update adds a `Secret` type, IFC calculus, declassification +rule, or noninterference theorem to this repository. [[transition_review]] == Cross-reference review — 2026-10-05 @@ -78,22 +135,24 @@ conclusions: 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). +* **Remains here:** this boundary/history note; issue #32 as the vintage + origin/decision record (closed 2026-10-05, no transfer — see + <>); 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 (landed in + `nextgen-typing` `docs/TYPE-CONNECTIONS.adoc` on 2026-10-05; `#118` closed, see + <>); 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). +transferred, and the tracking update for #32 was prepared but not posted at the +time. The owner subsequently closed #32 with a different closing comment on +2026-10-05T06:37Z; see <>. == Decision offered for issue #32 @@ -117,12 +176,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 **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. +implementation. *Superseded 2026-10-25:* this paragraph previously asked readers +to keep issue #32 open in this repository, because acceptance was to be the +standalone specification's review checklist and no transfer was required or +planned. That was the correct 2026-10-05 position. The owner closed #32 on +2026-10-05T06:37Z as delivered here, without a transfer; see +<>. Do not reopen it. == What this repository currently provides @@ -442,8 +501,11 @@ before this project relies on it. 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. +2026-10-04 — a standalone calculus repository. As of 2026-10-25 the standalone +repository has landed the typing rules and a proved noninterference theorem, +while its own checklist is still written as incomplete; the reconciliation +belongs to `secret-types` (see <>). This list is not an +agreement already reached here. ==== Issue #32's first-stage acceptance should require agreement on all of the @@ -476,8 +538,12 @@ prose-specification step. * 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. + review] — the cross-reference review and the ownership split, kept as the + 2026-10-05 historical record; its prepared update for issue #32 was never + posted (see <>). +* link:https://github.com/hyperpolymath/epistemic-types/issues/39[Issue #39] — + the boundary guard that keeps this pointer accurate and keeps `Secret`/IFC + claims out of this repository. * 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.