From 7ca95a787e7fc5d0b44f16c9571c6e61444e6b57 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 16:51:57 +0000 Subject: [PATCH 1/3] CI: move the estate-audit pin to cicd-suite #55 (lock record moves with it) The caller was at #50. Upstream since: per-validator ignore lists for manifest-check (#51), a case-insensitive de-onboard fix (#52), new language gates (#54) and a repin of the audit composites (#55). The caller template is unchanged. The lock record moves with the pin; the header comment claimed the lock lists the call as [], which it does not. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- .github/workflows/actions.lock | 8 ++++---- .github/workflows/main-estate-audit.yml | 9 ++++----- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 5376676..21b8852 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -20,7 +20,7 @@ workflows: '.github/workflows/label-triage.yml': [] '.github/workflows/labels.yml': [] '.github/workflows/main-estate-audit.yml': - - 'hyperpolymath/cicd-suite@376898bbe872226866ccbc7648d43123b8bb21b9' + - 'hyperpolymath/cicd-suite@b17ec1af1bbf097d77a58ac3363c4cf5db4d7f4a' '.github/workflows/proofs.yml': - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' '.github/workflows/push-email-notify.yml': @@ -45,9 +45,9 @@ dependencies: commit: 'sha1-b96794f015dfd88f77b49b1c93e0fa7110f94c63' owner_id: 9919 repo_id: 259445878 - 'hyperpolymath/cicd-suite@376898bbe872226866ccbc7648d43123b8bb21b9': - ref: '376898bbe872226866ccbc7648d43123b8bb21b9' - commit: 'sha1-376898bbe872226866ccbc7648d43123b8bb21b9' + 'hyperpolymath/cicd-suite@b17ec1af1bbf097d77a58ac3363c4cf5db4d7f4a': + ref: 'b17ec1af1bbf097d77a58ac3363c4cf5db4d7f4a' + commit: 'sha1-b17ec1af1bbf097d77a58ac3363c4cf5db4d7f4a' owner_id: 6759885 repo_id: 1326697643 'hyperpolymath/smtp-notify-action@v0.2.0': diff --git a/.github/workflows/main-estate-audit.yml b/.github/workflows/main-estate-audit.yml index 041c21e..6e38fa8 100644 --- a/.github/workflows/main-estate-audit.yml +++ b/.github/workflows/main-estate-audit.yml @@ -11,10 +11,9 @@ name: Central Estate CI/CD Audit # is the check. cicd-suite's templates/track-estate-audit.yml can open those # PRs weekly; it needs an AUTOMATION_TOKEN secret. # -# actions.lock lists this file as [], like secret-scanner.yml. A -# cross-repository reusable-workflow call recorded in the lock startup-fails -# with zero jobs under sha_pinning_required (see the header of cicd-suite's -# main-estate-audit.yml). +# actions.lock records this call at the pinned SHA. An untagged pin keeps the +# SHA as `ref`, which job setup accepts; move the lock record together with +# the pin, or the edge dangles and the run startup-fails with zero jobs. on: push: @@ -27,4 +26,4 @@ permissions: jobs: estate: - uses: hyperpolymath/cicd-suite/.github/workflows/main-estate-audit.yml@376898bbe872226866ccbc7648d43123b8bb21b9 # cicd-suite main, #50 + uses: hyperpolymath/cicd-suite/.github/workflows/main-estate-audit.yml@b17ec1af1bbf097d77a58ac3363c4cf5db4d7f4a # cicd-suite main, #55 From c4bfaa16f367258f2239e061852f9d6a90fbb42c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 17:03:22 +0000 Subject: [PATCH 2/3] Docs: T-6 is resolved upstream; the drafted epistemic-types issue is superseded epistemic-types' own kripke-2026-10-12 work added the world-indexed records (Kripke/Indexed) and keeps Warrant, Base and Access builtins-only, so the issue drafted for it was never needed. The one thing it waited for, an immutable external revision plus a type-check for the warrant-soundness theorem, is recorded in hyperpolymath/epistemic-types#41. The ledger row now says the mismatch is resolved upstream and that this repository still carries its own copy of the indexed record. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- PROOF-STATUS.adoc | 2 +- docs/LANDING.adoc | 3 ++- .../epistemic-types_issue-global-soundness-model.adoc | 7 +++++++ 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index e281a18..7aa701e 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -72,7 +72,7 @@ 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' `AccessibleModality` cannot be instantiated as stated: 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)` — field for field otherwise identical (`IndexedAccessible`) — the choreographic frame is a lawful instance with every law by `refl` | PROVEN (`knowledge`); the mismatch is a finding for epistemic-types +| T-6 | epistemic-types' `AccessibleModality` cannot be instantiated as stated: 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)` — field for field otherwise identical (`IndexedAccessible`) — the choreographic frame is a lawful instance with every law by `refl` | PROVEN (`knowledge`); epistemic-types has since added the same world-indexed records (its Kripke/Indexed module), so the mismatch is resolved upstream; this repository still carries its own copy of the indexed record rather than importing theirs |=== == Asynchrony (Async.agda, AsyncKnowledge.agda, AsyncBound.agda) diff --git a/docs/LANDING.adoc b/docs/LANDING.adoc index 63b8733..9660e44 100644 --- a/docs/LANDING.adoc +++ b/docs/LANDING.adoc @@ -19,7 +19,8 @@ Order matters: nothing below is citable until step 6 is green. applications file; `CHANGELOG-entry.adoc` into CHANGELOG. . Cross-repo: nextgen-typing decision record and TYPE-CONNECTIONS rows; absolute-zero T1 exception record (and a ruling on T7); the - epistemic-types issue (`cross-repo/`). occupancy-types: an issue linking + epistemic-types issue (`cross-repo/`, superseded: upstream did the indexed + records itself and its external-verification row is recorded in hyperpolymath/epistemic-types#41). occupancy-types: an issue linking H-2 (its R2–R3 algebra will supersede `Instances/HWM.agda`) and A-3. . CI: both `proofs.yml` files are DESIGNED until their first green run on the Debian `agda-bin=2.6.4.3-1+b2` pin. If the pin fails to install, that diff --git a/docs/cross-repo/epistemic-types_issue-global-soundness-model.adoc b/docs/cross-repo/epistemic-types_issue-global-soundness-model.adoc index 73ae05c..de7f0b8 100644 --- a/docs/cross-repo/epistemic-types_issue-global-soundness-model.adoc +++ b/docs/cross-repo/epistemic-types_issue-global-soundness-model.adoc @@ -1,4 +1,11 @@ // Issue text for hyperpolymath/epistemic-types. +// SUPERSEDED 2026-10-19. This text was never filed. epistemic-types' +// own 2026-10-12 Kripke work (kripke-2026-10-12, #40) already did asks 2 +// and 3: `Kripke/Indexed.agda` has IndexedModality / IndexedFactive / +// IndexedAccessible, and Warrant, Base and Access are builtins-only. Ask 1 is +// the external-verification row of their docs/kripke-status-2026-10-12.adoc; +// hyperpolymath/epistemic-types#41 records the external revision and CI run +// it was waiting for. Kept as the record of what was found. = An external model discharges "global soundness of warrants" for type-determined warrants README lists *global soundness of warrants* and *Kripke semantics* as From 382b0b08b29294810f5178a76d8a72467c461e8d Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 19 Oct 2026 17:22:29 +0000 Subject: [PATCH 3/3] Docs: Ask 1 is the README note; the verification row is its record CodeRabbit on #36: the superseded header called the external-verification row 'Ask 1', but the numbered Ask 1 is recording choreographic-types as an external model in the README. The README note covers Ask 1; the verification row is where its evidence is recorded. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01MF5GeeBBDF6sUzr6pZTjWV --- .../epistemic-types_issue-global-soundness-model.adoc | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/docs/cross-repo/epistemic-types_issue-global-soundness-model.adoc b/docs/cross-repo/epistemic-types_issue-global-soundness-model.adoc index de7f0b8..3263156 100644 --- a/docs/cross-repo/epistemic-types_issue-global-soundness-model.adoc +++ b/docs/cross-repo/epistemic-types_issue-global-soundness-model.adoc @@ -2,10 +2,12 @@ // SUPERSEDED 2026-10-19. This text was never filed. epistemic-types' // own 2026-10-12 Kripke work (kripke-2026-10-12, #40) already did asks 2 // and 3: `Kripke/Indexed.agda` has IndexedModality / IndexedFactive / -// IndexedAccessible, and Warrant, Base and Access are builtins-only. Ask 1 is -// the external-verification row of their docs/kripke-status-2026-10-12.adoc; -// hyperpolymath/epistemic-types#41 records the external revision and CI run -// it was waiting for. Kept as the record of what was found. +// IndexedAccessible, and Warrant, Base and Access are builtins-only. Ask 1 +// (record choreographic-types as an external model in the README) is covered +// by the README note there; its verification record is the external-verification +// row of their docs/kripke-status-2026-10-12.adoc, which +// hyperpolymath/epistemic-types#41 completes with the external revision and CI +// run it was waiting for. Kept as the record of what was found. = An external model discharges "global soundness of warrants" for type-determined warrants README lists *global soundness of warrants* and *Kripke semantics* as