chore(proofs): reconcile Grade 3 policy and proof status

.devcontainer/README.adoc

@@ -6,9 +6,10 @@
 `.devcontainer/Containerfile` builds a Debian 13 image pinned to the same base
 digest as the repository's Proof Safety workflow, and installs the same Agda
 (`agda-bin=2.6.4.3-1+b2`) plus `bash`, `git`, `just`, `make` and `ripgrep`
-(`tests/check-rejections.sh` needs `rg`). `devcontainer.json` runs `just check`
-once, after creation, so a fresh container either reproduces the positive and
-expected-rejection proof gates or reports the failing gate.
+(`tests/check-policy.sh` and `tests/check-rejections.sh` need `rg`).
+`devcontainer.json` runs `just check` once after creation, so a fresh container
+reproduces the policy guard, all 22 positive modules and all 13
+expected-rejection controls, or reports the failing gate.
 
 == Usage
 

.github/CONTRIBUTING.md

@@ -3,15 +3,15 @@
 `epistemic-types` is a small, deliberately honest Agda formalization of
 standpoint-indexed modal / epistemic / echo-like type formers. It
 favours mathematical honesty over a large API. Contributions are
-welcome, but the bar is **everything still type-checks under `--safe`
-`--without-K`, with no shortcuts**.
+welcome, but the bar is **everything still passes the canonical
+`--safe --without-K --cubical-compatible` profile, with no shortcuts**.
 
 - **Author:** Jonathan D.A. Jewell (hyperpolymath)
-  [j.d.a.jewell@open.ac](j.d.a.jewell@open.ac).uk
+  [j.d.a.jewell@open.ac.uk](mailto:j.d.a.jewell@open.ac.uk)
 
 - **Version:** 0.1.0 (status: prototype)
 
-- **Last updated:** 2026-06-15
+- **Last updated:** 2026-11-01
 
 ’’’’’
 
@@ -21,8 +21,8 @@ epistemic-types follows the estate-wide **Tri-Perimeter Contribution
 Framework (TPCF)** — graduated trust without gatekeeping:
 
 - **Perimeter 1 — Core Systems (maintainers only).** The proof kernel:
-  `src/EpistemicTypes/*.agda` (Base, Access, Warrant, ProofTransport,
-  the EchoBridge/SurrealBridge), the `All.agda` wiring, and build
+  all 22 modules recursively under `src/EpistemicTypes/` (core,
+  applications, and Kripke semantics), the `All.agda` wiring, and proof
   tooling.
 
 - **Perimeter 2 — Expert Extensions (trusted contributors).** New
@@ -35,9 +35,9 @@ Framework (TPCF)** — graduated trust without gatekeeping:
 ### Fork workflow
 
 External contributors use the standard **fork**-and-pull-request
-workflow: fork the repository, branch from `main`, run `just` `check`
-(the full `--safe` `--without-K` type-check) locally, and open a PR.
-Proofs are load-bearing — a red `agda` check blocks merge, and no
+workflow: fork the repository, branch from `main`, run `just check`
+(the policy gate, all positive modules, and all expected rejections) locally,
+and open a PR. Proofs are load-bearing — a red `agda` check blocks merge, and no
 `postulate` / `believe_me` shortcuts are accepted.
 
 ## Build and check
@@ -46,9 +46,10 @@ The combined proof and rejection gate must stay green:
 
     just check
 
-This checks every source module (including `All.agda`) and runs
-`tests/check-rejections.sh`. Deliberate rejection fixtures stay outside
-the positive `All.agda` import graph.
+This runs `tests/check-policy.sh`, checks all 22 source modules recursively,
+and validates all 13 expected-rejection fixtures. Deliberate rejection
+fixtures stay outside the positive `All.agda` import graph; coverage does not
+depend on `All.agda` alone.
 
 Requirements:
 
@@ -61,9 +62,10 @@ Requirements:
   `check-canonical`; its dependencies stay outside the default core
   gate.
 
-`All.agda` imports every core module, so `just` `check` checks the whole
-library. A change is not done until `just` `check` passes with no errors
-and no warnings.
+`All.agda` imports the full graph, but the gate also checks every source file
+independently so an omitted aggregate import cannot hide a module. A change is
+not done until `just check` passes with no errors and no warnings outside the
+single documented `UnsupportedIndexedMatch` transport-computation category.
 
 CI checks every source module, semantic rejection controls and pinned
 canonical Echo correspondence. Proof and security gates must pass before
@@ -84,13 +86,14 @@ merged.
   `BeliefModality`), so the assumption is visible at the type level
   rather than smuggled in.
 
-- **No standard library.** As above: `Agda.Builtin.*` and
-  `Agda.Primitive` only.
+- **No standard library in core source.** As above: `Agda.Builtin.*`,
+  `Agda.Primitive`, and local modules only. The optional pinned integration is
+  a separate boundary.
 
-- **`--safe` `--without-K`.** Every module compiles under `{-#`
-  `OPTIONS` `--safe` `--without-K` `#-}`. This rules out `postulate`,
-  unsafe pragmas, axiom K, and `--type-in-type`. Do not weaken these
-  options.
+- **Complete strict profile.** Every first-party module starts with
+  `{-# OPTIONS --safe --without-K --cubical-compatible --exact-split
+  --no-sized-types --no-guardedness #-}`. The command line repeats the first
+  three canonical flags. Do not weaken or partially restate this profile.
 
 - **No too-strong rules.** Keep the interfaces as weak as the proofs
   allow. The base form `E` `:` `K` `→` `Set` `ℓ` `→` `Set` `ℓ` is a
@@ -129,15 +132,15 @@ these separations when extending:
 
 ## Adding a module or lemma
 
-1.  Put Agda source under `src/EpistemicTypes/` and add the new module
-    to the `import`/re-export list in `src/EpistemicTypes/All.agda` so
-    `just` `check` covers it.
+1.  Put Agda source under `src/EpistemicTypes/` and wire it into
+    `src/EpistemicTypes/All.agda` where the full graph requires it. The
+    recursive gate will detect the new module; update the explicit 22-module
+    policy/metadata inventory in the same change rather than bypassing it.
 
-2.  Open each module with `{-#` `OPTIONS` `--safe` `--without-K` `#-}`.
+2.  Open each module with the exact complete strict `OPTIONS` line shown above.
 
-3.  Keep modules small and single-purpose, mirroring the existing
-    layout: `Base`, `Warrant`, `Access`, `EchoBridge`, `SurrealBridge`,
-    `ProofTransport`, `ProofTransportExample`, `Examples`.
+3.  Keep modules small and single-purpose, following the existing core,
+    `Applications/`, and `Kripke/` layout.
 
 4.  State assumptions as interface fields, not postulates. Add lawful
     instances only after the laws are proved or explicitly required as
@@ -156,8 +159,9 @@ keep the Agda model and the machine-readable description in step.
 - **AsciiDoc (`.adoc`) is the default** for documentation. Update the
   relevant `.adoc` file alongside any behavioural or interface change.
 
-- Existing docs keep their current names: `README.adoc` and
-  `explainme.adoc`. Do **not** rename or duplicate them.
+- Preserve exact current names and roles: `README.adoc` is the overview,
+  `explainme.adoc` the concise narrative, and `EXPLAINME.adoc` the detailed
+  claims/evidence ledger.
 
 - Machine-readable descriptions live under `.machine_readable/` (a2ml +
   Nickel/k9). a2ml files use the canonical TOML-like dialect:
@@ -230,10 +234,9 @@ check.
 
 ## Licence note
 
-The licence is owner-managed. Do **not** add `LICENSE`,
-`SPDX-License-Identifier` headers, or copyright header lines in a PR.
-The repo is currently SPDX-free and stays consistent; licensing is
-handled separately by the owner.
+The licence and existing SPDX declarations are owner-managed. Do **not** add,
+remove, or alter licence files, SPDX identifiers, or copyright lines without
+explicit owner instruction.
 
 ’’’’’
 
@@ -242,8 +245,9 @@ handled separately by the owner.
 `epistemic-types` sits alongside (and should stay coherent with) these
 estate repos:
 
-- **echo-types** — Agda loss-with-residue formalism; `EchoBridge`
-  composes with it. Audit it before duplicating echo machinery here.
+- **echo-types** — canonical proof-relevant Echo sibling. The optional pin
+  checks representation and one-way lowering; Echo is not a resource instance.
+  Audit it before duplicating Echo machinery here.
 
 - **ephapax** — sibling formal language (four-layer redesign with echo
   obligations).

.github/workflows/agda.yml

@@ -38,9 +38,22 @@ jobs:
         with:
           persist-credentials: false
       - name: Verify toolchain and proof constructions
+        shell: bash
         run: |
           test "$(agda --version)" = 'Agda version 2.6.4.3'
-          bash scripts/check.sh
+          set +e
+          output=$(bash scripts/check.sh 2>&1)
+          status=$?
+          set -e
+          printf '%s\n' "$output"
+          if [ "$status" -ne 0 ]; then
+            annotation=$(tail -n 20 <<< "$output")
+            annotation=${annotation//'%'/'%25'}
+            annotation=${annotation//$'\r'/'%0D'}
+            annotation=${annotation//$'\n'/'%0A'}
+            printf '::error title=Canonical proof gate::%s\n' "$annotation"
+            exit "$status"
+          fi
 
   echo:
     name: Canonical Echo correspondence
@@ -65,7 +78,7 @@ jobs:
       - name: Prove representation round trips and lowering agreement
         run: |
           test "$(agda --version)" = 'Agda version 2.6.4.3'
-          agda --no-libraries --safe --without-K --double-check --ignore-interfaces \
+          agda --no-libraries --safe --without-K --cubical-compatible --double-check --ignore-interfaces \
             -W error -W noUnsupportedIndexedMatch -i src -i tests/integration \
             -i .ci-deps/echo-types/proofs/agda -i /usr/share/agda-stdlib/src \
             tests/integration/CanonicalEcho.agda

.machine_readable/descriptiles/0-AI-MANIFEST.a2ml

@@ -6,13 +6,13 @@ project = "epistemic-types"
 repo = "hyperpolymath/epistemic-types"
 version = "0.1.0"
 status = "prototype"
-last-updated = "2026-06-15"
+last-updated = "2026-11-01"
 author = "Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>"
 
 [purpose]
 summary = "Agda prototypes for standpoint-indexed modal, epistemic, and echo-like type formers."
 stance = "Favours mathematical honesty over a large API."
-detail = "A small, deliberately honest Agda formalization. Constructive; compiles under {-# OPTIONS --safe --without-K #-}. No postulates. No Agda standard library (built with 'agda --no-libraries', using only Agda.Builtin.* / Agda.Primitive)."
+detail = "A small, deliberately honest Agda formalization. All first-party modules declare --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness. Core source has no postulates, escape hatches or standard-library imports."
 core-form = "E : K -> Set ℓ -> Set ℓ. E κ A reads 'A is epistemically available at standpoint κ'."
 base-interface = "A plain indexed endofunctor (map only) — NOT a monad/comonad; no generic return/reflect."
 
@@ -26,7 +26,7 @@ echo_distinction = "Echo values have explicit retention certificates; resource b
 no_collapse = "Do not collapse Echo C y and E κ A. Their composition is meaningful, but they are not the same modality."
 
 [typecheck]
-command = "bash tests/check-proofs.sh && bash tests/check-rejections.sh"
+command = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh"
 just-target = "just check"
 agda-version = "2.6.4.3"
 
@@ -36,6 +36,6 @@ agda-version = "2.6.4.3"
 present = ["0-AI-MANIFEST.a2ml", "AGENTIC.a2ml", "ECOSYSTEM.a2ml", "META.a2ml", "NEUROSYM.a2ml", "PLAYBOOK.a2ml", "README.adoc", "STATE.a2ml"]
 
 [invariants]
-single-source-of-truth = "This directory is authoritative; no duplicate metadata in the root directory."
+single-source-of-truth = "This directory is authoritative; the root 0-AI-MANIFEST.a2ml is a universal pointer and must agree with it."
 no-stale-metadata = true
 ci = "Proof and security workflows configured; see docs/ci-safety.adoc."

.machine_readable/descriptiles/AGENTIC.a2ml

@@ -7,7 +7,7 @@ repository = "hyperpolymath/epistemic-types"
 author = "Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>"
 version = "0.1.0"
 status = "prototype"
-last-updated = "2026-06-15"
+last-updated = "2026-11-01"
 
 [agent-permissions]
 can-edit-source = true        # Agda modules under src/EpistemicTypes/
@@ -16,15 +16,17 @@ can-edit-machine-readable = true  # .machine_readable/ (descriptiles, proof-tran
 can-edit-build = true         # Justfile, epistemic-types.agda-lib, .gitignore
 can-create-files = true
 can-edit-license = false      # LICENSE / SPDX are owner-manual — agents MUST NOT touch
-can-add-spdx-headers = false  # repo is intentionally SPDX-free; keep it consistent
+can-add-spdx-headers = false  # licensing declarations remain owner-managed
 
 [agent-constraints]
 # What AI agents must NOT do in this repository:
 # Honesty discipline (the whole point of the library):
 # - Never add a postulate. There are zero postulates and that is load-bearing.
-# - Never weaken the pragma: keep {-# OPTIONS --safe --without-K #-} everywhere.
-# - Never import an Agda standard library. Build stays `agda --no-libraries`;
-#   only Agda.Builtin.* and Agda.Primitive are permitted.
+# - Never weaken the full strict pragma: --safe --without-K --cubical-compatible
+#   --exact-split --no-sized-types --no-guardedness.
+# - Never import an Agda standard library into core source. Build stays
+#   `agda --no-libraries`; only Agda.Builtin.*, Agda.Primitive and local modules
+#   are permitted. The separately pinned CanonicalEcho integration is the exception.
 # - Never introduce a too-strong rule. The base interface E : K -> Set ℓ -> Set ℓ
 #   is a plain indexed endofunctor (map only). Do NOT add a generic return,
 #   reflect, join, or extract that is not justified by an explicit field or proof.
@@ -55,10 +57,10 @@ release-claim-requires-hard-pass = true
 [verification]
 # The single source of truth for "does it hold".
 command = "just check"
-underlying = "bash tests/check-proofs.sh && bash tests/check-rejections.sh"
+underlying = "bash tests/check-policy.sh && bash tests/check-proofs.sh && bash tests/check-rejections.sh"
 agda-version = "2.6.4.3"
-entrypoint = "src/EpistemicTypes/All.agda"
-expected = "type-checks clean, no postulates, no warnings"
+entrypoint = "scripts/check.sh (recursive source gate; All.agda is the aggregate module)"
+expected = "22 source modules accepted, 13 intended rejections, strict profile/import/escape-hatch policy and planted-postulate control pass"
 
 [automation-hooks]
 # on-enter: Read 0-AI-MANIFEST.a2ml, then STATE.a2ml.

.machine_readable/descriptiles/ECOSYSTEM.a2ml

@@ -5,19 +5,19 @@ project = "epistemic-types"
 ecosystem = "hyperpolymath"
 version = "0.1.0"
 status = "prototype"
-last-updated = "2026-06-15"
+last-updated = "2026-11-01"
 
 [position]
 type = "formal-methods-library"
 purpose = "A small, deliberately honest Agda formalization of standpoint-indexed modal / epistemic / echo-like type formers. Favours mathematical honesty over a large API: constructive, no postulates, no standard library."
 
 [stack]
 language = "Agda 2.6.4.3"
-options = "--safe --without-K"
-libraries = "none — built with 'agda --no-libraries' against Agda.Builtin.* and Agda.Primitive only"
+options = "--safe --without-K --cubical-compatible; source also declares --exact-split --no-sized-types --no-guardedness"
+libraries = "core: none — --no-libraries against Agda.Builtin.*, Agda.Primitive and local modules; optional CanonicalEcho integration has pinned external source/stdlib"
 machine-readable = "a2ml + Nickel/k9"
 docs = "AsciiDoc"
-check = "just check  ==  agda --no-libraries -i src src/EpistemicTypes/All.agda"
+check = "just check == policy inventory/negative control + all 22 source modules + all 13 expected rejections"
 notes = "Single-tool Agda library. The core has no runtime dependencies; CI uses a pinned Debian verification container."
 
 [core]
@@ -32,7 +32,10 @@ modules = [
   "EpistemicTypes.Examples",
   "EpistemicTypes.ProofTransport — standpoint-indexed proof transport across trust boundaries",
   "EpistemicTypes.ProofTransportExample — a K9-SVC / A2ML attestation scenario",
-  "EpistemicTypes.All — re-export aggregator"
+  "EpistemicTypes.ReadConsistency and ContinuityExamples — pure store history, freshness and continuity witnesses",
+  "EpistemicTypes.Applications.* — six modules for the RapidNJ bound, integer instance and skip warrants",
+  "EpistemicTypes.Kripke.* — five modules for indexed Box/frame correspondences, non-factive belief, residual candidates and dependence",
+  "EpistemicTypes.All — full-graph import; public re-export is deliberately narrower"
 ]
 
 [proof-transport]
@@ -43,8 +46,11 @@ no-smuggling = "proofNeedsChecker: no checker-free Proof -> Proof transport is e
 
 [related-projects]
 projects = [
-  { name = "echo-types", relationship = "sibling-formalism", notes = "Agda loss-with-residue (min-plus graded) formalism. EpistemicTypes.EchoBridge's 'Echo C y' composes with it; kept deliberately distinct from the epistemic E κ A modality (no collapse)." },
+  { name = "echo-types", relationship = "sibling-formalism", notes = "Agda proof-relevant fibre/residue formalism. Canonical Echo can be lowered one-way into separately measured resource evidence, but Echo is not a resource instance. The local bridge checks representation/lowering at a pin and does not collapse Echo into E κ A." },
   { name = "ephapax", relationship = "sibling-formal-language", notes = "Sibling formal language; its four-layer redesign carries echo obligations. Echo / standpoint vocabulary is shared at the conceptual level, not via a code dependency." },
+  { name = "choreographic-types", relationship = "external-proof-consumer", notes = "Imports the warrant interface and proves scoped finite binary/plain-merge K-CUT results, including asynchronous variants. Data-dependent warrants and generalized fragments remain open; not a local dependency." },
+  { name = "residual-evidence-types", relationship = "research-neighbour", notes = "Operated in production; its mathematical/API maturity remains early research with no stable API despite checked composition/revision/finite-checker progress. The local dependence result is a mirror, not an imported identity." },
+  { name = "secret-types", relationship = "standalone-boundary", notes = "Owns confidentiality labels and generic TINI. No Secret API or IFC theorem belongs here; termination-sensitive noninterference and declassification remain open there." },
   { name = "standards", relationship = "estate-foundation", notes = "Estate RSR / standards repo plus k9-svc and a2ml tooling. Supplies the descriptiles layout and the contractile / k9 rendering conventions this repo's .machine_readable mirrors." },
   { name = "a2ml + k9", relationship = "rendering-target", notes = "Machine-readable a2ml + Nickel/k9 contractile tooling. The engineering rendering target for ProofTransport: the standpoint-indexed proof-transport core is rendered to a2ml/k9 under .machine_readable/proof-transport/." }
 ]