From 9fac4e3a237035c73aaa83cbcd434c05144064f6 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:16:40 +0000 Subject: [PATCH 1/2] docs(status): the epistemic-types pin is 6ce8c74 since #40, not 495db9c PROOF-STATUS.adoc said in three present-tense places that the gate pins epistemic-types at 495db9c; scripts/fetch-siblings.sh pins 6ce8c74 since #40 (2026-11-07). 6ce8c74 contains the indexed-interface commit 5422cd5, but no module here imports EpistemicTypes.Kripke.Indexed yet, so the integration note still stands. docs/LANDING.adoc is updated the same way. Dated records (CHANGELOG entry, pre-registration addendum, the 2026-11-01 audit and toolchain notes) are left as written. Re-check (run in this session): the gate (scripts/fetch-siblings.sh then scripts/check.sh) exits 0 on main with 6ce8c74, and exits 0 at 5a2a6cf, the last commit that pinned 495db9c. Main at 495db9c fails, as expected, because PartialRecovery is newer than that pin. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- PROOF-STATUS.adoc | 11 ++++++----- docs/LANDING.adoc | 3 ++- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 6732615..47ba57c 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -51,8 +51,8 @@ is a layer over the same fragment (section "Asynchrony" below). == K-CUT-WARRANT, bound form (Kripke.agda, Bound.agda) -epistemic-types' `Warrant.agda` is imported (same kernel, pinned commit -495db9c), not re-declared, so "SoundWarrant" below is their record. +epistemic-types' `Warrant.agda` is imported (same kernel; pinned commit +`6ce8c74` since #40, 2026-11-07, previously `495db9c`), not re-declared, so "SoundWarrant" below is their record. [cols="1,3,1",options="header"] |=== @@ -80,8 +80,9 @@ epistemic-types' `Warrant.agda` is imported (same kernel, pinned commit |=== The upstream indexed interface is available at epistemic-types commit -`5422cd5bf1418c44321bf0f77e894737a451d8f5`; the gate still pins -`495db9cca003e12066a3cb9c9f2d7afa1a953aec`. Upstream packages `E` and +`5422cd5bf1418c44321bf0f77e894737a451d8f5`. The gate now pins +`6ce8c74e8a91e5021cb0c1fb4fc805bdff837178` (since #40), which contains it, +but no module here imports `EpistemicTypes.Kripke.Indexed` yet. Upstream packages `E` and `map` in an `IndexedModality` field, so integration requires adapting `knowledge` as well as replacing the local record. See link:docs/toolchain-and-prompts-2026-11-01.md[the pending integration plan]. @@ -222,7 +223,7 @@ warrants is documented precisely: the type provides the warrant structure and type-determined evidence (Kripke knowledge) but not data-dependent evidence or soundness. -epistemic-types' `SoundWarrant` (pinned commit `495db9cc`) is imported, +epistemic-types' `SoundWarrant` (pinned commit `6ce8c74`, previously `495db9cc`) is imported, not re-declared: `Warrant` carries an `Evidence` type; `SoundWarrant` adds `sound : Evidence → A`. A sound warrant alone can have an empty evidence type. The receiver-local side condition therefore also requires diff --git a/docs/LANDING.adoc b/docs/LANDING.adoc index 9660e44..9d2be24 100644 --- a/docs/LANDING.adoc +++ b/docs/LANDING.adoc @@ -13,7 +13,8 @@ Order matters: nothing below is citable until step 6 is green. sibling — the clone's HEAD on 2026-10-12). Open a PR; CodeRabbit and the estate workflows run; address every finding before merge (standing rule). . Fill `RESOURCE_ALGEBRA_COMMIT` in `scripts/fetch-siblings.sh` with the SHA - from step 1; the epistemic-types pin `495db9c` is already set. + from step 1; the epistemic-types pin is already set (`6ce8c74` since #40; + `495db9c` when this guide was written). . Splice `docs/README-keystone-section.adoc` into README (replacing the OPEN keystone section) and `docs/applications-header-patch.adoc` into the applications file; `CHANGELOG-entry.adoc` into CHANGELOG. From 7bc04f2858f8a27d0e27f9a78f9c23f4116eb7ae Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:20:11 +0000 Subject: [PATCH 2/2] docs(proof-status): T-6 pin update is done; warn off the 5422cd5 pin step - T-6 status: the sibling pin 6ce8c74 already contains the upstream Kripke/Indexed module, so only local integration (importing the upstream record and adapting `knowledge`) remains pending. - The note after the transport table now says the pin update is complete and readers should keep 6ce8c74: the historical integration plan's step 1 suggests 5422cd5, which lacks EpistemicTypes.PartialRecovery, which Choreographic.PartialRecovery imports. Only steps 2 to 4 remain. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- PROOF-STATUS.adoc | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 47ba57c..a16a168 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -76,16 +76,20 @@ epistemic-types' `Warrant.agda` is imported (same kernel; pinned commit | T-3 | p-accessibility is exactly sameness of p's projected cut (both directions) | PROVEN (`knows-local-cut`, `local-cut-determines`) | T-4 | Party access `p ⊑ q` ("q sees at least what p sees") is a preorder — epistemic-types' `Preorder` record, instantiated — and knowledge is monotone along it | PROVEN (`party-access`, `knows-mono`) | T-5 | A silent party is below every party; knowledge flows up the preorder only — `1 ⊑ 2` for the witness protocol is refused | PROVEN (`silent-⊑`, `inherited`); TESTED (`tests/reject/AccessWrongWay`) -| T-6 | epistemic-types' unindexed `AccessibleModality` cannot express this frame directly: its `E : K → Set → Set` has no world index, and world-free knowledge collapses to the proposition itself (reflexivity). With `E : K → (World → Set) → (World → Set)` in the local `IndexedAccessible` record, the choreographic frame is a lawful instance with every law by `refl` | PROVEN (`knowledge`); the current sibling pin lacks the upstream Kripke/Indexed module. The newer upstream interface exists, but updating the pin and adapting this local instance remain pending +| T-6 | epistemic-types' unindexed `AccessibleModality` cannot express this frame directly: its `E : K → Set → Set` has no world index, and world-free knowledge collapses to the proposition itself (reflexivity). With `E : K → (World → Set) → (World → Set)` in the local `IndexedAccessible` record, the choreographic frame is a lawful instance with every law by `refl` | PROVEN (`knowledge`); the sibling pin 6ce8c74 contains the upstream Kripke/Indexed module, but this repository still uses the local record. Only local integration (importing the upstream record and adapting `knowledge`) remains pending |=== -The upstream indexed interface is available at epistemic-types commit -`5422cd5bf1418c44321bf0f77e894737a451d8f5`. The gate now pins -`6ce8c74e8a91e5021cb0c1fb4fc805bdff837178` (since #40), which contains it, -but no module here imports `EpistemicTypes.Kripke.Indexed` yet. Upstream packages `E` and -`map` in an `IndexedModality` field, so integration requires adapting -`knowledge` as well as replacing the local record. See -link:docs/toolchain-and-prompts-2026-11-01.md[the pending integration plan]. +The upstream indexed interface was first verified at epistemic-types commit +`5422cd5bf1418c44321bf0f77e894737a451d8f5`. The pin update is complete: the +gate pins `6ce8c74e8a91e5021cb0c1fb4fc805bdff837178` (since #40), which contains +`EpistemicTypes.Kripke.Indexed`, but no module here imports it yet. Upstream +packages `E` and `map` in an `IndexedModality` field, so integration requires +adapting `knowledge` as well as replacing the local record. The historical +link:docs/toolchain-and-prompts-2026-11-01.md[integration plan] predates the +pin update and suggests pinning `5422cd5`; do not follow that step. `5422cd5` +lacks `EpistemicTypes.PartialRecovery`, which `Choreographic.PartialRecovery` +imports, so keep the pin at `6ce8c74`. Only steps 2 to 4 of that plan (the +local integration) remain. == Asynchrony (Async.agda, AsyncKnowledge.agda, AsyncBound.agda)