From 19f635ea8808e898d499ec94a9c1bbfd95f18251 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 5 Oct 2026 07:14:34 +0100 Subject: [PATCH 1/2] docs: record the epistemic-types transition review and correct its cross-references Records the 2026-10-04 Secret Types transition as verified on 2026-10-05, per ADR-0004's consequence list (cross-links that still describe the old alternatives need updating). - docs/epistemic-types-transition-review.adoc: new. Verifies the evidence in both repositories (secret-types PR #4; epistemic-types PRs #31/#33/#37; issue #29 closed COMPLETED; issue #32 open with the D154 ruling), checks each cross-reference claim, records what moved here, what remains owned by epistemic-types, and routes follow-up work. It includes the exact prepared (unposted) tracking updates: a comment for epistemic-types#32, a status refresh for secret-types#2, and a wording fix for epistemic-types docs/secret-types.adoc. They are unposted because this session's GitHub token has no issue-write access (403 on the labels endpoint, quoted in the document). - docs/secret-types.adoc: the review checklist no longer claims the handoff is tracked in secret-types#2; it now states that epistemic-types#32 remains the open, untransferred origin record. Provenance gains the transition-review entry; revdate -> 2026-10-05. - README.adoc and docs/README.adoc: point to the review record. Nothing was moved, deleted, transferred or closed. No issue state was changed by this work, and the history in both repositories is preserved. Commit created through the GitHub API so it is GitHub-signed (Require-Signed-Commits ruleset). --- README.adoc | 6 + docs/README.adoc | 1 + docs/epistemic-types-transition-review.adoc | 413 ++++++++++++++++++++ docs/secret-types.adoc | 19 +- 4 files changed, 435 insertions(+), 4 deletions(-) create mode 100644 docs/epistemic-types-transition-review.adoc diff --git a/README.adoc b/README.adoc index ed5fcac..bae32a7 100644 --- a/README.adoc +++ b/README.adoc @@ -60,6 +60,12 @@ this standalone home), the first model, and the explicit non-claims. * Neighbours and their limits (`epistemic-types`, `systemet`/`anytype`, `echo-types`, `tropical-types`) are covered in the canonical spec. None is a dependency. +* The origin record stays with `epistemic-types`: its + link:https://github.com/hyperpolymath/epistemic-types/blob/main/docs/secret-types.adoc[boundary/history note] + and link:https://github.com/hyperpolymath/epistemic-types/issues/32[issue #32] + remain open there, untransferred. link:docs/epistemic-types-transition-review.adoc[The transition review] + records the verified cross-references and the prepared, unposted tracking + updates. == Licence diff --git a/docs/README.adoc b/docs/README.adoc index dc7274f..2e8c712 100644 --- a/docs/README.adoc +++ b/docs/README.adoc @@ -43,6 +43,7 @@ and CI fails if it goes stale, so prefer it over any hand-written listing. * link:governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc[governance/SOFTWARE-DEVELOPMENT-APPROACH.adoc] * link:MAINTAINERS.adoc[MAINTAINERS.adoc] — the single maintainer roster. * link:GOVERNANCE.adoc[GOVERNANCE.adoc] — the governance model. +* link:epistemic-types-transition-review.adoc[epistemic-types transition review] — verified cross-references for the 2026-10-04 transition, the ownership split, and the prepared (unposted) issue updates. [NOTE] ==== diff --git a/docs/epistemic-types-transition-review.adoc b/docs/epistemic-types-transition-review.adoc new file mode 100644 index 0000000..d6cbf07 --- /dev/null +++ b/docs/epistemic-types-transition-review.adoc @@ -0,0 +1,413 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += Epistemic Types transition review: verified cross-references +:toc: macro +:toclevels: 3 +:icons: font +:revdate: 2026-10-05 + +[abstract] +Review of the 2026-10-04 Secret Types transition as it stands in +`hyperpolymath/epistemic-types`. It verifies the cross-references in both +directions, records what work has moved to this repository, what remains owned +by `epistemic-types`, and where follow-up work belongs. It changes no issue +state anywhere: no issue was closed, reopened, transferred, re-owned, relabelled +or commented on, because this session's GitHub token has no issue-write access +(verified below). The exact proposed tracking updates are prepared in +<> and are **unposted**. + +toc::[] + +== What this review is, and is not + +This is a *verification and cross-reference record*, prepared on the session +branch `arena/01a10aad-secret-types`. It is not a decision, not a transfer, and +not a claim that the Secret Types specification has passed review. + +* It does not move, delete or rewrite any work in `epistemic-types`. +* It does not transfer issue ownership, close issue #32, or duplicate the + decision record that #32 started. +* It does not adopt the model: the canonical scope statement in this repository + states that its review checklist has not been completed item by item, and + ADR-0004 states the model is not yet accepted item by item. That review is + still outstanding, so the corresponding tracking stays open. + +Everything below was checked on 2026-10-05 against the public repositories, the +two git trees, and the GitHub API. The commands are listed in +<>. + +[[evidence_checked]] +== Evidence checked + +[cols="1,2,3",options="header"] +|=== +| Repository | Artefact and revision | What it evidences + +| `secret-types` +| PR #4, merged 2026-10-04T09:07:42Z, commit `906e110ff7ba23b51409f53a028d1c9e8b9c6a2b`; files `docs/secret-types.adoc` (new, 317 lines), `README.adoc`, `docs/decisions/0004-standalone-repo-and-scope.adoc` +| The source change of the transition: this repository is minted in scope as the standalone home, with the canonical scope statement, the first model, and ADR-0004 (owner confirmation 2026-10-04, superseding the "fold into `epistemic-types`#32" alternative). + +| `secret-types` +| `docs/secret-types.adoc` "Provenance and status": ported 2026-10-04 from `epistemic-types` `docs/secret-types.adoc`, blob `583017cfd5fa`, landed via PR #33 for #32 on 2026-09-27 +| Verified exact: blob `583017cfd5fab189ca17128d01c7eddb494d8476` is `epistemic-types` `docs/secret-types.adoc` at commit `d97ecaa` (PR #33, merged 2026-09-27T08:14:42Z). + +| `secret-types` +| ADR-0004 "Consequences": cross-links that still describe the old alternatives need updating (`epistemic-types`#32, `nextgen-typing`#118 / `TYPE-CONNECTIONS`, valence-shell `docs/THEORY-FEED.adoc`) +| This review is the follow-up to that consequence list; it records the verified state rather than rewriting the linked work. + +| `secret-types` +| Issues: #2 open (only open issue); PRs #1, #3, #4, #5 merged; no transferred issue present +| No replacement specification issue exists here, and no issue transfer has landed in this repository. + +| `epistemic-types` +| PR #31, merged 2026-09-27T05:25:17Z, commit `c71cc257eec450fde46be85bb8f548ef9974090f`, "Closes #29"; `docs/secret-types.adoc` blob `cf0a152e46c6` +| Landed the preserved note inside `epistemic-types`; closed #29. + +| `epistemic-types` +| PR #33, merged 2026-09-27T08:14:42Z, commit `d97ecaab042ce3b793e151dbead43f9ffb9b88d7`, "docs(security): specify secret-type model boundary (#32)"; blob `583017cfd5fa` +| The revision this repository ported; it referenced #32 but did not close it. + +| `epistemic-types` +| PR #37, merged 2026-10-04T07:57:54Z, commit `eb810d4ee77086383dcf5ac74b8e5676c5b38c1b`; `docs/secret-types.adoc` blob `01dd2c24bd7d` +| The mirror side of the transition: the "Boundary and history — 2026-10-04" section, the superseded placement section, and updates to README, `docs/README.adoc`, CHANGELOG, `STATE.a2ml`, `META.a2ml` (ADR-007) and `0-AI-MANIFEST.a2ml`. + +| `epistemic-types` +| Issue #32: OPEN, labels design / priority:p1 / scope:repo / security / feeds:valence-shell; one comment, the D154 ruling (2026-09-30T14:15Z); timeline has no transfer event +| The origin decision record is open and explicitly supported by the owner ruling; nothing here has been transferred or re-owned. + +| `epistemic-types` +| Issue #29: CLOSED as COMPLETED, 2026-09-27T05:58:28Z +| Historical work, resolved by landing the note; no restoration of the retired pre-#22 `AUDIT.adoc` (current `AUDIT.adoc` is the #22 rewrite `ad14e35`; the older text stays in history at `a0153f4`). + +| `hyperpolymath/standards` +| issue #787, comment 5912989503 (decision harvest, 2026-09-30T14:10Z): D153 on `secret-types#2`, D154 on `epistemic-types#32` +| The ruling context: D153 defines a secret type and requires type-family-map registration; D154 fixes lattice reuse (two-point first), noninterference, and declassification only at explicit audited points. + +| neighbours +| `nextgen-typing#118` open with "secret-types pending" in the title; `valence-shell#210` open (D127 umbrella); `valence-shell#92` open and blocked on its own dependencies +| The family-map row is still pending, and no consumer or frontier item has been selected for this project. +|=== + +== Cross-reference verification + +[cols="2,2,1",options="header"] +|=== +| Claim in one repository | Verified state, 2026-10-05 | Verdict + +| This repository: "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)." +| Blob matches `d97ecaa` exactly; PR #33 merged 2026-09-27T08:14:42Z. The port is a point-in-time snapshot: the origin note has since been revised (blob `01dd2c24bd7d`, 2026-10-04) to mark the placement superseded. +| Accurate + +| This repository: "its handoff to this repository is tracked in secret-types#2" +| `secret-types#2` tracks the repository being un-minted, the scaffolding sweep and type-family-map registration. It is not a handoff tracker, and no issue transfer has occurred. +| *Inaccurate — corrected in this change* + +| `epistemic-types` `docs/secret-types.adoc`: "the replacement issue is the transferred #32 itself, not a duplicate" +| No transfer has occurred or is in flight: no transfer event on #32, no replacement issue in `secret-types`, and issue writes currently return 403 (matching `STATE.a2ml`'s "pending GitHub issue-write access"). +| *Not evidenced — wording fix prepared, unapplied (belongs to `epistemic-types`)* + +| `epistemic-types` `docs/secret-types.adoc`: "`epistemic-types#29` ... is resolved and stays closed" +| #29 is CLOSED as COMPLETED since 2026-09-27T05:58:28Z; PR #31 landed the note; the preserved commit `bde5842e` has no ref but is still retrievable by SHA through the API; `AUDIT.adoc` was not restored. +| Accurate + +| `epistemic-types` README: secrecy work is out of scope there; the standalone home is `hyperpolymath/secret-types` (D153/D154) +| This repository exists, is public, and carries the canonical scope statement and ADR-0004. +| Accurate + +| This repository: statements about `epistemic-types` modules "remain statements about *that* repository's narrower interfaces. They are not re-homed here." +| The module-by-module material (`Modality`, `Access.Preorder`, `BeliefModality`'s missing `reflect`, `FactiveModality.reflect`, `Warrant`, `ProofTransport`, `Echo`/`BoundedEcho`, the `--safe` gate) is retained in the origin note and is absent from this repository's canonical spec. +| Accurate + +| This repository: no consumer and no frontier item selected; `valence-shell#92` is the nearest frontier item by name only +| `valence-shell#92` is open and still blocked; the RMO key-provisioning use remains an inference in valence-shell's direction doc, not a selected consumer. +| Accurate + +| This repository: the TYPE-CONNECTIONS row is proposed in `nextgen-typing#118` +| #118 is open and still ends "secret-types pending"; no row has landed. +| Accurate + +| `secret-types#2` body: "This repo is un-minted. The README is still" unfilled template tokens. +| Stale since PR #4 (2026-10-04): the README is real project content. The placeholder sweep across the rest of the tree remains outstanding. +| *Premise stale — update prepared, unposted* + +| Attribution of rulings: D153 on `secret-types#2`, D154 on `epistemic-types#32` +| Matches the estate harvest table and both on-issue ruling comments. +| Accurate +|=== + +== What has moved, what remains, where follow-up belongs + +=== Moved to this repository (now canonical here) + +* The confidentiality-label model: two labels `Public ⊑ Secret`, the order + direction, the join of dependencies, and the clearance reading. +* The use case and trust boundary: the pure, total policy/configuration + function; trusted source labels that no annotation can authenticate. +* The attacker and observation model, including what it assumes and what it + excludes (no I/O, state, concurrency, divergence, or side channels). +* Permitted and forbidden flows, including implicit flow, and the baseline's + refusal to declassify anything (D154 admits declassification only at explicit + audited points, which the baseline does not yet specify). +* The low-equivalence and termination-insensitive noninterference target. +* The candidate `Secret ℓ A` surface and its limit (no unrestricted + eliminator, no observer API without a clearance semantics). +* Ownership of the remaining first-stage review and of all later stages: + syntax and typing rules, expected-rejection fixtures, the semantic + noninterference proof, and any runtime correspondence argument. +* The placement decision itself: standalone repository (checklist item 5 of the + origin note is now decided, which removes one previously open question). + +=== Remains owned by `epistemic-types` + +* Issue #32 as the origin decision record, open and untransferred, with the + D154 ruling comment of 2026-09-30 unchanged and still governing. +* `docs/secret-types.adoc` there as the boundary/history note (current blob + `01dd2c24bd7d`): why that repository hosts no `Secret` API, the superseded + 2026-09-27 placement recommendation, and the retained checklist as history. +* The statements about *that* repository's own interfaces: `Modality`, + `Access.Preorder` / `AccessibleModality.increase`, `BeliefModality`'s missing + `reflect` (a factivity gap, not a confidentiality result), `FactiveModality`, + `Warrant` / `ProofTransport`, `Echo` / `BoundedEcho` grades, and the + 17-module `--safe --without-K` gate. None of these is a security guarantee, + and none is re-homed here. +* The "`Access.Preorder` is not the security interface" comparison and the + repository-boundary analysis. +* The README out-of-scope entry, the documentation-index entry, the CHANGELOG + entries, `STATE.a2ml`, `META.a2ml` ADR-007, and the `0-AI-MANIFEST.a2ml` + entries. +* The closed history of #29 and of the preservation branch. + +=== Follow-up routing + +[cols="2,1,2",options="header"] +|=== +| Work item | Home | Status + +| Item-by-item review of the model checklist | this repository | Not started; the scope statement says so explicitly. + +| Syntax, typing rules, proof controls, expected-rejection fixtures | this repository | No issue exists yet here; the origin note keeps them as its checked follow-on stages. + +| The noninterference theorem | this repository | Not proved; stated only as the future target. + +| `just repo-init` placeholder sweep; type-family-map registration (D153) | this repository, tracked in issue #2 | Open; the map row is still "pending" in nextgen-typing#118. + +| Tracking disposition of `epistemic-types#32` (transfer it, or keep it as the origin record) | owner decision | Deliberately untouched by this review; #32 stays open and untransferred meanwhile. + +| Wording fix in `epistemic-types` `docs/secret-types.adoc` (the "transferred #32" sentence) | `epistemic-types` | Prepared here, unapplied; this session cannot push a branch there. + +| valence-shell `docs/THEORY-FEED.adoc` mint-vs-fold sentence and the RMO inference cell | valence-shell | Recorded in ADR-0004 consequences; not a selected consumer, no claim made here. + +| `occupancy-types` ULTRAPLAN no-imports mention | occupancy-types | Noted in `secret-types#2`; belongs to that repository's own tracked work. +|=== + +== Review status of `epistemic-types#32` + +The transition is evidenced in both repositories. The review is not complete. +That is the whole reason #32 stays open: + +* The origin note's checklist (labels and order; use case and low-observer + boundary; out-of-scope items; the exact noninterference statement and a + future soundness proof; placement; then syntax and typing rules) has been + carried into this repository's canonical spec, but no one has accepted it + item by item. ADR-0004 records the model as not yet accepted item by item. +* Issue #32's own acceptance criteria ask for the chosen definitions and + non-claims to be recorded, and for `BeliefModality`'s missing `reflect` and + `EchoBridge.Grade` never to be described as a confidentiality or leakage + guarantee. The recordings exist in both repositories, and both keep that + non-claim; but the required review has not happened, and the follow-on + module, fixtures, theorem and runtime integration were always separate, + separately reviewed work. +* Neither a closure nor a transfer is ours to make. No issue write is + available to this session at all (evidence in <>). + +[[prepared_updates]] +== Prepared updates (not posted) + +=== Why they are unposted + +On 2026-10-05 the session's token could read both repositories but not write +issues. The decisive probe: + +[source,bash] +---- +gh api -X POST repos/hyperpolymath/epistemic-types/issues/32/labels \ + -f 'labels[]=zzz-no-such-label-zzz' +# {"message":"Resource not accessible by integration", ... "status":"403"} +---- + +The same probe against `secret-types#2` returns the same 403. A token with +issue-write would have created the label instead of returning 403. This matches +the record in `secret-types` PR #4 ("`pull_requests=write` but not +`issues=write`") and `epistemic-types` `STATE.a2ml`'s "pending GitHub +issue-write access". + +Consequently **neither text below was posted, and no issue state was +changed**. They are stored here verbatim so that whoever next holds issue-write +can post them unchanged. + +=== Prepared comment for `epistemic-types#32` (unposted) + +[source,markdown] +---- +### Secret Types transition — verified cross-references (review recorded 2026-10-05) + +**Status: this issue stays open. Nothing is transferred, closed, or re-owned.** +(This update was prepared by the secret-types transition-review session but not +posted: that session's token has no issue-write access.) + +Verified 2026-10-05 against both repositories: + +- The transition is evidenced. `hyperpolymath/secret-types` PR #4 (merged + 2026-10-04T09:07:42Z, commit `906e110f`) mints the standalone repository: + canonical `docs/secret-types.adoc`, real README, and + `docs/decisions/0004-standalone-repo-and-scope.adoc` (owner confirmation + 2026-10-04, superseding the fold-into-#32 alternative). This repository's + PR #37 (merged 2026-10-04T07:57:54Z, commit `eb810d4`) added the + "Boundary and history — 2026-10-04" section to `docs/secret-types.adoc` + (blob `01dd2c24bd7d`), marked the 2026-09-27 placement section superseded, + and updated README, `docs/README.adoc`, CHANGELOG, `STATE.a2ml`, + `META.a2ml` (ADR-007) and `0-AI-MANIFEST.a2ml`. +- Provenance is exact: `secret-types` cites the ported blob `583017cfd5fa`, + which is this repository's `docs/secret-types.adoc` at PR #33 (`d97ecaa`, + merged 2026-09-27T08:14:42Z). +- `#29` stays closed (COMPLETED 2026-09-27T05:58:28Z), landed by PR #31 + (`c71cc25`). Its AUDIT.adoc criterion is consistent with the tree: the + current `AUDIT.adoc` is the #22 rewrite (`ad14e35`), the pre-#22 text stays + in history at `a0153f4`, and the retired copy was not restored. No action + requested. +- No transfer has occurred and none is in flight: this issue has no transfer + event, `secret-types` has no replacement specification issue, and issue + writes currently fail with 403 — matching `STATE.a2ml`'s "the transfer of + epistemic-types#32 to secret-types is pending GitHub issue-write access and + must not be duplicated". +- Wording fix needed in this repository: the boundary section says "the + replacement issue is the transferred #32 itself, not a duplicate", which + presumes a transfer that has not happened. Suggested replacement: "No + transfer has occurred; `secret-types` has no replacement specification issue + yet, and its only open issue (#2) tracks minting, scaffolding and + type-family-map registration." + +What moved, what remains here, where follow-ups belong: + +- **Moved to `secret-types` (canonical):** the two-level `Public ⊑ Secret` + label model and order direction; the pure/total use case and source-trust + boundary; the low-observer attacker and observation model; permitted and + forbidden flows; the low-equivalence/termination-insensitive + noninterference target; the candidate `Secret ℓ A` surface and its limits; + and ownership of the review checklist, typing rules, expected-rejection + fixtures, the noninterference proof, and any runtime correspondence. +- **Remains owned here:** this issue as the origin decision record (D154, + 2026-09-30, unchanged and still governing); `docs/secret-types.adoc` as the + boundary/history note; the module-by-module statements (`Modality`, + `Access.Preorder`, `BeliefModality`'s missing `reflect` is not + confidentiality, `FactiveModality.reflect`, `Warrant`, `ProofTransport`, + `Echo`/`BoundedEcho` grades, the 17-module `--safe --without-K` gate); + ADR-007 and the machine-readable state. No `Secret` API and no + information-flow implementation are added here. +- **Why open:** `secret-types`' own scope statement records that its review + checklist "has not yet been completed item by item" (ADR-0004: the model + "is not yet accepted item by item"). The transition is evidenced; the + required review is not complete. +- **Owner-gated next steps:** (1) post this update and the `secret-types#2` + update when issue-write access returns; (2) decide the tracking disposition + — transfer this issue by owner action, or keep it here as the origin record + and open an acceptance/review item in `secret-types`; (3) apply the wording + fix above. + +Verification record: `hyperpolymath/secret-types` +`docs/epistemic-types-transition-review.adoc` (branch +`arena/01a10aad-secret-types`; not yet on `main`). +---- + +=== Prepared comment for `secret-types#2` (unposted) + +[source,markdown] +---- +### Status refresh (prepared 2026-10-05; not posted — issue-write unavailable) + +The "un-minted" premise in the body is stale: PR #4 (merged 2026-10-04) landed +a real README, the canonical `docs/secret-types.adoc`, and ADR-0004, so the +repository is minted in scope. What remains from this issue: the +`just repo-init` placeholder sweep across the tree, the one-sentence +question/boundary in TYPE-CONNECTIONS style (the README now states it), and the +family-map row that `nextgen-typing#118` still carries as "secret-types +pending" — D153 requires registration on that boundary. + +Also recorded for accuracy: no transfer of `epistemic-types#32` has occurred, +and this issue is not the handoff tracker for it. The verified cross-references +are in `docs/epistemic-types-transition-review.adoc`; the prepared +`epistemic-types#32` update is stored there. Keeping this issue open. +---- + +=== Prepared wording fix for `epistemic-types` `docs/secret-types.adoc` (unapplied) + +Current text (blob `01dd2c24bd7d`, "Boundary and history — 2026-10-04"): + +[source,text] +---- +* `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. +---- + +Suggested replacement (not applied by this review; it belongs to +`epistemic-types`): + +[source,text] +---- +* `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), and this note and issue #32 remain the origin record. No issue + transfer has occurred as of 2026-10-05: the transfer is pending GitHub + issue-write access, and `secret-types` has no replacement specification issue + yet (its only open issue, #2, tracks minting, scaffolding and type-family-map + registration). Whether #32 is transferred or stays here as the origin record + is an owner decision; either way nothing is duplicated. See the verification + record in `secret-types` `docs/epistemic-types-transition-review.adoc`. +---- + +== History preservation + +* No file was moved, renamed or deleted in either repository by this review. + The only `epistemic-types` changes are the prepared texts above. +* `epistemic-types#29` stays closed with its receipts: PR #31 landed the note + (commit `c71cc25`), the branch `preserve/secret-types-note-2026-07-13` no + longer exists on origin (only `main` does), and the preserved commit + `bde5842e8b619018a751002fbfde9be829fc0974` has no ref but is still + retrievable by SHA through the GitHub API. Nothing was re-opened or + re-litigated. +* The retired pre-#22 `AUDIT.adoc` was not restored; the current file is the + #22 rewrite, and the older text remains in history at `a0153f4`. +* No issue ownership moved. The only write attempt made during this review was + the permission probe quoted above, which applied nothing. + +== Verification limits + +* No `asciidoctor` in this sandbox, so the local AsciiDoc-render gate was not + run here; CI remains the render authority. +* Issue writes are unavailable to this session (403), so every tracking update + is prepared, not posted. +* This session may only push branch `arena/01a10aad-secret-types` in this + repository; a change to `epistemic-types` (such as the wording fix) cannot be + made from here. +* Only public data (both repositories, the API, the `standards` harvest + comment) was used. + +[[how_to_re-verify]] +== How to re-verify + +[source,bash] +---- +gh issue view 32 --repo hyperpolymath/epistemic-types --json state,title,labels,comments +gh api repos/hyperpolymath/epistemic-types/issues/32/timeline --jq '.[].event' +gh api repos/hyperpolymath/epistemic-types/commits/d97ecaab042ce3b793e151dbead43f9ffb9b88d7 \ + --jq '.files[] | {filename, sha, additions}' +gh pr view 4 --repo hyperpolymath/secret-types --json title,mergedAt,files +gh api repos/hyperpolymath/standards/issues/comments/5912989503 --jq .body +git -C epistemic-types ls-remote --heads origin # preserve/* is absent +---- + +A fresh clone of `epistemic-types` at `eb810d4` plus a clone of this repository +at its current `main` is sufficient to reproduce every claim in +<>. diff --git a/docs/secret-types.adoc b/docs/secret-types.adoc index 88434d0..d939bbd 100644 --- a/docs/secret-types.adoc +++ b/docs/secret-types.adoc @@ -4,7 +4,7 @@ :toc: macro :toclevels: 3 :icons: font -:revdate: 2026-10-04 +:revdate: 2026-10-05 [abstract] This is the canonical scope statement for the standalone `secret-types` @@ -279,9 +279,13 @@ import builds in CI. == 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 +The specification issue (filed as `epistemic-types`#32, where it remains open +and untransferred as the origin decision record, with its 2026-09-30 D154 +ruling) asks for the first semantic boundary, not for a proof module. No issue +transfer has occurred as of 2026-10-05; this repository's own minting and +scaffolding are tracked separately in secret-types#2, and the verified +cross-references are recorded in +link:epistemic-types-transition-review.adoc[the transition review]. 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 @@ -300,6 +304,7 @@ 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]] == Provenance and status * Ported and adopted 2026-10-04 from `epistemic-types` @@ -315,3 +320,9 @@ argument. None is part of this prose-specification step. 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. +* Transition review (2026-10-05): the cross-references between this repository + and `epistemic-types` were checked against both trees and are recorded in + link:epistemic-types-transition-review.adoc[`docs/epistemic-types-transition-review.adoc`]. + `epistemic-types`#32 remains open there and no ownership moved; no issue was + closed, re-owned or transferred by the review, and the prepared (unposted) + tracking updates live in that record. From 0dff2c3c58d68d7296b1ab3190cc68e6521b66cf Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 5 Oct 2026 07:21:04 +0100 Subject: [PATCH 2/2] Update docs/epistemic-types-transition-review.adoc Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- docs/epistemic-types-transition-review.adoc | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/docs/epistemic-types-transition-review.adoc b/docs/epistemic-types-transition-review.adoc index d6cbf07..942cf3c 100644 --- a/docs/epistemic-types-transition-review.adoc +++ b/docs/epistemic-types-transition-review.adoc @@ -409,5 +409,9 @@ git -C epistemic-types ls-remote --heads origin # preserve/* is absent ---- A fresh clone of `epistemic-types` at `eb810d4` plus a clone of this repository -at its current `main` is sufficient to reproduce every claim in -<>. +at its current `main` lets readers inspect the repository content and Git +history cited in <>. Rerun the API checks +above to recheck current GitHub issue, PR, timeline and comment data. The +recorded 403 is specific to the session's token; reproduce it by rerunning the +POST label probe in <> with a token that lacks issue-write +access.