Skip to content

docs(status): the epistemic-types pin is 6ce8c74 since #40, not 495db9c #42

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
hyperpolymath wants to merge 2 commits into
base: main
Choose a base branch
from
+17 −11
Open

docs(status): the epistemic-types pin is 6ce8c74 since #40, not 495db9c #42

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9fac4e3
docs(status): the epistemic-types pin is 6ce8c74 since #40, not 495db9c
claude Nov 9, 2026
7bc04f2
docs(proof-status): T-6 pin update is done; warn off the 5422cd5 pin …
claude Nov 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 15 additions & 10 deletions PROOF-STATUS.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
|===
Expand All @@ -76,15 +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 still pins
`495db9cca003e12066a3cb9c9f2d7afa1a953aec`. 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)

Expand Down Expand Up @@ -222,7 +227,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
Expand Down
3 changes: 2 additions & 1 deletion docs/LANDING.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Loading